41 Étale Morphisms of Schemes

Chapter 41 of the Stacks Project, Étale Morphisms of Schemes, Tag 024J: the 19 sections of its 21 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 66 tags are carried by 131 declarations of the repository (all in StacksFrontier) and 22 registered declarations.

Section41.3 Unramified morphisms#

Section 41.3 of the Stacks Project, Tag 024L. 6 tags here are carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 024M, a definition

Tag 024M in the Stacks Project.

RingHom.IsUnramifiedLocalHom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/LocalHom.lean, line 58.

A local homomorphism f : A → B of local rings is an unramified homomorphism of local rings if 𝔪_A B = 𝔪_B, the residue field κ(𝔪_B) is a finite separable extension of κ(𝔪_A), and B is essentially of finite type over A.

structure IsUnramifiedLocalHom (f : A →+* B) [IsLocalHom f] : Prop

RingHom.isUnramifiedLocalHom_algebraMap_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/LocalHom.lean, line 98. The attribute's comment: “Equivalently, A → B is formally unramified and essentially of finite type.”.

The structure map of a local algebra B over A is an unramified homomorphism of local rings if and only if B is formally unramified and essentially of finite type over A.

theorem isUnramifiedLocalHom_algebraMap_iff :
    (algebraMap A B).IsUnramifiedLocalHom ↔
      Algebra.FormallyUnramified A B ∧ Algebra.EssFiniteType A B

RingHom.isUnramifiedLocalHom_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/LocalHom.lean, line 114. The attribute's comment: “Equivalently, f is formally unramified and essentially of finite type.”.

A local homomorphism of local rings is an unramified homomorphism of local rings if and only if it is formally unramified and essentially of finite type.

theorem isUnramifiedLocalHom_iff (f : A →+* B) [IsLocalHom f] :
    f.IsUnramifiedLocalHom ↔ f.FormallyUnramified ∧ f.EssFiniteType
Tag 039G, a lemma

Tag 039G in the Stacks Project.

Algebra.exists_unramified_away_iff_isUnramifiedLocalHom_algebraMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Unramified/LocalHomAtPrime.lean, line 67. The attribute's comment: “Without the Noetherian hypothesis on A, which is used in the source only to make Definition 024M applicable to A_p → B_q; RingHom.IsUnramifiedLocalHom is defined for all local rings. See the module docstring.”.

Stacks 039G. Let A → B be of finite type and let q be a prime of B lying over the prime p of A. Then A → B is unramified at q (there is g ∉ q with A → B_g unramified) if and only if A_p → B_q is an unramified homomorphism of local rings. The source assumes A Noetherian, which is not needed.

theorem exists_unramified_away_iff_isUnramifiedLocalHom_algebraMap {A B : Type*} [CommRing A]
    [CommRing B] [Algebra A B] [Algebra.FiniteType A B] (p : Ideal A) [p.IsPrime] (q : Ideal B)
    [q.IsPrime] [q.LiesOver p] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
    [Localization.AtPrime.IsLiesOverAlgebra p q] :
    (∃ g ∉ q, Algebra.Unramified A (Localization.Away g)) ↔
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)).IsUnramifiedLocalHom
Tag 039H, a lemma

Tag 039H in the Stacks Project.

RingHom.moduleFinite_adicCompletion_of_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/UnramifiedCompletion.lean, line 65. The attribute's comment: “part (1)”. References: EGA IV (17.4.4), “f) finiteness of B̂/”.

Stacks Project, Tag 039H, part (1). The completion of the target of an unramified local homomorphism of Noetherian local rings is a finite module over the completion of the source.

theorem moduleFinite_adicCompletion_of_formallyUnramified
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B] (f : A →+* B) [IsLocalHom f]
    (hfu : f.FormallyUnramified) (hft : f.EssFiniteType) :
    letI := (adicCompletionMap f (maximalIdeal A) (maximalIdeal B)
      (map_maximalIdeal_le f)).toAlgebra
    Module.Finite (AdicCompletion (maximalIdeal A) A)
      (AdicCompletion (maximalIdeal B) B)

RingHom.surjective_adicCompletionMap_of_bijective_residueFieldMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/UnramifiedCompletion.lean, line 130. The attribute's comment: “part (2)”. References: EGA IV (17.4.4), “f'') when k(x)=k(y)”; SGA 1 I (3.7), “unram ⇒ surj, κ(A)=κ(B)”; SGA 3 XI (1.3), “(ii) completion surj.”.

Stacks Project, Tag 039H, part (2). An unramified local homomorphism inducing a bijection on residue fields induces a surjection on completions.

theorem surjective_adicCompletionMap_of_bijective_residueFieldMap
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B] (f : A →+* B) [IsLocalHom f]
    (hfu : f.FormallyUnramified) (hft : f.EssFiniteType)
    (hκ : Function.Bijective (ResidueField.map f)) :
    Function.Surjective
      (adicCompletionMap f (maximalIdeal A) (maximalIdeal B) (map_maximalIdeal_le f))

RingHom.surjective_adicCompletionMap_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/UnramifiedCompletion.lean, line 192. The attribute's comment: “part (3)”. References: EGA IV (17.4.4), “f'') k sep closed”; EGA IV (17.6.3), “partial”; SGA 1 I (3.7), “unram ⇒ surj, κ sep cl”.

Stacks Project, Tag 039H, part (3). An unramified local homomorphism whose source has separably closed residue field induces a surjection on completions.

theorem surjective_adicCompletionMap_of_isSepClosed
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B] (f : A →+* B) [IsLocalHom f]
    (hfu : f.FormallyUnramified) (hft : f.EssFiniteType)
    [IsSepClosed (ResidueField A)] :
    Function.Surjective
      (adicCompletionMap f (maximalIdeal A) (maximalIdeal B) (map_maximalIdeal_le f))

RingHom.unramified_iff_uniformizer_and_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/UnramifiedCompletion.lean, line 210. The attribute's comment: “part (4)”.

Stacks Project, Tag 039H, part (4). A local homomorphism of complete discrete valuation rings is unramified exactly when it carries a uniformizer to a uniformizer, its residue field extension is finite and separable, and it is essentially of finite type.

theorem unramified_iff_uniformizer_and_residueField
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsDomain A] [IsDomain B]
    [IsDiscreteValuationRing A] [IsDiscreteValuationRing B]
    [IsAdicComplete (maximalIdeal A) A] [IsAdicComplete (maximalIdeal B) B]
    (f : A →+* B) [IsLocalHom f] (ϖ : A) (hϖ : Irreducible ϖ) :
    letI := f.toAlgebra
    (Algebra.FormallyUnramified A B ∧ Algebra.EssFiniteType A B) ↔
      (Irreducible (f ϖ) ∧ Module.Finite (ResidueField A) (ResidueField B) ∧
        Algebra.IsSeparable (ResidueField A) (ResidueField B) ∧ Algebra.EssFiniteType A B)
Tag 039I, a lemma

Tag 039I in the Stacks Project.

RingHom.formallyUnramified_iff_formallyUnramified_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/CompletionCriteria.lean, line 235. The attribute's comment: “parts (1) and (2)”. References: EGA IV (17.4.4), “f')”.

Stacks Project, Tag 039I, parts (1) and (2). An essentially finite type local homomorphism of Noetherian local rings is formally unramified if and only if the induced homomorphism of completions is.

theorem formallyUnramified_iff_formallyUnramified_adicCompletion
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B] (f : A →+* B) [IsLocalHom f] (hft : f.EssFiniteType) :
    letI := f.toAlgebra
    Algebra.FormallyUnramified A B ↔
      (letI := (adicCompletionMap f (maximalIdeal A) (maximalIdeal B)
        (map_maximalIdeal_le f)).toAlgebra
       Algebra.FormallyUnramified
         (AdicCompletion (maximalIdeal A) A) (AdicCompletion (maximalIdeal B) B))

RingHom.formallyUnramified_adicCompletion_iff_unramified_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/CompletionCriteria.lean, line 293. The attribute's comment: “parts (2) and (3)”.

Stacks Project, Tag 039I, parts (2) and (3). For the completion of an essentially finite type local homomorphism of Noetherian local rings, formal unramifiedness and unramifiedness agree.

theorem formallyUnramified_adicCompletion_iff_unramified_adicCompletion
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B] (f : A →+* B) [IsLocalHom f] (hft : f.EssFiniteType) :
    letI := (adicCompletionMap f (maximalIdeal A) (maximalIdeal B)
      (map_maximalIdeal_le f)).toAlgebra
    Algebra.FormallyUnramified
        (AdicCompletion (maximalIdeal A) A) (AdicCompletion (maximalIdeal B) B) ↔
      Algebra.Unramified
        (AdicCompletion (maximalIdeal A) A) (AdicCompletion (maximalIdeal B) B)
Tag 024N, a definition

Tag 024N in the Stacks Project.

AlgebraicGeometry.StalkwiseUnramifiedAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Unramified.lean, line 45. The attribute's comment: “part (1)”.

A locally finite type morphism to a locally Noetherian scheme is unramified at x if its map on local rings at x is unramified.

abbrev StalkwiseUnramifiedAt {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian Y]
    [LocallyOfFiniteType f] (x : X) : Prop

AlgebraicGeometry.StalkwiseUnramified, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Unramified.lean, line 53. The attribute's comment: “part (2)”.

A locally finite type morphism to a locally Noetherian scheme is unramified if it is unramified at every point of its source.

class StalkwiseUnramified {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian Y]
    [LocallyOfFiniteType f] : Prop
Tag 039J, a lemma

Tag 039J in the Stacks Project.

AlgebraicGeometry.unramifiedAt_iff_morphisms_unramifiedAt, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Unramified.lean, line 85.

For a locally finite type morphism to a locally Noetherian scheme, the stalk-theoretic definition of unramifiedness at a point agrees with the affine-neighbourhood definition.

lemma unramifiedAt_iff_morphisms_unramifiedAt
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian Y]
    [LocallyOfFiniteType f] (x : X) :
    StalkwiseUnramifiedAt f x ↔ UnramifiedAt f x
Sources
LeanRingHom.IsUnramifiedLocalHom · RingHom.isUnramifiedLocalHom_algebraMap_iff · RingHom.isUnramifiedLocalHom_iff · Algebra.exists_unramified_away_iff_isUnramifiedLocalHom_algebraMap · RingHom.moduleFinite_adicCompletion_of_formallyUnramified · RingHom.surjective_adicCompletionMap_of_bijective_residueFieldMap · RingHom.surjective_adicCompletionMap_of_isSepClosed · RingHom.unramified_iff_uniformizer_and_residueField

Section41.4 Three other characterizations of unramified morphisms#

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

Tag 024P, a theorem

Tag 024P in the Stacks Project.

AlgebraicGeometry.stalkwiseUnramifiedAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/UnramifiedCharacterizations.lean, line 123. The attribute's comment: “equivalence of conditions (1), (2) and (4)”. References: EGA IV (17.4.2), “Y loc. Noetherian, at x”; EGA IV (17.4.1), “Y loc. Noeth.; a),b),c)”.

Stacks Project, Tag 024P. Let Y be a locally Noetherian scheme, f : X ⟶ Y a morphism locally of finite type and x a point of X. Then f is unramified at x if and only if the stalk at x of the sheaf of relative differentials of f vanishes, and if and only if the diagonal Δ_{X/Y} is a local isomorphism at x.

theorem stalkwiseUnramifiedAt_tfae (f : X ⟶ Y) [IsLocallyNoetherian Y] [LocallyOfFiniteType f]
    (x : X) :
    List.TFAE [
      StalkwiseUnramifiedAt f x,
      Subsingleton ((Scheme.Hom.relativeDifferentials f).presheaf.stalk x),
      ∃ U : X.Opens, x ∈ U ∧ IsOpenImmersion (U.ι ≫ pullback.diagonal f)]

AlgebraicGeometry.stalkwiseUnramifiedAt_iff_hasDifferentialPresentationAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/UnramifiedDifferentialPresentation.lean, line 252. The attribute's comment: “equivalence of conditions (1) and (3)”.

Stacks Project, Tag 024P, condition (3). For a morphism locally of finite type to a locally Noetherian scheme, unramifiedness at x is equivalent to the existence of a local closed immersion into an affine space over an open of the target whose defining ideal has generating differentials at the image of x.

theorem stalkwiseUnramifiedAt_iff_hasDifferentialPresentationAt (f : X ⟶ Y)
    [IsLocallyNoetherian Y] [LocallyOfFiniteType f] (x : X) :
    StalkwiseUnramifiedAt f x ↔ HasDifferentialPresentationAt f x

AlgebraicGeometry.stalkwiseUnramifiedAt_tfae₄, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/UnramifiedDifferentialPresentation.lean, line 275. The attribute's comment: “equivalence of conditions (1), (2), (3) and (4)”.

Stacks Project, Tag 024P. Let Y be a locally Noetherian scheme, f : X ⟶ Y a morphism locally of finite type and x a point of X. The following are equivalent: f is unramified at x; the stalk at x of the sheaf of relative differentials of f vanishes; f restricts near x to a closed immersion into an affine space over an open of Y whose defining ideal has generating differentials at the image of x; and the diagonal Δ_{X/Y} is a local isomorphism at x.

theorem stalkwiseUnramifiedAt_tfae₄ (f : X ⟶ Y) [IsLocallyNoetherian Y] [LocallyOfFiniteType f]
    (x : X) :
    List.TFAE [
      StalkwiseUnramifiedAt f x,
      Subsingleton ((Scheme.Hom.relativeDifferentials f).presheaf.stalk x),
      HasDifferentialPresentationAt f x,
      ∃ U : X.Opens, x ∈ U ∧ IsOpenImmersion (U.ι ≫ pullback.diagonal f)]
Sources
LeanAlgebraicGeometry.stalkwiseUnramifiedAt_tfae · AlgebraicGeometry.stalkwiseUnramifiedAt_iff_hasDifferentialPresentationAt · AlgebraicGeometry.stalkwiseUnramifiedAt_tfae₄

Section41.5 The functorial characterization of unramified morphisms#

Section 41.5 of the Stacks Project, Tag 024Q. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 024R, a theorem

Tag 024R in the Stacks Project.

AlgebraicGeometry.unramified_iff_injective_hom_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FunctorialUnramified.lean, line 73.

