29.48 Absolute weak… to 29.59 Miscellany

Section29.48 Absolute weak normalization and seminormalization#

Section 29.48 of the Stacks Project, Tag 0EUK. 10 tags here are carried by 37 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0EUL, a definition

Tag 0EUL in the Stacks Project.

IsSeminormalRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Ring.lean, line 50. The attribute's comment: “part (1)”.

A commutative ring is seminormal if every x, y with x ^ 3 = y ^ 2 are uniquely the square and cube of a common element.

Use isSeminormalRing_iff to rewrite this predicate and IsSeminormalRing.existsUnique_of_cube_eq_square to apply its defining condition.

def IsSeminormalRing (A : Type*) [CommRing A] : Prop

IsAbsolutelyWeaklyNormalRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Ring.lean, line 74. The attribute's comment: “part (2)”.

A commutative ring is absolutely weakly normal if it is seminormal and, for every prime number p, every solution of p ^ p * x = y ^ p uniquely has the prescribed form x = a ^ p, y = p * a.

Use isAbsolutelyWeaklyNormalRing_iff to rewrite this predicate, IsAbsolutelyWeaklyNormalRing.isSeminormalRing for its seminormal part, and IsAbsolutelyWeaklyNormalRing.existsUnique_of_prime_pow_mul_eq_pow for its prime-root condition.

abbrev IsAbsolutelyWeaklyNormalRing (A : Type*) [CommRing A] : Prop

Tag 0EUM, a lemma

Tag 0EUM in the Stacks Project.

isSeminormalRing_propertyIsLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Local.lean, line 130. The attribute's comment: “seminormal_local_property”.

Seminormality is a local property of commutative rings.

theorem isSeminormalRing_propertyIsLocal :
    CommRing.PropertyIsLocal
      (fun (R : Type u) [CommRing R] => IsSeminormalRing R)

isAbsolutelyWeaklyNormalRing_propertyIsLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Local.lean, line 445. The attribute's comment: “absolutely_weakly_normal_local_property”.

Being an absolutely weakly normal commutative ring is a local property of rings.

theorem isAbsolutelyWeaklyNormalRing_propertyIsLocal :
    CommRing.PropertyIsLocal
      (fun (R : Type u) [CommRing R] => IsAbsolutelyWeaklyNormalRing R)

Tag 0EUN, a definition

Tag 0EUN in the Stacks Project.

AlgebraicGeometry.IsSeminormal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Scheme.lean, line 49. The attribute's comment: “part (1)”.

A scheme is seminormal if every point has an affine open neighbourhood whose ring of sections is seminormal.

abbrev IsSeminormal (X : Scheme.{u}) : Prop

AlgebraicGeometry.IsAbsolutelyWeaklyNormal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Scheme.lean, line 55. The attribute's comment: “part (2)”.

A scheme is absolutely weakly normal if every point has an affine open neighbourhood whose ring of sections is absolutely weakly normal.

abbrev IsAbsolutelyWeaklyNormal (X : Scheme.{u}) : Prop

Tag 0EUP, a lemma

Tag 0EUP in the Stacks Project.

AlgebraicGeometry.isSeminormal_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/SeminormalLocalCriteria.lean, line 50. The attribute's comment: “seminormal equivalent conditions”.

A scheme is seminormal if and only if the section ring of every affine open is seminormal, if and only if this holds on an affine open covering, if and only if the scheme has an open covering by seminormal open subschemes.

public theorem isSeminormal_tfae (X : Scheme.{u}) :
    List.TFAE [
      IsSeminormal X,
      ∀ U : X.affineOpens, IsSeminormalRing Γ(X, U.val),
      ∃ (I : Type u) (U : I → X.affineOpens),
        (⨆ i, (U i).val) = ⊤ ∧ ∀ i, IsSeminormalRing Γ(X, (U i).val),
      ∃ (I : Type u) (U : I → X.Opens),
        (⨆ i, U i) = ⊤ ∧ ∀ i, IsSeminormal (U i).toScheme]

AlgebraicGeometry.isSeminormal_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/SeminormalLocalCriteria.lean, line 65. The attribute's comment: “seminormal open subschemes”.

Every open subscheme of a seminormal scheme is seminormal.

public theorem isSeminormal_open {X : Scheme.{u}} (hX : IsSeminormal X)
    (U : X.Opens) : IsSeminormal U.toScheme

AlgebraicGeometry.isAbsolutelyWeaklyNormal_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/SeminormalLocalCriteria.lean, line 73. The attribute's comment: “absolutely weakly normal equivalent conditions”.

A scheme is absolutely weakly normal if and only if the section ring of every affine open is absolutely weakly normal, if and only if this holds on an affine open covering, if and only if the scheme has an open covering by absolutely weakly normal open subschemes.

public theorem isAbsolutelyWeaklyNormal_tfae (X : Scheme.{u}) :
    List.TFAE [
      IsAbsolutelyWeaklyNormal X,
      ∀ U : X.affineOpens, IsAbsolutelyWeaklyNormalRing Γ(X, U.val),
      ∃ (I : Type u) (U : I → X.affineOpens),
        (⨆ i, (U i).val) = ⊤ ∧ ∀ i, IsAbsolutelyWeaklyNormalRing Γ(X, (U i).val),
      ∃ (I : Type u) (U : I → X.Opens),
        (⨆ i, U i) = ⊤ ∧ ∀ i, IsAbsolutelyWeaklyNormal (U i).toScheme]

AlgebraicGeometry.isAbsolutelyWeaklyNormal_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/SeminormalLocalCriteria.lean, line 90. The attribute's comment: “absolutely weakly normal open subschemes”.

Every open subscheme of an absolutely weakly normal scheme is absolutely weakly normal.

public theorem isAbsolutelyWeaklyNormal_open {X : Scheme.{u}}
    (hX : IsAbsolutelyWeaklyNormal X) (U : X.Opens) :
    IsAbsolutelyWeaklyNormal U.toScheme

Tag 0EUQ, a lemma

Tag 0EUQ in the Stacks Project.

seminormalRing_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Ring.lean, line 98. The attribute's comment: “seminormal rings”.

Stacks Project, Tag 0EUQ. A seminormal commutative ring is reduced.

theorem seminormalRing_isReduced {A : Type*} [CommRing A]
    (hA : IsSeminormalRing A) : IsReduced A

absolutelyWeaklyNormalRing_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Ring.lean, line 106. The attribute's comment: “absolutely weakly normal rings”.

Stacks Project, Tag 0EUQ. An absolutely weakly normal commutative ring is reduced.

theorem absolutelyWeaklyNormalRing_isReduced {A : Type*} [CommRing A]
    (hA : IsAbsolutelyWeaklyNormalRing A) : IsReduced A

AlgebraicGeometry.seminormal_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Scheme.lean, line 60. The attribute's comment: “seminormal schemes”.

Stacks Project, Tag 0EUQ. A seminormal scheme is reduced.

theorem seminormal_isReduced {X : Scheme.{u}} (hX : IsSeminormal X) :
    IsReduced X

AlgebraicGeometry.absolutelyWeaklyNormal_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Scheme.lean, line 68. The attribute's comment: “absolutely weakly normal schemes”.

Stacks Project, Tag 0EUQ. An absolutely weakly normal scheme is reduced.

theorem absolutelyWeaklyNormal_isReduced {X : Scheme.{u}}
    (hX : IsAbsolutelyWeaklyNormal X) : IsReduced X

Tag 0EUR, a lemma

Tag 0EUR in the Stacks Project.

AlgebraicGeometry.isIso_lift_to_absoluteWeakNormalization_iff_isAbsolutelyWeaklyNormalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AbsoluteWeakNormalizationCharacterization/Basic.lean, line 243. The attribute's comment: “awn_characterization”.

A universally homeomorphic A-algebra is the absolute weak normalization of A precisely when its underlying ring is absolutely weakly normal.

public theorem isIso_lift_to_absoluteWeakNormalization_iff_isAbsolutelyWeaklyNormalRing
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (huniv : UniversalHomeomorphism
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op)) :
    IsIso ((absoluteWeakNormalizationCategoryObject_isTerminal A).from
      (⟨CommAlgCat.of A B, huniv⟩ :
        AbsoluteWeakNormalizationCategory A)) ↔
      IsAbsolutelyWeaklyNormalRing B

AlgebraicGeometry.existsUnique_absoluteWeakNormalizationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AbsoluteWeakNormalizationFunctorial/Basic.lean, line 478. The attribute's comment: “awn_functoriality”.

A ring homomorphism induces a unique compatible homomorphism between absolute weak normalizations.

public theorem existsUnique_absoluteWeakNormalizationMap
    {A : Type u} {A' : Type v} [CommRing A] [CommRing A'] (φ : A →+* A') :
    ∃! φawn : AbsoluteWeakNormalization A →+* AbsoluteWeakNormalization A',
      φawn.comp (algebraMap A (AbsoluteWeakNormalization A)) =
        (algebraMap A' (AbsoluteWeakNormalization A')).comp φ

AlgebraicGeometry.absoluteWeakNormalizationCategoryObject_isTerminal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AbsoluteWeakNormalizationTerminal/Basic.lean, line 270. The attribute's comment: “awn_final”.

The absolute weak normalization of A is final among A-algebras which give universal homeomorphisms on spectra.

public noncomputable def absoluteWeakNormalizationCategoryObject_isTerminal
    (A : Type u) [CommRing A] :
    IsTerminal (absoluteWeakNormalizationCategoryObject A)

Algebra.seminormalization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/RingColimit.lean, line 135. The attribute's comment: “seminormalization_of_a_ring”.

The seminormalization Aˢⁿ is the colimit of the finitely presented A-algebras which induce a universal homeomorphism on spectra and isomorphisms on residue fields. Its A-algebra structure is the canonical map A → Aˢⁿ.

def seminormalization (A : Type u) [CommRing A] : CommAlgCat.{u} A

Algebra.AbsoluteWeakNormalizationIndex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/RingColimit.lean, line 164. The attribute's comment: “absolute_weak_normalization_of_a_ring”.

A small category of representatives of finitely presented A-algebras whose maps on spectra are universal homeomorphisms.

abbrev AbsoluteWeakNormalizationIndex (A : Type u) [CommRing A] : Type u

Algebra.AbsoluteWeakNormalization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/RingColimit.lean, line 195. The attribute's comment: “absolute_weak_normalization_of_a_ring”.

The absolute weak normalization Aᵃʷⁿ is the colimit of all finitely presented A-algebras whose maps on spectra are universal homeomorphisms. Its inherited A-algebra structure supplies the canonical map A → Aᵃʷⁿ.

abbrev AbsoluteWeakNormalization (A : Type u) [CommRing A] : Type u

AlgebraicGeometry.seminormalizationAlgebraObject_isTerminal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SeminormalizationAffineInitial/Basic.lean, line 135. The attribute's comment: “sn_final”.

Stacks 0EUR. The seminormalization of A is terminal among the A-algebras whose spectrum morphism is a universal homeomorphism inducing isomorphisms on all residue fields.

def seminormalizationAlgebraObject_isTerminal :
    IsTerminal (seminormalizationAlgebraObject A)

AlgebraicGeometry.existsUnique_seminormalizationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SeminormalizationRingFunctorial/Basic.lean, line 359. The attribute's comment: “sn_functoriality”.

Stacks 0EUR. A ring homomorphism induces a unique compatible homomorphism between the seminormalizations of its source and target.

theorem existsUnique_seminormalizationMap
    {A : Type u} {A' : Type v} [CommRing A] [CommRing A'] (φ : A →+* A') :
    ∃! φsn : Algebra.seminormalization A →+* Algebra.seminormalization A',
      φsn.comp (algebraMap A (Algebra.seminormalization A)) =
        (algebraMap A' (Algebra.seminormalization A')).comp φ

AlgebraicGeometry.isIso_lift_to_seminormalization_iff_isSeminormalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SnCharacterization/Basic.lean, line 104. The attribute's comment: “sn_characterization”.

Stacks 0EUR. A subintegral A-algebra is the seminormalization of A precisely when its underlying ring is seminormal.

public theorem isIso_lift_to_seminormalization_iff_isSeminormalRing
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (huniv : UniversalHomeomorphism
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op))
    (hres : Scheme.Hom.InducesResidueFieldIsomorphisms
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op)) :
    IsIso ((seminormalizationAlgebraObject_isTerminal A).from
      (⟨CommAlgCat.of A B, huniv, hres⟩ : SeminormalizationAlgebraCategory A)) ↔
      IsSeminormalRing B

Algebra.isIso_toAbsoluteWeakNormalization_iff_isAbsolutelyWeaklyNormalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/RingCharacterization.lean, line 185. The attribute's comment: “awn_characterization”.

Stacks 0EUR. For an A-algebra B whose spectrum morphism to Spec A is a universal homeomorphism, the canonical map B ⟶ Aᵃʷⁿ is an isomorphism exactly when B is absolutely weakly normal.

theorem isIso_toAbsoluteWeakNormalization_iff_isAbsolutelyWeaklyNormalRing
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (huniv : UniversalHomeomorphism (Spec.map (CommRingCat.ofHom (algebraMap A B)))) :
    IsIso ((absoluteWeakNormalizationCandidate_isTerminal A).from
        (⟨CommAlgCat.of A B, huniv⟩ : AbsoluteWeakNormalizationCategory A)) ↔
      IsAbsolutelyWeaklyNormalRing B

Algebra.absoluteWeakNormalizationCandidate_isTerminal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/WeakNormalization/RingUniversalProperty.lean, line 246. The attribute's comment: “awn_final”.

Stacks 0EUR. The absolute weak normalization of A is terminal among the A-algebras whose spectrum morphism to Spec A is a universal homeomorphism.

def absoluteWeakNormalizationCandidate_isTerminal :
    IsTerminal (absoluteWeakNormalizationCandidate A)

Declarations registered for the tag:

• AlgebraicGeometry.seminormalization_universalHomeomorphism, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/SeminormalizationAffineInitial/Basic.lean, line 216 (StacksFrontier): “sn_final”.
• AlgebraicGeometry.seminormalization_inducesResidueFieldIsomorphisms, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/SeminormalizationAffineInitial/Basic.lean, line 218 (StacksFrontier): “sn_final”.

Tag 0EUS, a lemma

Tag 0EUS in the Stacks Project.

AlgebraicGeometry.hasInitialUniversalHomeomorphismOver, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AbsoluteWeakNormalizationInitial/Basic.lean, line 763. The attribute's comment: “absolute_weak_normalization_initial”.

The category of universal homeomorphisms to a scheme X has an initial object, the absolute weak normalization of X, which remains initial over every open subscheme.

public instance hasInitialUniversalHomeomorphismOver (X : Scheme.{u}) :
    HasLocallyInitialUniversalHomeomorphismOver X

AlgebraicGeometry.isIso_initialMap_iff_isAbsolutelyWeaklyNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AbsoluteWeakNormalizationIsoIff/Basic.lean, line 531. The attribute's comment: “absolute_weak_normalization_iso_iff”.

Stacks Project, Tag 0EUS. The canonical map from the absolute weak normalization of X to a universal homeomorphism Y ⟶ X is an isomorphism if and only if Y is absolutely weakly normal.

public theorem isIso_initialMap_iff_isAbsolutelyWeaklyNormal
    {X Y : Scheme.{u}} [HasLocallyInitialUniversalHomeomorphismOver X]
    (f : Y ⟶ X) (hf : UniversalHomeomorphism f) :
    IsIso ((initial.to (⟨Over.mk f, hf⟩ : UniversalHomeomorphismOver X)).hom.left) ↔
      IsAbsolutelyWeaklyNormal Y

AlgebraicGeometry.isIso_initialTo_iff_isAbsolutelyWeaklyNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/AbsoluteWeakNormalCriterion.lean, line 127. The attribute's comment: “absolute_weak_normalization_iso_iff”.

Stacks Project, Tag 0EUS. The canonical morphism from the absolute weak normalization of X to a universal homeomorphism Y ⟶ X is an isomorphism if and only if Y is absolutely weakly normal.

theorem isIso_initialTo_iff_isAbsolutelyWeaklyNormal (X : Scheme.{u})
    [HasLocallyInitialUniversalHomeomorphismOver X] (Y : UniversalHomeomorphismOver X) :
    IsIso ((initial.to Y).hom.left) ↔ IsAbsolutelyWeaklyNormal Y.obj.left

AlgebraicGeometry.existsUnique_absoluteWeakNormalization_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Functorial.lean, line 55. The attribute's comment: “absolute_weak_normalization_functorial”.

Every morphism of schemes has a unique compatible lift to the absolute weak normalizations.

theorem existsUnique_absoluteWeakNormalization_lift {X' X : Scheme.{u}} (h : X' ⟶ X) :
    ∃! hawn : X'.absoluteWeakNormalization ⟶ X.absoluteWeakNormalization,
      hawn ≫ X.absoluteWeakNormalizationHom =
        X'.absoluteWeakNormalizationHom ≫ h

AlgebraicGeometry.existsUnique_seminormalization_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/SeminormalizationFunctorial.lean, line 45. The attribute's comment: “seminormalization_functorial”.

Stacks Project, Tag 0EUS. A morphism of schemes has a unique compatible lift to their seminormalizations.

