58.17 Restriction to a closed… to 58.32 Tricks in positive…

Section58.17 Restriction to a closed subscheme #

Section 58.17 of the Stacks Project, Tag 0EJW. 7 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0EL8, a lemma

Tag 0EL8 in the Stacks Project.

Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_of_completionFullyFaithfulOnFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/RestrictionToClosedSubscheme.lean, line 1052. The attribute's comment: “proved from full faithfulness of completion on the finite locally free coherent modules alone”.

Let X be a Noetherian scheme and Y ⊆ X a closed subscheme with ideal sheaf I. If the completion functor Coh(𝒪_X) ⟶ Coh(X, I) is fully faithful on the full subcategory of finite locally free objects, then the restriction functor FÉt_X ⟶ FÉt_Y is fully faithful.

public theorem fullyFaithful_finiteEtaleBaseChange_of_completionFullyFaithfulOnFiniteLocallyFree
    {X Y : Scheme.{u}} (i : Y ⟶ X) [IsNoetherian X] [IsClosedImmersion i]
    (hcompletion : Stacks.Algebraization.CompletionFullyFaithfulOnFiniteLocallyFree X i.ker) :
    Nonempty (finiteEtaleBaseChange i).FullyFaithful

Tag 0EL9, a lemma

Tag 0EL9 in the Stacks Project.

Stacks.FundamentalGroup.finiteEtaleBaseChange_isEquivalence_of_completionEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/RestrictionEquivalenceOfCompletion.lean, line 2994. The attribute's comment: “completion an equivalence on finite locally free objects implies restriction FEt_X to FEt_Y an equivalence”.

[Stacks, Tag 0EL9]. Let X be a Noetherian scheme and Y ⊆ X a closed subscheme with ideal sheaf I. If the completion functor Coh(𝒪_X) ⥤ Coh(X, I), ℱ ↦ ℱ^∧, is an equivalence on the full subcategories of finite locally free objects, then the restriction functor FÉt_X ⥤ FÉt_Y, U ↦ U ×_X Y, is an equivalence.

The closed subscheme is given by a closed immersion i : Y ⟶ X with ideal sheaf I = ker i. Restriction factors as restriction to the closed subscheme cut out by I followed by base change along the isomorphism from Y onto it, and the second is an equivalence because an isomorphism is a thickening ([Stacks, Tag 0BQB]); the first is Stacks.FundamentalGroup.finiteEtaleBaseChange_isEquivalence_of_completion.

public theorem finiteEtaleBaseChange_isEquivalence_of_completionEquivalence
    {X Y : Scheme.{u}} (i : Y ⟶ X) [IsNoetherian X] [IsClosedImmersion i]
    [(finiteLocallyFreeCompletion X i.ker).IsEquivalence] :
    (AlgebraicGeometry.finiteEtaleBaseChange i).IsEquivalence

Tag 0ELA, a lemma

Tag 0ELA in the Stacks Project.

Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_of_sectionsExtendNearSubscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/RestrictionFromNeighborhoods.lean, line 366. The attribute's comment: “granted SectionsExtendNearSubscheme: the shrinking form of Tag 0EL8”.

[Stacks, Tag 0ELA], granted the section-extension input. Let X be a scheme, let Y ⊆ X be the closed subscheme cut out by the ideal sheaf Y, and let 𝒱 be the open subschemes of X containing it, ordered by reverse inclusion. If sections of a finite étale cover of a neighbourhood extend to a smaller neighbourhood and are determined there after further shrinking, then the restriction functor colim_𝒱 FÉt_V ⟶ FÉt_Y is fully faithful.

This is the first paragraph of the source's proof, which is the only part of it that is about finite étale covers: the category of finite étale coverings has an internal hom ([Stacks, Tag 0BL7]), and a section of the internal hom Hom_V(A, B) over a base is exactly a morphism A ⟶ B after that base change, so a morphism between the restrictions to the closed subscheme is a section of the internal hom over the closed subscheme and full faithfulness over the colimit is the extension property for sections of one finite étale cover.

What is granted and what is not. The hypothesis of the tag — full faithfulness of the completion functor colim_𝒱 Coh(𝒪_V) ⟶ Coh(X, I) on the finite locally free objects — is not used here at all: the section-extension property Stacks.FundamentalGroup.SectionsExtendNearSubscheme is assumed in its place. That property is the shrinking form of the conclusion of [Stacks, Tag 0EL8], and deducing it from the completion hypothesis is the rest of the source's proof: lift the section over the closed subscheme to the infinitesimal neighbourhoods ([Stacks, Tag 0BQB]), algebraize the resulting compatible system of module maps out of the finite locally free module f _* 𝒪_U over some smaller neighbourhood by fullness of completion, and shrink once more to make the algebraized map multiplicative by faithfulness of completion. That half is carried in this library only in its non-shrinking form, on the nose at a single scheme, as Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_of_completionFullyFaithful; the shrinking form would need the restriction of a direct image algebra to an open subscheme and the comparison of the infinitesimal neighbourhoods of the closed subscheme taken inside X and inside a neighbourhood, neither of which has a carrier here.

It is not enough to assume the pointwise analogue of the hypothesis at each individual neighbourhood, which would make the statement a formal consequence of Tag 0EL8 applied one neighbourhood at a time. The quantifiers over smaller neighbourhoods in both SectionsExtendNearSubscheme and FiniteEtaleColimitFullyFaithful are the content.

theorem finiteEtaleColimitFullyFaithful_of_sectionsExtendNearSubscheme
    (h : SectionsExtendNearSubscheme X Y) : FiniteEtaleColimitFullyFaithful X Y

Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_of_completionFullyFaithfulComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/SectionsExtendFromCompletion.lean, line 632. The attribute's comment: “proved from full faithfulness of completion on the finite locally free objects of the neighbourhood colimit, the tag's own hypothesis”.

[Stacks, Tag 0ELA]. Let X be a Noetherian scheme and let Y ⊆ X be a closed subscheme with ideal sheaf I. Let 𝒱 be the set of open subschemes V ⊆ X containing Y, ordered by reverse inclusion. Assume the completion functor colim_𝒱 Coh(𝒪_V) ⟶ Coh(X, I), ℱ ↦ ℱ^∧, is fully faithful on the full subcategory of finite locally free objects. Then the restriction functor colim_𝒱 FÉt_V ⟶ FÉt_Y is fully faithful.

The hypothesis is condition (4) of [Stacks, Tag 0EK2], Stacks.Algebraization.NeighbourhoodCompletion.CompletionFullyFaithfulComplete, at the closed immersion of Y; the conclusion is Stacks.FundamentalGroup.FiniteEtaleColimitFullyFaithful, full faithfulness spelled through the directed-colimit description of the hom sets of colim_𝒱 FÉt_V. The proof is the source's: the internal hom reduces the statement to the extension of sections of one finite étale cover (finiteEtaleColimitFullyFaithful_of_sectionsExtendNearSubscheme), and that extension is sectionsExtendNearSubscheme_of_completionFullyFaithfulComplete.

theorem finiteEtaleColimitFullyFaithful_of_completionFullyFaithfulComplete [IsNoetherian X]
    (h : NeighbourhoodCompletion.CompletionFullyFaithfulComplete Y.subschemeι) :
    FiniteEtaleColimitFullyFaithful X Y

Tag 0EK1, a lemma

Tag 0EK1 in the Stacks Project.

Stacks.FundamentalGroup.isEquivalence_restrictionFunctor_of_fullyFaithful_of_essentialImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/RestrictionColimitEquivalence.lean, line 288. The attribute's comment: “granted Stacks 0ELA for full faithfulness and the essential image of restriction”.

[Stacks, Tag 0EK1]. Let X be a Noetherian scheme, Y ⊆ X a closed subscheme with ideal sheaf I, and 𝒱 the open subschemes of X containing Y, ordered by reverse inclusion. If the completion functor colim_𝒱 Coh(𝒪_V) ⟶ Coh(X, I), ℱ ↦ ℱ^∧, is an equivalence of the full subcategories of finite locally free objects, then the restriction functor colim_𝒱 FÉt_V ⟶ FÉt_Y is an equivalence.

The hypothesis is carried through the two consequences the source draws from it, because it cannot be stated here: the finite locally free objects of Coh(X, I) and the comparison of Coh(X, I) with Coh(V, I|_V) for a neighbourhood V are both absent from this library. The first consequence, h0ELA, is full faithfulness of the restriction functor, which the source obtains from the fully faithful half of the hypothesis by [Stacks, Tag 0ELA]. The second, hessImage, is that every finite étale cover of Y is the restriction of a finite étale cover of some neighbourhood; the source obtains it by algebraizing the tower π_{n, *}𝒪_{U_n} of pushed forward structure sheaves of the covers of the infinitesimal neighbourhoods, which is a finite locally free object of Coh(X, I), transporting the algebra structure along the equivalence, and taking the relative spectrum, which is étale near Y by More on Morphisms, Tag 0A43. What is proved here is that the second consequence gives essential surjectivity of the functor out of the colimit.

public theorem isEquivalence_restrictionFunctor_of_fullyFaithful_of_essentialImage
    {X : Scheme.{u}} [IsNoetherian X] (Y : X.IdealSheafData)
    (P : FiniteEtaleColimitPresentation X Y) [HasColimit P.diagram]
    (h0ELA : Nonempty P.restrictionFunctor.FullyFaithful)
    (hessImage : ∀ A : FiniteEtaleOver Y.subscheme, ∃ (W : Neighborhood X Y)
      (U : FiniteEtaleOver (Neighborhood.open X Y W).toScheme),
      Nonempty ((finiteEtaleBaseChange (Neighborhood.toSchemeHom X Y W)).obj U ≅ A)) :
    P.restrictionFunctor.IsEquivalence

Stacks.FundamentalGroup.restriction_isEquivalence_of_completionEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/RestrictionColimitEquivalenceOfCompletion.lean, line 98. The attribute's comment: “the colimit functor is an equivalence: fully faithful, and every finite étale cover of Y extends to a neighbourhood”.

[Stacks, Tag 0EK1]. Let X be a Noetherian scheme, Y ⊆ X a closed subscheme with ideal sheaf I, and 𝒱 the open subschemes of X containing Y, ordered by reverse inclusion. If the completion functor colim_𝒱 Coh(𝒪_V) ⟶ Coh(X, I) defines an equivalence of the full subcategories of finite locally free objects, then the restriction functor colim_𝒱 FÉt_V ⟶ FÉt_Y is an equivalence: it is fully faithful in the directed-colimit sense of FiniteEtaleColimitFullyFaithful, and every finite étale cover of Y is the restriction of a finite étale cover of some V ∈ 𝒱.

public theorem restriction_isEquivalence_of_completionEquivalence [IsNoetherian X]
    (h : CompletionEquivalenceFiniteLocallyFree X Y) :
    FiniteEtaleColimitFullyFaithful X Y ∧
      ∀ A : FiniteEtaleOver Y.subscheme, ∃ (W : Neighborhood X Y)
        (U : FiniteEtaleOver (Neighborhood.open X Y W).toScheme),
        Nonempty ((finiteEtaleBaseChange (Neighborhood.toSchemeHom X Y W)).obj U ≅ A)

Tag 0EJX, a lemma

Tag 0EJX in the Stacks Project.

Stacks.FundamentalGroup.faithful_finiteEtaleRestriction_of_components_meet, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/FiniteEtaleMorphisms/Restriction.lean, line 102.

Stacks Project, Tag 0EJX. Restriction of finite étale schemes to a closed subscheme meeting every connected component is faithful.

public lemma faithful_finiteEtaleRestriction_of_components_meet
    {X Y : Scheme.{u}} (f : Y ⟶ X) [IsClosedImmersion f]
    (h : ∀ c : ConnectedComponents X,
      ∃ y : Y, ConnectedComponents.mk (f.base y) = c) :
    (MorphismProperty.Over.pullback
      ((@IsFinite ⊓ @Etale) : MorphismProperty Scheme.{u}) ⊤ f).Faithful

Tag 0EJZ, a lemma

Tag 0EJZ in the Stacks Project.

Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_of_sectionsComplete_of_or, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/RestrictionSectionwiseComplete.lean, line 80.

[Stacks, Tag 0EJZ]. Let X be a Noetherian scheme and Y ⊆ X a closed subscheme, with infinitesimal neighbourhoods Y_n ⊆ X. Assume one of the following holds:

X is quasi-affine and Γ(X, 𝒪_X) → lim Γ(Y_n, 𝒪_{Y_n}) is an isomorphism, or

X has an ample invertible module L and Γ(X, L^{⊗ m}) → lim Γ(Y_n, L^{⊗ m}|_{Y_n}) is an isomorphism for all m ≫ 0, or

for every finite locally free 𝒪_X-module ℰ the map Γ(X, ℰ) → lim Γ(Y_n, ℰ|_{Y_n}) is an isomorphism.

Then the restriction functor FÉt_X ⟶ FÉt_Y is fully faithful.

As in the source, cases (1) and (2) are reduced to case (3) by the implications (1) ⇒ (2) ⇒ (3) of [Stacks, Tag 0EKP], case (3) gives full faithfulness of completion on finite locally free modules by (3) ⇒ (4) of the same tag, and [Stacks, Tag 0EL8] concludes.

public theorem fullyFaithful_finiteEtaleBaseChange_of_sectionsComplete_of_or
    {X Y : Scheme.{u}} (i : Y ⟶ X) [IsNoetherian X] [IsClosedImmersion i]
    (h : SectionsCompleteQuasiAffine i ∨ SectionsCompleteAmplePowers i ∨
      SectionsCompleteFiniteLocallyFree i) :
    Nonempty (finiteEtaleBaseChange i).FullyFaithful

Stacks.FundamentalGroup.bijective_map_finiteEtaleBaseChange_of_sectionsComplete_of_or, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/RestrictionSectionwiseComplete.lean, line 105. The attribute's comment: “restated as bijectivity on hom sets”. References: SGA 2 X (2.5), “special case”.

[Stacks, Tag 0EJZ], restated as bijectivity on hom sets. Under any one of the three conditions of Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_of_sectionsComplete_of_or, restriction of finite étale covers of X to the closed subscheme Y is bijective on every hom set.

CategoryTheory.Functor.FullyFaithful carries the inverse map on hom sets as data, so full faithfulness is recorded as Nonempty _.FullyFaithful; CategoryTheory.Functor.FullyFaithful.nonempty_iff_map_bijective turns it into bijectivity on hom sets.

public theorem bijective_map_finiteEtaleBaseChange_of_sectionsComplete_of_or
    {X Y : Scheme.{u}} (i : Y ⟶ X) [IsNoetherian X] [IsClosedImmersion i]
    (h : SectionsCompleteQuasiAffine i ∨ SectionsCompleteAmplePowers i ∨
      SectionsCompleteFiniteLocallyFree i)
    (A B : FiniteEtaleOver X) :
    Function.Bijective (fun φ : A ⟶ B => (finiteEtaleBaseChange i).map φ)

Tag 0EK0, a lemma

Tag 0EK0 in the Stacks Project.

Stacks.FundamentalGroup.fullyFaithful_restrictionFunctor_of_neighbourhoodSectionsComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/RestrictionColimitEquivalence.lean, line 248. The attribute's comment: “granted Stacks 0EK2 (2)⇒(3), and Stacks 0EK2 (3)⇒(4) together with Stacks 0ELA”.

[Stacks, Tag 0EK0]. Let X be a Noetherian scheme, Y ⊆ X a closed subscheme with infinitesimal neighbourhoods Y_n ⊆ X, and 𝒱 the open subschemes of X containing Y, ordered by reverse inclusion. If one of

X is quasi-affine and colim_𝒱 Γ(V, 𝒪_V) → lim Γ(Y_n, 𝒪_{Y_n}) is an isomorphism,

X has an ample invertible module L and colim_𝒱 Γ(V, L^{⊗ m}) → lim Γ(Y_n, L^{⊗ m}|_{Y_n}) is an isomorphism for all m ≫ 0,

colim_{V' ≥ V} Γ(V', ℰ|_{V'}) → lim Γ(Y_n, ℰ|_{Y_n}) is an isomorphism for every V ∈ 𝒱 and every finite locally free 𝒪_V-module ℰ,

holds, then the restriction functor colim_𝒱 FÉt_V ⟶ FÉt_Y is fully faithful.

The source's proof is to combine [Stacks, Tag 0ELA] with [Stacks, Tag 0EK2]. Of that chain this library carries the implication (1) ⇒ (2) of Tag 0EK2 and no more, so condition (1) is converted to condition (2) here by the library's proof of that implication and the remaining steps are the two hypotheses h0EK2 and h0ELA; see Stacks.FundamentalGroup.AmplePowersImpliesFiniteLocallyFree and Stacks.FundamentalGroup.FullyFaithfulRestrictionOfSectionsComplete.

public theorem fullyFaithful_restrictionFunctor_of_neighbourhoodSectionsComplete
    {X : Scheme.{u}} [IsNoetherian X] (Y : X.IdealSheafData)
    (P : FiniteEtaleColimitPresentation X Y) [HasColimit P.diagram]
    (h : NeighbourhoodSectionsCompleteQuasiAffine Y ∨
      NeighbourhoodSectionsCompleteAmplePowers Y ∨
      NeighbourhoodSectionsCompleteFiniteLocallyFree Y)
    (h0EK2 : AmplePowersImpliesFiniteLocallyFree.{u})
    (h0ELA : FullyFaithfulRestrictionOfSectionsComplete.{u}) :
    Nonempty P.restrictionFunctor.FullyFaithful

Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_of_neighbourhoodSectionsComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/RestrictionColimitFullyFaithful.lean, line 80. The attribute's comment: “all three cases, under the tag's own hypotheses; full faithfulness spelled through the directed-colimit description of the hom sets of colim_V FEt_V”.

[Stacks, Tag 0EK0]. Let X be a Noetherian scheme, Y ⊆ X a closed subscheme with infinitesimal neighbourhoods Y_n ⊆ X, and 𝒱 the open subschemes of X containing Y, ordered by reverse inclusion. Assume one of the following holds:

X is quasi-affine and colim_𝒱 Γ(V, 𝒪_V) → lim Γ(Y_n, 𝒪_{Y_n}) is an isomorphism;

X has an ample invertible module L and colim_𝒱 Γ(V, L^{⊗ m}) → lim Γ(Y_n, L^{⊗ m}|_{Y_n}) is an isomorphism for all m ≫ 0;

for every V ∈ 𝒱 and every finite locally free 𝒪_V-module ℰ the map colim_{V' ≥ V} Γ(V', ℰ|_{V'}) → lim Γ(Y_n, ℰ|_{Y_n}) is an isomorphism.

Then the restriction functor colim_𝒱 FÉt_V ⟶ FÉt_Y is fully faithful. The conclusion is in the form FiniteEtaleColimitFullyFaithful, which describes the hom sets of the directed colimit.

The proof follows the source. By [Stacks, Tag 0EK2], condition (1) gives (2), (2) gives (3), and (3) gives full faithfulness of completion on the finite locally free objects. [Stacks, Tag 0ELA] then gives full faithfulness of restriction.

public theorem finiteEtaleColimitFullyFaithful_of_neighbourhoodSectionsComplete
    {X : Scheme.{u}} [IsNoetherian X] (Y : X.IdealSheafData)
    (h : NeighbourhoodSectionsCompleteQuasiAffine Y ∨
      NeighbourhoodSectionsCompleteAmplePowers Y ∨
      FiniteLocallyFreeComplete Y.subschemeι) :
    FiniteEtaleColimitFullyFaithful X Y

Sources

LeanStacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_of_completionFullyFaithfulOnFiniteLocallyFree · Stacks.FundamentalGroup.finiteEtaleBaseChange_isEquivalence_of_completionEquivalence · Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_of_sectionsExtendNearSubscheme · Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_of_completionFullyFaithfulComplete · Stacks.FundamentalGroup.isEquivalence_restrictionFunctor_of_fullyFaithful_of_essentialImage · Stacks.FundamentalGroup.restriction_isEquivalence_of_completionEquivalence · Stacks.FundamentalGroup.faithful_finiteEtaleRestriction_of_components_meet · Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_of_sectionsComplete_of_or

Section58.18 Pushouts and fundamental groups #

Section 58.18 of the Stacks Project, Tag 0EK3. 1 tag here is carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0EK4, a lemma

Tag 0EK4 in the Stacks Project.

AlgebraicGeometry.finiteEtalePushoutRestriction_isEquivalence, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/FiniteEtalePushout.lean, line 878. The attribute's comment: “the restriction functor is an equivalence”.

Stacks Project, Tag 0EK4. The restriction functor FÉt_{Y ⨿_Z X} ⟶ FÉt_Y ×_{FÉt_Z} FÉt_X is an equivalence of categories. Composed with the pushout of finite étale cartesian triples, which is an equivalence by [Stacks Project, Tag 0ECL], it is reading a triple in the 2-fibre product, which is an equivalence; so it is one itself.

instance finiteEtalePushoutRestriction_isEquivalence
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) :
    (finiteEtalePushoutRestriction s).IsEquivalence

AlgebraicGeometry.finiteEtalePushoutEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/FiniteEtalePushout.lean, line 894.

Stacks Project, Tag 0EK4. In the pushout situation of [Stacks Project, Tag 0ECI] — for example when Z ⟶ Y and Z ⟶ X are closed immersions of schemes — there is an equivalence of categories FÉt_{Y ⨿_Z X} ⟶ FÉt_Y ×_{FÉt_Z} FÉt_X. Its functor is AlgebraicGeometry.finiteEtalePushoutRestriction, which sends a finite étale cover of the pushout to its base changes to Y and to X together with the canonical identification of their restrictions to Z.

noncomputable def finiteEtalePushoutEquivalence
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) :
    FiniteEtaleOver (pushoutScheme s) ≌
      CategoricalPullback (finiteEtaleBaseChange s.j) (finiteEtaleBaseChange s.i)

AlgebraicGeometry.finiteEtalePushoutEquivalence_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/FiniteEtalePushout.lean, line 902. The attribute's comment: “the comparison functor”.

The equivalence of [Stacks Project, Tag 0EK4] is the restriction functor.

theorem finiteEtalePushoutEquivalence_functor
    (s : PushoutAlongClosedImmersionAndIntegralSituation.{u}) :
    (finiteEtalePushoutEquivalence s).functor = finiteEtalePushoutRestriction s

Sources

LeanAlgebraicGeometry.finiteEtalePushoutRestriction_isEquivalence · AlgebraicGeometry.finiteEtalePushoutEquivalence · AlgebraicGeometry.finiteEtalePushoutEquivalence_functor

Section58.19 Finite étale covers of punctured spectra, I #

Section 58.19 of the Stacks Project, Tag 0BLE. 7 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BLF, a situation

Tag 0BLF in the Stacks Project.

Stacks.FundamentalGroup.LocalLefschetzSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/LocalLefschetzSituation.lean, line 64.

The standing data and hypotheses of the local Lefschetz situation.

public structure LocalLefschetzSituation

AlgebraicGeometry.LocalLefschetzSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/LocalLefschetz.lean, line 62.

The standing data of the local Lefschetz situation: a Noetherian local ring A together with an element f of its maximal ideal.

structure LocalLefschetzSituation

Declarations registered for the tag:

Stacks.Divisors.puncturedSpectrum registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/LocalLefschetz.lean, line 57 (StacksFrontier): “the punctured spectra”.
Stacks.puncturedSpectrum, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/LocalCohomology/Deps/PuncturedSpectrumAffine.lean, line 59 (StacksFrontier): “the punctured spectra”.

Tag 0BLG, a lemma

Tag 0BLG in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.faithful_finiteEtaleRestriction, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FaithfulRestriction.lean, line 229.

Stacks Project, Tag 0BLG. In the local Lefschetz situation, base change of finite étale covers from the punctured spectrum of A to the punctured spectrum of A / fA is faithful, provided either that dim (A / 𝔭) ≥ 2 for every minimal prime 𝔭 of A with f ∉ 𝔭, or that every connected component of U meets U₀.

lemma faithful_finiteEtaleRestriction (S : LocalLefschetzSituation.{u})
    (h :
      (∀ p : PrimeSpectrum S.A, IsMinimalPrime p.asIdeal →
        S.f ∉ p.asIdeal → 2 ≤ ringKrullDim (S.A ⧸ p.asIdeal)) ∨
      (∀ c : ConnectedComponents S.U,
        ∃ x : S.U₀, ConnectedComponents.mk (S.U₀ToU.base x) = c)) :
    (finiteEtaleBaseChange S.U₀ToU).Faithful

Tag 0BLH, a lemma

Tag 0BLH in the Stacks Project.

AlgebraicGeometry.exists_finite_extension_of_completion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FiniteExtensionFromCompletion.lean, line 580.

A finite cover of the punctured spectrum which extends over the completed spectrum extends over the original local spectrum, compatibly with both given covers.

lemma exists_finite_extension_of_completion
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (V : Scheme.{u}) (pi : V ⟶ (Stacks.Divisors.puncturedSpectrum A).toScheme)
    [IsFinite pi] :
    let Ahat := AdicCompletion (maximalIdeal A) A
    let Xhat := Spec (.of Ahat)
    let completionMap : Xhat ⟶ Spec (.of A) :=
      Spec.map (CommRingCat.ofHom (algebraMap A Ahat))
    let Uhat := pullback (Stacks.Divisors.puncturedSpectrum A).ι completionMap
    let UhatToU : Uhat ⟶ (Stacks.Divisors.puncturedSpectrum A).toScheme := pullback.fst _ _
    let Vhat := pullback pi UhatToU
    let pihat : Vhat ⟶ Uhat := pullback.snd _ _
    ∀ (Yhat : Scheme.{u}) (fhat : Yhat ⟶ Xhat) [IsFinite fhat]
      (ghat : Vhat ⟶ Yhat),
      IsPullback pihat ghat
          (pullback.snd (Stacks.Divisors.puncturedSpectrum A).ι completionMap) fhat →
        (∃ (Y : Scheme.{u}) (f : Y ⟶ Spec (.of A)) (g : V ⟶ Y) (h : Yhat ⟶ Y),
          IsFinite f ∧
            IsPullback pi g (Stacks.Divisors.puncturedSpectrum A).ι f ∧
            IsPullback fhat h completionMap f ∧
            (pullback.fst pi UhatToU ≫ g = ghat ≫ h))

Tag 0BLI, a lemma

Tag 0BLI in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.fullyFaithful_finiteEtaleRestriction_of_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FullyFaithfulFromCompletion.lean, line 873.

Stacks Project, Tag 0BLI. In the local Lefschetz situation assume that A is henselian, or more generally that (A, fA) is a henselian pair. If restriction of finite étale covers from the punctured spectrum of the 𝔪-adic completion to its closed fibre is fully faithful, then restriction from U to U₀ is fully faithful.

theorem fullyFaithful_finiteEtaleRestriction_of_completion
    (S : LocalLefschetzSituation.{u})
    (hS : HenselianLocalRing S.A ∨ HenselianPair S.A S.principalIdeal)
    (h : let X' := Spec (.of (AdicCompletion (IsLocalRing.maximalIdeal S.A) S.A))
      let completionMap : X' ⟶ S.X :=
        Spec.map (CommRingCat.ofHom
          (algebraMap S.A (AdicCompletion (IsLocalRing.maximalIdeal S.A) S.A)))
      let U'ToU := pullback.fst S.UOpen.ι completionMap
      let U'₀ToU' := pullback.snd S.U₀ToU U'ToU
      Nonempty (finiteEtaleBaseChange U'₀ToU').FullyFaithful) :
    Nonempty (finiteEtaleBaseChange S.U₀ToU).FullyFaithful

Tag 0EK5, a lemma

Tag 0EK5 in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.fullyFaithful_finiteEtaleRestriction_of_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FullyFaithfulComplete.lean, line 334. The attribute's comment: “under hypothesis (c)(ii), the depth-plus-dimension form, and in the case where A is in addition f-adically complete; branch (c)(i) and the reduction to the complete case are not carried out, and hEKP (the chain (1) ⇒ (4) of Stacks 0EKP), h0GN2 (Stacks 0GN2) and halgebra are granted as general hypotheses about other rings and other schemes”.

[Stacks, Tag 0EK5] under hypothesis (c)(ii), in the case where A is in addition f-adically complete. In the local Lefschetz situation assume that A has a dualizing complex, that the pair (A, (f)) is henselian, and that depth(A_𝔭) + dim(A/𝔭) > 2 for every prime 𝔭 ⊂ A with f ∉ 𝔭. If moreover A is f-adically complete, then FÉt_U ⟶ FÉt_{U₀} is fully faithful.

Two restrictions of the tag are recorded in the attribute.

Hypothesis (c) of the tag is a disjunction, and only branch (ii) — the depth-plus-dimension inequality — is treated. Branch (c)(i) is not: deducing (ii) from it is the (S₂)-plus-dimension argument of the source, which goes through Stacks 0339, 0A80, 0AW6 and 0AWY and is not carried out here.

The f-adic completeness of A is the one hypothesis beyond the tag's own. The source obtains it by replacing A by its 𝔪-adic completion, which is Stacks 0BLI, available here as …fullyFaithful_finiteEtaleRestriction_of_completion, together with Stacks 0EHW for the inheritance of (c)(ii); that reduction is not carried out here. The henselian hypothesis hS is the tag's hypothesis (b) and is exactly what the omitted reduction consumes, so it is stated but not used below.

The carried hypotheses hEKP, h0GN2 and halgebra are the ones discussed on fullyFaithful_finiteEtaleRestriction_of_annihilated; here hEKP arrives through Stacks.Algebraization.completionFullyFaithful_of_isAdicComplete_of_depth (Stacks 0EKT) rather than through Stacks 0EKS. None of the three mentions A, f, U or U₀, and none is about finite étale covers.

public theorem fullyFaithful_finiteEtaleRestriction_of_depth
    (S : LocalLefschetzSituation.{u})
    (hS : HenselianPair S.A S.principalIdeal)
    (omega : DerivedCategory (ModuleCat.{u} S.A))
    (homega : Dualizing.IsDualizingComplex (A := S.A) (K := omega))
    (hcomplete : IsAdicComplete (Ideal.span {S.f}) S.A)
    (hdepth : ∀ p : PrimeSpectrum S.A, S.f ∉ p.asIdeal →
      enatToEInt
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule p.asIdeal.primeCompl S.A)) +
        krullDimToEInt (ringKrullDim (S.A ⧸ p.asIdeal)) > ((2 : ℤ) : EInt))
    (hEKP : ∀ (B : Type u) [CommRing B] [IsNoetherianRing B] (b : Ideal B) (g : B),
      Scheme.IsQuasiAffine (complementZeroLocus B b : Scheme) →
      Function.Bijective
        (Stacks.Algebraization.ComplementTower.sectionsToLimit B b g (ModuleCat.of B B)) →
      CompletionFullyFaithfulOnFiniteLocallyFree (complementZeroLocus B b : Scheme)
        (complementPrincipalIdealSheaf B b g))
    (h0GN2 : ∀ {Z Z' : Scheme.{u}} (κ : Z' ⟶ Z) [IsClosedImmersion κ] (N : Z.Modules),
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} N →
      Stacks.Algebraization.IsInfinitesimalSectionsComplete κ
        (Stacks.AlgebraicGeometry.ReflexiveModules.dualSheaf N) →
      (∀ φ ψ : N ⟶ SheafOfModules.unit Z.ringCatSheaf,
          (∀ n : ℕ, φ ≫ nthOrderUnitMap κ n = ψ ≫ nthOrderUnitMap κ n) → φ = ψ) ∧
        ∀ α : ∀ n : ℕ, N ⟶ AlgebraSheaf.underlyingModule (nthOrderAlgebra κ n),
          (∀ n : ℕ, α (n + 1) ≫ nthOrderTransitionMap κ n = α n) →
          ∃ φ : N ⟶ SheafOfModules.unit Z.ringCatSheaf,
            ∀ n : ℕ, φ ≫ nthOrderUnitMap κ n = α n)
    (halgebra : ∀ {Z : Scheme.{u}} (B C : AlgebraSheaf Z) (D : ℕ → AlgebraSheaf Z)
      (r : ∀ n : ℕ, C ⟶ D n)
      (φ : AlgebraSheaf.underlyingModule B ⟶ AlgebraSheaf.underlyingModule C),
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (AlgebraSheaf.underlyingModule B) →
      _root_.SheafOfModules.IsCoherent (AlgebraSheaf.underlyingModule B) →
      (∀ n : ℕ, ∃ ψ : B ⟶ D n,
        AlgebraSheaf.underlyingModuleMap ψ = φ ≫ AlgebraSheaf.underlyingModuleMap (r n)) →
      (∀ P : Z.Modules, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} P →
        _root_.SheafOfModules.IsCoherent P →
        ∀ a b : P ⟶ AlgebraSheaf.underlyingModule C,
          (∀ n : ℕ, a ≫ AlgebraSheaf.underlyingModuleMap (r n) =
            b ≫ AlgebraSheaf.underlyingModuleMap (r n)) → a = b) →
      ∃ ψ : B ⟶ C, AlgebraSheaf.underlyingModuleMap ψ = φ) :
    Nonempty (finiteEtaleBaseChange S.U₀ToU).FullyFaithful