Stacks 024R. Let f : X ⟶ S be a morphism of schemes with S locally Noetherian and f locally of finite type. Then f is unramified if and only if it is formally unramified in the functorial sense: for every affine S-scheme T and every subscheme T₀ of T defined by a square-zero ideal, the natural map Hom_S(T, X) → Hom_S(T₀, X) is injective.

public theorem unramified_iff_injective_hom_restriction {X S : Scheme.{u}}
    [IsLocallyNoetherian S] (f : X ⟶ S) [LocallyOfFiniteType f] :
    Unramified f ↔
      ∀ (T T₀ : Over S) (_ : IsAffine T.left) (i : T₀ ⟶ T),
        Stacks.Thickenings.IsFirstOrderThickening i.left →
          Function.Injective fun g : T ⟶ Over.mk f => i ≫ g
Sources
LeanAlgebraicGeometry.unramified_iff_injective_hom_restriction

Section41.6 Topological properties of unramified morphisms#

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

Tag 024T, a proposition

Tag 024T in the Stacks Project.

AlgebraicGeometry.Unramified.section_isOpenImmersion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/UnramifiedTopological/Sections.lean, line 57. The attribute's comment: “part (1)”.

A section of an unramified morphism is an open immersion.

public lemma section_isOpenImmersion {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Unramified f] (s : Y ⟶ X) (hs : s ≫ f = 𝟙 Y) :
    IsOpenImmersion s

AlgebraicGeometry.Unramified.section_isOpenImmersion_and_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/UnramifiedTopological/Sections.lean, line 81. The attribute's comment: “part (3)”. References: EGA IV (17.9.3), “more general”; SGA 3 VIB (5.6.3), “(i) ⇒ (ii), special case”.

A section of an unramified separated morphism is both an open immersion and a closed immersion.

public theorem section_isOpenImmersion_and_isClosedImmersion {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Unramified f] [IsSeparated f] (s : Y ⟶ X) (hs : s ≫ f = 𝟙 Y) :
    IsOpenImmersion s ∧ IsClosedImmersion s

AlgebraicGeometry.Unramified.isClopen_range_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/UnramifiedTopological/Sections.lean, line 88. The attribute's comment: “part (3), the image”.

The image of a section of an unramified separated morphism is open and closed.

public theorem isClopen_range_section {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Unramified f] [IsSeparated f] (s : Y ⟶ X) (hs : s ≫ f = 𝟙 Y) :
    IsClopen (Set.range s)

AlgebraicGeometry.isOpenImmersion_of_isSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Sections.lean, line 85. The attribute's comment: “part (1): a section of an unramified morphism is an open immersion”.

Stacks Project, Tag 024T, part (1). A section of an unramified morphism is an open immersion.

theorem isOpenImmersion_of_isSection (hs : s ≫ g = 𝟙 S) [Unramified g] :
    IsOpenImmersion s

AlgebraicGeometry.isClosedImmersion_of_isSection_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Sections.lean, line 98. The attribute's comment: “part (2): a section of a separated morphism is a closed immersion”. References: EGA I (5.4.6); SGA 3 VIB (5.6.3), “(i) ⇒ (ii)”.

Stacks Project, Tag 024T, part (2). A section of a separated morphism is a closed immersion.

theorem isClosedImmersion_of_isSection_of_isSeparated (hs : s ≫ g = 𝟙 S) [IsSeparated g] :
    IsClosedImmersion s

AlgebraicGeometry.isClopen_range_of_isSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Sections.lean, line 106. The attribute's comment: “part (3): a section of an unramified separated morphism is open and closed”.

Stacks Project, Tag 024T, part (3). A section of an unramified separated morphism is open and closed: its image is an open and closed subset of the source.

theorem isClopen_range_of_isSection (hs : s ≫ g = 𝟙 S) [Unramified g] [IsSeparated g] :
    IsClopen (Set.range s.base)

Stacks.AlgebraicGeometry.RelativeProjSeparated.isClosedImmersion_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeProjSeparated/Basic.lean, line 108. The attribute's comment: “part (2)”. References: EGA I (5.4.4), “special case”; EGA I (5.4.6); EGA IV (16.2.3), “special case”; SGA 3 II (4.11.4), “more general”; SGA 3 VIB (5.1), “more general”; SGA 3 VIB (5.6.3), “(i) ⇒ (ii)”.

A section of a separated morphism of schemes is a closed immersion.

public theorem isClosedImmersion_of_section {X Y : Scheme.{u}} (f : X ⟶ Y) [IsSeparated f]
    (σ : Y ⟶ X) (hσ : σ ≫ f = 𝟙 Y) : IsClosedImmersion σ
Tag 024U, a theorem

Tag 024U in the Stacks Project.

AlgebraicGeometry.Unramified.section_isIso_onto_connectedComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/UnramifiedTopological/Sections.lean, line 125. The attribute's comment: “sections are component isomorphisms”. References: EGA IV (17.4.9), “section is comp. iso”; EGA IV (17.9.4), “iso onto conn. component”; SGA 1 I (5.3), “section iso onto comp”.

A section of a separated unramified morphism onto a connected target is an isomorphism onto a connected component of its source.

public theorem section_isIso_onto_connectedComponent {X Y : Scheme.{u}}
    [ConnectedSpace Y] (f : X ⟶ Y) [Unramified f] [IsSeparated f]
    (s : Y ⟶ X) (hs : s ≫ f = 𝟙 Y) :
    ∃ (U : X.Opens) (sU : Y ⟶ U.toScheme),
      (∃ x : X, (U : Set X) = connectedComponent x) ∧ IsIso sU ∧ sU ≫ U.ι = s

AlgebraicGeometry.Unramified.sections_equiv_connectedComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/UnramifiedTopological/Sections.lean, line 172. The attribute's comment: “bijective correspondence”. References: EGA IV (17.9.4), “bijection g ↦ g(Y)”; EGA IV (17.4.9), “bijection g↦g(Y)”; SGA 1 I (5.3), “bijection with comps”.

Sections correspond to the connected components on which the morphism is an isomorphism; the component corresponding to a section is exactly its image.

public theorem sections_equiv_connectedComponents {X Y : Scheme.{u}}
    [ConnectedSpace Y] (f : X ⟶ Y) [Unramified f] [IsSeparated f] :
    ∃ e : {s : Y ⟶ X // s ≫ f = 𝟙 Y} ≃
      {U : X.Opens // (∃ x : X, (U : Set X) = connectedComponent x) ∧ IsIso (U.ι ≫ f)},
      ∀ s, ((e s).1 : Set X) = Set.range (fun y : Y => s.1 y)

AlgebraicGeometry.Unramified.section_eq_of_common_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/UnramifiedTopological/Sections.lean, line 226. The attribute's comment: “uniqueness through a point”. References: EGA IV (17.4.9), “"In particular" clause”; EGA IV (17.9.4), “injectivity of g↦g(Y)”; SGA 1 I (5.3), “determined by one point”.

At most one section of a separated unramified morphism passes through a given point of its source.

public theorem section_eq_of_common_point {X Y : Scheme.{u}}
    [ConnectedSpace Y] (f : X ⟶ Y) [Unramified f] [IsSeparated f]
    (s t : Y ⟶ X) (hs : s ≫ f = 𝟙 Y) (ht : t ≫ f = 𝟙 Y)
    (x : X) (y z : Y) (hsy : s y = x) (htz : t z = x) : s = t
Tag 024V, a proposition

Tag 024V in the Stacks Project.

AlgebraicGeometry.Unramified.eq_of_residueFieldMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/UnramifiedTopological/Sections.lean, line 249. References: SGA 1 I (5.4).

Two morphisms from a connected scheme to a separated unramified scheme over a base are equal if they induce the same point and the same residue-field map there.

public theorem eq_of_residueFieldMap_eq {S X Y : Scheme.{u}} (π : X ⟶ S)
    [Unramified π] [IsSeparated π] [ConnectedSpace Y]
    (f g : Y ⟶ X) (hover : f ≫ π = g ≫ π) (y : Y) (hy : f y = g y)
    (hκ : f.residueFieldMap y = (X.residueFieldCongr hy).hom ≫ g.residueFieldMap y) :
    f = g
Tag 0AKI, a lemma

Tag 0AKI in the Stacks Project.

AlgebraicGeometry.Unramified.finite_morphisms_over_of_unramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/UnramifiedTopological/Finiteness.lean, line 123.

There are finitely many morphisms over a Noetherian base from a Noetherian scheme to a quasi-compact unramified scheme.

public theorem finite_morphisms_over_of_unramified {S X Y : Scheme.{u}}
    (π : X ⟶ S) (g : Y ⟶ S) [IsNoetherian S] [IsNoetherian Y]
    [QuasiCompact π] [Unramified π] :
    Set.Finite {f : Y ⟶ X | f ≫ π = g}
Sources
LeanAlgebraicGeometry.Unramified.section_isOpenImmersion · AlgebraicGeometry.Unramified.section_isOpenImmersion_and_isClosedImmersion · AlgebraicGeometry.Unramified.isClopen_range_section · AlgebraicGeometry.isOpenImmersion_of_isSection · AlgebraicGeometry.isClosedImmersion_of_isSection_of_isSeparated · AlgebraicGeometry.isClopen_range_of_isSection · Stacks.AlgebraicGeometry.RelativeProjSeparated.isClosedImmersion_of_section · AlgebraicGeometry.Unramified.section_isIso_onto_connectedComponent

Section41.7 Universally injective, unramified morphisms#

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

Tag 05VH, a lemma

Tag 05VH in the Stacks Project.

AlgebraicGeometry.universallyInjective_unramified_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/UniversallyInjectiveUnramified/Basic.lean, line 87. References: EGA IV (17.2.6); EGA IV (8.11.5.1), “loc. finite type case”.

The equivalent characterizations of an unramified universally injective morphism of schemes.

public theorem universallyInjective_unramified_tfae {X S : Scheme.{u}} (f : X ⟶ S) :
    List.TFAE
      [ Unramified f ∧ Mono f,
        Unramified f ∧ UniversallyInjective f,
        LocallyOfFiniteType f ∧ Mono f,
        UniversallyInjective f ∧
          (LocallyOfFiniteType f ∧ FormallyUnramified f),
        LocallyOfFiniteType f ∧
          ∀ s : S, IsEmpty (f.fiber s) ∨ IsIso (f.fiberToSpecResidueField s) ]
Tag 04XV, a lemma

Tag 04XV in the Stacks Project.

AlgebraicGeometry.closedImmersion_conditions_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/UniversallyInjectiveUnramified/ClosedImmersion.lean, line 60. The attribute's comment: “(2) <=> (3) <=> (4) <=> (5) <=> (6) <=> (7)”. References: EGA IV (18.12.6), “b) <=> c)”; EGA IV (8.11.5), “b) <=> c)”.

The six equivalent characterizations of a proper monomorphism, hence of a closed immersion, in parts (2) through (7).

public theorem closedImmersion_conditions_tfae {X S : Scheme.{u}} (f : X ⟶ S) :
    List.TFAE
      [ IsProper f ∧ Mono f,
        IsProper f ∧ (Unramified f ∧ UniversallyInjective f),
        UniversallyClosed f ∧ (Unramified f ∧ Mono f),
        UniversallyClosed f ∧ (Unramified f ∧ UniversallyInjective f),
        UniversallyClosed f ∧ (LocallyOfFiniteType f ∧ Mono f),
        UniversallyClosed f ∧
          (UniversallyInjective f ∧ (LocallyOfFiniteType f ∧ FormallyUnramified f)) ]
Tag 04DG, a lemma

Tag 04DG in the Stacks Project.

AlgebraicGeometry.exists_open_restrict_isClosedImmersion_of_finite_unramified_fiber_eq_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/UniversallyInjectiveUnramified/FiniteUnramified.lean, line 147.

A finite unramified morphism with a singleton fibre and purely inseparable residue-field extension is a closed immersion over some neighbourhood of the point in the target.

public theorem exists_open_restrict_isClosedImmersion_of_finite_unramified_fiber_eq_singleton
    {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f] [Unramified f]
    (s : S) (x : X) (hfiber : f ⁻¹' {s} = {x})
    (hpure :
      let hxs : f x = s := by
        have : x ∈ f ⁻¹' {s} := by simp [hfiber]
        simpa only [Set.mem_preimage, Set.mem_singleton_iff] using this
      letI := ((S.residueFieldCongr hxs).inv ≫ f.residueFieldMap x).hom.toAlgebra
      IsPurelyInseparable (S.residueField s) (X.residueField x)) :
    ∃ U : S.Opens, s ∈ U ∧ IsClosedImmersion (f ∣_ U)
Sources
LeanAlgebraicGeometry.universallyInjective_unramified_tfae · AlgebraicGeometry.closedImmersion_conditions_tfae · AlgebraicGeometry.exists_open_restrict_isClosedImmersion_of_finite_unramified_fiber_eq_singleton

Section41.8 Examples of unramified morphisms#

Section 41.8 of the Stacks Project, Tag 024W. 3 tags here are carried by 23 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 024X, an example

Tag 024X in the Stacks Project.

AlgebraicGeometry.isAffine_of_unramified_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Examples/OverField.lean, line 119. The attribute's comment: “affineness”. References: EGA IV (17.15.11), “affineness in c)”.

A quasi-compact unramified scheme over a field is affine.

public theorem isAffine_of_unramified_quasiCompact
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [StalkwiseUnramified f] [QuasiCompact f] : IsAffine X

AlgebraicGeometry.unramified_quasiCompact_iff_iso_finite_coproduct_spectra_finite_separable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Examples/OverField.lean, line 130. The attribute's comment: “finite separable classification”.

A morphism to the spectrum of a field is quasi-compact and unramified exactly when its source is a finite disjoint union of spectra of finite separable field extensions, compatibly with the map to the base field.

public theorem unramified_quasiCompact_iff_iso_finite_coproduct_spectra_finite_separable
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) :
    ((∃ h : LocallyOfFiniteType f, letI := h; StalkwiseUnramified f) ∧ QuasiCompact f) ↔
      ∃ (I : Type u) (_ : Finite I) (K : I → Type u) (_ : ∀ i, Field (K i))
        (_ : ∀ i, Algebra k (K i)) (_ : ∀ i, Module.Finite k (K i))
        (_ : ∀ i, Algebra.IsSeparable k (K i))
        (e : X ≅ ∐ fun i ↦ Spec (.of (K i))),
        e.hom ≫ Sigma.desc (fun i ↦ Spec.map (CommRingCat.ofHom (algebraMap k (K i)))) = f

AlgebraicGeometry.exists_iso_spec_finite_separable_of_connected_unramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Examples/OverField.lean, line 155. The attribute's comment: “connected case”. References: EGA IV (17.15.11), “connected X, b) => c)”.

A connected unramified scheme over a field is the spectrum of one finite separable field extension, over the base field.

public theorem exists_iso_spec_finite_separable_of_connected_unramified
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [StalkwiseUnramified f] [ConnectedSpace X] :
    ∃ (K : Type u) (_ : Field K) (_ : Algebra k K) (_ : Module.Finite k K)
      (_ : Algebra.IsSeparable k K) (e : X ≅ Spec (.of K)),
      e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k K)) = f