theorem existsUnique_seminormalization_lift {X' X : Scheme.{u}}
    [HasInitial (SeminormalizationCategory X')]
    [HasInitial (SeminormalizationCategory X)]
    (h : X' ⟶ X) :
    ∃! hsn : X'.seminormalization ⟶ X.seminormalization,
      hsn ≫ X.seminormalizationHom =
        X'.seminormalizationHom ≫ h

AlgebraicGeometry.hasInitial_seminormalizationCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SeminormalizationGluing/Basic.lean, line 691. The attribute's comment: “seminormalization_initial”.

Stacks Project, Tag 0EUS. The category of universal homeomorphisms to a scheme which induce isomorphisms on all residue fields has an initial object, the seminormalization of that scheme.

noncomputable instance hasInitial_seminormalizationCategory (X : Scheme.{u}) :
    HasInitial (SeminormalizationCategory X)

AlgebraicGeometry.isIso_initialTo_iff_isSeminormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SeminormalizationGluing/Basic.lean, line 716. The attribute's comment: “seminormalization_iso_iff”.

Stacks Project, Tag 0EUS. The canonical morphism from the seminormalization of X to a universal homeomorphism Y ⟶ X inducing isomorphisms on all residue fields is an isomorphism precisely when Y is seminormal.

theorem isIso_initialTo_iff_isSeminormal (X : Scheme.{u})
    (Y : SeminormalizationCategory X) :
    IsIso (initial.to Y).hom.left ↔ IsSeminormal Y.obj.left

Tag 0EUT, a definition

Tag 0EUT in the Stacks Project.

AlgebraicGeometry.Scheme.seminormalizationHom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Functorial.lean, line 85. The attribute's comment: “part (1): the seminormalization morphism of an arbitrary scheme, no hypotheses”.

The canonical morphism from the seminormalization of X to X.

abbrev Scheme.seminormalizationHom (X : Scheme.{u}) : X.seminormalization ⟶ X

Declarations registered for the tag:

• Scheme.absoluteWeakNormalizationHom registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Functorial.lean, line 88 (StacksFrontier): “part (2): the absolute weak normalization morphism of an arbitrary scheme, no hypotheses”.

Tag 0H3G, a lemma

Tag 0H3G in the Stacks Project.

AlgebraicGeometry.isSeminormal_iff_isIso_seminormalizationHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Characterization.lean, line 100. The attribute's comment: “conditions (1) and (2)”.

Stacks Project, Tag 0H3G. A scheme is seminormal if and only if its canonical seminormalization morphism is an isomorphism, i.e. if and only if it equals its own seminormalization.

theorem isSeminormal_iff_isIso_seminormalizationHom (X : Scheme.{u}) :
    IsSeminormal X ↔ IsIso X.seminormalizationHom

AlgebraicGeometry.isSeminormal_iff_isIso_of_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Characterization.lean, line 114. The attribute's comment: “conditions (1) and (3)”.

Stacks Project, Tag 0H3G. A scheme is seminormal if and only if every universal homeomorphism to it from a reduced scheme inducing isomorphisms on all residue fields is an isomorphism.

theorem isSeminormal_iff_isIso_of_universalHomeomorphism (X : Scheme.{u}) :
    IsSeminormal X ↔
      ∀ (Y : Scheme.{u}) (π : Y ⟶ X), UniversalHomeomorphism π →
        (∀ y : Y, IsIso (π.residueFieldMap y)) → IsReduced Y → IsIso π

Tag 0H3H, a lemma

Tag 0H3H in the Stacks Project.

AlgebraicGeometry.isAbsolutelyWeaklyNormal_iff_isIso_absoluteWeakNormalizationHom', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Characterization.lean, line 154. The attribute's comment: “conditions (1) and (2)”.

Stacks Project, Tag 0H3H. A scheme is absolutely weakly normal if and only if its canonical absolute weak normalization morphism is an isomorphism, i.e. if and only if it equals its own absolute weak normalization.

theorem isAbsolutelyWeaklyNormal_iff_isIso_absoluteWeakNormalizationHom' (X : Scheme.{u}) :
    IsAbsolutelyWeaklyNormal X ↔ IsIso X.absoluteWeakNormalizationHom

AlgebraicGeometry.isAbsolutelyWeaklyNormal_iff_isIso_of_universalHomeomorphism', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Characterization.lean, line 187. The attribute's comment: “conditions (1) and (3)”.

Stacks Project, Tag 0H3H. A scheme is absolutely weakly normal if and only if every universal homeomorphism to it from a reduced scheme is an isomorphism.

theorem isAbsolutelyWeaklyNormal_iff_isIso_of_universalHomeomorphism' (X : Scheme.{u}) :
    IsAbsolutelyWeaklyNormal X ↔
      ∀ (Y : Scheme.{u}) (π : Y ⟶ X), UniversalHomeomorphism π → IsReduced Y → IsIso π

Sources

• Section 29.48, Tag 0EUK
• AxiomMath/Stacks at 5ed82d14

LeanIsSeminormalRing · IsAbsolutelyWeaklyNormalRing · isSeminormalRing_propertyIsLocal · isAbsolutelyWeaklyNormalRing_propertyIsLocal · AlgebraicGeometry.IsSeminormal · AlgebraicGeometry.IsAbsolutelyWeaklyNormal · AlgebraicGeometry.isSeminormal_tfae · AlgebraicGeometry.isSeminormal_open

Section29.49 Finite locally free morphisms#

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

Tag 02KA, a definition

Tag 02KA in the Stacks Project.

Stacks.Morphisms.IsFiniteLocallyFree, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteLocallyFreeOfRank.lean, line 61. The attribute's comment: “finite locally free”. References: SGA 1 I (4.10), “more general”.

Stacks Project, Tag 02KA. A morphism of schemes is finite locally free if it is affine and the direct image of its structure sheaf is a finite locally free module.

class IsFiniteLocallyFree {X S : Scheme.{u}} (f : X ⟶ S) : Prop
    extends IsAffineHom f,
      SheafOfModules.IsFiniteLocallyFree.{u, u, u} (pushforwardStructureSheaf.{u} f)

Stacks.Morphisms.IsFiniteLocallyFreeOfRank, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteLocallyFreeOfRank.lean, line 68. The attribute's comment: “rank or degree”.

Stacks Project, Tag 02KA. A finite locally free morphism has rank (or degree) r if the direct image of its structure sheaf is finite locally free of rank r.

class IsFiniteLocallyFreeOfRank {X S : Scheme.{u}} (f : X ⟶ S) (r : ℕ) : Prop
    extends IsAffineHom f,
      SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (pushforwardStructureSheaf.{u} f) r

Tag 02KB, a lemma

Tag 02KB in the Stacks Project.

Stacks.Morphisms.isFiniteLocallyFree_iff_isFinite_flat_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/FiniteFlat.lean, line 68. The attribute's comment: “conditions (1) and (2)”.

Stacks Project, Tag 02KB. A morphism of schemes is finite locally free if and only if it is finite, flat, and locally of finite presentation.

theorem isFiniteLocallyFree_iff_isFinite_flat_locallyOfFinitePresentation
    {X S : Scheme.{u}} (f : X ⟶ S) :
    IsFiniteLocallyFree f ↔
      IsFinite f ∧ Flat f ∧ LocallyOfFinitePresentation f

Stacks.Morphisms.isFiniteLocallyFree_iff_isFinite_flat_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/FiniteFlat.lean, line 96. The attribute's comment: “condition (3) over a locally Noetherian base”.

Stacks Project, Tag 02KB. Over a locally Noetherian base, a morphism of schemes is finite locally free if and only if it is finite and flat.

theorem isFiniteLocallyFree_iff_isFinite_flat_of_isLocallyNoetherian
    {X S : Scheme.{u}} (f : X ⟶ S) [IsLocallyNoetherian S] :
    IsFiniteLocallyFree f ↔ IsFinite f ∧ Flat f

Tag 02KC, a lemma

Tag 02KC in the Stacks Project.

Stacks.Morphisms.isFiniteLocallyFree_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteLocallyFree/Comp.lean, line 38.

Stacks Project, Tag 02KC. A composition of finite locally free morphisms is finite locally free.

theorem isFiniteLocallyFree_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    [IsFiniteLocallyFree f] [IsFiniteLocallyFree g] :
    IsFiniteLocallyFree (f ≫ g)

Tag 02KD, a lemma

Tag 02KD in the Stacks Project.

Stacks.Morphisms.isFiniteLocallyFree_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteLocallyFree/BaseChange.lean, line 40.

Stacks Project, Tag 02KD. A base change of a finite locally free morphism is finite locally free.

instance isFiniteLocallyFree_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (@IsFiniteLocallyFree : MorphismProperty Scheme.{u})

Tag 04MH, a lemma

Tag 04MH in the Stacks Project.

Stacks.Morphisms.exists_isClosed_isFiniteLocallyFreeOfRank_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/DegreeDecomposition.lean, line 93.

The base of a finite locally free morphism decomposes as a disjoint union of open and closed subschemes indexed by the degree, over the d-th of which the morphism is finite locally free of degree d.

theorem exists_isClosed_isFiniteLocallyFreeOfRank_decomposition {X S : Scheme.{u}} (f : X ⟶ S)
    [IsFiniteLocallyFree f] :
    ∃ Z : ℕ → S.Opens, (∀ d, IsClosed (Z d : Set S)) ∧
      (∀ d e, d ≠ e → Disjoint (Z d) (Z e)) ∧ (⨆ d : ℕ, Z d) = ⊤ ∧
      ∀ d, IsFiniteLocallyFreeOfRank (f ∣_ Z d) d

Tag 03HW, a lemma

Tag 03HW in the Stacks Project.

Stacks.Morphisms.exists_finiteLocallyFree_cover_closedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteLocallyFree/FiniteCover.lean, line 214.

Stacks Project, Tag 03HW. After a surjective finite locally free base change, a finite morphism to an affine scheme embeds into a finite locally free scheme covered set-theoretically by finitely many closed sections.

theorem exists_finiteLocallyFree_cover_closedImmersion
    {Y X : Scheme.{u}} (f : Y ⟶ X) [IsFinite f] [IsAffine X] :
    ∃ (X' : Scheme.{u}) (g : X' ⟶ X),
      Surjective g ∧ IsFiniteLocallyFree g ∧
      Surjective (pullback.fst f g) ∧
      IsFiniteLocallyFree (pullback.fst f g) ∧
      ∃ (Z' : Scheme.{u}) (p : Z' ⟶ X')
        (i : pullback f g ⟶ Z'),
        IsClosedImmersion i ∧
        i ≫ p = pullback.snd f g ∧
        IsFiniteLocallyFree p ∧
        ∃ (m : ℕ) (s : Fin m → (X' ⟶ Z')),
          (∀ j, IsClosedImmersion (s j) ∧ s j ≫ p = 𝟙 X') ∧
          (∀ z : Z', ∃ j : Fin m, ∃ x : X', (s j).base x = z)

Tag 03HX, a lemma

Tag 03HX in the Stacks Project.

Stacks.Morphisms.isNowhereDense_image_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteLocallyFree/NowhereDense.lean, line 186. The attribute's comment: “nowhere denseness of the image”.

Stacks Project, Tag 03HX. The image of a closed nowhere dense subset under a finite morphism of schemes is nowhere dense.

theorem isNowhereDense_image_of_isFinite {Y X : Scheme.{u}} (f : Y ⟶ X) [IsFinite f]
    {T : Set Y} (hT_closed : IsClosed T) (hT : IsNowhereDense T) :
    IsNowhereDense (f.base '' T)

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.Hom.isClosedMap registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteLocallyFree/NowhereDense.lean, line 218 (StacksFrontier): “closedness of the image”.

Sources

• Section 29.49, Tag 02K9
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Morphisms.IsFiniteLocallyFree · Stacks.Morphisms.IsFiniteLocallyFreeOfRank · Stacks.Morphisms.isFiniteLocallyFree_iff_isFinite_flat_locallyOfFinitePresentation · Stacks.Morphisms.isFiniteLocallyFree_iff_isFinite_flat_of_isLocallyNoetherian · Stacks.Morphisms.isFiniteLocallyFree_comp · Stacks.Morphisms.isFiniteLocallyFree_isStableUnderBaseChange · Stacks.Morphisms.exists_isClosed_isFiniteLocallyFreeOfRank_decomposition · Stacks.Morphisms.exists_finiteLocallyFree_cover_closedImmersion

Section29.50 Rational maps#

Section 29.50 of the Stacks Project, Tag 01RR. 12 tags here are carried by 22 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01RS, a definition

Tag 01RS in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.PartialMap registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 136 (StacksFrontier): “(1) a morphism defined on a dense open subscheme”. References: SGA 3 XVIII (1.5), “representatives f”.
• AlgebraicGeometry.Scheme.PartialMap.equiv registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 138 (StacksFrontier): “(1) equivalence”. References: EGA I (7.1.1); EGA I (7.1.2); EGA IV (20.2.8), “special case”.
• AlgebraicGeometry.Scheme.RationalMap registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 139 (StacksFrontier): “(2) rational map”. References: EGA I (7.1.2).
• AlgebraicGeometry.Scheme.RationalMap.IsOver registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 140 (StacksFrontier): “(3) S-rational map”. References: EGA I (7.1.2); EGA IV (18.10.19); SGA 3 XVIII (1.5), “special case”.

Tag 0BX8, a lemma

Tag 0BX8 in the Stacks Project.

AlgebraicGeometry.GenericPointMapContext.bijective_genericPointMapForRationalMaps_of_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/GenericPointMapFinitePresentation.lean, line 279. The attribute's comment: “finite_presentation_bijectivity”. References: EGA IV (20.3.7), “bijectivity (fin pres)”; EGA I (7.1.11), “bijectivity”.

When the target is locally of finite presentation over the base, every compatible collection of points and local maps at the generic points comes from a unique rational map over the base.

public theorem bijective_genericPointMapForRationalMaps_of_locallyOfFinitePresentation
    [LocallyOfFinitePresentation C.toBaseTarget] :
    Function.Bijective C.genericPointMapForRationalMaps

AlgebraicGeometry.GenericPointMapContext.genericPointMapForRationalMaps_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/GenericPointMapInjective.lean, line 76. The attribute's comment: “injectivity”. References: EGA IV (20.2.11), “(i)”; EGA IV (20.3.7), “injectivity”; EGA I (7.1.11), “injectivity”.

A rational map over the base is determined by its values and induced local maps at the generic points of the irreducible components when the target is locally of finite type over the base.

public theorem genericPointMapForRationalMaps_injective
    (C : GenericPointMapContext.{u}) [LocallyOfFiniteType C.toBaseTarget] :
    Function.Injective C.genericPointMapForRationalMaps

AlgebraicGeometry.GenericPointMapContext.bijective_genericPointMapForRationalMaps_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/GenericPointMapReduced.lean, line 203. The attribute's comment: “reduced_source_bijectivity”. References: EGA IV (20.2.11), “(ii) reduced case”; EGA I (7.1.11), “bijectivity, X reduced”.

For a reduced source and a target locally of finite type over the base, rational maps over the base are determined by, and realize, arbitrary compatible local data at the generic points of the source.

public theorem bijective_genericPointMapForRationalMaps_of_isReduced
    [LocallyOfFiniteType C.toBaseTarget] [IsReduced C.X] :
    Function.Bijective C.genericPointMapForRationalMaps

Tag 01RT, a definition

Tag 01RT in the Stacks Project.

AlgebraicGeometry.Scheme.rationalFunctions, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RationalFunctions/Basic.lean, line 117. References: EGA I (7.1.2); EGA IV (20.2.8), “special case”.

A rational function on a scheme is a rational map to the affine line over the integers.

abbrev Scheme.rationalFunctions (X : Scheme.{u}) : Type u

Tag 01RU, a definition

Tag 01RU in the Stacks Project.

Stacks.Chow.rationalFunctionsRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalFunctions.lean, line 466.

Stacks 01RU. The ring structure on rational maps to the affine line is the one induced by the ring operations on sections on every dense open: there is a commutative ring structure on R(X) for which, for every dense open U ⊆ X, the map sending a section s ∈ Γ(X, U) to the rational function it represents is a ring homomorphism.

theorem rationalFunctionsRing (X : Scheme.{u}) :
    ∃ R : CommRing (rationalFunctions X),
      letI := R
      ∀ U : DenseOpen X,
        ∃ φ : Γ(X, U.1) →+* rationalFunctions X,
          ∀ s, φ s = ofSection X U s

Tag 01RV, a lemma

Tag 01RV in the Stacks Project.

Stacks.Chow.rationalFunctionsEquivStalks, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalFunctions/FunctionField.lean, line 592. The attribute's comment: “product of generic local rings”. References: EGA I (7.1.13), “more general”; EGA I (7.1.5), “more general”; EGA I (7.1.8), “partial”; EGA I (7.3.3), “partial”; SGA 1 I (10.3), “more general”; SGA 4 IX (4.0), “partial”.

Stacks 01RV. The rational functions of a scheme with finitely many irreducible components are the product of the local rings at the generic points of those components; the identification sends a section on a dense open to its family of germs.

def rationalFunctionsEquivStalks (X : Scheme.{u}) [Finite (irreducibleComponents X)] :
    { e : rationalFunctions X ≃+*
        (∀ Z : irreducibleComponents X, X.presheaf.stalk Z.2.1.genericPoint) //
      ∀ (U : DenseOpen X) (s : Γ(X, U.1)) (Z : irreducibleComponents X)
        (h : Z.2.1.genericPoint ∈ U.1),
        e (ofSection X U s) Z = X.presheaf.germ U.1 Z.2.1.genericPoint h s }

Stacks.Chow.rationalFunctionsEquivResidueFields, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalFunctions/FunctionField.lean, line 608. The attribute's comment: “product of generic residue fields”. References: EGA I (7.3.3), “special case”; SGA 1 I (10.3), “special case”; SGA 4 IX (4.0), “special case”.

Stacks 01RV. On a reduced scheme the generic local rings are the residue fields at the generic points, so the rational functions are their product.

def rationalFunctionsEquivResidueFields (X : Scheme.{u}) [Finite (irreducibleComponents X)]
    [IsReduced X] :
    { e : rationalFunctions X ≃+*
        (∀ Z : irreducibleComponents X, X.residueField Z.2.1.genericPoint) //
      ∀ (U : DenseOpen X) (s : Γ(X, U.1)) (Z : irreducibleComponents X)
        (h : Z.2.1.genericPoint ∈ U.1),
        e (ofSection X U s) Z = X.evaluation U.1 Z.2.1.genericPoint h s }

Stacks.Chow.rationalFunctionsEquivFunctionField, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalFunctions/FunctionField.lean, line 625. The attribute's comment: “integral function field”. References: EGA I (7.1.5), “integral case”.

Stacks 01RV. On an integral scheme the rational functions are the function field, that is, the stalk at the generic point.

def rationalFunctionsEquivFunctionField (X : Scheme.{u}) [IsIntegral X] :
    { e : rationalFunctions X ≃+* X.functionField //
      ∀ (U : DenseOpen X) (s : Γ(X, U.1)) (h : genericPoint X ∈ U.1),
        e (ofSection X U s) = X.presheaf.germ U.1 (genericPoint X) h s }

Stacks.Chow.rationalFunctionsEquivResidueField, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalFunctions/FunctionField.lean, line 666. The attribute's comment: “integral residue field”. References: EGA I (7.1.5), “κ(η) when integral”.

Stacks 01RV. On an integral scheme the rational functions are the residue field of the generic point.

def rationalFunctionsEquivResidueField (X : Scheme.{u}) [IsIntegral X] :
    { e : rationalFunctions X ≃+* X.residueField (genericPoint X) //
      ∀ (U : DenseOpen X) (s : Γ(X, U.1)) (h : genericPoint X ∈ U.1),
        e (ofSection X U s) = X.evaluation U.1 (genericPoint X) h s }

Stacks.Chow.isField_rationalFunctions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalFunctions/FunctionField.lean, line 682. The attribute's comment: “field property”. References: EGA I (7.1.5), “field when integral”; EGA I (7.1.8), “special case”.

Stacks 01RV. The ring of rational functions of an integral scheme is a field.

theorem isField_rationalFunctions (X : Scheme.{u}) [IsIntegral X] :
    IsField (rationalFunctions X)

Tag 01RW, a definition

Tag 01RW in the Stacks Project.

AlgebraicGeometry.Scheme.functionFieldOfRationalFunctions, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RationalFunctions/FunctionField.lean, line 44.

The function field, or field of rational functions, of an integral scheme X: the ring R(X) of rational functions on X, which is a field because X is integral.

abbrev functionFieldOfRationalFunctions (X : Scheme.{u}) [IsIntegral X] : Type u

Tag 02NF, a lemma

Tag 02NF in the Stacks Project.

Stacks.Chow.not_subset_range_genericStalk_of_not_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalFunctions/LocalRings.lean, line 69. The attribute's comment: “noninclusion of local rings”. References: EGA I (8.2.4); EGA I (8.2.3), “sufficiency direction”.

Stacks Project, Tag 02NF. On an integral separated scheme, if an irreducible closed subset Z₁ is not contained in an irreducible closed subset Z₂, then the local ring at the generic point of Z₁ is not contained in the local ring at the generic point of Z₂, as subrings of the field of rational functions.

theorem not_subset_range_genericStalk_of_not_le (X : Scheme.{u})
    [IsIntegral X] [Scheme.IsSeparated X] (Z₁ Z₂ : IrreducibleCloseds X) (hZ : ¬ Z₁ ≤ Z₂) :
    ¬ Set.range (algebraMap (X.presheaf.stalk Z₁.isIrreducible.genericPoint) X.functionField) ⊆
      Set.range (algebraMap (X.presheaf.stalk Z₂.isIrreducible.genericPoint)
        X.functionField)

Stacks.Chow.exists_section_notMem_range_genericStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalFunctions/LocalRings.lean, line 143. The attribute's comment: “closed-point neighbourhood form”. References: EGA I (8.2.4), “closed point case”; EGA I (8.2.3), “closed point, separated”.

Stacks Project, Tag 02NF. On an integral separated scheme, a closed point x outside an irreducible closed subset Z carries a function regular on a neighbourhood of x whose class in the field of rational functions does not lie in the local ring at the generic point of Z.

theorem exists_section_notMem_range_genericStalk (X : Scheme.{u})
    [IsIntegral X] [Scheme.IsSeparated X] (Z : IrreducibleCloseds X) (x : X)
    (hx : IsClosed ({x} : Set X)) (hxZ : x ∉ Z) :
    ∃ (U : X.Opens) (hxU : x ∈ U) (s : Γ(X, U)),
      algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ U x hxU s) ∉
        Set.range (algebraMap (X.presheaf.stalk Z.isIrreducible.genericPoint)
          X.functionField)

Tag 0A1X, a definition

Tag 0A1X in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.RationalMap.domain registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 265 (StacksFrontier): “the domain of definition”. References: EGA I (7.2.1); EGA IV (18.10.19); EGA IV (20.2.3), “special case”.
• AlgebraicGeometry.Scheme.RationalMap.mem_domain registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 266 (StacksFrontier): “a point is in it iff some representative is defined there”. References: EGA I (7.2.1); EGA IV (20.2.3), “special case”.

Tag 0A1Y, a lemma

Tag 0A1Y in the Stacks Project.

AlgebraicGeometry.Scheme.RationalMap.existsUnique_hom_domain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RationalFunctions/DomainOfDefinition.lean, line 59. The attribute's comment: “existence and uniqueness of the morphism on the domain of definition”. References: EGA I (7.2.2), “special case”; EGA IV (20.2.4), “special case”; EGA IV (20.2.8), “special case”; EGA IV (20.3.2), “special case”.

Let X and Y be schemes with X reduced and Y separated, and let φ be a rational map from X to Y with domain of definition φ.domain. There is exactly one morphism φ.domain ⟶ Y representing φ, that is, exactly one morphism on the domain of definition whose partial map lies in the equivalence class φ.

theorem existsUnique_hom_domain [IsReduced X] [Y.IsSeparated] (φ : X ⤏ Y) :
    ∃! f : φ.domain.toScheme ⟶ Y,
      (PartialMap.mk φ.domain φ.dense_domain f).toRationalMap = φ

AlgebraicGeometry.Scheme.RationalMap.isOver_of_toRationalMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RationalFunctions/DomainOfDefinition.lean, line 77. The attribute's comment: “the morphism on the domain of definition is a morphism over a separated base”. References: EGA IV (20.2.5), “special case”.

Let X and Y be schemes over a separated scheme S, with X reduced and Y separated, and let φ be an S-rational map from X to Y. Then the morphism on the domain of definition of φ that represents φ is a morphism over S.

theorem isOver_of_toRationalMap_eq [X.Over S] [Y.Over S] [IsReduced X] [Y.IsSeparated]
    [S.IsSeparated] (φ : X ⤏ Y) [φ.IsOver S] {f : φ.domain.toScheme ⟶ Y}
    (hf : (PartialMap.mk φ.domain φ.dense_domain f).toRationalMap = φ) :
    f.IsOver S

Tag 0A20, a definition

Tag 0A20 in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.BirationalOver registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Basic.lean, line 92 (StacksFrontier): “(2)”.

Tag 0BAA, a lemma

Tag 0BAA in the Stacks Project.

AlgebraicGeometry.birational_iff_exists_nonempty_open_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/BirationalOpenIso.lean, line 40. The attribute's comment: “part (1)”.

Two irreducible schemes are birational if and only if they have isomorphic nonempty open subschemes.

public theorem birational_iff_exists_nonempty_open_iso
    {X Y : Scheme.{u}} [IrreducibleSpace X] [IrreducibleSpace Y] :
    Scheme.Birational X Y ↔
      ∃ (U : X.Opens) (V : Y.Opens),
        (U : Set X).Nonempty ∧ (V : Set Y).Nonempty ∧
          Nonempty (U.toScheme ≅ V.toScheme)

Declarations registered for the tag:

• AlgebraicGeometry.birationalOver_iff_exists_nonempty_open_iso, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/DifferentialsAndValuative/BirationalOpenIso.lean, line 49 (StacksFrontier): “part (2)”.

Tag 01RX, a remark

Tag 01RX in the Stacks Project.

AlgebraicGeometry.Scheme.PseudoMap, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/PseudoMorphism.lean, line 82. The attribute's comment: “the pseudo-maps: morphisms into Y defined on scheme-theoretically dense opens of X, the objects whose equivalence classes the remark calls pseudo-morphisms”.

A pseudo-map from X to Y is a morphism into Y defined on a scheme-theoretically dense open subscheme of X. This is the variant of AlgebraicGeometry.Scheme.PartialMap in which the domain of definition is required to be scheme-theoretically dense.

structure PseudoMap (X Y : Scheme.{u})

AlgebraicGeometry.Scheme.PseudoMap.equiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/PseudoMorphism.lean, line 140. The attribute's comment: “the equivalence relation on pseudo-maps: agreement after restriction to a scheme-theoretically dense open”. References: EGA IV (20.2.1).

Two pseudo-maps are equivalent if they agree after restriction to a scheme-theoretically dense open subscheme.

protected noncomputable def equiv (f g : X.PseudoMap Y) : Prop

AlgebraicGeometry.Scheme.PseudoMap.equivalence_rel, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/PseudoMorphism.lean, line 169. The attribute's comment: “equivalence relation, via stability of scheme-theoretic density under intersection (Tag 01RF)”.

Equivalence of pseudo-maps is an equivalence relation.

lemma equivalence_rel : Equivalence (@Scheme.PseudoMap.equiv X Y)

AlgebraicGeometry.Scheme.PseudoMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/PseudoMorphism.lean, line 188. The attribute's comment: “the pseudo-morphisms from X to Y: the equivalence classes of pseudo-maps”.

A pseudo-morphism from X to Y is an equivalence class of pseudo-maps, where two pseudo-maps are equivalent if they agree on a scheme-theoretically dense open subscheme.

noncomputable def PseudoMorphism (X Y : Scheme.{u}) : Type u

AlgebraicGeometry.Scheme.PseudoMorphism.IsOver, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/PseudoMorphism.lean, line 206. The attribute's comment: “the S-pseudo-morphisms: the analogue for pseudo-morphisms of part (3) of the definition of an S-rational map”.

A pseudo-morphism is an S-pseudo-morphism if some pseudo-map in the equivalence class is an S-morphism.

class PseudoMorphism.IsOver [X.Over S] [Y.Over S] (f : X.PseudoMorphism Y) : Prop

AlgebraicGeometry.Scheme.PseudoMorphism.equivRationalMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/PseudoMorphism.lean, line 262. The attribute's comment: “agreement of pseudo-morphisms with rational maps for reduced X”. References: EGA IV (20.2.7); EGA IV (20.4.3), “Identification”.

If X is reduced, pseudo-morphisms from X to Y are the same thing as rational maps from X to Y.

noncomputable def PseudoMorphism.equivRationalMap : X.PseudoMorphism Y ≃ X.RationalMap Y

Sources

• Section 29.50, Tag 01RR
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Scheme.PartialMap · AlgebraicGeometry.Scheme.PartialMap.equiv · AlgebraicGeometry.Scheme.RationalMap · AlgebraicGeometry.Scheme.RationalMap.IsOver · AlgebraicGeometry.GenericPointMapContext.bijective_genericPointMapForRationalMaps_of_locallyOfFinitePresentation · AlgebraicGeometry.GenericPointMapContext.genericPointMapForRationalMaps_injective · AlgebraicGeometry.GenericPointMapContext.bijective_genericPointMapForRationalMaps_of_isReduced · AlgebraicGeometry.Scheme.rationalFunctions

Section29.51 Birational morphisms#

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

Tag 01RO, a definition

Tag 01RO in the Stacks Project.

AlgebraicGeometry.IsBirational, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Basic.lean, line 67. References: EGA I (2.2.9); EGA IV (6.15.4), “finitely many comps”; EGA I (6.5.5).

A morphism of schemes is birational if it induces a bijection on the generic points of irreducible components and an isomorphism on the local rings at every such point of its source.

This definition is meaningful without the finiteness hypotheses on the sets of irreducible components imposed in [Stacks Project, Tag 01RO].

def IsBirational {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop

Tag 01RP, a lemma

Tag 01RP in the Stacks Project.

AlgebraicGeometry.IsBirational.isDominant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Dominant.lean, line 57. References: EGA I (2.2.9), “more general”.

A birational morphism of schemes is dominant.

theorem IsBirational.isDominant {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : IsBirational f) :
    IsDominant f

Tag 0BAB, a lemma

Tag 0BAB in the Stacks Project.

AlgebraicGeometry.isIso_pullback_snd_fromSpecStalk_of_isBirational, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/GenericBaseChange.lean, line 131.

The base change of a birational morphism to the spectrum of the local ring at a generic point of an irreducible component of the target is an isomorphism.

lemma isIso_pullback_snd_fromSpecStalk_of_isBirational
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Finite (irreducibleComponents X)] [Finite (irreducibleComponents Y)]
    (hf : IsBirational f) (y : Y) (hy : y ∈ genericPoints Y) :
    IsIso (pullback.snd f (Y.fromSpecStalk y))

Tag 01RQ, an example

Tag 01RQ in the Stacks Project.

AlgebraicGeometry.localization_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Examples/Localization.lean, line 57. The attribute's comment: “localization_birational”.

The localization morphism of spectra is birational: both spectra are irreducible with generic point the zero ideal, and the local rings there agree.

theorem localization_isBirational (A : Type u) [CommRing A] [IsDomain A]
    (S : Submonoid A) (hS : (0 : A) ∉ S) :
    IsBirational
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A (Localization S))).op)

AlgebraicGeometry.exists_nonzero_away_isUnit_of_isIso_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Examples/Localization.lean, line 80. The attribute's comment: “localization_open_criterion”.

If the localization morphism is an isomorphism over a nonempty open, then every denominator already becomes a unit on some nonempty principal open.

theorem exists_nonzero_away_isUnit_of_isIso_restrict
    (A : Type u) [CommRing A] [IsDomain A]
    (S : Submonoid A) (_hS : (0 : A) ∉ S)
    (U : (Spec (CommRingCat.of A)).Opens)
    (hU : Set.Nonempty (U : Set (Spec (CommRingCat.of A))))
    (hiso : IsIso
      ((Scheme.Spec.map (CommRingCat.ofHom (algebraMap A (Localization S))).op) ∣_ U)) :
    ∃ a : A, a ≠ 0 ∧ ∀ s : S, IsUnit (algebraMap A (Localization.Away a) s.1)

AlgebraicGeometry.oddIntegers, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Examples/Localization.lean, line 132. The attribute's comment: “integer_counterexample”.

The multiplicative submonoid of odd integers.

def oddIntegers : Submonoid ℤ

AlgebraicGeometry.localization_not_isIso_restrict_nonempty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Examples/Localization.lean, line 140. The attribute's comment: “integer_counterexample”.

The localization of ℤ at all odd integers is not an isomorphism over any nonempty open of its target.

theorem localization_not_isIso_restrict_nonempty
    (U : (Scheme.Spec.obj (Opposite.op (CommRingCat.of ℤ))).Opens) (hU : U ≠ ⊥) :
    ¬ IsIso
      ((Scheme.Spec.map
        (CommRingCat.ofHom (algebraMap ℤ (Localization oddIntegers))).op) ∣_ U)

AlgebraicGeometry.PolynomialRetract.retractionMap_comp_inclusionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Examples/PolynomialRetract.lean, line 97. The attribute's comment: “ring_maps”.

Setting every y_a to zero is a retraction of the canonical inclusion of k[x].

theorem retractionMap_comp_inclusionMap :
    (retractionMap k).comp (inclusionMap k) = RingHom.id (baseRing k)

AlgebraicGeometry.PolynomialRetract.inclusionMap_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Examples/PolynomialRetract.lean, line 109. The attribute's comment: “ring_maps”.

The canonical map from k[x] to the quotient ring is injective, being a section of the retraction.

theorem inclusionMap_injective : Function.Injective (inclusionMap k)

AlgebraicGeometry.PolynomialRetract.inclusionMap_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Examples/PolynomialRetractBirational.lean, line 185. The attribute's comment: “projection_birational”.

The canonical inclusion k[x] → B induces a birational morphism on spectra.

theorem inclusionMap_isBirational (k : Type u) [Field k] :
    IsBirational
      (Scheme.Spec.map (CommRingCat.ofHom (inclusionMap k)).op)

AlgebraicGeometry.PolynomialRetract.retraction_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Examples/PolynomialRetractBirational.lean, line 209. The attribute's comment: “section_birational”.

The retraction B → k[x], setting every y_a to zero, induces a birational morphism on spectra: the section Spec k[x] ⟶ Spec B is birational.

theorem retraction_isBirational (k : Type u) [Field k] :
    IsBirational
      (Scheme.Spec.map (CommRingCat.ofHom (retractionMap k)).op)

AlgebraicGeometry.PolynomialRetract.not_isIso_restrict_specMap_inclusionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Examples/PolynomialRetractNotIso.lean, line 59. The attribute's comment: “projection_not_iso”.

The spectrum of the polynomial retract is not isomorphic to the base over any nonempty open.

theorem not_isIso_restrict_specMap_inclusionMap
    (k : Type u) [Field k] [Infinite k]
    (U : (Spec (.of (baseRing k))).Opens) (hU : (U : Set (Spec (.of (baseRing k)))).Nonempty) :
    ¬ IsIso ((Spec.map (CommRingCat.ofHom (inclusionMap k))) ∣_ U)

AlgebraicGeometry.PolynomialRetract.not_isIso_restrict_specMap_retractionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/Examples/PolynomialRetractNotIso.lean, line 119. The attribute's comment: “section_not_iso”.

The section induced by the polynomial-ring retraction is not an isomorphism over any nonempty open of the target.

theorem not_isIso_restrict_specMap_retractionMap
    (k : Type u) [Field k] [Infinite k]
    (U : (Spec (.of (extensionRing k))).Opens)
    (hU : (U : Set (Spec (.of (extensionRing k)))).Nonempty) :
    ¬ IsIso ((Spec.map (CommRingCat.ofHom (retractionMap k))) ∣_ U)

Tag 0BAC, a lemma

Tag 0BAC in the Stacks Project.

AlgebraicGeometry.exists_dense_opens_isIso_resLE_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/DenseOpenIso.lean, line 138. The attribute's comment: “dense open isomorphism”.

A birational morphism between schemes with finitely many irreducible components is an isomorphism between dense open subschemes, provided that it is locally of finite type with reduced target or locally of finite presentation.

public theorem exists_dense_opens_isIso_resLE_of_isBirational
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Finite (irreducibleComponents X)] [Finite (irreducibleComponents Y)]
    (hf : IsBirational f)
    (hfin : (LocallyOfFiniteType f ∧ IsReduced Y) ∨ LocallyOfFinitePresentation f) :
    ∃ (U : X.Opens) (V : Y.Opens) (hUV : U ≤ f ⁻¹ᵁ V),
      Dense (U : Set X) ∧ Dense (V : Set Y) ∧ IsIso (f.resLE V U hUV)

AlgebraicGeometry.birationalOver_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/DenseOpenIso.lean, line 285. The attribute's comment: “over-base consequence”.

A birational morphism of schemes over a base, under either finiteness hypothesis of the theorem, makes the schemes birational over that base.

public theorem birationalOver_of_isBirational
    {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S) (f : X ⟶ Y)
    [Finite (irreducibleComponents X)] [Finite (irreducibleComponents Y)]
    (hf : IsBirational f) (hfS : f ≫ sY = sX)
    (hfin : (LocallyOfFiniteType f ∧ IsReduced Y) ∨ LocallyOfFinitePresentation f) :
    Scheme.BirationalOver sX sY

Tag 0BAD, a lemma

Tag 0BAD in the Stacks Project.

AlgebraicGeometry.birationalOver_iff_exists_nonempty_open_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/GenericStalkCriterion.lean, line 113. The attribute's comment: “parts (1) and (2)”.

For irreducible schemes, birationality over a base is witnessed by an isomorphism of nonempty open subschemes over that base.

public theorem birationalOver_iff_exists_nonempty_open_iso
    {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
    [IrreducibleSpace X] [IrreducibleSpace Y] :
    Scheme.BirationalOver sX sY ↔
      ∃ (U : X.Opens) (V : Y.Opens),
        (U : Set X).Nonempty ∧ (V : Set Y).Nonempty ∧
          ∃ e : U.toScheme ≅ V.toScheme,
            e.hom ≫ V.ι ≫ sY = U.ι ≫ sX

AlgebraicGeometry.birationalOver_iff_generic_stalk_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/GenericStalkCriterion.lean, line 133. The attribute's comment: “parts (1) and (3)”. References: EGA I (6.5.4), “(ii), special case”.

For irreducible schemes locally of finite presentation over a base, birationality over that base is equivalent to an isomorphism of their generic local rings as algebras over the local ring of the common image.

public theorem birationalOver_iff_generic_stalk_iso
    {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
    [IrreducibleSpace X] [IrreducibleSpace Y]
    [LocallyOfFinitePresentation sX] [LocallyOfFinitePresentation sY] :
    Scheme.BirationalOver sX sY ↔
      ∃ (h : sX (genericPoint X) = sY (genericPoint Y))
        (e : X.presheaf.stalk (genericPoint X) ≅
          Y.presheaf.stalk (genericPoint Y)),
          h ▸ (sX.stalkMap (genericPoint X) ≫ e.hom) =
            sY.stalkMap (genericPoint Y)

Tag 0552, a lemma

Tag 0552 in the Stacks Project.

AlgebraicGeometry.birationalOver_tfae_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/CommonOpen.lean, line 206.

Stacks Project, Tag 0552. For integral schemes locally of finite type over a base, birationality over the base, the existence of isomorphic nonempty open subschemes over the base, and the existence of an isomorphism of the residue fields at the generic points over the base are equivalent.

public theorem birationalOver_tfae_of_isIntegral {S X Y : Scheme.{u}}
    (sX : X ⟶ S) (sY : Y ⟶ S) [IsIntegral X] [IsIntegral Y]
    [LocallyOfFiniteType sX] [LocallyOfFiniteType sY] :
    List.TFAE
      [Scheme.BirationalOver sX sY,
        ∃ (U : X.Opens) (V : Y.Opens), (U : Set X).Nonempty ∧ (V : Set Y).Nonempty ∧
          ∃ e : U.toScheme ≅ V.toScheme, e.hom ≫ V.ι ≫ sY = U.ι ≫ sX,
        ∃ (h : sX (genericPoint X) = sY (genericPoint Y))
          (e : X.residueField (genericPoint X) ≅ Y.residueField (genericPoint Y)),
          h ▸ (sX.residueFieldMap (genericPoint X) ≫ e.hom) =
            sY.residueFieldMap (genericPoint Y)]

AlgebraicGeometry.birationalOver_iff_generic_residueField_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIntegral/BirationalResidueField.lean, line 75. The attribute's comment: “parts (1) and (3)”.

Stacks 0552, parts (1) and (3). Birationality over a base of two integral schemes locally of finite type over it is equivalent to their generic points having the same image in the base together with an isomorphism of their residue fields at those generic points over the residue field of that common image.

theorem birationalOver_iff_generic_residueField_iso
    {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
    [IsIntegral X] [IsIntegral Y]
    [LocallyOfFiniteType sX] [LocallyOfFiniteType sY] :
    Scheme.BirationalOver sX sY ↔
      ∃ (h : sX (genericPoint X) = sY (genericPoint Y))
        (e : X.residueField (genericPoint X) ≅ Y.residueField (genericPoint Y)),
        h ▸ (sX.residueFieldMap (genericPoint X) ≫ e.hom) =
          sY.residueFieldMap (genericPoint Y)

Declarations registered for the tag:

• AlgebraicGeometry.birationalOver_iff_exists_nonempty_open_iso, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/GeometricallyIntegral/BirationalResidueField.lean, line 163 (StacksFrontier): “parts (1) and (2)”.

Sources

• Section 29.51, Tag 01RN
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.IsBirational · AlgebraicGeometry.IsBirational.isDominant · AlgebraicGeometry.isIso_pullback_snd_fromSpecStalk_of_isBirational · AlgebraicGeometry.localization_isBirational · AlgebraicGeometry.exists_nonzero_away_isUnit_of_isIso_restrict · AlgebraicGeometry.oddIntegers · AlgebraicGeometry.localization_not_isIso_restrict_nonempty · AlgebraicGeometry.PolynomialRetract.retractionMap_comp_inclusionMap

Section29.52 Generically finite morphisms#

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

Tag 02NW, a lemma

Tag 02NW in the Stacks Project.

AlgebraicGeometry.finite_preimage_singleton_iff_exists_affine_cover_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/GenericallyFinite.lean, line 478. The attribute's comment: “conditions (1) and (2)”.

Stacks Project, Tag 02NW, conditions (1) and (2). For a morphism locally of finite type, the fibre over a generic point of an irreducible component is finite exactly when it is covered by finitely many affine opens which are finite over a common affine neighbourhood of that generic point.

theorem finite_preimage_singleton_iff_exists_affine_cover_isFinite
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    (η : Y) (hη : η ∈ genericPoints Y) :
    (f ⁻¹' {η}).Finite ↔
      ∃ (n : ℕ) (U : Fin n → X.affineOpens) (V : Y.affineOpens),
        (η ∈ V.1) ∧
          (f ⁻¹' {η} ⊆ ⋃ i, (U i).1) ∧
            ∀ i, ∃ hUi : (U i).1 ≤ f ⁻¹ᵁ V.1, IsFinite (f.resLE V.1 (U i).1 hUi)

AlgebraicGeometry.finite_preimage_singleton_iff_exists_affine_opens_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/GenericallyFinite.lean, line 495. The attribute's comment: “condition (3)”.

Stacks Project, Tag 02NW, condition (3). For a quasi-separated morphism locally of finite type, the fibre over a generic point of an irreducible component is finite exactly when one affine open containing the fibre is finite over an affine neighbourhood of that point.

theorem finite_preimage_singleton_iff_exists_affine_opens_isFinite
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [QuasiSeparated f]
    (η : Y) (hη : η ∈ genericPoints Y) :
    (f ⁻¹' {η}).Finite ↔
      ∃ (V : Y.affineOpens) (U : X.affineOpens)
        (hUV : U.1 ≤ f ⁻¹ᵁ V.1),
        (η ∈ V.1) ∧ (f ⁻¹' {η} ⊆ U.1) ∧ IsFinite (f.resLE V.1 U.1 hUV)

AlgebraicGeometry.finite_preimage_singleton_iff_exists_affine_open_isFinite_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/GenericallyFinite.lean, line 513. The attribute's comment: “condition (4)”.

Stacks Project, Tag 02NW, condition (4). For a quasi-compact and quasi-separated morphism locally of finite type, finiteness of the fibre over a generic point of an irreducible component is equivalent to finiteness over some affine neighbourhood of the point.

theorem finite_preimage_singleton_iff_exists_affine_open_isFinite_restrict
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [QuasiCompact f]
    [QuasiSeparated f] (η : Y) (hη : η ∈ genericPoints Y) :
    (f ⁻¹' {η}).Finite ↔
      ∃ V : Y.affineOpens, (η ∈ V.1) ∧ IsFinite (f ∣_ V.1)

Tag 03HY, an example

Tag 03HY in the Stacks Project.

AlgebraicGeometry.coordinatePoint_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 79. The attribute's comment: “distinctness of coordinate points”.

Distinct coordinate projections induce distinct points of the spectrum of a countable product of copies of a field.

theorem coordinatePoint_injective (k : Type*) [Field k] :
    Function.Injective fun n : ℕ ↦ (coordinate k n).base (default : base k)

AlgebraicGeometry.doubledPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 223. The attribute's comment: “the doubled-point construction”.

The spectrum of ∏ n : ℕ, 𝔽₂ with a closed, non-open point doubled, together with its canonical projection and chart identifications.

noncomputable def doubledPoint : DoubledPoint

AlgebraicGeometry.doubledPoint_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 291. The attribute's comment: “generic point of an irreducible component”.

The doubled point is the generic point of an irreducible component of the spectrum.

theorem doubledPoint_genericPoint :
    doubledPoint.point ∈ genericPoints (space (ZMod 2))

AlgebraicGeometry.doubledPoint_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 301. The attribute's comment: “quasi-compactness”.

The canonical projection is quasi-compact.

theorem doubledPoint_quasiCompact : QuasiCompact doubledPoint.projection

AlgebraicGeometry.doubledPoint_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 311. The attribute's comment: “finite type”.

The canonical projection is locally of finite type.

theorem doubledPoint_locallyOfFiniteType : LocallyOfFiniteType doubledPoint.projection

AlgebraicGeometry.doubledPoint_finiteFibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 329. The attribute's comment: “finite fibres”.

Every fibre of the canonical projection is finite.

theorem doubledPoint_finiteFibres (y : space (ZMod 2)) :
    (doubledPoint.projection ⁻¹' {y}).Finite

AlgebraicGeometry.doubledPoint_noAffinePreimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 386. The attribute's comment: “failure of conditions (3) and (4) of Tag 02NW”.

The inverse image of every open neighbourhood of the doubled point is non-affine.

theorem doubledPoint_noAffinePreimage (U : (space (ZMod 2)).Opens)
    (hU : doubledPoint.point ∈ U) :
    ¬ IsAffine ((doubledPoint.projection ⁻¹ᵁ U).toScheme)

AlgebraicGeometry.doubledPoint_notQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 422. The attribute's comment: “failure of quasi-separatedness”.

The canonical projection is not quasi-separated.

theorem doubledPoint_notQuasiSeparated : ¬ QuasiSeparated doubledPoint.projection

AlgebraicGeometry.doubledPoint_noAffineOpenContainingFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 448. The attribute's comment: “failure of condition (3) of Tag 02NW”.

There is no affine open neighbourhood V of the doubled point together with an affine open U over V containing the whole fibre over the doubled point such that the restriction U ⟶ V of the canonical projection is finite.

theorem doubledPoint_noAffineOpenContainingFibre :
    ¬ ∃ (V : (space (ZMod 2)).affineOpens) (U : doubledPoint.source.affineOpens)
      (hUV : U.1 ≤ doubledPoint.projection ⁻¹ᵁ V.1),
        doubledPoint.point ∈ V.1 ∧
        doubledPoint.projection ⁻¹' {doubledPoint.point} ⊆ U.1 ∧
        IsFinite (doubledPoint.projection.resLE V.1 U.1 hUV)

AlgebraicGeometry.doubledPoint_noFiniteRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 500. The attribute's comment: “failure of condition (4) of Tag 02NW”.

There is no affine open neighbourhood of the doubled point above which the canonical projection is finite.

theorem doubledPoint_noFiniteRestriction :
    ¬ ∃ V : (space (ZMod 2)).affineOpens, doubledPoint.point ∈ V.1 ∧
      IsFinite (doubledPoint.projection ∣_ V.1)

Declarations registered for the tag:

• PrimeSpectrum.compactSpace registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 62 (StacksFrontier): “quasi-compactness of the affine spectrum”. References: EGA I (1.1.10), “more general”.
• AlgebraicGeometry.Space.InfiniteProduct.pow_card_eq_self, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 63 (StacksFrontier): “idempotence of the product ring”.
• AlgebraicGeometry.Space.InfiniteProduct.isClosed_singleton, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 65 (StacksFrontier): “closed points of the spectrum”.
• AlgebraicGeometry.Space.InfiniteProduct.nonempty_algEquiv_residueField, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 67 (StacksFrontier): “residue fields”.
• AlgebraicGeometry.Space.InfiniteProduct.isOpen_singleton_iff_coordinate, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 69 (StacksFrontier): “open coordinate points”.
• AlgebraicGeometry.Space.InfiniteProduct.not_discreteTopology, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 71 (StacksFrontier): “existence of a non-open point”.
• AlgebraicGeometry.Space.InfiniteProduct.instTotallyDisconnectedSpace, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/DoubledPoint.lean, line 73 (StacksFrontier): “total disconnectedness”.

Tag 03HZ, a remark

Tag 03HZ in the Stacks Project.

AlgebraicGeometry.exists_dense_open_isFinite_of_quasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/FiniteOverDenseOpen.lean, line 208. The attribute's comment: “the whole content of the remark: the alternative to Tag 02NW that it states, namely that a quasi-finite morphism is finite over a dense open of the target, whose proof the remark defers to Tag 03I1”.

Stacks Project, Tag 03I1. A quasi-finite morphism of schemes is finite over a dense open subscheme of its target. This is also the statement of [Stacks Project, Tag 03HZ], the remark offering it as an alternative to [Stacks Project, Tag 02NW] and deferring its proof to here.

theorem exists_dense_open_isFinite_of_quasiFinite {Y X : Scheme.{u}} (f : Y ⟶ X)
    [LocallyOfFiniteType f] [LocallyQuasiFinite f] [QuasiCompact f] :
    ∃ U : X.Opens, Dense (U : Set X) ∧ IsFinite (f ∣_ U)

Tag 0BAH, a lemma

Tag 0BAH in the Stacks Project.

AlgebraicGeometry.quasiFiniteAt_over_genericPoint_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Fibre.lean, line 104.

For a locally finite type morphism, the fibre over a generic point consists of generic points if and only if the morphism is quasi-finite at every point of the fibre, equivalently if it is quasi-finite at every generic point of the fibre.

public theorem quasiFiniteAt_over_genericPoint_tfae {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] (η : Y) (hη : η ∈ genericPoints Y) :
    List.TFAE [
      f ⁻¹' {η} ⊆ genericPoints X,
      ∀ x : X, f x = η → quasiFiniteAt f x,
      ∀ ξ : X, ξ ∈ genericPoints X → f ξ = η → quasiFiniteAt f ξ]

Tag 0BAI, a lemma

Tag 0BAI in the Stacks Project.

AlgebraicGeometry.exists_dense_open_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/FiniteOverDenseOpen.lean, line 448.

Stacks 0BAI. A locally finite type morphism carrying precisely the generic points of its source to the generic points of its target is finite over a dense open of the target, if it is quasi-compact or separated.

theorem exists_dense_open_isFinite {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] (hX : (genericPoints X).Finite) (hY : (genericPoints Y).Finite)
    (hgeneric : f ⁻¹' genericPoints Y = genericPoints X)
    (hqc_or_sep : QuasiCompact f ∨ IsSeparated f) :
    ∃ V : Y.Opens, Dense (V : Set Y) ∧ IsFinite (f ∣_ V)

Tag 0BAJ, a lemma

Tag 0BAJ in the Stacks Project.

AlgebraicGeometry.exists_dense_open_isIso_morphismRestrict_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/IsoOverDenseOpen.lean, line 79.

Stacks Project, Tag 0BAJ. A birational morphism between schemes with finitely many irreducible components is an isomorphism over a dense open subscheme of its target, provided it is quasi-compact or separated and provided it is locally of finite type with reduced target or locally of finite presentation.

theorem exists_dense_open_isIso_morphismRestrict_of_isBirational
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Finite (irreducibleComponents X)] [Finite (irreducibleComponents Y)]
    (hf : IsBirational f) (hqc_or_sep : QuasiCompact f ∨ IsSeparated f)
    (hfin : (LocallyOfFiniteType f ∧ IsReduced Y) ∨ LocallyOfFinitePresentation f) :
    ∃ V : Y.Opens, Dense (V : Set Y) ∧ IsIso (f ∣_ V)

Tag 02NX, a lemma

Tag 02NX in the Stacks Project.

AlgebraicGeometry.eq_genericPoint_iff_finite_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/GenericallyFiniteDominant.lean, line 233. The attribute's comment: “condition (4), restated as finiteness of the fibre over the generic point of the target, which is the hypothesis of Tag 02NW”.

Stacks Project, Tag 02NX, condition (4) as finiteness of the generic fibre. For a morphism locally of finite type between integral schemes, the generic point of the source is the only point above the generic point of the target exactly when that fibre is finite.

theorem eq_genericPoint_iff_finite_fibre :
    (∀ x : X, f x = genericPoint Y → x = genericPoint X) ↔
      (f ⁻¹' {genericPoint Y}).Finite

AlgebraicGeometry.exists_affineOpens_isFinite_iff_eq_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/GenericallyFiniteDominant.lean, line 257. The attribute's comment: “conditions (3) and (4)”.

Stacks Project, Tag 02NX, conditions (3) and (4). For a dominant morphism locally of finite type between integral schemes, finiteness on some pair of nonempty affine opens of the source and target is equivalent to the generic point of the source being the only point above the generic point of the target.

theorem exists_affineOpens_isFinite_iff_eq_genericPoint :
    (∃ (U : X.affineOpens) (V : Y.affineOpens) (hUV : U.1 ≤ f ⁻¹ᵁ V.1),
        (U.1 : Set X).Nonempty ∧ (V.1 : Set Y).Nonempty ∧
          IsFinite (f.resLE V.1 U.1 hUV)) ↔
      (∀ x : X, f x = genericPoint Y → x = genericPoint X)

AlgebraicGeometry.exists_affineOpen_isFinite_restrict_iff_eq_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/GenericallyFiniteDominant.lean, line 298. The attribute's comment: “condition (5)”.

Stacks Project, Tag 02NX, condition (5). For a dominant morphism locally of finite type between integral schemes which is separated or quasi-compact, finiteness over some nonempty affine open of the target is equivalent to the generic point of the source being the only point above the generic point of the target.

theorem exists_affineOpen_isFinite_restrict_iff_eq_genericPoint
    (hsep_or_qc : IsSeparated f ∨ QuasiCompact f) :
    (∃ V : Y.affineOpens, (V.1 : Set Y).Nonempty ∧ IsFinite (f ∣_ V.1)) ↔
      (∀ x : X, f x = genericPoint Y → x = genericPoint X)

AlgebraicGeometry.trdeg_functionField_eq_zero_of_eq_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/GenericallyFiniteDominant.lean, line 338. The attribute's comment: “the implication from condition (4) -- equivalently (3), or (5) -- to condition (1)”.

Stacks Project, Tag 02NX, the implication to condition (1). If the generic point of the source is the only point above the generic point of the target, then the induced extension of function fields has transcendence degree zero.

theorem trdeg_functionField_eq_zero_of_eq_genericPoint
    (h : ∀ x : X, f x = genericPoint Y → x = genericPoint X) :
    letI : Algebra Y.functionField X.functionField := (dominantFunctionFieldMap f).toAlgebra
    Algebra.trdeg Y.functionField X.functionField = 0

AlgebraicGeometry.trdeg_functionField_eq_zero_iff_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/GenericallyFiniteDominant.lean, line 400. The attribute's comment: “conditions (1) and (2): the extension of function fields has transcendence degree zero if and only if it is finite”.

Stacks Project, Tag 02NX, conditions (1) and (2). For a dominant morphism locally of finite type between integral schemes, the extension of function fields R(Y) ⊆ R(X) has transcendence degree zero exactly when it is finite.

theorem trdeg_functionField_eq_zero_iff_finite :
    letI : Algebra Y.functionField X.functionField := (dominantFunctionFieldMap f).toAlgebra
    Algebra.trdeg Y.functionField X.functionField = 0 ↔
      Module.Finite Y.functionField X.functionField

AlgebraicGeometry.eq_genericPoint_of_trdeg_functionField_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/GenericallyFiniteDominant.lean, line 416. The attribute's comment: “the implication from condition (1) to condition (4)”.

Stacks Project, Tag 02NX, the implication from condition (1) to condition (4). If the extension of function fields has transcendence degree zero, then the generic point of the source is the only point above the generic point of the target: on a pair of affine opens the point in question cuts out a prime contracting to the zero ideal, and over an algebraic extension of fraction fields such a prime is zero, which is the prime cut out by the generic point.

theorem eq_genericPoint_of_trdeg_functionField_eq_zero
    (h : letI : Algebra Y.functionField X.functionField :=
        (dominantFunctionFieldMap f).toAlgebra
      Algebra.trdeg Y.functionField X.functionField = 0) :
    ∀ x : X, f x = genericPoint Y → x = genericPoint X

AlgebraicGeometry.tfae_trdeg_functionField_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/GenericallyFiniteDominant.lean, line 444. The attribute's comment: “the equivalence of conditions (1), (2), (3) and (4)”. References: EGA II (6.1.8), “more general”.

Stacks Project, Tag 02NX, conditions (1)–(4). For a dominant morphism locally of finite type between integral schemes the following are equivalent: the extension of function fields R(Y) ⊆ R(X) has transcendence degree zero; that extension is finite; f is finite on some pair of nonempty affine opens U ⊆ X, V ⊆ Y with f(U) ⊆ V; the generic point of X is the only point of X above the generic point of Y.

theorem tfae_trdeg_functionField_eq_zero :
    letI : Algebra Y.functionField X.functionField := (dominantFunctionFieldMap f).toAlgebra
    List.TFAE
      [Algebra.trdeg Y.functionField X.functionField = 0,
        Module.Finite Y.functionField X.functionField,
        ∃ (U : X.affineOpens) (V : Y.affineOpens) (hUV : U.1 ≤ f ⁻¹ᵁ V.1),
          (U.1 : Set X).Nonempty ∧ (V.1 : Set Y).Nonempty ∧ IsFinite (f.resLE V.1 U.1 hUV),
        ∀ x : X, f x = genericPoint Y → x = genericPoint X]

Tag 02NY, a definition

Tag 02NY in the Stacks Project.

AlgebraicGeometry.degreeOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/FunctionFieldDegree.lean, line 88.

Stacks Project, Tag 02NY. The degree of X over Y for a morphism f : X ⟶ Y of integral schemes which is locally of finite type and dominant: the degree deg(X/Y) = [R(X) : R(Y)] of the extension of function fields induced by f.

This is a positive integer whenever that extension is finite, which is the case the source defines it in; see AlgebraicGeometry.degreeOver_pos.

noncomputable def degreeOver (f : X ⟶ Y) [IsIntegral X] [IsIntegral Y]
    [LocallyOfFiniteType f] [IsDominant f] : ℕ

Tag 02NZ, a lemma

Tag 02NZ in the Stacks Project.

AlgebraicGeometry.finrank_functionField_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/FunctionFieldDegree.lean, line 140.

Stacks Project, Tag 02NZ. The degree of a tower of dominant morphisms of integral schemes is the product of the two degrees: if the function field of X is finite over that of Y and the function field of Y is finite over that of Z, then [R(X) : R(Z)] = [R(X) : R(Y)] * [R(Y) : R(Z)].

theorem finrank_functionField_comp
    [FiniteDimensional Y.functionField X.functionField]
    [FiniteDimensional Z.functionField Y.functionField]
    (hf : algebraMap Y.functionField X.functionField = dominantFunctionFieldMap f)
    (hg : algebraMap Z.functionField Y.functionField = dominantFunctionFieldMap g)
    (hfg : algebraMap Z.functionField X.functionField = dominantFunctionFieldMap (f ≫ g)) :
    Module.finrank Z.functionField X.functionField =
      Module.finrank Y.functionField X.functionField *
        Module.finrank Z.functionField Y.functionField

Tag 0AAZ, a definition

Tag 0AAZ in the Stacks Project.

AlgebraicGeometry.IsModification, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Dominant/Modification.lean, line 45.

A morphism f : X' ⟶ X to an integral scheme is a modification if X' is integral and f is birational and proper.

public abbrev IsModification {X X' : Scheme.{u}} [IsIntegral X] (f : X' ⟶ X) : Prop

Tag 0AB0, a definition

Tag 0AB0 in the Stacks Project.

AlgebraicGeometry.IsAlteration, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Dominant/Alteration.lean, line 33.

A morphism to an integral scheme is an alteration if it is proper and dominant, its source is integral, and its restriction over some nonempty open of the target is finite.

public abbrev IsAlteration {Y X : Scheme.{u}} [IsIntegral X] (f : Y ⟶ X) : Prop

Sources

• Section 29.52, Tag 02NV
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.finite_preimage_singleton_iff_exists_affine_cover_isFinite · AlgebraicGeometry.finite_preimage_singleton_iff_exists_affine_opens_isFinite · AlgebraicGeometry.finite_preimage_singleton_iff_exists_affine_open_isFinite_restrict · AlgebraicGeometry.coordinatePoint_injective · AlgebraicGeometry.doubledPoint · AlgebraicGeometry.doubledPoint_genericPoint · AlgebraicGeometry.doubledPoint_quasiCompact · AlgebraicGeometry.doubledPoint_locallyOfFiniteType

Section29.53 The dimension formula#

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

Tag 02JU, a lemma

Tag 02JU in the Stacks Project.

AlgebraicGeometry.ringKrullDim_stalk_add_trdeg_residueField_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DimensionFormula/Formula.lean, line 100. The attribute's comment: “inequality”. References: EGA IV (13.3.4), “Inequality dim O_{X_j”; EGA IV (5.5.6), “partial”; EGA IV (5.5.8), “more general”; EGA IV (5.6.5), “(5.6.5.1), special case”.

The dimension formula for a dominant morphism f : X ⟶ S locally of finite type between integral schemes over a locally Noetherian base: dim 𝒪_{X, x} + trdeg_{κ(f x)} κ(x) ≤ dim 𝒪_{S, f x} + trdeg_{R(S)} R(X).

theorem ringKrullDim_stalk_add_trdeg_residueField_le
    [IsLocallyNoetherian S] [LocallyOfFiniteType f] [IsIntegral X] [IsIntegral S] [IsDominant f]
    (x : X) :
    letI : Algebra (S.residueField (f x)) (X.residueField x) :=
      (f.residueFieldMap x).hom.toAlgebra
    letI : Algebra S.functionField X.functionField := f.functionFieldMap.hom.toAlgebra
    ringKrullDim (X.presheaf.stalk x) +
        (Cardinal.toNat (Algebra.trdeg (S.residueField (f x)) (X.residueField x)) : WithBot ℕ∞)
      ≤ ringKrullDim (S.presheaf.stalk (f x)) +
        (Cardinal.toNat (Algebra.trdeg S.functionField X.functionField) : WithBot ℕ∞)

AlgebraicGeometry.ringKrullDim_stalk_add_trdeg_residueField_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/DimensionFormula/Formula.lean, line 119. The attribute's comment: “equality for a universally catenary base”. References: EGA IV (5.5.8), “special case”; EGA IV (5.6.5), “partial”.

Over a universally catenary base the dimension formula is an equality: dim 𝒪_{X, x} + trdeg_{κ(f x)} κ(x) = dim 𝒪_{S, f x} + trdeg_{R(S)} R(X).

theorem ringKrullDim_stalk_add_trdeg_residueField_eq
    [IsLocallyNoetherian S] [LocallyOfFiniteType f] [IsIntegral X] [IsIntegral S] [IsDominant f]
    (hS : Scheme.IsUniversallyCatenary S) (x : X) :
    letI : Algebra (S.residueField (f x)) (X.residueField x) :=
      (f.residueFieldMap x).hom.toAlgebra
    letI : Algebra S.functionField X.functionField := f.functionFieldMap.hom.toAlgebra
    ringKrullDim (X.presheaf.stalk x) +
        (Cardinal.toNat (Algebra.trdeg (S.residueField (f x)) (X.residueField x)) : WithBot ℕ∞)
      = ringKrullDim (S.presheaf.stalk (f x)) +
        (Cardinal.toNat (Algebra.trdeg S.functionField X.functionField) : WithBot ℕ∞)

AlgebraicGeometry.localDimension_add_trdeg_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/DimensionFormula.lean, line 400. The attribute's comment: “dimension-formula inequality”.

Stacks 02JU. The dimension formula for a dominant locally finite-type morphism of integral schemes over a locally Noetherian base: the dimension of the local ring at x plus the transcendence degree of κ(x)/κ(f x) is at most the dimension of the local ring at f x plus the transcendence degree of the function field extension.

theorem localDimension_add_trdeg_le {X S : Scheme.{u}} (f : X ⟶ S)
    [IsLocallyNoetherian S] [LocallyOfFiniteType f]
    [IsIntegral X] [IsIntegral S] [IsDominant f] (x : X) :
    letI := (dominantFunctionFieldMap f).toAlgebra
    letI := (f.residueFieldMap x).hom.toAlgebra
    ringKrullDim (X.presheaf.stalk x) +
        (Cardinal.toENat
          (Algebra.trdeg (S.residueField (f x)) (X.residueField x)) : WithBot ℕ∞) ≤
      ringKrullDim (S.presheaf.stalk (f x)) +
        (Cardinal.toENat (Algebra.trdeg S.functionField X.functionField) : WithBot ℕ∞)

AlgebraicGeometry.localDimension_add_trdeg_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/DimensionFormula.lean, line 417. The attribute's comment: “universally catenary equality”.

Stacks 02JU. Over a universally catenary base the dimension formula is an equality.

theorem localDimension_add_trdeg_eq {X S : Scheme.{u}} (f : X ⟶ S)
    [IsLocallyNoetherian S] [LocallyOfFiniteType f]
    [IsIntegral X] [IsIntegral S] [IsDominant f]
    (hS : Scheme.IsUniversallyCatenary S) (x : X) :
    letI := (dominantFunctionFieldMap f).toAlgebra
    letI := (f.residueFieldMap x).hom.toAlgebra
    ringKrullDim (X.presheaf.stalk x) +
        (Cardinal.toENat
          (Algebra.trdeg (S.residueField (f x)) (X.residueField x)) : WithBot ℕ∞) =
      ringKrullDim (S.presheaf.stalk (f x)) +
        (Cardinal.toENat (Algebra.trdeg S.functionField X.functionField) : WithBot ℕ∞)

Tag 0BAE, a lemma

Tag 0BAE in the Stacks Project.

AlgebraicGeometry.ringKrullDim_stalk_add_residueFieldTranscendenceDegree_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/DimensionFormula.lean, line 881. References: EGA IV (13.3.4), “partial”; EGA IV (5.5.6), “partial”; EGA IV (5.5.7), “more general”; EGA IV (5.5.8), “more general”; EGA IV (5.6.5), “more general”.

Stacks 0BAE. The general dimension formula: for a morphism f : X ⟶ S locally of finite type over a locally Noetherian scheme and a point x of X, dim 𝒪_{X,x} + trdeg_{κ(f x)} κ(x) ≤ dim 𝒪_{S,f x} + E, where E is the supremum of trdeg_{κ(f ξ)} κ(ξ) over the generic points ξ of the irreducible components of X containing x.

theorem ringKrullDim_stalk_add_residueFieldTranscendenceDegree_le {X S : Scheme.{u}}
    (f : X ⟶ S) (x : X)
    [IsLocallyNoetherian S] [LocallyOfFiniteType f] :
    ringKrullDim (X.presheaf.stalk x) + (residueFieldTranscendenceDegree f x : WithBot ℕ∞) ≤
      ringKrullDim (S.presheaf.stalk (f x)) +
        (genericResidueFieldTranscendenceDegreeAt f x : WithBot ℕ∞)

Tag 02JW, a lemma

Tag 02JW in the Stacks Project.

Stacks.Chow.relativeDimension_isDimensionFunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeDimension.lean, line 544. References: SGA 6 X (1.5), “special case”.

Stacks 02JW. A dimension function on a locally Noetherian universally catenary scheme propagates along every locally finite-type morphism by adding the transcendence degree of the residue-field extension: relativeDimension δ f is the underlying function of a dimension function on the source.

theorem relativeDimension_isDimensionFunction {X S : Scheme.{u}}
    [IsLocallyNoetherian S] (hS : Scheme.IsUniversallyCatenary S)
    (δ : DimensionFunction S) (f : X ⟶ S) [LocallyOfFiniteType f] :
    ∃ d : DimensionFunction X, ∀ x, d x = relativeDimension δ f x

Tag 02JX, a lemma

Tag 02JX in the Stacks Project.

AlgebraicGeometry.topologicalKrullDim_le_add_trdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/DimensionDominant.lean, line 162. The attribute's comment: “dimension inequality”.

Stacks Project, Tag 02JX. For a dominant morphism of integral schemes locally of finite type over a locally Noetherian base, the dimension of the source is at most the dimension of the target plus the transcendence degree of the extension of function fields.

theorem topologicalKrullDim_le_add_trdeg (f : X ⟶ Y) [IsLocallyNoetherian Y]
    [IsIntegral X] [IsIntegral Y] [IsDominant f] [LocallyOfFiniteType f] :
    letI := (functionFieldMap f).toAlgebra
    topologicalKrullDim X ≤ topologicalKrullDim Y +
      (Cardinal.toENat (Algebra.trdeg Y.functionField X.functionField) : WithBot ℕ∞)

AlgebraicGeometry.topologicalKrullDim_eq_add_trdeg_of_isClosedMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/DimensionDominant.lean, line 233. The attribute's comment: “equality for closed morphisms”.

Stacks Project, Tag 02JX. For a closed dominant morphism of integral schemes locally of finite type over a locally Noetherian base — in particular for a proper one — the bound on the dimension of the source is an equality.

theorem topologicalKrullDim_eq_add_trdeg_of_isClosedMap (f : X ⟶ Y) [IsLocallyNoetherian Y]
    [IsIntegral X] [IsIntegral Y] [IsDominant f] [LocallyOfFiniteType f] (hf : IsClosedMap f) :
    letI := (functionFieldMap f).toAlgebra
    topologicalKrullDim X = topologicalKrullDim Y +
      (Cardinal.toENat (Algebra.trdeg Y.functionField X.functionField) : WithBot ℕ∞)

Tag 0BAG, a lemma

Tag 0BAG in the Stacks Project.

AlgebraicGeometry.topologicalKrullDim_le_add_iSup_residueFieldTrdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteType/DimensionFormula.lean, line 920. References: EGA IV (5.6.6), “more general”.

Stacks 0BAG. The dimension of the source of a morphism locally of finite type over a locally Noetherian scheme is at most the dimension of the target plus the supremum of the residue-field transcendence degrees at the generic points of the irreducible components of the source.

theorem topologicalKrullDim_le_add_iSup_residueFieldTrdeg
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian Y] [LocallyOfFiniteType f] :
    topologicalKrullDim X ≤ topologicalKrullDim Y +
      ((⨆ ξ : genericPoints X, residueFieldTranscendenceDegree f ξ.1 : ℕ∞) : WithBot ℕ∞)

Sources

• Section 29.53, Tag 02JT
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.ringKrullDim_stalk_add_trdeg_residueField_le · AlgebraicGeometry.ringKrullDim_stalk_add_trdeg_residueField_eq · AlgebraicGeometry.localDimension_add_trdeg_le · AlgebraicGeometry.localDimension_add_trdeg_eq · AlgebraicGeometry.ringKrullDim_stalk_add_residueFieldTranscendenceDegree_le · Stacks.Chow.relativeDimension_isDimensionFunction · AlgebraicGeometry.topologicalKrullDim_le_add_trdeg · AlgebraicGeometry.topologicalKrullDim_eq_add_trdeg_of_isClosedMap

Section29.54 Relative normalization#

Section 29.54 of the Stacks Project, Tag 0BAK. 14 tags here are carried by 26 declarations of the repository (all in StacksFrontier) and 15 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BAK, the section

Tag 0BAK in the Stacks Project.

Stacks.RelativeNormalization.integralClosureSpectrum_isRelativeNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/IntegralClosureSpectrum.lean, line 352. References: EGA IV (18.10.10), “more general”; EGA IV (18.12.14), “partial”; EGA IV (8.12.3).

Relative normalization. Let f : Y ⟶ X be a quasi-compact and quasi-separated morphism of schemes, let 𝒪' ⊆ f_* 𝒪_Y be the integral closure of 𝒪_X in f_* 𝒪_Y, and let ν : X' = Spec_X(𝒪') ⟶ X be its relative spectrum, the normalization of X in Y. Then:

• f factors as f = ν ∘ f', where f' : Y ⟶ X' is the canonical morphism Y ⟶ Spec_X(f_* 𝒪_Y) followed by the morphism of relative spectra induced by the inclusion 𝒪' ⊆ f_* 𝒪_Y;
• ν is integral and f' is dominant;
• for every factorization f = π ∘ g with π : Z ⟶ X integral there is a unique h : X' ⟶ Z with h ∘ f' = g and π ∘ h = ν;
• consequently X' is uniquely isomorphic, under Y and over X, to the relative normalization f.normalization.

theorem integralClosureSpectrum_isRelativeNormalization :
    toIntegralClosureSpectrum f ≫ (integralClosureSpectrum f).toBase = f ∧
    toRelativeSpec f ≫ relativeSpectrumMapOfAlgebraHom (integralClosureSituation f)
        (pushforwardAlgebra f) (AlgebraSheaf.isQuasicoherent_pushforwardAlgebra f)
        (integralClosureAlgebraι (pushforwardAlgebra f)) = toIntegralClosureSpectrum f ∧
    IsIntegralHom (integralClosureSpectrum f).toBase ∧
    IsDominant (toIntegralClosureSpectrum f) ∧
    (∀ (Z : Scheme.{u}) (g : Y ⟶ Z) (π : Z ⟶ X), IsIntegralHom π → g ≫ π = f →
      ∃! h : (integralClosureSpectrum f).scheme ⟶ Z,
        toIntegralClosureSpectrum f ≫ h = g ∧ h ≫ π = (integralClosureSpectrum f).toBase) ∧
    ∃! e : (integralClosureSpectrum f).scheme ≅ f.normalization,
      toIntegralClosureSpectrum f ≫ e.hom = f.toNormalization ∧
        e.hom ≫ f.fromNormalization = (integralClosureSpectrum f).toBase

Tag 035F, a lemma

Tag 035F in the Stacks Project.

AlgebraicGeometry.Scheme.QuasicoherentAlgebra.mem_range_integralClosureAlgebraι_app_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/IntegralClosureAlgebra.lean, line 897. The attribute's comment: “the defining rule”.

A section of A over U lies in the integral closure of the structure sheaf exactly when its germ at every point of U is integral over the local ring of X at that point.

theorem mem_range_integralClosureAlgebraι_app_iff {X : Scheme.{u}}
    (A : X.QuasicoherentAlgebra) (U : Opens X) (s : A.right.presheaf.obj (.op U)) :
    s ∈ Set.range ((integralClosureAlgebraι A).right.hom.app (.op U)) ↔
      ∀ (x : X) (hx : x ∈ U),
        ((TopCat.Presheaf.stalkFunctor CommRingCat x).map A.hom.hom).hom.IsIntegralElem
          (A.right.presheaf.germ U x hx s)

AlgebraicGeometry.Scheme.QuasicoherentAlgebra.isQuasicoherent_integralClosureAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/IntegralClosureAlgebra.lean, line 912. The attribute's comment: “quasi-coherence”. References: EGA II (6.3.4), “quasi-coherence”.

The integral closure of the structure sheaf in a quasi-coherent sheaf of 𝒪_X-algebras is itself a quasi-coherent sheaf of 𝒪_X-algebras.

theorem isQuasicoherent_integralClosureAlgebra {X : Scheme.{u}} (A : X.QuasicoherentAlgebra)
    [(underlyingModule A).IsQuasicoherent] :
    (underlyingModule (integralClosureAlgebra A)).IsQuasicoherent

AlgebraicGeometry.Scheme.QuasicoherentAlgebra.range_stalkFunctor_map_integralClosureAlgebraι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/IntegralClosureAlgebra.lean, line 920. The attribute's comment: “stalks”. References: EGA II (6.3.2), “special case”.

The stalk at x of the integral closure of the structure sheaf in A is the integral closure of the local ring 𝒪_{X,x} in the stalk A_x.

theorem range_stalkFunctor_map_integralClosureAlgebraι {X : Scheme.{u}}
    (A : X.QuasicoherentAlgebra) (x : X) :
    letI : Algebra ((TopCat.Presheaf.stalkFunctor CommRingCat x).obj X.presheaf)
        ((TopCat.Presheaf.stalkFunctor CommRingCat x).obj A.right.presheaf) :=
      ((TopCat.Presheaf.stalkFunctor CommRingCat x).map A.hom.hom).hom.toAlgebra
    Set.range (((TopCat.Presheaf.stalkFunctor CommRingCat x).map
        (integralClosureAlgebraι A).right.hom).hom) =
      (integralClosure ((TopCat.Presheaf.stalkFunctor CommRingCat x).obj X.presheaf)
        ((TopCat.Presheaf.stalkFunctor CommRingCat x).obj A.right.presheaf) : Set _)

AlgebraicGeometry.Scheme.QuasicoherentAlgebra.range_integralClosureAlgebraι_app_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/IntegralClosureAlgebra.lean, line 955. The attribute's comment: “affine sections”. References: EGA II (6.3.4), “affine sections”.

Over an affine open U, the sections of the integral closure of the structure sheaf in a quasi-coherent A form the integral closure of 𝒪_X(U) in A(U).

theorem range_integralClosureAlgebraι_app_of_isAffineOpen {X : Scheme.{u}}
    (A : X.QuasicoherentAlgebra) [(underlyingModule A).IsQuasicoherent]
    (U : Opens X) (hU : IsAffineOpen U) :
    letI : Algebra (X.presheaf.obj (.op U)) (A.right.presheaf.obj (.op U)) :=
      (A.hom.hom.app (.op U)).hom.toAlgebra
    Set.range ((integralClosureAlgebraι A).right.hom.app (.op U)) =
      (integralClosure (X.presheaf.obj (.op U)) (A.right.presheaf.obj (.op U)) : Set _)

Tag 035G, a definition

Tag 035G in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.QuasicoherentAlgebra.integralClosureAlgebra, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/IntegralClosureAlgebra.lean, line 971 (StacksFrontier).

Tag 035I, a lemma

Tag 035I in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.normalization_universalProperty_iff_existsUnique_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Relative.lean, line 95. The attribute's comment: “universal_property”.

An integral factorization of a quasi-compact, quasi-separated morphism has the universal property of relative normalization if and only if it is uniquely isomorphic to the relative normalization, compatibly with both maps of the factorization.

theorem normalization_universalProperty_iff_existsUnique_iso
    {X Y Z : Scheme.{u}} (f : Y ⟶ X) [QuasiCompact f] [QuasiSeparated f]
    (i : Y ⟶ Z) (p : Z ⟶ X) [IsIntegralHom p] (hip : i ≫ p = f) :
    (∀ (T : Scheme.{u}) (j : Y ⟶ T) (q : T ⟶ X),
      IsIntegralHom q → j ≫ q = f →
        ∃! k : Z ⟶ T, i ≫ k = j ∧ k ≫ q = p) ↔
      ∃! e : Z ≅ f.normalization,
        i ≫ e.hom = f.toNormalization ∧ e.hom ≫ f.fromNormalization = p

AlgebraicGeometry.Scheme.Hom.normalizationDesc_universalProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Relative.lean, line 133. The attribute's comment: “normalization_over_intermediate”.

Relative normalization is unchanged after replacing the target by an intermediate scheme integral over it.

theorem normalizationDesc_universalProperty
    {X Y Z : Scheme.{u}} (f : Y ⟶ X) [QuasiCompact f] [QuasiSeparated f]
    (g : Y ⟶ Z) (p : Z ⟶ X) [IsIntegralHom p] (H : f = g ≫ p) :
    ∀ (T : Scheme.{u}) (j : Y ⟶ T) (q : T ⟶ Z),
      IsIntegralHom q → j ≫ q = g →
        ∃! k : f.normalization ⟶ T,
          f.toNormalization ≫ k = j ∧
            k ≫ q = f.normalizationDesc g p H

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.Hom.instIsIntegralHomFromNormalization registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Relative.lean, line 66 (StacksFrontier): “integral”.
• AlgebraicGeometry.Scheme.Hom.instIsDominantToNormalization registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Relative.lean, line 68 (StacksFrontier): “dominant”.
• AlgebraicGeometry.Scheme.Hom.normalizationDesc registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Relative.lean, line 72 (StacksFrontier): “universal_property”.
• AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationDesc registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Relative.lean, line 75 (StacksFrontier): “universal_property”.
• AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Relative.lean, line 78 (StacksFrontier): “universal_property”.
• AlgebraicGeometry.Scheme.Hom.normalization.hom_ext registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Relative.lean, line 81 (StacksFrontier): “universal_property”.

Tag 035J, a lemma

Tag 035J in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.normalizationMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Functorial.lean, line 55. The attribute's comment: “canonical morphism”.

The canonical morphism between relative normalizations induced by a commutative square.

noncomputable def normalizationMap : f₂.normalization ⟶ f₁.normalization

AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationMap, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Functorial.lean, line 65. The attribute's comment: “upper square”.

The canonical morphism between normalizations commutes with the maps from the source schemes.

lemma toNormalization_normalizationMap :
    f₂.toNormalization ≫ normalizationMap f₁ f₂ gY gX sq =
      gY ≫ f₁.toNormalization

AlgebraicGeometry.Scheme.Hom.normalizationMap_fromNormalization, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Functorial.lean, line 74. The attribute's comment: “lower square”.

The canonical morphism between normalizations commutes with the maps to the target schemes.

lemma normalizationMap_fromNormalization :
    normalizationMap f₁ f₂ gY gX sq ≫ f₁.fromNormalization =
      f₂.fromNormalization ≫ gX

AlgebraicGeometry.Scheme.Hom.normalizationMap_unique, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Functorial.lean, line 84. The attribute's comment: “uniqueness”.

A morphism between the relative normalizations that makes both squares commute is the canonical morphism.

lemma normalizationMap_unique (h : f₂.normalization ⟶ f₁.normalization)
    (h_source : f₂.toNormalization ≫ h = gY ≫ f₁.toNormalization)
    (h_target : h ≫ f₁.fromNormalization = f₂.fromNormalization ≫ gX) :
    h = normalizationMap f₁ f₂ gY gX sq

Tag 035K, a lemma

Tag 035K in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.Hom.normalizationPullback registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 350 (StacksFrontier): “the comparison morphism from the normalization of the base change to the base change of the normalization, for f quasi-compact and quasi-separated”.
• AlgebraicGeometry.Scheme.Hom.instIsIsoNormalizationPullbackOfSmooth registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 353 (StacksFrontier): “it is an isomorphism for a smooth base change, in particular for the inclusion of an open U”. References: SGA 3 X (8.9), “partial”.
• AlgebraicGeometry.instSmoothOfIsOpenImmersion registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 355 (StacksFrontier): “open immersions are smooth”. References: SGA 1 II (1.3), “more general”.

Tag 0BXA, a lemma

Tag 0BXA in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.normalization_fromNormalization_isIso, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Relative.lean, line 156.

The normalization of f.normalization in X is canonically isomorphic to f.normalization.

instance normalization_fromNormalization_isIso :
    IsIso (f.toNormalization.fromNormalization)

Tag 0AXP, a lemma

Tag 0AXP in the Stacks Project.

AlgebraicGeometry.exists_genericPoint_irreducibleComponent_mapping_to, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/RelativeGenericPoints.lean, line 42.

Every generic point of an irreducible component of the relative normalization of the target in the source is the image of a generic point of an irreducible component of the source.

public theorem exists_genericPoint_irreducibleComponent_mapping_to
    {X Y : Scheme.{u}} (f : Y ⟶ X) [QuasiCompact f] [QuasiSeparated f]
    {x : f.normalization} {Z : Set f.normalization}
    (hZ : Z ∈ irreducibleComponents f.normalization) (hx : IsGenericPoint x Z) :
    ∃ (y : Y) (T : Set Y),
      T ∈ irreducibleComponents Y ∧ IsGenericPoint y T ∧ f.toNormalization y = x

Tag 03GO, a lemma

Tag 03GO in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 117 (StacksFrontier): “the isomorphism of schemes”. References: EGA IV (18.10.8), “partial”; EGA IV (18.10.10), “partial”.
• AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso_inv_coprodDesc_fromNormalization registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 120 (StacksFrontier): “compatibility with the morphisms to the base”. References: EGA II (6.3.6), “more general”.
• AlgebraicGeometry.Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 123 (StacksFrontier): “compatibility with the dominant morphism from the first summand”.
• AlgebraicGeometry.Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 126 (StacksFrontier): “compatibility with the dominant morphism from the second summand”.

Tag 03GQ, a lemma

Tag 03GQ in the Stacks Project.

AlgebraicGeometry.isIntegral_app_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/SteinFactorization/UniversallyClosed.lean, line 64. The attribute's comment: “integrality of the pushed-forward structure sheaf”.

Stacks Project, Tag 03GQ. For a universally closed morphism of schemes f : X ⟶ S and an affine open U of S, the ring map Γ(S, U) ⟶ Γ(X, f⁻¹(U)) on sections is integral. This is the assertion that f_* 𝒪_X is integral over 𝒪_S.

Only universal closedness is needed; the quasi-compactness and quasi-separatedness of Tag 03GQ are what make f_* 𝒪_X a quasi-coherent algebra, not what make it integral.

theorem isIntegral_app_of_universallyClosed (f : X ⟶ S) [UniversallyClosed f] {U : S.Opens}
    (hU : IsAffineOpen U) : RingHom.IsIntegral (f.app U).hom

AlgebraicGeometry.isIntegralHom_toBase_pushforwardSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversallyClosed/IntegralPushforward.lean, line 113. The attribute's comment: “integral”.

For a quasi-separated, universally closed morphism f : X ⟶ S the sheaf of algebras f_* 𝒪_X is integral over 𝒪_S: the structure morphism Spec_S(f_* 𝒪_X) ⟶ S of its relative spectrum is an integral morphism.

An affine morphism is integral as soon as it is universally closed, and universal closedness is checked on the affine opens of S, where the structure morphism is the spectrum of the integral ring map Γ(S, U) ⟶ Γ(X, f⁻¹U).

theorem isIntegralHom_toBase_pushforwardSpectrum :
    IsIntegralHom (pushforwardSpectrum f).toBase

AlgebraicGeometry.normalizationIsoPushforwardSpectrum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversallyClosed/IntegralPushforward.lean, line 209. The attribute's comment: “normalization”.

For a quasi-separated, universally closed morphism f : X ⟶ S the normalization of S in X is isomorphic to the relative spectrum Spec_S(f_* 𝒪_X).

noncomputable def normalizationIsoPushforwardSpectrum :
    f.normalization ≅ (pushforwardSpectrum f).scheme

AlgebraicGeometry.toNormalization_normalizationIsoPushforwardSpectrum_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversallyClosed/IntegralPushforward.lean, line 216. The attribute's comment: “normalization: first factor”.

Under the identification of the normalization of S in X with Spec_S(f_* 𝒪_X), the canonical morphism X ⟶ f.normalization becomes the canonical morphism X ⟶ Spec_S(f_* 𝒪_X).

theorem toNormalization_normalizationIsoPushforwardSpectrum_hom :
    f.toNormalization ≫ (normalizationIsoPushforwardSpectrum f).hom = canonicalMorphism f

AlgebraicGeometry.normalizationIsoPushforwardSpectrum_hom_comp_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversallyClosed/IntegralPushforward.lean, line 223. The attribute's comment: “normalization: second factor”.

Under the identification of the normalization of S in X with Spec_S(f_* 𝒪_X), the structure morphism f.normalization ⟶ S becomes the structure morphism Spec_S(f_* 𝒪_X) ⟶ S.

theorem normalizationIsoPushforwardSpectrum_hom_comp_toBase :
    (normalizationIsoPushforwardSpectrum f).hom ≫ (pushforwardSpectrum f).toBase =
      f.fromNormalization

Stacks.RelativeSpec.normalizationIsoRelativeSpec, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/Normalization.lean, line 191. The attribute's comment: “comparison with relative normalization”.

Stacks Project, Tag 03GQ. For a quasi-separated and universally closed morphism f : X ⟶ S, the relative normalization of S in X is the relative spectrum of f_* 𝒪_X.

noncomputable def normalizationIsoRelativeSpec :
    f.normalization ≅ (gluedSpectrum (pushforwardSituation f)).scheme

Stacks.RelativeSpec.normalizationIsoRelativeSpec_hom_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/Normalization.lean, line 198. The attribute's comment: “comparison over the base”.

Stacks Project, Tag 03GQ. The comparison of the relative normalization with the relative spectrum of f_* 𝒪_X is an isomorphism over the base.

theorem normalizationIsoRelativeSpec_hom_toBase :
    (normalizationIsoRelativeSpec f).hom ≫
        (gluedSpectrum (pushforwardSituation f)).toBase = f.fromNormalization

Stacks.RelativeSpec.toNormalization_normalizationIsoRelativeSpec_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeSpec/Normalization.lean, line 209. The attribute's comment: “comparison of canonical source maps”.

Stacks Project, Tag 03GQ. The comparison of the relative normalization with the relative spectrum of f_* 𝒪_X carries the canonical morphism to the relative normalization to the canonical morphism of [Stacks, Tag 01LY]. Together with Stacks.RelativeSpec.normalizationIsoRelativeSpec_hom_toBase this says that the relative normalization of S in X is the factorization X ⟶ Spec_S(f_* 𝒪_X) ⟶ S.

theorem toNormalization_normalizationIsoRelativeSpec_hom :
    f.toNormalization ≫ (normalizationIsoRelativeSpec f).hom = toRelativeSpec f

Tag 035L, a lemma

Tag 035L in the Stacks Project.

AlgebraicGeometry.exists_iso_sigma_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/RelativeNormal.lean, line 517. The attribute's comment: “disjoint union of integral normal schemes”.

Stacks Project, Tag 035L. The normalization of Y in a normal scheme X whose quasi-compact opens have finitely many irreducible components is a disjoint union of integral normal schemes.

theorem exists_iso_sigma_normalization [IsNormal X]
    (hX : ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite) :
    ∃ (ι : Type u) (Z : ι → Scheme.{u}) (_ : ∀ i, IsNormal (Z i))
        (_ : ∀ i, AlgebraicGeometry.IsIntegral (Z i)), Nonempty (f.normalization ≅ ∐ Z)

AlgebraicGeometry.bijOn_irreducibleComponents_toNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/RelativeNormal.lean, line 529. The attribute's comment: “bijection on irreducible components”.

Stacks Project, Tag 035L. The dominant morphism from X to the normalization of Y in X carries irreducible components to irreducible components bijectively.

theorem bijOn_irreducibleComponents_toNormalization [IsNormal X]
    (hX : ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite) :
    Set.BijOn (fun C ↦ closure (f.toNormalization.base '' C))
      (irreducibleComponents X) (irreducibleComponents f.normalization)

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.Hom.instIsDominantToNormalization registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Relative.lean, line 70 (StacksFrontier): “dominance”.

Tag 0AVK, a lemma

Tag 0AVK in the Stacks Project.

AlgebraicGeometry.isFinite_fromNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/Basic.lean, line 164.

Stacks Project, Tag 0AVK. Let f : X ⟶ S be quasi-compact and quasi-separated with X reduced. If the quasi-compact opens of X have finitely many irreducible components, the residue field extension at every generic point of an irreducible component of X is finitely generated, and S is Nagata, then the normalization of S in X is finite over S.

theorem isFinite_fromNormalization
    {X S : Scheme.{u}} (f : X ⟶ S) (hS : IsNagataScheme S)
    [QuasiCompact f] [QuasiSeparated f] [IsReduced X]
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (hκ : ∀ x : genericPoints X,
      letI := (f.residueFieldMap x.1).hom.toAlgebra
      (⊤ : IntermediateField (S.residueField (f x.1)) (X.residueField x.1)).FG) :
    IsFinite f.fromNormalization

Tag 03GR, a lemma

Tag 03GR in the Stacks Project.

AlgebraicGeometry.isFinite_fromNormalization_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/Basic.lean, line 208.

Stacks Project, Tag 03GR. Let f : X ⟶ S be of finite type with X reduced and S Nagata. Then the normalization of S in X is finite over S.

theorem isFinite_fromNormalization_of_locallyOfFiniteType {X S : Scheme.{u}} (f : X ⟶ S)
    (hS : IsNagataScheme S) [LocallyOfFiniteType f] [QuasiCompact f] [IsReduced X] :
    haveI : IsLocallyNoetherian S :=
      ((isNagataScheme_iff_isLocallyNoetherian_and_isUniversallyJapaneseScheme S).mp hS).1
    IsFinite f.fromNormalization

Tag 0BXB, a lemma

Tag 0BXB in the Stacks Project.

AlgebraicGeometry.isDiscreteValuationRing_stalk_normalization_of_isEmpty_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/CodimensionOne.lean, line 234.

Stacks Project, Tag 0BXB. Let f : Y ⟶ X be of finite type with Y reduced and X Nagata, and let X' be the normalization of X in Y. If the local ring of X' at a point x' has Krull dimension one and the fibre of Y ⟶ X' over x' is empty, then that local ring is a discrete valuation ring.

theorem isDiscreteValuationRing_stalk_normalization_of_isEmpty_fiber {X Y : Scheme.{u}}
    (f : Y ⟶ X) [LocallyOfFiniteType f] [QuasiCompact f] [IsReduced Y] (hX : IsNagataScheme X) :
    haveI : IsLocallyNoetherian X :=
      ((isNagataScheme_iff_isLocallyNoetherian_and_isUniversallyJapaneseScheme X).mp hX).1
    ∀ x' : f.normalization,
      ringKrullDim (f.normalization.presheaf.stalk x') = 1 →
      IsEmpty (f.toNormalization.fiber x') →
      ∃ _ : IsDomain (f.normalization.presheaf.stalk x'),
        IsDiscreteValuationRing (f.normalization.presheaf.stalk x')

Sources

• Section 29.54, Tag 0BAK
• AxiomMath/Stacks at 5ed82d14

LeanStacks.RelativeNormalization.integralClosureSpectrum_isRelativeNormalization · AlgebraicGeometry.Scheme.QuasicoherentAlgebra.mem_range_integralClosureAlgebraι_app_iff · AlgebraicGeometry.Scheme.QuasicoherentAlgebra.isQuasicoherent_integralClosureAlgebra · AlgebraicGeometry.Scheme.QuasicoherentAlgebra.range_stalkFunctor_map_integralClosureAlgebraι · AlgebraicGeometry.Scheme.QuasicoherentAlgebra.range_integralClosureAlgebraι_app_of_isAffineOpen · AlgebraicGeometry.Scheme.QuasicoherentAlgebra.integralClosureAlgebra · AlgebraicGeometry.Scheme.Hom.normalization_universalProperty_iff_existsUnique_iso · AlgebraicGeometry.Scheme.Hom.normalizationDesc_universalProperty

Section29.55 Normalization#

Section 29.55 of the Stacks Project, Tag 035E. 14 tags here are carried by 28 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 035E, the section

Tag 035E in the Stacks Project.

AlgebraicGeometry.Scheme.exists_totalQuotientSheaf_iso_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/MeromorphicPushforward.lean, line 178. The attribute's comment: “K_X = f_* O_Y for X reduced”. References: EGA II (6.3.6), “special case”.

Let X be a reduced scheme whose quasi-compact opens have finitely many irreducible components, and let f : Y ⟶ X be the canonical morphism from the coproduct of the spectra of the residue fields at the generic points of X. Then the sheaf of meromorphic functions of X is f_* 𝒪_Y, as a sheaf of 𝒪_X-algebras.

theorem exists_totalQuotientSheaf_iso_pushforward [IsReduced X]
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    ∃ e : X.totalQuotientSheaf.presheaf ≅
        (fromGenericPointResidueFields X).base _* (genericPointResidueSpectrum X).presheaf,
      X.toTotalQuotientSheaf.hom ≫ e.hom = (fromGenericPointResidueFields X).c

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.quasiCompactFromGenericPointResidueFields, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/MeromorphicPushforward.lean, line 189 (StacksFrontier): “the morphism (035M) is quasi-compact”.
• AlgebraicGeometry.Scheme.quasiSeparatedFromGenericPointResidueFields, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/MeromorphicPushforward.lean, line 191 (StacksFrontier): “the morphism (035M) is quasi-separated”.
• Stacks.AlgebraicGeometry.GenericPointProduct.finiteComponentsOnCompactOpens_of_isLocallyNoetherian, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/MeromorphicPushforward.lean, line 193 (StacksFrontier): “a locally Noetherian scheme has locally finitely many irreducible components”.
• AlgebraicGeometry.Scheme.existsUnique_iso_normalizationScheme_reduction, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/MeromorphicPushforward.lean, line 195 (StacksFrontier): “the normalization of X is the normalization of X_red”.
• AlgebraicGeometry.Scheme.normalizationIsoMeromorphicSpectrum_hom_toBase, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/MeromorphicPushforward.lean, line 197 (StacksFrontier): “for X reduced, the normalization is the relative spectrum of the integral closure of O_X in K_X”.

Tag 035M, an equation

Tag 035M in the Stacks Project.

AlgebraicGeometry.Scheme.genericPointResidueSpectrum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/GenericPoints.lean, line 73. The attribute's comment: “the source scheme”.

Stacks Project, Tag 035M. The coproduct of the spectra of the residue fields at the generic points of the irreducible components of X.

noncomputable def genericPointResidueSpectrum (X : Scheme.{u}) : Scheme.{u}

AlgebraicGeometry.Scheme.fromGenericPointResidueFields, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/GenericPoints.lean, line 79. The attribute's comment: “the morphism”.

Stacks Project, Tag 035M. The canonical morphism from the spectra of the residue fields at the generic points of X to X.

noncomputable def fromGenericPointResidueFields (X : Scheme.{u}) :
    genericPointResidueSpectrum X ⟶ X

Tag 035N, a definition

Tag 035N in the Stacks Project.

AlgebraicGeometry.Scheme.normalization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Scheme.lean, line 118. References: EGA II (7.4.6), “special case”.

Stacks Project, Tag 035N. The normalization morphism of a scheme whose quasi-compact opens have finitely many irreducible components.

noncomputable abbrev normalization (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    normalizationScheme X hX ⟶ X

Tag 035O, a lemma

Tag 035O in the Stacks Project.

AlgebraicGeometry.Scheme.normalizationToReduction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/Reduction.lean, line 160. The attribute's comment: “canonical factor”.

Stacks Project, Tag 035O. The canonical factor of the normalization morphism of X through the reduction of X.

noncomputable def normalizationToReduction (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    X.normalizationScheme hX ⟶ X.nilradical.subscheme

AlgebraicGeometry.Scheme.normalizationToReduction_subschemeι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/Reduction.lean, line 169. The attribute's comment: “factorization”.

Stacks Project, Tag 035O. The normalization morphism of X is the composite of its canonical factor through the reduction with the closed immersion of the reduction.

theorem normalizationToReduction_subschemeι (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    X.normalizationToReduction hX ≫ X.nilradical.subschemeι = X.normalization hX

AlgebraicGeometry.Scheme.existsUnique_iso_normalizationScheme_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/Reduction.lean, line 293. The attribute's comment: “an iso over the reduction with the normalization of the reduction”.

Stacks Project, Tag 035O. The normalization of X is the normalization of the reduction of X: the canonical factor of the normalization morphism of X through the reduction is uniquely isomorphic, over the reduction, to the normalization morphism of the reduction, compatibly with the morphisms from the generic-point residue spectra.

theorem existsUnique_iso_normalizationScheme_reduction (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    ∃! e : X.normalizationScheme hX ≅
        X.nilradical.subscheme.normalizationScheme
          (X.finite_irreducibleComponents_reduction hX),
      (X.genericPointResidueSpectrumReductionIso.hom ≫ X.toNormalizationScheme hX) ≫ e.hom =
          X.nilradical.subscheme.toNormalizationScheme
            (X.finite_irreducibleComponents_reduction hX) ∧
        e.hom ≫ X.nilradical.subscheme.normalization
            (X.finite_irreducibleComponents_reduction hX) =
          X.normalizationToReduction hX

AlgebraicGeometry.Scheme.normalizationReductionIso_hom_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/Reduction.lean, line 353. The attribute's comment: “the iso of X^nu with (X_red)^nu is over X_red”.

Stacks Project, Tag 035O. The isomorphism of the normalization of X with the normalization of the reduction of X is an isomorphism over the reduction: it carries the normalization morphism of the reduction to the canonical factor of the normalization morphism of X through the reduction.

theorem normalizationReductionIso_hom_normalization (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    (X.normalizationReductionIso hX).hom ≫
        X.nilradical.subscheme.normalization
          (X.finite_irreducibleComponents_reduction hX) =
      X.normalizationToReduction hX

Tag 035P, a lemma

Tag 035P in the Stacks Project.

AlgebraicGeometry.preimageNormalizationIsoSpecIntegralClosure_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Affine.lean, line 707. The attribute's comment: “affine_normalization”.

Under AlgebraicGeometry.preimageNormalizationIsoSpecIntegralClosure, the restriction of the normalization morphism is the spectrum map induced by the inclusion into the integral closure.

theorem preimageNormalizationIsoSpecIntegralClosure_hom_comp
    {X : Scheme.{u}} [IsReduced X]
    (hX : ∀ V : X.Opens,
      IsCompact (V : Set X) → (irreducibleComponents V).Finite)
    {A : Type u} [CommRing A] (U : X.Opens)
    (e : Spec (.of A) ≅ U.toScheme) :
    (preimageNormalizationIsoSpecIntegralClosure hX U e).hom ≫
        Spec.map (CommRingCat.ofHom
          (algebraMap A (integralClosure A (FractionRing A)))) =
      (Scheme.normalization X hX ∣_ U) ≫ e.inv

AlgebraicGeometry.finite_minimalPrimes_of_affine_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/TotalFractionRing.lean, line 64. The attribute's comment: “minimal_primes”.

If every quasi-compact open of a scheme has finitely many irreducible components, then a ring presenting an affine open of that scheme has finitely many minimal primes.

theorem finite_minimalPrimes_of_affine_open
    {X : Scheme.{u}}
    {A : Type u} [CommRing A]
    (hX : ∀ (V : X.Opens), IsCompact (V : Set X) → (irreducibleComponents V).Finite)
    (U : X.Opens) (e : Spec (.of A) ≅ (U : Scheme)) :
    (minimalPrimes A).Finite

minimalPrimes.totalFractionRing_algEquiv_pi_fractionRing_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/TotalFractionRing.lean, line 136. The attribute's comment: “total_fraction_ring”. References: EGA II (6.5.1), “partial”.

The total ring of fractions of a reduced ring with finitely many minimal primes is the product of the fraction fields of its minimal-prime quotients.

theorem totalFractionRing_algEquiv_pi_fractionRing_quotient
    {A : Type*} [CommRing A] [IsReduced A] (hA : (minimalPrimes A).Finite) :
    letI : (p : minimalPrimes A) → Algebra A (FractionRing (A ⧸ (p : Ideal A))) :=
      fun p => ((algebraMap (A ⧸ (p : Ideal A)) (FractionRing (A ⧸ (p : Ideal A)))).comp
        (Ideal.Quotient.mk (p : Ideal A))).toAlgebra
    Nonempty (FractionRing A ≃ₐ[A]
      (∀ p : minimalPrimes A, FractionRing (A ⧸ (p : Ideal A))))

minimalPrimes.integralClosure_fractionRing_algEquiv_pi_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/TotalFractionRing.lean, line 208. The attribute's comment: “integral_closure_product”. References: EGA II (6.4.7), “integral closure product”.

The integral closure of a reduced ring in its total fraction ring is the product of the integral closures of its minimal-prime quotients in their fraction fields.

theorem integralClosure_fractionRing_algEquiv_pi_quotient
    {A : Type*} [CommRing A] [IsReduced A] (hA : (minimalPrimes A).Finite) :
    letI : (p : minimalPrimes A) →
        Algebra A
          (integralClosure (A ⧸ (p : Ideal A)) (FractionRing (A ⧸ (p : Ideal A)))) :=
      fun p =>
        ((algebraMap (A ⧸ (p : Ideal A))
          (integralClosure (A ⧸ (p : Ideal A))
            (FractionRing (A ⧸ (p : Ideal A))))).comp
          (Ideal.Quotient.mk (p : Ideal A))).toAlgebra
    Nonempty
      (integralClosure A (FractionRing A) ≃ₐ[A]
        (∀ p : minimalPrimes A,
          integralClosure (A ⧸ (p : Ideal A)) (FractionRing (A ⧸ (p : Ideal A)))))

Tag 0C3B, a lemma

Tag 0C3B in the Stacks Project.

Stacks.NormalizationStalkAmbient.normalizationStalkAlgEquivIntegralClosureMinimalPrimes, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MinimalPrimeResidueLocalization/Stalk.lean, line 87. The attribute's comment: “the product of the minimal-prime residue fields”.

The stalk of the pushforward of the structure sheaf of the normalization is canonically isomorphic, as an 𝒪_{X,x}-algebra, to the integral closure of 𝒪_{X,x} in the product of the residue fields of its minimal primes.

public noncomputable def
    normalizationStalkAlgEquivIntegralClosureMinimalPrimes (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (x : X) :
    letI : Algebra (X.presheaf.stalk x) (normalizationPushforwardStalk X hX x) :=
      normalizationPushforwardStalkAlgebra X hX x
    letI : Algebra (X.presheaf.stalk x)
        (minimalPrimeResidueFieldProduct (X.presheaf.stalk x)) :=
      (minimalPrimeResidueFieldProductHom (X.presheaf.stalk x)).toAlgebra
    normalizationPushforwardStalk X hX x ≃ₐ[X.presheaf.stalk x]
      integralClosure (X.presheaf.stalk x)
        (minimalPrimeResidueFieldProduct (X.presheaf.stalk x))

Stacks.NormalizationStalkAmbient.normalizationStalkAlgEquivIntegralClosureFractionRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MinimalPrimeResidueLocalization/Stalk.lean, line 106. The attribute's comment: “the total ring of fractions of the reduction”.

The stalk of the pushforward of the structure sheaf of the normalization is canonically isomorphic, as an 𝒪_{X,x}-algebra, to the integral closure of 𝒪_{X,x} in the total ring of fractions of its reduction.

public noncomputable def
    normalizationStalkAlgEquivIntegralClosureFractionRing (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (x : X) :
    letI : Algebra (X.presheaf.stalk x) (normalizationPushforwardStalk X hX x) :=
      normalizationPushforwardStalkAlgebra X hX x
    letI : Algebra (X.presheaf.stalk x)
        (FractionRing (X.presheaf.stalk x ⧸ nilradical (X.presheaf.stalk x))) :=
      (reductionFractionRingHom (X.presheaf.stalk x)).toAlgebra
    normalizationPushforwardStalk X hX x ≃ₐ[X.presheaf.stalk x]
      integralClosure (X.presheaf.stalk x)
        (FractionRing (X.presheaf.stalk x ⧸ nilradical (X.presheaf.stalk x)))

AlgebraicGeometry.Scheme.normalizationPushforwardStalkEquivIntegralClosureReductionFractionRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Stalk.lean, line 618. The attribute's comment: “the total ring of fractions of the reduction”.

The stalk of the pushforward of the structure sheaf of the normalization is canonically isomorphic, as an 𝒪_{X,x}-algebra, to the integral closure of 𝒪_{X,x} in the total ring of fractions of its reduction.

public noncomputable def
    normalizationPushforwardStalkEquivIntegralClosureReductionFractionRing
    (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (x : X) :
    let A := X.presheaf.stalk x
    letI : Algebra A (normalizationPushforwardStalk X hX x) :=
      normalizationPushforwardStalkAlgebra X hX x
    letI : Algebra A (FractionRing (A ⧸ _root_.nilradical A)) :=
      (Stacks.NormalizationStalkAmbient.reductionFractionRingHom A).toAlgebra
    normalizationPushforwardStalk X hX x ≃ₐ[A]
      integralClosure A (FractionRing (A ⧸ _root_.nilradical A))

AlgebraicGeometry.Scheme.normalizationPushforwardStalkEquivIntegralClosureMinimalPrimeResidueFields, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Stalk.lean, line 698. The attribute's comment: “the product of the minimal-prime residue fields”.

The stalk of the pushforward of the structure sheaf of the normalization is canonically isomorphic, as an 𝒪_{X,x}-algebra, to the integral closure of 𝒪_{X,x} in the product of the residue fields of its minimal primes.

public noncomputable def
    normalizationPushforwardStalkEquivIntegralClosureMinimalPrimeResidueFields
    (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (x : X) :
    let A := X.presheaf.stalk x
    letI (p : minimalPrimes A) : p.1.IsPrime := p.2.1.1
    letI : Algebra A (normalizationPushforwardStalk X hX x) :=
      normalizationPushforwardStalkAlgebra X hX x
    letI : Algebra A (minimalPrimes.residueFieldProduct A) :=
      (minimalPrimes.residueFieldProductHom A).toAlgebra
    normalizationPushforwardStalk X hX x ≃ₐ[A]
      integralClosure A (minimalPrimes.residueFieldProduct A)

Stacks.StalkMinimalPrimes.Basic.finite_minimalPrimes_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StalkMinimalPrimes/Basic.lean, line 60. The attribute's comment: “finiteness of the minimal primes”.

If every quasi-compact open of X has finitely many irreducible components, the local ring of X at x has only finitely many minimal primes.

public theorem finite_minimalPrimes_stalk (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (x : X) : (minimalPrimes (X.presheaf.stalk x)).Finite

Tag 035Q, a lemma

Tag 035Q in the Stacks Project.

AlgebraicGeometry.Scheme.exists_iso_sigma_isIntegral_isNormal_normalizationScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Components.lean, line 510. The attribute's comment: “normalization_disjoint_union_of_integral_normal”.

Stacks Project, Tag 035Q. The normalization of a scheme whose quasi-compact opens have finitely many irreducible components is a disjoint union of integral normal schemes: it is isomorphic to the coproduct of the normalizations of its reduced irreducible components, and each of those is integral and normal.

theorem exists_iso_sigma_isIntegral_isNormal_normalizationScheme
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    ∃ (ι : Type u) (Y : ι → Scheme.{u})
        (_ : ∀ i, IsNormal (Y i)) (_ : ∀ i, IsIntegral (Y i)),
      Nonempty (X.normalizationScheme hX ≅ ∐ Y)

AlgebraicGeometry.exists_normalizationFactorization_of_integral_of_birational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/IntegralBirational.lean, line 315. The attribute's comment: “normalization_integral_birational”.

Stacks Project, Tag 035Q. An integral morphism which is birational over every quasi-compact open does not change the normalization.

theorem exists_normalizationFactorization_of_integral_of_birational
    {X X' : Scheme.{u}} (hX : ∀ U : X.Opens, IsCompact (U : Set X) →
      (irreducibleComponents U).Finite) (α : X' ⟶ X) [IsIntegralHom α]
    (hcomponents : ∀ U : X.Opens, IsCompact (U : Set X) →
      (irreducibleComponents (α ⁻¹ᵁ U)).Finite)
    (hbirational : ∀ U : X.Opens, IsCompact (U : Set X) →
      IsBirational (α ∣_ U)) :
    ∃ (hX' : ∀ V : X'.Opens, IsCompact (V : Set X') →
        (irreducibleComponents V).Finite)
      (g : Scheme.normalizationScheme X hX ⟶ X')
      (e : Scheme.normalizationScheme X hX ≅
        Scheme.normalizationScheme X' hX'),
      g ≫ α = Scheme.normalization X hX ∧
        e.hom ≫ Scheme.normalization X' hX' = g

AlgebraicGeometry.Scheme.isIntegralHom_surjective_bijOn_irreducibleComponents_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/SurjectiveComponents.lean, line 143. The attribute's comment: “normalization_integral_surjective_bijection_on_components”.

Stacks Project, Tag 035Q. Part (2). Let X be a scheme such that every quasi-compact open of X has finitely many irreducible components. Then the normalization morphism ν : X^ν ⟶ X is integral, it is surjective, and it induces a bijection on irreducible components: sending an irreducible component of X^ν to the closure of its image under ν is a bijection onto the set of irreducible components of X.

Integrality is AlgebraicGeometry.Scheme.isIntegralHom_normalization (Tag 035I), surjectivity is AlgebraicGeometry.Scheme.surjective_normalization, and the bijection on components is AlgebraicGeometry.Scheme.bijOn_irreducibleComponents_normalization, which rests on Tags 035O and 0BXC.

theorem isIntegralHom_surjective_bijOn_irreducibleComponents_normalization
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    IsIntegralHom (X.normalization hX) ∧ Surjective (X.normalization hX) ∧
      Set.BijOn (fun D ↦ closure ((X.normalization hX).base '' D))
        (irreducibleComponents (X.normalizationScheme hX)) (irreducibleComponents X)

AlgebraicGeometry.Scheme.existsUnique_lift_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/UniversalProperty.lean, line 793. The attribute's comment: “normalization_universal_property”. References: EGA II (6.3.9), “special case”; EGA IV (8.12.11), “special case”.

Stacks Project, Tag 035Q part (4). A morphism to X from a normal scheme each of whose irreducible components dominates an irreducible component of X factors uniquely through the normalization of X.

theorem existsUnique_lift_normalization {X Z : Scheme.{u}}
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (f : Z ⟶ X) [IsNormal Z]
    (hgeneric : ∀ η : genericPoints Z, f η.1 ∈ genericPoints X) :
    ∃! g : Z ⟶ X.normalizationScheme hX, g ≫ X.normalization hX = f

Tag 0CDV, a lemma

Tag 0CDV in the Stacks Project.

AlgebraicGeometry.Scheme.exists_iso_normalizationScheme_sigma_reducedComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Components.lean, line 476.

Stacks Project, Tag 0CDV. Let X be a scheme whose quasi-compact opens have finitely many irreducible components, and give each irreducible component of X its reduced induced closed subscheme structure. Then the coproduct of the normalizations of those components, with its canonical morphism to X, is the normalization of X.

theorem exists_iso_normalizationScheme_sigma_reducedComponent
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    ∃ e : (∐ fun Z : irreducibleComponents X ↦ (X.reducedComponent Z).normalizationScheme
        (X.finite_irreducibleComponents_reducedComponent Z)) ≅ X.normalizationScheme hX,
      e.hom ≫ X.normalization hX =
        Sigma.desc fun Z : irreducibleComponents X ↦
          (X.reducedComponent Z).normalization
            (X.finite_irreducibleComponents_reducedComponent Z) ≫ X.reducedComponentι Z

Tag 0BXC, a lemma

Tag 0BXC in the Stacks Project.

AlgebraicGeometry.Scheme.isBirational_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBirational/Basic.lean, line 158.

Stacks Project, Tag 0BXC. The normalization morphism of a reduced scheme whose quasi-compact opens have finitely many irreducible components is birational.

theorem isBirational_normalization
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    IsBirational (X.normalization hX)

Tag 0AB1, a lemma

Tag 0AB1 in the Stacks Project.

AlgebraicGeometry.isIso_of_isIntegralHom_of_isBirational_of_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/BirationalIsIso.lean, line 107. References: EGA IV (8.12.10.1), “more general”; EGA II (6.1.15); EGA II (8.11.2), “special case”; EGA IV (17.15.14.1), “(i), special case”; EGA IV (8.12.10), “special case”.

Stacks Project, Tag 0AB1. An integral birational morphism of integral schemes whose target is normal is an isomorphism.

public theorem isIso_of_isIntegralHom_of_isBirational_of_isNormal
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegral X] [IsIntegral Y]
    [IsIntegralHom f] [IsNormal Y] (hf : IsBirational f) :
    IsIso f

Tag 0H7D, a lemma

Tag 0H7D in the Stacks Project.

AlgebraicGeometry.Scheme.isIso_normalization_iff_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/Normal.lean, line 378.

Stacks Project, Tag 0H7D. The normalization morphism of a scheme whose quasi-compact opens have finitely many irreducible components is an isomorphism if and only if the scheme is normal.

theorem isIso_normalization_iff_isNormal (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    IsIso (X.normalization hX) ↔ IsNormal X

Tag 035R, a lemma

Tag 035R in the Stacks Project.

AlgebraicGeometry.normalization_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/Japanese.lean, line 95.

Stacks Project, Tag 035R. The normalization morphism of an integral Japanese scheme is finite.

theorem normalization_isFinite (X : Scheme.{u}) [IsIntegral X]
    (hX : IsJapaneseScheme X) :
    let hfinite : ∀ U : X.Opens,
        IsCompact (U : Set X) → (irreducibleComponents U).Finite := by
      intro U _
      cases isEmpty_or_nonempty U with
      | inl hU =>
          rw [Set.finite_def]
          let : IsEmpty U := hU
          exact ⟨⟨∅, fun C ↦ isEmptyElim (C.2.1.nonempty.some)⟩⟩
      | inr hU =>
          let : Nonempty U := hU
          rw [irreducibleComponents_eq_singleton]
          exact Set.finite_singleton _
    IsFinite (Scheme.normalization X hfinite)

Tag 035S, a lemma

Tag 035S in the Stacks Project.

AlgebraicGeometry.Scheme.isFinite_normalization_of_isNagataScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NagataNormalization/Basic.lean, line 252.

Stacks Project, Tag 035S. The normalization morphism ν : X^ν ⟶ X of a Nagata scheme X is finite.

A Nagata scheme is locally Noetherian, so each of its quasi-compact opens is a Noetherian space and has finitely many irreducible components; the Nagata hypothesis therefore both forms the normalization morphism and makes it finite.

theorem isFinite_normalization_of_isNagataScheme {X : Scheme.{u}} (hNagata : IsNagataScheme X) :
    IsFinite (X.normalization (finite_irreducibleComponents_of_isNagataScheme X hNagata))

Tag 0GIQ, a lemma

Tag 0GIQ in the Stacks Project.

AlgebraicGeometry.Scheme.universalHomeomorphism_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Normalization/UniversalHomeomorphism.lean, line 94. References: EGA 0 (23.2.2), “sufficiency + homeo”; SGA 3 X (5.14.0), “univ. homeomorphism”; SGA 4 VIII (1.3), “1.3 c), special case”.

Stacks Project, Tag 0GIQ. The normalization morphism of an irreducible, geometrically unibranch scheme is a universal homeomorphism.

public theorem universalHomeomorphism_normalization (X : Scheme.{u}) [IrreducibleSpace X]
    (hX : IsGeometricallyUnibranch X) :
    UniversalHomeomorphism
      (normalization X (finite_irreducibleComponents_of_irreducibleSpace X))

Sources

• Section 29.55, Tag 035E
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Scheme.exists_totalQuotientSheaf_iso_pushforward · AlgebraicGeometry.Scheme.quasiCompactFromGenericPointResidueFields · AlgebraicGeometry.Scheme.quasiSeparatedFromGenericPointResidueFields · Stacks.AlgebraicGeometry.GenericPointProduct.finiteComponentsOnCompactOpens_of_isLocallyNoetherian · AlgebraicGeometry.Scheme.existsUnique_iso_normalizationScheme_reduction · AlgebraicGeometry.Scheme.normalizationIsoMeromorphicSpectrum_hom_toBase · AlgebraicGeometry.Scheme.genericPointResidueSpectrum · AlgebraicGeometry.Scheme.fromGenericPointResidueFields

Section29.56 Weak normalization#

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

Tag 0H3J, a lemma

Tag 0H3J in the Stacks Project.

AlgebraicGeometry.relativeWeakNormalization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/RelativeWeakNormalization.lean, line 251. The attribute's comment: “the algebra”.

The relative weak normalization of A in B: the largest A-subalgebra of B whose spectrum is a universal homeomorphism over Spec(A).

def relativeWeakNormalization (A B : Type u) [CommRing A] [CommRing B] [Algebra A B] :
    Subalgebra A B

AlgebraicGeometry.relativeWeakNormalization_isUniversalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/RelativeWeakNormalization.lean, line 260. The attribute's comment: “part (1)”.

If Spec(B) → Spec(A) is dominant, the relative weak normalization has spectrum universally homeomorphic to Spec(A).

theorem relativeWeakNormalization_isUniversalHomeomorphism
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (_h : IsDominant (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op)) :
    UniversalHomeomorphism
      (Scheme.Spec.map
        (CommRingCat.ofHom (algebraMap A (relativeWeakNormalization A B))).op)

AlgebraicGeometry.range_le_relativeWeakNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/RelativeWeakNormalization.lean, line 271. The attribute's comment: “part (2)”.

The image of every intermediate A-algebra universally homeomorphic over Spec(A) is contained in the relative weak normalization.

theorem range_le_relativeWeakNormalization
    (A B C : Type u) [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C]
    (g : C →ₐ[A] B)
    (_hB : IsDominant (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op))
    (hC : UniversalHomeomorphism
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A C)).op)) :
    g.range ≤ relativeWeakNormalization A B

Tag 0H3K, a lemma

Tag 0H3K in the Stacks Project.

AlgebraicGeometry.relativeWeakNormalization_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/Localization.lean, line 595.

Relative weak normalization commutes with localization at a submonoid of the base.

public theorem relativeWeakNormalization_localization
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (h : IsDominant (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op))
    (S : Submonoid A) :
    let f : Localization S →+* Localization (S.map (algebraMap A B)) :=
      IsLocalization.map (Localization (S.map (algebraMap A B))) (algebraMap A B)
        S.le_comap_map
    let _ : Algebra (Localization S) (Localization (S.map (algebraMap A B))) := f.toAlgebra
    Algebra.adjoin (Localization S)
        (algebraMap B (Localization (S.map (algebraMap A B))) ''
          (relativeWeakNormalization A B : Set B)) =
      relativeWeakNormalization (Localization S)
    (Localization (S.map (algebraMap A B)))

Tag 0H3L, a lemma

Tag 0H3L in the Stacks Project.

AlgebraicGeometry.relativeSeminormalization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/RelativeSeminormalization.lean, line 466. The attribute's comment: “the algebra”.

The relative seminormalization of A in B, for a dominant map Spec B ⟶ Spec A.

public noncomputable def relativeSeminormalization
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (_hdom : IsDominant
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op)) :
    Subalgebra A B

AlgebraicGeometry.relativeSeminormalization_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/RelativeSeminormalization.lean, line 478. The attribute's comment: “part (1), universal homeomorphism”.

The spectrum of the relative seminormalization is universally homeomorphic to the spectrum of the base.

public theorem relativeSeminormalization_universalHomeomorphism
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (hdom : IsDominant
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op)) :
    UniversalHomeomorphism
      (Scheme.Spec.map (CommRingCat.ofHom
        (algebraMap A (relativeSeminormalization A B hdom))).op)

AlgebraicGeometry.relativeSeminormalization_residueFieldMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/RelativeSeminormalization.lean, line 489. The attribute's comment: “part (1), residue fields”.

The relative seminormalization induces isomorphisms on all residue fields.

public theorem relativeSeminormalization_residueFieldMap_isIso
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (hdom : IsDominant
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op)) :
    let f := Scheme.Spec.map (CommRingCat.ofHom
      (algebraMap A (relativeSeminormalization A B hdom))).op
    ∀ x, IsIso (f.residueFieldMap x)

AlgebraicGeometry.map_mem_relativeSeminormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/RelativeSeminormalization.lean, line 501. The attribute's comment: “part (2)”.

Every intermediate algebra universally homeomorphic to the base and with unchanged residue fields maps into the relative seminormalization.

public theorem map_mem_relativeSeminormalization
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (hdom : IsDominant
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op))
    {C : Type u} [CommRing C] [Algebra A C] (g : C →ₐ[A] B)
    [UniversalHomeomorphism
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A C)).op)]
    (hres : ∀ x, IsIso ((Scheme.Spec.map
      (CommRingCat.ofHom (algebraMap A C)).op).residueFieldMap x)) :
    ∀ c, g c ∈ relativeSeminormalization A B hdom

Tag 0H3M, a lemma

Tag 0H3M in the Stacks Project.

AlgebraicGeometry.mem_relativeSeminormalization_localization_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/SeminormalizationLocalization.lean, line 485.

An element of the relative seminormalization after localization is exactly a fraction whose numerator belongs to the original relative seminormalization.

public theorem mem_relativeSeminormalization_localization_iff
    (A B Aₛ Bₛ : Type u) [CommRing A] [CommRing B] [CommRing Aₛ] [CommRing Bₛ]
    [Algebra A B] (S : Submonoid A)
    [Algebra A Aₛ] [IsLocalization S Aₛ]
    [Algebra B Bₛ] [IsLocalization (S.map (algebraMap A B)) Bₛ]
    [Algebra A Bₛ] [IsScalarTower A B Bₛ]
    [Algebra Aₛ Bₛ] [IsScalarTower A Aₛ Bₛ]
    (hdom : IsDominant
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap A B)).op))
    (hdomₛ : IsDominant
      (Scheme.Spec.map (CommRingCat.ofHom (algebraMap Aₛ Bₛ)).op))
    (x : Bₛ) :
    x ∈ relativeSeminormalization Aₛ Bₛ hdomₛ ↔
      ∃ (b : B), b ∈ relativeSeminormalization A B hdom ∧
        ∃ s : S, x = IsLocalization.mk' Bₛ b
          ⟨algebraMap A B s.1, Submonoid.mem_map.mpr ⟨s.1, s.2, rfl⟩⟩

Tag 0H3N, a lemma

Tag 0H3N in the Stacks Project.

AlgebraicGeometry.exists_initial_universalHomeomorphismFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/RelativeInitial.lean, line 1150. The attribute's comment: “weak_initial”.

Relative weak normalization ([Stacks, Tag 0H3N]). A quasi-compact, quasi-separated, dominant morphism f : Y ⟶ X has an initial factorization Y ⟶ X' ⟶ X with X' ⟶ X a universal homeomorphism, and this factorization is glued from the affine relative weak normalizations.

public theorem exists_initial_universalHomeomorphismFactorization
    {Y X : Scheme.{u}} (f : Y ⟶ X) [QuasiCompact f] [QuasiSeparated f]
    [IsDominant f] :
    ∃ F : UniversalHomeomorphismFactorization f,
      Nonempty (Limits.IsInitial F) ∧ Nonempty F.AffineGluingData

AlgebraicGeometry.weakNormalization_isPullback_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeWeakNormalizationOpen/Basic.lean, line 732. The attribute's comment: “weak_open”.

Relative weak normalization commutes with restriction to an open subscheme of the target, as a factorization of the restricted morphism.

public theorem weakNormalization_isPullback_open
    {Y X : Scheme.{u}} (f : Y ⟶ X) [QuasiCompact f] [QuasiSeparated f]
    [IsDominant f] (U : X.Opens) :
    letI : IsDominant (f ∣_ U) := IsZariskiLocalAtTarget.restrict (‹IsDominant f›) U
    let F := weakNormalizationFactorization f
    let F_U := weakNormalizationFactorization (f ∣_ U)
    ∃! h : F_U.middle ⟶ F.middle,
      IsPullback h F_U.toBase F.toBase U.ι ∧
      F_U.toMiddle ≫ h = (f ⁻¹ᵁ U).ι ≫ F.toMiddle

AlgebraicGeometry.exists_initial_subintegralFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Seminormalization/SeminormalizationInitial/Initiality.lean, line 536. The attribute's comment: “part (2), the seminormalization factorization”.

The category of factorizations through universal homeomorphisms inducing isomorphisms on residue fields has an initial object.

public theorem exists_initial_subintegralFactorization
    {Y X : Scheme.{u}} (f : Y ⟶ X) [QuasiCompact f] [QuasiSeparated f]
    [IsDominant f] :
    ∃ F : SubintegralFactorization f, Nonempty (Limits.IsInitial F)

AlgebraicGeometry.existsUnique_isPullback_seminormalizationFactorization_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Seminormalization/SeminormalizationInitial/OpenRestriction.lean, line 395. The attribute's comment: “part (3), compatibility with restriction to opens”.

Stacks Project, Tag 0H3N. Formation of the relative seminormalization factorization commutes with base change to an open subscheme of the target: the intermediate scheme of the factorization of f ∣_ U is the restriction of the intermediate scheme of the factorization of f, by a unique morphism compatible with both legs.

public theorem existsUnique_isPullback_seminormalizationFactorization_restrict
    {Y X : Scheme.{u}} (f : Y ⟶ X) [QuasiCompact f] [QuasiSeparated f]
    [IsDominant f] (U : X.Opens) :
    letI : IsDominant (f ∣_ U) := IsZariskiLocalAtTarget.restrict (‹IsDominant f›) U
    ∃! h : (seminormalizationFactorization (f ∣_ U)).middle ⟶
        (seminormalizationFactorization f).middle,
      IsPullback h (seminormalizationFactorization (f ∣_ U)).toBase
          (seminormalizationFactorization f).toBase U.ι ∧
        (seminormalizationFactorization (f ∣_ U)).toMiddle ≫ h =
          (f ⁻¹ᵁ U).ι ≫ (seminormalizationFactorization f).toMiddle

Tag 0H3P, a definition

Tag 0H3P in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.seminormalizationFactorization, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Seminormalization/RelativeSeminormalizationFactorization.lean, line 28 (StacksFrontier): “part (1)”.
• AlgebraicGeometry.weakNormalizationFactorization, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Seminormalization/RelativeSeminormalizationFactorization.lean, line 30 (StacksFrontier): “part (2)”.

Tag 0H3Q, a lemma

Tag 0H3Q in the Stacks Project.

AlgebraicGeometry.existsUnique_iso_seminormalization_seminormalizationFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/SeminormalizationInNormalization.lean, line 169. The attribute's comment: “the seminormalization of X in its normalization agrees with the seminormalization of X; the only hypothesis is the tag's own assumption hX that every quasi-compact open of X has finitely many irreducible components, which is what makes the normalization of X exist”.

Stacks Project, Tag 0H3Q. If every quasi-compact open of X has finitely many irreducible components, the seminormalization of X in its normalization is canonically isomorphic over X to the seminormalization of X.

theorem existsUnique_iso_seminormalization_seminormalizationFactorization (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    letI := Scheme.quasiCompactFromGenericPointResidueFields X hX
    letI := Scheme.quasiSeparatedFromGenericPointResidueFields X
    letI := Scheme.normalization_isDominant X hX
    ∃! e : (seminormalizationFactorization (Scheme.normalization X hX)).middle ≅
        X.seminormalization,
      e.hom ≫ X.seminormalizationHom =
        (seminormalizationFactorization (Scheme.normalization X hX)).toBase

Tag 0H3R, a definition

Tag 0H3R in the Stacks Project.

AlgebraicGeometry.Scheme.weakNormalizationFactorization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/WeaklyNormalScheme.lean, line 75.

The weak normalization of X in its normalization, as a factorization.

public noncomputable abbrev weakNormalizationFactorization (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    UniversalHomeomorphismFactorization (normalization X hX)

Tag 0H3S, a definition

Tag 0H3S in the Stacks Project.

AlgebraicGeometry.Scheme.IsWeaklyNormal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/WeaklyNormalScheme.lean, line 103.

A scheme is weakly normal if its weak normalization morphism is an isomorphism.

public abbrev IsWeaklyNormal (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) : Prop

Tag 0H3T, a lemma

Tag 0H3T in the Stacks Project.

AlgebraicGeometry.isWeaklyNormal_spec_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/AffineWeaklyNormal.lean, line 809.

Stacks Project, Tag 0H3T. An affine scheme with finitely many irreducible components is weakly normal exactly when its coordinate ring is seminormal and satisfies the prime-power divisibility condition for nonzerodivisors.

theorem isWeaklyNormal_spec_iff (A : Type u) [CommRing A]
    (hA : ∀ U : (Spec (.of A)).Opens, IsCompact (U : Set (Spec (.of A))) →
      (irreducibleComponents U).Finite) :
    Scheme.IsWeaklyNormal (Spec (.of A)) hA ↔ IsWeaklyNormalRing A

Tag 0H3U, a lemma

Tag 0H3U in the Stacks Project.

AlgebraicGeometry.isWeaklyNormal_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/WeaklyNormalLocal.lean, line 305. The attribute's comment: “open subschemes”.

Stacks Project, Tag 0H3U. Every open subscheme of a weakly normal scheme is weakly normal.

theorem isWeaklyNormal_open {X : Scheme.{u}}
    (hX : ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite)
    (hWN : Scheme.IsWeaklyNormal X hX) (U : X.Opens) :
    ∃ hU : ∀ V : U.toScheme.Opens,
      IsCompact (V : Set U.toScheme) → (irreducibleComponents V).Finite,
      Scheme.IsWeaklyNormal U.toScheme hU

AlgebraicGeometry.isWeaklyNormal_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeakNormalization/WeaklyNormalLocal.lean, line 322. The attribute's comment: “equivalent conditions”.

Stacks Project, Tag 0H3U. For a scheme whose quasi-compact opens have finitely many irreducible components, weak normality is equivalent to the two ring conditions of Tag 0H3T on every affine open, to those conditions on a single affine open covering, and to the existence of an open covering by weakly normal schemes.

theorem isWeaklyNormal_tfae (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    List.TFAE [
      Scheme.IsWeaklyNormal X hX,
      ∀ U : X.affineOpens, IsWeaklyNormalRing Γ(X, U.1),
      ∃ (I : Type u) (U : I → X.affineOpens),
        (⨆ i, (U i).1) = ⊤ ∧ ∀ i, IsWeaklyNormalRing Γ(X, (U i).1),
      ∃ (I : Type u) (U : I → X.Opens),
        (⨆ i, U i) = ⊤ ∧
          ∀ i, ∃ hUi : ∀ V : (U i).toScheme.Opens,
            IsCompact (V : Set (U i).toScheme) → (irreducibleComponents V).Finite,
            Scheme.IsWeaklyNormal (U i).toScheme hUi]

Sources

• Section 29.56, Tag 0H3I
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.relativeWeakNormalization · AlgebraicGeometry.relativeWeakNormalization_isUniversalHomeomorphism · AlgebraicGeometry.range_le_relativeWeakNormalization · AlgebraicGeometry.relativeWeakNormalization_localization · AlgebraicGeometry.relativeSeminormalization · AlgebraicGeometry.relativeSeminormalization_universalHomeomorphism · AlgebraicGeometry.relativeSeminormalization_residueFieldMap_isIso · AlgebraicGeometry.map_mem_relativeSeminormalization

Section29.57 Zariski's Main Theorem (algebraic version)#

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

Tag 03GT, a theorem

Tag 03GT in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch29.lean, line 129 (StacksFrontier). References: EGA III (4.4.1), “more general”; EGA III (4.4.12), “partial”.

Tag 01TI, a lemma

Tag 01TI in the Stacks Project.

AlgebraicGeometry.mem_quasiFiniteLocus_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Locus.lean, line 66. The attribute's comment: “openness of the quasi-finite locus”.

A point belongs to the locally quasi-finite locus exactly when the morphism is quasi-finite at that point. In particular, the set of such points is open.

public theorem mem_quasiFiniteLocus_iff {X S : Scheme.{u}} (f : X ⟶ S) (x : X) :
    x ∈ quasiFiniteLocus f ↔ quasiFiniteAt f x

AlgebraicGeometry.locallyOfFiniteType_quasiFiniteLocus, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Locus.lean, line 92. The attribute's comment: “the induced morphism, local finite type”.

The restriction to the quasi-finite locus is locally of finite type.

public instance locallyOfFiniteType_quasiFiniteLocus {X S : Scheme.{u}} (f : X ⟶ S) :
    LocallyOfFiniteType ((quasiFiniteLocus f).ι ≫ f)

AlgebraicGeometry.locallyQuasiFinite_quasiFiniteLocus, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/Locus.lean, line 124. The attribute's comment: “the induced morphism, fiber isolation”.

The restriction to the quasi-finite locus is locally quasi-finite in Mathlib's fiber-isolation sense.

public instance locallyQuasiFinite_quasiFiniteLocus {X S : Scheme.{u}} (f : X ⟶ S) :
    LocallyQuasiFinite ((quasiFiniteLocus f).ι ≫ f)

Tag 03GU, a lemma

Tag 03GU in the Stacks Project.

AlgebraicGeometry.exists_isOpenImmersion_isFinite_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/FiniteFactorization.lean, line 176. References: EGA IV (18.12.13), “affine case”; EGA IV (8.12.6), “affine case”; EGA III (4.4.3), “special case”; SGA 3 VIB (5.6.0), “(ii), special case”.

Stacks Project, Tag 03GU. A quasi-finite morphism f : Y ⟶ X of affine schemes factors as j ≫ π with Z affine, j : Y ⟶ Z an open immersion and π : Z ⟶ X finite.

Quasi-compactness of f is not assumed: it is automatic for an affine source.

public theorem exists_isOpenImmersion_isFinite_factorization {X Y : Scheme.{u}} (f : Y ⟶ X)
    [IsAffine X] [IsAffine Y] [LocallyOfFiniteType f] [LocallyQuasiFinite f] :
    ∃ (Z : Scheme.{u}) (_ : IsAffine Z) (j : Y ⟶ Z) (π : Z ⟶ X),
      IsOpenImmersion j ∧ IsFinite π ∧ j ≫ π = f

Tag 03J2, a lemma

Tag 03J2 in the Stacks Project.

AlgebraicGeometry.isNowhereDense_image_of_quasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/NowhereDenseImage.lean, line 111.

Stacks Project, Tag 03J2. The image of a closed nowhere dense subset under a quasi-finite morphism of schemes is nowhere dense.

theorem isNowhereDense_image_of_quasiFinite {Y X : Scheme.{u}} (f : Y ⟶ X)
    [LocallyOfFiniteType f] [LocallyQuasiFinite f] [QuasiCompact f] (T : Set Y)
    (hT_closed : IsClosed T) (hT_nowhereDense : IsNowhereDense T) :
    IsNowhereDense (f.base '' T)

Sources

• Section 29.57, Tag 03GS
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization · AlgebraicGeometry.mem_quasiFiniteLocus_iff · AlgebraicGeometry.locallyOfFiniteType_quasiFiniteLocus · AlgebraicGeometry.locallyQuasiFinite_quasiFiniteLocus · AlgebraicGeometry.exists_isOpenImmersion_isFinite_factorization · AlgebraicGeometry.isNowhereDense_image_of_quasiFinite

Section29.58 Universally bounded fibres#

Section 29.58 of the Stacks Project, Tag 03J3. 10 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03J4, a definition

Tag 03J4 in the Stacks Project.

AlgebraicGeometry.BoundsFiberDegrees, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBounded.lean, line 50. The attribute's comment: “part (1)”.

An integer bounds the degrees of the fibres of f if each fibre is finite locally free of some rank no greater than that integer.

public abbrev BoundsFiberDegrees {X Y : Scheme.{u}} (f : X ⟶ Y) (n : ℤ) : Prop

AlgebraicGeometry.HasUniversallyBoundedFibers, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBounded.lean, line 56. The attribute's comment: “part (2)”.

The fibres of f are universally bounded if their degrees have a common integer bound.

public abbrev HasUniversallyBoundedFibers {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop

Tag 03J5, a lemma

Tag 03J5 in the Stacks Project.

AlgebraicGeometry.cardinalMk_pullback_le_of_degree_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/FibreCardinality.lean, line 77. The attribute's comment: “card_fibre_le_bound”.

Stacks Project, Tag 03J5. If all field-valued base changes of a morphism are finite of degree at most n, then each of them has at most n points.

theorem cardinalMk_pullback_le_of_degree_le
    {X Y : Scheme.{u}} (f : X ⟶ Y) (n : ℕ)
    (h : ∀ (k : Type u) [Field k] (g : Spec (.of k) ⟶ Y),
      ∃ r ≤ n, Stacks.Morphisms.IsFiniteLocallyFreeOfRank (pullback.fst g f) r) :
    ∀ (k : Type u) [Field k] (g : Spec (.of k) ⟶ Y),
      Cardinal.mk (pullback g f : Scheme.{u}) ≤ n

AlgebraicGeometry.sum_finrank_residueField_le_of_degree_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/ResidueDegreeBound.lean, line 121. The attribute's comment: “sum_residue_degrees_le_bound”.

Stacks Project, Tag 03J5. In a field-valued base change whose degree is uniformly bounded by n, the sum of the residue degrees at any finite family of distinct points is at most n.

public theorem sum_finrank_residueField_le_of_degree_le
    {X Y : Scheme.{u}} (f : X ⟶ Y) (n : ℕ)
    (h : ∀ (k : Type u) [Field k] (g : Spec (.of k) ⟶ Y),
      ∃ r ≤ n, Stacks.Morphisms.IsFiniteLocallyFreeOfRank (pullback.fst g f) r) :
    ∀ (k : Type u) [Field k] (g : Spec (.of k) ⟶ Y) {t : ℕ}
      (x : Fin t → (pullback g f : Scheme.{u})), Function.Injective x →
      (∑ i,
        letI := ((Scheme.ΓSpecIso (.of k)).inv ≫ (pullback.fst g f).appTop ≫
          (pullback g f).Γevaluation (x i)).hom.toAlgebra
        Module.finrank k ((pullback g f).residueField (x i))) ≤ n

AlgebraicGeometry.hasUniversallyBoundedFibers_of_boundsFiberDegrees, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBounded.lean, line 62. The attribute's comment: “universally_bounded”.

A common integer bound on the degrees of the fibres makes those fibres universally bounded.

public lemma hasUniversallyBoundedFibers_of_boundsFiberDegrees {X Y : Scheme.{u}} (f : X ⟶ Y)
    (n : ℤ) (h : BoundsFiberDegrees f n) : HasUniversallyBoundedFibers f

AlgebraicGeometry.boundsFiberDegrees_iff_field_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBoundedBaseChange.lean, line 100. The attribute's comment: “bounded_degree_iff_field_base_changes”.

An integer bounds the degrees of the fibres of a morphism of schemes exactly when each of its base changes to the spectrum of a field is finite locally free of a rank bounded by that integer.

theorem boundsFiberDegrees_iff_field_baseChange {X Y : Scheme.{u}} (f : X ⟶ Y) (n : ℤ) :
    BoundsFiberDegrees f n ↔
      ∀ (k : Type u) [Field k] (g : Spec (.of k) ⟶ Y),
        ∃ r : ℕ, (r : ℤ) ≤ n ∧
          Stacks.Morphisms.IsFiniteLocallyFreeOfRank (pullback.fst g f) r

AlgebraicGeometry.boundsFiberDegrees_iff_field_baseChange_of_nonneg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Varieties/BoundedDegree/FieldBaseChange.lean, line 75. The attribute's comment: “bounded_degree_iff_field_base_changes”.

Stacks Project, Tag 03J5. A nonnegative integer bounds the degrees of the fibres of a scheme morphism exactly when every field-valued base change is finite locally free of rank at most that integer.

The nonnegativity hypothesis is the source's and is not used, so it is named _hn; the form without it is AlgebraicGeometry.boundsFiberDegrees_iff_field_baseChange, in StacksFrontier.AlgebraicGeometry.Morphisms.FibreDimension.UniversallyBoundedBaseChange.

theorem boundsFiberDegrees_iff_field_baseChange_of_nonneg
    {X Y : Scheme.{u}} (f : X ⟶ Y) (n : ℤ) (_hn : 0 ≤ n) :
    BoundsFiberDegrees f n ↔
      ∀ (k : Type u) [Field k] (g : Spec (.of k) ⟶ Y),
        ∃ r : ℕ, (r : ℤ) ≤ n ∧
          Stacks.Morphisms.IsFiniteLocallyFreeOfRank (pullback.fst g f) r

Tag 0CC2, a lemma

Tag 0CC2 in the Stacks Project.

AlgebraicGeometry.boundsFiberDegrees_of_isFiniteLocallyFreeOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBoundedBaseChange.lean, line 132.

The degree of a finite locally free morphism bounds the degrees of all of its fibres.

theorem boundsFiberDegrees_of_isFiniteLocallyFreeOfRank {X Y : Scheme.{u}} (f : X ⟶ Y) (d : ℕ)
    [Stacks.Morphisms.IsFiniteLocallyFreeOfRank f d] : BoundsFiberDegrees f (d : ℤ)

Tag 03J6, a lemma

Tag 03J6 in the Stacks Project.

AlgebraicGeometry.boundsFiberDegrees_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBoundedComposition.lean, line 183.

Stacks Project, Tag 03J6. If a nonnegative integer n bounds the degrees of the fibres of f and an integer m bounds the degrees of the fibres of g, then n * m bounds the degrees of the fibres of the composite f ≫ g.

theorem boundsFiberDegrees_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (n m : ℤ)
    (hn : 0 ≤ n) (hf : BoundsFiberDegrees f n) (hg : BoundsFiberDegrees g m) :
    BoundsFiberDegrees (f ≫ g) (n * m)

AlgebraicGeometry.hasUniversallyBoundedFibers_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBoundedComposition.lean, line 221.

Stacks Project, Tag 03J6. A composition of morphisms with universally bounded fibres has universally bounded fibres.

theorem hasUniversallyBoundedFibers_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasUniversallyBoundedFibers f) (hg : HasUniversallyBoundedFibers g) :
    HasUniversallyBoundedFibers (f ≫ g)

Tag 03J7, a lemma

Tag 03J7 in the Stacks Project.

AlgebraicGeometry.boundsFiberDegrees_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBoundedBaseChange.lean, line 60.

Every integer bound on the degrees of the fibres of a morphism of schemes is preserved by arbitrary base change.

instance boundsFiberDegrees_isStableUnderBaseChange (n : ℤ) :
    MorphismProperty.IsStableUnderBaseChange
      (fun {X Y : Scheme.{u}} (f : X ⟶ Y) ↦ BoundsFiberDegrees f n)

Tag 03J8, a lemma

Tag 03J8 in the Stacks Project.

AlgebraicGeometry.boundsFiberDegrees_of_isPullback_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBoundedSurjectiveDescent.lean, line 44. The attribute's comment: “specified bound”.

Let f' be a base change of f along a surjective morphism. An integer bounding the degrees of the fibres of f' also bounds the degrees of the fibres of f.

theorem boundsFiberDegrees_of_isPullback_of_surjective {X Y X' Y' : Scheme.{u}} {f : X ⟶ Y}
    {f' : X' ⟶ Y'} {g' : X' ⟶ X} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g) [Surjective g]
    (n : ℤ) (h : BoundsFiberDegrees f' n) : BoundsFiberDegrees f n

AlgebraicGeometry.hasUniversallyBoundedFibers_of_isPullback_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBoundedSurjectiveDescent.lean, line 65. The attribute's comment: “universally bounded fibres”.

Let f' be a base change of f along a surjective morphism. If f' has universally bounded fibres, then so does f.

theorem hasUniversallyBoundedFibers_of_isPullback_of_surjective {X Y X' Y' : Scheme.{u}}
    {f : X ⟶ Y} {f' : X' ⟶ Y'} {g' : X' ⟶ X} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    [Surjective g] (h : HasUniversallyBoundedFibers f') : HasUniversallyBoundedFibers f

Tag 03J9, a lemma

Tag 03J9 in the Stacks Project.

AlgebraicGeometry.hasUniversallyBoundedFibers_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/ImmersionBounded.lean, line 46.

An immersion of schemes has universally bounded fibres; the integer one bounds the degrees of its fibres.

theorem hasUniversallyBoundedFibers_of_isImmersion {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsImmersion f] : HasUniversallyBoundedFibers f

Tag 03WU, a lemma

Tag 03WU in the Stacks Project.

AlgebraicGeometry.etale_boundsFiberDegrees_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/EtaleUniversallyBounded.lean, line 209.

For an étale morphism, bounding fibre degrees, bounding the points of every field-valued base change, and bounding the points after passage to separable closures of residue fields are equivalent.

theorem etale_boundsFiberDegrees_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) [Etale f] (n : ℕ) :
    List.TFAE [
      BoundsFiberDegrees f (n : ℤ),
      ∀ (k : Type u) [Field k] (g : Spec (.of k) ⟶ Y),
        Cardinal.mk (pullback g f : Scheme.{u}) ≤ n,
      ∀ (y : Y) (ksep : Type u) [Field ksep] [Algebra (Y.residueField y) ksep]
        [IsSepClosure (Y.residueField y) ksep],
        Cardinal.mk
          (pullback
            (Spec.map (CommRingCat.ofHom (algebraMap (Y.residueField y) ksep)))
            (f.fiberToSpecResidueField y) : Scheme.{u}) ≤ n]

Tag 03JA, a lemma

Tag 03JA in the Stacks Project.

AlgebraicGeometry.hasUniversallyBoundedFibers_of_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/QuasiFiniteUniversallyBounded.lean, line 437.

Stacks 03JA. A locally quasi-finite morphism of finite type whose source is quasi-compact has universally bounded fibres.

theorem hasUniversallyBoundedFibers_of_locallyQuasiFinite {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] [LocallyQuasiFinite f] [CompactSpace X] :
    HasUniversallyBoundedFibers f

Tag 03JB, a lemma

Tag 03JB in the Stacks Project.

AlgebraicGeometry.boundsFiberDegrees_of_comp_of_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBoundedFlatDescent.lean, line 130. The attribute's comment: “specified bound”.

Stacks Project, Tag 03JB, the precise form. If f is surjective and flat, then an integer bounding the degrees of the fibres of f ≫ h also bounds the degrees of the fibres of h.

public theorem boundsFiberDegrees_of_comp_of_surjective_flat {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (h : Y ⟶ Z) [Surjective f] [Flat f] (n : ℤ)
    (hbound : BoundsFiberDegrees (f ≫ h) n) :
    BoundsFiberDegrees h n

AlgebraicGeometry.hasUniversallyBoundedFibers_of_comp_of_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/UniversallyBoundedFlatDescent.lean, line 164. The attribute's comment: “universally bounded fibres”.

Stacks Project, Tag 03JB. If f is surjective and flat and the fibres of f ≫ h are universally bounded, then so are the fibres of h.

public theorem hasUniversallyBoundedFibers_of_comp_of_surjective_flat {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (h : Y ⟶ Z) [Surjective f] [Flat f]
    (hbound : HasUniversallyBoundedFibers (f ≫ h)) :
    HasUniversallyBoundedFibers h

Sources

• Section 29.58, Tag 03J3
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.BoundsFiberDegrees · AlgebraicGeometry.HasUniversallyBoundedFibers · AlgebraicGeometry.cardinalMk_pullback_le_of_degree_le · AlgebraicGeometry.sum_finrank_residueField_le_of_degree_le · AlgebraicGeometry.hasUniversallyBoundedFibers_of_boundsFiberDegrees · AlgebraicGeometry.boundsFiberDegrees_iff_field_baseChange · AlgebraicGeometry.boundsFiberDegrees_iff_field_baseChange_of_nonneg · AlgebraicGeometry.boundsFiberDegrees_of_isFiniteLocallyFreeOfRank

Section29.59 Miscellany#

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

Tag 0H1M, a lemma

Tag 0H1M in the Stacks Project.

AlgebraicGeometry.exists_comp_fromSpecResidueField_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Misc/PointFactorization.lean, line 43.

Stacks Project, Tag 0H1M. A morphism from a reduced scheme whose image is contained in a single point factors through the spectrum of the residue field of that point.

lemma exists_comp_fromSpecResidueField_eq {X Y : Scheme.{u}} (f : Y ⟶ X) (x : X)
    [IsReduced Y] (hf : Set.range f.base ⊆ {x}) :
    ∃ g : Y ⟶ Spec (.of (X.residueField x)), g ≫ X.fromSpecResidueField x = f

Tag 0H1N, a lemma

Tag 0H1N in the Stacks Project.

AlgebraicGeometry.exists_factorization_through_residueFields, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Misc/ResidueFieldFactorization.lean, line 226.

Stacks Project, Tag 0H1N. A morphism from a reduced scheme into a locally Noetherian scheme, whose image lies in a set having no nontrivial specializations among its points, factors through the coproduct of the corresponding residue-field points.

theorem exists_factorization_through_residueFields
    {X Y : Scheme.{u}} (f : Y ⟶ X) (E : Set X)
    [IsLocallyNoetherian X] [IsReduced Y]
    (hE : ∀ x x' : E, x.1 ⤳ x'.1 → x.1 = x'.1)
    (hf : ∀ y : Y, f y ∈ E) :
    ∃ g : Y ⟶ ∐ fun x : E ↦ Spec (.of (X.residueField x.1)),
      g ≫ Sigma.desc (fun x : E ↦ X.fromSpecResidueField x.1) = f

Sources

• Section 29.59, Tag 0H1L
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.exists_comp_fromSpecResidueField_eq · AlgebraicGeometry.exists_factorization_through_residueFields

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.