AlgebraicGeometry.LocalLefschetzSituation.fullyFaithful_finiteEtaleRestriction_of_dualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FullyFaithfulPunctured.lean, line 216.

[Stacks, Tag 0EK5]. In the local Lefschetz situation assume

(a) A has a dualizing complex,

(b) the pair (A, (f)) is henselian,

(c) one of the following is true:

(i) A_f is (S₂) and every irreducible component of X not contained in X₀ has dimension ≥ 3, or

(ii) for every prime 𝔭 ⊂ A with f ∉ 𝔭 we have depth(A_𝔭) + dim(A/𝔭) > 2.

Then the restriction functor FÉt_U ⟶ FÉt_{U₀} is fully faithful.

Hypothesis (a) is hdual, (b) is hS and (c) is the disjunction hc. In branch (c)(i), (S₂) for A_f is PropertySkRing (Localization.Away S.f) 2, and an irreducible component of X not contained in X₀ is V(𝔮) for a minimal prime 𝔮 of A with f ∉ 𝔮, of dimension dim(A/𝔮). In branch (c)(ii) the depth of A_𝔭 is that of A_𝔭 as a module over itself along its maximal ideal, and the inequality is read in the extended integers.

The proof is the source's: branch (c)(i) implies branch (c)(ii), by two_lt_depth_add_ringKrullDim_of_propertySkRing_away — A is universally catenary by Stacks 0A80 because it has a dualizing complex — and under (c)(ii) the statement is fullyFaithful_finiteEtaleRestriction_of_depth_add_dim: reduction to the 𝔪-adic completion by Stacks 0BLI, then Stacks 0EKT and Stacks 0EL8.

public theorem fullyFaithful_finiteEtaleRestriction_of_dualizingComplex
    (S : LocalLefschetzSituation.{u})
    (hdual : ∃ omega : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex omega)
    (hS : HenselianPair S.A S.principalIdeal)
    (hc : (PropertySkRing (Localization.Away S.f) 2 ∧
        ∀ q : Ideal S.A, q ∈ minimalPrimes S.A → S.f ∉ q →
          (3 : WithBot ℕ∞) ≤ ringKrullDim (S.A ⧸ q)) ∨
      ∀ p : PrimeSpectrum S.A, S.f ∉ p.asIdeal →
        enatToEInt
            (Module.depth (Localization.AtPrime p.asIdeal)
              (maximalIdeal (Localization.AtPrime p.asIdeal))
              (LocalizedModule p.asIdeal.primeCompl S.A)) +
          krullDimToEInt (ringKrullDim (S.A ⧸ p.asIdeal)) > ((2 : ℤ) : EInt)) :
    Nonempty (finiteEtaleBaseChange S.U₀ToU).FullyFaithful

Tag 0BM6, a lemma

Tag 0BM6 in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.fullyFaithful_finiteEtaleRestriction_of_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FullyFaithfulComplete.lean, line 258. The attribute's comment: “the case where A is in addition f-adically complete, the reduction to that case (Stacks 0BLI together with Stacks 0ALZ) not being carried out; granted hEKP (the chain (1) ⇒ (4) of Stacks 0EKP), h0GN2 (Stacks 0GN2) and halgebra, all three carried as general hypotheses about other rings and other schemes”.

[Stacks, Tag 0BM6] in the case where A is in addition f-adically complete. In the local Lefschetz situation assume that H¹_𝔪(A) and H²_𝔪(A) are annihilated by a power of f and that A is henselian — or more generally that the pair (A, (f)) is henselian. If moreover A is f-adically complete, then FÉt_U ⟶ FÉt_{U₀} is fully faithful.

The f-adic completeness of A is the one hypothesis beyond the tag's own. The source's proof obtains it by replacing A with its 𝔪-adic completion, which is Stacks 0BLI, available here as AlgebraicGeometry.LocalLefschetzSituation.fullyFaithful_finiteEtaleRestriction_of_completion, together with Stacks 0ALZ for the inheritance of the annihilation hypothesis; that reduction is not carried out here, so the statement is the tag restricted to an f-adically complete A. The henselian hypothesis hS is the tag's hypothesis (2); it is exactly what the omitted reduction consumes, so it is stated but not used below.

Three hypotheses about other objects are carried, each inherited verbatim from the result that needs it and each stated about arbitrary rings or arbitrary schemes:

hEKP is the chain (1) ⇒ (4) of [Stacks, Tag 0EKP], the hypothesis of Stacks.Algebraization.completionFullyFaithful_of_isAdicComplete_of_annihilated (Stacks 0EKS). It speaks of every Noetherian ring B, every ideal 𝔟 ⊆ B and every g ∈ B.

h0GN2 is [Stacks, Tag 0GN2] in the shape in which Stacks 0EL8 uses it, and halgebra is the multiplicativity criterion for a morphism of the underlying modules of two sheaves of algebras; both are the hypotheses of Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_of_completionFullyFaithful (Stacks 0EL8) and both are stated about arbitrary schemes and arbitrary closed immersions.

None of the three mentions A, f, U or U₀, and none is about finite étale covers of a punctured spectrum.

public theorem fullyFaithful_finiteEtaleRestriction_of_annihilated
    (S : LocalLefschetzSituation.{u})
    (hS : HenselianLocalRing S.A ∨ HenselianPair S.A S.principalIdeal)
    (hcomplete : IsAdicComplete (Ideal.span {S.f}) S.A)
    (h1 : ∃ n, ∀ x : localCohomologyModule S.A (maximalIdeal S.A)
      (Ideal.fg_of_isNoetherianRing (maximalIdeal S.A)) (ModuleCat.of S.A S.A) 1,
      S.f ^ n • x = 0)
    (h2 : ∃ n, ∀ x : localCohomologyModule S.A (maximalIdeal S.A)
      (Ideal.fg_of_isNoetherianRing (maximalIdeal S.A)) (ModuleCat.of S.A S.A) 2,
      S.f ^ n • x = 0)
    (hEKP : ∀ (B : Type u) [CommRing B] [IsNoetherianRing B] (b : Ideal B) (g : B),
      Scheme.IsQuasiAffine (complementZeroLocus B b : Scheme) →
      Function.Bijective
        (Stacks.Algebraization.ComplementTower.sectionsToLimit B b g (ModuleCat.of B B)) →
      CompletionFullyFaithfulOnFiniteLocallyFree (complementZeroLocus B b : Scheme)
        (complementPrincipalIdealSheaf B b g))
    (h0GN2 : ∀ {Z Z' : Scheme.{u}} (κ : Z' ⟶ Z) [IsClosedImmersion κ] (N : Z.Modules),
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} N →
      Stacks.Algebraization.IsInfinitesimalSectionsComplete κ
        (Stacks.AlgebraicGeometry.ReflexiveModules.dualSheaf N) →
      (∀ φ ψ : N ⟶ SheafOfModules.unit Z.ringCatSheaf,
          (∀ n : ℕ, φ ≫ nthOrderUnitMap κ n = ψ ≫ nthOrderUnitMap κ n) → φ = ψ) ∧
        ∀ α : ∀ n : ℕ, N ⟶ AlgebraSheaf.underlyingModule (nthOrderAlgebra κ n),
          (∀ n : ℕ, α (n + 1) ≫ nthOrderTransitionMap κ n = α n) →
          ∃ φ : N ⟶ SheafOfModules.unit Z.ringCatSheaf,
            ∀ n : ℕ, φ ≫ nthOrderUnitMap κ n = α n)
    (halgebra : ∀ {Z : Scheme.{u}} (B C : AlgebraSheaf Z) (D : ℕ → AlgebraSheaf Z)
      (r : ∀ n : ℕ, C ⟶ D n)
      (φ : AlgebraSheaf.underlyingModule B ⟶ AlgebraSheaf.underlyingModule C),
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (AlgebraSheaf.underlyingModule B) →
      _root_.SheafOfModules.IsCoherent (AlgebraSheaf.underlyingModule B) →
      (∀ n : ℕ, ∃ ψ : B ⟶ D n,
        AlgebraSheaf.underlyingModuleMap ψ = φ ≫ AlgebraSheaf.underlyingModuleMap (r n)) →
      (∀ P : Z.Modules, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} P →
        _root_.SheafOfModules.IsCoherent P →
        ∀ a b : P ⟶ AlgebraSheaf.underlyingModule C,
          (∀ n : ℕ, a ≫ AlgebraSheaf.underlyingModuleMap (r n) =
            b ≫ AlgebraSheaf.underlyingModuleMap (r n)) → a = b) →
      ∃ ψ : B ⟶ C, AlgebraSheaf.underlyingModuleMap ψ = φ) :
    Nonempty (finiteEtaleBaseChange S.U₀ToU).FullyFaithful

AlgebraicGeometry.LocalLefschetzSituation.fullyFaithful_finiteEtaleRestriction_of_annihilated_of_henselian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FullyFaithfulPunctured.lean, line 139.

[Stacks, Tag 0BM6]. In the local Lefschetz situation assume that H¹_𝔪(A) and H²_𝔪(A) are annihilated by a power of f and that A is henselian, or more generally that the pair (A, (f)) is henselian. Then FÉt_U ⟶ FÉt_{U₀} is fully faithful.

The proof is the source's. Replacing A by its 𝔪-adic completion reduces the statement to the case of an f-adically complete A, which is Stacks 0BLI in the form fullyFaithful_finiteEtaleRestriction_of_isAdicCompleteCase; the henselian hypothesis hS is what that reduction consumes, and the annihilation hypothesis passes to the completion by Stacks 0ALZ, which is annihilated_completion. In the complete case completion along (f)𝒪_U is fully faithful on the finite locally free sheaves by Stacks 0EKS, Stacks.Algebraization.completionFullyFaithfulOnFiniteLocallyFree_of_isAdicComplete_of_ annihilated, and fullyFaithful_finiteEtaleRestriction_of_completionFullyFaithfulOnFiniteLocallyFree concludes.

public theorem fullyFaithful_finiteEtaleRestriction_of_annihilated_of_henselian
    (S : LocalLefschetzSituation.{u})
    (hS : HenselianLocalRing S.A ∨ HenselianPair S.A S.principalIdeal)
    (h1 : ∃ n, ∀ x : localCohomologyModule S.A (maximalIdeal S.A)
      (Ideal.fg_of_isNoetherianRing (maximalIdeal S.A)) (ModuleCat.of S.A S.A) 1,
      S.f ^ n • x = 0)
    (h2 : ∃ n, ∀ x : localCohomologyModule S.A (maximalIdeal S.A)
      (Ideal.fg_of_isNoetherianRing (maximalIdeal S.A)) (ModuleCat.of S.A S.A) 2,
      S.f ^ n • x = 0) :
    Nonempty (finiteEtaleBaseChange S.U₀ToU).FullyFaithful

Tag 0BLJ, a lemma

Tag 0BLJ in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.fullyFaithful_finiteEtaleRestriction_of_three_le_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FullyFaithfulComplete.lean, line 409. The attribute's comment: “the case where A is in addition f-adically complete, inherited from the form in which Stacks 0BM6 is available here: the reduction to that case (Stacks 0BLI together with Stacks 0ALZ) is not carried out; granted hEKP (the chain (1) ⇒ (4) of Stacks 0EKP), h0GN2 (Stacks 0GN2) and halgebra, all three carried as general hypotheses about other rings and other schemes. The passage from the depth hypothesis to the vanishing of H¹_𝔪(A) and H²_𝔪(A), which is the source's own proof, is supplied unconditionally from Stacks 0AVZ”.

[Stacks, Tag 0BLJ] in the case where A is in addition f-adically complete. In the local Lefschetz situation assume that A has depth at least 3 and that the pair (A, (f)) is henselian. Then FÉt_U ⟶ FÉt_{U₀} is fully faithful.

This is the source's two-line proof: depth at least 3 forces H¹_𝔪(A) = H²_𝔪(A) = 0 by [Stacks, Tag 0AVZ], so the annihilation hypothesis of Stacks 0BM6 holds with any exponent and fullyFaithful_finiteEtaleRestriction_of_annihilated applies. The henselian hypothesis is stated in the more general of the two forms the source offers — (A, (f)) a henselian pair, rather than A henselian — and is handed on unchanged.

The restrictions are inherited from fullyFaithful_finiteEtaleRestriction_of_annihilated and are nothing beyond them: A is assumed f-adically complete, the reduction to that case (Stacks 0BLI with Stacks 0ALZ) not being carried out, and hEKP, h0GN2 and halgebra are carried as discussed there. None of the three mentions A, f, U or U₀. The depth hypothesis itself is consumed here, not carried.

public theorem fullyFaithful_finiteEtaleRestriction_of_three_le_depth
    (S : LocalLefschetzSituation.{u})
    (hS : HenselianPair S.A S.principalIdeal)
    (hdepth : 3 ≤ Module.depth S.A (maximalIdeal S.A) S.A)
    (hcomplete : IsAdicComplete (Ideal.span {S.f}) S.A)
    (hEKP : ∀ (B : Type u) [CommRing B] [IsNoetherianRing B] (b : Ideal B) (g : B),
      Scheme.IsQuasiAffine (complementZeroLocus B b : Scheme) →
      Function.Bijective
        (Stacks.Algebraization.ComplementTower.sectionsToLimit B b g (ModuleCat.of B B)) →
      CompletionFullyFaithfulOnFiniteLocallyFree (complementZeroLocus B b : Scheme)
        (complementPrincipalIdealSheaf B b g))
    (h0GN2 : ∀ {Z Z' : Scheme.{u}} (κ : Z' ⟶ Z) [IsClosedImmersion κ] (N : Z.Modules),
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} N →
      Stacks.Algebraization.IsInfinitesimalSectionsComplete κ
        (Stacks.AlgebraicGeometry.ReflexiveModules.dualSheaf N) →
      (∀ φ ψ : N ⟶ SheafOfModules.unit Z.ringCatSheaf,
          (∀ n : ℕ, φ ≫ nthOrderUnitMap κ n = ψ ≫ nthOrderUnitMap κ n) → φ = ψ) ∧
        ∀ α : ∀ n : ℕ, N ⟶ AlgebraSheaf.underlyingModule (nthOrderAlgebra κ n),
          (∀ n : ℕ, α (n + 1) ≫ nthOrderTransitionMap κ n = α n) →
          ∃ φ : N ⟶ SheafOfModules.unit Z.ringCatSheaf,
            ∀ n : ℕ, φ ≫ nthOrderUnitMap κ n = α n)
    (halgebra : ∀ {Z : Scheme.{u}} (B C : AlgebraSheaf Z) (D : ℕ → AlgebraSheaf Z)
      (r : ∀ n : ℕ, C ⟶ D n)
      (φ : AlgebraSheaf.underlyingModule B ⟶ AlgebraSheaf.underlyingModule C),
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (AlgebraSheaf.underlyingModule B) →
      _root_.SheafOfModules.IsCoherent (AlgebraSheaf.underlyingModule B) →
      (∀ n : ℕ, ∃ ψ : B ⟶ D n,
        AlgebraSheaf.underlyingModuleMap ψ = φ ≫ AlgebraSheaf.underlyingModuleMap (r n)) →
      (∀ P : Z.Modules, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} P →
        _root_.SheafOfModules.IsCoherent P →
        ∀ a b : P ⟶ AlgebraSheaf.underlyingModule C,
          (∀ n : ℕ, a ≫ AlgebraSheaf.underlyingModuleMap (r n) =
            b ≫ AlgebraSheaf.underlyingModuleMap (r n)) → a = b) →
      ∃ ψ : B ⟶ C, AlgebraSheaf.underlyingModuleMap ψ = φ) :
    Nonempty (finiteEtaleBaseChange S.U₀ToU).FullyFaithful

AlgebraicGeometry.LocalLefschetzSituation.fullyFaithful_finiteEtaleRestriction_of_three_le_depth_of_henselian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FullyFaithfulPunctured.lean, line 246.

[Stacks, Tag 0BLJ]. In the local Lefschetz situation assume that A has depth at least 3 and that the pair (A, (f)) is henselian. Then FÉt_U ⟶ FÉt_{U₀} is fully faithful.

This is the source's proof: depth at least 3 forces H¹_𝔪(A) = H²_𝔪(A) = 0 by [Stacks, Tag 0AVZ], through Stacks.LocalCohomology.isZero_localCohomology_of_lt_depth, so the annihilation hypothesis of Stacks 0BM6 holds with any exponent and fullyFaithful_finiteEtaleRestriction_of_annihilated_of_henselian applies. The henselian hypothesis is the more general of the two forms the source offers — (A, (f)) a henselian pair, rather than A henselian.

public theorem fullyFaithful_finiteEtaleRestriction_of_three_le_depth_of_henselian
    (S : LocalLefschetzSituation.{u})
    (hS : HenselianPair S.A S.principalIdeal)
    (hdepth : 3 ≤ Module.depth S.A (maximalIdeal S.A) S.A) :
    Nonempty (finiteEtaleBaseChange S.U₀ToU).FullyFaithful

Sources

LeanStacks.FundamentalGroup.LocalLefschetzSituation · AlgebraicGeometry.LocalLefschetzSituation · Stacks.Divisors.puncturedSpectrum · Stacks.puncturedSpectrum · AlgebraicGeometry.LocalLefschetzSituation.faithful_finiteEtaleRestriction · AlgebraicGeometry.exists_finite_extension_of_completion · AlgebraicGeometry.LocalLefschetzSituation.fullyFaithful_finiteEtaleRestriction_of_completion · AlgebraicGeometry.LocalLefschetzSituation.fullyFaithful_finiteEtaleRestriction_of_depth

Section58.20 Purity in local case, I #

Section 58.20 of the Stacks Project, Tag 0BM7. 7 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BM8, a lemma

Tag 0BM8 in the Stacks Project.

AlgebraicGeometry.exists_iso_spec_sections_punctured_spectrum, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/Basic.lean, line 134.

Stacks Project, Tag 0BM8. A scheme finite over the spectrum of a Noetherian local ring, whose local rings at closed points all have depth at least two, is canonically the spectrum of its sections over the inverse image of the punctured spectrum.

lemma exists_iso_spec_sections_punctured_spectrum
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    {Y : Scheme.{u}} (π : Y ⟶ Spec (.of A)) [IsFinite π]
    (hdepth : ∀ y : Y, IsClosed ({y} : Set Y) →
      2 ≤ Module.depth (Y.presheaf.stalk y)
        (IsLocalRing.maximalIdeal (Y.presheaf.stalk y)) (Y.presheaf.stalk y)) :
    let U : (Spec (.of A)).Opens :=
      ⟨({IsLocalRing.closedPoint A} : Set (PrimeSpectrum A))ᶜ,
        IsLocalRing.isClosed_singleton_closedPoint A |>.isOpen_compl⟩
    let V : Y.Opens := π ⁻¹ᵁ U
    ∃ e : Y ≅ Spec Γ(Y, V),
      e.hom ≫ Spec.map (Y.presheaf.map (homOfLE le_top).op) = Y.toSpecΓ

Tag 0BLK, a lemma

Tag 0BLK in the Stacks Project.

AlgebraicGeometry.exists_finiteEtale_extension_iff_globalSections_finiteEtale, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/GlobalSectionsCriterion.lean, line 274.

Stacks Project, Tag 0BLK. For a Noetherian local ring of depth at least two, a finite étale scheme over the punctured spectrum extends to a finite étale scheme over the whole spectrum if and only if its ring of global sections is finite étale over the ring.

lemma exists_finiteEtale_extension_iff_globalSections_finiteEtale
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (V : Scheme.{u}) (π : V ⟶ (Stacks.Divisors.puncturedSpectrum A).toScheme)
    [IsFinite π] [Etale π]
    (hdepth : 2 ≤ Module.depth A (IsLocalRing.maximalIdeal A) A) :
    (∃ (Y : Scheme.{u}) (f : Y ⟶ Spec (.of A)) (g : V ⟶ Y),
      IsFinite f ∧ Etale f ∧ IsPullback π g (Stacks.Divisors.puncturedSpectrum A).ι f) ↔
      letI : Algebra A Γ(V, ⊤) :=
        ((Scheme.ΓSpecIso (.of A)).inv ≫
          (π ≫ (Stacks.Divisors.puncturedSpectrum A).ι).appTop).hom.toAlgebra
      Module.Finite A Γ(V, ⊤) ∧ Algebra.Etale A Γ(V, ⊤)

Tag 0BM9, a lemma

Tag 0BM9 in the Stacks Project.

AlgebraicGeometry.NormalPurity.globalSections_isEquivalence_normalFiniteEtaleAwayAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/NormalEquivalence.lean, line 992. The attribute's comment: “the equivalence”.

Stacks Project, Tag 0BM9. On a Noetherian normal local ring of dimension at least two, global sections give an equivalence from the opposite of the category of finite étale covers of the punctured spectrum to finite normal torsion-free algebras which are étale there.

public theorem globalSections_isEquivalence_normalFiniteEtaleAwayAlgebra
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (hnormal : IsNormalRing A) (hdim : (2 : WithBot ℕ∞) ≤ ringKrullDim A) :
    ∃ F : Functor
        (FiniteEtaleOver (Stacks.Divisors.puncturedSpectrum A).toScheme)ᵒᵖ
        (NormalFiniteEtaleAwayAlgebra A),
      F.IsEquivalence ∧ Nonempty
        (F ⋙ ObjectProperty.ι _ ≅ globalSections A)

AlgebraicGeometry.NormalPurity.exists_finiteEtale_extension_iff_globalSections_finiteEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/NormalEquivalence.lean, line 1019. The attribute's comment: “the extension criterion”.

Stacks Project, Tag 0BM9. A finite étale cover of the punctured spectrum extends to a finite étale cover of the whole spectrum exactly when its ring of global sections is finite étale over the base ring.

public theorem exists_finiteEtale_extension_iff_globalSections_finiteEtale
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (hnormal : IsNormalRing A) (hdim : (2 : WithBot ℕ∞) ≤ ringKrullDim A)
    (V : Scheme.{u}) (π : V ⟶ (Stacks.Divisors.puncturedSpectrum A).toScheme)
    [IsFinite π] [Etale π] :
    (∃ (Y : Scheme.{u}) (f : Y ⟶ Spec (.of A)) (g : V ⟶ Y),
      IsFinite f ∧ Etale f ∧ IsPullback π g (Stacks.Divisors.puncturedSpectrum A).ι f) ↔
      letI : Algebra A Γ(V, ⊤) :=
        ((Scheme.ΓSpecIso (.of A)).inv ≫
          (π ≫ (Stacks.Divisors.puncturedSpectrum A).ι).appTop).hom.toAlgebra
      Module.Finite A Γ(V, ⊤) ∧ Algebra.Etale A Γ(V, ⊤)

Tag 0BLL, a lemma

Tag 0BLL in the Stacks Project.

AlgebraicGeometry.exists_finiteEtale_extension_iff_completion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/CompletionCriterion.lean, line 50.

Stacks Project, Tag 0BLL. A finite étale cover of the punctured spectrum of a Noetherian local ring extends over the spectrum exactly when its base change to the adic completion extends over the completed spectrum.

lemma exists_finiteEtale_extension_iff_completion
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (V : Scheme.{u}) (pi : V ⟶ (Stacks.Divisors.puncturedSpectrum A).toScheme)
    [IsFinite pi] [Etale pi] :
    let Ahat := AdicCompletion (maximalIdeal A) A
    let Xhat := Spec (.of Ahat)
    let completionMap : Xhat ⟶ Spec (.of A) :=
      Spec.map (CommRingCat.ofHom (algebraMap A Ahat))
    let Uhat := pullback (Stacks.Divisors.puncturedSpectrum A).ι completionMap
    let UhatToU : Uhat ⟶ (Stacks.Divisors.puncturedSpectrum A).toScheme :=
      pullback.fst _ _
    let Vhat := pullback pi UhatToU
    let pihat : Vhat ⟶ Uhat := pullback.snd _ _
    (∃ (Y : Scheme.{u}) (f : Y ⟶ Spec (.of A)) (g : V ⟶ Y),
      IsFinite f ∧ Etale f ∧
        IsPullback pi g (Stacks.Divisors.puncturedSpectrum A).ι f) ↔
      ∃ (Yhat : Scheme.{u}) (fhat : Yhat ⟶ Xhat) (ghat : Vhat ⟶ Yhat),
        IsFinite fhat ∧ Etale fhat ∧
          IsPullback pihat ghat (pullback.snd (Stacks.Divisors.puncturedSpectrum A).ι completionMap)
            fhat

Tag 0EK6, a lemma

Tag 0EK6 in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.exists_finiteEtale_extension_of_dualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/ExtensionFromHypersurface.lean, line 243.

[Stacks, Tag 0EK6]. In the local Lefschetz situation (Tag 0BLF) let V be finite étale over U. Assume

(a) A has a dualizing complex,

(b) the pair (A, (f)) is henselian,

(c) one of the following is true: (i) A_f is (S₂) and every irreducible component of X not contained in X₀ has dimension ≥ 3, or (ii) depth(A_𝔭) + dim(A/𝔭) > 2 for every prime 𝔭 ⊂ A with f ∉ 𝔭,

(d) V₀ = V ×_U U₀ is equal to Y₀ ×_{X₀} U₀ for some Y₀ → X₀ finite étale.

Then V = Y ×_X U for some Y → X finite étale.

Spelling. Hypothesis (a) is hdual, (b) is hS and (c) is the disjunction hc. "A has a dualizing complex" is ∃ ω, Dualizing.IsDualizingComplex ω, the predicate of [Stacks, Tag 0A7B] on the derived category of A-modules. (S₂) for A_f is PropertySkRing (Localization.Away S.f) 2, Serre's condition of [Stacks, Tag 031P]. The irreducible components of X = Spec A are the V(𝔮) for 𝔮 a minimal prime of A; V(𝔮) is contained in X₀ = V(f) exactly when f ∈ 𝔮, and its dimension is dim(A/𝔮); so the second half of (c)(i) is the quantification over minimal primes 𝔮 with f ∉ 𝔮. In (c)(ii) depth(A_𝔭) is the depth of the A_𝔭-module A_𝔭 along its maximal ideal and the sum is formed in ℤ ∪ {±∞}. Hypothesis (d) and the conclusion record "V₀ = Y₀ ×_{X₀} U₀" and "V = Y ×_X U" as cartesian squares (CategoryTheory.IsPullback), V ×_U U₀ being the chosen pullback.

The proof is the source's. Branch (c)(i) implies branch (c)(ii) for a ring with a dualizing complex (two_lt_depth_add_ringKrullDim_of_propertySkRing_away, through the universal catenarity of Stacks 0A80), and under (c)(ii) the statement is exists_finiteEtale_extension_of_depth_add_dim: Stacks 0BLL reduces to the complete case, where Stacks 09ZL/09ZS lifts Y₀ (the pair being henselian by Stacks 0ALJ) and Stacks 0EK5 descends the isomorphism over U₀ to one over U.

public theorem exists_finiteEtale_extension_of_dualizingComplex
    (S : LocalLefschetzSituation.{u})
    (hdual : ∃ omega : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex omega)
    (hS : HenselianPair S.A S.principalIdeal)
    (hc : (PropertySkRing (Localization.Away S.f) 2 ∧
        ∀ q : Ideal S.A, q ∈ minimalPrimes S.A → S.f ∉ q →
          (3 : WithBot ℕ∞) ≤ ringKrullDim (S.A ⧸ q)) ∨
      ∀ p : PrimeSpectrum S.A, S.f ∉ p.asIdeal →
        enatToEInt
            (Module.depth (Localization.AtPrime p.asIdeal)
              (maximalIdeal (Localization.AtPrime p.asIdeal))
              (LocalizedModule p.asIdeal.primeCompl S.A)) +
          krullDimToEInt (ringKrullDim (S.A ⧸ p.asIdeal)) > ((2 : ℤ) : EInt))
    (V : Scheme.{u}) (pi : V ⟶ S.U) [IsFinite pi] [Etale pi]
    (Y₀ : Scheme.{u}) (f₀ : Y₀ ⟶ S.X₀) [IsFinite f₀] [Etale f₀]
    (g₀ : pullback pi S.U₀ToU ⟶ Y₀)
    (h₀ : IsPullback (pullback.snd pi S.U₀ToU) g₀ S.U₀Open.ι f₀) :
    ∃ (Y : Scheme.{u}) (p : Y ⟶ S.X) (g : V ⟶ Y),
      IsFinite p ∧ Etale p ∧ IsPullback pi g S.UOpen.ι p

Tag 0BLS, a lemma

Tag 0BLS in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.exists_finiteEtale_extension_of_localCohomology_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/ExtensionFromHypersurface.lean, line 288.

[Stacks, Tag 0BLS]. In the local Lefschetz situation let V be finite étale over U and assume (1) H¹_𝔪(A) and H²_𝔪(A) are annihilated by a power of f, and (2) V ×_U U₀ is Y₀ ×_{X₀} U₀ for some Y₀ → X₀ finite étale. Then V = Y ×_X U for some Y → X finite étale.

The proof is the source's. Stacks 0BLL reduces the existence of the extension to the case of an f-adically complete base, which is …LocalLefschetzSituation.exists_finiteEtale_extension_of_isAdicCompleteCase, and the annihilation hypothesis is inherited by the 𝔪-adic completion through Stacks 0ALZ, which is …LocalLefschetzSituation.annihilated_completion. In the complete case (A, fA) is a henselian pair by Stacks 0ALJ (IsAdicComplete.henselianRing and henselianPair_of_henselianRing); that henselian pair feeds Stacks 09ZS, lifting Y₀ to a finite étale Y → X, and is also hypothesis (2) of Stacks 0BM6, which supplies the full faithfulness of restriction that the descent step needs, as fullyFaithful_finiteEtaleRestriction_of_annihilated_of_henselian.

public theorem exists_finiteEtale_extension_of_localCohomology_annihilated
    (S : LocalLefschetzSituation.{u})
    (h1 : ∃ n, ∀ x : localCohomologyModule S.A (maximalIdeal S.A)
      (Ideal.fg_of_isNoetherianRing (maximalIdeal S.A)) (ModuleCat.of S.A S.A) 1,
      S.f ^ n • x = 0)
    (h2 : ∃ n, ∀ x : localCohomologyModule S.A (maximalIdeal S.A)
      (Ideal.fg_of_isNoetherianRing (maximalIdeal S.A)) (ModuleCat.of S.A S.A) 2,
      S.f ^ n • x = 0)
    (V : Scheme.{u}) (pi : V ⟶ S.U) [IsFinite pi] [Etale pi]
    (Y₀ : Scheme.{u}) (f₀ : Y₀ ⟶ S.X₀) [IsFinite f₀] [Etale f₀]
    (g₀ : pullback pi S.U₀ToU ⟶ Y₀)
    (h₀ : IsPullback (pullback.snd pi S.U₀ToU) g₀ S.U₀Open.ι f₀) :
    ∃ (Y : Scheme.{u}) (p : Y ⟶ S.X) (g : V ⟶ Y),
      IsFinite p ∧ Etale p ∧ IsPullback pi g S.UOpen.ι p

Tag 0BLM, a lemma

Tag 0BLM in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.exists_finiteEtale_extension_of_three_le_depth_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/ExtensionFromHypersurface.lean, line 317.

[Stacks, Tag 0BLM]. In the local Lefschetz situation let V be finite étale over U and assume (1) A has depth at least 3, and (2) V ×_U U₀ is Y₀ ×_{X₀} U₀ for some Y₀ → X₀ finite étale. Then V = Y ×_X U for some Y → X finite étale.

This is the source's proof. Depth at least 3 forces H¹_𝔪(A) = H²_𝔪(A) = 0 by [Stacks, Tag 0AVZ] (Stacks.LocalCohomology.subsingleton_localCohomologyModule_of_lt_depth), so both are annihilated by f ^ 0, and the conclusion is [Stacks, Tag 0BLS] at S, which is exists_finiteEtale_extension_of_localCohomology_annihilated.

public theorem exists_finiteEtale_extension_of_three_le_depth_self
    (S : LocalLefschetzSituation.{u})
    (hdepth : 3 ≤ Module.depth S.A (maximalIdeal S.A) S.A)
    (V : Scheme.{u}) (pi : V ⟶ S.U) [IsFinite pi] [Etale pi]
    (Y₀ : Scheme.{u}) (f₀ : Y₀ ⟶ S.X₀) [IsFinite f₀] [Etale f₀]
    (g₀ : pullback pi S.U₀ToU ⟶ Y₀)
    (h₀ : IsPullback (pullback.snd pi S.U₀ToU) g₀ S.U₀Open.ι f₀) :
    ∃ (Y : Scheme.{u}) (p : Y ⟶ S.X) (g : V ⟶ Y),
      IsFinite p ∧ Etale p ∧ IsPullback pi g S.UOpen.ι p

AlgebraicGeometry.LocalLefschetzSituation.exists_finiteEtale_extension_of_three_le_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/LiftFromDepthThree.lean, line 178. The attribute's comment: “the unrestricted Stacks 0BLS is carried as a named general hypothesis”.

[Stacks, Tag 0BLM] In the local Lefschetz situation let V be finite étale over U and assume (1) A has depth at least 3, and (2) V ×_U U₀ is Y₀ ×_{X₀} U₀ for some Y₀ → X₀ finite étale. Then V = Y ×_X U for some Y → X finite étale.