AlgebraicGeometry.etale_iff_unramified_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Examples/OverField.lean, line 196. The attribute's comment: “étale iff unramified”. References: EGA IV (17.15.11), “a) <=> b)”.

Over a field, a morphism is étale exactly when it is locally of finite type and unramified.

public theorem etale_iff_unramified_over_field
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) :
    Etale f ↔ ∃ h : LocallyOfFiniteType f, letI := h; StalkwiseUnramified f
Tag 024Y, an example

Tag 024Y in the Stacks Project.

AlgebraicGeometry.FullRankJacobianSituation.unramifiedAt_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/SquareJacobian.lean, line 268. The attribute's comment: “unramified_point”.

A polynomial quotient whose Jacobian has full rank at a prime is unramified over the base at the corresponding point of its zero scheme.

public theorem unramifiedAt_over (S : FullRankJacobianSituation R n m) :
    UnramifiedAt S.over S.point

AlgebraicGeometry.FullRankJacobianSituation.numVariables_le_numEquations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/SquareJacobian.lean, line 318. The attribute's comment: “enough_equations”.

A full-rank Jacobian needs at least as many equations as variables.

public theorem numVariables_le_numEquations (S : FullRankJacobianSituation R n m) : n ≤ m

AlgebraicGeometry.FullRankJacobianSituation.etaleAt_over_of_square, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/SquareJacobian.lean, line 325. The attribute's comment: “square_etale”.

A polynomial quotient with a square, full-rank Jacobian at a prime is étale over the base at the corresponding point.

public theorem etaleAt_over_of_square (S : FullRankJacobianSituation R n m) (h : m = n) :
    EtaleAt S.over S.point

AlgebraicGeometry.FullRankJacobianSituation.isFlatAt_over_of_square, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/SquareJacobian.lean, line 361. The attribute's comment: “square_flat”.

A square system of equations whose Jacobian has full rank at a prime defines a morphism flat at the corresponding point of its zero scheme.

public theorem isFlatAt_over_of_square (S : FullRankJacobianSituation R n n) :
    IsFlatAt S.over.toLRSHom.toShHom S.point

AlgebraicGeometry.FullRankJacobianSystem.numVariables_le_numEquations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Examples/JacobianCriterion.lean, line 62. The attribute's comment: “enough_equations”.

A full-rank Jacobian needs at least as many equations as variables.

public theorem numVariables_le_numEquations (S : FullRankJacobianSystem R n m) : n ≤ m

AlgebraicGeometry.FullRankJacobianSystem.unramifiedAt_of_jacobian_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Examples/JacobianCriterion.lean, line 138. The attribute's comment: “unramified_point”.

Stacks Project, Tag 024Y. Full column rank of the Jacobian at a prime makes the corresponding point of the zero scheme unramified over the base.

public theorem unramifiedAt_of_jacobian_rank (S : FullRankJacobianSystem R n m) :
    UnramifiedAt S.over S.point

AlgebraicGeometry.FullRankJacobianSystem.etaleAt_of_square_jacobian_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Examples/JacobianCriterion.lean, line 161. The attribute's comment: “square_etale”.

Stacks Project, Tag 024Y. A polynomial quotient with a square Jacobian of full rank at a prime is étale over the base at the corresponding point.

public theorem etaleAt_of_square_jacobian_rank (S : FullRankJacobianSystem R n m) (h : m = n) :
    EtaleAt S.over S.point

AlgebraicGeometry.FullRankJacobianSystem.flatAt_of_square_jacobian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/Examples/JacobianCriterion.lean, line 181. The attribute's comment: “square_flat”.

Stacks Project, Tag 024Y. A polynomial quotient with a square Jacobian of full rank at a prime is flat over the base at the corresponding point.

public theorem flatAt_of_square_jacobian (S : FullRankJacobianSystem R n n) :
    IsFlatAt S.over.toLRSHom.toShHom S.point
Tag 024Z, an example

Tag 024Z in the Stacks Project.

AlgebraicGeometry.unramifiedAt_iff_ramificationIdx_eq_one_and_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/NumberFields.lean, line 112. The attribute's comment: “agreement_of_unramifiedness”.

Stacks Project, Tag 024Z. At a nonzero prime of the larger ring of integers, scheme-theoretic unramifiedness is equivalent to ramification index one together with separability of the residue extension.

theorem unramifiedAt_iff_ramificationIdx_eq_one_and_isSeparable
    (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
    (q : PrimeSpectrum (RingOfIntegers L)) (hq : q.asIdeal ≠ ⊥) :
    letI : Module.Finite (RingOfIntegers K) (RingOfIntegers L) :=
      IsIntegralClosure.finite (RingOfIntegers K) K L (RingOfIntegers L)
    letI : IsFinite (ringOfIntegersSpecMap K L) := (IsFinite.SpecMap_iff _).2
      (IsIntegralClosure.finite (RingOfIntegers K) K L (RingOfIntegers L))
    letI : LocallyOfFiniteType (ringOfIntegersSpecMap K L) := inferInstance
    StalkwiseUnramifiedAt (ringOfIntegersSpecMap K L) q ↔
      (letI := Localization.AtPrime.algebraOfLiesOver
          (q.asIdeal.under (RingOfIntegers K)) q.asIdeal
       Ideal.ramificationIdx q.asIdeal (RingOfIntegers K) = 1 ∧
        Algebra.IsSeparable (q.asIdeal.under (RingOfIntegers K)).ResidueField
          q.asIdeal.ResidueField)

AlgebraicGeometry.unramifiedAt_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/NumberFields.lean, line 141. The attribute's comment: “agreement_of_unramifiedness”.

Stacks Project, Tag 024Z. The morphism on spectra of rings of integers is unramified at the generic point.

theorem unramifiedAt_genericPoint
    (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] :
    letI : Module.Finite (RingOfIntegers K) (RingOfIntegers L) :=
      IsIntegralClosure.finite (RingOfIntegers K) K L (RingOfIntegers L)
    letI : IsFinite (ringOfIntegersSpecMap K L) := (IsFinite.SpecMap_iff _).2
      (IsIntegralClosure.finite (RingOfIntegers K) K L (RingOfIntegers L))
    letI : LocallyOfFiniteType (ringOfIntegersSpecMap K L) := inferInstance
    StalkwiseUnramifiedAt (ringOfIntegersSpecMap K L)
      (⟨⊥, inferInstance⟩ : PrimeSpectrum (RingOfIntegers L))

AlgebraicGeometry.flat_ringOfIntegersSpecMap, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/NumberFieldsDifferent.lean, line 95. The attribute's comment: “the morphism Spec(O_L) -> Spec(O_K) is flat (on all of Spec(O_L), so in particular on X)”.

The morphism on spectra of rings of integers is flat.

instance flat_ringOfIntegersSpecMap : Flat (ringOfIntegersSpecMap K L)

AlgebraicGeometry.stalkwiseUnramifiedAt_ringOfIntegersSpecMap_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/NumberFieldsDifferent.lean, line 104. The attribute's comment: “the points where f is unramified in our sense are the points where f is unramified in the conventional sense, at every point of Spec(O_L)”.

The points of Spec(𝒪_L) where f : Spec(𝒪_L) → Spec(𝒪_K) is unramified in the sense of schemes are the points where it is unramified in the conventional sense: the generic point, and the nonzero primes with ramification index one and separable residue field extension.

theorem stalkwiseUnramifiedAt_ringOfIntegersSpecMap_iff (q : PrimeSpectrum (𝓞 L)) :
    StalkwiseUnramifiedAt (ringOfIntegersSpecMap K L) q ↔
      (q.asIdeal ≠ ⊥ →
        (letI := Localization.AtPrime.algebraOfLiesOver (q.asIdeal.under (𝓞 K)) q.asIdeal
         Ideal.ramificationIdx q.asIdeal (𝓞 K) = 1 ∧
          Algebra.IsSeparable (q.asIdeal.under (𝓞 K)).ResidueField q.asIdeal.ResidueField))

AlgebraicGeometry.zeroLocus_differentIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/NumberFieldsDifferent.lean, line 176. The attribute's comment: “in the conventional sense, the locus of ramification in Spec(O_L) is the vanishing set of the different”.

In the conventional sense, the locus of ramification in Spec(𝒪_L) is the vanishing set of the different: a point of Spec(𝒪_L) lies in the vanishing set of the different exactly when it is a nonzero prime whose ramification index is not one or whose residue field extension is not separable.

theorem zeroLocus_differentIdeal :
    zeroLocus (differentIdeal (𝓞 K) (𝓞 L) : Set (𝓞 L)) =
      {q | q.asIdeal ≠ ⊥ ∧
        ¬ (letI := Localization.AtPrime.algebraOfLiesOver (q.asIdeal.under (𝓞 K)) q.asIdeal
           Ideal.ramificationIdx q.asIdeal (𝓞 K) = 1 ∧
            Algebra.IsSeparable (q.asIdeal.under (𝓞 K)).ResidueField
              q.asIdeal.ResidueField)}

AlgebraicGeometry.algebraDiscriminantIdeal_ringOfIntegers_eq_relNorm_differentIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/NumberFieldsDifferent.lean, line 202. The attribute's comment: “the discriminant is an ideal in O_K, namely it is the norm of the different”.

The discriminant of L/K, an ideal of 𝒪_K — the discriminant ideal of the finite locally free algebra 𝒪_L over 𝒪_K, the zeroth Fitting ideal of the cokernel of its trace pairing — is the norm of the different.

theorem algebraDiscriminantIdeal_ringOfIntegers_eq_relNorm_differentIdeal :
    Stacks.Discriminant.algebraDiscriminantIdeal (𝓞 K) (𝓞 L) =
      Ideal.relNorm (𝓞 K) (differentIdeal (𝓞 K) (𝓞 L))

AlgebraicGeometry.zeroLocus_algebraDiscriminantIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/NumberFieldsDifferent.lean, line 293. The attribute's comment: “the vanishing set of the discriminant is precisely the set of points of Spec(O_K) which ramify in L”.

The vanishing set of the discriminant is precisely the set of points of Spec(𝒪_K) which ramify in L: the primes of 𝒪_K lying under a nonzero prime of 𝒪_L whose ramification index is not one or whose residue field extension is not separable.

theorem zeroLocus_algebraDiscriminantIdeal :
    zeroLocus (Stacks.Discriminant.algebraDiscriminantIdeal (𝓞 K) (𝓞 L) : Set (𝓞 K)) =
      {p | ∃ q : PrimeSpectrum (𝓞 L), comap (algebraMap (𝓞 K) (𝓞 L)) q = p ∧
        q.asIdeal ≠ ⊥ ∧
        ¬ (letI := Localization.AtPrime.algebraOfLiesOver (q.asIdeal.under (𝓞 K)) q.asIdeal
           Ideal.ramificationIdx q.asIdeal (𝓞 K) = 1 ∧
            Algebra.IsSeparable (q.asIdeal.under (𝓞 K)).ResidueField
              q.asIdeal.ResidueField)}

AlgebraicGeometry.stalkwiseUnramified_flat_and_etale_differentOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/NumberFieldsDifferent.lean, line 318. The attribute's comment: “the morphism X -> Spec(O_K) is unramified, flat, and hence etale”.

Denote by X the complement of the closed subset defined by the different in Spec(𝒪_L). The morphism X → Spec(𝒪_K) is unramified; it is furthermore flat, and hence it is actually étale.

theorem stalkwiseUnramified_flat_and_etale_differentOpen :
    StalkwiseUnramified ((differentOpen K L).ι ≫ ringOfIntegersSpecMap K L) ∧
      Flat ((differentOpen K L).ι ≫ ringOfIntegersSpecMap K L) ∧
        Etale ((differentOpen K L).ι ≫ ringOfIntegersSpecMap K L)

AlgebraicGeometry.isFinite_and_etale_morphismRestrict_discriminantOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/NumberFieldsDifferent.lean, line 449. The attribute's comment: “if L/K is finite Galois, X is the preimage of Y and X -> Y is finite etale (and surjective): a finite etale covering”.

If L/K is finite Galois and Y is the complement of the closed subset defined by the discriminant in Spec(𝒪_K), then the preimage of Y is the complement X of the closed subset defined by the different in Spec(𝒪_L), and X → Y is a finite étale morphism, which is moreover surjective: a finite étale covering.

theorem isFinite_and_etale_morphismRestrict_discriminantOpen [IsGalois K L] :
    ringOfIntegersSpecMap K L ⁻¹ᵁ discriminantOpen K L = differentOpen K L ∧
      IsFinite (ringOfIntegersSpecMap K L ∣_ discriminantOpen K L) ∧
        Etale (ringOfIntegersSpecMap K L ∣_ discriminantOpen K L) ∧
          Surjective (ringOfIntegersSpecMap K L ∣_ discriminantOpen K L)

NumberField.differentIdeal_eq_annihilator_kaehlerDifferential_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/NumberTheory/DifferentAnnihilatorGeneral.lean, line 261. The attribute's comment: “the different is the annihilator of the module of differentials”.

The different of an extension of number rings is the annihilator of the module of differentials. For an arbitrary extension of number fields L/K,

differentIdeal 𝒪_K 𝒪_L = Module.annihilator 𝒪_L Ω[𝒪_L⁄𝒪_K].

theorem differentIdeal_eq_annihilator_kaehlerDifferential_general :
    differentIdeal (𝓞 K) (𝓞 L) = Module.annihilator (𝓞 L) Ω[(𝓞 L)⁄(𝓞 K)]

RingHom.Flat.of_injective_of_isDiscreteValuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/DiscreteValuationRing/FlatExtension.lean, line 45. The attribute's comment: “any local homomorphism of discrete valuation rings is flat, in the corrected form for injective local homomorphisms (extensions of discrete valuation rings), proved here for any injective homomorphism from a discrete valuation ring to a domain”. References: EGA 0 (6.3.4), “last assertion, A a DVR”; SGA 6 X (7.15), “special case”.

Stacks Project, Tag 024Z. An injective ring homomorphism from a discrete valuation ring to a domain is flat. In particular any extension of discrete valuation rings — an injective local homomorphism of discrete valuation rings — is flat.

theorem RingHom.Flat.of_injective_of_isDiscreteValuationRing {R S : Type*} [CommRing R]
    [IsDomain R] [IsDiscreteValuationRing R] [CommRing S] [IsDomain S] (f : R →+* S)
    (hf : Function.Injective f) : f.Flat

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.isAffine_of_unramified_quasiCompact · AlgebraicGeometry.unramified_quasiCompact_iff_iso_finite_coproduct_spectra_finite_separable · AlgebraicGeometry.exists_iso_spec_finite_separable_of_connected_unramified · AlgebraicGeometry.etale_iff_unramified_over_field · AlgebraicGeometry.FullRankJacobianSituation.unramifiedAt_over · AlgebraicGeometry.FullRankJacobianSituation.numVariables_le_numEquations · AlgebraicGeometry.FullRankJacobianSituation.etaleAt_over_of_square · AlgebraicGeometry.FullRankJacobianSituation.isFlatAt_over_of_square

Section41.9 Flat morphisms#

Section 41.9 of the Stacks Project, Tag 0250. 3 tags here are carried by 1 declaration of the repository (in StacksFrontier) and 9 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0251, a definition

Tag 0251 in the Stacks Project.

Declarations registered for the tag:

Tag 0252, a theorem

Tag 0252 in the Stacks Project.

Module.flat_quotient_smul_of_isSMulRegular_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/FlatQuotient.lean, line 48.

Stacks Project, Tag 0252. A finite module flat over the base remains flat after quotienting by an element that acts injectively on its closed fibre.

theorem flat_quotient_smul_of_isSMulRegular_maximalIdeal
    {R S M : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
    [Algebra R S] [IsLocalHom (algebraMap R S)] [IsNoetherianRing S]
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Module.Finite S M] [Module.Flat R M] {f : S}
    (hf : IsSMulRegular
      (M ⧸ (Ideal.map (algebraMap R S) (maximalIdeal R) • (⊤ : Submodule S M))) f) :
    Module.Flat R (M ⧸ (Ideal.span {f} • (⊤ : Submodule S M)))
Tag 0253, a definition

Tag 0253 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanModule.Flat · Module.Flat.iff_rTensor_exact · Module.FaithfullyFlat · Module.FaithfullyFlat.iff_zero_iff_rTensor_zero · RingHom.Flat · RingHom.FaithfullyFlat · Module.flat_quotient_smul_of_isSMulRegular_maximalIdeal · AlgebraicGeometry.IsFlatOverAt

Section41.10 Topological properties of flat morphisms#

Section 41.10 of the Stacks Project, Tag 0254. 3 tags here are carried by 1 declaration of the repository (in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0255, a theorem

Tag 0255 in the Stacks Project.

AlgebraicGeometry.isOpen_setOf_isFlatAt_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/FlatLocusOpenness.lean, line 52. The attribute's comment: “flat locus of the morphism”. References: EGA IV (11.1.1), “F = O_X case”; EGA IV (11.1.6), “M = C = B case”; EGA IV (11.3.1), “Noetherian, F = O_X”; SGA 1 IV (6.10), “F = O_X case”.

Stacks Project, Tag 0255. The flat locus of a morphism locally of finite type to a locally Noetherian scheme is open.

theorem isOpen_setOf_isFlatAt_of_isLocallyNoetherian
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian Y] [LocallyOfFiniteType f] :
    IsOpen {x : X | IsFlatAt f.toLRSHom.toShHom x}

Declarations registered for the tag:

Tag 039K, a theorem

Tag 039K in the Stacks Project.

Declarations registered for the tag:

  • AlgebraicGeometry.UniversallyOpen.of_flat registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch41.lean, line 20 (StacksFrontier): “flat and locally of finite presentation implies universally open”. References: EGA IV (1.10.4), “b) ⇒ a), special case”; EGA IV (11.3.1), “special case”; EGA IV (14.4.10), “special case”; EGA IV (15.2.1); EGA IV (15.2.4), “(ii), special case”; EGA IV (18.2.7), “partial”; EGA IV (2.4.6); EGA IV (2.4.7), “more general”; EGA IV (4.4.1), “special case”; SGA 1 IV (6.6), “F = O_X”; SGA 1 VIII (4.9), “more general”; SGA 3 V (10.1.1), “more general”; SGA 3 V (4.1.1), “flat and fp implies open”; SGA 3 VIA (2.5.4), “Final implication”; SGA 3 VIB (3.11), “more general”; SGA 3 VIB (4.3); SGA 3 VIB (7.5), “f|_V is an open morphism”; SGA 3 X (5.4), “partial”; SGA 3 XVI (2.1), “more general”; SGA 6 VIII (1.3), “more general”.
  • AlgebraicGeometry.LocallyOfFinitePresentation.iff_locallyOfFiniteType registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch41.lean, line 22 (StacksFrontier): “over a locally Noetherian base, locally of finite type is locally of finite presentation”. References: SGA 1 IX (4.7), “partial”; SGA 1 IX (4.10), “more general”; SGA 1 IX (4.12), “partial”; SGA 3 V (6.1), “partial”.
Tag 0256, a theorem

Tag 0256 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.isOpen_setOf_isFlatAt_of_isLocallyNoetherian · AlgebraicGeometry.isOpen_setOf_coherent_flatOverAt · AlgebraicGeometry.UniversallyOpen.of_flat · AlgebraicGeometry.LocallyOfFinitePresentation.iff_locallyOfFiniteType · AlgebraicGeometry.Flat.isQuotientMap_of_surjective

Section41.11 Étale morphisms#

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

Tag 0258, a definition

Tag 0258 in the Stacks Project.

RingHom.IsEtaleLocalHom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/EtaleLocalHom.lean, line 57. References: SGA 1 I (4.1), “special case”; SGA 1 III (1.2), “partial”.

A local homomorphism between Noetherian local rings is étale if it is flat, formally unramified, and essentially of finite type.

abbrev IsEtaleLocalHom {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B] [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f] : Prop
Tag 039L, a lemma

Tag 039L in the Stacks Project.

Algebra.isEtaleAt_iff_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/EtaleLocalHom.lean, line 104.

A finite type algebra over a Noetherian ring is étale at a prime if and only if the induced map between the local rings at the corresponding primes is an étale local homomorphism.

theorem isEtaleAt_iff_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [Algebra A B] [Algebra.FiniteType A B] [IsNoetherianRing A]
    (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p] :
    Algebra.IsEtaleAt A q ↔
      letI : IsNoetherianRing B := Algebra.FiniteType.isNoetherianRing A B
      letI : IsNoetherianRing (Localization.AtPrime p) :=
        IsLocalization.isNoetherianRing p.primeCompl _ inferInstance
      letI : IsNoetherianRing (Localization.AtPrime q) :=
        IsLocalization.isNoetherianRing q.primeCompl _ inferInstance
      RingHom.IsEtaleLocalHom
        (Localization.localRingHom p q (algebraMap A B) Ideal.LiesOver.over)
Tag 039M, a lemma

Tag 039M in the Stacks Project.

RingHom.isEtaleLocalHom_iff_isEtaleLocalHom_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/CompletionCriteria.lean, line 318. The attribute's comment: “parts (1) and (2)”. References: EGA IV (17.6.3), “a) <=> e)”; SGA 1 I (4.2), “special case”.

Stacks Project, Tag 039M, parts (1) and (2). An essentially finite type local homomorphism of Noetherian local rings is étale if and only if the induced homomorphism of completions is étale.

theorem isEtaleLocalHom_iff_isEtaleLocalHom_adicCompletion
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B] (f : A →+* B) [IsLocalHom f] (hft : f.EssFiniteType) :
    letI := AdicCompletion.isLocalHom_adicCompletionMap f
    IsEtaleLocalHom f ↔
      IsEtaleLocalHom
        (adicCompletionMap f (maximalIdeal A) (maximalIdeal B) (map_maximalIdeal_le f))

RingHom.isEtaleLocalHom_adicCompletion_iff_etale_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/CompletionCriteria.lean, line 349. The attribute's comment: “parts (2) and (3)”.

Stacks Project, Tag 039M, parts (2) and (3). For the completion of an essentially finite type local homomorphism of Noetherian local rings, étaleness as a homomorphism of local rings agrees with étaleness as an algebra.

theorem isEtaleLocalHom_adicCompletion_iff_etale_adicCompletion
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B] (f : A →+* B) [IsLocalHom f] (hft : f.EssFiniteType) :
    letI := AdicCompletion.isLocalHom_adicCompletionMap f
    IsEtaleLocalHom
        (adicCompletionMap f (maximalIdeal A) (maximalIdeal B) (map_maximalIdeal_le f)) ↔
      (letI := (adicCompletionMap f (maximalIdeal A) (maximalIdeal B)
        (map_maximalIdeal_le f)).toAlgebra
       Algebra.Etale
         (AdicCompletion (maximalIdeal A) A) (AdicCompletion (maximalIdeal B) B))

RingHom.exists_linearEquiv_fin_adicCompletion_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/CompletionCriteria.lean, line 391. The attribute's comment: “finite free conclusion”. References: EGA IV (17.6.3), “e') freeness”.

Stacks Project, Tag 039M. The completion of the target of an étale local homomorphism of Noetherian local rings is a finite free module of positive rank over the completion of the source.

theorem exists_linearEquiv_fin_adicCompletion_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B] (f : A →+* B) [IsLocalHom f] (hf : IsEtaleLocalHom f) :
    letI := (adicCompletionMap f (maximalIdeal A) (maximalIdeal B)
      (map_maximalIdeal_le f)).toAlgebra
    ∃ n : ℕ, 0 < n ∧ Nonempty
      (AdicCompletion (maximalIdeal B) B ≃ₗ[AdicCompletion (maximalIdeal A) A]
        (Fin n → AdicCompletion (maximalIdeal A) A))
Tag 0259, a definition

Tag 0259 in the Stacks Project.

AlgebraicGeometry.IsEtaleAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/EtaleAt.lean, line 57. The attribute's comment: “étale at a point”. References: SGA 1 I (4.1), “loc. Noetherian base”.

A locally finite type morphism over a locally Noetherian scheme is étale at x when the induced local homomorphism on stalks is étale.

abbrev IsEtaleAt {X Y : Scheme.{u}} (f : X ⟶ Y) (x : X)
    [LocallyOfFiniteType f] [IsLocallyNoetherian Y] : Prop

AlgebraicGeometry.etale_iff_forall_isEtaleAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/EtaleAt.lean, line 72. The attribute's comment: “global étaleness is étaleness at every point”. References: SGA 1 I (4.1), “loc. Noetherian base”.

Over a locally Noetherian scheme, a locally finite type morphism is étale if and only if it is étale at each point in the local-ring sense.

theorem etale_iff_forall_isEtaleAt {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] [IsLocallyNoetherian Y] :
    AlgebraicGeometry.Etale f ↔ ∀ x : X, IsEtaleAt f x

Declarations registered for the tag:

Tag 039N, a lemma

Tag 039N in the Stacks Project.

AlgebraicGeometry.isEtaleAt_iff_etaleAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/EtaleAt.lean, line 129.

Stacks Project, Tag 039N. For a morphism locally of finite type over a locally Noetherian scheme, étaleness of the induced map of local rings at x is equivalent to étaleness on suitable affine neighbourhoods of x and its image.

theorem isEtaleAt_iff_etaleAt {X Y : Scheme.{u}} (f : X ⟶ Y) (x : X)
    [LocallyOfFiniteType f] [IsLocallyNoetherian Y] :
    IsEtaleAt f x ↔ EtaleAt f x
Sources
LeanRingHom.IsEtaleLocalHom · Algebra.isEtaleAt_iff_isEtaleLocalHom · RingHom.isEtaleLocalHom_iff_isEtaleLocalHom_adicCompletion · RingHom.isEtaleLocalHom_adicCompletion_iff_etale_adicCompletion · RingHom.exists_linearEquiv_fin_adicCompletion_of_isEtaleLocalHom · AlgebraicGeometry.IsEtaleAt · AlgebraicGeometry.etale_iff_forall_isEtaleAt · AlgebraicGeometry.Etale

Section41.12 The structure theorem#

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

Tag 025B, a theorem

Tag 025B in the Stacks Project.

Algebra.exists_standardEtalePair_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/StructureTheorem.lean, line 42.

If A → B is an étale local homomorphism of Noetherian local rings, then B is isomorphic as an A-algebra to the localization of a standard étale A-algebra at a prime.

theorem exists_standardEtalePair_localization
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B] [Algebra A B]
    [IsLocalHom (algebraMap A B)]
    (h : RingHom.IsEtaleLocalHom (algebraMap A B)) :
    ∃ (P : StandardEtalePair A) (q : Ideal P.Ring) (hq : q.IsPrime),
      letI := hq
      Nonempty (B ≃ₐ[A] Localization.AtPrime q)
Tag 039O, a theorem

Tag 039O in the Stacks Project.

Algebra.exists_standardEtalePair_localization_surjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/UnramifiedStructure.lean, line 33. References: SGA 1 I (7.7), “unramified ⇒ quotient”.

An unramified local algebra over a local ring is a quotient of the localization at a prime of a standard étale algebra.

theorem exists_standardEtalePair_localization_surjection
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
    [IsLocalRing A] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
    [Algebra.EssFiniteType A B] [Algebra.FormallyUnramified A B] :
    ∃ (P : StandardEtalePair A) (q : Ideal P.Ring) (hq : q.IsPrime),
      letI := hq
      ∃ φ : Localization.AtPrime q →ₐ[A] B, Function.Surjective φ
Tag 025C, a theorem