This is the source's proof. Depth at least 3 forces H¹_𝔪(A) = H²_𝔪(A) = 0 by [Stacks, Tag 0AVZ], which is the whole content supplied here, and the conclusion is then [Stacks, Tag 0BLS] at the situation S.

That last step is the hypothesis hLiftFromHypersurface, stated in the unrestricted form the source gives [Stacks, Tag 0BLS], universally quantified over all local Lefschetz situations, with its own annihilation hypothesis intact — it is not specialised to S, says nothing about depth, and does not grant this statement's conclusion. It holds by exists_finiteEtale_extension_of_localCohomology_annihilated. The f-adically complete case is exists_finiteEtale_extension_of_three_le_depth_of_isAdicComplete above, where it is discharged.

public theorem exists_finiteEtale_extension_of_three_le_depth
    (S : LocalLefschetzSituation.{u})
    (hdepth : 3 ≤ Module.depth S.A (maximalIdeal S.A) S.A)
    (hLiftFromHypersurface : ∀ T : LocalLefschetzSituation.{u},
      (∃ n : ℕ, ∀ x : localCohomologyModule T.A (maximalIdeal T.A)
        (Ideal.fg_of_isNoetherianRing (maximalIdeal T.A)) (ModuleCat.of T.A T.A) 1,
        T.f ^ n • x = 0) →
      (∃ n : ℕ, ∀ x : localCohomologyModule T.A (maximalIdeal T.A)
        (Ideal.fg_of_isNoetherianRing (maximalIdeal T.A)) (ModuleCat.of T.A T.A) 2,
        T.f ^ n • x = 0) →
      ∀ (W : Scheme.{u}) (ρ : W ⟶ T.U), IsFinite ρ → Etale ρ →
      ∀ (Z₀ : Scheme.{u}) (q₀ : Z₀ ⟶ T.X₀), IsFinite q₀ → Etale q₀ →
      ∀ e₀ : pullback ρ T.U₀ToU ⟶ Z₀,
        IsPullback (pullback.snd ρ T.U₀ToU) e₀ T.U₀Open.ι q₀ →
        ∃ (Z : Scheme.{u}) (q : Z ⟶ T.X) (e : W ⟶ Z),
          IsFinite q ∧ Etale q ∧ IsPullback ρ e T.UOpen.ι q)
    (V : Scheme.{u}) (pi : V ⟶ S.U) [IsFinite pi] [Etale pi]
    (Y₀ : Scheme.{u}) (f₀ : Y₀ ⟶ S.X₀) [IsFinite f₀] [Etale f₀]
    (g₀ : pullback pi S.U₀ToU ⟶ Y₀)
    (h₀ : IsPullback (pullback.snd pi S.U₀ToU) g₀ S.U₀Open.ι f₀) :
    ∃ (Y : Scheme.{u}) (p : Y ⟶ S.X) (g : V ⟶ Y),
      IsFinite p ∧ Etale p ∧ IsPullback pi g S.UOpen.ι p

AlgebraicGeometry.LocalLefschetzSituation.exists_finiteEtale_lift_of_three_le_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/LiftFromDepthThreeCompletion.lean, line 65.

[Stacks, Tag 0BLM] In the local Lefschetz situation let V be finite étale over U and assume (1) A has depth at least 3, and (2) V ×_U U₀ is Y₀ ×_{X₀} U₀ for some Y₀ → X₀ finite étale. Then V = Y ×_X U for some Y → X finite étale.

The reduction to the complete case is by Tag 0BLL, as in the source's proof of Tag 0BLS (AlgebraicGeometry.LocalLefschetzSituation.exists_finiteEtale_extension_of_isAdicCompleteCase): the completion Â has the same depth (Tag 07NW) and is f-adically complete, and the base change of Y₀ to Spec (Â / fÂ) witnesses hypothesis (2) for the base change of V.

theorem exists_finiteEtale_lift_of_three_le_depth
    (hdepth : 3 ≤ Module.depth S.A (maximalIdeal S.A) S.A)
    (V : Scheme.{u}) (pi : V ⟶ S.U) [IsFinite pi] [Etale pi]
    (Y₀ : Scheme.{u}) (f₀ : Y₀ ⟶ S.X₀) [IsFinite f₀] [Etale f₀]
    (g₀ : pullback pi S.U₀ToU ⟶ Y₀)
    (h₀ : IsPullback (pullback.snd pi S.U₀ToU) g₀ S.U₀Open.ι f₀) :
    ∃ (Y : Scheme.{u}) (p : Y ⟶ S.X) (g : V ⟶ Y),
      IsFinite p ∧ Etale p ∧ IsPullback pi g S.UOpen.ι p

Sources

LeanAlgebraicGeometry.exists_iso_spec_sections_punctured_spectrum · AlgebraicGeometry.exists_finiteEtale_extension_iff_globalSections_finiteEtale · AlgebraicGeometry.NormalPurity.globalSections_isEquivalence_normalFiniteEtaleAwayAlgebra · AlgebraicGeometry.NormalPurity.exists_finiteEtale_extension_iff_globalSections_finiteEtale · AlgebraicGeometry.exists_finiteEtale_extension_iff_completion · AlgebraicGeometry.LocalLefschetzSituation.exists_finiteEtale_extension_of_dualizingComplex · AlgebraicGeometry.LocalLefschetzSituation.exists_finiteEtale_extension_of_localCohomology_annihilated · AlgebraicGeometry.LocalLefschetzSituation.exists_finiteEtale_extension_of_three_le_depth_self

Section58.21 Purity of branch locus #

Section 58.21 of the Stacks Project, Tag 0BJE. 6 tags here are carried by 27 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BJG, a lemma

Tag 0BJG in the Stacks Project.

IsLocalRing.exists_isPrime_height_eq_one_of_mem_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/Basic.lean, line 40.

An element of the maximal ideal of a positive-dimensional Noetherian local ring is contained in a prime ideal of height one.

public theorem exists_isPrime_height_eq_one_of_mem_maximalIdeal
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (hdim : 1 ≤ ringKrullDim A) (f : A) (hf : f ∈ IsLocalRing.maximalIdeal A) :
    ∃ p : Ideal A, p.IsPrime ∧ f ∈ p ∧ p.height = 1

Tag 0BJH, a lemma

Tag 0BJH in the Stacks Project.

AlgebraicGeometry.etaleAt_of_flat_of_unramifiedAt_codimensionOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/UnramifiedCodimensionOne.lean, line 328.

Stacks Project, Tag 0BJH. A flat morphism of locally Noetherian schemes which is quasi-finite at a point that is not the generic point of an irreducible component of its source is étale at that point, provided it is unramified at every one-dimensional generization of the point.

public theorem etaleAt_of_flat_of_unramifiedAt_codimensionOne
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [Flat f]
    (x : X) (hqf : quasiFiniteAt f x) (hgen : x ∉ genericPoints X)
    (hunr : ∀ x' : X, x' ⤳ x → ringKrullDim (X.presheaf.stalk x') = 1 → UnramifiedAt f x') :
    EtaleAt f x

Tag 0BMA, a lemma

Tag 0BMA in the Stacks Project.

Stacks.PurityDimensionTwo.quotient_maximalIdeal_counterexample_clauseTwo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/PurityClauseTwoCounterexample.lean, line 116. The attribute's comment: “clause (2) as literally stated is false: for every regular local ring A with 2 ≤ ringKrullDim A, B = A ⧸ 𝔪 is a finite A-algebra and a normal ring (IsNormalRing), the preimage of the punctured spectrum under Spec B ⟶ Spec A is empty, so the induced morphism over the punctured spectrum is finite étale, but A → B is not étale (A ⧸ 𝔪 is not even torsion-free over A). This is why the clause-(2) declaration Stacks.PurityDimensionTwo.etale_of_isNormalRing_of_two_le_ringKrullDim carries the extra hypothesis Module.IsTorsionFree A B.”.

Clause (2) of [Stacks, Tag 0BMA] as literally stated is false: the residue field is a counterexample. Let A be a regular local ring of dimension at least two and B = A ⧸ 𝔪. Then B is a finite A-algebra and a normal ring, the preimage of the punctured spectrum U under Spec B ⟶ Spec A is empty (so Spec B ×_X U = ∅), and Spec B ⟶ Spec A is étale over U (it is finite everywhere); but A → B is not étale. These are the hypotheses of clause (2) in the spelling of Stacks.PurityDimensionTwo.etale_of_isNormalRing_of_two_le_ringKrullDim without its added hypothesis Module.IsTorsionFree A B, which A ⧸ 𝔪 violates.

theorem quotient_maximalIdeal_counterexample_clauseTwo [IsRegularLocalRing A]
    (hdim : (2 : WithBot ℕ∞) ≤ ringKrullDim A) :
    Module.Finite A (A ⧸ maximalIdeal A) ∧ IsNormalRing (A ⧸ maximalIdeal A) ∧
      IsEmpty ↥(Spec.map (CommRingCat.ofHom (algebraMap A (A ⧸ maximalIdeal A))) ⁻¹ᵁ
        Stacks.puncturedSpectrum A) ∧
      Etale (Spec.map (CommRingCat.ofHom (algebraMap A (A ⧸ maximalIdeal A))) ∣_
        Stacks.puncturedSpectrum A) ∧
      ¬ Algebra.Etale A (A ⧸ maximalIdeal A)

Stacks.PurityDimensionTwo.hasPurity_of_ringKrullDim_eq_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/PurityRegularDimensionTwo.lean, line 127. The attribute's comment: “clause (1) of the tag, and in the case d = 2: A regular local with ringKrullDim A = 2, and the conclusion is AlgebraicGeometry.HasPurity A, i.e. essential surjectivity of FÉt_{Spec A} ⟶ FÉt_U, which is the source's definition of purity for (A, 𝔪). This is the base case of the source's induction on d; the inductive step is tag 0BLM.”. References: SGA 2 X (3.4), “partial”.

Purity of the branch locus, [Stacks, Tag 0BMA] clause (1), in dimension two. Let A be a regular local ring of Krull dimension 2. Then every finite étale cover of the punctured spectrum of A is the restriction of a finite étale cover of Spec A.

This is the source's argument. A regular local ring is a normal ring, so [Stacks, Tag 0BM9] applies to it: the global sections B = Γ(V, 𝒪_V) of a finite étale V ⟶ U are a finite normal A-algebra, torsion-free over A, whose spectrum is étale over U, and V extends over Spec A exactly when B is finite étale over A. The latter is clause (2) of the tag in dimension two, etale_of_isNormalRing_of_ringKrullDim_eq_two, whose hypotheses — normality of B, finiteness and torsion-freeness over A, and étaleness over the punctured spectrum — are precisely what [Stacks, Tag 0BM9] supplies.

public theorem hasPurity_of_ringKrullDim_eq_two (A : Type u) [CommRing A]
    [IsRegularLocalRing A] (hdimA : ringKrullDim A = 2) :
    HasPurity A

Stacks.PurityDimensionTwo.etale_of_isNormalRing_of_two_le_ringKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/PurityRegularLocal.lean, line 85. The attribute's comment: “clause (2) of the tag, at every d ≥ 2: A regular local with 2 ≤ ringKrullDim A, B a finite A-algebra which is a normal ring in the sense of IsNormalRing (item (1) of tag 030C) and is torsion-free over A, and Spec B ⟶ Spec A étale over the punctured spectrum; the conclusion is Algebra.Etale A B. The source's derivation from clause (1) through tag 0BM9 is the proof, and clause (1) at every d ≥ 2 is AlgebraicGeometry.purityAtRegularLocalRings. Torsion-freeness over A is an extra hypothesis, not present in the source and necessary for the statement to be true: the residue field A ⧸ 𝔪 is a finite normal A-algebra whose spectrum misses the punctured spectrum, hence is étale there, and is not flat over A. Weakening it to injectivity of algebraMap A B, or to surjectivity of Spec B ⟶ Spec A, leaves the statement false as well: B = A × (A ⧸ 𝔪) is a finite normal A-algebra with both properties which is the identity over the punctured spectrum and is not flat over A. That clause (2) as literally stated is false is proved in Stacks.PurityDimensionTwo.quotient_maximalIdeal_counterexample_clauseTwo (PurityBranchLocus.PurityClauseTwoCounterexample); see also the module docstring of PurityBranchLocus.RegularDimensionTwo.”. References: SGA 1 X (3.2), “Case B finite over A”; SGA 4½ Arcata (5.2.4), “special case”.

[Stacks, Tag 0BMA] clause (2) for every d ≥ 2. Let A be a regular local ring of dimension at least two and let B be a finite A-algebra which is a normal ring and torsion-free over A, such that Spec B ⟶ Spec A is étale over the punctured spectrum. Then A → B is étale.

This is the source's derivation of clause (2) from clause (1) through [Stacks, Tag 0BM9]: A is normal, so B is an object of the category NormalFiniteEtaleAwayAlgebra A equivalent to (FÉt_U)ᵒᵖ, hence B ≅ Γ(V, 𝒪_V) for some finite étale V ⟶ U; purity extends V over Spec A, and the extension criterion of [Stacks, Tag 0BM9] then says that Γ(V, 𝒪_V) is finite étale over A.

The hypothesis Module.IsTorsionFree A B is not in the source, and is necessary: it is exactly the point at which the source's statement of clause (2) is wrong, and the counterexample is recorded in the module docstring of StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/RegularDimensionTwo.lean. In brief: B = A ⧸ 𝔪 is finite over A, is a field and hence a normal ring, and has empty punctured spectrum, so it is étale over U vacuously; but A is a domain with 𝔪 ≠ 0, so A ⧸ 𝔪 is not even flat over A; this is proved as Stacks.PurityDimensionTwo.quotient_maximalIdeal_counterexample_clauseTwo. Nor does it help to ask only that algebraMap A B be injective, or that Spec B ⟶ Spec A be surjective: B = A × (A ⧸ 𝔪) is a finite normal A-algebra satisfying both, is the identity over U, and is not flat over A.

public theorem etale_of_isNormalRing_of_two_le_ringKrullDim
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B] [IsRegularLocalRing A]
    [Module.Finite A B] [Module.IsTorsionFree A B] (hB : IsNormalRing B)
    (hdim : (2 : WithBot ℕ∞) ≤ ringKrullDim A)
    (hetale : Etale (Spec.map (CommRingCat.ofHom (algebraMap A B)) ∣_
      Stacks.puncturedSpectrum A)) :
    Algebra.Etale A B

Stacks.PurityDimensionTwo.etale_of_isNormalRing_of_ringKrullDim_eq_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/RegularDimensionTwo.lean, line 439. The attribute's comment: “clause (2) of the tag, and only in the case d = 2: A regular local with ringKrullDim A = 2, B a finite A-algebra which is a normal ring in the sense of IsNormalRing (item (1) of tag 030C) and is torsion-free over A, and Spec B ⟶ Spec A étale over the punctured spectrum; the conclusion is Algebra.Etale A B. This is the base case of the source's induction on d; the inductive step is tag 0BLM, and clause (2) for every d ≥ 2 is etale_of_isNormalRing_of_two_le_ringKrullDim in PurityBranchLocus.PurityRegularLocal. Clause (1) at d = 2 — essential surjectivity of FÉt_X ⟶ FÉt_U, i.e. purity for A — follows from this result through tag 0BM9 and is Stacks.PurityDimensionTwo.hasPurity_of_ringKrullDim_eq_two. Torsion-freeness over A is an extra hypothesis, not present in the source and necessary for the statement to be true: the residue field A ⧸ 𝔪 is a finite normal A-algebra whose spectrum misses the punctured spectrum, hence is étale there, and is not étale over A. See the module docstring.”. References: SGA 1 X (3.2), “special case”.

Let A be a regular local ring of Krull dimension 2, and let B be a finite A-algebra which is a normal ring and torsion-free over A, such that the induced morphism on punctured spectra is étale. Then A → B is étale.

public theorem etale_of_isNormalRing_of_ringKrullDim_eq_two
    [IsRegularLocalRing A] [Module.Finite A B] [Module.IsTorsionFree A B]
    (hB : IsNormalRing B) (hdimA : ringKrullDim A = 2)
    (hetale : Etale (Spec.map (CommRingCat.ofHom (algebraMap A B)) ∣_
      Stacks.puncturedSpectrum A)) :
    Algebra.Etale A B

Declarations registered for the tag:

AlgebraicGeometry.purityAtRegularLocalRings, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/PurityRegularLocal.lean, line 128 (StacksFrontier): “clause (1) of the tag, at every d ≥ 2: for every regular local ring A with 2 ≤ ringKrullDim A, AlgebraicGeometry.HasPurity A, i.e. essential surjectivity of FÉt_{Spec A} ⟶ FÉt_U for U the punctured spectrum, which is the source's definition of purity for (A, 𝔪).”.

Tag 0BMB, a lemma

Tag 0BMB in the Stacks Project.

AlgebraicGeometry.etaleAt_of_quasiFiniteAt_of_unramifiedAt_codimensionOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/AnyDimension.lean, line 697. The attribute's comment: “the whole tag, in every dimension: hypotheses (1) 𝒪_{X,x} normal, (2) 𝒪_{Y,f x} regular, (3) f quasi-finite at x, (4) dim 𝒪_{X,x} = dim 𝒪_{Y,f x} and 1 ≤ dim 𝒪_{X,x}, and (5) f unramified at every point specializing to x whose local ring has dimension one; the conclusion is EtaleAt f x. The proof is the source's induction on dim 𝒪_{X,x}, with the case dim 𝒪_{X,x} ≤ 2 as its base case and tag 0BMA clause (2) in every dimension, Stacks.PurityDimensionTwo.etale_of_isNormalRing_of_two_le_ringKrullDim, supplying Cohen–Macaulayness of 𝒪_{X,x} above it.”. References: EGA IV (21.12.14), “(v), (v), special case”; SGA 1 X (3.1), “more general”; SGA 1 X (3.2), “more general”.

Purity of the branch locus, [Stacks, Tag 0BMB], in any dimension. Let f : X ⟶ Y be a morphism of locally Noetherian schemes and let x : X be a point whose local ring is normal, with regular local ring at f x, at which f is quasi-finite, and such that the two local rings have the same dimension, which is at least one. If f is unramified at every point specializing to x whose local ring has dimension one, then f is étale at x.

The hypotheses are exactly the tag's own.

The proof is the source's induction on d = dim 𝒪_{X,x}. For d ≤ 2 the conclusion is AlgebraicGeometry.etaleAt_of_quasiFiniteAt_of_unramifiedAt_codimensionOne_of_dim_le_two. For d ≥ 3 the induction hypothesis gives étaleness at every proper generization of x — their local rings are normal, the local rings below them regular, f is quasi-finite there because the quasi-finite locus is open, and the two dimensions agree there by AlgebraicGeometry.ringKrullDim_stalk_eq_of_specializes_of_quasiFiniteAt — and that is what makes 𝒪_{X,x} Cohen–Macaulay, whence the conclusion. The Cohen–Macaulay step is where [Stacks, Tag 0BMA] clause (2) enters, through Stacks.PurityBranchLocus.purityFiniteNormal.