Tag 025C in the Stacks Project.

AlgebraicGeometry.exists_isOpenImmersion_specMap_derivativePair_of_etaleAt, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/LocalStructure.lean, line 383. The attribute's comment: “the étale local structure theorem”.

Stacks Project, Tag 0CBJ, étale case. At a point where the morphism is étale, the immersion of AlgebraicGeometry.exists_isImmersion_specMap_derivativePair_of_unramifiedAt may be chosen to be an open immersion.

public lemma exists_isOpenImmersion_specMap_derivativePair_of_etaleAt
    {X S : Scheme.{u}} (f : X ⟶ S) (x : X) (V : S.Opens)
    (hV : IsAffineOpen V) (hxV : f x ∈ V) (hf : EtaleAt f x) :
    ∃ (U : X.Opens) (_ : IsAffineOpen U) (_ : x ∈ U)
      (hUV : U ≤ f ⁻¹ᵁ V) (P : StandardEtalePair Γ(S, V)),
      P.g = P.f.derivative ∧
        ∃ (j : U.toScheme ⟶ Spec (CommRingCat.of P.Ring)),
          IsOpenImmersion j ∧
            j ≫ Spec.map (CommRingCat.ofHom (aeval P.X).toRingHom) ≫
                Spec.map (CommRingCat.ofHom (Polynomial.C : Γ(S, V) →+* Γ(S, V)[X])) =
              f.resLE V U hUV ≫ hV.isoSpec.hom
Sources
LeanAlgebra.exists_standardEtalePair_localization · Algebra.exists_standardEtalePair_localization_surjection · AlgebraicGeometry.exists_isOpenImmersion_specMap_derivativePair_of_etaleAt

Section41.13 Étale and smooth morphisms#

Section 41.13 of the Stacks Project, Tag 039P. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 039Q, a theorem

Tag 039Q in the Stacks Project.

AlgebraicGeometry.exists_affine_open_etale_affineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Smooth/EtaleAffineSpace.lean, line 100. The attribute's comment: “smooth at a point is étale-locally an affine space”. References: EGA IV (17.11.4), “smooth ⇒ étale/A^d”.

A morphism of schemes which is smooth at a point is, over any affine open neighbourhood V of the image of that point, étale-locally an affine space over V: there is an affine open neighbourhood U of the point mapping into V and an étale morphism from U to an affine space over V commuting with the morphism.

theorem exists_affine_open_etale_affineSpace {X Y : Scheme.{u}} (f : X ⟶ Y) (x : X)
    (V : Y.Opens) (hV : IsAffineOpen V) (hxV : x ∈ f ⁻¹ᵁ V)
    (hf : InfinitesimalLifting.SmoothAt f x) :
    ∃ (d : ℕ) (U : X.Opens) (_ : IsAffineOpen U) (_ : x ∈ U) (hUV : U ≤ f ⁻¹ᵁ V)
      (π : U.toScheme ⟶ AffineSpace (ULift.{u} (Fin d)) V.toScheme),
      Etale π ∧
        π ≫ (AffineSpace (ULift.{u} (Fin d)) V.toScheme ↘ V.toScheme) =
          f.resLE V U hUV
Sources
LeanAlgebraicGeometry.exists_affine_open_etale_affineSpace

Section41.14 Topological properties of étale morphisms#

Section 41.14 of the Stacks Project, Tag 025F. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 025G, a theorem

Tag 025G in the Stacks Project.

Stacks.Etale.tfae_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvariance/MorphismDescent.lean, line 94. References: EGA IV (17.9.1); SGA 1 I (5.1), “more general”; SGA 3 X (3.7), “partial”; SGA 3 XXII (5.4.10), “Footnote (36)”; SGA 7 IX (3.1.3), “more general”.

Stacks Project, Tag 025G. For a morphism of schemes, being an open immersion, being universally injective and étale, and being a flat monomorphism locally of finite presentation are all equivalent.

theorem tfae_isOpenImmersion {A B : Scheme.{u}} (g : A ⟶ B) :
    List.TFAE [IsOpenImmersion g, UniversallyInjective g ∧ Etale g,
      Flat g ∧ Mono g ∧ LocallyOfFinitePresentation g]

Declarations registered for the tag:

Tag 04DH, a lemma

Tag 04DH in the Stacks Project.

AlgebraicGeometry.exists_open_restrict_isIso_of_finite_etale_fiber_eq_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/SingletonFibre.lean, line 166.

Stacks Project, Tag 04DH. A finite étale morphism with a singleton fibre and purely inseparable residue-field extension is an isomorphism over some open neighbourhood of the point in the target.

theorem exists_open_restrict_isIso_of_finite_etale_fiber_eq_singleton
    {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f] [Etale f]
    (s : S) (x : X) (hfiber : f ⁻¹' {s} = {x})
    (hpure :
      let hxs : f x = s := by
        have : x ∈ f ⁻¹' {s} := by simp [hfiber]
        simpa only [Set.mem_preimage, Set.mem_singleton_iff] using this
      letI := ((S.residueFieldCongr hxs).inv ≫ f.residueFieldMap x).hom.toAlgebra
      IsPurelyInseparable (S.residueField s) (X.residueField x)) :
    ∃ U : S.Opens, s ∈ U ∧ IsIso (f ∣_ U)
Tag 0EBS, a lemma

Tag 0EBS in the Stacks Project.

AlgebraicGeometry.isIso_relativeFrobenius_of_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/TopologicalProperties/RelativeFrobenius.lean, line 34. References: SGA 4½ Fonctions L (3.4); SGA 5 XV (1.Proposition2), “Clause c) 2)”.

The relative Frobenius of an étale scheme is an isomorphism.

public instance isIso_relativeFrobenius_of_etale (X : Scheme.{u}) (p : ℕ)
    [Fact p.Prime] (hX : IsInCharacteristic X p) (U : Over X) [Etale U.hom] :
    IsIso (relativeFrobenius X p hX U)
Sources
LeanStacks.Etale.tfae_isOpenImmersion · AlgebraicGeometry.IsOpenImmersion.mono · AlgebraicGeometry.instUniversallyInjectiveOfMonoScheme · AlgebraicGeometry.Etale.instOfIsOpenImmersion · AlgebraicGeometry.Flat.instOfIsOpenImmersion · AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion · AlgebraicGeometry.isOpenImmersion_of_etale_universallyInjective · AlgebraicGeometry.IsOpenImmersion.of_flat_of_mono

Section41.15 Topological invariance of the étale topology#

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

Tag 025H, a theorem

Tag 025H in the Stacks Project.

Stacks.Etale.bijective_pullbackHom_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/EtaleDescentIntegral.lean, line 345. References: EGA IV (18.1.3); EGA IV (18.1.2), “fully faithful”; SGA 1 I (5.5); SGA 1 IX (1.7), “fully faithful”.

Base change along a closed immersion with the same underlying space induces a bijection on morphisms into an étale scheme.

theorem bijective_pullbackHom_of_etale
    {S S₀ : Scheme.{u}} (i : S₀ ⟶ S) [IsClosedImmersion i]
    (hi : Function.Surjective i.base) (X Y : Over S) [Etale X.hom] :
    Function.Bijective (fun f : Y ⟶ X => (Over.pullback i).map f)
Tag 039R, a theorem

Tag 039R in the Stacks Project.

Stacks.Etale.etalePullback_isEquivalence_of_surjective_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TopologicalInvarianceThickening.lean, line 99. References: EGA IV (18.1.2); SGA 3 X (2.0); SGA 1 IX (1.7); SGA 1 I (5.5), “special case”.

Une équivalence remarquable de catégories. Let S₀ ⊆ S be a closed subscheme with the same underlying topological space. Base change along the closed immersion is an equivalence from the category of schemes étale over S to the category of schemes étale over S₀.

theorem etalePullback_isEquivalence_of_surjective_isClosedImmersion (i : S₀ ⟶ S)
    [IsClosedImmersion i] (hi : Function.Surjective i.base) :
    letI : MorphismProperty.HasPullbacksAlong
        (@Etale : MorphismProperty Scheme.{u}) i := ⟨fun _ _ ↦ inferInstance⟩
    letI : MorphismProperty.IsStableUnderBaseChangeAlong
        (@Etale : MorphismProperty Scheme.{u}) i :=
      ⟨fun pb hg ↦ MorphismProperty.IsStableUnderBaseChange.of_isPullback pb hg⟩
    (show S.Etale ⥤ S₀.Etale from
      MorphismProperty.Over.pullback
        (@Etale : MorphismProperty Scheme.{u}) ⊤ i).IsEquivalence
Sources
LeanStacks.Etale.bijective_pullbackHom_of_etale · Stacks.Etale.etalePullback_isEquivalence_of_surjective_isClosedImmersion

Section41.16 The functorial characterization#

Section 41.16 of the Stacks Project, Tag 025J. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 025K, a theorem

Tag 025K in the Stacks Project.

AlgebraicGeometry.etale_iff_locallyOfFinitePresentation_and_formallyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/EtaleIffFormallyEtale.lean, line 46. The attribute's comment: “étale iff the unique-lifting property, for a morphism locally of finite”. References: EGA IV (17.3.2), “(ii) etale”; EGA IV (17.6.1), “a) <=> d)”; EGA IV (17.3.1); SGA 3 XI (1.6), “étale case”; SGA 4 VII (1.1), “functorial criterion”; SGA 3 XI (1.1); SGA 4½ Arcata (2.1.1), “more general”.

A morphism of schemes is étale exactly when it is locally of finite presentation and formally étale.

theorem etale_iff_locallyOfFinitePresentation_and_formallyEtale
    {X S : Scheme.{u}} (f : X ⟶ S) :
    Etale f ↔ (LocallyOfFinitePresentation f ∧ FormallyEtale f)
Sources
LeanAlgebraicGeometry.etale_iff_locallyOfFinitePresentation_and_formallyEtale

Section41.17 Étale local structure of unramified morphisms#

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

Tag 04HH, a lemma

Tag 04HH in the Stacks Project.

AlgebraicGeometry.exists_etaleNeighborhood_isClosedImmersion_opens_of_unramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/EtaleLocalStructure/ClosedImmersionOpens.lean, line 126.

Stacks Project, Tag 04HH. After a single étale base change, finitely many distinct points of one fibre at which a morphism of schemes is unramified are covered, in that fibre, by open subschemes which are closed immersions over the new base, pass through the distinguished point, and pairwise avoid one another there.

public theorem exists_etaleNeighborhood_isClosedImmersion_opens_of_unramifiedAt
    {X S : Scheme.{u}} (f : X ⟶ S) (n : ℕ) (x : Fin n → X) (s : S)
    (hx : ∀ i, f (x i) = s) (hx_injective : Function.Injective x)
    (hunramified : ∀ i, UnramifiedAt f (x i)) :
    ∃ (U : EtaleNeighborhood S s) (m : Fin n → ℕ)
      (V : (Σ i, Fin (m i)) → (pullback f U.toBase).Opens),
      (∀ a, IsClosedImmersion ((V a).ι ≫ pullback.snd f U.toBase) ∧
        ∃ y : (pullback f U.toBase : Scheme.{u}),
          y ∈ V a ∧ (pullback.snd f U.toBase) y = U.point) ∧
      (∀ a b, a ≠ b → ∀ y : (pullback f U.toBase : Scheme.{u}),
        y ∈ V a → y ∈ V b → (pullback.snd f U.toBase) y ≠ U.point) ∧
      (∀ (i : Fin n) (y : (pullback f U.toBase : Scheme.{u})),
        (pullback.snd f U.toBase) y = U.point →
        (pullback.fst f U.toBase) y = x i →
        ∃ j : Fin (m i), y ∈ V ⟨i, j⟩)
Tag 04HI, a lemma

Tag 04HI in the Stacks Project.

AlgebraicGeometry.exists_etaleNeighborhood_disjoint_closed_decomposition_of_unramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/EtaleLocalStructure/DisjointDecomposition.lean, line 66.

Stacks Project, Tag 04HI. A separated morphism of schemes which is unramified at finitely many points of one fibre becomes, after a single étale base change around the image point, the disjoint union of finitely many closed subschemes of the new base passing through the distinguished point and a remainder whose distinguished fibre avoids the chosen points. The remainder has empty distinguished fibre when the chosen points exhaust the original fibre.

public theorem exists_etaleNeighborhood_disjoint_closed_decomposition_of_unramifiedAt
    {X S : Scheme.{u}} (f : X ⟶ S) [IsSeparated f] (n : ℕ) (x : Fin n → X) (s : S)
    (hx : ∀ i, f (x i) = s) (hunramified : ∀ i, UnramifiedAt f (x i)) :
    ∃ (U : EtaleNeighborhood S s)
      (W : (pullback f U.toBase).Opens) (m : Fin n → ℕ)
      (V : (Σ i, Fin (m i)) → (pullback f U.toBase).Opens),
      (sSup (Set.range V) ⊔ W = ⊤) ∧
        (Pairwise (Disjoint on V)) ∧
        (∀ a, Disjoint (V a) W) ∧
        (∀ a, IsClosedImmersion ((V a).ι ≫ pullback.snd f U.toBase)) ∧
        (∀ a, ∃ z : (V a).toScheme,
          ((V a).ι ≫ pullback.snd f U.toBase) z = U.point) ∧
        (∀ (z : (W.ι ≫ pullback.snd f U.toBase).fiber U.point) (i : Fin n),
          ((W.ι ≫ pullback.snd f U.toBase).fiberι U.point ≫ W.ι ≫
            pullback.fst f U.toBase) z ≠ x i) ∧
    ((∀ y : X, f y = s → ∃ i, y = x i) →
          IsEmpty ((W.ι ≫ pullback.snd f U.toBase).fiber U.point))
Tag 04HJ, a lemma

Tag 04HJ in the Stacks Project.

AlgebraicGeometry.exists_etaleNeighborhood_disjoint_closed_decomposition_of_finite_unramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/EtaleLocalStructure/DisjointDecomposition.lean, line 271.

Stacks Project, Tag 04HJ. A finite unramified morphism of schemes becomes a finite disjoint union of closed immersions after an étale base change around any chosen point of the target.

public theorem exists_etaleNeighborhood_disjoint_closed_decomposition_of_finite_unramified
    {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f] [Unramified f] (s : S) :
    ∃ (U : EtaleNeighborhood S s) (n : ℕ) (V : Fin n → (pullback f U.toBase).Opens),
      (sSup (Set.range V) = ⊤) ∧
        (Pairwise (Disjoint on V)) ∧
        (∀ j, IsClosedImmersion ((V j).ι ≫ pullback.snd f U.toBase))
Sources
LeanAlgebraicGeometry.exists_etaleNeighborhood_isClosedImmersion_opens_of_unramifiedAt · AlgebraicGeometry.exists_etaleNeighborhood_disjoint_closed_decomposition_of_unramifiedAt · AlgebraicGeometry.exists_etaleNeighborhood_disjoint_closed_decomposition_of_finite_unramified

Section41.18 Étale local structure of étale morphisms#

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

Tag 04HL, a lemma

Tag 04HL in the Stacks Project.

AlgebraicGeometry.exists_etaleNeighborhood_openCopies_cover_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/LocalStructure/OpenCopies.lean, line 134.

Stacks Project, Tag 04HL. A morphism which is étale at finitely many distinct points of one fibre admits, after an étale base change, open subschemes of the base change which map isomorphically onto the new base, meet one another nowhere over the distinguished point, and together contain every point of that fibre lying over one of the given points.

public theorem exists_etaleNeighborhood_openCopies_cover_fibers
    {X S : Scheme.{u}} (f : X ⟶ S) (n : ℕ) (x : Fin n → X) (s : S)
    (hinj : Function.Injective x) (hx : ∀ i, f (x i) = s) (hetale : ∀ i, EtaleAt f (x i)) :
    ∃ (U : EtaleNeighborhood S s) (m : Fin n → ℕ)
      (V : (Σ i, Fin (m i)) → (pullback f U.toBase).Opens),
      (∀ a, IsIso ((V a).ι ≫ pullback.snd f U.toBase)) ∧
      (∀ a b, a ≠ b → ∀ z : (pullback f U.toBase : Scheme.{u}),
        z ∈ (V a).1 → z ∈ (V b).1 → pullback.snd f U.toBase z ≠ U.point) ∧
      (∀ i (z : (pullback f U.toBase : Scheme.{u})),
        pullback.snd f U.toBase z = U.point → pullback.fst f U.toBase z = x i →
          ∃ j : Fin (m i), z ∈ (V ⟨i, j⟩).1)
Tag 04HM, a lemma

Tag 04HM in the Stacks Project.

AlgebraicGeometry.exists_etaleNeighborhood_disjoint_openCopies_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/LocalStructure/DisjointDecomposition.lean, line 406.

Stacks Project, Tag 04HM. After an étale base change, a separated morphism which is étale at finitely many points over one point of the base is the disjoint union of copies of the new base together with a remainder whose distinguished fibre contains none of those points. If the given points exhaust the original fibre, that remaining fibre is empty.

public theorem exists_etaleNeighborhood_disjoint_openCopies_decomposition
    {X S : Scheme.{u}} (f : X ⟶ S) [IsSeparated f] (n : ℕ) (x : Fin n → X) (s : S)
    (hx : ∀ i, f (x i) = s) (hetale : ∀ i, EtaleAt f (x i)) :
    ∃ (U : EtaleNeighborhood S s) (W : (pullback f U.toBase).Opens) (m : Fin n → ℕ)
      (V : (Σ i, Fin (m i)) → (pullback f U.toBase).Opens),
      sSup (Set.range V) ⊔ W = ⊤ ∧ Pairwise (Disjoint on V) ∧ (∀ a, Disjoint (V a) W) ∧
        (∀ a, IsIso ((V a).ι ≫ pullback.snd f U.toBase)) ∧
        (∀ (z : (W.ι ≫ pullback.snd f U.toBase).fiber U.point) (i : Fin n),
          ((W.ι ≫ pullback.snd f U.toBase).fiberι U.point ≫ W.ι ≫
            pullback.fst f U.toBase) z ≠ x i) ∧
        ((∀ y : X, f y = s → ∃ i, y = x i) →
          IsEmpty ((W.ι ≫ pullback.snd f U.toBase).fiber U.point))
Tag 04HN, a lemma

Tag 04HN in the Stacks Project.

Stacks.Etale.exists_etale_pullback_iso_sigma, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteEtaleLocal.lean, line 243.

Let f : X ⟶ S be a finite étale morphism of schemes and let s : S. There is an étale neighbourhood g : U ⟶ S of s, a finite index type ι and an isomorphism X ×_S U ≅ ∐_{i : ι} U over U; that is, X becomes a finite disjoint union of copies of the base, each mapping isomorphically onto it, after an étale base change near s.

theorem exists_etale_pullback_iso_sigma {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f] [Etale f]
    (s : S) :
    ∃ (U : Scheme.{u}) (g : U ⟶ S) (_ : Etale g) (u : U) (_ : g u = s) (ι : Type u)
      (_ : Finite ι) (e : pullback f g ≅ ∐ fun _ : ι ↦ U),
      e.hom ≫ Limits.Sigma.desc (fun _ ↦ 𝟙 U) = pullback.snd f g

Stacks.Etale.exists_etaleCover_pullback_iso_sigma, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FiniteEtaleLocal.lean, line 254. The attribute's comment: “étale covering form”.

A finite étale morphism f : X ⟶ S admits an étale covering 𝒰 of S together with, for each member i, a finite index type ι i and an isomorphism X ×_S 𝒰.X i ≅ ∐_{ι i} 𝒰.X i over 𝒰.X i.

theorem exists_etaleCover_pullback_iso_sigma {X S : Scheme.{u}} (f : X ⟶ S)
    [IsFinite f] [Etale f] :
    ∃ (𝒰 : S.Cover.{u} (Scheme.precoverage @Etale)) (ι : 𝒰.I₀ → Type u)
      (_ : ∀ i, Finite (ι i)) (e : ∀ i, pullback f (𝒰.f i) ≅ ∐ fun _ : ι i ↦ 𝒰.X i),
      ∀ i, (e i).hom ≫ Limits.Sigma.desc (fun _ ↦ 𝟙 (𝒰.X i)) = pullback.snd f (𝒰.f i)

Stacks.Etale.exists_isSplitOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/SplitOver.lean, line 177. The attribute's comment: “sheets over an étale neighbourhood”.

Stacks 04HN, in terms of sheets. Let f : X ⟶ S be finite étale and let q : V ⟶ S be any scheme over S. Every point of V has an étale neighbourhood g : W ⟶ V over which f has sheet data.

public theorem exists_isSplitOver {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f] [Etale f]
    {V : Scheme.{u}} (q : V ⟶ S) (v : V) :
    ∃ (W : Scheme.{u}) (g : W ⟶ V) (_ : Etale g) (w : W) (_ : g w = v),
      Nonempty (IsSplitOver f (g ≫ q))
Sources
LeanAlgebraicGeometry.exists_etaleNeighborhood_openCopies_cover_fibers · AlgebraicGeometry.exists_etaleNeighborhood_disjoint_openCopies_decomposition · Stacks.Etale.exists_etale_pullback_iso_sigma · Stacks.Etale.exists_etaleCover_pullback_iso_sigma · Stacks.Etale.exists_isSplitOver

Section41.19 Permanence properties#

Section 41.19 of the Stacks Project, Tag 025L. 7 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 025L, the section

Tag 025L in the Stacks Project.

RingHom.depth_eq_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 72. The tag is given by the attribute command at StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 90. The attribute's comment: “Proposition 039T of the section: for an étale homomorphism A → B of Noetherian local rings, depth(A) = depth(B).”.

An étale local homomorphism between Noetherian local rings preserves depth.

theorem depth_eq_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    Module.depth A (IsLocalRing.maximalIdeal A) A =
      Module.depth B (IsLocalRing.maximalIdeal B) B

RingHom.isReduced_iff_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 97. The tag is given by the attribute command at StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 115. The attribute's comment: “Proposition 025O of the section: for an étale homomorphism A → B of Noetherian local rings, A is reduced if and only if B is reduced.”. References: SGA 1 I (9.3), “Noetherian case”.

An étale local homomorphism between Noetherian local rings preserves and reflects reducedness.

theorem isReduced_iff_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    IsReduced A ↔ IsReduced B

RingHom.isCohenMacaulayLocalRing_iff_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 153. The tag is given by the attribute command at StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 168. The attribute's comment: “Proposition 025Q of the section: for an étale homomorphism A → B of Noetherian local rings, A is Cohen-Macaulay if and only if B is Cohen-Macaulay.”.

Cohen-Macaulayness is preserved and reflected by an étale local homomorphism of Noetherian local rings.

theorem isCohenMacaulayLocalRing_iff_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    IsCohenMacaulayLocalRing A ↔ IsCohenMacaulayLocalRing B

RingHom.ringKrullDim_eq_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 175. The tag is given by the attribute command at StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 184. The attribute's comment: “Lemma 039S of the section: for an étale homomorphism A → B of Noetherian local rings, dim(A) = dim(B).”. References: EGA IV (6.1.3), “special case”.

An étale homomorphism of Noetherian local rings preserves the Krull dimension: the dimension of the source equals the dimension of the target.

theorem ringKrullDim_eq_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    ringKrullDim A = ringKrullDim B

RingHom.isRegularLocalRing_iff_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/Permanence.lean, line 56. The tag is given by the attribute command at StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/Permanence.lean, line 73. The attribute's comment: “Proposition 025N of the section: for an étale homomorphism A → B of Noetherian local rings, A is regular if and only if B is regular.”. References: SGA 1 I (9.1).

Stacks Project, Tag 025N. An étale local homomorphism between Noetherian local rings preserves and reflects regularity.

theorem isRegularLocalRing_iff_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    IsRegularLocalRing A ↔ IsRegularLocalRing B

RingHom.isNormalDomain_iff_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/Permanence.lean, line 97. The tag is given by the attribute command at StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/Permanence.lean, line 123. The attribute's comment: “Proposition 025P of the section: for an étale homomorphism A → B of Noetherian local rings, A is a normal domain if and only if B is a normal domain.”. References: SGA 1 I (9.5), “(i), Noetherian”.

Stacks Project, Tag 025P. An étale local homomorphism between Noetherian local rings preserves and reflects the property of being a normal domain.

theorem isNormalDomain_iff_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    IsNormalDomain A ↔ IsNormalDomain B
Tag 039S, a lemma

Tag 039S in the Stacks Project.

RingHom.ringKrullDim_eq_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 175. References: EGA IV (6.1.3), “special case”.

An étale homomorphism of Noetherian local rings preserves the Krull dimension: the dimension of the source equals the dimension of the target.

theorem ringKrullDim_eq_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    ringKrullDim A = ringKrullDim B
Tag 039T, a proposition

Tag 039T in the Stacks Project.

RingHom.depth_eq_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 72.

An étale local homomorphism between Noetherian local rings preserves depth.

theorem depth_eq_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    Module.depth A (IsLocalRing.maximalIdeal A) A =
      Module.depth B (IsLocalRing.maximalIdeal B) B
Tag 025Q, a proposition

Tag 025Q in the Stacks Project.

RingHom.isCohenMacaulayLocalRing_iff_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 153.

Cohen-Macaulayness is preserved and reflected by an étale local homomorphism of Noetherian local rings.

theorem isCohenMacaulayLocalRing_iff_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    IsCohenMacaulayLocalRing A ↔ IsCohenMacaulayLocalRing B
Tag 025N, a proposition

Tag 025N in the Stacks Project.

RingHom.isRegularLocalRing_iff_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/Permanence.lean, line 56. References: SGA 1 I (9.1).

Stacks Project, Tag 025N. An étale local homomorphism between Noetherian local rings preserves and reflects regularity.

theorem isRegularLocalRing_iff_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    IsRegularLocalRing A ↔ IsRegularLocalRing B
Tag 025O, a proposition

Tag 025O in the Stacks Project.

RingHom.isReduced_iff_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Permanence.lean, line 97. References: SGA 1 I (9.3), “Noetherian case”.

An étale local homomorphism between Noetherian local rings preserves and reflects reducedness.

theorem isReduced_iff_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    IsReduced A ↔ IsReduced B
Tag 025P, a proposition

Tag 025P in the Stacks Project.

RingHom.isNormalDomain_iff_of_isEtaleLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/Permanence.lean, line 97. References: SGA 1 I (9.5), “(i), Noetherian”.

Stacks Project, Tag 025P. An étale local homomorphism between Noetherian local rings preserves and reflects the property of being a normal domain.

theorem isNormalDomain_iff_of_isEtaleLocalHom
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B]
    [IsLocalRing A] [IsLocalRing B]
    (f : A →+* B) [IsLocalHom f]
    (hf : IsEtaleLocalHom f) :
    IsNormalDomain A ↔ IsNormalDomain B
Sources
LeanRingHom.depth_eq_of_isEtaleLocalHom · RingHom.isReduced_iff_of_isEtaleLocalHom · RingHom.isCohenMacaulayLocalRing_iff_of_isEtaleLocalHom · RingHom.ringKrullDim_eq_of_isEtaleLocalHom · RingHom.isRegularLocalRing_iff_of_isEtaleLocalHom · RingHom.isNormalDomain_iff_of_isEtaleLocalHom

Section41.20 Descending étale morphisms#

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

Tag 0BTI, an equation

Tag 0BTI in the Stacks Project.

AlgebraicGeometry.canonicalDescentData_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Descent.lean, line 91. The attribute's comment: “étale objects”.

The canonical descent datum of an étale scheme over S has an étale underlying scheme over X.

theorem canonicalDescentData_etale (f : X ⟶ S) (U : S.Etale) :
    IsEtaleDescentData f
      ((DescentData.canonicalFunctor f).obj ((Scheme.Etale.forget S).obj U))

AlgebraicGeometry.etaleDescentFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/Descent.lean, line 113. The attribute's comment: “the functor”.

The canonical functor, given by pullback along f, from étale S-schemes to descent data relative to f with étale underlying X-scheme.

def etaleDescentFunctor (f : X ⟶ S) :
    S.Etale ⥤ EtaleDescentData f
Tag 0BTJ, a lemma

Tag 0BTJ in the Stacks Project.

AlgebraicGeometry.etaleDescentFunctor_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/DescentFullyFaithful.lean, line 128.

Pullback to a surjective scheme detects equality of morphisms between étale schemes over the base.