public theorem etaleAt_of_quasiFiniteAt_of_unramifiedAt_codimensionOne
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian X] [IsLocallyNoetherian Y] (x : X)
    (hX : IsNormalRing (X.presheaf.stalk x))
    (hY : IsRegularLocalRing (Y.presheaf.stalk (f x)))
    (hqf : quasiFiniteAt f x)
    (hdim : ringKrullDim (X.presheaf.stalk x) = ringKrullDim (Y.presheaf.stalk (f x)))
    (hone : 1 ≤ ringKrullDim (X.presheaf.stalk x))
    (hunr : ∀ x' : X, x' ⤳ x → ringKrullDim (X.presheaf.stalk x') = 1 → UnramifiedAt f x') :
    EtaleAt f x

AlgebraicGeometry.etaleAt_of_quasiFiniteAt_of_unramifiedAt_codimensionOne_of_dim_le_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/DimensionAtMostTwo.lean, line 232. The attribute's comment: “the case 1 ≤ dim 𝒪_{X,x} = dim 𝒪_{Y,f x} ≤ 2. Hypotheses (1), (2), (3) and (5) are the tag's own; hypothesis (4) is the tag's dim 𝒪_{X,x} = dim 𝒪_{Y,f x} ≥ 1 together with the case restriction dim 𝒪_{X,x} ≤ 2. Flatness of 𝒪_{Y,f x} → 𝒪_{X,x} is miracle flatness (tag 00R4), a normal Noetherian local ring of dimension at most two being Cohen–Macaulay by Serre's criterion (tag 031S) and the fibre ring being zero-dimensional by quasi-finiteness; étaleness at x then follows from tag 0BJH. For dim 𝒪_{X,x} ≥ 3 the same reduction leaves exactly the flatness of 𝒪_{Y,f x} → 𝒪_{X,x}, which is tag 0BMA clause (2) at a general dimension. See the module docstring.”. References: EGA IV (21.12.14), “(v), (v), special case”; SGA 1 X (3.1), “partial, special case”.

Purity of the branch locus, [Stacks, Tag 0BMB], in dimension at most two. Let f : X ⟶ Y be a morphism of locally Noetherian schemes and let x : X be a point whose local ring is normal, with regular local ring at f x, at which f is quasi-finite, and such that the two local rings have the same dimension, which is at least one and at most two. If f is unramified at every point specializing to x whose local ring has dimension one, then f is étale at x.

This is the tag with its hypothesis 1 ≤ dim 𝒪_{X,x} supplemented by dim 𝒪_{X,x} ≤ 2. See the module docstring for what the case dim 𝒪_{X,x} ≥ 3 comes down to.

public theorem etaleAt_of_quasiFiniteAt_of_unramifiedAt_codimensionOne_of_dim_le_two
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian X] [IsLocallyNoetherian Y] (x : X)
    (hX : IsNormalRing (X.presheaf.stalk x))
    (hY : IsRegularLocalRing (Y.presheaf.stalk (f x)))
    (hqf : quasiFiniteAt f x)
    (hdim : ringKrullDim (X.presheaf.stalk x) = ringKrullDim (Y.presheaf.stalk (f x)))
    (hone : 1 ≤ ringKrullDim (X.presheaf.stalk x))
    (hle : ringKrullDim (X.presheaf.stalk x) ≤ 2)
    (hunr : ∀ x' : X, x' ⤳ x → ringKrullDim (X.presheaf.stalk x') = 1 → UnramifiedAt f x') :
    EtaleAt f x

AlgebraicGeometry.etaleAt_of_quasiFiniteAt_of_unramifiedAt_codimensionOne_of_dim_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/DimensionOne.lean, line 201. The attribute's comment: “the case dim 𝒪_{X,x} = dim 𝒪_{Y,f x} = 1, which is the base case of the source's induction on the dimension; hypotheses (1), (2), (3) and (5) are the tag's own and hypothesis (4) is the tag's with 1 ≤ d restricted to d = 1. The range 1 ≤ d ≤ 2 is etaleAt_of_quasiFiniteAt_of_unramifiedAt_codimensionOne_of_dim_le_two in PurityBranchLocus.DimensionAtMostTwo.”. References: EGA IV (21.12.14), “(v)”; SGA 1 X (3.1), “partial”.

Purity of the branch locus, [Stacks, Tag 0BMB], in dimension one. Let f : X ⟶ Y be a morphism of locally Noetherian schemes and let x : X be a point whose local ring is normal, with regular local ring at f x, at which f is quasi-finite, and such that the two local rings have the same dimension, equal to one. If f is unramified at every point specializing to x whose local ring has dimension one, then f is étale at x.

This is the tag with its hypothesis 1 ≤ dim 𝒪_{X,x} restricted to dim 𝒪_{X,x} = 1, the base case of the source's induction on the dimension. The whole range 1 ≤ dim 𝒪_{X,x} ≤ 2 is etaleAt_of_quasiFiniteAt_of_unramifiedAt_codimensionOne_of_dim_le_two in PurityBranchLocus.DimensionAtMostTwo, which subsumes this statement.

theorem etaleAt_of_quasiFiniteAt_of_unramifiedAt_codimensionOne_of_dim_eq_one
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian X] [IsLocallyNoetherian Y] (x : X)
    (hX : IsNormalRing (X.presheaf.stalk x))
    (hY : IsRegularLocalRing (Y.presheaf.stalk (f x)))
    (hqf : quasiFiniteAt f x)
    (hdim : ringKrullDim (X.presheaf.stalk x) = ringKrullDim (Y.presheaf.stalk (f x)))
    (hone : ringKrullDim (X.presheaf.stalk x) = 1)
    (hunr : ∀ x' : X, x' ⤳ x → ringKrullDim (X.presheaf.stalk x') = 1 → UnramifiedAt f x') :
    EtaleAt f x

Tag 0EY6, a lemma

Tag 0EY6 in the Stacks Project.

Stacks.FundamentalGroup.flatBaseChange_algebraPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleAlgebra/FlatBaseChange/AlgebraComparisonEpi.lean, line 395. The attribute's comment: “flat_base_change”.

The base-change clause of [Stacks, Tag 0EY6]. For a quasi-compact quasi-separated morphism f : V ⟶ Y and a flat morphism q : Y' ⟶ Y, the pushed-forward structure sheaf of the base change is the extension of scalars of the inverse image of f_* 𝒪_V.

public theorem flatBaseChange_algebraPullback {V Y Y' : Scheme.{u}} (f : V ⟶ Y)
    [QuasiCompact f] [QuasiSeparated f] (q : Y' ⟶ Y) [Flat q] :
    IsPushout
      ((TopCat.Sheaf.pullback CommRingCat q.base).map (pushforwardAlgebra f).hom)
      (inverseImageStructureMap q)
      (pushforwardBaseChangeMap q (Over.mk f))
      (pushforwardAlgebra ((Over.pullback q).obj (Over.mk f)).hom).hom

Stacks.FundamentalGroup.exists_extendedEtaleAlgebraComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleAlgebra/FlatBaseChange/ExtensionAlgebra.lean, line 266. The attribute's comment: “flat_base_change”.

[Stacks, Tag 0EY6], flat base change of the extension algebra. Let X be locally Noetherian, j : U ⟶ X an open immersion whose complement carries depth at least two and π : V ⟶ U a finite étale cover, and let g : X' ⟶ X be flat with j' the base change of j and π' the base change of π. Then every extension of scalars of the extension algebra 𝓑 = (π ≫ j)_* 𝒪_V along g is canonically isomorphic to the extension algebra (π' ≫ j')_* 𝒪_{V'} of the base-changed cover, by an isomorphism carrying the canonical map g⁻¹𝓑 ⟶ g⁺𝓑 to the base-change morphism transported along the Cartesian comparison of covers.

This is stated for an arbitrary Stacks.RelativeSpec.AlgebraPullback, hence in particular for any choice of one; exists_extendedEtaleAlgebraComparison_algebraPullbackOfFlat is the instance at algebraPullbackOfFlat.

public theorem exists_extendedEtaleAlgebraComparison {U X V U' X' V' : Scheme.{u}}
    [IsLocallyNoetherian X] [IsLocallyNoetherian X']
    (j : U ⟶ X) [IsOpenImmersion j]
    (π : V ⟶ U) [IsFinite π] [Etale π]
    (g : X' ⟶ X) [Flat g]
    (j' : U' ⟶ X') [IsOpenImmersion j'] (gU : U' ⟶ U)
    (π' : V' ⟶ U') [IsFinite π'] [Etale π'] (gV : V' ⟶ V)
    (hj : IsPullback j' gU g j)
    (hπ : IsPullback π' gV gU π)
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (X.presheaf.stalk x))
    (d : AlgebraPullback (ExtendedEtaleFold.extendedEtaleSituation j π hdepth) g) :
    let hdepth' := extendedEtaleDepth_flatBaseChange j g j' gU hj hdepth
    let e : Over.mk (π' ≫ j') ≅ (Over.pullback g).obj (Over.mk (π ≫ j)) :=
      Over.isoMk (hπ.paste_horiz hj).flip.isoPullback (by simp)
    ∃ i : d.algebra ≅
        (ExtendedEtaleFold.extendedEtaleSituation j' π' hdepth').algebra,
      d.map ≫ i.hom.right =
        pushforwardBaseChangeMap g (Over.mk (π ≫ j)) ≫
          (pushforwardAlgebraMap e.hom).right

Stacks.FundamentalGroup.extendedEtaleAlgebraComparison_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleAlgebra/FlatBaseChange/SpectrumComparison.lean, line 125. The attribute's comment: “flat_base_change”.

The comparison carries the canonical map of the extension of scalars to the base-change morphism, transported along the Cartesian comparison of covers. This is the property that specifies Stacks.FundamentalGroup.extendedEtaleAlgebraComparison.

public theorem extendedEtaleAlgebraComparison_map {U X V U' X' V' : Scheme.{u}}
    [IsLocallyNoetherian X] [IsLocallyNoetherian X']
    (j : U ⟶ X) [IsOpenImmersion j]
    (π : V ⟶ U) [IsFinite π] [Etale π]
    (g : X' ⟶ X) [Flat g]
    (j' : U' ⟶ X') [IsOpenImmersion j'] (gU : U' ⟶ U)
    (π' : V' ⟶ U') [IsFinite π'] [Etale π'] (gV : V' ⟶ V)
    (hj : IsPullback j' gU g j)
    (hπ : IsPullback π' gV gU π)
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (X.presheaf.stalk x))
    (d : AlgebraPullback (ExtendedEtaleFold.extendedEtaleSituation j π hdepth) g) :
    d.map ≫
        (extendedEtaleAlgebraComparison j π g j' gU π' gV hj hπ hdepth d).hom.right =
      pushforwardBaseChangeMap g (Over.mk (π ≫ j)) ≫
        (pushforwardAlgebraMap
          (Over.isoMk (hπ.paste_horiz hj).flip.isoPullback (by simp) :
            Over.mk (π' ≫ j') ≅ (Over.pullback g).obj (Over.mk (π ≫ j))).hom).right

Stacks.FundamentalGroup.extendedEtaleSpectrumComparison_universalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleAlgebra/FlatBaseChange/SpectrumComparison.lean, line 187. The attribute's comment: “flat_base_change”.

[Stacks, Tag 0EY6], the universal-map equation for the spectrum comparison. Under the representing bijection of [Stacks, Tag 01LV] the comparison is the structure morphism of the base-changed relative spectrum together with its universal algebra map precomposed with the algebra comparison. This is the defining property of Stacks.FundamentalGroup.extendedEtaleSpectrumComparison, so it holds by Equiv.apply_symm_apply.

public theorem extendedEtaleSpectrumComparison_universalMap {U X V U' X' V' : Scheme.{u}}
    [IsLocallyNoetherian X] [IsLocallyNoetherian X']
    (j : U ⟶ X) [IsOpenImmersion j]
    (π : V ⟶ U) [IsFinite π] [Etale π]
    (g : X' ⟶ X) [Flat g]
    (j' : U' ⟶ X') [IsOpenImmersion j'] (gU : U' ⟶ U)
    (π' : V' ⟶ U') [IsFinite π'] [Etale π'] (gV : V' ⟶ V)
    (hj : IsPullback j' gU g j)
    (hπ : IsPullback π' gV gU π)
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (X.presheaf.stalk x))
    (d : AlgebraPullback (ExtendedEtaleFold.extendedEtaleSituation j π hdepth) g) :
    let e := ExtendedEtaleFold.extendedEtaleSituation j' π'
      (extendedEtaleDepth_flatBaseChange j g j' gU hj hdepth)
    (relativeSpecRepresentableBy d.situation).homEquiv
        (extendedEtaleSpectrumComparison j π g j' gU π' gV hj hπ hdepth d) =
      ⟨(gluedSpectrum e).toBase,
        algebraHomAsUnder
            (extendedEtaleAlgebraComparison j π g j' gU π' gV hj hπ hdepth d).hom ≫
          universalAlgebraMap e⟩

Stacks.FundamentalGroup.isIso_extendedEtaleSpectrumComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleAlgebra/FlatBaseChange/SpectrumComparison.lean, line 216. The attribute's comment: “flat_base_change”.

[Stacks, Tag 0EY6], the spectrum comparison is an isomorphism. The two relative spectra represent functors identified by Stacks.RelativeSpec.relativeSpecFunctorIsoOfAlgebraIso, and the comparison is the induced comparison of representing objects.

public theorem isIso_extendedEtaleSpectrumComparison {U X V U' X' V' : Scheme.{u}}
    [IsLocallyNoetherian X] [IsLocallyNoetherian X']
    (j : U ⟶ X) [IsOpenImmersion j]
    (π : V ⟶ U) [IsFinite π] [Etale π]
    (g : X' ⟶ X) [Flat g]
    (j' : U' ⟶ X') [IsOpenImmersion j'] (gU : U' ⟶ U)
    (π' : V' ⟶ U') [IsFinite π'] [Etale π'] (gV : V' ⟶ V)
    (hj : IsPullback j' gU g j)
    (hπ : IsPullback π' gV gU π)
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (X.presheaf.stalk x))
    (d : AlgebraPullback (ExtendedEtaleFold.extendedEtaleSituation j π hdepth) g) :
    IsIso (extendedEtaleSpectrumComparison j π g j' gU π' gV hj hπ hdepth d)

Stacks.FundamentalGroup.ExtendedEtaleFold.extendedEtaleAlgebra_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtale/Algebra.lean, line 134. The attribute's comment: “algebra”.

The extension algebra of a finite étale cover is a coherent module over the base. Let j : U ⟶ X be an open immersion into a locally Noetherian scheme whose complement carries depth at least two and let π : V ⟶ U be finite étale. Then the 𝒪_X-module underlying 𝓑 = (π ≫ j)_* 𝒪_V is coherent.

public theorem extendedEtaleAlgebra_isCoherent {U X V : Scheme.{u}} [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] (π : V ⟶ U) [IsFinite π] [Etale π]
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) :
    _root_.SheafOfModules.IsCoherent
      (AlgebraSheaf.underlyingModule (pushforwardAlgebra (π ≫ j)))

Stacks.FundamentalGroup.ExtendedEtaleFold.extendedEtaleAlgebra_isReflexive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtale/Algebra.lean, line 149. The attribute's comment: “algebra”.

The extension algebra of a finite étale cover is reflexive as a module over the base. Let j : U ⟶ X be an open immersion into a locally Noetherian scheme whose complement carries depth at least two and let π : V ⟶ U be finite étale. Then the 𝒪_X-module underlying 𝓑 = (π ≫ j)_* 𝒪_V is reflexive.

public theorem extendedEtaleAlgebra_isReflexive {U X V : Scheme.{u}} [IsLocallyNoetherian X]
    (j : U ⟶ X) [IsOpenImmersion j] (π : V ⟶ U) [IsFinite π] [Etale π]
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) :
    IsReflexive (AlgebraSheaf.underlyingModule (pushforwardAlgebra (π ≫ j)))

Stacks.FundamentalGroup.ExtendedEtaleFold.extendedEtaleSituation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtale/Algebra.lean, line 165. The attribute's comment: “algebra”.

The extension algebra, with its quasi-coherence, as a relative-spectrum situation. It is the pair consisting of X and the quasi-coherent 𝒪_X-algebra 𝓑 = (π ≫ j)_* 𝒪_V, whose relative spectrum Spec_X(𝓑) is the extension scheme of the cover.

public def extendedEtaleSituation {U X V : Scheme.{u}} [IsLocallyNoetherian X] (j : U ⟶ X)
    [IsOpenImmersion j] (π : V ⟶ U) [IsFinite π] [Etale π]
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) :
    Stacks.RelativeSpec.RelativeSpecSituation.{u}

Stacks.FundamentalGroup.extendedEtaleSpectrum_flatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtale/FlatBaseChangeSquare.lean, line 122. The attribute's comment: “flat_base_change”.

The flat_base_change clause of [Stacks, Tag 0EY6], the Cartesian square of relative spectra. Let X be locally Noetherian, j : U ⟶ X an open immersion whose complement carries depth at least two and π : V ⟶ U a finite étale cover, and let g : X' ⟶ X be flat with j' the base change of j and π' the base change of π. Then Spec_{X'}((π' ≫ j')_* 𝒪_{V'}) is the fibre product of Spec_X((π ≫ j)_* 𝒪_V) with X' over X.

The morphism exhibiting it is the comparison extendedEtaleSpectrumComparison of the two algebras on X' — an isomorphism over X', because flat base change identifies the extension of scalars of (π ≫ j)_* 𝒪_V with (π' ≫ j')_* 𝒪_{V'} — followed by the canonical base-change morphism Stacks.RelativeSpec.relativeSpectrumBaseChangeMap, whose square is Cartesian by [Stacks, Tag 01LX] part (2). Transporting the latter square along the former isomorphism is extendedEtaleSpectrum_flatBaseChange_of_isPullback.

public theorem extendedEtaleSpectrum_flatBaseChange {U X V U' X' V' : Scheme.{u}}
    [IsLocallyNoetherian X] [IsLocallyNoetherian X']
    (j : U ⟶ X) [IsOpenImmersion j]
    (π : V ⟶ U) [IsFinite π] [Etale π]
    (g : X' ⟶ X) [Flat g]
    (j' : U' ⟶ X') [IsOpenImmersion j'] (gU : U' ⟶ U)
    (π' : V' ⟶ U') [IsFinite π'] [Etale π'] (gV : V' ⟶ V)
    (hj : IsPullback j' gU g j)
    (hπ : IsPullback π' gV gU π)
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (X.presheaf.stalk x)) :
    IsPullback
      (gluedSpectrum (ExtendedEtaleFold.extendedEtaleSituation j' π'
        (extendedEtaleDepth_flatBaseChange j g j' gU hj hdepth))).toBase
      (extendedEtaleSpectrumComparison j π g j' gU π' gV hj hπ hdepth
            (pullbackAlgebra (ExtendedEtaleFold.extendedEtaleSituation j π hdepth) g) ≫
        relativeSpectrumBaseChangeMap (ExtendedEtaleFold.extendedEtaleSituation j π hdepth) g)
      g (gluedSpectrum (ExtendedEtaleFold.extendedEtaleSituation j π hdepth)).toBase

Stacks.FundamentalGroup.ExtendedEtaleFold.existsUnique_restrictionIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtale/LargerOpenIso.lean, line 68. The attribute's comment: “larger_open”.

The larger_open clause of [Stacks, Tag 0EY6]. Let i : U ⟶ U' and k : U' ⟶ X be open immersions into a locally Noetherian scheme with X ∖ (i ≫ k)(U) of depth at least two, let π : V ⟶ U be a finite étale cover and let Y = Spec_X(𝓑) be its canonical extension, for 𝓑 = (π ≫ i ≫ k)_* 𝒪_V. Given a finite étale cover π' : V' ⟶ U' of the larger open subscheme, an identification eY of the restriction of Y to U with π, and an identification eV of the restriction of π' to U with π, there is exactly one isomorphism over U' between the restriction of Y to U' and π' whose own restriction to U carries eV back to eY.

Both Y ×_X U' and V' are finite over U', restrict over U to π, and have depth at least two above U' ∖ i(U); so extendedEtale_unique, over the base U', identifies each with the extension of π across that complement, and the isomorphism is the composite of those two identifications. Its uniqueness is the uniqueness in that clause.

public theorem existsUnique_restrictionIso {U U' X V V' : Scheme.{u}} [IsLocallyNoetherian X]
    (i : U ⟶ U') [IsOpenImmersion i] (k : U' ⟶ X) [IsOpenImmersion k]
    (π : V ⟶ U) [IsFinite π] [Etale π] (π' : V' ⟶ U') [IsFinite π'] [Etale π']
    (hdepth : ∀ x : X, x ∉ ((i ≫ k).opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) :
    let Y := gluedSpectrum (extendedEtaleSituation (i ≫ k) π hdepth)
    ∀ (eY : (Over.pullback (i ≫ k)).obj (Over.mk Y.toBase) ≅ Over.mk π)
      (eV : (Over.pullback i).obj (Over.mk π') ≅ Over.mk π),
      ∃! e : (Over.pullback k).obj (Over.mk Y.toBase) ≅ Over.mk π',
        (Over.pullbackComp i k).hom.app (Over.mk Y.toBase) ≫
          (Over.pullback i).map e.hom ≫ eV.hom = eY.hom

Stacks.FundamentalGroup.ExtendedEtaleFold.etaleAt_iff_isFlatAt_extendedEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtale/Purity.lean, line 148. The attribute's comment: “etale_iff_flat”.

The etale_iff_flat clause of [Stacks, Tag 0EY6]. Let j : U ⟶ X be an open immersion into a locally Noetherian scheme whose complement carries depth at least two and let π : V ⟶ U be finite étale. At every point of the canonical extension Y = Spec_X(𝓑), for 𝓑 = (π ≫ j)_* 𝒪_V, the structure morphism Y ⟶ X is étale if and only if it is flat.

Forwards this is one half of "étale is flat and G-unramified". Backwards, write W for the flat locus of Y ⟶ X, an open subscheme by [Stacks, Tag 05IM] since the base has locally finite weakly associated points, and let y ∈ W. If y lies over the open j(U) then Y ⟶ X is étale at y outright, because over j(U) it is the finite étale cover π (extendedEtaleCoverMap_isPullback). Otherwise the depth clause (extendedEtale_depth_ge_two) gives depth 𝒪_{Y, y} ≥ 2, hence dim 𝒪_{Y, y} ≥ 2; so y is not a generic point of a component of W, and any z ⤳ y with dim 𝒪_{W, z} = 1 must lie over j(U), where Y ⟶ X is étale and so unramified. Those are the hypotheses of [Stacks, Tag 0BJH], which turns flatness at y into étaleness at y.

public theorem etaleAt_iff_isFlatAt_extendedEtale {U X V : Scheme.{u}}
    [IsLocallyNoetherian X] (j : U ⟶ X) [IsOpenImmersion j]
    (π : V ⟶ U) [IsFinite π] [Etale π]
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) :
    let Y := gluedSpectrum (extendedEtaleSituation j π hdepth)
    ∀ y : Y.scheme,
      EtaleAt Y.toBase y ↔ IsFlatAt Y.toBase.toLRSHom.toShHom y

Stacks.FundamentalGroup.ExtendedEtaleFold.etale_iff_isFiniteLocallyFree_extendedEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtale/Purity.lean, line 238. The attribute's comment: “etale_iff_free”.

The etale_iff_free clause of [Stacks, Tag 0EY6]. The structure morphism of the canonical extension Y = Spec_X(𝓑) is étale if and only if 𝓑 = (π ≫ j)_* 𝒪_V is finite locally free as an 𝒪_X-module.

The chain is: étale means étale at every point (AlgebraicGeometry.etale_iff_forall_etaleAt); at every point étale is flat (etaleAt_iff_isFlatAt_extendedEtale); flat at every point means flat (AlgebraicGeometry.Flat.iff_flat_stalkMap); and for a morphism over a locally Noetherian base finite plus flat is finite locally free ([Stacks, Tag 02KB]), which for an affine morphism is finite local freeness of the direct image of its structure sheaf ([Stacks, Tag 02KA]). That direct image is 𝓑 itself, because Y is the relative spectrum of 𝓑 (Stacks.AffineAlgebraEquivalence.pushforwardAlgebraIso).

public theorem etale_iff_isFiniteLocallyFree_extendedEtale {U X V : Scheme.{u}}
    [IsLocallyNoetherian X] (j : U ⟶ X) [IsOpenImmersion j]
    (π : V ⟶ U) [IsFinite π] [Etale π]
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) :
    let Y := gluedSpectrum (extendedEtaleSituation j π hdepth)
    Etale Y.toBase ↔
      _root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (AlgebraSheaf.underlyingModule (pushforwardAlgebra (π ≫ j)))

Stacks.FundamentalGroup.ExtendedEtaleFold.isFinite_extendedEtaleToBase, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtale/UniqueExtension.lean, line 70. The attribute's comment: “unique_extension”.

The extension of a finite étale cover across a depth-two complement is finite over the base: the structure morphism of Spec_X(𝓑), for 𝓑 = (π ≫ j)_* 𝒪_V, is a finite morphism.

public instance isFinite_extendedEtaleToBase : IsFinite (extendedEtaleToBase j π hdepth)

Stacks.FundamentalGroup.ExtendedEtaleFold.extendedEtaleCoverMap_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtale/UniqueExtensionCover.lean, line 134. The attribute's comment: “unique_extension”.

The comparison morphism identifies the cover with the restriction of the extension to the open subscheme. This is the pullback clause of [Stacks, Tag 0EY6]: the square formed by the cover π, the comparison morphism, the open immersion j and the structure morphism of the extension is cartesian.

public theorem extendedEtaleCoverMap_isPullback :
    IsPullback π (extendedEtaleCoverMap j π hdepth) j
      (gluedSpectrum (extendedEtaleSituation j π hdepth)).toBase

Stacks.FundamentalGroup.ExtendedEtaleFold.extendedEtale_depth_ge_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtale/UniqueExtensionDepth.lean, line 284. The attribute's comment: “unique_extension”.

The depth clause of [Stacks, Tag 0EY6]. The local rings of the extension Spec_X(𝓑) of a finite étale cover across a depth-two complement have depth at least two above every point of X outside the cover.

The stalk of 𝓑 at such a point has depth at least two over the local ring of the base (two_le_depth_stalk_extendedEtaleAlgebra); the local ring of Spec_X(𝓑) at a point above it is a localization of that stalk at a maximal ideal, so its depth is at least as large (depth_stalk_pushforwardAlgebra_le_depth_stalk). The identification of 𝓑 with the structure algebra of its own relative spectrum is Stacks.AffineAlgebraEquivalence.pushforwardAlgebraIso.

public theorem extendedEtale_depth_ge_two :
    let Y := (relativeSpectrum (extendedEtaleSituation j π hdepth)).scheme
    let f := (relativeSpectrum (extendedEtaleSituation j π hdepth)).toBase
    ∀ y : Y, f y ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (Y.presheaf.stalk y)
        (IsLocalRing.maximalIdeal (Y.presheaf.stalk y))
        (Y.presheaf.stalk y)

Stacks.FundamentalGroup.ExtendedEtaleFold.extendedEtale_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtale/UniqueExtensionUniqueness.lean, line 245. The attribute's comment: “unique_extension”.

The extension of a finite étale cover is the unique finite extension with the same restriction over the open subscheme and the same depth condition off it. This is the uniqueness clause of [Stacks, Tag 0EY6]: for any finite f' : Y' ⟶ X whose restriction over U is the given cover and whose local rings off U have depth at least two, there is exactly one isomorphism of Y' with the relative spectrum of (π ≫ j)_* 𝒪_V commuting both with the structure morphisms to X and with the canonical comparison from the cover.

public theorem extendedEtale_unique {U X V Y' : Scheme.{u}}
    [IsLocallyNoetherian X] (j : U ⟶ X) [IsOpenImmersion j]
    (π : V ⟶ U) [IsFinite π] [Etale π]
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (X.presheaf.stalk x))
    (f' : Y' ⟶ X) [IsFinite f'] (g' : V ⟶ Y')
    (hg' : IsPullback π g' j f')
    (hdepth' : ∀ y : Y', f' y ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (Y'.presheaf.stalk y)
        (IsLocalRing.maximalIdeal (Y'.presheaf.stalk y))
        (Y'.presheaf.stalk y)) :
    ∃! e : Y' ≅ (gluedSpectrum (extendedEtaleSituation j π hdepth)).scheme,
      (e.hom ≫ (gluedSpectrum (extendedEtaleSituation j π hdepth)).toBase = f') ∧
      (g' ≫ e.hom = extendedEtaleCoverMap j π hdepth)

Stacks.FundamentalGroup.extendedEtaleDepth_flatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ExtendedEtaleBaseChange.lean, line 92. The attribute's comment: “flat_base_change”.

Stacks 0EY6, flat base change: the depth condition. Depth at least two outside the open subscheme persists after flat base change: if the local rings of X at the points outside the open U have depth at least two and g : X' ⟶ X is flat with U' = g⁻¹(U), then the local rings of X' at the points outside U' have depth at least two.

This is one of the seven declarations making up tag 0EY6's flat_base_change clause. All seven are now proved — the last was the Cartesian square of relative spectra, in StacksFrontier.AlgebraicGeometry.FundamentalGroup.ExtendedEtale.FlatBaseChangeSquare — so each carries @[stacks 0EY6 "flat_base_change"], the clause string recording which part of the tag is covered.

theorem extendedEtaleDepth_flatBaseChange {U X U' X' : Scheme.{u}}
    [IsLocallyNoetherian X] [IsLocallyNoetherian X']
    (j : U ⟶ X) [IsOpenImmersion j]
    (g : X' ⟶ X) [Flat g]
    (j' : U' ⟶ X') [IsOpenImmersion j'] (gU : U' ⟶ U)
    (hj : IsPullback j' gU g j)
    (hdepth : ∀ x : X, x ∉ (j.opensRange : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (X.presheaf.stalk x)) :
    ∀ x' : X', x' ∉ (j'.opensRange : Set X') →
      (2 : ℕ∞) ≤ Module.depth (X'.presheaf.stalk x')
        (IsLocalRing.maximalIdeal (X'.presheaf.stalk x'))
        (X'.presheaf.stalk x')

Tag 0EY7, a lemma

Tag 0EY7 in the Stacks Project.

AlgebraicGeometry.essSurj_finiteEtaleBaseChange_of_hasPurity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/ExtendFiniteEtale.lean, line 346.

Stacks Project, Tag 0EY7. Let j : U ⟶ X be an open immersion of Noetherian schemes such that purity holds for 𝒪_{X, x} at every point x outside the image of j. Then every finite étale cover of U is the restriction of a finite étale cover of X.

theorem essSurj_finiteEtaleBaseChange_of_hasPurity
    {X U : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j] [IsNoetherian X]
    (h : ∀ x : X, x ∉ j.opensRange → HasPurity (X.presheaf.stalk x)) :
    (finiteEtaleBaseChange j).EssSurj

Sources

LeanIsLocalRing.exists_isPrime_height_eq_one_of_mem_maximalIdeal · AlgebraicGeometry.etaleAt_of_flat_of_unramifiedAt_codimensionOne · Stacks.PurityDimensionTwo.quotient_maximalIdeal_counterexample_clauseTwo · Stacks.PurityDimensionTwo.hasPurity_of_ringKrullDim_eq_two · Stacks.PurityDimensionTwo.etale_of_isNormalRing_of_two_le_ringKrullDim · Stacks.PurityDimensionTwo.etale_of_isNormalRing_of_ringKrullDim_eq_two · AlgebraicGeometry.purityAtRegularLocalRings · AlgebraicGeometry.etaleAt_of_quasiFiniteAt_of_unramifiedAt_codimensionOne

Section58.22 Finite étale covers of punctured spectra, II #

Section 58.22 of the Stacks Project, Tag 0BLU. 3 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BLN, a lemma

Tag 0BLN in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.HasLargeMissingComponents.mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FaithfulRestriction.lean, line 260. The attribute's comment: “stability of the dimension hypothesis under shrinking U'”.

The dimension condition passes to smaller opens: a minimal prime in the smaller open lies in the larger one.

theorem HasLargeMissingComponents.mono {S : LocalLefschetzSituation.{u}} {W W' : S.X.Opens}
    (hWW' : W' ≤ W) (hW : S.HasLargeMissingComponents W) :
    S.HasLargeMissingComponents W'

AlgebraicGeometry.LocalLefschetzSituation.faithful_finiteEtaleBaseChange_of_hasLargeMissingComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FaithfulRestriction.lean, line 283. The attribute's comment: “faithfulness of restriction from an open U' with U₀ ⊆ U' ⊆ U”.

Stacks Project, Tag 0BLN. In the local Lefschetz situation let U' be an open of X with U₀ ⊆ U' ⊆ U. If every minimal prime of A lying in U' but not in U₀ has dim (A / 𝔭) ≥ 2, then base change of finite étale covers along U₀ ⟶ U' is faithful.

theorem faithful_finiteEtaleBaseChange_of_hasLargeMissingComponents
    (S : LocalLefschetzSituation.{u}) {W : S.X.Opens} (hW : W ≤ S.UOpen)
    (r : S.U₀ ⟶ W.toScheme) (hr : r ≫ W.ι = S.U₀ToU ≫ S.UOpen.ι)
    (hdim : S.HasLargeMissingComponents W) :
    (finiteEtaleBaseChange r).Faithful

AlgebraicGeometry.LocalLefschetzSituation.exists_hasLargeMissingComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FaithfulRestriction.lean, line 342. The attribute's comment: “existence of an open U' with U₀ ⊆ U' ⊆ U satisfying the dimension hypothesis”.

Stacks Project, Tag 0BLN. In the local Lefschetz situation there is an open U' of X with U₀ ⊆ U' ⊆ U satisfying the dimension hypothesis: remove from U the one-dimensional irreducible components of X that do not meet U₀.

theorem exists_hasLargeMissingComponents (S : LocalLefschetzSituation.{u}) :
    ∃ W : S.X.Opens, W ≤ S.UOpen ∧ S.U₀Open ≤ S.X₀ToX ⁻¹ᵁ W ∧
      S.HasLargeMissingComponents W

AlgebraicGeometry.LocalLefschetzSituation.exists_le_faithful_finiteEtaleBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FaithfulRestriction.lean, line 419. The attribute's comment: “cofinality of the faithful neighbourhoods of U₀ in U, the criterion for faithfulness of restriction from the colimit over all such neighbourhoods”.

Stacks Project, Tag 0BLN. The opens U' with U₀ ⊆ U' ⊆ U for which restriction of finite étale covers to U₀ is faithful are cofinal among all opens between U₀ and U: this is what makes restriction from colim_{U₀ ⊆ U' ⊆ U} FÉt_{U'} to FÉt_{U₀} faithful.

theorem exists_le_faithful_finiteEtaleBaseChange (S : LocalLefschetzSituation.{u})
    {V : S.X.Opens} (hV : V ≤ S.UOpen) (hVU₀ : S.U₀Open ≤ S.X₀ToX ⁻¹ᵁ V) :
    ∃ (W : S.X.Opens) (hWU₀ : S.U₀Open ≤ S.X₀ToX ⁻¹ᵁ W),
      W ≤ V ∧ (finiteEtaleBaseChange (S.homToOpen hWU₀)).Faithful

AlgebraicGeometry.LocalLefschetzSituation.exists_le_finiteEtaleBaseChange_map_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FaithfulRestriction.lean, line 434. The attribute's comment: “faithfulness of restriction from the colimit over the opens between U₀ and U, written out on representatives of the filtered colimit”.

Stacks Project, Tag 0BLN. Two morphisms of finite étale covers of an open U' with U₀ ⊆ U' ⊆ U which agree after base change to U₀ already agree after base change to some smaller open U'' with U₀ ⊆ U'' ⊆ U'. This is faithfulness of the restriction functor colim_{U₀ ⊆ U' ⊆ U} FÉt_{U'} ⟶ FÉt_{U₀} written out on representatives.

theorem exists_le_finiteEtaleBaseChange_map_eq (S : LocalLefschetzSituation.{u})
    {V : S.X.Opens} (hV : V ≤ S.UOpen) (hVU₀ : S.U₀Open ≤ S.X₀ToX ⁻¹ᵁ V)
    {A B : FiniteEtaleOver V.toScheme} (a b : A ⟶ B)
    (hab : (finiteEtaleBaseChange (S.homToOpen hVU₀)).map a =
      (finiteEtaleBaseChange (S.homToOpen hVU₀)).map b) :
    ∃ (W : S.X.Opens) (_ : S.U₀Open ≤ S.X₀ToX ⁻¹ᵁ W) (hWV : W ≤ V),
      (finiteEtaleBaseChange (S.X.homOfLE hWV)).map a =
        (finiteEtaleBaseChange (S.X.homOfLE hWV)).map b

Tag 0DXX, a lemma

Tag 0DXX in the Stacks Project.

Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_puncturedSpectrum_of_three_le_ringKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ReducedThickening/ThreeDimensionalReduction.lean, line 318. The attribute's comment: “the whole statement, under the source's hypotheses only: a dualizing complex and f-adic completeness, and dimension at least three for every irreducible component of X not contained in the zero locus of f”.

Restriction of finite étale covers from the neighbourhoods of U₀ in U is fully faithful. Let (A, 𝔪) be a Noetherian local ring, f ∈ A, X = Spec A, X₀ = V(f), U = X ∖ {𝔪} and U₀ = U ∩ V(f). Assume A has a dualizing complex, is f-adically complete, and that every irreducible component of X not contained in X₀ has dimension at least 3 — that is, dim (A/𝔭) ≥ 3 for every minimal prime 𝔭 of A with f ∉ 𝔭. Then the restriction functor colim_{U₀ ⊆ U' ⊆ U open} FÉt_{U'} ⟶ FÉt_{U₀} is fully faithful.

The dimension hypothesis is a bound at the minimal primes, whereas the completion theorem behind full faithfulness needs one at the associated primes; so A is first replaced by its reduction, where the associated primes are the minimal primes. The punctured spectrum of the reduction is a thickening of U carrying its closed subscheme cut out by the image of f to U₀, and full faithfulness of restriction is insensitive to such a thickening; a dualizing complex, f-adic completeness and the dimension bound all survive the passage to the reduction.

The dualizing complex is asked for in an arbitrary model of the derived category of A-modules, and moved to the standard model — the one the completion results are stated in — by Stacks.Dualizing.exists_isDualizingComplex_iff_of_models.

theorem finiteEtaleColimitFullyFaithful_puncturedSpectrum_of_three_le_ringKrullDim (A : Type u)
    [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [HasDerivedCategory.{w} (ModuleCat.{u} A)]
    (f : A)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (hcomplete : IsAdicComplete (Ideal.span {f}) A)
    (hdim : ∀ p : PrimeSpectrum A, IsMinimalPrime p.asIdeal → f ∉ p.asIdeal →
      (3 : WithBot ℕ∞) ≤ ringKrullDim (A ⧸ p.asIdeal)) :
    FiniteEtaleColimitFullyFaithful (complementZeroLocus A (maximalIdeal A) : Scheme.{u})
      (idealSheafNearVanishing A (Ideal.span {f}) (maximalIdeal A))

Tag 0BLP, a lemma

Tag 0BLP in the Stacks Project.

Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_puncturedSpectrum_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PuncturedSpectrumFiniteEtaleFullyFaithful.lean, line 139. The attribute's comment: “the full statement, proved from the tag's three hypotheses through 0EKV and 0ELA”.

[Stacks, Tag 0BLP]. In Situation [Stacks, Tag 0BLF] — a Noetherian local ring (A, 𝔪) and f ∈ 𝔪, with U = Spec(A) ∖ {𝔪} the punctured spectrum and U₀ = U ∩ V(f) the closed subscheme of U cut out by f 𝒪_U — assume

A is f-adically complete,

f is a nonzerodivisor, and

H¹_𝔪(A/fA) is a finite A-module.

Then the restriction functor colim_{U₀ ⊆ U' ⊆ U open} FÉt_{U'} ⟶ FÉt_{U₀} is fully faithful.

The proof is the source's: [Stacks, Tag 0EKV] (Stacks.FundamentalGroup.completionFullyFaithfulComplete_puncturedSpectrum_principal) gives full faithfulness of the completion functor colim_{U'} Coh(𝒪_{U'}) ⟶ Coh(U, f𝒪_U) on finite locally free objects, and [Stacks, Tag 0ELA] (Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_of_completionFullyFaithfulComplete) turns that into the conclusion.

theorem finiteEtaleColimitFullyFaithful_puncturedSpectrum_of_isAdicComplete
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (f : A)
    (hf : f ∈ IsLocalRing.maximalIdeal A)
    (hcomplete : IsAdicComplete (Ideal.span {f}) A)
    (hnzd : f ∈ nonZeroDivisors A)
    (hfinite : Module.Finite A (localCohomologyModule A (IsLocalRing.maximalIdeal A)
      (IsLocalRing.maximalIdeal A).fg_of_isNoetherianRing
      (ModuleCat.of A (A ⧸ Ideal.span {f})) 1)) :
    FiniteEtaleColimitFullyFaithful
      (complementZeroLocus A (IsLocalRing.maximalIdeal A) : Scheme)
      (idealSheafNearVanishing A (Ideal.span {f}) (IsLocalRing.maximalIdeal A))

Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_puncturedSpectrum_principal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/RestrictionFromPuncturedSpectrumNeighborhoods.lean, line 122. The attribute's comment: “granted SectionsExtendNearSubscheme in place of the 0EKV completion input”.

[Stacks, Tag 0BLP], granted the section-extension input. In Situation [Stacks, Tag 0BLF] — a Noetherian local ring (A, 𝔪) and an element f ∈ 𝔪, with U = Spec(A) ∖ {𝔪} the punctured spectrum and U₀ = U ∩ V(f) the zero locus of f on it — assume that A is f-adically complete, that f is a nonzerodivisor and that H¹_𝔪(A/fA) is a finite A-module. Then the restriction functor colim_{U₀ ⊆ U' ⊆ U} FÉt_{U'} ⟶ FÉt_{U₀} is fully faithful.

What is granted. The three hypotheses of the tag are recorded but not consumed. They are the hypotheses of [Stacks, Tag 0EKV], whose conclusion — full faithfulness of the completion functor colim_{U'} Coh(𝒪_{U'}) ⟶ Coh(U, f𝒪_U) on the finite locally free objects — is the input the source feeds to [Stacks, Tag 0ELA]; that conclusion is not available in this library, and neither is the passage from it to the section-extension property, which is the remainder of the proof of Tag 0ELA. Accordingly Stacks.FundamentalGroup.SectionsExtendNearSubscheme, the shrinking form of the conclusion of [Stacks, Tag 0EL8] and the actual input of Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_of_sectionsExtendNearSubscheme, is assumed here in place of hypotheses (1)–(3).

theorem finiteEtaleColimitFullyFaithful_puncturedSpectrum_principal
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (f : A)
    (_hf : f ∈ IsLocalRing.maximalIdeal A)
    (_hcomplete : IsAdicComplete (Ideal.span {f}) A)
    (_hnzd : f ∈ nonZeroDivisors A)
    (_hfinite : Module.Finite A (localCohomologyModule A (IsLocalRing.maximalIdeal A)
      (IsLocalRing.maximalIdeal A).fg_of_isNoetherianRing
      (ModuleCat.of A (A ⧸ Ideal.span {f})) 1))
    (hsections : SectionsExtendNearSubscheme
      (complementZeroLocus A (IsLocalRing.maximalIdeal A) : Scheme)
      (idealSheafNearVanishing A (Ideal.span {f}) (IsLocalRing.maximalIdeal A))) :
    FiniteEtaleColimitFullyFaithful
      (complementZeroLocus A (IsLocalRing.maximalIdeal A) : Scheme)
      (idealSheafNearVanishing A (Ideal.span {f}) (IsLocalRing.maximalIdeal A))

Sources

LeanAlgebraicGeometry.LocalLefschetzSituation.HasLargeMissingComponents.mono · AlgebraicGeometry.LocalLefschetzSituation.faithful_finiteEtaleBaseChange_of_hasLargeMissingComponents · AlgebraicGeometry.LocalLefschetzSituation.exists_hasLargeMissingComponents · AlgebraicGeometry.LocalLefschetzSituation.exists_le_faithful_finiteEtaleBaseChange · AlgebraicGeometry.LocalLefschetzSituation.exists_le_finiteEtaleBaseChange_map_eq · Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_puncturedSpectrum_of_three_le_ringKrullDim · Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_puncturedSpectrum_of_isAdicComplete · Stacks.FundamentalGroup.finiteEtaleColimitFullyFaithful_puncturedSpectrum_principal

Section58.23 Finite étale covers of punctured spectra, III #

Section 58.23 of the Stacks Project, Tag 0EK7. 3 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DXY, a lemma

Tag 0DXY in the Stacks Project.

Stacks.FundamentalGroup.finiteEtaleColimitEquivalence_puncturedSpectrum_of_dualizing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/RestrictionColimitDualizingEquivalence.lean, line 327. The attribute's comment: “the restriction functor colim_{U₀ ⊆ U' ⊆ U} FÉt_{U'} → FÉt_{U₀} is an equivalence: fully faithful, and every finite étale cover of U₀ extends to a neighbourhood”.

[Stacks, Tag 0DXY]. In Situation [Stacks, Tag 0BLF] — (A, 𝔪) a Noetherian local ring, f ∈ 𝔪, U = Spec(A) ∖ {𝔪} the punctured spectrum of A and U₀ = U ∩ V(f) the punctured spectrum of A/fA, as the closed subscheme of U cut out by f 𝒪_U — assume

A has a dualizing complex and is f-adically complete, and

one of

(a) A_f is (S₂) and dim(A/𝔭) ≥ 4 for every minimal prime 𝔭 of A with f ∉ 𝔭, or

(b) depth(A_𝔭) + dim(A/𝔭) > 3 for every prime 𝔭 ∉ V(f) with V(𝔭) ∩ V(f) ≠ {𝔪}.

Then the restriction functor colim_{U₀ ⊆ U' ⊆ U open} FÉt_{U'} ⟶ FÉt_{U₀} is an equivalence.

The colimit is directed, so the functor is an equivalence exactly when the two conjuncts below hold. The first is that it is fully faithful, in the form Stacks.FundamentalGroup.FiniteEtaleColimitFullyFaithful: morphisms between restrictions to U₀ come from a smaller neighbourhood, and morphisms agreeing on U₀ agree on a smaller neighbourhood. The second is that it is essentially surjective: every finite étale cover of U₀ is the restriction of a finite étale cover of some open U' with U₀ ⊆ U' ⊆ U.

As in the source, this is [Stacks, Tag 0EK1] for the closed subscheme U₀ of U, with the completion equivalence of [Stacks, Tag 0EKY] as input. Full faithfulness is [Stacks, Tag 0ELA] applied to Stacks.FundamentalGroup.completionFullyFaithfulComplete_puncturedSpectrum_of_dualizing, and the essential image is the algebraization step of [Stacks, Tag 0EK1] fed by that same input together with Stacks.FundamentalGroup.exists_finiteLocallyFree_completion_puncturedSpectrum_of_dualizing.

public theorem finiteEtaleColimitEquivalence_puncturedSpectrum_of_dualizing
    [HasDerivedCategory.{w} (ModuleCat.{u} A)] (hf : f ∈ maximalIdeal A)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (hcomplete : IsAdicComplete (Ideal.span {f}) A)
    (hcond :
      (PropertySkRing (Localization.Away f) 2 ∧
          ∀ p : PrimeSpectrum A, IsMinimalPrime p.asIdeal → f ∉ p.asIdeal →
            (4 : WithBot ℕ∞) ≤ ringKrullDim (A ⧸ p.asIdeal)) ∨
        (∀ p : PrimeSpectrum A, f ∉ p.asIdeal →
          ({q : PrimeSpectrum A | p.asIdeal ≤ q.asIdeal} ∩
            {q : PrimeSpectrum A | f ∈ q.asIdeal}) ≠
            {⟨maximalIdeal A, (maximalIdeal.isMaximal A).isPrime⟩} →
          (3 : WithBot ℕ∞) <
            (Module.depth (Localization.AtPrime p.asIdeal)
              (maximalIdeal (Localization.AtPrime p.asIdeal))
              (Localization.AtPrime p.asIdeal) : WithBot ℕ∞) +
              ringKrullDim (A ⧸ p.asIdeal))) :
    FiniteEtaleColimitFullyFaithful (complementZeroLocus A (maximalIdeal A) : Scheme)
        (idealSheafNearVanishing A (Ideal.span {f}) (maximalIdeal A)) ∧
      ∀ C : FiniteEtaleOver
        (idealSheafNearVanishing A (Ideal.span {f}) (maximalIdeal A)).subscheme,
      ∃ (W : Neighborhood (complementZeroLocus A (maximalIdeal A) : Scheme)
          (idealSheafNearVanishing A (Ideal.span {f}) (maximalIdeal A)))
        (V : FiniteEtaleOver (Neighborhood.open _ _ W).toScheme),
        Nonempty ((finiteEtaleBaseChange (Neighborhood.toSchemeHom _ _ W)).obj V ≅ C)

Tag 0BLV, a lemma

Tag 0BLV in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.isColimitRestrictionEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/NeighbourhoodRestrictionEquivalence.lean, line 328. The attribute's comment: “the equivalence, carrying as explicit hypotheses the purity of restriction FÉt_{Spec (A/fA)} ⟶ FÉt_{U₀} and the purity of restriction FÉt_{Spec A} ⟶ FÉt_{U'} for the opens U₀ ⊆ U' ⊆ U”.

Stacks Project, Tag 0BLV. In the local Lefschetz situation of Stacks 0BLF assume that A is f-adically complete, that f is a nonzerodivisor, and that H¹_𝔪(A / fA) and H²_𝔪(A / fA) are finite A-modules. Then the restriction functor
colim_{U₀ ⊆ U' ⊆ U} FÉt_{U'} ⟶ FÉt_{U₀}
is an equivalence.

Two purity statements are carried as explicit hypotheses, each about a restriction functor out of an affine spectrum and neither about the functor above: that restriction FÉt_{Spec (A / fA)} ⟶ FÉt_{U₀} is an equivalence, and that restriction FÉt_{Spec A} ⟶ FÉt_{U'} is an equivalence for every open U' between U₀ and U. The f-adic completeness hypothesis is discharged: it makes (A, fA) a henselian pair, so that Stacks 09ZS identifies FÉt_{Spec A} with FÉt_{Spec (A / fA)}, which is what turns the two carried statements into the equivalence of restriction from each neighbourhood U' to U₀.

theorem isColimitRestrictionEquivalence (h : S.Hypotheses)
    (hfibre : S.RestrictionToClosedFibreIsEquivalence)
    (hnbhd : S.RestrictionToNeighbourhoodsIsEquivalence) :
    S.IsColimitRestrictionEquivalence

Stacks.FundamentalGroup.finiteEtaleColimitEquivalence_puncturedSpectrum_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/PuncturedNeighbourhoodEquivalence.lean, line 152. The attribute's comment: “the restriction functor colim_{U₀ ⊆ U' ⊆ U} FÉt_{U'} → FÉt_{U₀} is an equivalence: fully faithful, and every finite étale cover of U₀ extends to a neighbourhood”.

[Stacks, Tag 0BLV]. In Situation [Stacks, Tag 0BLF] — (A, 𝔪) a Noetherian local ring, f ∈ 𝔪, U = Spec(A) ∖ {𝔪} the punctured spectrum of A and U₀ = U ∩ V(f) the punctured spectrum of A/fA — assume

A is f-adically complete,

f is a nonzerodivisor, and

H¹_𝔪(A/fA) and H²_𝔪(A/fA) are finite A-modules.

Then the restriction functor colim_{U₀ ⊆ U' ⊆ U} FÉt_{U'} ⟶ FÉt_{U₀} is an equivalence.

The colimit is directed, so the functor is an equivalence exactly when the two conjuncts below hold. The first is that it is fully faithful, in the form Stacks.FundamentalGroup.FiniteEtaleColimitFullyFaithful: morphisms between restrictions to U₀ come from a smaller neighbourhood, and morphisms agreeing on U₀ agree on a smaller neighbourhood. The second is that it is essentially surjective: every finite étale cover of U₀ is the restriction of a finite étale cover of some open U' with U₀ ⊆ U' ⊆ U.

theorem finiteEtaleColimitEquivalence_puncturedSpectrum_of_isAdicComplete
    (hf : f ∈ IsLocalRing.maximalIdeal A)
    (hcomplete : IsAdicComplete (Ideal.span {f}) A) (hnzd : f ∈ nonZeroDivisors A)
    (hH1 : Module.Finite A (localCohomologyModule A (IsLocalRing.maximalIdeal A)
      (IsLocalRing.maximalIdeal A).fg_of_isNoetherianRing
      (ModuleCat.of A (A ⧸ Ideal.span {f})) 1))
    (hH2 : Module.Finite A (localCohomologyModule A (IsLocalRing.maximalIdeal A)
      (IsLocalRing.maximalIdeal A).fg_of_isNoetherianRing
      (ModuleCat.of A (A ⧸ Ideal.span {f})) 2)) :
    FiniteEtaleColimitFullyFaithful (complementZeroLocus A (IsLocalRing.maximalIdeal A) : Scheme)
        (idealSheafNearVanishing A (Ideal.span {f}) (IsLocalRing.maximalIdeal A)) ∧
      ∀ C : FiniteEtaleOver
        (idealSheafNearVanishing A (Ideal.span {f}) (IsLocalRing.maximalIdeal A)).subscheme,
      ∃ (W : Neighborhood (complementZeroLocus A (IsLocalRing.maximalIdeal A) : Scheme)
          (idealSheafNearVanishing A (Ideal.span {f}) (IsLocalRing.maximalIdeal A)))
        (V : FiniteEtaleOver (Neighborhood.open _ _ W).toScheme),
        Nonempty ((finiteEtaleBaseChange (Neighborhood.toSchemeHom _ _ W)).obj V ≅ C)

Tag 0BLW, a remark

Tag 0BLW in the Stacks Project.

AlgebraicGeometry.finiteEtaleColimitEquivalence_puncturedSpectrum_of_propertySk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/CompleteFourDimensional.lean, line 84. The attribute's comment: “the equivalence of the remark, from the tag's own hypotheses: A complete local Noetherian, f ∈ 𝔪 nonzero, A_f satisfying (S₂), and every irreducible component of Spec A of dimension at least 4; nothing beyond them is assumed”.

Stacks Project, Tag 0BLW. Let (A, 𝔪) be a complete local Noetherian ring and let f ∈ 𝔪 be nonzero. Assume A_f satisfies Serre's condition (S₂) and every irreducible component of Spec A has dimension at least 4. Then the restriction functor
colim_{U₀ ⊆ U' ⊆ U open} FÉt_{U'} ⟶ FÉt_{U₀}
is an equivalence, where U = Spec A ∖ {𝔪} and U₀ = U ∩ V(f).

This is Stacks 0DXY under its hypothesis (2)(a). Its hypothesis (1) is available: a complete local Noetherian ring has a dualizing complex by Stacks 0BFR, and it is f-adically complete because f A is contained in the maximal ideal, with respect to which it is complete. The dimension bound of (2)(a) is on the components of Spec A not contained in V(f), so the bound on all of them is more than enough.

theorem finiteEtaleColimitEquivalence_puncturedSpectrum_of_propertySk
    [HasDerivedCategory.{w} (ModuleCat.{u} A)] [IsAdicComplete (maximalIdeal A) A]
    (hf : f ∈ maximalIdeal A) (_hfne : f ≠ 0)
    (hS2 : PropertySkRing (Localization.Away f) 2)
    (hdim : ∀ p : PrimeSpectrum A, IsMinimalPrime p.asIdeal →
      (4 : WithBot ℕ∞) ≤ ringKrullDim (A ⧸ p.asIdeal)) :
    FiniteEtaleColimitFullyFaithful (complementZeroLocus A (maximalIdeal A) : Scheme)
        (idealSheafNearVanishing A (Ideal.span {f}) (maximalIdeal A)) ∧
      ∀ C : FiniteEtaleOver
        (idealSheafNearVanishing A (Ideal.span {f}) (maximalIdeal A)).subscheme,
      ∃ (W : Neighborhood (complementZeroLocus A (maximalIdeal A) : Scheme)
          (idealSheafNearVanishing A (Ideal.span {f}) (maximalIdeal A)))
        (V : FiniteEtaleOver (Neighborhood.open _ _ W).toScheme),
        Nonempty ((finiteEtaleBaseChange (Neighborhood.toSchemeHom _ _ W)).obj V ≅ C)

AlgebraicGeometry.finiteEtaleColimitEquivalence_puncturedSpectrum_of_isIntegrallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/CompleteFourDimensional.lean, line 161. The attribute's comment: “the example at the end of the remark: a complete local normal domain of dimension at least 4, with f ∈ 𝔪 nonzero, satisfies the remark's hypotheses, so the equivalence holds for it; normality is IsDomain together with IsIntegrallyClosed and nothing beyond the remark's own hypotheses is assumed”.

Stacks Project, Tag 0BLW, the example at the end of the remark. The hypotheses of AlgebraicGeometry.finiteEtaleColimitEquivalence_puncturedSpectrum_of_propertySk hold when A is a complete local normal domain of dimension at least 4 and f ∈ 𝔪 is nonzero, so the restriction functor colim_{U₀ ⊆ U' ⊆ U} FÉt_{U'} ⟶ FÉt_{U₀} is an equivalence in that case.

A localization of a normal domain at a set of nonzero elements is again a normal domain, so A_f and each of its local rings is an integrally closed domain; Serre's criterion then gives (S₂) for A_f. The only minimal prime of a domain is (0), and A / (0) = A has dimension at least 4, which is the dimension bound on the irreducible components of Spec A.

theorem finiteEtaleColimitEquivalence_puncturedSpectrum_of_isIntegrallyClosed
    [HasDerivedCategory.{w} (ModuleCat.{u} A)] [IsAdicComplete (maximalIdeal A) A]
    [IsDomain A] [IsIntegrallyClosed A]
    (hdim : (4 : WithBot ℕ∞) ≤ ringKrullDim A) (hf : f ∈ maximalIdeal A) (hfne : f ≠ 0) :
    FiniteEtaleColimitFullyFaithful (complementZeroLocus A (maximalIdeal A) : Scheme)
        (idealSheafNearVanishing A (Ideal.span {f}) (maximalIdeal A)) ∧
      ∀ C : FiniteEtaleOver
        (idealSheafNearVanishing A (Ideal.span {f}) (maximalIdeal A)).subscheme,
      ∃ (W : Neighborhood (complementZeroLocus A (maximalIdeal A) : Scheme)
          (idealSheafNearVanishing A (Ideal.span {f}) (maximalIdeal A)))
        (V : FiniteEtaleOver (Neighborhood.open _ _ W).toScheme),
        Nonempty ((finiteEtaleBaseChange (Neighborhood.toSchemeHom _ _ W)).obj V ≅ C)

Sources

LeanStacks.FundamentalGroup.finiteEtaleColimitEquivalence_puncturedSpectrum_of_dualizing · AlgebraicGeometry.LocalLefschetzSituation.isColimitRestrictionEquivalence · Stacks.FundamentalGroup.finiteEtaleColimitEquivalence_puncturedSpectrum_of_isAdicComplete · AlgebraicGeometry.finiteEtaleColimitEquivalence_puncturedSpectrum_of_propertySk · AlgebraicGeometry.finiteEtaleColimitEquivalence_puncturedSpectrum_of_isIntegrallyClosed

Section58.24 Finite étale covers of punctured spectra, IV #

Section 58.24 of the Stacks Project, Tag 0EK8. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0EK9, a lemma

Tag 0EK9 in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.essSurj_finiteEtaleBaseChange_U₀ToU_of_dualizing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/NeighbourhoodVocabularyDualizing.lean, line 133. The attribute's comment: “the restriction functor FÉt_U ⥤ FÉt_{U₀} is essentially surjective, under the tag's three hypotheses; nothing beyond them is assumed”.

Stacks Project, Tag 0EK9. Let (A, 𝔪) be a Noetherian local ring and let f ∈ 𝔪. Write X = Spec A, let U = X ∖ {𝔪} and U₀ = Spec (A / fA) ∖ {𝔪} be the two punctured spectra. Assume

A has a dualizing complex and is f-adically complete,

one of

(a) A_f satisfies Serre's condition (S₂) and every irreducible component of X not contained in V(f) has dimension at least 4, or

(b) depth(A_𝔭) + dim(A/𝔭) > 3 whenever 𝔭 ∉ V(f) and V(𝔭) ∩ V(f) ≠ {𝔪},

purity holds for (A_f)_𝔭 for every maximal ideal 𝔭 ⊂ A_f.

Then the restriction functor FÉt_U ⥤ FÉt_{U₀} is essentially surjective.

The source's argument is followed. Hypotheses (1) and (2) make the restriction functor colim_{U₀ ⊆ U' ⊆ U} FÉt_{U'} ⥤ FÉt_{U₀} an equivalence, so a given finite étale cover of U₀ is already the restriction of a cover of some open U' of X with U₀ ⊆ U' ⊆ U. The points of U that U' omits correspond to maximal ideals of A_f, so hypothesis (3) makes purity available at each of them and the cover extends from U' across them to a cover of U.

theorem essSurj_finiteEtaleBaseChange_U₀ToU_of_dualizing
    [HasDerivedCategory.{w} (ModuleCat.{u} S.A)]
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hcomplete : IsAdicComplete (Ideal.span {S.f}) S.A)
    (hcond :
      (PropertySkRing (Localization.Away S.f) 2 ∧
          ∀ p : PrimeSpectrum S.A, IsMinimalPrime p.asIdeal → S.f ∉ p.asIdeal →
            (4 : WithBot ℕ∞) ≤ ringKrullDim (S.A ⧸ p.asIdeal)) ∨
        (∀ p : PrimeSpectrum S.A, S.f ∉ p.asIdeal →
          ({q : PrimeSpectrum S.A | p.asIdeal ≤ q.asIdeal} ∩
            {q : PrimeSpectrum S.A | S.f ∈ q.asIdeal}) ≠
            {⟨maximalIdeal S.A, (maximalIdeal.isMaximal S.A).isPrime⟩} →
          (3 : WithBot ℕ∞) <
            (Module.depth (Localization.AtPrime p.asIdeal)
              (maximalIdeal (Localization.AtPrime p.asIdeal))
              (Localization.AtPrime p.asIdeal) : WithBot ℕ∞) +
              ringKrullDim (S.A ⧸ p.asIdeal)))
    (haway : ∀ (p : Ideal (Localization.Away S.f)) [p.IsMaximal],
      HasPurity (Localization.AtPrime p)) :
    (finiteEtaleBaseChange S.U₀ToU).EssSurj

Tag 0EKA, a lemma

Tag 0EKA in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.essSurj_finiteEtaleBaseChange_U₀ToU_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/HypersurfaceExtension.lean, line 247. The attribute's comment: “the restriction functor FÉt_U ⥤ FÉt_{U₀} is essentially surjective, under the tag's four hypotheses; nothing beyond them is assumed”.

Stacks Project, Tag 0EKA. Let (A, 𝔪) be a Noetherian local ring and let f ∈ 𝔪. Assume

A is f-adically complete,

f is a nonzerodivisor,

H¹_𝔪(A/fA) and H²_𝔪(A/fA) are finite A-modules, and

purity holds for (A_f)_𝔭 for every maximal ideal 𝔭 ⊂ A_f.

Then the restriction functor FÉt_U ⥤ FÉt_{U₀} is essentially surjective.

The source proves this by the proof of Stacks 0EK9 with Stacks 0BLV in place of Stacks 0DXY, and that is what happens here. Hypotheses (1)–(3) are the hypotheses of Stacks 0BLV, and give an open U' of X with U₀ ⊆ U' ⊆ U over which a given finite étale cover of U₀ is already defined. The points of U outside U' are maximal ideals of A_f, so hypothesis (4) makes purity available at each of them and the cover extends from U' to U.

theorem essSurj_finiteEtaleBaseChange_U₀ToU_of_isAdicComplete
    (hcomplete : IsAdicComplete S.principalIdeal S.A) (hnzd : S.f ∈ nonZeroDivisors S.A)
    (hH1 : Module.Finite S.A (localCohomologyModule S.A (maximalIdeal S.A)
      (maximalIdeal S.A).fg_of_isNoetherianRing (ModuleCat.of S.A S.quotientRing) 1))
    (hH2 : Module.Finite S.A (localCohomologyModule S.A (maximalIdeal S.A)
      (maximalIdeal S.A).fg_of_isNoetherianRing (ModuleCat.of S.A S.quotientRing) 2))
    (haway : ∀ (p : Ideal (Localization.Away S.f)) [p.IsMaximal],
      HasPurity (Localization.AtPrime p)) :
    (finiteEtaleBaseChange S.U₀ToU).EssSurj

Sources

LeanAlgebraicGeometry.LocalLefschetzSituation.essSurj_finiteEtaleBaseChange_U₀ToU_of_dualizing · AlgebraicGeometry.LocalLefschetzSituation.essSurj_finiteEtaleBaseChange_U₀ToU_of_isAdicComplete

Section58.25 Purity in local case, II #

Section 58.25 of the Stacks Project, Tag 0BPB. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DXZ, a lemma

Tag 0DXZ in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.hasPurity_quotientRing_of_dualizing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/NeighbourhoodVocabularyDualizing.lean, line 175. The attribute's comment: “purity for A/fA under the tag's four hypotheses; nothing beyond them is assumed”.

Stacks Project, Tag 0DXZ. Let (A, 𝔪) be a Noetherian local ring and let f ∈ 𝔪. Write X = Spec A. Assume

A has a dualizing complex and is f-adically complete,

one of

(a) A_f satisfies Serre's condition (S₂) and every irreducible component of X not contained in V(f) has dimension at least 4, or

(b) depth(A_𝔭) + dim(A/𝔭) > 3 whenever 𝔭 ∉ V(f) and V(𝔭) ∩ V(f) ≠ {𝔪},

purity holds for (A_f)_𝔭 for every maximal ideal 𝔭 ⊂ A_f, and

purity holds for A.

Then purity holds for A / fA.

The source's argument is followed. A finite étale cover of the punctured spectrum U₀ of A / fA is, by the essential surjectivity of FÉt_U ⥤ FÉt_{U₀} under (1)–(3), the restriction of a finite étale cover of the punctured spectrum U of A; hypothesis (4) extends the latter over X; and the restriction of that extension to Spec (A / fA) is the desired extension of the original cover.

theorem hasPurity_quotientRing_of_dualizing [HasDerivedCategory.{w} (ModuleCat.{u} S.A)]
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hcomplete : IsAdicComplete (Ideal.span {S.f}) S.A)
    (hcond :
      (PropertySkRing (Localization.Away S.f) 2 ∧
          ∀ p : PrimeSpectrum S.A, IsMinimalPrime p.asIdeal → S.f ∉ p.asIdeal →
            (4 : WithBot ℕ∞) ≤ ringKrullDim (S.A ⧸ p.asIdeal)) ∨
        (∀ p : PrimeSpectrum S.A, S.f ∉ p.asIdeal →
          ({q : PrimeSpectrum S.A | p.asIdeal ≤ q.asIdeal} ∩
            {q : PrimeSpectrum S.A | S.f ∈ q.asIdeal}) ≠
            {⟨maximalIdeal S.A, (maximalIdeal.isMaximal S.A).isPrime⟩} →
          (3 : WithBot ℕ∞) <
            (Module.depth (Localization.AtPrime p.asIdeal)
              (maximalIdeal (Localization.AtPrime p.asIdeal))
              (Localization.AtPrime p.asIdeal) : WithBot ℕ∞) +
              ringKrullDim (S.A ⧸ p.asIdeal)))
    (haway : ∀ (p : Ideal (Localization.Away S.f)) [p.IsMaximal],
      HasPurity (Localization.AtPrime p))
    (hpurity : HasPurity S.A) :
    HasPurity S.quotientRing

Tag 0BPC, a lemma

Tag 0BPC in the Stacks Project.

AlgebraicGeometry.LocalLefschetzSituation.hasPurity_quotientRing_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/HypersurfaceExtension.lean, line 275. The attribute's comment: “purity for A/fA under the tag's five hypotheses; nothing beyond them is assumed”.

Stacks Project, Tag 0BPC. Let (A, 𝔪) be a Noetherian local ring and let f ∈ 𝔪. Assume

A is f-adically complete,

f is a nonzerodivisor,

H¹_𝔪(A/fA) and H²_𝔪(A/fA) are finite A-modules,

purity holds for (A_f)_𝔭 for every maximal ideal 𝔭 ⊂ A_f, and

purity holds for A.

Then purity holds for A / fA.

The source proves this by the proof of Stacks 0DXZ with Stacks 0EKA in place of Stacks 0EK9, and that is what happens here. A finite étale cover of U₀ is, by Stacks 0EKA, the restriction of a finite étale cover of U; hypothesis (5) extends the latter over X; and the restriction of that extension to X₀ = Spec (A / fA) is the extension of the original cover.

theorem hasPurity_quotientRing_of_isAdicComplete
    (hcomplete : IsAdicComplete S.principalIdeal S.A) (hnzd : S.f ∈ nonZeroDivisors S.A)
    (hH1 : Module.Finite S.A (localCohomologyModule S.A (maximalIdeal S.A)
      (maximalIdeal S.A).fg_of_isNoetherianRing (ModuleCat.of S.A S.quotientRing) 1))
    (hH2 : Module.Finite S.A (localCohomologyModule S.A (maximalIdeal S.A)
      (maximalIdeal S.A).fg_of_isNoetherianRing (ModuleCat.of S.A S.quotientRing) 2))
    (haway : ∀ (p : Ideal (Localization.Away S.f)) [p.IsMaximal],
      HasPurity (Localization.AtPrime p))
    (hpurity : HasPurity S.A) :
    HasPurity S.quotientRing

Tag 0BPD, a proposition

Tag 0BPD in the Stacks Project.

AlgebraicGeometry.hasPurity_of_isCompleteIntersectionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/CompleteIntersectionPurity.lean, line 512. The attribute's comment: “purity for a complete intersection local ring of dimension at least three; the complete intersection hypothesis is LocalCompleteIntersection.IsCompleteIntersectionRing (Tag 09Q3 (1)) and purity is AlgebraicGeometry.HasPurity”. References: SGA 2 X (3.4), “3.4(ii)”; SGA 2 XII (3.5), “partial”; SGA 2 XII (4.9), “Clause a)”.

Purity for a complete intersection of dimension at least three, [Stacks, Tag 0BPD]. Let (A, 𝔪) be a Noetherian local ring which is a complete intersection of dimension at least three. Then purity holds for A: every finite étale cover of the punctured spectrum of A is, up to isomorphism, the restriction of a finite étale cover of Spec A.

Purity descends from the completion of A, which by hypothesis is the quotient of a regular local ring by an ideal generated by a regular sequence.

theorem hasPurity_of_isCompleteIntersectionRing
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (hA : LocalCompleteIntersection.IsCompleteIntersectionRing A)
    (hdim : 3 ≤ ringKrullDim A) :
    HasPurity A

Sources

LeanAlgebraicGeometry.LocalLefschetzSituation.hasPurity_quotientRing_of_dualizing · AlgebraicGeometry.LocalLefschetzSituation.hasPurity_quotientRing_of_isAdicComplete · AlgebraicGeometry.hasPurity_of_isCompleteIntersectionRing

Section58.26 Purity in local case, III #

Section 58.26 of the Stacks Project, Tag 0EY8. 4 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0EY9, a lemma

Tag 0EY9 in the Stacks Project.

Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_restrict_mvPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityPowerSeriesRestriction.lean, line 139. The attribute's comment: “the full statement under the source's hypotheses; nothing is assumed”.

Let (A, 𝔪) be a Noetherian local ring of depth at least two, let B = A[[x_1, …, x_d]] with d ≥ 1, set Y = Spec B and let Y_0 = V(x_1, …, x_d) be the closed fibre, the image of the closed immersion Spec A ⟶ Y induced by the constant coefficient. For any open V ⊆ Y with V ∩ Y_0 the punctured spectrum of A, the restriction functor FÉt_V ⟶ FÉt_{V ∩ Y_0} is fully faithful.

The condition on V is the hypothesis hV: the inverse image of V under the closed immersion Spec A ⟶ Y is the complement of the closed point of Spec A.

public theorem fullyFaithful_finiteEtaleBaseChange_restrict_mvPowerSeries (A : Type u)
    [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (d : ℕ) (hd : 0 < d)
    (hdepth : (2 : ℕ∞) ≤ Module.depth A (IsLocalRing.maximalIdeal A) A)
    (V : (Spec (.of (MvPowerSeries (Fin d) A))).Opens)
    (hV : (Spec.map (CommRingCat.ofHom
        (MvPowerSeries.constantCoeff : MvPowerSeries (Fin d) A →+* A)) ⁻¹ᵁ V :
      Set (Spec (.of A))) = {IsLocalRing.closedPoint A}ᶜ) :
    Nonempty (finiteEtaleBaseChange (Spec.map (CommRingCat.ofHom
      (MvPowerSeries.constantCoeff : MvPowerSeries (Fin d) A →+* A)) ∣_ V)).FullyFaithful

Tag 0EYA, a lemma

Tag 0EYA in the Stacks Project.

Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_and_hasPurity_mvPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityPowerSeries.lean, line 57. The attribute's comment: “the full statement under the tag's hypotheses: for every open V containing the primes 𝔮 with 𝔮 ∩ A ≠ 𝔪 and the prime 𝔪B, the restriction FÉt_Y ⟶ FÉt_V is an equivalence, and purity holds for B.”. References: SGA 1 XIII (4.7), “special case”.

[Stacks, Tag 0EYA] (Ramanujam--Samuel for finite étale covers). Let (A, 𝔪) be a Noetherian local ring of depth at least two and let B = A[[x_1, …, x_d]] with d ≥ 1. Let V ⊆ Y = Spec B be an open which contains every prime 𝔮 of B with 𝔮 ∩ A ≠ 𝔪 (hV₁) and contains the prime 𝔪B (hV₂). Then the restriction functor FÉt_Y ⟶ FÉt_V is an equivalence, and purity holds for B.

The equivalence is isEquivalence_finiteEtaleBaseChange_mvPowerSeries with its two hypotheses discharged: the density of V by dense_of_comap_ne_maximalIdeal_mem_of_flat, B being flat over A ([Stacks, Tag 059T]) and A of positive depth, and essential surjectivity by essSurj_finiteEtaleBaseChange_mvPowerSeries. Purity for B is the equivalence for the punctured spectrum of B, which satisfies both conditions on V (mem_puncturedSpectrum_of_comap_ne_maximalIdeal, mem_puncturedSpectrum_of_eq_map_maximalIdeal; the latter is where d ≥ 1 is used).

public theorem isEquivalence_finiteEtaleBaseChange_and_hasPurity_mvPowerSeries (A : Type u)
    [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (d : ℕ) (hd : 0 < d)
    (hdepth : (2 : ℕ∞) ≤ Module.depth A (maximalIdeal A) A)
    (V : (Spec (.of (MvPowerSeries (Fin d) A))).Opens)
    (hV₁ : ∀ q : PrimeSpectrum (MvPowerSeries (Fin d) A),
      q.asIdeal.comap (MvPowerSeries.C : A →+* MvPowerSeries (Fin d) A) ≠ maximalIdeal A →
        q ∈ V)
    (hV₂ : ∀ q : PrimeSpectrum (MvPowerSeries (Fin d) A),
      q.asIdeal = Ideal.map (MvPowerSeries.C : A →+* MvPowerSeries (Fin d) A)
        (maximalIdeal A) → q ∈ V) :
    (finiteEtaleBaseChange V.ι).IsEquivalence ∧ HasPurity (MvPowerSeries (Fin d) A)

Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_mvPowerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityPowerSeriesEquivalence.lean, line 249. The attribute's comment: “the fully faithful half unconditionally: a point of Spec B outside V lies over 𝔪 by the tag's condition (1), hence its local ring has depth at least two, by flatness of B over A (Tag 059T) fed to Tag 0337, which is the source's first paragraph; Tag 0BLR through isConnectedPuncturedStrictHenselization_of_two_le_depth turns that into the local hypothesis of Tag 0BQF, which gives full faithfulness. Two hypotheses are carried. hessSurj is the essential surjectivity half, that is the whole of the source's second paragraph, standing for Tag 0EY6 and Tag 0EY9 together with the step the source itself marks small detail omitted. hdense is the density of V in Spec B, which Tag 0BQF requires and which the source does not verify. The tag's condition (2) on V and its hypothesis d ≥ 1 are stated; they are used by the purity corollary hasPurity_mvPowerSeries below rather than by the equivalence itself.”.

[Stacks, Tag 0EYA] (Ramanujam--Samuel for finite étale covers). Let (A, 𝔪) be a Noetherian local ring of depth at least two and let B = A[[x_1, …, x_d]] with d ≥ 1. Let V ⊆ Y = Spec B be an open which contains every prime 𝔮 of B with 𝔮 ∩ A ≠ 𝔪 and contains the prime 𝔪B. Then the restriction functor FÉt_Y ⟶ FÉt_V is an equivalence.

The two conditions on V are hV₁ and hV₂. hV₂ is phrased as a condition on the points of Spec B rather than on the ideal 𝔪B, so that the primality of 𝔪B need not be produced.

The fully faithful half is proved: a point of Spec B outside V lies over 𝔪 by hV₁, so its local ring has depth at least two by two_le_depth_stalk_of_notMem_mvPowerSeries, which is flatness of B over A ([Stacks, Tag 059T]) fed to [Stacks, Tag 0337]; isConnectedPuncturedStrictHenselization_of_two_le_depth ([Stacks, Tag 0BLR]) turns that into the local hypothesis of [Stacks, Tag 0BQF], which concludes. That is the source's first paragraph.

Two hypotheses are carried.

hdense is the density of V in Spec B, which [Stacks, Tag 0BQF] requires and which the source does not verify when it appeals to that tag.

hessSurj is essential surjectivity, the source's second paragraph: the unique finite extension Spec C ⟶ Y of a finite étale W ⟶ V from [Stacks, Tag 0EY6], the isomorphism C ≅ C₀ ⊗_A B obtained from [Stacks, Tag 0EY9] over U ×_X Y through the compatibility of that construction with flat base change and with change of opens, and the deduction that A ⟶ C₀ is finite étale — a step at which the source itself writes "small detail omitted".

public theorem isEquivalence_finiteEtaleBaseChange_mvPowerSeries (A : Type u) [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] (d : ℕ) (hd : 0 < d)
    (hdepth : (2 : ℕ∞) ≤ Module.depth A (maximalIdeal A) A)
    (V : (Spec (.of (MvPowerSeries (Fin d) A))).Opens)
    (hV₁ : ∀ q : PrimeSpectrum (MvPowerSeries (Fin d) A),
      q.asIdeal.comap (MvPowerSeries.C : A →+* MvPowerSeries (Fin d) A) ≠ maximalIdeal A →
        q ∈ V)
    (hV₂ : ∀ q : PrimeSpectrum (MvPowerSeries (Fin d) A),
      q.asIdeal = Ideal.map (MvPowerSeries.C : A →+* MvPowerSeries (Fin d) A)
        (maximalIdeal A) → q ∈ V)
    (hdense : Dense (V : Set (Spec (.of (MvPowerSeries (Fin d) A)))))
    (hessSurj : (finiteEtaleBaseChange V.ι).EssSurj) :
    (finiteEtaleBaseChange V.ι).IsEquivalence

Tag 0EYB, a lemma

Tag 0EYB in the Stacks Project.

Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_of_smooth_of_fibrewise_dense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PuritySmooth.lean, line 97. The attribute's comment: “the full statement under the tag's four hypotheses and nothing else: (1) Smooth f, (2) IsNoetherian S, (3) hfib, the tag's X_s = U_s at every s with depth 𝒪_{S, s} ≤ 1, spelled as containment of the fibre f⁻¹(s) in U, and (4) hdense, the density of U_s in X_s, spelled as every point of f⁻¹(s) lying in the closure of U ∩ f⁻¹(s); the conclusion is that the restriction finiteEtaleBaseChange U.ι is an equivalence FÉt_X ⟶ FÉt_U.”.

[Stacks, Tag 0EYB]. Let f : X ⟶ S be a morphism of schemes and U ⊆ X an open subscheme. Assume that

f is smooth,

S is Noetherian,

for every s ∈ S with depth 𝒪_{S, s} ≤ 1 we have X_s = U_s, spelled as containment of the fibre f⁻¹(s) in U (hfib), and

U_s ⊆ X_s is dense for every s ∈ S, spelled as every point of f⁻¹(s) lying in the closure of U ∩ f⁻¹(s) (hdense).

Then the restriction functor FÉt_X ⟶ FÉt_U is an equivalence of categories.

Full faithfulness is nonempty_fullyFaithful_finiteEtaleBaseChange_of_smooth (the source's first paragraph, by [Stacks, Tag 0BQF], [Stacks, Tag 0BLR] and [Stacks, Tag 0337]) and essential surjectivity is essSurj_finiteEtaleBaseChange_of_smooth (the source's second paragraph, by [Stacks, Tag 0EY6] and [Stacks, Tag 0EYA]).

public theorem isEquivalence_finiteEtaleBaseChange_of_smooth_of_fibrewise_dense
    {X S : Scheme.{u}} (f : X ⟶ S) [Smooth f] [IsNoetherian S] (U : X.Opens)
    (hfib : ∀ s : S, Module.depth (S.presheaf.stalk s) (maximalIdeal (S.presheaf.stalk s))
      (S.presheaf.stalk s) ≤ 1 → f.base ⁻¹' {s} ⊆ (U : Set X))
    (hdense : ∀ s : S, f.base ⁻¹' {s} ⊆ closure ((U : Set X) ∩ f.base ⁻¹' {s})) :
    (finiteEtaleBaseChange U.ι).IsEquivalence

Tag 0EYC, a proposition

Tag 0EYC in the Stacks Project.

Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_of_formallySmoothNAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FormallySmoothEquivalence.lean, line 328. The attribute's comment: “the fully faithful half unconditionally: a point of Spec B outside V lies over 𝔪_A by the tag's condition (1), hence its local ring has depth at least two by flatness of B over A fed to Tag 0337, which is the source's first paragraph; Tag 0BLR through isConnectedPuncturedStrictHenselization_of_two_le_depth turns that into the local hypothesis of Tag 0BQF, and the density of V that Tag 0BQF also needs — and that the source does not verify — is proved here: such an open contains every minimal prime of B, since a minimal prime lying over 𝔪_A would give a zero-dimensional local ring of depth at least two, against Tag 00LK. Two hypotheses are carried. hflat is the flatness of A → B, which the source asserts in the first paragraph without justification and which follows from the formal smoothness hypothesis by Tag 07ED and Tag 07PM. hessSurj is the essential surjectivity half, that is the whole of the source's argument after the first paragraph: the reduction to the completions (Tags 07NV, 07NW, 07ED, 0BLL), Popescu's theorem (Tag 07GC), the descent along the resulting filtered colimit (Tags 01Z4, 01ZM, 01ZO, 07RP) and the appeal to Tag 0EYB. The formal smoothness hypothesis hsmooth and the tag's condition (2) on V are stated; they are consumed by the carried half and by the corollary at the punctured spectrum below rather than by the fully faithful half.”.

[Stacks, Tag 0EYC] (Ramanujam--Samuel for finite étale covers). Let A → B be a local homomorphism of Noetherian local rings with depth(A) ≥ 2, with A → B formally smooth for the 𝔪_B-adic topology, and with dim(B) > dim(A). Let V ⊆ Y = Spec B be an open which contains every prime 𝔮 of B with 𝔮 ∩ A ≠ 𝔪_A and contains the prime 𝔪_A B. Then the restriction functor FÉt_Y ⟶ FÉt_V is an equivalence.

The two conditions on V are hV₁ and hV₂. hV₂ is phrased as a condition on the points of Spec B rather than on the ideal 𝔪_A B, so that the primality of 𝔪_A B need not be produced.

The fully faithful half is proved: a point of Spec B outside V lies over 𝔪_A by hV₁, so its local ring has depth at least two by two_le_depth_stalk_of_notMem_of_flat, which is flatness fed to [Stacks, Tag 0337]; isConnectedPuncturedStrictHenselization_of_two_le_depth ([Stacks, Tag 0BLR]) turns that into the local hypothesis of [Stacks, Tag 0BQF], whose remaining hypothesis — the density of V, which the source does not verify — is dense_of_forall_comap_ne_maximalIdeal_mem. That is the source's first paragraph.

Two hypotheses are carried.

hflat is the flatness of A → B, asserted without justification in the source's first paragraph; it follows from hsmooth by [Stacks, Tag 07ED] and [Stacks, Tag 07PM].

hessSurj is essential surjectivity, the source's argument after the first paragraph: the reduction to the completions of A and B, Popescu's theorem writing B as a filtered colimit of smooth A-algebras, the descent of W ⟶ V to a finite étale cover of an open of one Spec B_i, and the appeal to [Stacks, Tag 0EYB].

public theorem isEquivalence_finiteEtaleBaseChange_of_formallySmoothNAdic (A B : Type u)
    [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A]
    [IsNoetherianRing B] [Algebra A B] [IsLocalHom (algebraMap A B)]
    (hdepth : (2 : ℕ∞) ≤ Module.depth A (maximalIdeal A) A)
    (hsmooth : RingHom.FormallySmoothNAdic.{u} (algebraMap A B) (maximalIdeal B))
    (hdim : ringKrullDim A < ringKrullDim B)
    (V : (Spec (.of B)).Opens)
    (hV₁ : ∀ q : PrimeSpectrum B, q.asIdeal.comap (algebraMap A B) ≠ maximalIdeal A → q ∈ V)
    (hV₂ : ∀ q : PrimeSpectrum B,
      q.asIdeal = Ideal.map (algebraMap A B) (maximalIdeal A) → q ∈ V)
    (hflat : Module.Flat A B)
    (hessSurj : (finiteEtaleBaseChange V.ι).EssSurj) :
    (finiteEtaleBaseChange V.ι).IsEquivalence

Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_of_formallySmoothNAdic_of_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FormallySmoothPurity.lean, line 190. The attribute's comment: “the equivalence FÉt_Y → FÉt_V, under the tag's hypotheses; nothing is assumed”. References: SGA 1 XIII (4.7), “special case”.

[Stacks, Tag 0EYC] (Ramanujam--Samuel for finite étale covers). Let A → B be a local homomorphism of Noetherian local rings. Assume A has depth at least two, A → B is formally smooth for the 𝔪_B-adic topology, and dim(B) > dim(A). For any open V ⊆ Y = Spec B which contains every prime 𝔮 ⊆ B with 𝔮 ∩ A ≠ 𝔪_A (hV₁) and the prime 𝔪_A B (hV₂, phrased as a condition on the points of Spec B), the restriction functor FÉt_Y ⟶ FÉt_V is an equivalence.

Full faithfulness is the source's first paragraph, isEquivalence_finiteEtaleBaseChange_of_formallySmoothNAdic; flatness of A → B is [Stacks, Tag 07NP]; essential surjectivity is essSurj_finiteEtaleBaseChange_of_formallySmoothNAdic. The hypothesis dim(B) > dim(A) is the source's own; it is what makes the punctured spectrum an open as in the tag (see hasPurity_of_formallySmoothNAdic) and is not needed for the equivalence itself.

public theorem isEquivalence_finiteEtaleBaseChange_of_formallySmoothNAdic_of_depth
    (A B : Type u) [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A]
    [IsNoetherianRing B] [Algebra A B] [IsLocalHom (algebraMap A B)]
    (hdepth : (2 : ℕ∞) ≤ Module.depth A (maximalIdeal A) A)
    (hsmooth : RingHom.FormallySmoothNAdic.{u} (algebraMap A B) (maximalIdeal B))
    (hdim : ringKrullDim A < ringKrullDim B)
    (V : (Spec (.of B)).Opens)
    (hV₁ : ∀ q : PrimeSpectrum B, q.asIdeal.comap (algebraMap A B) ≠ maximalIdeal A → q ∈ V)
    (hV₂ : ∀ q : PrimeSpectrum B,
      q.asIdeal = Ideal.map (algebraMap A B) (maximalIdeal A) → q ∈ V) :
    (finiteEtaleBaseChange V.ι).IsEquivalence

Stacks.FundamentalGroup.hasPurity_of_formallySmoothNAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityLocalCase/FormallySmoothPurity.lean, line 214. The attribute's comment: “purity holds for B, under the tag's hypotheses; nothing is assumed”.

[Stacks, Tag 0EYC], "in particular purity holds for B". Let A → B be a local homomorphism of Noetherian local rings with depth(A) ≥ 2, formally smooth for the 𝔪_B-adic topology, with dim(B) > dim(A). Then every finite étale cover of the punctured spectrum of B extends to a finite étale cover of Spec B.

The punctured spectrum is an open as in the tag: condition (1) because the closed point contracts to 𝔪_A, condition (2) because 𝔪_A B ≠ 𝔪_B, which is where dim(A) < dim(B) enters (mem_puncturedSpectrum_of_eq_map_maximalIdeal_of_ringKrullDim_lt).

public theorem hasPurity_of_formallySmoothNAdic (A B : Type u) [CommRing A] [CommRing B]
    [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A] [IsNoetherianRing B] [Algebra A B]
    [IsLocalHom (algebraMap A B)]
    (hdepth : (2 : ℕ∞) ≤ Module.depth A (maximalIdeal A) A)
    (hsmooth : RingHom.FormallySmoothNAdic.{u} (algebraMap A B) (maximalIdeal B))
    (hdim : ringKrullDim A < ringKrullDim B) :
    HasPurity B

Sources

LeanStacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_restrict_mvPowerSeries · Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_and_hasPurity_mvPowerSeries · Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_mvPowerSeries · Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_of_smooth_of_fibrewise_dense · Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_of_formallySmoothNAdic · Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_of_formallySmoothNAdic_of_depth · Stacks.FundamentalGroup.hasPurity_of_formallySmoothNAdic

Section58.27 Lefschetz for the fundamental group #

Section 58.27 of the Stacks Project, Tag 0ELB. 3 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0ELC, a proposition

Tag 0ELC in the Stacks Project.

Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_zeroScheme_of_depthAddDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/LefschetzZeroSchemePurity.lean, line 253. The attribute's comment: “first statement: restriction FÉt_X → FÉt_Y to the zero scheme of a section of an ample invertible module is fully faithful. Nothing is carried: Stacks 0EL1 is isIso_zeroSchemeComparison_of_isProper, and the passage from it to full faithfulness is the formalized Stacks 0EKP chain followed by Stacks 0EL8”. References: SGA 1 X (2.13), “partial”.

[Stacks, Tag 0ELC], first statement. Let k be a field, X a proper scheme over k, L an ample invertible 𝒪_X-module, s ∈ Γ(X, L) and Y = Z(s) the zero scheme of s. If depth(𝒪_{X, x}) + dim({x}‾) > 1 at every point x of X outside Y, then the restriction functor FÉt_X ⟶ FÉt_Y is fully faithful.

The statement is that of Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_zeroScheme_of_isProper, and nothing is carried here: the source's appeal to Algebraic and Formal Geometry, Proposition [Stacks, Tag 0EL1] is Stacks.Algebraization.isIso_zeroSchemeComparison_of_isProper, and the route from there to full faithfulness runs through conditions (2) and (4) of [Stacks, Tag 0EKP] rather than through [Stacks, Tag 0EJZ]; see the module documentation for the chain. This is the full faithfulness that the source uses in [Stacks, Tag 0ELE].

CategoryTheory.Functor.FullyFaithful carries the inverse map on hom sets as data, so full faithfulness is recorded as Nonempty _.FullyFaithful. X is Noetherian by Stacks.FundamentalGroup.isNoetherian_of_isProper_of_isAmple.

public theorem fullyFaithful_finiteEtaleBaseChange_zeroScheme_of_depthAddDim
    (hdepth : DepthAddDimGtOneOutsideSupport X (zeroScheme X L s)) :
    Nonempty (finiteEtaleBaseChange (zeroScheme X L s).subschemeι).FullyFaithful

Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_zeroScheme_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/LefschetzZeroSchemeRestrictionFromDepth.lean, line 78. The attribute's comment: “first statement: restriction FÉt_X → FÉt_Y to the zero scheme of a section of an ample invertible module on a proper scheme over a field is fully faithful when depth + dim > 1 off the zero scheme”. References: SGA 1 X (2.13), “partial”.

[Stacks, Tag 0ELC], first statement. Let k be a field, X a proper scheme over k, L an ample invertible 𝒪_X-module, s ∈ Γ(X, L) and Y = Z(s) the zero scheme of s. If depth(𝒪_{X, x}) + dim({x}‾) > 1 at every point x of X ∖ Y, then the restriction functor FÉt_X ⟶ FÉt_Y is fully faithful.

CategoryTheory.Functor.FullyFaithful carries the inverse map on hom sets as data, so full faithfulness is stated as Nonempty _.FullyFaithful.

public theorem fullyFaithful_finiteEtaleBaseChange_zeroScheme_of_isProper
    (k : Type u) [Field k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsProper g]
    (L : X.Modules) [Stacks.Ample.IsInvertibleModule X L]
    (hL : AlgebraicGeometry.Scheme.Modules.IsAmple X L) (s : Γ(L, ⊤))
    (hdepth : DepthAddDimGtOneOutsideSupport X (zeroScheme X L s)) :
    Nonempty (finiteEtaleBaseChange (zeroScheme X L s).subschemeι).FullyFaithful

Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_neighborhood_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/LefschetzZeroSchemeRestrictionFromDepth.lean, line 99. The attribute's comment: “second statement: restriction FÉt_V → FÉt_Y is fully faithful for every open V of X containing the zero scheme”. References: SGA 1 X (2.13), “partial”; SGA 2 XII (3.5), “more general”.

[Stacks, Tag 0ELC], second statement. In the situation of Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_zeroScheme_of_isProper, the restriction functor FÉt_V ⟶ FÉt_Y is fully faithful for every open subscheme V ⊆ X containing Y.

The open subschemes containing Y are Stacks.FundamentalGroup.Neighborhood X Y, and the closed immersion Y ⟶ V is Stacks.FundamentalGroup.Neighborhood.toSchemeHom.

public theorem fullyFaithful_finiteEtaleBaseChange_neighborhood_of_isProper
    (k : Type u) [Field k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsProper g]
    (L : X.Modules) [Stacks.Ample.IsInvertibleModule X L]
    (hL : AlgebraicGeometry.Scheme.Modules.IsAmple X L) (s : Γ(L, ⊤))
    (hdepth : DepthAddDimGtOneOutsideSupport X (zeroScheme X L s))
    (W : Neighborhood X (zeroScheme X L s)) :
    Nonempty (finiteEtaleBaseChange
      (Neighborhood.toSchemeHom X (zeroScheme X L s) W)).FullyFaithful

Tag 0ELD, a proposition

Tag 0ELD in the Stacks Project.

Stacks.FundamentalGroup.finiteEtaleColimitEquivalence_zeroScheme_of_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/LefschetzZeroSchemeFiniteEtaleEquivalence.lean, line 100. The attribute's comment: “the restriction functor colim_V FÉt_V → FÉt_Y is an equivalence, stated as its fully faithful half and its essentially surjective half, at exactly the source's hypotheses”.

Stacks Project, Tag 0ELD. Let k be a field, X a proper scheme over k, L an ample invertible 𝒪_X-module, s ∈ Γ(X, L), Y = Z(s) the zero scheme of s, and 𝒱 the open subschemes of X containing Y, ordered by reverse inclusion. If depth(𝒪_{X, x}) + dim({x}‾) > 2 for every x ∈ X ∖ Y, then the restriction functor colim_𝒱 FÉt_V ⟶ FÉt_Y is an equivalence.

The equivalence colim_𝒱 FÉt_V ≃ FÉt_Y is stated as its two halves: the restriction functor is fully faithful (FiniteEtaleColimitFullyFaithful X Y: morphisms of restrictions to Y come from morphisms over a smaller neighbourhood, and morphisms with equal restrictions to Y agree over a smaller neighbourhood), and essentially surjective (every finite étale cover of Y is the restriction of a finite étale cover of some open neighbourhood of Y).

public theorem finiteEtaleColimitEquivalence_zeroScheme_of_depth
    (k : Type u) [Field k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsProper g]
    (L : X.Modules) [Stacks.Ample.IsInvertibleModule X L]
    (hL : AlgebraicGeometry.Scheme.Modules.IsAmple X L) (s : Γ(L, ⊤))
    (hdepth : DepthAddDimGtTwoOutsideSupport X (zeroScheme X L s)) :
    FiniteEtaleColimitFullyFaithful X (zeroScheme X L s) ∧
      ∀ A : FiniteEtaleOver (zeroScheme X L s).subscheme,
        ∃ (W : Neighborhood X (zeroScheme X L s))
          (U : FiniteEtaleOver (Neighborhood.open X (zeroScheme X L s) W).toScheme),
          Nonempty ((finiteEtaleBaseChange
            (Neighborhood.toSchemeHom X (zeroScheme X L s) W)).obj U ≅ A)

Tag 0ELE, a proposition

Tag 0ELE in the Stacks Project.

Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_zeroScheme_of_hasPurity_of_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/LefschetzZeroSchemePurity.lean, line 452. The attribute's comment: “first conclusion: restriction FÉt_X → FÉt_Y to the zero scheme of a section of an ample invertible module is an equivalence”. References: SGA 1 X (2.13), “more general”; SGA 2 XII (3.5), “special case”.

[Stacks, Tag 0ELE], the first conclusion. Let k be a field, X a proper scheme over k, L an ample invertible 𝒪_X-module, s ∈ Γ(X, L) and Y = Z(s) the zero scheme of s. Assume that depth(𝒪_{X, x}) + dim({x}‾) > 2 for every x ∈ X ∖ Y, and that purity holds for 𝒪_{X, x} at every closed x ∈ X ∖ Y. Then the restriction functor FÉt_X ⟶ FÉt_Y is an equivalence.

The proof is the source's. Full faithfulness is Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_zeroScheme_of_depthAddDim ([Stacks, Tag 0ELC]), whose bound > 1 follows from the bound > 2 assumed here. For essential surjectivity, [Stacks, Tag 0ELD] writes a given finite étale cover of Y as the restriction of a finite étale cover of an open neighbourhood V of Y; every point of X ∖ V is a closed point off Y, because its closure misses Y and so lies in the affine open where s does not vanish, and purity therefore holds there, so [Stacks, Tag 0EY7] extends the cover from V to all of X.

The depth hypothesis is Stacks.FundamentalGroup.DepthAddDimGtTwoOutsideSupport, which unfolds to the displayed inequality in the extended integers.

public theorem isEquivalence_finiteEtaleBaseChange_zeroScheme_of_hasPurity_of_depth
    (hdepth : DepthAddDimGtTwoOutsideSupport X (zeroScheme X L s))
    (hpurity : ∀ x : X, x ∉ ((zeroScheme X L s).support : Set X) → IsClosed ({x} : Set X) →
      AlgebraicGeometry.HasPurity (X.presheaf.stalk x)) :
    (finiteEtaleBaseChange (zeroScheme X L s).subschemeι).IsEquivalence

Stacks.FundamentalGroup.connectedSpace_zeroScheme_iff_of_hasPurity_of_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/LefschetzZeroSchemePurity.lean, line 467. The attribute's comment: “the "or equivalently": X is connected if and only if its zero scheme Y = Z(s) is”.

[Stacks, Tag 0ELE], the "or equivalently". In the situation of Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_zeroScheme_of_hasPurity_of_depth the zero scheme Y = Z(s) is connected exactly when X is. This is [Stacks, Tag 0BQA] part (2) applied to the equivalence FÉt_X ⟶ FÉt_Y.

public theorem connectedSpace_zeroScheme_iff_of_hasPurity_of_depth
    (hdepth : DepthAddDimGtTwoOutsideSupport X (zeroScheme X L s))
    (hpurity : ∀ x : X, x ∉ ((zeroScheme X L s).support : Set X) → IsClosed ({x} : Set X) →
      AlgebraicGeometry.HasPurity (X.presheaf.stalk x)) :
    ConnectedSpace (zeroScheme X L s).subscheme ↔ ConnectedSpace X

Stacks.FundamentalGroup.fundamentalGroupEquiv_zeroScheme_of_hasPurity_of_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/LefschetzZeroSchemePurity.lean, line 488. The attribute's comment: “second conclusion: for X, equivalently Y, connected, the induced map π₁(Y, y‾) → π₁(X, y‾) is an isomorphism of topological groups at every geometric point of Y”. References: SGA 1 X (2.13), “more general”; SGA 2 X (3.10), “special case”; SGA 2 XII (4.9), “4.9 a), special case”.

[Stacks, Tag 0ELE], the second conclusion. In the situation of Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_zeroScheme_of_hasPurity_of_depth, with X and Y = Z(s) connected, the map π₁(Y, y‾) ⟶ π₁(X, y‾) induced by the closed immersion is an isomorphism of topological groups for every geometric point y‾ of Y. The isomorphism produced is the canonical induced map AlgebraicGeometry.etaleFundamentalGroupMap. This is [Stacks, Tag 0BQA] part (2), the lemma the source's proof quotes for the π₁ statement.

public theorem fundamentalGroupEquiv_zeroScheme_of_hasPurity_of_depth
    (hdepth : DepthAddDimGtTwoOutsideSupport X (zeroScheme X L s))
    (hpurity : ∀ x : X, x ∉ ((zeroScheme X L s).support : Set X) → IsClosed ({x} : Set X) →
      AlgebraicGeometry.HasPurity (X.presheaf.stalk x))
    [ConnectedSpace (zeroScheme X L s).subscheme] [ConnectedSpace X]
    (y : AlgebraicGeometry.GeometricPoint (zeroScheme X L s).subscheme) :
    ∃ e : AlgebraicGeometry.EtaleFundamentalGroup (zeroScheme X L s).subscheme y ≃ₜ*
        AlgebraicGeometry.EtaleFundamentalGroup X (y.map (zeroScheme X L s).subschemeι),
      ∀ σ : AlgebraicGeometry.EtaleFundamentalGroup (zeroScheme X L s).subscheme y,
        e σ = AlgebraicGeometry.etaleFundamentalGroupMap
          (zeroScheme X L s).subschemeι y σ

Sources

LeanStacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_zeroScheme_of_depthAddDim · Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_zeroScheme_of_isProper · Stacks.FundamentalGroup.fullyFaithful_finiteEtaleBaseChange_neighborhood_of_isProper · Stacks.FundamentalGroup.finiteEtaleColimitEquivalence_zeroScheme_of_depth · Stacks.FundamentalGroup.isEquivalence_finiteEtaleBaseChange_zeroScheme_of_hasPurity_of_depth · Stacks.FundamentalGroup.connectedSpace_zeroScheme_iff_of_hasPurity_of_depth · Stacks.FundamentalGroup.fundamentalGroupEquiv_zeroScheme_of_hasPurity_of_depth

Section58.28 Purity of ramification locus #

Section 58.28 of the Stacks Project, Tag 0EA1. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0EA2, a lemma

Tag 0EA2 in the Stacks Project.

AlgebraicGeometry.DualizingDivisor.eq_top_of_isMinimalResolution_of_relativeDualizingModule_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/DualizingDivisor/MinimalResolution.lean, line 68. The attribute's comment: “second sentence: if f is a minimal resolution, then E = 0”.

[Stacks, Tag 0EA2], second sentence. Let A be a Noetherian normal local domain of dimension two which is Nagata and has a dualizing module ω_A, and let f : X ⟶ Spec(A) be a minimal resolution of singularities. Let ω_X = H^{-2}(f^×(ω_A[2])) be as in [Stacks, Remark 0B4R] (Stacks.Duality.relativeDualizingModule at ω_A[2]^~, as in the first sentence, definesRationalSingularity_of_relativeDualizingModule_iso). If ω_X ≅ 𝒪_X(E) for an effective Cartier divisor E ⊆ X supported on the exceptional fibre, then E = 0, i.e. the ideal sheaf of E is the unit ideal ⊤. The hypotheses are those of the first sentence with IsMinimalResolution f in place of IsResolution f; properness of f and quasi-compactness and quasi-separatedness of X, needed to form f^×, are derived from it inside the statement.

theorem eq_top_of_isMinimalResolution_of_relativeDualizingModule_iso (A : Type u) [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] [IsNormalDomain A] (hdim : ringKrullDim A = 2)
    (hNagata : IsNagataRing A) (ωA : ModuleCat.{u} A)
    (hω : Stacks.Duality.IsDualizingRingModule A ωA)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) (hf : IsMinimalResolution f)
    (E : X.IdealSheafData) [Stacks.Divisors.IsEffectiveCartierDivisor E]
    (hE : ∀ x : X, x ∈ E.support → f x = closedPoint A)
    (e : haveI : IsProper f := hf.1.1.isProper
      haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
      haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
      Nonempty (relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        ((derivedTilde (CommRingCat.of A)).obj ((singleFunctor (ModuleCat.{u} A) (-2)).obj ωA)) ≅
          (Stacks.Divisors.invertibleSheaf' E : X.Modules))) :
    E = ⊤

AlgebraicGeometry.DualizingDivisor.definesRationalSingularity_of_relativeDualizingModule_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/DualizingDivisor/RationalSingularity.lean, line 380. The attribute's comment: “first sentence: if ω_X ≅ O_X(E) for an effective Cartier divisor E supported on the exceptional fibre of a resolution, then A defines a rational singularity”.

[Stacks, Tag 0EA2], first sentence. Let A be a Noetherian normal local domain of dimension two which is Nagata, has a dualizing module ω_A, and has a resolution of singularities f : X ⟶ Spec(A). Let ω_X be as in [Stacks, Tag 0B4R]: the dualizing module of X normalized with respect to ω_A, that is ω_X = H^{-2}(f^×(ω_A[2])) with f^× the twisted inverse image (Stacks.Duality.relativeDualizingModule at ω_A[2]^~, whose degree -dim X is -2). If ω_X ≅ 𝒪_X(E) for an effective Cartier divisor E ⊆ X supported on the exceptional fibre (every point of E lies over the closed point), then A defines a rational singularity.

Following the source, duality turns the map 𝒪_X ⟶ 𝒪_X(E) = ω_X into a generator of Hom(RΓ(X, 𝒪_X[2]), ω_A[2]) (hom_derivedSectionsUnitShift_free); the criterion Stacks.PurityRamification.subsingleton_homology_succ_of_forall_eq_smul (depth of ω_A, [Stacks, Tag 0AXC], torsion of H¹(X, 𝒪_X)) gives H¹(X, 𝒪_X) = 0, and a resolution with H¹(X, 𝒪_X) = 0 makes A a rational singularity (definesRationalSingularity_of_isResolution_of_isZero_structureSheafH1). Forming f^×, hence ω_X, uses that f is proper and X quasi-compact and quasi-separated; inside the statement these are derived from IsResolution f (a resolution is proper over the affine scheme Spec(A)) by haveI, not assumed.

theorem definesRationalSingularity_of_relativeDualizingModule_iso (A : Type u) [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] [IsNormalDomain A] (hdim : ringKrullDim A = 2)
    (hNagata : IsNagataRing A) (ωA : ModuleCat.{u} A)
    (hω : Stacks.Duality.IsDualizingRingModule A ωA)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) (hf : IsResolution f)
    (E : X.IdealSheafData) [Stacks.Divisors.IsEffectiveCartierDivisor E]
    (hE : ∀ x : X, x ∈ E.support → f x = closedPoint A)
    (e : haveI : IsProper f := hf.1.isProper
      haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
      haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
      Nonempty (relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        ((derivedTilde (CommRingCat.of A)).obj ((singleFunctor (ModuleCat.{u} A) (-2)).obj ωA)) ≅
          (Stacks.Divisors.invertibleSheaf' E : X.Modules))) :
    DefinesRationalSingularity A

Tag 0EA3, a lemma

Tag 0EA3 in the Stacks Project.

AlgebraicGeometry.etaleAt_of_etaleAt_outside_closure_of_ringKrullDim_eq_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityRamification/EtaleAtDimensionTwo.lean, line 52.

Stacks Project, Tag 0EA3. Let f : X ⟶ Spec A be a morphism (locally) of finite type and x ∈ X. Assume A is an excellent regular local ring, 𝒪_{X, x} is normal of dimension 2, and f is étale at every point outside closure {x}. Then f is étale at x.

theorem etaleAt_of_etaleAt_outside_closure_of_ringKrullDim_eq_two {A : Type u} [CommRing A]
    [IsRegularLocalRing A] (hA : IsExcellent A) {X : Scheme.{u}} (f : X ⟶ Spec (.of A))
    [LocallyOfFiniteType f] (x : X) (hX : IsNormalRing (X.presheaf.stalk x))
    (hdim : ringKrullDim (X.presheaf.stalk x) = 2)
    (het : ∀ z : X, z ∉ closure ({x} : Set X) → EtaleAt f z) : EtaleAt f x

Tag 0EA4, a lemma

Tag 0EA4 in the Stacks Project.

AlgebraicGeometry.etaleAt_of_etaleAt_codimensionOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityRamificationLocus/Induction.lean, line 378. The attribute's comment: “the whole lemma: hypotheses (1) 𝒪_{X,x} normal of dimension ≥ 1, (2) 𝒪_{Y,f x} regular, (3) f locally of finite type, (4) f étale at every x' ⤳ x with dim 𝒪_{X,x'} = 1; the conclusion is EtaleAt f x.”. References: EGA IV (21.12.14), “more general”; SGA 1 X (3.1), “more general”.

[Stacks, Tag 0EA4], purity of the ramification locus. Let f : X ⟶ Y be a morphism of locally Noetherian schemes, let x : X and y = f x, and assume that (1) 𝒪_{X,x} is normal of dimension at least one, (2) 𝒪_{Y,y} is regular, (3) f is locally of finite type, and (4) f is étale at every specialization x' ⤳ x with dim 𝒪_{X,x'} = 1. Then f is étale at x.

The hypotheses are exactly the tag's own. "Normal" is IsNormalRing of the stalk (for a local ring: a normal domain), "dimension" is ringKrullDim, and a specialization x' ⤳ x of the source is Mathlib's x' ⤳ x, that is x ∈ closure {x'}.

The proof is the source's: the proper generizations of x are handled by induction on dim 𝒪_{X,x}, base change to Spec 𝒪_{Y,f x} ([Stacks, Tag 0476]) and then to the spectrum of its completion changes neither étaleness at the relevant point (both being flat) nor normality of the local ring there (Serre's criterion), and over the complete — hence excellent — regular local base the induction of AlgebraicGeometry.etaleAt_of_etaleAt_codimensionOne_over_excellent applies, with [Stacks, Tag 0EA3] in dimension two and [Stacks, Tag 0BMB] above it.

theorem etaleAt_of_etaleAt_codimensionOne
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [LocallyOfFiniteType f] (x : X)
    (hX : IsNormalRing (X.presheaf.stalk x))
    (hY : IsRegularLocalRing (Y.presheaf.stalk (f x)))
    (hpositive : 1 ≤ ringKrullDim (X.presheaf.stalk x))
    (hetale : ∀ x' : X, x' ⤳ x → ringKrullDim (X.presheaf.stalk x') = 1 → EtaleAt f x') :
    EtaleAt f x

Sources

LeanAlgebraicGeometry.DualizingDivisor.eq_top_of_isMinimalResolution_of_relativeDualizingModule_iso · AlgebraicGeometry.DualizingDivisor.definesRationalSingularity_of_relativeDualizingModule_iso · AlgebraicGeometry.etaleAt_of_etaleAt_outside_closure_of_ringKrullDim_eq_two · AlgebraicGeometry.etaleAt_of_etaleAt_codimensionOne

Section58.29 Affineness of complement of ramification locus #

Section 58.29 of the Stacks Project, Tag 0ECA. 3 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0ECB, a lemma

Tag 0ECB in the Stacks Project.

Stacks.EtalePuncturedSpectrum.exists_directSum_injectiveHull_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PuncturedSpectrumCohomology.lean, line 641.

Stacks Project, Tag 0ECB. Let A be a regular local ring containing a field k, let f : V ⟶ Spec A be étale and quasi-compact, and suppose f factors as g ≫ U.ι through the punctured spectrum U = Spec A ∖ V(𝔪) with g affine. Then for every i > 0 the A-module H ⁱ(V, 𝒪_V) is a direct sum of copies of an injective hull E of the residue field of A.

The index set and the isomorphism are not determined by the statement.

theorem exists_directSum_injectiveHull_residueField
    (A k E : Type u) [CommRing A] [IsRegularLocalRing A] [Field k] [Algebra k A]
    [AddCommGroup E] [Module A E]
    {V : Scheme.{u}} (f : V ⟶ Spec (.of A)) [Etale f] [QuasiCompact f]
    (g : V ⟶ (complementZeroLocus A (IsLocalRing.maximalIdeal A) : Scheme)) [IsAffineHom g]
    (hg : g ≫ (complementZeroLocus A (IsLocalRing.maximalIdeal A)).ι = f)
    (i : ModuleCat.of A (IsLocalRing.ResidueField A) ⟶ ModuleCat.of A E) [Mono i]
    (hi : Module.IsInjectiveHull i) (n : ℕ) (hn : 0 < n) :
    ∃ J : Type u, Nonempty (structureSheafCohomology f n ≃ₗ[A] DirectSum J (fun _ => E))

Tag 0ECC, a lemma

Tag 0ECC in the Stacks Project.

Stacks.SpectralSequence.isZero_derivedTensorHomology_zero_singleHomology_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/OriginVanishing.lean, line 188. The attribute's comment: “the cohomological step: the tensor spectral sequence at the origin”.

Let K and L be bounded-above objects of the derived category of A-modules. Suppose

H⁰(K ⊗^L L) = 0;

H^q(K) = 0 for q < 0;

H^{-r}(H^{r-1}(K)[0] ⊗^L L) = 0 for every r ≥ 2.

Then H⁰(H⁰(K)[0] ⊗^L L) = 0.

theorem isZero_derivedTensorHomology_zero_singleHomology_zero
    (K L : DerivedCategory.Minus (ModuleCat.{u} A))
    (habut : IsZero (derivedTensorHomology A K.1 L.1 0))
    (hneg : ∀ q : ℤ, q < 0 →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) q).obj K.1))
    (hTor : ∀ r : ℤ, 2 ≤ r →
      IsZero (derivedTensorHomology A (singleHomology A K.1 (r - 1)) L.1 (-r))) :
    IsZero (derivedTensorHomology A (singleHomology A K.1 0) L.1 0)

Stacks.PuncturedSpectrum.isAffine_of_cohomologyOverBase_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/AffineOfCohomologyVanishing.lean, line 196. The attribute's comment: “the proof assembled under the source's own hypotheses: the cohomology vanishing above dim(A) - 1 is the hypothesis of the tag, and both cited inputs are proved — the abutment H⁰(RΓ(V,𝒪_V) ⊗^L_A A/𝔪) = 0 by computing the derived tensor product on an injective resolution against the Koszul complex of a generating family of the maximal ideal, which is acyclic because the standard opens of the generators cover V, and the Tor vanishing from Tags 0ECB and 0EBT”.

[Stacks, Tag 0ECC], the proof assembled, with the source's own degree bound. In the situation of [Stacks, Tag 0ECB], write d for the Krull dimension of A. If H ⁿ(V, 𝒪_V) = 0 for every n ≥ d - 1, then V is affine.

Both inputs the source cites are discharged: the abutment H⁰(RΓ(V, 𝒪_V) ⊗^L_A A/𝔪) = 0 by Stacks.PuncturedSpectrum.isZero_derivedTensor_derivedSectionsOverBase_residueField, and the vanishing of Tor_r^A(H^{r-1}(V, 𝒪_V), A/𝔪) for 2 ≤ r < d by Stacks.PuncturedSpectrum.isZero_derivedTensorHomology_cohomologyOverBase_residueField. See the module documentation.

theorem isAffine_of_cohomologyOverBase_vanishing (A k : Type u) [CommRing A]
    [IsRegularLocalRing A] [Field k] [Algebra k A] {V : Scheme.{u}}
    (f : V ⟶ Spec (CommRingCat.of A)) [Etale f] [QuasiCompact f]
    (g : V ⟶ (Stacks.LocalCohomology.puncturedSpectrum (CommRingCat.of A) : Scheme))
    [IsAffineHom g]
    (hg : g ≫ (Stacks.LocalCohomology.puncturedSpectrum (CommRingCat.of A)).ι = f)
    (hvanish : ∀ n : ℕ, ((ringKrullDim A).unbotD 0).toNat - 1 ≤ n →
      IsZero (cohomologyOverBase A f (SheafOfModules.unit V.ringCatSheaf) n)) :
    IsAffine V

Stacks.PuncturedSpectrum.isAffine_of_subsingleton_quotTensor_globalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/AffineOverPuncturedSpectrum.lean, line 272. The attribute's comment: “the final step: affineness once the residue field kills the global sections”.

[Stacks, Tag 0ECC], the final step of the proof. In the situation of [Stacks, Tag 0ECB] — A a regular local ring containing a field k, f : V ⟶ Spec A étale and quasi-compact, and the structure morphism factored through the punctured spectrum Spec A \ {𝔪} by an affine morphism g — if H⁰(V, 𝒪_V) ⊗_A A/𝔪 = 0, then V is affine.

This is the last paragraph of the source's proof: the vanishing of the residue tensor product says that a system of generators of 𝔪 maps to a system of generators of the unit ideal of Γ(V, 𝒪_V), so the affine opens V_{x_i} cover V.

What the source derives this vanishing from — the hypothesis H^i(V, 𝒪_V) = 0 for i ≥ dim(A) - 1, Tag 0ECB, Tag 0EBT and cohomology and base change — is not formalized here; see the module documentation.

The hypotheses of Tag 0ECB that this step does not use are nevertheless imposed, so that the statement is literally in the situation of that lemma. The ambient algebra structure on Γ(V, 𝒪_V) is required to be the one induced by f.

theorem isAffine_of_subsingleton_quotTensor_globalSections
    (A _k : Type u) [CommRing A] [IsRegularLocalRing A] [Field _k] [Algebra _k A]
    {V : Scheme.{u}} (f : V ⟶ Spec (CommRingCat.of A)) [Etale f] [QuasiCompact f]
    (g : V ⟶ (LocalCohomology.puncturedSpectrum (CommRingCat.of A) : Scheme)) [IsAffineHom g]
    (hg : g ≫ (LocalCohomology.puncturedSpectrum (CommRingCat.of A)).ι = f)
    [Algebra A Γ(V, ⊤)] (halg : algebraMap A Γ(V, ⊤) = baseHom f)
    (hzero : Subsingleton ((A ⧸ IsLocalRing.maximalIdeal A) ⊗[A] Γ(V, ⊤))) :
    IsAffine V

Stacks.PuncturedSpectrum.isZero_derivedTensorHomology_cohomologyOverBase_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/PuncturedSpectrumResidueFieldTor.lean, line 116. The attribute's comment: “the incoming terms of the tensor spectral sequence: Tor_r(H ⁿ(V,𝒪_V), A/𝔪) = 0 for n > 0 and r ≠ dim A, from Tags 0ECB and 0EBT”.

The incoming terms of the tensor spectral sequence of [Stacks, Tag 0ECC]. In the situation of [Stacks, Tag 0ECB] — A a regular local ring containing a field k, f : V ⟶ Spec A étale and quasi-compact, and the structure morphism factored through the punctured spectrum by an affine morphism g — write d for the Krull dimension of A. Then for every n > 0 and every r ≠ d, Tor_r^A(H ⁿ(V, 𝒪_V), A ⧸ 𝔪) = 0, in the derived form H ^{-r}(H ⁿ(V, 𝒪_V)[0] ⊗ᴸ_A (A ⧸ 𝔪)[0]) = 0.

By [Stacks, Tag 0ECB] the cohomology is a direct sum of copies of an injective hull of the residue field, by [Stacks, Tag 0EBT] each copy contributes nothing away from the dimension, and the derived tensor product commutes with the direct sum.

theorem isZero_derivedTensorHomology_cohomologyOverBase_residueField (A k : Type u) [CommRing A]
    [IsRegularLocalRing A] [Field k] [Algebra k A] {V : Scheme.{u}}
    (f : V ⟶ Spec (CommRingCat.of A)) [Etale f] [QuasiCompact f]
    (g : V ⟶ (LocalCohomology.puncturedSpectrum (CommRingCat.of A) : Scheme)) [IsAffineHom g]
    (hg : g ≫ (LocalCohomology.puncturedSpectrum (CommRingCat.of A)).ι = f)
    (d : ℕ) (hdim : ringKrullDim A = (d : WithBot ℕ∞)) (n : ℕ) (hn : 0 < n) (r : ℤ)
    (hr : r ≠ (d : ℤ)) :
    IsZero (derivedTensorHomology A
      ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
        (cohomologyOverBase A f (SheafOfModules.unit V.ringCatSheaf) n))
      ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
        (ModuleCat.of A (A ⧸ IsLocalRing.maximalIdeal A))) (-r))

Stacks.LocalCohomology.derivedSectionsMinus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/HigherDegree/DerivedSectionsOverBase.lean, line 219. The attribute's comment: “the complex RΓ(V, 𝒪_V) of A-modules, bounded above and concentrated in degrees ≥ 0”.

RΓ(V, F) as an object of the bounded above derived category D⁻(A), given a bound above which the cohomology of F on V vanishes.

Together with Stacks.LocalCohomology.nonempty_homology_derivedSectionsOverBase_iso and Stacks.LocalCohomology.isGE_derivedSectionsOverBase this is the complex RΓ(V, 𝒪_V) the proof of [Stacks, Tag 0ECC] feeds to its spectral sequence: an object of D⁻(A) with no cohomology in negative degrees whose cohomology in degree p is H^p(V, 𝒪_V).

The attribute is qualified: this is the construction of that complex, not the whole tag. The remaining steps need Tags 08IB, 0ECB and 0EBT, none of which the library carries; see the module documentation.

def derivedSectionsMinus (f : V ⟶ Spec (.of A))
    (F : SheafOfModules.{u} V.ringCatSheaf) (a : ℤ)
    (hvanish : ∀ n : ℕ, a < (n : ℤ) → IsZero (cohomologyOverBase.{u, u} A f F n)) :
    DerivedCategory.Minus (ModuleCat.{u} A)

Tag 0ECD, a theorem

Tag 0ECD in the Stacks Project.

AlgebraicGeometry.MaximalEtaleOpen.isAffineHom_maximalEtaleOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/AffineMaximalEtaleOpen.lean, line 1451. References: EGA IV (21.12.14), “special case”.

Stacks Project, Tag 0ECD. Let Y be an excellent regular scheme over a field k, let f : X ⟶ Y be a morphism of finite type with X normal, and let V ⊆ X be the maximal open subscheme on which f is étale. Then the inclusion V ⟶ X is affine.

Y regular is AlgebraicGeometry.IsRegular ([Stacks, Tag 02IS]); Y excellent is the existence around every point of an affine open neighbourhood whose ring of sections is excellent, which is the definition of an excellent scheme; Y over a field is a morphism g : Y ⟶ Spec k; finite type is LocallyOfFiniteType with QuasiCompact; X normal is AlgebraicGeometry.IsNormal ([Stacks, Tag 033I]); and "the maximal open subscheme where f is étale" is an open V that is the greatest element of the set of opens U with U.ι ≫ f étale. The proof uses purity of the ramification locus, AlgebraicGeometry.etaleAt_of_etaleAt_codimensionOne ([Stacks, Tag 0EA4]), and [Stacks, Tag 0ECC], Stacks.PuncturedSpectrum.isAffine_of_cohomologyOverBase_vanishing; see the module documentation. Quasi-compactness of f is not used by the argument.

theorem isAffineHom_maximalEtaleOpen
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] [QuasiCompact f] [IsNormal X]
    (hYregular : IsRegular Y)
    (hYexcellent : ∀ y : Y, ∃ U : Y.affineOpens, y ∈ U.1 ∧ IsExcellent Γ(Y, U))
    (k : Type u) [Field k] (g : Y ⟶ Spec (.of k))
    (V : X.Opens) (hV : IsGreatest {U : X.Opens | Etale (U.ι ≫ f)} V) :
    IsAffineHom V.ι

Sources

LeanStacks.EtalePuncturedSpectrum.exists_directSum_injectiveHull_residueField · Stacks.SpectralSequence.isZero_derivedTensorHomology_zero_singleHomology_zero · Stacks.PuncturedSpectrum.isAffine_of_cohomologyOverBase_vanishing · Stacks.PuncturedSpectrum.isAffine_of_subsingleton_quotTensor_globalSections · Stacks.PuncturedSpectrum.isZero_derivedTensorHomology_cohomologyOverBase_residueField · Stacks.LocalCohomology.derivedSectionsMinus · AlgebraicGeometry.MaximalEtaleOpen.isAffineHom_maximalEtaleOpen

Section58.30 Specialization maps in the smooth proper case #

Section 58.30 of the Stacks Project, Tag 0BUQ. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0C0P, a lemma

Tag 0C0P in the Stacks Project.

AlgebraicGeometry.surjective_specializationMap_of_isProper_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/SpecializationSurjective.lean, line 542. The attribute's comment: “the whole statement, under the source's hypotheses only.”. References: SGA 1 X (2.4), “more general”; SGA 1 X (3.8), “more general”.

Stacks Project, Tag 0C0P. Let f : X ⟶ S be a flat proper morphism with geometrically connected fibres and let s' ⇝ s be a specialization of points of S, realized as in the construction of the specialization map: A is a strict henselization of 𝒪_{S,s} relative to a separable closure of κ(s), and the two geometric points are factored through Spec A, the special one over the closed point. Let
sp : π₁(X_{s̄'}) ⟶ π₁(X_{s̄})
be the resulting specialization map, that is, a continuous homomorphism satisfying the equation defining it against the canonical maps to π₁(X_A). If the fibre X_s is geometrically reduced, then sp is surjective.

No finiteness hypothesis beyond properness is needed. Every specialization map is isomorphic to a specialization map over a strictly henselian valuation ring R, for the base change X_R ⟶ Spec R along a morphism Spec R ⟶ S carrying the generic point of Spec R to the image of s̄' and the closed point to the image of s̄. That base change is flat and proper with geometrically connected fibres, its closed fibre is geometrically reduced because X_s is, and over a valuation ring a flat morphism of finite type is automatically of finite presentation. So the geometrically reduced fibre locus of X_R ⟶ Spec R is open and contains the closed point of the local scheme Spec R, hence is all of it; the homotopy sequence of X_R ⟶ Spec R together with the triviality of π₁(Spec R) makes the specialization map over R surjective, and surjectivity transports back to sp.

AlgebraicGeometry.surjective_specializationMap_of_properFlat is the same conclusion for a morphism which is moreover assumed to be of finite presentation.

theorem surjective_specializationMap_of_isProper_of_flat {X S : Scheme.{u}} (f : X ⟶ S)
    [IsProper f] [Flat f] [GeometricallyConnected f] (s' s : GeometricPoint S)
    (hred : GeometricallyReduced
      (f.fiberToSpecResidueField (s.hom (closedPoint s.residueField))))
    (A : Type u) [CommRing A] [IsLocalRing A]
    [Algebra (S.presheaf.stalk (s.hom (closedPoint s.residueField))) A]
    (hA : Stacks.StrictHenselization.IsStrictHenselization
      (S.presheaf.stalk (s.hom (closedPoint s.residueField)))
      (SeparableClosure
        (maximalIdeal (S.presheaf.stalk (s.hom (closedPoint s.residueField)))).ResidueField) A)
    (p' : s'.source ⟶ Spec (.of A))
    (hp' : p' ≫ specStalkAlgebraHom S (s.hom (closedPoint s.residueField)) A = s'.hom)
    (p : s.source ⟶ Spec (.of A))
    (hp : p ≫ specStalkAlgebraHom S (s.hom (closedPoint s.residueField)) A = s.hom)
    (hclosed : p (closedPoint s.residueField) = closedPoint A)
    (x' : GeometricPoint (fiberOverGeometricPoint f s'))
    (x : GeometricPoint (fiberOverGeometricPoint f s))
    (sp : EtaleFundamentalGroup (fiberOverGeometricPoint f s') x' →ₜ*
      EtaleFundamentalGroup (fiberOverGeometricPoint f s) x) :
    letI : ConnectedSpace
        ↥(pullback f (specStalkAlgebraHom S (s.hom (closedPoint s.residueField)) A)) :=
      connectedSpace_pullback_spec_of_isProper f A _
    ∀ t : finiteEtaleFiberFunctor (x'.map (fiberOverGeometricPointMap f s' _ p' hp')) ≅
        finiteEtaleFiberFunctor (x.map (fiberOverGeometricPointMap f s _ p hp)),
      (∀ γ, etaleFundamentalGroupMap (fiberOverGeometricPointMap f s _ p hp) x (sp γ)
          = etaleFundamentalGroupMulEquiv t
            (etaleFundamentalGroupMap (fiberOverGeometricPointMap f s' _ p' hp') x' γ)) →
        Function.Surjective sp

Tag 0C0Q, a proposition

Tag 0C0Q in the Stacks Project.

AlgebraicGeometry.bijective_isSpecializationMap_of_ringChar_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/SpecializationInjective/GaloisGenericFibreDescent.lean, line 723. The attribute's comment: “the whole statement, under the source's hypotheses only: f smooth and proper with geometrically connected fibres (IsProper f, Smooth f, GeometricallyConnected f), a specialization of points of S realized by a specialization map sp (hsp), and κ(s) of characteristic zero (hchar). The conclusion Function.Bijective sp is the source's conclusion that sp is an isomorphism: sp is a continuous homomorphism of profinite groups, so bijectivity is invertibility. Both halves are proved -- surjectivity through Tag 0C0P and injectivity through the descent of the Galois covers of a geometric generic fibre over a strictly henselian discrete valuation ring of residue characteristic zero.”. References: SGA 1 X (2.5), “more general”; SGA 1 X (3.8), “special case”; SGA 1 X (3.9).

[Stacks, Tag 0C0Q]. Let f : X ⟶ S be a smooth proper morphism with geometrically connected fibres, let s' ⇝ s be a specialization of points of S realized by a specialization map sp : π₁(X_{s̄'}) ⟶ π₁(X_{s̄}), and suppose the residue characteristic of s is zero. Then sp is bijective, i.e. an isomorphism of topological groups.

Surjectivity is [Stacks, Tag 0C0P]. Injectivity is reduced, by AlgebraicGeometry.bijective_isSpecializationMap_of_ringChar_zero_of_forall_essImage_isGalois, to the descent of the Galois covers of a geometric generic fibre over a strictly henselian discrete valuation ring of residue characteristic zero, which is AlgebraicGeometry.exists_finiteEtale_model_of_isGalois_geometricGenericFibre.

theorem bijective_isSpecializationMap_of_ringChar_zero {X S : Scheme.{u}} (f : X ⟶ S)
    [IsProper f] [Smooth f] [GeometricallyConnected f] (s' s : GeometricPoint S)
    (x' : GeometricPoint (fiberOverGeometricPoint f s'))
    (x : GeometricPoint (fiberOverGeometricPoint f s))
    (sp : EtaleFundamentalGroup (fiberOverGeometricPoint f s') x' →ₜ*
      EtaleFundamentalGroup (fiberOverGeometricPoint f s) x)
    (hsp : IsSpecializationMap f s' s x' x sp)
    (hchar : ringChar (S.residueField (s.hom default)) = 0) :
    Function.Bijective sp

Tag 0C0R, a theorem

Tag 0C0R in the Stacks Project.

AlgebraicGeometry.surjective_and_exists_continuousMulEquiv_primeToP, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/SpecializationPrimeToP/GaloisGenericFibrePrimeToP.lean, line 461. The attribute's comment: “the whole statement, under the source's hypotheses only: f smooth and proper with geometrically connected fibres (IsProper f, Smooth f, GeometricallyConnected f), a specialization of points of S realized by a specialization map sp (hsp), and p the characteristic of κ(s) (hchar). Both of the source's conclusions are stated and proved: sp is surjective, and the induced map of the maximal prime-to-p quotients is an isomorphism of topological groups commuting with the projections, which is the source's isomorphism π'₁(X_{s̄'}) ≅ π'₁(X_{s̄}).”. References: SGA 1 X (3.8), “more general”; SGA 1 X (3.9).

[Stacks, Tag 0C0R]. Let f : X ⟶ S be a smooth proper morphism with geometrically connected fibres, let s' ⇝ s be a specialization of points of S realized by a specialization map sp : π₁(X_{s̄'}) ⟶ π₁(X_{s̄}), and let p be the characteristic of κ(s). Then sp is surjective and induces an isomorphism π'₁(X_{s̄'}) ≅ π'₁(X_{s̄}) of the maximal prime-to-p quotients, commuting with the projections.

Surjectivity is [Stacks, Tag 0C0P]. The isomorphism of the maximal prime-to-p quotients is reduced by surjective_and_exists_continuousMulEquiv_primeToP_of_forall_isDiscreteValuationRing to the descent of the Galois covers of order prime to p of a geometric generic fibre over a strictly henselian discrete valuation ring with algebraically closed residue field of characteristic p, which is AlgebraicGeometry.exists_finiteEtale_model_of_isGalois_geometricGenericFibre_of_not_dvd.

theorem surjective_and_exists_continuousMulEquiv_primeToP {X S : Scheme.{u}} (f : X ⟶ S)
    [Smooth f] [IsProper f] [GeometricallyConnected f] (s' s : GeometricPoint S) (p : ℕ)
    (x' : GeometricPoint (fiberOverGeometricPoint f s'))
    (x : GeometricPoint (fiberOverGeometricPoint f s))
    (sp : EtaleFundamentalGroup (fiberOverGeometricPoint f s') x' →ₜ*
      EtaleFundamentalGroup (fiberOverGeometricPoint f s) x)
    (hsp : IsSpecializationMap f s' s x' x sp)
    (hchar : ringChar (S.residueField (s.hom default)) = p) :
    Function.Surjective sp ∧
      ∃ e : PrimeToP p (EtaleFundamentalGroup (fiberOverGeometricPoint f s') x') ≃ₜ*
          PrimeToP p (EtaleFundamentalGroup (fiberOverGeometricPoint f s) x),
        ∀ g, e (primeToPMk p _ g) = primeToPMk p _ (sp g)

Sources

LeanAlgebraicGeometry.surjective_specializationMap_of_isProper_of_flat · AlgebraicGeometry.bijective_isSpecializationMap_of_ringChar_zero · AlgebraicGeometry.surjective_and_exists_continuousMulEquiv_primeToP

Section58.31 Tame ramification #

Section 58.31 of the Stacks Project, Tag 0BSE. 9 tags here are carried by 26 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0EYD, a lemma

Tag 0EYD in the Stacks Project.

Stacks.FundamentalGroup.pulledBackCover_isFinite, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/CodimensionOnePullback.lean, line 207. The attribute's comment: “finite_etale_pullback”.

The canonical pullback of the cover is finite.

public instance pulledBackCover_isFinite
    (D : CodimensionOnePullbackSetup.{u}) :
    IsFinite D.pulledBackCover

Stacks.FundamentalGroup.pulledBackCover_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/CodimensionOnePullback.lean, line 216. The attribute's comment: “finite_etale_pullback”.

The canonical pullback of the cover is étale.

public instance pulledBackCover_etale
    (D : CodimensionOnePullbackSetup.{u}) :
    Etale D.pulledBackCover

Stacks.FundamentalGroup.pulledBackCover_isUnramifiedInCodimensionOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/CodimensionOnePullbackRamification.lean, line 511. The attribute's comment: “unramified_in_codimension_one”.

Stacks 0EYD, unramified half. If the cover Y → U is unramified over X in codimension one, then the pulled-back cover is unramified over X' in codimension one.

public theorem pulledBackCover_isUnramifiedInCodimensionOne
    (D : CodimensionOnePullbackSetup.{u})
    (h : IsUnramifiedInCodimensionOne D.U.ι D.f) :
    IsUnramifiedInCodimensionOne (pullback.fst D.g D.U.ι) D.pulledBackCover

Stacks.FundamentalGroup.pulledBackCover_isTamelyRamifiedInCodimensionOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/CodimensionOnePullbackRamification.lean, line 533. The attribute's comment: “tamely_ramified_in_codimension_one”. References: SGA 1 XIII (2.0.2), “partial”; SGA 1 XIII (2.0.3), “more general”.

Stacks 0EYD, tamely ramified half. If the cover Y → U is tamely ramified over X in codimension one, then the pulled-back cover is tamely ramified over X' in codimension one.

public theorem pulledBackCover_isTamelyRamifiedInCodimensionOne
    (D : CodimensionOnePullbackSetup.{u})
    (h : IsTamelyRamifiedInCodimensionOne D.U.ι D.f) :
    IsTamelyRamifiedInCodimensionOne (pullback.fst D.g D.U.ι) D.pulledBackCover

Tag 0H2W, a lemma

Tag 0H2W in the Stacks Project.

AlgebraicGeometry.exists_finiteEtale_of_isUnramifiedInCodimensionOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/ExtendUnramifiedCodimensionOne.lean, line 140. The attribute's comment: “extension across a regular complement, with the two inputs carried”.

Stacks Project, Tag 0H2W. Let X be a locally Noetherian scheme, U ⊆ X a dense open and f : Y ⟶ U finite étale. If Y is unramified over X in codimension one and 𝒪_{X, x} is regular for every x outside U, then f is the restriction of a finite étale cover of X.

public theorem exists_finiteEtale_of_isUnramifiedInCodimensionOne
    (hExtend : ExtendsAcrossCodimensionOneBoundary.{u})
    (hPurity : PurityAtRegularLocalRings.{u})
    {X : Scheme.{u}} [IsLocallyNoetherian X] (U : X.Opens) (hdense : DenseRange U.ι.base)
    (hEssSurj : ∀ V : X.Opens, (∀ x : X, x ∉ V → HasPurity (X.presheaf.stalk x)) →
      (finiteEtaleBaseChange V.ι).EssSurj)
    {Y : Scheme.{u}} (f : Y ⟶ U) [IsFinite f] [Etale f]
    (hunr : Stacks.FundamentalGroup.IsUnramifiedInCodimensionOne U.ι f)
    (hreg : ∀ x : X, x ∉ U → IsRegularLocalRing (X.presheaf.stalk x)) :
    ∃ (Y' : Scheme.{u}) (p : Y' ⟶ X), IsFinite p ∧ Etale p ∧
      ∃ e : pullback p U.ι ≅ Y, e.hom ≫ f = pullback.snd p U.ι

AlgebraicGeometry.exists_finiteEtale_extension_of_isUnramifiedInCodimensionOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/ExtendUnramifiedRegularBoundary.lean, line 183. The attribute's comment: “a finite étale cover unramified in codimension one extends across a regular complement”. References: SGA 1 X (3.3), “partial”; SGA 2 XIV (1.11), “Regular case”.

Stacks Project, Tag 0H2W. Let X be a locally Noetherian scheme, U ⊆ X a dense open and f : Y ⟶ U finite étale. If Y is unramified over X in codimension one and 𝒪_{X, x} is regular for every x outside U, then f is the restriction of a finite étale cover of X: there is a finite étale p : Y' ⟶ X and an isomorphism Y' ×_X U ≅ Y over U.

public theorem exists_finiteEtale_extension_of_isUnramifiedInCodimensionOne
    {X : Scheme.{u}} [IsLocallyNoetherian X] (U : X.Opens) (hdense : DenseRange U.ι.base)
    {Y : Scheme.{u}} (f : Y ⟶ U) [IsFinite f] [Etale f]
    (hunr : Stacks.FundamentalGroup.IsUnramifiedInCodimensionOne U.ι f)
    (hreg : ∀ x : X, x ∉ U → IsRegularLocalRing (X.presheaf.stalk x)) :
    ∃ (Y' : Scheme.{u}) (p : Y' ⟶ X), IsFinite p ∧ Etale p ∧
      ∃ e : pullback p U.ι ≅ Y, e.hom ≫ f = pullback.snd p U.ι

Tag 0EYE, a lemma

Tag 0EYE in the Stacks Project.

AlgebraicGeometry.exists_finiteEtale_extension_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/PurityBranchLocus/ExtendAcrossRegularDivisor.lean, line 67. The attribute's comment: “a finite étale cover of X ∖ D unramified in codimension one extends across a regular effective Cartier divisor D; the special case U = X ∖ D of Tag 0H2W”. References: SGA 7 II (2.3.1), “Extension clause”.

Stacks Project, Tag 0EYE. Let X be a locally Noetherian scheme and let D ⊆ X be an effective Cartier divisor such that D is a regular scheme. Let f : Y ⟶ X ∖ D be a finite étale morphism. If Y is unramified over X in codimension one, then there exists a finite étale morphism p : Y' ⟶ X whose restriction to X ∖ D is Y: an isomorphism Y' ×_X (X ∖ D) ≅ Y over X ∖ D.

Here D is the closed subscheme D.subscheme cut out by the ideal sheaf D, and X ∖ D is the open subscheme D.support.compl.

public theorem exists_finiteEtale_extension_of_isEffectiveCartierDivisor
    {X : Scheme.{u}} [IsLocallyNoetherian X] (D : X.IdealSheafData)
    (hD : Stacks.Divisors.IsEffectiveCartierDivisor D) (hDreg : IsRegular D.subscheme)
    {Y : Scheme.{u}} (f : Y ⟶ D.support.compl) [IsFinite f] [Etale f]
    (hunr : Stacks.FundamentalGroup.IsUnramifiedInCodimensionOne
      (Scheme.Opens.ι D.support.compl) f) :
    ∃ (Y' : Scheme.{u}) (p : Y' ⟶ X), IsFinite p ∧ Etale p ∧
      ∃ e : pullback p (Scheme.Opens.ι D.support.compl) ≅ Y,
        e.hom ≫ f = pullback.snd p (Scheme.Opens.ι D.support.compl)

Tag 0EYF, an example

Tag 0EYF in the Stacks Project.

AlgebraicGeometry.standardTamelyRamifiedAlgebra, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/Basic.lean, line 64. The attribute's comment: “standard_tamely_ramified_morphism”.

The standard tamely ramified algebra A[X] / (X ^ e - f).

public abbrev standardTamelyRamifiedAlgebra (A : Type u) [CommRing A] (f : A) (e : ℕ)

AlgebraicGeometry.standardTamelyRamifiedMorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/Basic.lean, line 69. The attribute's comment: “standard_tamely_ramified_morphism”.

The canonical morphism Spec(A[X] / (X ^ e - f)) ⟶ Spec(A).

public noncomputable abbrev standardTamelyRamifiedMorphism
    (A : Type u) [CommRing A] (f : A) (e : ℕ) :
    Scheme.Spec.obj (Opposite.op (CommRingCat.of (standardTamelyRamifiedAlgebra A f e))) ⟶
      Scheme.Spec.obj (Opposite.op (CommRingCat.of A))

AlgebraicGeometry.standardTamelyRamifiedCover, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/Basic.lean, line 79. The attribute's comment: “standard_tamely_ramified_morphism”.

The associated cover, obtained by restricting the standard morphism over Spec(A_f).

public noncomputable abbrev standardTamelyRamifiedCover
    (A : Type u) [CommRing A] (f : A) (e : ℕ) :
    Scheme.Spec.obj (Opposite.op (CommRingCat.of
        (Localization.Away (algebraMap A (standardTamelyRamifiedAlgebra A f e) f)))) ⟶
      Scheme.Spec.obj (Opposite.op (CommRingCat.of (Localization.Away f)))

AlgebraicGeometry.standardTamelyRamifiedCover_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/Basic.lean, line 91. The attribute's comment: “standard_cover_etale_away”. References: SGA 1 XIII (5.1), “r = 1, étale part”.

Away from f, the standard cover defined by X ^ e = f is étale when e is a unit in the base ring.

public theorem standardTamelyRamifiedCover_etale
    (A : Type u) [CommRing A] (f : A) (e : ℕ) [NeZero e]
    (he : IsUnit (e : A)) :
    Etale (standardTamelyRamifiedCover A f e)

AlgebraicGeometry.standardTamelyRamifiedMorphism_finiteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/Basic.lean, line 181. The attribute's comment: “standard_morphism_finite_locally_free”. References: SGA 1 XIII (5.1), “r = 1, finite part”.

The standard morphism Spec(A[X] / (X ^ e - f)) ⟶ Spec(A) is finite locally free: it is finite, flat and locally of finite presentation. In fact A[X] / (X ^ e - f) is free of rank e over A (standardTamelyRamifiedAlgebra_free, standardTamelyRamifiedAlgebra_finrank), so the morphism is even finite free.

public theorem standardTamelyRamifiedMorphism_finiteLocallyFree
    (A : Type u) [CommRing A] (f : A) (e : ℕ) [NeZero e] :
    IsFinite (standardTamelyRamifiedMorphism A f e) ∧
      Flat (standardTamelyRamifiedMorphism A f e) ∧
      LocallyOfFinitePresentation (standardTamelyRamifiedMorphism A f e)

AlgebraicGeometry.standardTamelyRamifiedCover_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/Basic.lean, line 210. The attribute's comment: “the restriction of the standard morphism over Spec(A_f), that is the standard cover, is finite”.

Stacks 0EYF, finiteness of the standard cover. The restriction Spec(C_f) ⟶ Spec(A_f) of the standard morphism over Spec(A_f) is finite. The ring C_f is the localization of C = A[X] / (X ^ e - f) at the image of f, so it is a finite module over A_f because C is a finite A-module (standardTamelyRamifiedAlgebra_finite); finiteness of a ring map is preserved by localizing source and target at the same element. Together with standardTamelyRamifiedCover_etale this is the assertion of the tag that Spec(C_f) ⟶ Spec(A_f) is a finite étale morphism. As for étaleness, the Noetherian, nonzerodivisor, reducedness and invertibility hypotheses of the tag are not needed away from f and are omitted; only positivity of e, expressed by NeZero e, is used.

public theorem standardTamelyRamifiedCover_isFinite
    (A : Type u) [CommRing A] (f : A) (e : ℕ) [NeZero e] :
    IsFinite (standardTamelyRamifiedCover A f e)

AlgebraicGeometry.isDiscreteValuationRing_of_mem_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/StandardExample.lean, line 177. The attribute's comment: “the hypotheses on the base imply that A_p is a DVR with uniformizer f, for every minimal prime p over f”.

Tag 0EYF, the base of the standard tamely ramified morphism. Let A be a Noetherian ring, let f : A be a nonzerodivisor such that A / fA is reduced, and let p be a minimal prime over f. Then the localization A_p is a discrete valuation ring and f is a uniformizer of it. This is the implication asserted in the first sentences of the tag; it is what licenses the discrete valuation ring hypotheses in the tameness statements below.

public theorem isDiscreteValuationRing_of_mem_minimalPrimes [IsNoetherianRing A] {f : A}
    (hf : f ∈ nonZeroDivisors A) (hred : _root_.IsReduced (A ⧸ Ideal.span ({f} : Set A)))
    {p : Ideal A} [p.IsPrime] (hp : p ∈ (Ideal.span ({f} : Set A)).minimalPrimes)
    (S : Type v) [CommRing S] [Algebra A S] [IsLocalization.AtPrime S p] :
    ∃ _ : IsDomain S, IsDiscreteValuationRing S ∧ Irreducible (algebraMap A S f)

AlgebraicGeometry.standardTamelyRamifiedGenericFibreEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/StandardExample.lean, line 254. The attribute's comment: “standard_cover_generic_fibre”.

The generic fibre of the standard morphism is the Kummer extension. Base changing C = A[X] / (X ^ e - f) along A → K gives K[X] / (X ^ e - f), i.e. the Kummer algebra K[f ^ (1 / e)] of Tag 09EV.

public def standardTamelyRamifiedGenericFibreEquiv :
    K ⊗[A] standardTamelyRamifiedAlgebra A f e ≃ₐ[K] K1 K f e

AlgebraicGeometry.standardTamelyRamifiedGenericFibre_isTamelyRamified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/StandardExample.lean, line 271. The attribute's comment: “the generic fibre of the standard cover at a codimension-one point is tamely ramified with respect to the local ring, for an exponent e ≥ 2”. References: SGA 1 XIII (5.1), “r = 1, tame part”.

Tag 0EYF, tameness in codimension one. Let A be a discrete valuation ring with uniformizer f; this is the local ring of Spec(A) at the generic point of a prime divisor contained in the complement of Spec(A_f). Let K be its fraction field and let e ≥ 2 be invertible in A. The generic fibre of the standard morphism over that point is the field K[f ^ (1 / e)] = K[X] / (X ^ e - f) (standardTamelyRamifiedGenericFibreEquiv), and that field extension of K is tamely ramified with respect to A.

public theorem standardTamelyRamifiedGenericFibre_isTamelyRamified
    (hf : Irreducible f) (he : 2 ≤ e) (hinv : IsUnit (e : A)) :
    letI : Fact (Irreducible (kummerPoly K f e)) :=
      ⟨kummerPoly_irreducible K f e (by omega) hf⟩
    letI : Algebra.IsSeparable K (K1 K f e) :=
      isSeparable_K1 K f e he hf (ringChar_residue_coprime_of_isUnit (R := A) e hinv)
    IsDiscreteValuationRing.IsTamelyRamifiedWithRespectTo A K (K1 K f e)

AlgebraicGeometry.isTamelyRamified_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/StandardExample.lean, line 307. The attribute's comment: “trivial_extension_tame”.

The trivial extension is tamely ramified. K / K is tamely ramified with respect to the discrete valuation ring A.

public theorem isTamelyRamified_self :
    IsDiscreteValuationRing.IsTamelyRamifiedWithRespectTo A K K

AlgebraicGeometry.standardTamelyRamifiedGenericFibreEquivOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/StandardExample.lean, line 322. The attribute's comment: “standard_cover_generic_fibre_one”.

Tag 0EYF, the exponent e = 1. The generic fibre of the standard morphism for e = 1 is K itself; combined with isTamelyRamified_self this is tameness in codimension one for the degenerate exponent.

public def standardTamelyRamifiedGenericFibreEquivOne :
    K ⊗[A] standardTamelyRamifiedAlgebra A f 1 ≃ₐ[K] K

AlgebraicGeometry.standardTamelyRamifiedGenericFibreFactor_isTamelyRamified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/StandardExample.lean, line 390. The attribute's comment: “every field factor of the generic fibre of the standard cover at a codimension-one point is tamely ramified with respect to the local ring”.

Tag 0EYF, tameness in codimension one for every field factor. Let A be a discrete valuation ring with uniformizer f — by isDiscreteValuationRing_of_mem_minimalPrimes this is the local ring of Spec(A) at the generic point of a prime divisor outside Spec(A_f) — let K be its fraction field, and let e ≥ 1 be invertible in A. Then every field factor of the generic fibre K ⊗[A] C of the standard cover, that is, every field L receiving a surjection of K-algebras from it, is a finite separable extension of K which is tamely ramified with respect to A.

public theorem standardTamelyRamifiedGenericFibreFactor_isTamelyRamified
    (hf : Irreducible f) (he : 1 ≤ e) (hinv : IsUnit (e : A))
    (L : Type*) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    (φ : K ⊗[A] standardTamelyRamifiedAlgebra A f e →ₐ[K] L)
    (hφ : Function.Surjective φ) :
    ∃ (_ : Module.Finite K L) (_ : Algebra.IsSeparable K L),
      IsDiscreteValuationRing.IsTamelyRamifiedWithRespectTo A K L

AlgebraicGeometry.standardTamelyRamifiedCover_isTamelyRamifiedInCodimensionOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameRamification/StandardExampleCodimensionOne.lean, line 387. The attribute's comment: “standard_cover_tame_codimension_one”. References: SGA 1 XIII (5.1), “r = 1, codim 1 tame”.

Stacks 0EYF, tameness in codimension one. Let A be a Noetherian ring, let f : A be a nonzerodivisor such that A / fA is reduced, and let e ≥ 1 be invertible in A. The finite étale cover Spec(C_f) ⟶ Spec(A_f) attached to C = A[x] / (x ^ e - f) is tamely ramified over Spec(A) in codimension one.

public theorem standardTamelyRamifiedCover_isTamelyRamifiedInCodimensionOne
    (A : Type u) [CommRing A] [IsNoetherianRing A] (f : A) (e : ℕ) [NeZero e]
    (hf : f ∈ nonZeroDivisors A)
    (hred : _root_.IsReduced (A ⧸ Ideal.span ({f} : Set A)))
    (hinv : IsUnit (e : A)) :
    Stacks.FundamentalGroup.IsTamelyRamifiedInCodimensionOne
      (standardTamelyRamifiedOpen A f) (standardTamelyRamifiedCover A f e)

Tag 0EYG, a lemma

Tag 0EYG in the Stacks Project.

AlgebraicGeometry.isEtaleLocallyStandardTamelyRamified_of_isTamelyRamifiedInCodimensionOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/Abhyankar/RegularDivisorUnconditional.lean, line 98. The attribute's comment: “Abhyankar's lemma for a regular divisor: a finite étale cover of X ∖ D tamely ramified in codimension one is étale locally on X a finite disjoint union of the standard tamely ramified covers of Example 0EYF”.

Abhyankar's lemma for a regular divisor, [Stacks, Tag 0EYG]. Let X be a locally Noetherian scheme and let D ⊆ X be an effective Cartier divisor such that D is a regular scheme. Let f : Y ⟶ X ∖ D be a finite étale morphism. If Y is tamely ramified over X in codimension one, then étale locally on X the morphism Y ⟶ X is a finite disjoint union of standard tamely ramified morphisms as described in [Stacks, Example 0EYF]: every x ∈ X lies in the image of an étale Spec A ⟶ X with A Noetherian, on which X ∖ D is Spec A_φ for a nonzerodivisor φ with A / φA reduced, and over which Y is ∐ᵢ Spec (A[x]/(x^{eᵢ} - φ))_φ with each eᵢ ≥ 1 invertible in A.

Here D is the closed subscheme D.subscheme cut out by the ideal sheaf D, and X ∖ D is the open subscheme D.support.compl.

theorem isEtaleLocallyStandardTamelyRamified_of_isTamelyRamifiedInCodimensionOne
    {X : Scheme.{u}} [IsLocallyNoetherian X] (D : X.IdealSheafData)
    (hD : Stacks.Divisors.IsEffectiveCartierDivisor D) (hDreg : IsRegular D.subscheme)
    {Y : Scheme.{u}} (f : Y ⟶ (D.support.compl : X.Opens)) [IsFinite f] [Etale f]
    (htame : IsTamelyRamifiedInCodimensionOne (Scheme.Opens.ι (D.support.compl : X.Opens)) f) :
    IsEtaleLocallyStandardTamelyRamified (D.support.compl : X.Opens) f

Tag 0EYH, a lemma

Tag 0EYH in the Stacks Project.

AlgebraicGeometry.TameCovers.normalization_of_isTamelyRamifiedInCodimensionOne_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameCovers/NormalizationAlongRegularDivisor.lean, line 73. The attribute's comment: “the normalization of X in a tame cover Y of X ∖ D is finite locally free, restricts to Y, has π⁻¹(D)_red a regular effective Cartier divisor, and is étale locally a finite disjoint union of standard Spec(A[x]/(x^e - f)) ⟶ Spec(A)”.

Stacks Project, Tag 0EYH. Let X be a locally Noetherian scheme, let D ⊆ X be an effective Cartier divisor such that D is a regular scheme, and let f : Y ⟶ X ∖ D be finite étale and tamely ramified over X in codimension one (the situation of [Stacks, Tag 0EYG]). Then the normalization π : Y' ⟶ X of X in Y is a finite locally free morphism such that 1. the restriction of Y' to X ∖ D is isomorphic to Y (over X ∖ D), 2. D' = π⁻¹(D)_red is an effective Cartier divisor on Y', and 3. D' is a regular scheme. Moreover, étale locally on X the morphism Y' ⟶ X is a finite disjoint union of morphisms Spec(A[x]/(x^e - φ)) ⟶ Spec(A) where A is a Noetherian ring, φ ∈ A is a nonzerodivisor with A/φA regular, and e ≥ 1 is invertible in A: every x ∈ X is in the image of an étale g : Spec A ⟶ X over which Y' ×_X Spec A ≅ ∐ᵢ Spec(A[x]/(x^{eᵢ} - φ)) over Spec A.

Here π is (f ≫ ι).fromNormalization for the inclusion ι of X ∖ D = D.support.compl, and D' is the closed subscheme of the radical of the ideal sheaf D.comap π.

public theorem normalization_of_isTamelyRamifiedInCodimensionOne_of_isRegular {X : Scheme.{u}}
    [IsLocallyNoetherian X] (D : X.IdealSheafData)
    (hD : Stacks.Divisors.IsEffectiveCartierDivisor D) (hDreg : IsRegular D.subscheme)
    {Y : Scheme.{u}} (f : Y ⟶ (D.support.compl : X.Opens)) [IsFinite f] [Etale f]
    (hf : Stacks.FundamentalGroup.IsTamelyRamifiedInCodimensionOne
      (Scheme.Opens.ι (D.support.compl : X.Opens)) f) :
    Stacks.Morphisms.IsFiniteLocallyFree
        (f ≫ Scheme.Opens.ι (D.support.compl : X.Opens)).fromNormalization ∧
      (∃ e : pullback (f ≫ Scheme.Opens.ι (D.support.compl : X.Opens)).fromNormalization
          (Scheme.Opens.ι (D.support.compl : X.Opens)) ≅ Y,
        e.hom ≫ f = pullback.snd _ _) ∧
      Stacks.Divisors.IsEffectiveCartierDivisor
        (D.comap (f ≫ Scheme.Opens.ι (D.support.compl : X.Opens)).fromNormalization).radical ∧
      IsRegular (D.comap (f ≫ Scheme.Opens.ι
          (D.support.compl : X.Opens)).fromNormalization).radical.subscheme ∧
      ∀ x : X, ∃ (A : CommRingCat.{u}) (g : Spec A ⟶ X) (_ : Etale g) (a : Spec A)
        (_ : g a = x) (φ : A) (_ : IsNoetherianRing A) (_ : φ ∈ nonZeroDivisors A)
        (_ : IsRegularRing (A ⧸ Ideal.span {φ})) (n : ℕ) (e : Fin n → ℕ)
        (_ : ∀ i, 0 < e i ∧ IsUnit (e i : A)),
        ∃ ι : pullback (f ≫ Scheme.Opens.ι (D.support.compl : X.Opens)).fromNormalization g ≅
            ∐ fun i ↦ Spec (.of (standardTamelyRamifiedAlgebra A φ (e i))),
          ι.hom ≫ Sigma.desc (fun i ↦ standardTamelyRamifiedMorphism A φ (e i)) =
            pullback.snd _ g

Tag 0EYI, a lemma

Tag 0EYI in the Stacks Project.

AlgebraicGeometry.TameCovers.exists_lift_etaleAt_fromNormalization_of_isTamelyRamified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameCovers/LiftDiscreteValuationRingPoints.lean, line 61. The attribute's comment: “(1): a lift of t|_{Spec K} to Y gives a lift t' of t to the normalization Y', and Y' ⟶ X is étale along t'(Spec R)”.

Stacks Project, Tag 0EYI (1). Let X be a locally Noetherian scheme, D ⊆ X an effective Cartier divisor such that D is a regular scheme, and f : Y ⟶ X ∖ D a finite étale morphism tamely ramified over X in codimension one (the situation of [Stacks, Tag 0EYG]). Let π : Y' ⟶ X be the normalization of X in Y ([Stacks, Tag 0EYH]). Let R be a discrete valuation ring with fraction field K and t : Spec R ⟶ X a morphism such that the scheme theoretic inverse image t⁻¹D is the reduced closed point of Spec R. If t|_{Spec K} lifts to a point y : Spec K ⟶ Y, then there is a lift t' : Spec R ⟶ Y' of t (extending y) such that π is étale along t'(Spec R).

Here D is the closed subscheme D.subscheme cut out by the ideal sheaf D, X ∖ D is the open subscheme D.support.compl, and Y' is the relative normalization of Y ⟶ X.

theorem exists_lift_etaleAt_fromNormalization_of_isTamelyRamified
    {X : Scheme.{u}} [IsLocallyNoetherian X] (D : X.IdealSheafData)
    (hD : Stacks.Divisors.IsEffectiveCartierDivisor D) (hDreg : IsRegular D.subscheme)
    {Y : Scheme.{u}} (f : Y ⟶ (D.support.compl : X.Opens)) [IsFinite f] [Etale f]
    (hf : Stacks.FundamentalGroup.IsTamelyRamifiedInCodimensionOne
      (Scheme.Opens.ι (D.support.compl : X.Opens)) f)
    (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    (K : Type u) [Field K] [Algebra R K] [IsFractionRing R K]
    (t : Spec (.of R) ⟶ X)
    (ht : D.comap t = Scheme.IdealSheafData.vanishingIdeal
      ⟨({IsLocalRing.closedPoint R} : Set (Spec (.of R))),
        (PrimeSpectrum.isClosed_singleton_iff_isMaximal _).mpr
          (IsLocalRing.maximalIdeal.isMaximal R)⟩)
    (y : Spec (.of K) ⟶ Y)
    (hy : y ≫ f ≫ Scheme.Opens.ι (D.support.compl : X.Opens) =
      Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ t) :
    ∃ t' : Spec (.of R) ⟶ (f ≫ Scheme.Opens.ι (D.support.compl : X.Opens)).normalization,
      t' ≫ (f ≫ Scheme.Opens.ι (D.support.compl : X.Opens)).fromNormalization = t ∧
      Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ t' =
        y ≫ (f ≫ Scheme.Opens.ι (D.support.compl : X.Opens)).toNormalization ∧
      ∀ r, EtaleAt (f ≫ Scheme.Opens.ι (D.support.compl : X.Opens)).fromNormalization (t' r)

AlgebraicGeometry.TameCovers.exists_opens_etale_fromNormalization_of_isTamelyRamified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/TameCovers/LiftDiscreteValuationRingPoints.lean, line 95. The attribute's comment: “(2): if Spec K ×_X Y is a disjoint union of copies of Spec K, the normalization Y' ⟶ X is finite étale over an open neighbourhood of t(Spec R)”.

Stacks Project, Tag 0EYI (2). In the situation of Tag 0EYI (1) (X locally Noetherian, D ⊆ X an effective Cartier divisor which is a regular scheme, f : Y ⟶ X ∖ D finite étale and tamely ramified over X in codimension one, π : Y' ⟶ X the normalization of X in Y, R a discrete valuation ring with fraction field K, t : Spec R ⟶ X with t⁻¹D the reduced closed point of Spec R): if Spec K ×_X Y is isomorphic, over Spec K, to a disjoint union of copies of Spec K, then π is finite étale over an open neighbourhood V of t(Spec R).

theorem exists_opens_etale_fromNormalization_of_isTamelyRamified
    {X : Scheme.{u}} [IsLocallyNoetherian X] (D : X.IdealSheafData)
    (hD : Stacks.Divisors.IsEffectiveCartierDivisor D) (hDreg : IsRegular D.subscheme)
    {Y : Scheme.{u}} (f : Y ⟶ (D.support.compl : X.Opens)) [IsFinite f] [Etale f]
    (hf : Stacks.FundamentalGroup.IsTamelyRamifiedInCodimensionOne
      (Scheme.Opens.ι (D.support.compl : X.Opens)) f)
    (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    (K : Type u) [Field K] [Algebra R K] [IsFractionRing R K]
    (t : Spec (.of R) ⟶ X)
    (ht : D.comap t = Scheme.IdealSheafData.vanishingIdeal
      ⟨({IsLocalRing.closedPoint R} : Set (Spec (.of R))),
        (PrimeSpectrum.isClosed_singleton_iff_isMaximal _).mpr
          (IsLocalRing.maximalIdeal.isMaximal R)⟩)
    (J : Type u)
    (eJ : pullback (Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ t)
        (f ≫ Scheme.Opens.ι (D.support.compl : X.Opens)) ≅ ∐ fun _ : J ↦ Spec (.of K))
    (heJ : eJ.hom ≫ Sigma.desc (fun _ ↦ 𝟙 _) = pullback.fst _ _) :
    ∃ V : X.Opens, (∀ r, t r ∈ V) ∧
      IsFinite ((f ≫ Scheme.Opens.ι (D.support.compl : X.Opens)).fromNormalization ∣_ V) ∧
      Etale ((f ≫ Scheme.Opens.ι (D.support.compl : X.Opens)).fromNormalization ∣_ V)

Tag 0EYJ, a lemma

Tag 0EYJ in the Stacks Project.

AlgebraicGeometry.FiniteEtaleGaloisCover.exists_extension_of_genericFiber_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/Abhyankar/GaloisCoverNoetherianExtension.lean, line 51. The attribute's comment: “the full statement under the tag's hypotheses and nothing else: S integral (IsIntegral S), normal (IsNormal S) and Noetherian (IsNoetherian S); f smooth with geometrically connected fibres (Smooth f, GeometricallyConnected f); a section σ of f (hσ); a finite étale Galois cover Z of the generic fibre X_η with group G, G finite of order invertible on S (hG: a unit in every residue field); a κ(η)-rational point z of Z over σ(η) (hz). The conclusion is a finite étale Galois cover Y of X with group G and a G-equivariant isomorphism Y ×_X X_η ≅ Z over X_η.”.

Extending a Galois cover of the generic fibre. Let S be an integral normal Noetherian scheme with generic point η, let f : X ⟶ S be a smooth morphism with geometrically connected fibres and let σ : S ⟶ X be a section of f. Let Z ⟶ X_η be a finite étale Galois cover with group G whose order is invertible on S (a unit in every residue field κ(s)), such that Z has a κ(η)-rational point z mapping to σ(η). Then there is a finite étale Galois cover Y ⟶ X with group G whose restriction to X_η is Z: an isomorphism Y ×_X X_η ≅ Z over X_η compatible with the actions of G.

theorem exists_extension_of_genericFiber_of_isNoetherian
    {S X : Scheme.{u}} (f : X ⟶ S) [IsNoetherian S] [IsIntegral S] [IsNormal S]
    [Smooth f] [GeometricallyConnected f]
    (σ : S ⟶ X) (hσ : σ ≫ f = 𝟙 S)
    (G : Type v) [Group G] [Finite G]
    (hG : ∀ s : S, IsUnit (Nat.card G : S.residueField s))
    (Z : FiniteEtaleGaloisCover (f.fiber (genericPoint S)) G)
    (z : Spec (S.residueField (genericPoint S)) ⟶ Z.obj.left)
    (hz : z ≫ Z.obj.hom = genericFiberSection f σ hσ) :
    ∃ (Y : FiniteEtaleGaloisCover X G)
      (e : (finiteEtaleBaseChange (f.fiberι (genericPoint S))).obj Y.obj ≅ Z.obj),
      ∀ g : Gᵐᵒᵖ, (finiteEtaleBaseChange (f.fiberι (genericPoint S))).map (Y.action g).asIso.hom ≫
        e.hom = e.hom ≫ (Z.action g).asIso.hom

Tag 0EZJ, a lemma

Tag 0EZJ in the Stacks Project.

AlgebraicGeometry.FiniteEtaleGaloisCover.exists_extending_genericFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/GaloisCoverLimits/ExtensionTheorem.lean, line 57. The attribute's comment: “the full statement under the tag's hypotheses: S qcqs integral normal; f qcqs smooth with geometrically connected fibres and a section σ; Z a finite étale Galois cover of X_η with group G of order invertible on S and a κ(η)-point over σ(η); the extension Y is G-equivariantly a Galois cover restricting to Z”.

Stacks Project, Tag 0EZJ. Let S be a quasi-compact and quasi-separated integral normal scheme with generic point η, let f : X ⟶ S be a quasi-compact and quasi-separated smooth morphism with geometrically connected fibres and σ a section of f. Let Z ⟶ X_η be a finite étale Galois cover (Section 03SF) with group G of order invertible on S such that Z has a κ(η)-rational point z mapping to σ(η). Then there is a finite étale Galois cover Y ⟶ X with group G whose restriction to X_η is Z: the restriction is isomorphic to Z by an isomorphism compatible with the two actions of G.

The order of G is invertible on S when it is a unit in every residue field of S.

theorem exists_extending_genericFiber
    {S X : Scheme.{u}} (f : X ⟶ S)
    [CompactSpace S] [QuasiSeparatedSpace S] [IsIntegral S] [IsNormal S]
    [QuasiCompact f] [QuasiSeparated f] [Smooth f] [GeometricallyConnected f]
    (σ : S ⟶ X) (hσ : σ ≫ f = 𝟙 S)
    (G : Type v) [Group G] [Finite G]
    (hG : ∀ s : S, IsUnit (Nat.card G : S.residueField s))
    (Z : FiniteEtaleGaloisCover (f.fiber (genericPoint S)) G)
    (z : Spec (S.residueField (genericPoint S)) ⟶ Z.obj.left)
    (hz : z ≫ Z.obj.hom = genericFiberSection f σ hσ) :
    ∃ (Y : FiniteEtaleGaloisCover X G)
      (e : (finiteEtaleBaseChange (f.fiberι (genericPoint S))).obj Y.obj ≅ Z.obj),
      ∀ g : Gᵐᵒᵖ, (finiteEtaleBaseChange (f.fiberι (genericPoint S))).map (Y.action g).asIso.hom ≫
        e.hom = e.hom ≫ (Z.action g).asIso.hom

Sources

LeanStacks.FundamentalGroup.pulledBackCover_isFinite · Stacks.FundamentalGroup.pulledBackCover_etale · Stacks.FundamentalGroup.pulledBackCover_isUnramifiedInCodimensionOne · Stacks.FundamentalGroup.pulledBackCover_isTamelyRamifiedInCodimensionOne · AlgebraicGeometry.exists_finiteEtale_of_isUnramifiedInCodimensionOne · AlgebraicGeometry.exists_finiteEtale_extension_of_isUnramifiedInCodimensionOne · AlgebraicGeometry.exists_finiteEtale_extension_of_isEffectiveCartierDivisor · AlgebraicGeometry.standardTamelyRamifiedAlgebra

Section58.32 Tricks in positive characteristic #

Section 58.32 of the Stacks Project, Tag 0G1E. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0G1F, a lemma

Tag 0G1F in the Stacks Project.

Stacks.Etale.exists_etalePresentation_nonfiniteGeneratorNumber_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/NonfiniteGenerators.lean, line 421.

In positive characteristic, an étale presentation of a finite étale algebra whose nonfinite-generator invariant is positive can be replaced by a compatible étale presentation with strictly smaller invariant.

theorem exists_etalePresentation_nonfiniteGeneratorNumber_lt
    (k : Type u) [Field k] (p : ℕ) [CharP k p] (hp : 0 < p)
    (n : ℕ) (I : Ideal (MvPolynomial (Fin n) k))
    (B : Type w) [CommRing B]
    [Algebra ((MvPolynomial (Fin n) k) ⧸ I) B]
    [Algebra k B] [IsScalarTower k ((MvPolynomial (Fin n) k) ⧸ I) B]
    [Module.Finite ((MvPolynomial (Fin n) k) ⧸ I) B]
    [Algebra.Etale ((MvPolynomial (Fin n) k) ⧸ I) B]
    (C : Type v) [CommRing C] [Algebra k C]
    (φ : MvPolynomial (Fin n) k →ₐ[k] C) (hφ : φ.toRingHom.Etale)
    (τ : (C ⧸ Ideal.map φ.toRingHom I) →ₐ[k] B) (hτ : Function.Surjective τ)
    (hcomm : ∀ f : MvPolynomial (Fin n) k,
      τ (Ideal.Quotient.mk (Ideal.map φ.toRingHom I) (φ f)) =
        algebraMap ((MvPolynomial (Fin n) k) ⧸ I) B (Ideal.Quotient.mk I f))
    (hpos : 0 < nonfiniteGeneratorNumber φ.toRingHom) :
    ∃ (φ' : MvPolynomial (Fin n) k →ₐ[k] C),
      φ'.toRingHom.Etale ∧
      ∃ τ' : (C ⧸ Ideal.map φ'.toRingHom I) →ₐ[k] B,
        Function.Surjective τ' ∧
        (∀ f : MvPolynomial (Fin n) k,
          τ' (Ideal.Quotient.mk (Ideal.map φ'.toRingHom I) (φ' f)) =
            algebraMap ((MvPolynomial (Fin n) k) ⧸ I) B (Ideal.Quotient.mk I f)) ∧
        nonfiniteGeneratorNumber φ'.toRingHom < nonfiniteGeneratorNumber φ.toRingHom

Tag 0G1G, a lemma

Tag 0G1G in the Stacks Project.

AlgebraicGeometry.exists_finiteEtale_to_affineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteEtaleOverAffineSpace.lean, line 82.

An affine scheme étale over affine space in positive characteristic admits a (possibly different) finite étale morphism to the same affine space.

theorem exists_finiteEtale_to_affineSpace
    (k : Type u) [Field k] (p : ℕ) [CharP k p] (hp : 0 < p) (n : ℕ)
    {X : Scheme.{u}} [IsAffine X]
    (f : X ⟶ AffineSpace (ULift.{u} (Fin n)) (Spec (.of k))) [Etale f] :
    ∃ g : X ⟶ AffineSpace (ULift.{u} (Fin n)) (Spec (.of k)),
      IsFinite g ∧ Etale g

Tag 0G1H, a lemma

Tag 0G1H in the Stacks Project.

AlgebraicGeometry.exists_finiteEtale_openClosed_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteEtaleOverClosedSubschemeOfAffineSpace.lean, line 166.

Stacks Project, Tag 0G1H. In positive characteristic, a finite étale cover of a closed subscheme of affine space is an open-and-closed part of the restriction of a finite étale cover of affine space.

theorem exists_finiteEtale_openClosed_pullback
    (k : Type u) [Field k] (p : ℕ) [CharP k p] (hp : 0 < p) (n : ℕ)
    {Z : Scheme.{u}}
    (i : Z ⟶ Spec (.of (MvPolynomial (Fin n) k))) [IsClosedImmersion i]
    {Y : Scheme.{u}} (g : Y ⟶ Z) [IsFinite g] [Etale g] :
    ∃ (U : Scheme.{u}) (f : U ⟶ Spec (.of (MvPolynomial (Fin n) k)))
      (_ : IsFinite f) (_ : Etale f)
      (j : Y ⟶ pullback f i),
      IsOpenImmersion j ∧ IsClosedImmersion j ∧
        j ≫ pullback.snd f i = g

Tag 0G1I, a proposition

Tag 0G1I in the Stacks Project.

AlgebraicGeometry.injective_etaleFundamentalGroupMap_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ClosedImmersionPositiveCharacteristic.lean, line 294.

Stacks Project, Tag 0G1I. A closed immersion of connected affine schemes over 𝐅_p induces an injection on étale fundamental groups. Being a scheme over 𝐅_p is spelled as p being zero in the ring of global sections of the ambient scheme.

theorem injective_etaleFundamentalGroupMap_of_isClosedImmersion (p : ℕ) (hp : p.Prime)
    {Z X : Scheme.{u}} [ConnectedSpace Z] [ConnectedSpace X] [IsAffine Z] [IsAffine X]
    (i : Z ⟶ X) [IsClosedImmersion i] (hX : (p : Γ(X, ⊤)) = 0) (z : GeometricPoint Z) :
    Function.Injective (etaleFundamentalGroupMap i z)

Sources

LeanStacks.Etale.exists_etalePresentation_nonfiniteGeneratorNumber_lt · AlgebraicGeometry.exists_finiteEtale_to_affineSpace · AlgebraicGeometry.exists_finiteEtale_openClosed_pullback · AlgebraicGeometry.injective_etaleFundamentalGroupMap_of_isClosedImmersion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

58.17 Restriction to a closed… to 58.32 Tricks in positive…

Section58.17 Restriction to a closed subscheme#

Tag 0EL8, a lemma

Tag 0EL9, a lemma

Tag 0ELA, a lemma

Tag 0EK1, a lemma

Tag 0EJX, a lemma

Tag 0EJZ, a lemma

Tag 0EK0, a lemma

Sources

Section58.18 Pushouts and fundamental groups#

Tag 0EK4, a lemma

Sources

Section58.19 Finite étale covers of punctured spectra, I#

Tag 0BLF, a situation

Tag 0BLG, a lemma

Tag 0BLH, a lemma

Tag 0BLI, a lemma

Tag 0EK5, a lemma

Tag 0BM6, a lemma

Tag 0BLJ, a lemma

Sources

Section58.20 Purity in local case, I#

Tag 0BM8, a lemma

Tag 0BLK, a lemma

Tag 0BM9, a lemma

Tag 0BLL, a lemma

Tag 0EK6, a lemma

Tag 0BLS, a lemma

Tag 0BLM, a lemma

Sources

Section58.21 Purity of branch locus#

Tag 0BJG, a lemma

Tag 0BJH, a lemma

Tag 0BMA, a lemma

Tag 0BMB, a lemma

Tag 0EY6, a lemma

Tag 0EY7, a lemma

Sources

Section58.22 Finite étale covers of punctured spectra, II#

Tag 0BLN, a lemma

Tag 0DXX, a lemma

Tag 0BLP, a lemma

Sources

Section58.23 Finite étale covers of punctured spectra, III#

Tag 0DXY, a lemma

Tag 0BLV, a lemma

Tag 0BLW, a remark

Sources

Section58.24 Finite étale covers of punctured spectra, IV#

Tag 0EK9, a lemma

Tag 0EKA, a lemma

Sources

Section58.25 Purity in local case, II#

Tag 0DXZ, a lemma

Tag 0BPC, a lemma

Tag 0BPD, a proposition

Sources

Section58.26 Purity in local case, III#

Tag 0EY9, a lemma

Tag 0EYA, a lemma

Tag 0EYB, a lemma

Tag 0EYC, a proposition

Sources

Section58.27 Lefschetz for the fundamental group#

Tag 0ELC, a proposition

Tag 0ELD, a proposition

Tag 0ELE, a proposition

Sources

Section58.28 Purity of ramification locus#

Tag 0EA2, a lemma

Tag 0EA3, a lemma

Tag 0EA4, a lemma

Sources

Section58.29 Affineness of complement of ramification locus#

Tag 0ECB, a lemma

Tag 0ECC, a lemma

Tag 0ECD, a theorem

Sources

Section58.30 Specialization maps in the smooth proper case#

Section58.17 Restriction to a closed subscheme #

Section58.18 Pushouts and fundamental groups #

Section58.19 Finite étale covers of punctured spectra, I #

Section58.20 Purity in local case, I #

Section58.21 Purity of branch locus #

Section58.22 Finite étale covers of punctured spectra, II #

Section58.23 Finite étale covers of punctured spectra, III #

Section58.24 Finite étale covers of punctured spectra, IV #

Section58.25 Purity in local case, II #

Section58.26 Purity in local case, III #

Section58.27 Lefschetz for the fundamental group #

Section58.28 Purity of ramification locus #

Section58.29 Affineness of complement of ramification locus #

Section58.30 Specialization maps in the smooth proper case #

Section58.31 Tame ramification #

Section58.32 Tricks in positive characteristic #