theorem etaleDescentFunctor_faithful (f : X ⟶ S) [Surjective f] :
    (etaleDescentFunctor f).Faithful
Tag 0BTK, a lemma

Tag 0BTK in the Stacks Project.

AlgebraicGeometry.etaleDescentFunctor_fullyFaithful_of_submersive_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/DescentFullyFaithful.lean, line 275. References: SGA 1 IX (3.4), “fully faithful”.

Étale descent is fully faithful when the morphism and all its étale base changes are submersive.

theorem etaleDescentFunctor_fullyFaithful_of_submersive_baseChange (f : X ⟶ S)
    (hf : Topology.IsQuotientMap f)
    (hbase : ∀ {U : Scheme.{u}} (g : U ⟶ S), Etale g →
      Topology.IsQuotientMap (pullback.snd f g)) :
    Nonempty (etaleDescentFunctor f).FullyFaithful
Tag 0BTL, a lemma

Tag 0BTL in the Stacks Project.

AlgebraicGeometry.etaleDescentFunctor_fullyFaithful_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/DescentFullyFaithful.lean, line 508. The attribute's comment: “universally_closed”. References: SGA 1 IX (6.9), “fully faithful half”.

Étale descent along a surjective universally closed morphism is fully faithful.

theorem etaleDescentFunctor_fullyFaithful_of_universallyClosed (f : X ⟶ S) [Surjective f]
    [UniversallyClosed f] : Nonempty (etaleDescentFunctor f).FullyFaithful

AlgebraicGeometry.etaleDescentFunctor_fullyFaithful_of_universallyOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/DescentFullyFaithful.lean, line 518. The attribute's comment: “universally_open”.

Étale descent along a surjective universally open morphism is fully faithful.

theorem etaleDescentFunctor_fullyFaithful_of_universallyOpen (f : X ⟶ S) [Surjective f]
    [UniversallyOpen f] : Nonempty (etaleDescentFunctor f).FullyFaithful

AlgebraicGeometry.etaleDescentFunctor_fullyFaithful_of_quasiCompact_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/DescentFullyFaithful.lean, line 528. The attribute's comment: “quasi_compact_flat”.

Étale descent along a surjective quasi-compact flat morphism is fully faithful.

theorem etaleDescentFunctor_fullyFaithful_of_quasiCompact_of_flat (f : X ⟶ S) [Surjective f]
    [QuasiCompact f] [Flat f] : Nonempty (etaleDescentFunctor f).FullyFaithful
Tag 0BTM, a lemma

Tag 0BTM in the Stacks Project.

AlgebraicGeometry.DescentDatum.isEtaleEffective_of_isOpenCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Scheme/EtaleBaseLocal.lean, line 659. References: SGA 1 IX (4.3), “sufficiency”; SGA 1 VIII (7.3), “partial”.

Effectivity of an étale descent datum is Zariski-local on the base. Let f : X ⟶ S be a morphism of schemes and (V, φ) a descent datum relative to X/S with V ⟶ X étale, and let S = ⋃ Sᵢ be an open covering. Assume that the pullback of (V, φ) to X ×_S Sᵢ / Sᵢ is effective by an étale scheme for every i, that the étale descent functor for X ×_S (Sᵢ ∩ Sⱼ) ⟶ Sᵢ ∩ Sⱼ is fully faithful, and that the étale descent functor for X ×_S (Sᵢ ∩ Sⱼ ∩ Sₖ) ⟶ Sᵢ ∩ Sⱼ ∩ Sₖ is faithful. Then (V, φ) is effective, by a scheme étale over S.

theorem isEtaleEffective_of_isOpenCover {S X : Scheme.{u}} {f : X ⟶ S} (D : DescentDatum f)
    [Etale D.over.hom] {ι : Type v} (U : ι → S.Opens) (hU : ⨆ i, U i = ⊤)
    (hlocal : ∀ i, (D.baseDatum (U i)).IsEtaleEffective)
    (hpair : ∀ i j, (etaleDescentFunctor (pullback.snd f (U i ⊓ U j).ι)).FullyFaithful)
    (htriple : ∀ i j k,
      (etaleDescentFunctor (pullback.snd f (U i ⊓ U j ⊓ U k).ι)).Faithful) :
    D.IsEtaleEffective
Tag 0BTN, a lemma

Tag 0BTN in the Stacks Project.

Stacks.Etale.exists_coprod_isFinite_and_isEmpty_closedFiber, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/DescentEffectivity/HenselianSplitting.lean, line 387.

Stacks Project, Tag 0BTN. A quasi-compact separated étale scheme over a henselian pair, with finite closed fibre, is the disjoint union of a finite scheme over the base and a scheme with empty closed fibre.

lemma exists_coprod_isFinite_and_isEmpty_closedFiber
    (A : Type u) [CommRing A] (I : Ideal A) (hI : HenselianPair A I)
    (U : Scheme.{u}) (f : U ⟶ Spec (.of A))
    [QuasiCompact f] [IsSeparated f] [Etale f]
    [IsFinite (pullback.snd f
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))))] :
    ∃ (Ufin Uaway : Scheme.{u}) (iFin : Ufin ⟶ U) (iAway : Uaway ⟶ U),
      IsIso (coprod.desc iFin iAway) ∧ IsFinite (iFin ≫ f) ∧
        IsEmpty ((pullback (iAway ≫ f)
          (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) : Scheme.{u}))
Tag 0BTP, a proposition

Tag 0BTP in the Stacks Project.

AlgebraicGeometry.fullyFaithful_quasiCompactSeparatedEtaleDescentFunctor_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/IntegralEtaleDescent.lean, line 224. The attribute's comment: “the fully faithful half of the equivalence”.

Stacks Project, Tag 0BTP, the fully faithful half. Let f : X ⟶ S be a surjective integral morphism. The functor of Tag 0BTI, restricted to the schemes quasi-compact, separated and étale over S and to the descent data relative to X/S whose underlying X-scheme is quasi-compact, separated and étale, is fully faithful.

Fullness is Tag 0BTL for a surjective universally closed morphism, which a surjective integral morphism is, and faithfulness is Tag 0BTJ.

theorem fullyFaithful_quasiCompactSeparatedEtaleDescentFunctor_of_isIntegralHom
    (f : X ⟶ S) [Surjective f] [IsIntegralHom f] :
    Nonempty (quasiCompactSeparatedEtaleDescentFunctor f).FullyFaithful

AlgebraicGeometry.isEquivalence_quasiCompactSeparatedEtaleDescentFunctor_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/DescentEffectivity/HenselianCase.lean, line 267. References: SGA 1 IX (4.11), “more general”; SGA 1 IX (4.7).

Stacks, Tag 0BTP. Let f : X ⟶ S be a surjective integral morphism. The functor of Tag 0BTI induces an equivalence between the category of schemes quasi-compact, separated and étale over S and the category of descent data (V, φ) relative to X/S with V quasi-compact, separated and étale over X.

theorem isEquivalence_quasiCompactSeparatedEtaleDescentFunctor_of_isIntegralHom
    {S X : Scheme.{u}} (f : X ⟶ S) [Surjective f] [IsIntegralHom f] :
    (quasiCompactSeparatedEtaleDescentFunctor f).IsEquivalence
Sources
LeanAlgebraicGeometry.canonicalDescentData_etale · AlgebraicGeometry.etaleDescentFunctor · AlgebraicGeometry.etaleDescentFunctor_faithful · AlgebraicGeometry.etaleDescentFunctor_fullyFaithful_of_submersive_baseChange · AlgebraicGeometry.etaleDescentFunctor_fullyFaithful_of_universallyClosed · AlgebraicGeometry.etaleDescentFunctor_fullyFaithful_of_universallyOpen · AlgebraicGeometry.etaleDescentFunctor_fullyFaithful_of_quasiCompact_of_flat · AlgebraicGeometry.DescentDatum.isEtaleEffective_of_isOpenCover

Section41.21 Normal crossings divisors#

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

Tag 0BI9, a definition

Tag 0BI9 in the Stacks Project.

Stacks.Divisors.IsStrictNormalCrossingsDivisor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/NormalCrossings/Defs.lean, line 58. References: SGA 5 I (3.1.5), “a) strict n.c.”.

An effective Cartier divisor locally cut out by a product of a nonempty initial segment of a regular system of parameters.

public abbrev IsStrictNormalCrossingsDivisor {X : Scheme.{u}}
    [IsLocallyNoetherian X] (D : X.IdealSheafData) : Prop
Tag 0BIA, a lemma

Tag 0BIA in the Stacks Project.

Stacks.Divisors.isStrictNormalCrossingsDivisor_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/Components.lean, line 1139.

A locally Noetherian effective Cartier divisor has strict normal crossings if and only if it is reduced and all finite nonempty intersections of its irreducible components are regular of the expected codimension.

public theorem isStrictNormalCrossingsDivisor_iff {X : Scheme.{u}}
    [IsLocallyNoetherian X] (D : X.IdealSheafData)
    (hD : IsEffectiveCartierDivisor D) :
    IsStrictNormalCrossingsDivisor D ↔
      (IsReduced D.subscheme ∧
        (∀ C : irreducibleComponents D.subscheme,
          IsEffectiveCartierDivisor
            (componentIdeal D C)) ∧
        (∀ J : Finset (irreducibleComponents D.subscheme), J.Nonempty →
          AlgebraicGeometry.IsRegular (componentIntersection D J).subscheme ∧
            ∀ C : irreducibleComponents (componentIntersection D J).subscheme,
              codimension (IrreducibleCloseds.closureSingleton
                ((componentIntersection D J).subschemeι C.2.1.genericPoint)) =
                  (J.card : ℕ∞)))
Tag 0CBP, a lemma

Tag 0CBP in the Stacks Project.

Stacks.Divisors.isStrictNormalCrossingsDivisor_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/SmoothPullback.lean, line 295.

Stacks Project, Tag 0CBP. The pullback of a strict normal crossings divisor along a smooth morphism is a strict normal crossings divisor.

theorem isStrictNormalCrossingsDivisor_comap {X Y : Scheme.{u}} [IsLocallyNoetherian X]
    (f : Y ⟶ X) [Smooth f] (D : X.IdealSheafData)
    (hD : IsStrictNormalCrossingsDivisor D) :
    @IsStrictNormalCrossingsDivisor Y (LocallyOfFiniteType.isLocallyNoetherian f)
      (D.comap f)
Tag 0BSF, a definition

Tag 0BSF in the Stacks Project.

Stacks.Divisors.IsNormalCrossingsDivisor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/NormalCrossings/Defs.lean, line 70. References: SGA 1 XIII (2.1.0), “absolute case”; SGA 5 I (3.1.5), “a) normal crossings”.

An effective Cartier divisor which acquires strict normal crossings étale-locally at every point of its support.

public abbrev IsNormalCrossingsDivisor {X : Scheme.{u}}
    [IsLocallyNoetherian X] (D : X.IdealSheafData) : Prop
Tag 0CBQ, a lemma

Tag 0CBQ in the Stacks Project.

Stacks.Divisors.isNormalCrossingsDivisor_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/SmoothPullback.lean, line 319.

Stacks Project, Tag 0CBQ. The pullback of a normal crossings divisor along a smooth morphism is a normal crossings divisor.

theorem isNormalCrossingsDivisor_comap {X Y : Scheme.{u}} [IsLocallyNoetherian X]
    (f : Y ⟶ X) [Smooth f] (D : X.IdealSheafData)
    (hD : IsNormalCrossingsDivisor D) :
    @IsNormalCrossingsDivisor Y (LocallyOfFiniteType.isLocallyNoetherian f) (D.comap f)
Tag 0CBR, a lemma

Tag 0CBR in the Stacks Project.

Stacks.Divisors.isClopen_normalizationDistinctLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationCriterion.lean, line 275. The attribute's comment: “first paragraph of the proof: Z_n is an open and closed subscheme of the fibre power of the normalization. Neither implication of the equivalence is asserted.”.

Z_n is open and closed in the fibre power of the normalization, once the latter is unramified.

public theorem isClopen_normalizationDistinctLocus [Unramified (divisorNormalization D)]
    (n : ℕ) : IsClopen (fibrePowerDistinctLocus (divisorNormalization D) n)

Stacks.Divisors.unramified_normalizationDistinctToAmbient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationCriterion.lean, line 283. The attribute's comment: “first paragraph of the proof: Z_n ⟶ X is unramified. Neither implication of the equivalence is asserted.”.

Once the normalization of D is unramified, Z_n ⟶ X is unramified: it is the composition of an open immersion, an iterated base change of the normalization, and a closed immersion.

public theorem unramified_normalizationDistinctToAmbient
    [Unramified (divisorNormalization D)] (n : ℕ) :
    Unramified (normalizationDistinctToAmbient D n)

Stacks.Divisors.formallyUnramified_normalizationDistinctToAmbient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationCriterion.lean, line 294. The attribute's comment: “first paragraph of the proof: Z_n ⟶ X is formally unramified, so the conormal sheaf 𝒞_n exists. Neither implication of the equivalence is asserted.”.

Once the normalization of D is unramified, Z_n ⟶ X is formally unramified, so that it has a conormal sheaf.

public theorem formallyUnramified_normalizationDistinctToAmbient
    [Unramified (divisorNormalization D)] (n : ℕ) :
    FormallyUnramified (normalizationDistinctToAmbient D n)

Stacks.Divisors.IsNormalizationCrossingsDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationCriterion.lean, line 306. The attribute's comment: “condition (2). Its equivalence with condition (1), Stacks.Divisors.IsNormalCrossingsDivisor, is not asserted.”.

Condition (2) of Tag 0CBR: the closed subscheme cut out by D is reduced, its normalization is unramified, and every Z_n with n ≥ 1 is regular and maps to the ambient scheme by a local complete intersection morphism whose conormal sheaf is locally free of rank n.

public def IsNormalizationCrossingsDivisor : Prop

Stacks.Divisors.isReduced_of_isNormalCrossingsDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationCriterion.lean, line 323. The attribute's comment: “the implication (1) to (2), restricted to its reducedness clause. The remaining clauses of (2) under hypothesis (1), and the converse implication, are not asserted.”.

A normal crossings divisor is reduced, which is the first clause of condition (2) of Tag 0CBR. Étale-locally the divisor has strict normal crossings, hence is reduced by Tag 0BIA, and reducedness descends along the faithfully flat maps that an étale chart induces on stalks of the divisor.

public theorem isReduced_of_isNormalCrossingsDivisor (h : IsNormalCrossingsDivisor D) :
    IsReduced D.subscheme

Stacks.Divisors.isNormal_reducedComponent_of_isStrictNormalCrossingsDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationCriterion.lean, line 420. The attribute's comment: “an input to the implication (1) to (2) in the strict case: an irreducible component of a strict normal crossings divisor, with its reduced induced closed subscheme structure, is normal. Neither implication of the equivalence is asserted.”.

An irreducible component of a strict normal crossings divisor, with its reduced induced closed subscheme structure, is a normal scheme: it is regular by Tag 0BIA, and a regular scheme is normal.

public theorem isNormal_reducedComponent_of_isStrictNormalCrossingsDivisor
    (h : IsStrictNormalCrossingsDivisor D) (C : irreducibleComponents D.subscheme) :
    IsNormal (D.subscheme.reducedComponent C)

Stacks.Divisors.unramified_divisorNormalization_of_isStrictNormalCrossingsDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationCriterion.lean, line 438. The attribute's comment: “the implication (1) to (2) for a strict normal crossings divisor, restricted to the clause that the normalization of the divisor is unramified. The general normal crossings case, the remaining clauses of (2), and the converse implication are not asserted.”.

The normalization of a strict normal crossings divisor is unramified, which is the unramifiedness clause of condition (2) of Tag 0CBR in the strict case. The normalization is the disjoint union of the normalizations of the irreducible components of the divisor, each component is normal, so each of those normalization morphisms is an isomorphism, and what remains is a disjoint union of closed immersions.

public theorem unramified_divisorNormalization_of_isStrictNormalCrossingsDivisor
    (h : IsStrictNormalCrossingsDivisor D) : Unramified (divisorNormalization D)

Stacks.Divisors.isNormalCrossingsDivisor_iff_reduced_unramified_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationEquivalence.lean, line 78.

Let X be a locally Noetherian scheme and let D ⊂ X be a closed subscheme. The following are equivalent:

  1. D is a normal crossings divisor in X;
  2. D is reduced, the normalization ν : D^ν ⟶ D is unramified, and for every n ≥ 1 the scheme Z_n, obtained from the n-fold fibre power of ν over D by deleting the fat diagonal, is regular and the morphism Z_n ⟶ X is a local complete intersection morphism whose conormal sheaf is locally free of rank n.
theorem isNormalCrossingsDivisor_iff_reduced_unramified_normalization {X : Scheme.{u}}
    [IsLocallyNoetherian X] (D : X.IdealSheafData) :
    IsNormalCrossingsDivisor D ↔
      (IsReduced D.subscheme ∧
        ∃ hν : Unramified (divisorNormalization D), ∀ n : ℕ, 1 ≤ n →
          AlgebraicGeometry.IsRegular (normalizationDistinct D n) ∧
            IsLocalCompleteIntersectionMorphism (normalizationDistinctToAmbient D n) ∧
              (letI : Unramified (divisorNormalization D) := hν
               haveI := formallyUnramified_normalizationDistinctToAmbient D n
               SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
                 (Stacks.Thickenings.universalConormalSheaf
                   (normalizationDistinctToAmbient D n)) n))

Stacks.Divisors.isIntegralHom_divisorNormalization, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationFiniteness.lean, line 102. The attribute's comment: “the proof of (2) to (1), first step: the normalization ν : D^ν ⟶ D is integral. Neither implication of the equivalence is asserted.”.

The normalization of the closed subscheme cut out by a divisor on a locally Noetherian scheme is an integral morphism.

public instance isIntegralHom_divisorNormalization : IsIntegralHom (divisorNormalization D)

Stacks.Divisors.isFinite_divisorNormalization, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationFiniteness.lean, line 116. The attribute's comment: “the proof of (2) to (1), first step: an unramified ν is finite, being integral and locally of finite type (Tag 01WJ). Neither implication of the equivalence is asserted.”.

An unramified normalization of the closed subscheme cut out by a divisor on a locally Noetherian scheme is finite: it is integral and, being unramified, locally of finite type.

public instance isFinite_divisorNormalization [Unramified (divisorNormalization D)] :
    IsFinite (divisorNormalization D)

Stacks.Divisors.isFinite_divisorNormalizationToAmbient, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationFiniteness.lean, line 130. The attribute's comment: “the proof of (2) to (1), second step: D^ν ⟶ X is finite. Neither implication of the equivalence is asserted.”.

The morphism D^ν ⟶ X is finite when the normalization of D is unramified: it is the composition of the finite normalization with a closed immersion.

public instance isFinite_divisorNormalizationToAmbient
    [Unramified (divisorNormalization D)] : IsFinite (divisorNormalizationToAmbient D)

Stacks.Divisors.unramified_divisorNormalizationToAmbient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationFiniteness.lean, line 138. The attribute's comment: “the proof of (2) to (1), second step: D^ν ⟶ X is unramified. Neither implication of the equivalence is asserted.”.

The morphism D^ν ⟶ X is unramified when the normalization of D is: it is the composition of the unramified normalization with a closed immersion.

public theorem unramified_divisorNormalizationToAmbient
    [Unramified (divisorNormalization D)] : Unramified (divisorNormalizationToAmbient D)

Stacks.Divisors.exists_etaleNeighborhood_disjoint_closed_decomposition_divisorNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationFiniteness.lean, line 149. The attribute's comment: “the proof of (2) to (1), third step: étale-locally on X the normalization is a finite disjoint union of closed subschemes of the étale neighbourhood (Tag 04HJ). The further shrinking making the chosen point lie on every D_i is not asserted, nor is either implication of the equivalence.”.

Around any point of the ambient scheme the normalization of D becomes, after an étale base change, a finite disjoint union of closed subschemes of the étale neighbourhood: the morphism D^ν ⟶ X is finite and unramified, so Tag 04HJ applies to it.

public theorem exists_etaleNeighborhood_disjoint_closed_decomposition_divisorNormalization
    [Unramified (divisorNormalization D)] (p : X) :
    ∃ (U : EtaleNeighborhood X p) (n : ℕ)
      (V : Fin n → (pullback (divisorNormalizationToAmbient D) U.toBase).Opens),
      sSup (Set.range V) = ⊤ ∧ Pairwise (Disjoint on V) ∧
        ∀ j, IsClosedImmersion
          ((V j).ι ≫ pullback.snd (divisorNormalizationToAmbient D) U.toBase)

Stacks.Divisors.normalizationDistinctOneIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationFiniteness.lean, line 164. The attribute's comment: “the identification Z_1 = D^ν used in the proof of (2) to (1). Neither implication of the equivalence is asserted.”.

The scheme Z_1 is the normalization of D itself: a one-fold fibre power has empty fat diagonal and is the normalization.

public noncomputable def normalizationDistinctOneIso :
    normalizationDistinct D 1 ≅ divisorNormalizationScheme D

Stacks.Divisors.isRegular_divisorNormalizationScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationFiniteness.lean, line 194. The attribute's comment: “the proof of (2) to (1), fourth step, partially: the hypothesis on Z_1 makes D^ν regular. The conclusion that each D_i is an effective Cartier divisor is not asserted.”.

Condition (2) of Tag 0CBR makes the normalization of D a regular scheme: it is the scheme Z_1 of that condition.

public theorem isRegular_divisorNormalizationScheme (h : IsNormalizationCrossingsDivisor D) :
    IsRegular (divisorNormalizationScheme D)

Stacks.Divisors.isLocalCompleteIntersectionMorphism_divisorNormalizationToAmbient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/NormalizationFiniteness.lean, line 210. The attribute's comment: “the proof of (2) to (1), fourth step, partially: the hypothesis on Z_1 makes D^ν ⟶ X a local complete intersection morphism. The conclusion that each D_i is an effective Cartier divisor is not asserted.”.

Condition (2) of Tag 0CBR makes D^ν ⟶ X a local complete intersection morphism: it is the morphism Z_1 ⟶ X of that condition, up to the identification of Z_1 with the normalization.

public theorem isLocalCompleteIntersectionMorphism_divisorNormalizationToAmbient
    (h : IsNormalizationCrossingsDivisor D) :
    IsLocalCompleteIntersectionMorphism (divisorNormalizationToAmbient D)
Tag 0CBS, a lemma

Tag 0CBS in the Stacks Project.

Stacks.Divisors.isStrictNormalCrossingsDivisor_comap_fromSpecStalk_of_isNormalCrossingsDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/StrictHenselization.lean, line 68. The attribute's comment: “(1) ⇒ (2)”.

The strict henselization of a normal crossings divisor has strict normal crossings. For D a normal crossings divisor on a locally Noetherian scheme X and x a point of D, the pullback of D to the spectrum of a strict henselization of 𝒪_{X, x} is a strict normal crossings divisor.

theorem isStrictNormalCrossingsDivisor_comap_fromSpecStalk_of_isNormalCrossingsDivisor
    {X : Scheme.{u}} [IsLocallyNoetherian X] (D : X.IdealSheafData)
    (hD : IsNormalCrossingsDivisor D) (x : X) (hx : ∃ y : D.subscheme, D.subschemeι y = x)
    (L : Type u) [Field L]
    [Algebra (IsLocalRing.ResidueField (X.presheaf.stalk x)) L]
    [IsSepClosure (IsLocalRing.ResidueField (X.presheaf.stalk x)) L]
    (Ash : Type u) [CommRing Ash] [IsLocalRing Ash]
    [Algebra (X.presheaf.stalk x) Ash]
    [IsLocalRing.IsHenselization (X.presheaf.stalk x) L Ash] :
    haveI : IsNoetherianRing Ash :=
      IsLocalRing.isNoetherianRing_of_isHenselization (A := X.presheaf.stalk x) L
    IsStrictNormalCrossingsDivisor (D.comap
      (Spec.map (CommRingCat.ofHom (algebraMap (X.presheaf.stalk x) Ash)) ≫
        X.fromSpecStalk x))

Stacks.Divisors.isStrictNormalCrossingsDivisor_of_exists_regular_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/StrictHenselizationCriterion.lean, line 75. The attribute's comment: “(2) ⇒ (1), the step that upgrades condition (2) to strict normal crossings once each local equation factors into regular factors. The construction of an étale chart on which it does, which is where the J-2 or Nagata hypothesis of the lemma enters, is not asserted.”.

Let D be a closed subscheme of a locally Noetherian scheme X which has strict normal crossings at the strict henselizations, and suppose that at every point p of D the stalk ideal is generated by a product f₁ ⋯ f_k of at least one element with each quotient 𝒪_{X, p} / (fⱼ) a regular local ring. Then D is a strict normal crossings divisor.

In Tag 0CBS the factorization hypothesis is what the J-2 or Nagata assumption produces, by realizing a regular system of parameters of 𝒪^{sh}_{X, p} on an étale neighbourhood and shrinking it so that each of the resulting divisors is regular.

theorem isStrictNormalCrossingsDivisor_of_exists_regular_factorization {X : Scheme.{u}}
    [IsLocallyNoetherian X] (D : X.IdealSheafData)
    (hD : IsStrictNormalCrossingsAtStrictHenselizations D)
    (hfac : ∀ x : X, x ∈ D.support → ∃ fs : List (X.presheaf.stalk x),
      (∀ f ∈ fs, IsRegularLocalRing ((X.presheaf.stalk x : Type u) ⧸ Ideal.span {f})) ∧
        1 ≤ fs.length ∧
        AlgebraicGeometry.IdealSheafData.stalk D x = Ideal.span {fs.prod}) :
    IsStrictNormalCrossingsDivisor D

Stacks.Divisors.isNormalCrossingsDivisor_iff_isStrictNormalCrossingsAtStrictHenselizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/StrictHenselizationEquivalence.lean, line 122.

Let X be a locally Noetherian scheme and D ⊂ X a closed subscheme. If X is J-2 or Nagata, then D is a normal crossings divisor in X if and only if for every point p of D the pullback of D to the spectrum of the strict henselization 𝒪^{sh}_{X, p} is a strict normal crossings divisor.

public theorem isNormalCrossingsDivisor_iff_isStrictNormalCrossingsAtStrictHenselizations
    {X : Scheme.{u}} [IsLocallyNoetherian X] (D : X.IdealSheafData)
    (hX : AlgebraicGeometry.Scheme.IsJ2 X ∨ IsNagataScheme X) :
    IsNormalCrossingsDivisor D ↔ IsStrictNormalCrossingsAtStrictHenselizations D

Stacks.Divisors.isEffectiveCartierDivisor_of_isStrictNormalCrossingsAtStrictHenselizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleBasics/NormalCrossings/StrictHenselizationStalkIdeal.lean, line 246. The attribute's comment: “(2) ⇒ (1), the effective Cartier divisor conjunct of condition (1). The étale-local strict normal crossings clause of (1) is not asserted, and no J-2 or Nagata hypothesis is used for this conjunct.”.

Stacks Project, Tag 0CBS, the effective Cartier divisor conjunct of (2) ⇒ (1). A closed subscheme of a locally Noetherian scheme whose inverse image to the spectrum of a strict henselization of the local ring at each of its points is a strict normal crossings divisor is an effective Cartier divisor. No J-2 or Nagata hypothesis is needed for this conjunct: the local equation is recovered one point at a time by descent along the henselization.

theorem isEffectiveCartierDivisor_of_isStrictNormalCrossingsAtStrictHenselizations
    {X : Scheme.{u}} [IsLocallyNoetherian X] (D : X.IdealSheafData)
    (hD : IsStrictNormalCrossingsAtStrictHenselizations D) :
    IsEffectiveCartierDivisor D
Sources
LeanStacks.Divisors.IsStrictNormalCrossingsDivisor · Stacks.Divisors.isStrictNormalCrossingsDivisor_iff · Stacks.Divisors.isStrictNormalCrossingsDivisor_comap · Stacks.Divisors.IsNormalCrossingsDivisor · Stacks.Divisors.isNormalCrossingsDivisor_comap · Stacks.Divisors.isClopen_normalizationDistinctLocus · Stacks.Divisors.unramified_normalizationDistinctToAmbient · Stacks.Divisors.formallyUnramified_normalizationDistinctToAmbient

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.