33.3 Varieties to 33.22 Global generation

Section33.3 Varieties #

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

Tag 020D, a definition

Tag 020D in the Stacks Project.

AlgebraicGeometry.IsVariety, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Basic.lean, line 50.

A scheme over a field is a variety when it is integral and its structure morphism is separated and of finite type.

class IsVariety (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) : Prop
    extends IsIntegral X, IsSeparated f, LocallyOfFiniteType f, QuasiCompact f

Tag 020G, an example

Tag 020G in the Stacks Project.

AlgebraicGeometry.gaussianRationals_isVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Product.lean, line 296. The attribute's comment: “each factor is a variety”.

Spec ℚ(i) is a variety over ℚ.

public theorem gaussianRationals_isVariety :
    IsVariety ℚ gaussianRationalsToRat

AlgebraicGeometry.gaussianRationals_product_reducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Product.lean, line 308. The attribute's comment: “the product is reducible”.

The product Spec ℚ(i) ×_{Spec ℚ} Spec ℚ(i) is reducible.

public theorem gaussianRationals_product_reducible :
    ¬ IrreducibleSpace
      (pullback gaussianRationalsToRat gaussianRationalsToRat : Scheme)

AlgebraicGeometry.gaussianRationals_product_not_isVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Product.lean, line 341. The attribute's comment: “the product is not a variety”.

The product of these two varieties is not a variety.

public theorem gaussianRationals_product_not_isVariety :
    ¬ IsVariety ℚ
      (pullback.fst gaussianRationalsToRat gaussianRationalsToRat ≫
        gaussianRationalsToRat)

AlgebraicGeometry.gaussianRationals_product_iso_coprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Product.lean, line 349. The attribute's comment: “the product is two copies of the factor”.

The product is isomorphic to two disjoint copies of Spec ℚ(i).

public theorem gaussianRationals_product_iso_coprod :
    Nonempty ((pullback gaussianRationalsToRat gaussianRationalsToRat) ≅
      (Spec (.of GaussianRationals) ⨿ Spec (.of GaussianRationals)))

Tag 05P3, a lemma

Tag 05P3 in the Stacks Project.

AlgebraicGeometry.isVariety_pullback, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Product.lean, line 82.

Stacks Project, Tag 05P3. The fibre product of two varieties over an algebraically closed field is a variety.

public instance isVariety_pullback (k : Type u) [Field k] [IsAlgClosed k]
    {X Y : Scheme.{u}} (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k))
    [IsVariety k f] [IsVariety k g] :
    IsVariety k (pullback.fst f g ≫ f)

Sources

LeanAlgebraicGeometry.IsVariety · AlgebraicGeometry.gaussianRationals_isVariety · AlgebraicGeometry.gaussianRationals_product_reducible · AlgebraicGeometry.gaussianRationals_product_not_isVariety · AlgebraicGeometry.gaussianRationals_product_iso_coprod · AlgebraicGeometry.isVariety_pullback

Section33.4 Varieties and rational maps #

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

Tag 0BXN, a theorem

Tag 0BXN in the Stacks Project.

AlgebraicGeometry.varietyEquivalenceFinitelyGeneratedFieldExtensionOpposite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Varieties/FunctionFieldEquivalence/Equivalence.lean, line 85.

Stacks Project, Tag 0BXN. Varieties and dominant rational maps over a field are contravariantly equivalent to finitely generated field extensions of that field.

noncomputable def varietyEquivalenceFinitelyGeneratedFieldExtensionOpposite
    (k : Type u) [Field k] :
    Variety k ≌ (FinitelyGeneratedFieldExtension k)ᵒᵖ

Tag 0BXP, a lemma

Tag 0BXP in the Stacks Project.

AlgebraicGeometry.birationalOver_tfae_functionField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/RationalMap/FunctionField.lean, line 254.

Stacks Project, Tag 0BXP. The four characterizations of birationality for varieties over a field: birationality over k, isomorphy of the function fields as extensions of k, isomorphy of nonempty open subvarieties, and the existence of a birational morphism from an open subvariety.

public theorem birationalOver_tfae_functionField
    (k : Type u) [Field k] {X Y : Scheme.{u}}
    (sX : X ⟶ Spec (.of k)) (sY : Y ⟶ Spec (.of k))
    [IsVariety k sX] [IsVariety k sY] :
    letI : Algebra k (Stacks.Chow.rationalFunctions X) :=
      ((Stacks.Chow.ofSectionRingHom X ⟨⊤, dense_univ⟩).comp
        ((Scheme.ΓSpecIso (.of k)).inv ≫ sX.appTop).hom).toAlgebra
    letI : Algebra k (Stacks.Chow.rationalFunctions Y) :=
      ((Stacks.Chow.ofSectionRingHom Y ⟨⊤, dense_univ⟩).comp
        ((Scheme.ΓSpecIso (.of k)).inv ≫ sY.appTop).hom).toAlgebra
    List.TFAE [
      Scheme.BirationalOver sX sY,
      Nonempty (Stacks.Chow.rationalFunctions X ≃ₐ[k]
        Stacks.Chow.rationalFunctions Y),
      ∃ (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,
      ∃ (U : X.Opens), (U : Set X).Nonempty ∧
        ∃ f : U.toScheme ⟶ Y,
          IsBirational f ∧ f ≫ sY = U.ι ≫ sX]

Sources

LeanAlgebraicGeometry.varietyEquivalenceFinitelyGeneratedFieldExtensionOpposite · AlgebraicGeometry.birationalOver_tfae_functionField

Section33.5 Change of fields and local rings #

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

Tag 0C4Y, a lemma

Tag 0C4Y in the Stacks Project.

AlgebraicGeometry.stalkOfBaseChange_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/CohenMacaulay/FieldExtensionStalk.lean, line 364. The attribute's comment: “localization_description”.

Stacks Project, Tag 0C4Y (localization description). The local ring at a point of a base change by a field extension is the localization of 𝒪_{X,x} ⊗_k K at the prime obtained from the map to the residue field of that point.

public theorem stalkOfBaseChange_isLocalization
    {k K : Type u} [Field k] [Field K] [Algebra k K]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) (x : X)
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}))
    (hy : (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y = x) :
    let Y := (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u})
    let A := stalkBaseChangeRing (K := K) f x
    let B := residueBaseChangeRing (K := K) f x
    ∃ θ : A ⟶ B, ∃ ψ : B ⟶ Y.residueField y, ∃ φ : A ⟶ Y.presheaf.stalk y,
      pushout.inl (fieldToStalk f x)
          (CommRingCat.ofHom (algebraMap k K : k →+* K)) ≫ θ =
        X.residue x ≫ pushout.inl (fieldToResidue f x)
          (CommRingCat.ofHom (algebraMap k K : k →+* K)) ∧
      pushout.inr (fieldToStalk f x)
          (CommRingCat.ofHom (algebraMap k K : k →+* K)) ≫ θ =
        pushout.inr (fieldToResidue f x)
          (CommRingCat.ofHom (algebraMap k K : k →+* K)) ∧
      pushout.inl (fieldToResidue f x)
          (CommRingCat.ofHom (algebraMap k K : k →+* K)) ≫ ψ =
        (X.residueFieldCongr hy.symm).hom ≫
          (pullback.fst f (Spec.map
            (CommRingCat.ofHom (algebraMap k K)))).residueFieldMap y ∧
      pushout.inr (fieldToResidue f x)
          (CommRingCat.ofHom (algebraMap k K : k →+* K)) ≫ ψ =
        fieldToResidue
          (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k K)))) y ∧
      pushout.inl (fieldToStalk f x)
          (CommRingCat.ofHom (algebraMap k K : k →+* K)) ≫ φ =
        (X.presheaf.stalkCongr (.of_eq hy.symm)).hom ≫
          (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).stalkMap y ∧
      pushout.inr (fieldToStalk f x)
          (CommRingCat.ofHom (algebraMap k K : k →+* K)) ≫ φ =
        fieldToStalk
          (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k K)))) y ∧
      θ ≫ ψ = φ ≫ Y.residue y ∧
      letI : Algebra A (Y.presheaf.stalk y) := φ.hom.toAlgebra
      let p₀ := RingHom.ker ψ.hom
      let p := stalkBaseChangePrime f x θ p₀
      letI : p₀.IsPrime := RingHom.ker_isPrime _
      letI : p.IsPrime := Ideal.comap_isPrime _ _
      IsLocalization.AtPrime (Y.presheaf.stalk y) p

AlgebraicGeometry.faithfullyFlat_stalkMap_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/FaithfullyFlatStalk.lean, line 57. The attribute's comment: “faithfully_flat_local”.

For an extension of fields K / k, the map on local rings from a point of a k-scheme to a point above it after base change to K is faithfully flat.

public theorem faithfullyFlat_stalkMap_fieldExtension
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) (x : X)
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}))
    (hy : (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y = x) :
    ((eqToHom (congrArg X.presheaf.stalk hy.symm)) ≫
      (pullback.fst f
        (Spec.map (CommRingCat.ofHom (algebraMap k K)))).stalkMap y).hom.FaithfullyFlat

AlgebraicGeometry.Scheme.Pullback.isIso_residueFieldMap_to_residueField_specOfPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ResidueField.lean, line 45. The attribute's comment: “residue_field”.

Stacks Project, Tag 0C4Y (residue field). If y is a point of the base change of a scheme over k to a field extension K/k, its residue field is canonically isomorphic to the residue field at the corresponding prime of κ(x) ⊗[k] K.

public theorem isIso_residueFieldMap_to_residueField_specOfPoint
    {X Y S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S}
    (y : (pullback f g : Scheme)) :
    let T := Scheme.Pullback.Triplet.ofPoint y
    let p := Scheme.Pullback.SpecOfPoint y
    IsIso (((pullback f g : Scheme).residueFieldCongr
        (Scheme.Pullback.SpecTensorTo_SpecOfPoint y).symm).hom ≫
      T.SpecTensorTo.residueFieldMap p ≫
      (Scheme.Spec.residueFieldIso T.tensor p).hom)

AlgebraicGeometry.specialFibreRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/RationalMap/MaximalIdealFieldChange.lean, line 527. The attribute's comment: “special_fibre”.

Stacks Project, Tag 0C4Y (special fibre). For a point y of the base change of a scheme over k to an extension field K, the quotient of 𝒪_{Y,y} by the extension of the maximal ideal of 𝒪_{X,x} is the localization of κ(x) ⊗_k K at the prime induced by y.

noncomputable def specialFibreRingEquiv
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u})) :
    let p := RingHom.ker (Scheme.Pullback.ofPointTensor y).hom
    letI : p.IsPrime := RingHom.ker_isPrime _
    ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}).presheaf.stalk y ⧸
        Ideal.map
          ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).stalkMap y).hom
          (IsLocalRing.maximalIdeal
            (X.presheaf.stalk
              ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y)))) ≃+*
      Localization.AtPrime p

Tag 0C4Z, a lemma

Tag 0C4Z in the Stacks Project.

AlgebraicGeometry.fiberLocalRing_dimension_add_localRing_dimension_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/RationalMap/LocalRingDimension.lean, line 103. The attribute's comment: “local-ring dimension equality”.

Stacks Project, Tag 0C4Z. After extension of the ground field, the dimension of the local fibre ring plus the dimension of the original local ring is the dimension of the new local ring.

theorem fiberLocalRing_dimension_add_localRing_dimension_eq
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u})) :
    let Y := (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u})
    let g : Y ⟶ X := pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))
    let x := g.base y
    ringKrullDim
          ((Y.presheaf.stalk y) ⧸
            Ideal.map (g.stalkMap y).hom
              (IsLocalRing.maximalIdeal (X.presheaf.stalk x))) +
        ringKrullDim (X.presheaf.stalk x) =
      ringKrullDim (Y.presheaf.stalk y)

AlgebraicGeometry.fiberLocalRing_dimension_add_trdeg_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/RationalMap/LocalRingDimension.lean, line 142. The attribute's comment: “transcendence degree equality”.

Stacks Project, Tag 0C4Z. After extension of the ground field, the dimension of the local fibre ring plus the transcendence degree of the new residue field is the transcendence degree of the original residue field.

theorem fiberLocalRing_dimension_add_trdeg_eq
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u})) :
    let Y := (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u})
    let g : Y ⟶ X := pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))
    let h : Y ⟶ Spec (.of K) := pullback.snd f (Spec.map
      (CommRingCat.ofHom (algebraMap k K)))
    let x := g.base y
    letI : Algebra k (X.residueField x) := (fieldToResidue f x).hom.toAlgebra
    letI : Algebra K (Y.residueField y) := (fieldToResidue h y).hom.toAlgebra
    ringKrullDim
          ((Y.presheaf.stalk y) ⧸
            Ideal.map (g.stalkMap y).hom
              (IsLocalRing.maximalIdeal (X.presheaf.stalk x))) +
        (Cardinal.toENat (Algebra.trdeg K (Y.residueField y)) : WithBot ℕ∞) =
      (Cardinal.toENat (Algebra.trdeg k (X.residueField x)) : WithBot ℕ∞)

Tag 0C50, a lemma

Tag 0C50 in the Stacks Project.

AlgebraicGeometry.map_maximalIdeal_stalkMap_eq_of_isReduced_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/RationalMap/MaximalIdealFieldChange.lean, line 858.

Stacks Project, Tag 0C50. Let X be locally of finite type over a field k and let Y = X ×_{Spec k} Spec K for an extension of fields K / k. If a point y of Y and its image x in X have local rings of the same dimension, and the scalar extension κ(x) ⊗[k] K of the residue field at x is reduced — for instance if κ(x) / k or K / k is separable — then the maximal ideal of 𝒪_{X, x} generates the maximal ideal of 𝒪_{Y, y}.

theorem map_maximalIdeal_stalkMap_eq_of_isReduced_tensorProduct
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}))
    (hdim :
      ringKrullDim
          (X.presheaf.stalk
            ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y)) =
        ringKrullDim
          ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).presheaf.stalk y))
    (hreduced :
      let x := (pullback.fst f
        (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y
      letI : (f x).asIdeal.IsPrime := (f x).isPrime
      letI := ((CommRingCat.ofHom (algebraMap k (f x).asIdeal.ResidueField)) ≫
        (Scheme.Spec.residueFieldIso (.of k) (f x)).inv ≫
        f.residueFieldMap x).hom.toAlgebra
      _root_.IsReduced (TensorProduct k (X.residueField x) K)) :
    Ideal.map
        ((pullback.fst f
          (Spec.map (CommRingCat.ofHom (algebraMap k K)))).stalkMap y).hom
        (IsLocalRing.maximalIdeal
          (X.presheaf.stalk
            ((pullback.fst f
              (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y))) =
      IsLocalRing.maximalIdeal
        ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).presheaf.stalk y)

Sources

LeanAlgebraicGeometry.stalkOfBaseChange_isLocalization · AlgebraicGeometry.faithfullyFlat_stalkMap_fieldExtension · AlgebraicGeometry.Scheme.Pullback.isIso_residueFieldMap_to_residueField_specOfPoint · AlgebraicGeometry.specialFibreRingEquiv · AlgebraicGeometry.fiberLocalRing_dimension_add_localRing_dimension_eq · AlgebraicGeometry.fiberLocalRing_dimension_add_trdeg_eq · AlgebraicGeometry.map_maximalIdeal_stalkMap_eq_of_isReduced_tensorProduct

Section33.6 Geometrically reduced schemes #

Section 33.6 of the Stacks Project, Tag 035U. 11 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 035V, a definition

Tag 035V in the Stacks Project.

AlgebraicGeometry.IsGeometricallyReducedOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Reduced.lean, line 107.

[Stacks, Tag 035V]. Let k be a field and let X be a scheme over k, given by its structure morphism f : X ⟶ Spec k.

X is geometrically reduced at a point x ∈ X if for any field extension k'/k and any point x' of X_{k'} lying over x the local ring 𝒪_{X_{k'}, x'} is reduced. That pointwise condition is AlgebraicGeometry.IsGeometricallyReducedAt f x, the body of this definition under its quantifier: the base change X_{k'} is the pullback of f along Spec k' ⟶ Spec k, and x' lies over x when the first projection sends it to x.

X is geometrically reduced over k if it is geometrically reduced at every point of X, which is exactly what this definition says.

Mathlib's AlgebraicGeometry.GeometricallyReduced is the notion of part (2) for an arbitrary base, defined by reducedness of every field-valued base change rather than pointwise; over a field the two agree by AlgebraicGeometry.geometricallyReduced_iff_forall_isGeometricallyReducedAt, so the results stated for it — such as AlgebraicGeometry.geometricallyReduced_of_isReduced over a perfect field — apply to this predicate as well.

public abbrev IsGeometricallyReducedOver {k : Type u} [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) : Prop

Tag 035W, a lemma

Tag 035W in the Stacks Project.

AlgebraicGeometry.isGeometricallyReducedAt_iff_isGeometricallyReduced_stalk, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Reduced.lean, line 256.

A scheme over a field is geometrically reduced at a point if and only if its local ring at that point is geometrically reduced over the field.

public lemma isGeometricallyReducedAt_iff_isGeometricallyReduced_stalk
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) (x : X) :
    IsGeometricallyReducedAt f x ↔
      let : Algebra k (X.presheaf.stalk x) :=
        let : Algebra k ((Spec (.of k)).presheaf.stalk (f.base x)) :=
          StructureSheaf.stalkAlgebra k (f.base x)
        ((f.stalkMap x).hom.comp
          (algebraMap k ((Spec (.of k)).presheaf.stalk (f.base x)))).toAlgebra
      Algebra.IsGeometricallyReduced k (X.presheaf.stalk x)

Tag 020I, a lemma

Tag 020I in the Stacks Project.

AlgebraicGeometry.isGeometricallyReducedAt_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Reduced.lean, line 292. The attribute's comment: “part (1)”. References: EGA IV (4.6.11), “partial”; EGA IV (4.6.12), “special case”.

A reduced local ring of a scheme over a perfect field is geometrically reduced at the corresponding point.

public theorem isGeometricallyReducedAt_of_isReduced
    {k : Type u} [Field k] [PerfectField k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (x : X) [_root_.IsReduced (X.presheaf.stalk x)] :
    IsGeometricallyReducedAt f x

AlgebraicGeometry.geometricallyReduced_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Reduced.lean, line 312. The attribute's comment: “part (2)”. References: EGA IV (4.6.1), “(c) ⇒ (b), special case”; EGA IV (4.6.12), “(b) ⇒ (a), special case”.

A reduced scheme over a perfect field is geometrically reduced over that field.

public theorem geometricallyReduced_of_isReduced
    {k : Type u} [Field k] [PerfectField k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsReduced X] :
    GeometricallyReduced f

Tag 035X, a lemma

Tag 035X in the Stacks Project.

AlgebraicGeometry.geometricallyReduced_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/ReducedTFAE.lean, line 124.

Stacks Project, Tag 035X. The seven standard characterizations of geometric reducedness for a scheme over a field are equivalent.

public theorem geometricallyReduced_tfae
    (k : Type u) [Field k] (p : ℕ) [ExpChar k p] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k))
    (kperf : Type u) [Field kperf] [Algebra k kperf] [ExpChar kperf p]
    [PerfectRing kperf p] [IsPerfectClosure (algebraMap k kperf) p]
    (K : Type u) [Field K] [Algebra k K] [IsAlgClosure k K] :
    let isReducedAfterBaseChange := fun (k' : Type u) [Field k'] [Algebra k k'] ↦
      IsReduced (pullback f (Spec.map (ofHom (algebraMap k k'))))
    let geometricallyReducedSections := fun U : X.Opens ↦
      letI : Algebra k Γ(X, U) :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appLE ⊤ U (by simp)).hom.toAlgebra
      Algebra.IsGeometricallyReduced k Γ(X, U)
    List.TFAE
      [ GeometricallyReduced f,
        ∀ (k' : Type u) [Field k'] [Algebra k k'], isReducedAfterBaseChange k',
        ∀ (k' : Type u) [Field k'] [Algebra k k'] [FiniteDimensional k k']
          [IsPurelyInseparable k k'], isReducedAfterBaseChange k',
        isReducedAfterBaseChange (AdjoinPthRoots k),
        isReducedAfterBaseChange kperf,
        isReducedAfterBaseChange K,
        ∀ U : X.affineOpens, geometricallyReducedSections U.1 ]

Tag 035Y, a lemma

Tag 035Y in the Stacks Project.

AlgebraicGeometry.isGeometricallyReducedAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedPurelyInseparable.lean, line 51. References: EGA IV (6.7.7), “reduced: b), e), f)”; EGA IV (4.6.1), “special case”; EGA IV (4.6.12), “special case”.

Stacks Project, Tag 035Y. For a scheme over a field of positive characteristic, geometric reducedness at a point is equivalent to reducedness of the local rings above that point after every finite purely inseparable extension, after adjoining all p-th roots, or after passing to a perfect closure.

public theorem isGeometricallyReducedAt_tfae
    {k : Type u} [Field k] (p : ℕ) [CharP k p] (hp : p ≠ 0)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) (x : X) :
    [IsGeometricallyReducedAt f x,
      ∀ (k' : Type u) [Field k'] [Algebra k k'] [FiniteDimensional k k']
          [IsPurelyInseparable k k'],
        let g : Spec (.of k') ⟶ Spec (.of k) :=
          Spec.map (CommRingCat.ofHom (algebraMap k k'))
        ∀ x' : (pullback f g : Scheme), pullback.fst f g x' = x →
          _root_.IsReduced ((pullback f g).presheaf.stalk x'),
      let g : Spec (.of (AdjoinPthRoots k)) ⟶ Spec (.of k) :=
        Spec.map (CommRingCat.ofHom (algebraMap k (AdjoinPthRoots k)))
      ∀ x' : (pullback f g : Scheme), pullback.fst f g x' = x →
        _root_.IsReduced ((pullback f g).presheaf.stalk x'),
      let g : Spec (.of (perfectClosure k (AlgebraicClosure k))) ⟶ Spec (.of k) :=
        Spec.map (CommRingCat.ofHom
          (algebraMap k (perfectClosure k (AlgebraicClosure k))))
      ∀ x' : (pullback f g : Scheme), pullback.fst f g x' = x →
        _root_.IsReduced ((pullback f g).presheaf.stalk x')].TFAE

Tag 0384, a lemma

Tag 0384 in the Stacks Project.

AlgebraicGeometry.isGeometricallyReducedAt_iff_baseChange_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedBaseChange.lean, line 215. The attribute's comment: “pointwise equivalence”. References: EGA IV (4.6.10).

Stacks Project, Tag 0384, pointwise statement. Geometric reducedness at a point is preserved and reflected after extending the base field and choosing a point above it.

public theorem isGeometricallyReducedAt_iff_baseChange_fieldExtension
    (k k' : Type u) [Field k] [Field k'] [Algebra k k'] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (x : X)
    (x' : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k k'))) : Scheme))
    (hx' : pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k k'))) x' = x) :
    IsGeometricallyReducedAt f x ↔
      IsGeometricallyReducedAt
        (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k k')))) x'

AlgebraicGeometry.geometricallyReduced_iff_baseChange_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedBaseChange.lean, line 234. The attribute's comment: “global equivalence”.

Stacks Project, Tag 0384, global statement. A scheme over a field is geometrically reduced if and only if its base change along a field extension is geometrically reduced.

public theorem geometricallyReduced_iff_baseChange_fieldExtension
    (k k' : Type u) [Field k] [Field k'] [Algebra k k'] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) :
    GeometricallyReduced f ↔
      GeometricallyReduced
        (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k k'))))

Tag 035Z, a lemma

Tag 035Z in the Stacks Project.

AlgebraicGeometry.isReduced_stalk_pullback_of_isGeometricallyReducedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedProduct.lean, line 52. The attribute's comment: “reduced_at_points_over_x”. References: EGA IV (4.6.1), “more general”; EGA IV (4.6.12), “partial”.

A product with a reduced scheme is reduced at every point above a geometrically reduced point of the other factor.

public theorem isReduced_stalk_pullback_of_isGeometricallyReducedAt
    {k : Type u} [Field k] {X Y : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k)) (x : X)
    (hX : IsGeometricallyReducedAt f x) [IsReduced Y]
    (z : (pullback f g : Scheme)) (hz : pullback.fst f g z = x) :
    _root_.IsReduced ((pullback f g).presheaf.stalk z)

AlgebraicGeometry.isReduced_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedProduct.lean, line 120. The attribute's comment: “reduced_product”. References: EGA IV (4.6.1), “(b) ⇒ (a)”.

The fibre product of a geometrically reduced scheme and a reduced scheme over a field is reduced.

public theorem isReduced_pullback
    {k : Type u} [Field k] {X Y : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k))
    [GeometricallyReduced f] [IsReduced Y] :
    IsReduced (pullback f g)

AlgebraicGeometry.geometricallyReduced_pullback_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedProduct.lean, line 142. The attribute's comment: “geometrically_reduced_product”. References: EGA IV (4.6.5).

The fibre product over a field of two geometrically reduced schemes is geometrically reduced.

public theorem geometricallyReduced_pullback_over_field
    {k : Type u} [Field k] {X Y : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k))
    [GeometricallyReduced f] [GeometricallyReduced g] :
    GeometricallyReduced (pullback.fst f g ≫ f)

AlgebraicGeometry.isReduced_pullback_over_perfectField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedProduct.lean, line 163. The attribute's comment: “perfect_field_reduced_product”. References: EGA IV (4.6.1), “special case”; SGA 3 VIA (0.2), “partial”.

The fibre product of two reduced schemes over a perfect field is reduced.

public theorem isReduced_pullback_over_perfectField
    {k : Type u} [Field k] [PerfectField k]
    {X Y : Scheme.{u}} (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k))
    [IsReduced X] [IsReduced Y] :
    IsReduced (pullback f g)

Tag 04KS, a lemma

Tag 04KS in the Stacks Project.

AlgebraicGeometry.isGeometricallyReducedAt_of_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedGenericPoints.lean, line 87. The attribute's comment: “geometric_reducedness_at_generalization”.

Stacks Project, Tag 04KS. Geometric reducedness at a point of a scheme over a field is preserved on passing to a generalization of that point.

public theorem isGeometricallyReducedAt_of_specializes
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) {x' x : X}
    (hsp : x' ⤳ x) (hx : IsGeometricallyReducedAt f x) :
    IsGeometricallyReducedAt f x'

AlgebraicGeometry.isGeometricallyReducedAt_of_isReduced_stalk_of_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedGenericPoints.lean, line 272. The attribute's comment: “geometric_reducedness_at_point_of_generic_points”.

Stacks Project, Tag 04KS. A scheme over a field is geometrically reduced at a point whose local ring is reduced if it is geometrically reduced at every generic point of an irreducible component specializing to that point.

public theorem isGeometricallyReducedAt_of_isReduced_stalk_of_genericPoints
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) (x : X)
    (hx : _root_.IsReduced (X.presheaf.stalk x))
    (hgeneric : ∀ x' : X, x' ∈ genericPoints X → x' ⤳ x →
      IsGeometricallyReducedAt f x') :
    IsGeometricallyReducedAt f x

AlgebraicGeometry.geometricallyReduced_of_isGeometricallyReducedAt_genericPoints, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedGenericPoints.lean, line 317. The attribute's comment: “geometric_reducedness_of_generic_points”.

A reduced scheme over a field which is geometrically reduced at the generic points of all its irreducible components is geometrically reduced.

public lemma geometricallyReduced_of_isGeometricallyReducedAt_genericPoints
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsReduced X]
    (h : ∀ x : X, x ∈ genericPoints X → IsGeometricallyReducedAt f x) :
    GeometricallyReduced f

AlgebraicGeometry.geometricallyReduced_iff_isSeparableExtension_functionField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedGenericPoints.lean, line 339. The attribute's comment: “geometric_reducedness_iff_separable_function_field”. References: EGA IV (4.2.4), “(ii), special case”; EGA IV (4.6.1), “(b) ⇔ (e), special case”; EGA IV (4.6.3); EGA IV (6.7.5), “partial”; SGA 1 X (1.1), “special case”.

Stacks Project, Tag 04KS. An integral scheme over a field is geometrically reduced if and only if its function field is a separable extension of the base field.

public theorem geometricallyReduced_iff_isSeparableExtension_functionField
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsIntegral X] :
    letI : Nonempty (⊤ : X.Opens) := ⟨⟨genericPoint X, trivial⟩⟩
    letI : Algebra k X.functionField :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫
        X.germToFunctionField ⊤).hom.toAlgebra
    GeometricallyReduced f ↔ Algebra.IsSeparableExtension k X.functionField

Tag 0360, a lemma

Tag 0360 in the Stacks Project.

AlgebraicGeometry.exists_open_geometricallyReduced_of_isGeometricallyReducedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedNoetherian.lean, line 66. References: EGA IV (4.6.13), “(a) ⇒ (f)”.

Stacks Project, Tag 0360. A locally Noetherian scheme that is geometrically reduced at a point has a geometrically reduced open neighbourhood of that point.

public theorem exists_open_geometricallyReduced_of_isGeometricallyReducedAt
    {k : Type u} [Field k] {X : Scheme.{u}} [IsLocallyNoetherian X]
    (f : X ⟶ Spec (.of k)) (x : X) (hx : IsGeometricallyReducedAt f x) :
    ∃ U : X.Opens, x ∈ U ∧ GeometricallyReduced (U.ι ≫ f)

Tag 020F, an example

Tag 020F in the Stacks Project.

AlgebraicGeometry.InseparableHypersurface.nilpotentElement_pow_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedCounterexample.lean, line 121. The attribute's comment: “the displayed element has p-th power zero”.

Stacks Project, Tag 020F. The displayed element is nilpotent.

public theorem nilpotentElement_pow_eq_zero (K : Type*) [Field K]
    [Algebra (rationalFunctionField p) K] (a b : K)
    (ha : a ^ p = algebraMap (rationalFunctionField p) K (transcendentalGenerator p 0))
    (hb : b ^ p = algebraMap (rationalFunctionField p) K (transcendentalGenerator p 1)) :
    nilpotentElement p K a b ^ p = 0

AlgebraicGeometry.InseparableHypersurface.hypersurface_isVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedCounterexample.lean, line 312. The attribute's comment: “the original scheme is a variety”.

Stacks Project, Tag 020F. The hypersurface over 𝔽ₚ(s,t) is a variety.

public theorem hypersurface_isVariety :
    IsVariety (rationalFunctionField p) (hypersurfaceToSpec p)

AlgebraicGeometry.InseparableHypersurface.nilpotentElement_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedCounterexample.lean, line 423. The attribute's comment: “the displayed element is nonzero”.

Stacks Project, Tag 020F. The displayed element is nonzero.

public theorem nilpotentElement_ne_zero (K : Type*) [Field K]
    [Algebra (rationalFunctionField p) K] (a b : K) :
    nilpotentElement p K a b ≠ 0

AlgebraicGeometry.InseparableHypersurface.baseChange_not_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ReducedCounterexample.lean, line 464. The attribute's comment: “the base change is not reduced”.

Stacks Project, Tag 020F. The base change to a field containing both roots is not reduced.

public theorem baseChange_not_isReduced (K : Type) [Field K]
    [Algebra (rationalFunctionField p) K] (a b : K)
    (ha : a ^ p = algebraMap (rationalFunctionField p) K (transcendentalGenerator p 0))
    (hb : b ^ p = algebraMap (rationalFunctionField p) K (transcendentalGenerator p 1)) :
    ¬ IsReduced (pullback (hypersurfaceToSpec p)
      (Spec.map (CommRingCat.ofHom (algebraMap (rationalFunctionField p) K))))

Tag 04KT, a lemma

Tag 04KT in the Stacks Project.

AlgebraicGeometry.exists_finite_purelyInseparable_extension_geometricallyReduced_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/ReducedReduction.lean, line 647. References: EGA IV (17.15.14.2), “geom. reduced reduction”; EGA IV (4.6.6), “more general”; EGA IV (4.6.8), “First clause”.

Stacks Project, Tag 04KT. After a finite purely inseparable extension of the ground field, the reduction of the base change of a scheme with finitely many irreducible components is geometrically reduced.

public theorem exists_finite_purelyInseparable_extension_geometricallyReduced_reduction
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (hX : (irreducibleComponents X).Finite) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k')
      (_ : Module.Finite k k') (_ : IsPurelyInseparable k k'),
      let g : Spec (.of k') ⟶ Spec (.of k) :=
        Spec.map (CommRingCat.ofHom (algebraMap k k'))
      let p : pullback f g ⟶ Spec (.of k') := pullback.snd f g
      let I := Scheme.IdealSheafData.vanishingIdeal
        (X := (pullback f g : Scheme.{u})) (⊤ : Closeds (pullback f g : Scheme.{u}))
      GeometricallyReduced (I.subschemeι ≫ p)

Sources

LeanAlgebraicGeometry.IsGeometricallyReducedOver · AlgebraicGeometry.isGeometricallyReducedAt_iff_isGeometricallyReduced_stalk · AlgebraicGeometry.isGeometricallyReducedAt_of_isReduced · AlgebraicGeometry.geometricallyReduced_of_isReduced · AlgebraicGeometry.geometricallyReduced_tfae · AlgebraicGeometry.isGeometricallyReducedAt_tfae · AlgebraicGeometry.isGeometricallyReducedAt_iff_baseChange_fieldExtension · AlgebraicGeometry.geometricallyReduced_iff_baseChange_fieldExtension

Section33.7 Geometrically connected schemes #

Section 33.7 of the Stacks Project, Tag 0361. 19 tags here are carried by 24 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0362, a definition

Tag 0362 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.GeometricallyConnected registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch33.lean, line 49 (StacksFrontier): “geometrically connected, for a morphism; the tag is the case of X ⟶ Spec k”. References: EGA III (4.3.4); EGA IV (4.5.2), “partial”; SGA 1 IX (3.4).

Tag 054N, a lemma

Tag 054N in the Stacks Project.

AlgebraicGeometry.geometricallyConnected_iff_baseChange_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedBaseChange.lean, line 40.

Stacks Project, Tag 054N. A scheme over a field is geometrically connected if and only if its base change along a field extension is geometrically connected.

public theorem geometricallyConnected_iff_baseChange_fieldExtension
    {X : Scheme.{u}} (k k' : Type u) [Field k] [Field k'] [Algebra k k']
    (f : X ⟶ Spec (.of k)) :
    GeometricallyConnected f ↔
      GeometricallyConnected
        (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k k'))))

Tag 0385, a lemma

Tag 0385 in the Stacks Project.

AlgebraicGeometry.pullback_snd_connectedComponentsMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedProductProjection.lean, line 64.

Stacks 0385. Let k be a field and let X, Y be schemes over k, presented by their structure maps f : X ⟶ Spec k and g : Y ⟶ Spec k. If X is geometrically connected over k, then the projection X ×_k Y ⟶ Y induces a bijection between the connected components of X ×_k Y and the connected components of Y.

public theorem pullback_snd_connectedComponentsMap_bijective
    (k : Type u) [Field k] {X Y : Scheme.{u}} (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k))
    [GeometricallyConnected f] :
    Function.Bijective (pullback.snd f g).continuous.connectedComponentsMap

Tag 0386, a lemma

Tag 0386 in the Stacks Project.

AlgebraicGeometry.geometricallyConnected_spec_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedAffine.lean, line 34.

An affine scheme is geometrically connected over a field if and only if its coordinate algebra is geometrically connected over that field.

public theorem geometricallyConnected_spec_iff (k A : Type u) [Field k] [CommRing A]
    [Algebra k A] :
    GeometricallyConnected (Spec.map (ofHom (algebraMap k A))) ↔
      Algebra.IsGeometricallyConnected k A

Tag 0363, a lemma

Tag 0363 in the Stacks Project.

AlgebraicGeometry.baseChange_connectedComponents_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedSeparablyClosed.lean, line 60. The attribute's comment: “bijection on connected components”. References: EGA III (4.3.4), “special case”; EGA IV (4.4.1), “special case”; EGA IV (4.5.15), “special case”; EGA IV (4.5.21), “more general”; EGA IV (4.5.6), “(i), special case”; SGA 3 VIA (4.1), “special case”.

Stacks Project, Tag 0363. Base change along any extension of a separably closed field induces a bijection on the connected components of a scheme.

public theorem baseChange_connectedComponents_bijective
    (k k' : Type u) [Field k] [IsSepClosed k] [Field k'] [Algebra k k']
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) :
    Function.Bijective
      (pullback.fst f
        (Spec.map (CommRingCat.ofHom (algebraMap k k')))).continuous.connectedComponentsMap

AlgebraicGeometry.geometricallyConnected_iff_connectedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedSeparablyClosed.lean, line 77. The attribute's comment: “geometric connectedness”. References: EGA IV (4.4.4), “more general”; EGA IV (8.4.5), “special case”.

Stacks Project, Tag 0363. Over a separably closed field, a scheme is geometrically connected if and only if its underlying topological space is connected.

public theorem geometricallyConnected_iff_connectedSpace
    (k : Type u) [Field k] [IsSepClosed k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) :
    GeometricallyConnected f ↔ ConnectedSpace X

Tag 0387, a lemma

Tag 0387 in the Stacks Project.

AlgebraicGeometry.geometricallyConnected_iff_connectedSpace_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedSeparableClosure.lean, line 58.

A scheme over a field is geometrically connected if and only if its base change to a separable algebraic closure is connected.

public theorem geometricallyConnected_iff_connectedSpace_baseChange
    (k : Type u) [Field k] (ksep : Type u) [Field ksep] [Algebra k ksep]
    [IsSepClosure k ksep] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) :
    GeometricallyConnected f ↔
      ConnectedSpace
        (CategoryTheory.Limits.pullback f
          (Spec.map (CommRingCat.ofHom (algebraMap k ksep))) : Scheme.{u})

Tag 0388, a lemma

Tag 0388 in the Stacks Project.

AlgebraicGeometry.exists_fg_subalgebra_descending_isCompact_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/QuasiCompactOpenSubalgebra.lean, line 231. References: EGA IV (8.2.11), “X_A over f.g. subalgs”.

[Stacks, Tag 0388]. Let X be a scheme over a commutative ring k and let A be a k-algebra. A quasi-compact open V of the base change X_A is the inverse image of a quasi-compact open V' of X_{A'} for some finitely generated k-subalgebra A' ⊆ A.

The morphism X_A ⟶ X_{A'} along which V' is pulled back is characterised by its two projections: it covers the morphism Spec A ⟶ Spec A' induced by the inclusion A' ⊆ A and it commutes with the projection to X.

public theorem exists_fg_subalgebra_descending_isCompact_open
    {k A : Type u} [CommRing k] [CommRing A] [Algebra k A]
    (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
    (V : (pullback (Spec.map (CommRingCat.ofHom (algebraMap k A))) f).Opens)
    (hV : IsCompact V.1) :
    ∃ (A' : Subalgebra k A) (_ : A'.FG)
      (V' : (pullback (Spec.map (CommRingCat.ofHom (algebraMap k A'))) f).Opens),
      IsCompact V'.1 ∧
        ∃ p : pullback (Spec.map (CommRingCat.ofHom (algebraMap k A))) f ⟶
              pullback (Spec.map (CommRingCat.ofHom (algebraMap k A'))) f,
          p ≫ pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k A'))) f =
              pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k A))) f ≫
                Spec.map (CommRingCat.ofHom (Subalgebra.val A').toRingHom) ∧
            p ≫ pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k A'))) f =
              pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k A))) f ∧
            V = p ⁻¹ᵁ V'

Tag 038A, an equation

Tag 038A in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.galoisActionOnBaseChange, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleGaloisAction.lean, line 128 (StacksFrontier): “For a Galois extension kbar/k the group kbar ≃ₐ[k] kbar is Gal(kbar/k), and galoisActionOnBaseChange is the canonical action of its opposite group on X_kbar, induced by the automorphisms Spec σ of Spec kbar through the defining fibre product. The opposite group appears because Spec σ ≫ Spec τ = Spec (τ ∘ σ).”.

Tag 04KU, a lemma

Tag 04KU in the Stacks Project.

AlgebraicGeometry.exists_finite_subextension_descending_isCompact_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/QuasiCompactOpen.lean, line 407. The attribute's comment: “part (1)”.

A quasi-compact open in the base change of a scheme to an algebraic extension is pulled back from a quasi-compact open after a finite intermediate extension.

public theorem exists_finite_subextension_descending_isCompact_open
    {k K : Type u} [Field k] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
    (V : (pullback f (spectrumMap k K)).Opens) (hV : IsCompact V.1) :
    ∃ (E : IntermediateField k K) (_ : FiniteDimensional k E)
      (V' : (pullback f (spectrumMap k E)).Opens),
      IsCompact V'.1 ∧
        ∃ p : pullback f (spectrumMap k K) ⟶ pullback f (spectrumMap k E),
          p ≫ pullback.fst f (spectrumMap k E) = pullback.fst f (spectrumMap k K) ∧
          p ≫ pullback.snd f (spectrumMap k E) =
            pullback.snd f (spectrumMap k K) ≫ Spec.map (CommRingCat.ofHom E.val) ∧
          V = p ⁻¹ᵁ V'

AlgebraicGeometry.exists_open_subgroup_fixing_isCompact_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/QuasiCompactOpen.lean, line 483. The attribute's comment: “part (2)”.

A quasi-compact open in the base change of a scheme to a Galois extension is fixed by an open subgroup of the Galois group.

public theorem exists_open_subgroup_fixing_isCompact_open
    {k K : Type u} [Field k] [Field K] [Algebra k K] [IsGalois k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
    (V : (pullback f (spectrumMap k K)).Opens) (hV : IsCompact V.1) :
    ∃ H : Subgroup Gal(K/k), IsOpen (H : Set Gal(K/k)) ∧
      ∀ σ : Gal(K/k), σ ∈ H →
        ∃ a : pullback f (spectrumMap k K) ≅ pullback f (spectrumMap k K),
          a.hom ≫ pullback.fst f (spectrumMap k K) = pullback.fst f (spectrumMap k K) ∧
          a.hom ≫ pullback.snd f (spectrumMap k K) =
            pullback.snd f (spectrumMap k K) ≫
              Spec.map (CommRingCat.ofHom σ.toRingEquiv.toRingHom) ∧
      V = a.hom ⁻¹ᵁ V

Tag 038B, a lemma

Tag 038B in the Stacks Project.

AlgebraicGeometry.exists_closed_subset_with_preimage_eq_of_galois_invariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/GaloisInvariantClosed.lean, line 511.

Stacks Project, Tag 038B. A closed subset of a scheme after base change by a Galois field extension descends if it is invariant under the Galois group.

public theorem exists_closed_subset_with_preimage_eq_of_galois_invariant
    (k K : Type u) [Field k] [Field K] [Algebra k K] [IsGalois k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    (Tbar : Set (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme))
    (hTbar : IsClosed Tbar)
    (hstable : ∀ σ : K ≃ₐ[k] K,
      (galoisBaseChangeMap k K X f σ) ⁻¹' Tbar = Tbar) :
    ∃ T : Set X, IsClosed T ∧
      (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))) ⁻¹' T = Tbar

Tag 0389, a lemma

Tag 0389 in the Stacks Project.

AlgebraicGeometry.geometricallyConnected_iff_forall_finite_separable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedFiniteSeparable.lean, line 193. References: EGA IV (8.4.5), “more general”; EGA IV (4.5.17), “more general”.

A scheme over a field is geometrically connected if and only if its base change to every finite separable extension is connected.

public theorem geometricallyConnected_iff_forall_finite_separable
    {k : Type u} [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) :
    GeometricallyConnected f ↔
      ∀ (k' : Type u) [Field k'] [Algebra k k'] [FiniteDimensional k k']
        [Algebra.IsSeparable k k'],
        ConnectedSpace ↥(pullback f
          (Spec.map (CommRingCat.ofHom (algebraMap k k'))))

Tag 038C, a lemma

Tag 038C in the Stacks Project.

AlgebraicGeometry.not_connectedSpace_of_galois_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedGalois.lean, line 117.

Let kbar/k be a possibly infinite Galois extension and let T → X be a morphism of schemes over k. If T_kbar is connected and X_kbar is disconnected, then X is disconnected.

public theorem not_connectedSpace_of_galois_baseChange
    (k kbar : Type u) [Field k] [Field kbar] [Algebra k kbar] [IsGalois k kbar]
    {T X : Scheme.{u}} (f : T ⟶ X) (p : X ⟶ Spec (.of k))
    (hT : ConnectedSpace
      ((pullback (f ≫ p) (Spec.map <| ofHom <| algebraMap k kbar)) : Scheme.{u}))
    (hX : ¬ ConnectedSpace
      ((pullback p (Spec.map <| ofHom <| algebraMap k kbar)) : Scheme.{u})) :
    ¬ ConnectedSpace X

Tag 056R, a lemma

Tag 056R in the Stacks Project.

AlgebraicGeometry.geometricallyConnected_of_comp_of_connectedSpace, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedCriterion.lean, line 41.

If a connected scheme over a field admits a morphism over that field from a geometrically connected scheme, then it is geometrically connected.

public lemma geometricallyConnected_of_comp_of_connectedSpace
    (k : Type u) [Field k] {T X : Scheme.{u}} (f : T ⟶ X)
    (p : X ⟶ Spec (.of k)) [GeometricallyConnected (f ≫ p)] [ConnectedSpace X] :
    GeometricallyConnected p

Tag 04KV, a lemma

Tag 04KV in the Stacks Project.

AlgebraicGeometry.geometricallyConnected_of_connectedSpace_of_algebraicClosure_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedPoint.lean, line 47. The attribute's comment: “point with algebraically closed base field”.

Stacks Project, Tag 04KV. A connected scheme over a field is geometrically connected if the field is algebraically closed in the residue field of one of its points.

public theorem geometricallyConnected_of_connectedSpace_of_algebraicClosure_eq_bot
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [ConnectedSpace X] (x : X)
    (h : let : (f x).asIdeal.IsPrime := (f x).isPrime
      let := ((CommRingCat.ofHom (algebraMap k (f x).asIdeal.ResidueField)) ≫
        (Scheme.Spec.residueFieldIso (.of k) (f x)).inv ≫
        f.residueFieldMap x).hom.toAlgebra
      IsAlgClosedIn k (X.residueField x)) :
    GeometricallyConnected f

AlgebraicGeometry.geometricallyConnected_of_connectedSpace_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedPoint.lean, line 100. The attribute's comment: “rational-point consequence”. References: SGA 3 VIA (2.1.2), “Y = Spec of field ext”.

Stacks Project, Tag 04KV, rational-point consequence. A connected scheme over a field with a rational point is geometrically connected.

public theorem geometricallyConnected_of_connectedSpace_of_section
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [ConnectedSpace X] (s : Spec (.of k) ⟶ X) (hs : s ≫ f = 𝟙 _) :
    GeometricallyConnected f

Tag 04PY, a lemma

Tag 04PY in the Stacks Project.

Declarations registered for the tag:

Continuous.preimage_connectedComponent registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch33.lean, line 46 (StacksFrontier): “for the continuous map X_K → X; stated for any continuous map”.

Tag 07VM, a lemma

Tag 07VM in the Stacks Project.

AlgebraicGeometry.baseChange_image_connectedComponent_eq_connectedComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedComponentsFiniteExtension.lean, line 98. References: EGA IV (4.4.1), “partial, special case”; SGA 3 VIA (2.4.1), “partial”.

Stacks Project, Tag 07VM. Let K/k be a finite extension of fields and let X be a scheme over k. The projection X_K → X sends every connected component of X_K onto a connected component of X.

public theorem baseChange_image_connectedComponent_eq_connectedComponent
    {X : Scheme.{u}} (k K : Type u) [Field k] [Field K] [Algebra k K] [FiniteDimensional k K]
    (f : X ⟶ Spec (.of k))
    (t : ↥(pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))))) :
    (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base ''
        connectedComponent t =
      connectedComponent
        ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base t)

Tag 04PZ, a lemma

Tag 04PZ in the Stacks Project.

AlgebraicGeometry.image_connectedComponent_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedComponentsFieldExtension.lean, line 443. References: EGA IV (4.4.1), “partial”; SGA 3 VIA (2.4.1), “partial”; SGA 3 VIB (1.4.1), “partial”.

Stacks Project, Tag 04PZ (Gabber). Let K/k be an extension of fields -- not assumed finite, algebraic or separable -- and let X be a scheme over k. The projection X_K ⟶ X sends every connected component of X_K onto a connected component of X: the image of the connected component of a point x is the connected component of its image.

theorem image_connectedComponent_baseChange
    {X : Scheme.{u}} (k K : Type u) [Field k] [Field K] [Algebra k K]
    (f : X ⟶ Spec (.of k))
    (x : ↥(pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))))) :
    (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base ''
        connectedComponent x =
      connectedComponent
        ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base x)

Tag 038D, a lemma

Tag 038D in the Stacks Project.

AlgebraicGeometry.galoisActionOnGeometricConnectedComponents, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedGaloisAction.lean, line 95. The attribute's comment: “galois_action_on_geometric_connected_components”.

The canonical action of the opposite Galois group on the connected components of a scheme after base change. A component is sent to its image under the corresponding automorphism of the base-changed scheme.

public noncomputable def galoisActionOnGeometricConnectedComponents
    (X : Over (Spec (.of R))) :
    Action (Type u) (MulOpposite (S ≃ₐ[R] S))

AlgebraicGeometry.galoisActionOnGeometricConnectedComponents_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedGaloisAction.lean, line 175. The attribute's comment: “base_extension_compatibility”.

Restriction of Galois automorphisms commutes with the canonical map on the connected components of the two geometric base changes.

public theorem galoisActionOnGeometricConnectedComponents_baseChange
    (k' : Type u) [Field k'] [Algebra k k'] [Algebra k' kbar']
    [IsScalarTower k k' kbar'] [Normal k kbar]
    (p : pullback X.hom (spectrumMap k kbar') ⟶ pullback X.hom (spectrumMap k kbar))
    (hp₁ : p ≫ pullback.fst X.hom (spectrumMap k kbar) =
      pullback.fst X.hom (spectrumMap k kbar'))
    (hp₂ : p ≫ pullback.snd X.hom (spectrumMap k kbar) =
      pullback.snd X.hom (spectrumMap k kbar') ≫
        Spec.map (CommRingCat.ofHom (algebraMap kbar kbar')))
    (σ : kbar' ≃ₐ[k'] kbar')
    (C : ConnectedComponents (galoisActionOnBaseChange k kbar' X).V) :
    p.continuous.connectedComponentsMap
        (ConcreteCategory.hom
          ((galoisActionOnGeometricConnectedComponents k kbar' X).ρ
            (MulOpposite.op (σ.restrictScalars k))).asHom C) =
      ConcreteCategory.hom
        ((galoisActionOnGeometricConnectedComponents k kbar X).ρ
          (MulOpposite.op ((σ.restrictScalars k).restrictNormal kbar))).asHom
        (p.continuous.connectedComponentsMap C)

AlgebraicGeometry.baseChangeComparison_connectedComponents_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedGaloisAction.lean, line 222. The attribute's comment: “base_extension_compatibility”.

The canonical base-extension map is bijective on geometric connected components.

public theorem baseChangeComparison_connectedComponents_bijective
    [IsSepClosed kbar]
    (p : pullback X.hom (spectrumMap k kbar') ⟶ pullback X.hom (spectrumMap k kbar))
    (hp₁ : p ≫ pullback.fst X.hom (spectrumMap k kbar) =
      pullback.fst X.hom (spectrumMap k kbar'))
    (hp₂ : p ≫ pullback.snd X.hom (spectrumMap k kbar) =
      pullback.snd X.hom (spectrumMap k kbar') ≫
        Spec.map (CommRingCat.ofHom (algebraMap kbar kbar'))) :
    Function.Bijective p.continuous.connectedComponentsMap

AlgebraicGeometry.galoisActionOnGeometricConnectedComponents_fixed_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedGaloisFixed.lean, line 318. The attribute's comment: “fixed_components”.

Stacks Project, Tag 038D. A connected component of the base change of X to a separable algebraic closure kbar of k is fixed by the Galois action if and only if it is the inverse image of a connected component of X which is geometrically connected over k.

public theorem galoisActionOnGeometricConnectedComponents_fixed_iff
    (k kbar : Type u) [Field k] [Field kbar] [Algebra k kbar] [IsSepClosure k kbar]
    (X : Over (Spec (.of k)))
    (C : ConnectedComponents (galoisActionOnBaseChange k kbar X).V) :
    (∀ σ : MulOpposite (kbar ≃ₐ[k] kbar),
        ConcreteCategory.hom
          ((galoisActionOnGeometricConnectedComponents k kbar X).ρ σ).asHom C = C) ↔
      ∃ T : Set X.left, (∃ x : X.left, T = connectedComponent x) ∧
        IsGeometricallyConnectedSubset X.hom T ∧
        ⇑(pullback.fst X.hom (spectrumMap k kbar)) ⁻¹' T =
          ConnectedComponents.mk ⁻¹' {C}

Tag 038E, a lemma

Tag 038E in the Stacks Project.

AlgebraicGeometry.finite_geometricConnectedComponents_of_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedGaloisContinuity.lean, line 100. The attribute's comment: “part (a)”.

Open connected components of the geometric base change of a quasi-compact scheme are finite in number.

public theorem finite_geometricConnectedComponents_of_isOpen
    [CompactSpace X.left]
    (hopen : ∀ x : (galoisActionOnBaseChange k ksep X).V,
      IsOpen (connectedComponent x)) :
    Finite (ConnectedComponents (galoisActionOnBaseChange k ksep X).V)

AlgebraicGeometry.continuous_galoisActionOnGeometricConnectedComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedGaloisContinuity.lean, line 113. The attribute's comment: “part (b)”.

The absolute Galois action on open geometric connected components of a quasi-compact scheme is continuous for the Krull topology.

public theorem continuous_galoisActionOnGeometricConnectedComponents
    [CompactSpace X.left]
    (hopen : ∀ x : (galoisActionOnBaseChange k ksep X).V,
      IsOpen (connectedComponent x)) :
    let : TopologicalSpace (galoisActionOnGeometricConnectedComponents k ksep X).V :=
      (inferInstance : TopologicalSpace
        (ConnectedComponents (galoisActionOnBaseChange k ksep X).V))
    Continuous (fun p : MulOpposite (ksep ≃ₐ[k] ksep) ×
        ConnectedComponents (galoisActionOnBaseChange k ksep X).V =>
      ConcreteCategory.hom
        ((galoisActionOnGeometricConnectedComponents k ksep X).ρ p.1).asHom p.2)

AlgebraicGeometry.isOpen_geometricConnectedComponent_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedGaloisContinuity.lean, line 168. The attribute's comment: “finite type implies assumption (2)”.

The geometric connected components of a scheme of finite type over a field are open.

public theorem isOpen_geometricConnectedComponent_of_finiteType
    [LocallyOfFiniteType X.hom] [QuasiCompact X.hom]
    (x : (galoisActionOnBaseChange k ksep X).V) :
    IsOpen (connectedComponent x)

Declarations registered for the tag:

AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ConnectedGaloisContinuity.lean, line 50 (StacksFrontier): “finite type implies assumption (1)”. References: SGA 3 VIB (10.1), “Y is quasi-compact”; SGA 4 VI (1.14), “(i), special case”; SGA 4 VIII (5.1), “partial”.

Sources

LeanAlgebraicGeometry.GeometricallyConnected · AlgebraicGeometry.geometricallyConnected_iff_baseChange_fieldExtension · AlgebraicGeometry.pullback_snd_connectedComponentsMap_bijective · AlgebraicGeometry.geometricallyConnected_spec_iff · AlgebraicGeometry.baseChange_connectedComponents_bijective · AlgebraicGeometry.geometricallyConnected_iff_connectedSpace · AlgebraicGeometry.geometricallyConnected_iff_connectedSpace_baseChange · AlgebraicGeometry.exists_fg_subalgebra_descending_isCompact_open

Section33.8 Geometrically irreducible schemes #

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

Tag 0365, a definition

Tag 0365 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.GeometricallyIrreducible registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch33.lean, line 52 (StacksFrontier): “geometrically irreducible, for a morphism; the tag is the case of X ⟶ Spec k”. References: EGA IV (4.5.2), “more general”; EGA IV (4.5.5); EGA IV (4.5.9).

Tag 054P, a lemma

Tag 054P in the Stacks Project.

AlgebraicGeometry.geometricallyIrreducible_iff_baseChange_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleBaseChange.lean, line 42.

Stacks Project, Tag 054P. A scheme over a field is geometrically irreducible if and only if its base change along any field extension is geometrically irreducible.

public theorem geometricallyIrreducible_iff_baseChange_fieldExtension
    (k k' : Type u) [Field k] [Field k'] [Algebra k k'] {X : Scheme.{u}}
    (f : X ⟶ Spec (of k)) :
    GeometricallyIrreducible f ↔
      GeometricallyIrreducible
        (pullback.snd f (Spec.map (ofHom (algebraMap k k'))))

Tag 020J, a lemma

Tag 020J in the Stacks Project.

AlgebraicGeometry.geometricallyIrreducible_of_irreducibleSpace_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleSeparablyClosed.lean, line 53. References: EGA IV (4.4.4), “more general”; EGA IV (4.5.9), “(b) ⇒ (a), special case”.

Stacks Project, Tag 020J. An irreducible scheme over a separably closed field is geometrically irreducible.

public theorem geometricallyIrreducible_of_irreducibleSpace_of_isSepClosed
    (k : Type u) [Field k] [IsSepClosed k] (X : Scheme.{u})
    (f : X ⟶ Spec (.of k)) [IrreducibleSpace X] : GeometricallyIrreducible f

Tag 038F, a lemma

Tag 038F in the Stacks Project.

AlgebraicGeometry.bijOn_image_irreducibleComponents_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleProductProjection.lean, line 88. References: EGA IV (4.5.8), “more general”.

Stacks 038F. Let k be a field and let X, Y be schemes over k, presented by their structure maps f : X ⟶ Spec k and g : Y ⟶ Spec k. If X is geometrically irreducible over k, then X ×_k Y ⟶ Y induces a bijection between irreducible components: taking images along it is a bijection from the irreducible components of X ×_k Y onto the irreducible components of Y.

public theorem bijOn_image_irreducibleComponents_pullback_snd
    (k : Type u) [Field k] {X Y : Scheme.{u}} (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k))
    [GeometricallyIrreducible f] :
    Set.BijOn (fun Z ↦ (pullback.snd f g).base '' Z)
      (irreducibleComponents (pullback (C := Scheme.{u}) f g))
      (irreducibleComponents Y)

Tag 038G, a lemma

Tag 038G in the Stacks Project.

AlgebraicGeometry.geometricallyIrreducible_tfae_local, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleLocal.lean, line 118. The attribute's comment: “equivalent conditions”.

Stacks Project, Tag 038G. For a scheme over a field, geometric irreducibility is equivalent to each of the three stated local criteria.

public theorem geometricallyIrreducible_tfae_local
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) :
    let geometricallyIrreducibleSections := fun U : X.Opens ↦
      let : Algebra k Γ(X, U) :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appLE ⊤ U (by simp)).hom.toAlgebra
      Algebra.IsGeometricallyIrreducible k Γ(X, U)
    List.TFAE
      [ GeometricallyIrreducible f,
        Nonempty X ∧ ∀ U : X.affineOpens,
          Nonempty (U : Set X) → geometricallyIrreducibleSections U.1,
        IrreducibleSpace X ∧
          ∃ (I : Type u) (U : I → X.affineOpens),
            (⨆ i, (U i).1) = ⊤ ∧ ∀ i, geometricallyIrreducibleSections (U i).1,
        ∃ (I : Type u) (_ : Nonempty I) (U : I → X.Opens),
          (⨆ i, U i) = ⊤ ∧
            (∀ i, GeometricallyIrreducible ((U i).ι ≫ f)) ∧
            ∀ i j, U i ⊓ U j ≠ ⊥ ]

AlgebraicGeometry.geometricallyIrreducible_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleLocal.lean, line 186. The attribute's comment: “nonempty open subschemes”.

Stacks Project, Tag 038G. Every nonempty open subscheme of a geometrically irreducible scheme over a field is geometrically irreducible.

public theorem geometricallyIrreducible_open
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [GeometricallyIrreducible f] (U : X.Opens) (hU : Nonempty U) :
    GeometricallyIrreducible (U.ι ≫ f)

Tag 054Q, a lemma

Tag 054Q in the Stacks Project.

AlgebraicGeometry.geometricallyIrreducible_fiber_iff_isGeometricallyIrreducible_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/GenericFibreResidueFieldCriterion.lean, line 82. The attribute's comment: “the generic fibre, read on the residue field of the source”. References: EGA IV (4.5.12), “more general”.

The generic fibre is geometrically irreducible exactly when the residue field at the generic point is. Let R be a domain and let f : X ⟶ Spec R carry the generic point of an irreducible X to the generic point η of Spec R. Then the generic fibre of f is geometrically irreducible over κ(η) if and only if the residue field of X at its generic point is geometrically irreducible over κ(η).

This is [Stacks, Tag 054Q] applied to the generic fibre, which is irreducible by AlgebraicGeometry.Scheme.Hom.irreducibleSpace_fiber_of_genericPoint, followed by the identification AlgebraicGeometry.genericFiberResidueFieldMap of its residue field at its generic point with that of X. X is not assumed reduced.

theorem geometricallyIrreducible_fiber_iff_isGeometricallyIrreducible_residueField :
    letI := residueFieldAlgebraOfEq f hgen
    GeometricallyIrreducible (f.fiberToSpecResidueField (genericPoint (Spec R))) ↔
      Algebra.IsGeometricallyIrreducible
        ↥((Spec R).residueField (genericPoint (Spec R))) ↥(X.residueField (genericPoint X))

AlgebraicGeometry.geometricallyIrreducible_fiber_genericPoint_iff_residueField_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/GenericFibreResidueFieldCriterion.lean, line 147. The attribute's comment: “the generic fibre over an affine base, read on the residue field of the source”. References: EGA IV (4.5.12), “more general”.

The generic fibre over an integral affine base is geometrically irreducible exactly when the residue field at the generic point is. The criterion AlgebraicGeometry.geometricallyIrreducible_fiber_iff_isGeometricallyIrreducible_residueField for a base presented as an integral affine scheme rather than literally as the spectrum of a domain; the residue field of the base is then written at the generic point of Spec Γ(Y, ⊤), which is where a fraction-field presentation of it is available.

theorem geometricallyIrreducible_fiber_genericPoint_iff_residueField_of_isAffine
    (hgen : f (genericPoint X) = genericPoint Y) :
    letI := residueFieldAlgebraOfEq (f ≫ Y.isoSpec.hom) (comp_isoSpec_genericPoint_eq f hgen)
    GeometricallyIrreducible (f.fiberToSpecResidueField (genericPoint Y)) ↔
      Algebra.IsGeometricallyIrreducible
        ↥((Spec Γ(Y, ⊤)).residueField (genericPoint (Spec Γ(Y, ⊤))))
        ↥(X.residueField (genericPoint X))

AlgebraicGeometry.geometricallyIrreducible_tfae_functionField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricIrreducibleComponents/FunctionField.lean, line 277. References: EGA IV (4.5.12); EGA IV (4.5.9), “(a) ⇔ (c)”.

Stacks Project, Tag 054Q. For an irreducible scheme X over a field k, the following are equivalent: X is geometrically irreducible over k; the residue field at a generic point is geometrically irreducible over k; and the separable closure of k in that residue field is trivial.

public theorem geometricallyIrreducible_tfae_functionField
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [IrreducibleSpace X] (ξ : X) (hξ : IsGenericPoint ξ Set.univ) :
    letI : Algebra k (X.residueField ξ) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation ξ).hom.toAlgebra
    List.TFAE [
      GeometricallyIrreducible f,
      Algebra.IsGeometricallyIrreducible k (X.residueField ξ),
      separableClosure k (X.residueField ξ) = ⊥]

Algebra.isGeometricallyIrreducible_tfae_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GeometricallyIntegral/GenericPointIrreducible.lean, line 188. The attribute's comment: “The affine case. The source states this for an irreducible scheme X over k and the residue field at its generic point; here X = Spec A, and that the spectrum is irreducible is expressed by the hypothesis that the nilradical of A is the prime I. The scheme-level statement is NOT proved here: deducing it needs in addition the reduction of geometric irreducibility to affine opens (Stacks 038G, formalized as AlgebraicGeometry.geometricallyIrreducible_tfae_local) and the identification of the residue field at the generic point with the generic residue field of an affine open's ring of sections.”.

Let A be an algebra over a field k whose spectrum is irreducible, i.e. whose nilradical I is prime; I is then the generic point of Spec A and κ(I) is the function field. The following are equivalent.

A is geometrically irreducible over k;

κ(I) is geometrically irreducible over k;

the separable closure of k in κ(I) is k itself.

theorem isGeometricallyIrreducible_tfae_residueField (k A : Type u) [Field k] [CommRing A]
    [Algebra k A] (I : Ideal A) [I.IsPrime] (hI : I = nilradical A) :
    List.TFAE [IsGeometricallyIrreducible k A, IsGeometricallyIrreducible k I.ResidueField,
      separableClosure k I.ResidueField = ⊥]

Tag 0H8G, a lemma

Tag 0H8G in the Stacks Project.

AlgebraicGeometry.geometricallyIrreducible_iff_irreducibleSpace_self_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleSelfProduct.lean, line 311. References: EGA IV (4.5.8), “(i), special case”.

Stacks Project, Tag 0H8G. A scheme over a field is geometrically irreducible if and only if its self-product over the field is irreducible.

public theorem geometricallyIrreducible_iff_irreducibleSpace_self_pullback
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    GeometricallyIrreducible f ↔ IrreducibleSpace ↥(pullback f f)

Tag 038H, a lemma

Tag 038H in the Stacks Project.

AlgebraicGeometry.bijOn_irreducibleComponents_baseChange_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleSeparablyClosed.lean, line 71. References: EGA IV (4.5.19), “partial, special case”; EGA IV (4.5.21), “more general”; EGA IV (4.5.6), “(i), special case”; SGA 3 VIA (2.6.0), “k sep. alg. closed”.

Stacks Project, Tag 038H. If k is separably algebraically closed, k' / k is a field extension, and X is a scheme over k, then the projection X_{k'} ⟶ X induces a bijection on irreducible components.

public theorem bijOn_irreducibleComponents_baseChange_of_isSepClosed
    (k k' : Type u) [Field k] [IsSepClosed k] [Field k'] [Algebra k k']
    (X : Scheme.{u}) (f : X ⟶ Spec (of k)) :
    Set.BijOn
      (fun Z ↦
        (pullback.fst (C := Scheme.{u}) f (Spec.map (ofHom (algebraMap k k')))).base '' Z)
      (irreducibleComponents
        (pullback (C := Scheme.{u}) f (Spec.map (ofHom (algebraMap k k')))))
      (irreducibleComponents X)

Tag 038I, a lemma

Tag 038I in the Stacks Project.

AlgebraicGeometry.geometricallyIrreducible_tfae_of_isSepClosure, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleSeparableClosure.lean, line 63. References: EGA IV (4.5.9).

Stacks Project, Tag 038I. Geometric irreducibility of a scheme over a field can be tested after every finite separable extension, or after base change to any separable algebraic closure.

public lemma geometricallyIrreducible_tfae_of_isSepClosure
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    (ksep : Type u) [Field ksep] [Algebra k ksep] [IsSepClosure k ksep] :
    List.TFAE
      [GeometricallyIrreducible f,
        ∀ (k' : Type u) [Field k'] [Algebra k k'] [FiniteDimensional k k']
          [Algebra.IsSeparable k k'],
          IrreducibleSpace ↥(pullback f (Spec.map (ofHom (algebraMap k k')))),
    IrreducibleSpace ↥(pullback f (Spec.map (ofHom (algebraMap k ksep))))]

Tag 04KW, a lemma

Tag 04KW in the Stacks Project.

AlgebraicGeometry.preimage_irreducibleComponent_eq_sUnion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/IrreducibleComponentsBaseChange.lean, line 67.

Stacks Project, Tag 04KW. After extension of the base field, the inverse image of an irreducible component is a union of irreducible components.

public theorem preimage_irreducibleComponent_eq_sUnion
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    (T : Set X) (hT : T ∈ irreducibleComponents X) :
    let p : Scheme.{u} :=
      pullback (C := Scheme) f (Spec.map (CommRingCat.ofHom (algebraMap k K)))
    let π : p ⟶ X :=
      pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))
    π.base ⁻¹' T =
      ⋃₀ {Z : Set p | Z ∈ irreducibleComponents p ∧ Z ⊆ π.base ⁻¹' T}

Tag 04KX, a lemma

Tag 04KX in the Stacks Project.

AlgebraicGeometry.mapsTo_irreducibleComponents_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/IrreducibleComponentsBaseChange.lean, line 237. References: SGA 3 VIA (2.6.0).

Stacks Project, Tag 04KX. Let K/k be an extension of fields and let X be a scheme over k. The image of every irreducible component of X ×_{Spec k} Spec K under the projection to X is an irreducible component of X.

public theorem mapsTo_irreducibleComponents_baseChange
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    Set.MapsTo
      (fun Z ↦ (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base '' Z)
      (irreducibleComponents
        (pullback (C := Scheme) f (Spec.map (CommRingCat.ofHom (algebraMap k K)))))
      (irreducibleComponents X)

AlgebraicGeometry.surjOn_irreducibleComponents_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/IrreducibleComponentsBaseChange.lean, line 290.

Stacks Project, Tag 04KX. Let K/k be an extension of fields and let X be a scheme over k. Every irreducible component of X is the image of an irreducible component of X ×_{ Spec k} Spec K under the projection to X.

public theorem surjOn_irreducibleComponents_baseChange
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    Set.SurjOn
      (fun Z ↦ (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base '' Z)
      (irreducibleComponents
        (pullback (C := Scheme) f (Spec.map (CommRingCat.ofHom (algebraMap k K)))))
      (irreducibleComponents X)

Tag 0G69, a lemma

Tag 0G69 in the Stacks Project.

AlgebraicGeometry.geometricallyIrreducible_of_irreducibleSpace_of_dense_rationalPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleRationalPoints.lean, line 151.

Stacks Project, Tag 0G69. An irreducible scheme over a field with a dense set of rational points is geometrically irreducible.

theorem geometricallyIrreducible_of_irreducibleSpace_of_dense_rationalPoints
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [IrreducibleSpace X]
    (h : Dense {x : X | ∃ (s : Spec (.of k) ⟶ X),
      s ≫ f = 𝟙 (Spec (.of k)) ∧ x ∈ Set.range s.base}) :
    GeometricallyIrreducible f

Tag 038J, a lemma

Tag 038J in the Stacks Project.

AlgebraicGeometry.fixed_geometricComponent_iff_exists_geometricallyIrreducible_component, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GaloisFixedComponentDescent.lean, line 117. The attribute's comment: “fixed_component_descent”.

A geometric irreducible component is fixed by the Galois action exactly when it descends to a geometrically irreducible component of the original scheme.

theorem fixed_geometricComponent_iff_exists_geometricallyIrreducible_component
    (k ksep : Type u) [Field k] [Field ksep] [Algebra k ksep]
    [IsSepClosure k ksep]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    (Tbar : (galoisActionOnGeometricIrreducibleComponents k ksep (Over.mk f)).V) :
    (∀ σ : MulOpposite (ksep ≃ₐ[k] ksep),
      ConcreteCategory.hom
        ((galoisActionOnGeometricIrreducibleComponents k ksep (Over.mk f)).ρ σ).asHom Tbar =
        Tbar) ↔
      ∃ T : irreducibleComponents X,
        GeometricallyIrreducible
          ((Scheme.IdealSheafData.vanishingIdeal
              ⟨(T : Set X), isClosed_of_mem_irreducibleComponents T.1 T.2⟩).subschemeι ≫ f) ∧
        (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k ksep)))).base ⁻¹'
          (T : Set X) = Tbar.1

AlgebraicGeometry.galoisActionOnGeometricIrreducibleComponents, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleGaloisAction.lean, line 162. The attribute's comment: “galois_action_on_geometric_irreducible_components”.

The canonical action of the opposite Galois group on the irreducible components of a scheme after base change. A component is sent to its image under the corresponding automorphism of the base-changed scheme.

public noncomputable def galoisActionOnGeometricIrreducibleComponents
    (X : Over (Spec (.of R))) :
    Action (Type u) (MulOpposite (S ≃ₐ[R] S))

AlgebraicGeometry.galoisActionOnGeometricIrreducibleComponents_fixed_iff_and_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/IrreducibleGaloisActionCompatibility.lean, line 97. References: EGA IV (4.5.21), “more general”.

Stacks Project, Tag 038J. Let k be a field with separable algebraic closure ksep and let X be a scheme over k. The canonical action of Gal(ksep/k)ᵐᵒᵖ on the irreducible components of X_{ksep} has the following properties.

A component Tbar is fixed by the action if and only if there is an irreducible component T of X, geometrically irreducible over k, with T_{ksep} = Tbar.

For every field extension k'/k with separable algebraic closure ksep', and every embedding ksep → ksep' over k, taking images along X_{ksep'} ⟶ X_{ksep} is a bijection on irreducible components (Tag 038H), and it intertwines the action of Gal(ksep'/k') with the action of Gal(ksep/k) through restriction of automorphisms.

Geometric irreducibility of T is that of its reduced induced closed subscheme over k, and T_{ksep} is the inverse image of T in X_{ksep}.

public theorem galoisActionOnGeometricIrreducibleComponents_fixed_iff_and_compatible
    (k ksep : Type u) [Field k] [Field ksep] [Algebra k ksep] [IsSepClosure k ksep]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    (∀ Tbar : (galoisActionOnGeometricIrreducibleComponents k ksep (Over.mk f)).V,
      (∀ σ : MulOpposite (ksep ≃ₐ[k] ksep),
        ConcreteCategory.hom
          ((galoisActionOnGeometricIrreducibleComponents k ksep (Over.mk f)).ρ σ).asHom Tbar = Tbar) ↔
        ∃ T : irreducibleComponents X,
          GeometricallyIrreducible
            ((Scheme.IdealSheafData.vanishingIdeal
                ⟨(T : Set X), isClosed_of_mem_irreducibleComponents T.1 T.2⟩).subschemeι ≫ f) ∧
          (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k ksep)))).base ⁻¹'
            (T : Set X) = Tbar.1) ∧
    ∀ (k' ksep' : Type u) [Field k'] [Field ksep']
      [Algebra k k'] [Algebra k' ksep'] [Algebra k ksep'] [Algebra ksep ksep']
      [IsScalarTower k k' ksep'] [IsScalarTower k ksep ksep'] [IsSepClosure k' ksep'],
      Set.BijOn (fun Z ↦ (baseChangeComparison k ksep ksep' X f).base '' Z)
          (irreducibleComponents
            (pullback (C := Scheme.{u}) f (Spec.map (CommRingCat.ofHom (algebraMap k ksep')))))
          (irreducibleComponents
            (pullback (C := Scheme.{u}) f (Spec.map (CommRingCat.ofHom (algebraMap k ksep))))) ∧
        ∀ (σ : MulOpposite (ksep' ≃ₐ[k'] ksep'))
          (Z : (galoisActionOnGeometricIrreducibleComponents k ksep' (Over.mk f)).V),
          irreducibleComponentsBaseChangeComparisonEquiv k ksep ksep' (hsep :=
              IsSepClosure.sep_closed k) X f
            (ConcreteCategory.hom
              ((galoisActionOnGeometricIrreducibleComponents k ksep' (Over.mk f)).ρ
                (MulOpposite.op (AlgEquiv.restrictScalars k σ.unop))).asHom Z) =
          ConcreteCategory.hom
            ((galoisActionOnGeometricIrreducibleComponents k ksep (Over.mk f)).ρ
              (MulOpposite.op
                ((AlgEquiv.restrictNormalHom ksep) (AlgEquiv.restrictScalars k σ.unop)))).asHom
            (irreducibleComponentsBaseChangeComparisonEquiv k ksep ksep' (hsep :=
              IsSepClosure.sep_closed k) X f Z)

Tag 04KY, a lemma

Tag 04KY in the Stacks Project.

AlgebraicGeometry.fiber_irreducibleComponentsBaseChangeMap_eq_orbit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricIrreducibleComponents/GaloisOrbit.lean, line 465.

Stacks Project, Tag 04KY. For a scheme over a field k and a normal extension K/k, for instance a separable closure of k, the fibre through each geometric irreducible component of the canonical map to the irreducible components downstairs is its orbit under the group K ≃ₐ[k] K.

public theorem fiber_irreducibleComponentsBaseChangeMap_eq_orbit
    (k K : Type u) [Field k] [Field K] [Algebra k K] [Normal k K]
    (X : Over (Spec (.of k)))
    (Z : (galoisActionOnGeometricIrreducibleComponents k K X).V) :
    (irreducibleComponentsBaseChangeMap k K X) ⁻¹'
        {irreducibleComponentsBaseChangeMap k K X Z} =
      Set.range (fun σ : MulOpposite (K ≃ₐ[k] K) ↦
        ConcreteCategory.hom
          ((galoisActionOnGeometricIrreducibleComponents k K X).ρ σ).asHom Z)

Tag 04KZ, a lemma

Tag 04KZ in the Stacks Project.

AlgebraicGeometry.exists_finite_subextension_defining_component, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricIrreducibleComponents/FiniteExtension.lean, line 408. The attribute's comment: “component_defined_over_finite_extension”.

Stacks Project, Tag 04KZ. Every irreducible component after extension to a separable closure is defined over a finite intermediate extension.

public theorem exists_finite_subextension_defining_component
    {k K : Type u} [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    (Z : irreducibleComponents
      (pullback (C := Scheme.{u}) f (Spec.map (CommRingCat.ofHom (algebraMap k K))))) :
    ∃ (E : IntermediateField k K) (_ : FiniteDimensional k E)
      (T : irreducibleComponents
        (pullback (C := Scheme.{u}) f (Spec.map (CommRingCat.ofHom (algebraMap k E)))))
      (p : pullback (C := Scheme.{u}) f (Spec.map (CommRingCat.ofHom (algebraMap k K))) ⟶
        pullback (C := Scheme.{u}) f (Spec.map (CommRingCat.ofHom (algebraMap k E)))),
      p ≫ pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k E))) =
          pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K))) ∧
        p ≫ pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k E))) =
          pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k K))) ≫
            Spec.map (CommRingCat.ofHom E.val) ∧
        p.base ⁻¹' (T : Set _) = (Z : Set _)

AlgebraicGeometry.continuous_galoisActionOnGeometricIrreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricIrreducibleComponents/OrbitDecomposition.lean, line 85. The attribute's comment: “continuous_action”.

Stacks Project, Tag 04KZ. The Galois action on the geometric irreducible components of a locally finite-type scheme is continuous when the component set is discrete.

public theorem continuous_galoisActionOnGeometricIrreducibleComponents
    {k K : Type u} [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
    (X : Over (Spec (.of k))) [LocallyOfFiniteType X.hom] :
    letI : TopologicalSpace (galoisActionOnGeometricIrreducibleComponents k K X).V := ⊥
    Continuous (fun p : MulOpposite (K ≃ₐ[k] K) ×
        (galoisActionOnGeometricIrreducibleComponents k K X).V =>
      ConcreteCategory.hom
        ((galoisActionOnGeometricIrreducibleComponents k K X).ρ p.1).asHom p.2)

AlgebraicGeometry.exists_finite_single_orbit_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricIrreducibleComponents/OrbitDecomposition.lean, line 205. The attribute's comment: “finite_single_orbit_decomposition”.

Stacks Project, Tag 04KZ. Over a separable closure, the inverse image of an irreducible component is a finite union of irreducible components forming a single Galois orbit.

public theorem exists_finite_single_orbit_decomposition
    {k K : Type u} [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
    (X : Over (Spec (.of k))) [LocallyOfFiniteType X.hom]
    (T : irreducibleComponents X.left) :
    ∃ s : Finset (galoisActionOnGeometricIrreducibleComponents k K X).V,
      s.Nonempty ∧
        ((pullback.fst X.hom (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base ⁻¹'
              (T : Set X.left) =
            ⋃ Z ∈ s, Z.1) ∧
          ∀ Z ∈ s, ∀ Z' ∈ s,
            ∃ σ : MulOpposite (K ≃ₐ[k] K),
              ConcreteCategory.hom
                  ((galoisActionOnGeometricIrreducibleComponents k K X).ρ σ).asHom Z = Z'

Tag 054R, a lemma

Tag 054R in the Stacks Project.

AlgebraicGeometry.exists_finite_separable_extension_geometricallyIrreducible_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/ComponentsOverFiniteSeparableExtension.lean, line 272.

Stacks Project, Tag 054R. After a finite separable extension of the ground field, every irreducible component of a scheme locally of finite type over a field is geometrically irreducible, provided that the original scheme has only finitely many irreducible components.

public theorem exists_finite_separable_extension_geometricallyIrreducible_components
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (hX : (irreducibleComponents X).Finite) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k')
      (_ : FiniteDimensional k k') (_ : Algebra.IsSeparable k k'),
      let X' := pullback (C := Scheme.{u}) f (Spec.map (ofHom (algebraMap k k')))
      ∀ Z : irreducibleComponents X',
        GeometricallyIrreducible
          ((Scheme.IdealSheafData.vanishingIdeal (X := X')
              ⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.2⟩).subschemeι ≫
            pullback.snd f (Spec.map (ofHom (algebraMap k k'))))

Tag 054S, a lemma

Tag 054S in the Stacks Project.

TopologicalSpace.finite_connectedComponents_of_finite_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricIrreducibleComponents/ConnectedComponents.lean, line 59. The attribute's comment: “finiteness of connected components”.

Stacks Project, Tag 054S. Finitely many irreducible components imply finitely many connected components.

public theorem finite_connectedComponents_of_finite_irreducibleComponents
    {X : Type*} [TopologicalSpace X] (hX : (irreducibleComponents X).Finite) :
    Finite (ConnectedComponents X)

AlgebraicGeometry.geometricallyConnected_connectedComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricIrreducibleComponents/ConnectedComponents.lean, line 91. The attribute's comment: “geometric connectedness of connected components”. References: EGA IV (4.5.13.1), “(ii)”.

Stacks Project, Tag 054S. If each of the finitely many irreducible components of a scheme over a field is geometrically irreducible, each connected component has an open subscheme structure that is geometrically connected over that field.

public theorem geometricallyConnected_connectedComponent
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    (hX : (irreducibleComponents X).Finite)
    (hgeom : ∀ Z : irreducibleComponents X,
      GeometricallyIrreducible
        ((Scheme.IdealSheafData.vanishingIdeal (X := X)
            ⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.2⟩).subschemeι ≫ f))
    (c : ConnectedComponents X) :
    ∃ U : X.Opens,
      (U : Set X) = (ConnectedComponents.mk : X → ConnectedComponents X) ⁻¹' {c} ∧
        GeometricallyConnected (U.ι ≫ f)

Sources

Section33.9 Geometrically integral schemes #

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

Tag 020H, a definition

Tag 020H in the Stacks Project.

AlgebraicGeometry.GeometricallyPointwiseIntegralAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Integral.lean, line 57. The attribute's comment: “part (1)”.

A morphism f : X ⟶ Y is geometrically pointwise integral at x : X if, after every base change from the spectrum of a field, every point above x has an integral local ring.

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

AlgebraicGeometry.GeometricallyPointwiseIntegral, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Integral.lean, line 66. The attribute's comment: “part (2)”.

A morphism is geometrically pointwise integral if it is geometrically pointwise integral at every point of its source.

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

AlgebraicGeometry.geometricallyIntegral_iff_isIntegral_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Integral.lean, line 132. The attribute's comment: “part (3)”. References: EGA IV (4.6.2).

A scheme X over a field k is geometrically integral if and only if the base change X_{k'} is integral for every field extension k'/k.

public theorem geometricallyIntegral_iff_isIntegral_pullback {k : Type u} [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) :
    GeometricallyIntegral f ↔
      ∀ (K : Type u) [Field K] [Algebra k K],
        IsIntegral (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))))

Declarations registered for the tag:

AlgebraicGeometry.GeometricallyIntegral registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Integral.lean, line 142 (StacksFrontier): “part (3)”. References: EGA IV (4.6.2), “more general”; SGA 6 XII (1.2), “partial”.

Tag 038K, a lemma

Tag 038K in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch33.lean, line 55 (StacksFrontier). References: EGA IV (4.6.2), “more general”; EGA IV (4.6.14), “special case”; SGA 3 XIX (2.1), “partial”.

Tag 0BUG, a lemma

Tag 0BUG in the Stacks Project.

Stacks.AlgebraicGeometry.ProperSectionsGeom.componentwiseArtinianDecomposition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSectionsGeom/Components.lean, line 151. The attribute's comment: “clause (2): for an ARBITRARY proper scheme over a field, the global functions are a product of Artinian local algebras over that field with one factor for each connected component. The index set is the set of connected components itself, the product is finite because a proper scheme over a field is a Noetherian space, and the isomorphism is pinned to be simultaneous restriction, so the factor at a component is the ring of functions on that component. Openness of the components replaces the source's correspondence between primitive idempotents and components; the product decomposition is the sheaf condition for a disjoint open cover; each factor is Artinian because it is a quotient of the global functions, finite over the base field by clause (1), and local because its component is connected.”.

[Stacks, Tag 0BUG] (2). The ring of global functions on a scheme proper over a field k is a finite product of Artinian local k-algebras, with one factor for each connected component of X, the factor at a component being the ring of functions on that component and the isomorphism being simultaneous restriction.

No hypothesis beyond properness: X need not be connected, reduced, normal or integral, and the structure morphism need not be affine.

def componentwiseArtinianDecomposition [IsProper f] :
    GlobalSectionsComponentDecomposition k f

Stacks.AlgebraicGeometry.ProperSectionsGeom.isGeometricallyIrreducible_globalSections_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSectionsGeom/Connected.lean, line 116. The attribute's comment: “clause (5): for a GEOMETRICALLY CONNECTED proper scheme over a field k, the global sections are geometrically irreducible over k: every base change to a field extension of k has irreducible spectrum.”.

[Stacks, Tag 0BUG] (5). Let X be a geometrically connected proper scheme over a field k. Then the ring of global sections of X, with its canonical k-algebra structure, is geometrically irreducible over k.

theorem isGeometricallyIrreducible_globalSections_of_isProper
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [GeometricallyConnected f] [IsProper f] :
    letI : Algebra k Γ(X, ⊤) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    Algebra.IsGeometricallyIrreducible k Γ(X, ⊤)

Stacks.AlgebraicGeometry.ProperSectionsGeom.isGeometricallyIrreducible_globalSections_of_geometricallyIrreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSectionsGeom/Connected.lean, line 161. The attribute's comment: “clause (6): for a GEOMETRICALLY IRREDUCIBLE proper scheme over a field k, the global sections are geometrically irreducible over k. The source deduces this clause from clause (5) by the remark that a geometrically irreducible scheme is geometrically connected, and that is what is done here: every base change has an irreducible, hence connected, underlying space.”.

[Stacks, Tag 0BUG] (6). Let X be a geometrically irreducible proper scheme over a field k. Then the ring of global sections of X, with its canonical k-algebra structure, is geometrically irreducible over k.

A geometrically irreducible morphism is geometrically connected, every base change of it having an irreducible and hence connected underlying space, so this is clause (5) applied to the same X.

theorem isGeometricallyIrreducible_globalSections_of_geometricallyIrreducible
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [GeometricallyIrreducible f] [IsProper f] :
    letI : Algebra k Γ(X, ⊤) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    Algebra.IsGeometricallyIrreducible k Γ(X, ⊤)

Stacks.AlgebraicGeometry.ProperSectionsGeom.isField_globalSections_of_connectedSpace_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSectionsGeom/ConnectedLocal.lean, line 101. The attribute's comment: “special case of clauses (2) and (3): X connected and reduced, where the ring of global functions is a field”.

The ring of global functions on a connected reduced scheme proper over a field is a field.

This is clauses (2) and (3) read at a single connected component: a reduced Artinian local ring is a field. The clauses in full are componentwiseArtinianDecomposition (clause (2)) and globalSectionsFieldDecomposition_of_isReduced (clause (3)).

theorem isField_globalSections_of_connectedSpace_of_isReduced
    [IsProper f] [ConnectedSpace X] [AlgebraicGeometry.IsReduced X] : IsField Γ(X, ⊤)

Stacks.AlgebraicGeometry.ProperSectionsGeom.isSeparable_globalSections_of_connectedSpace_of_geometricallyReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSectionsGeom/ConnectedLocal.lean, line 115. The attribute's comment: “special case of clauses (2), (3) and (4): X connected and geometrically reduced, where the field of global functions is separable over k”.

The field of global functions on a connected geometrically reduced scheme proper over a field k is separable over k.

This is clauses (2), (3) and (4) read at a single connected component. The clauses in full are stated by other declarations, among them GlobalSectionsFieldDecomposition.factor_isSeparable (clause (4)).

theorem isSeparable_globalSections_of_connectedSpace_of_geometricallyReduced
    [IsProper f] [ConnectedSpace X] [GeometricallyReduced f] :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    Algebra.IsSeparable k Γ(X, ⊤)

Stacks.AlgebraicGeometry.ProperSectionsGeom.isIso_globalSections_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSectionsGeom/ReducedConnected.lean, line 136. The attribute's comment: “clause (7): for a GEOMETRICALLY REDUCED and GEOMETRICALLY CONNECTED proper scheme over a field k, the global sections are k. The equality A = k is stated canonically, as the induced homomorphism from k to the global sections being an isomorphism. Geometric irreducibility of the global sections (clause (5)) makes the extension purely inseparable; geometric reducedness of a stalk makes it separable (Tag 030W, Tag 035W); a purely inseparable separable extension is trivial. No finiteness of the global sections over k is used.”.

[Stacks, Tag 0BUG] (7). The canonical homomorphism from a field to the global sections of a geometrically reduced, geometrically connected proper scheme over that field is an isomorphism.

This is the whole of clause (7): the source's conclusion A = k is the assertion that the homomorphism k ⟶ Γ(X, 𝒪_X) induced by the structure morphism is an isomorphism, the standard identification Γ(Spec k, 𝒪) ≅ k being part of that map.

theorem isIso_globalSections_of_isProper
    [GeometricallyReduced f] [GeometricallyConnected f] [IsProper f] :
    IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop)

Stacks.AlgebraicGeometry.ProperSectionsGeom.moduleFinite_globalSections_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSectionsGeom/ReducedSections.lean, line 118. The attribute's comment: “clause (1): the global sections of an arbitrary proper scheme over a field form a finite module over that field, with no integrality, connectedness, normality, reducedness or affineness hypothesis. Finiteness of coherent cohomology over a field (Tag 02O6) plus coherence of the structure sheaf (Tag 01XZ), with the degree-zero identification of cohomology and sections supplied here from left exactness of global sections.”.

[Stacks, Tag 0BUG] (1). The ring of global functions on a scheme proper over a field k is a finite k-module, for the k-algebra structure the structure morphism induces.

No hypothesis beyond properness: the scheme need not be integral, connected, normal or reduced, and the structure morphism need not be affine.

theorem moduleFinite_globalSections_of_isProper [IsProper f] :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    Module.Finite k Γ(X, ⊤)

Stacks.AlgebraicGeometry.ProperSectionsGeom.globalSectionsFieldDecomposition_of_isReduced, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSectionsGeom/ReducedSections.lean, line 139. The attribute's comment: “clause (3): for a REDUCED proper scheme over a field, the presentation of the global sections as a finite product of finite field extensions of the base field. Clause (1) makes the ring Artinian; an Artinian reduced ring is the product of its residue fields. Reducedness only, where the library's normal-case decomposition needs each connected component irreducible. Separability of the factors is clause (4) and is not asserted here.”.

[Stacks, Tag 0BUG] (3). The ring of global functions on a reduced scheme proper over a field k is a finite product of finite field extensions of k.

The hypothesis is reducedness of X, weaker than the normality assumed by AlgebraicGeometry.globalSectionsFieldDecomposition_of_isNormal, which this supersedes.

def globalSectionsFieldDecomposition_of_isReduced [IsProper f] [IsReduced X] :
    GlobalSectionsFieldDecomposition k X f

Stacks.AlgebraicGeometry.ProperSectionsGeom.GlobalSectionsFieldDecomposition.factor_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSectionsGeom/Separable.lean, line 182. The attribute's comment: “clause (4): for a GEOMETRICALLY REDUCED proper scheme over a field k, every field factor of a presentation of the global sections as a finite product of finite field extensions of k (clause (3)) is separable over k. The decomposition is an argument, so the conclusion holds for every such presentation, in particular the one clause (3) constructs.”.

Every field factor in a finite product decomposition of the global sections of a geometrically reduced proper scheme is separable over the base field. Together with GlobalSectionsFieldDecomposition.factorModuleFinite, this says that every factor is a finite separable extension.

theorem GlobalSectionsFieldDecomposition.factor_isSeparable
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsProper f] [GeometricallyReduced f] (D : GlobalSectionsFieldDecomposition k X f)
    (i : Fin D.numFactors) : Algebra.IsSeparable k (D.factor i)

AlgebraicGeometry.isIso_globalSections_of_geometricallyIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ProperGlobalSections.lean, line 85. The attribute's comment: “clause (8): for a GEOMETRICALLY INTEGRAL proper scheme over a field k, the global sections are k. The equality A = k is stated canonically, as the induced homomorphism from k to the global sections being an isomorphism. The source deduces this clause from clause (7): a geometrically integral morphism is geometrically reduced, and geometrically connected because every base change of it has an integral, hence irreducible, hence connected, underlying space.”.

The canonical homomorphism from a field to the global sections of a geometrically integral proper scheme over that field is an isomorphism.

theorem isIso_globalSections_of_geometricallyIntegral
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [GeometricallyIntegral f] [IsProper f] :
    IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop)

Tag 0FD1, a lemma

Tag 0FD1 in the Stacks Project.

Stacks.AlgebraicGeometry.ProperGeomConnected.geometricallyConnected_toSpecΓ_of_isProper_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GeomConnectedFibres/Basic.lean, line 135. References: EGA III (4.3.4), “special case”.

Stacks Project, Tag 0FD1. If X is proper over a field, then the canonical morphism from X to the spectrum of its ring of global sections has geometrically connected fibres.

theorem geometricallyConnected_toSpecΓ_of_isProper_over_field (k : Type u) [Field k]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [IsProper f] :
    GeometricallyConnected X.toSpecΓ

Tag 0FD2, a lemma

Tag 0FD2 in the Stacks Project.

AlgebraicGeometry.isIso_globalSections_iff_geometricallyConnected, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ProperGlobalSections.lean, line 64.

A proper geometrically reduced scheme over a field has only constant global functions exactly when it is geometrically connected.

theorem isIso_globalSections_iff_geometricallyConnected
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsProper f] [GeometricallyReduced f] :
    IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop) ↔ GeometricallyConnected f

Sources

LeanAlgebraicGeometry.GeometricallyPointwiseIntegralAt · AlgebraicGeometry.GeometricallyPointwiseIntegral · AlgebraicGeometry.geometricallyIntegral_iff_isIntegral_pullback · AlgebraicGeometry.GeometricallyIntegral · AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible · Stacks.AlgebraicGeometry.ProperSectionsGeom.componentwiseArtinianDecomposition · Stacks.AlgebraicGeometry.ProperSectionsGeom.isGeometricallyIrreducible_globalSections_of_isProper · Stacks.AlgebraicGeometry.ProperSectionsGeom.isGeometricallyIrreducible_globalSections_of_geometricallyIrreducible

Section33.10 Geometrically normal schemes #

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

Tag 038M, a definition

Tag 038M in the Stacks Project.

AlgebraicGeometry.IsGeometricallyNormalAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Normal.lean, line 53. The attribute's comment: “part (1)”. References: EGA IV (6.7.6); EGA IV (6.7.8).

A scheme X ⟶ Spec k is geometrically normal at x if, after every field extension K / k, the local ring at every point of the base change lying over x is normal.

public def IsGeometricallyNormalAt (f : X ⟶ Spec (.of k)) (x : X) : Prop

AlgebraicGeometry.IsGeometricallyNormal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Normal.lean, line 62. The attribute's comment: “part (2)”. References: EGA IV (6.7.6).

A scheme over k is geometrically normal if it is geometrically normal at every point.

public def IsGeometricallyNormal (f : X ⟶ Spec (.of k)) : Prop

Tag 038N, a lemma

Tag 038N in the Stacks Project.

AlgebraicGeometry.geometricallyNormalAt_tfae, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/Normal.lean, line 133.

Geometric normality at a point is equivalent both to normality at every point above it after every finite purely inseparable field extension and to geometric normality of its local ring over the ground field.

lemma geometricallyNormalAt_tfae
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) (x : X) :
    List.TFAE [
      IsGeometricallyNormalAt f x,
      ∀ (K : Type u) [Field K] [Algebra k K] [Module.Finite k K]
        [IsPurelyInseparable k K],
        ∀ (x' : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u})),
          pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K))) x' = x →
            IsNormalRing
              ((pullback f
                (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}).presheaf.stalk x'),
      letI : Algebra k (X.presheaf.stalk x) :=
        letI : Algebra k ((Spec (.of k)).presheaf.stalk (f.base x)) :=
          StructureSheaf.stalkAlgebra k (f.base x)
        ((f.stalkMap x).hom.comp
          (algebraMap k ((Spec (.of k)).presheaf.stalk (f.base x)))).toAlgebra
      Algebra.IsGeometricallyNormal k (X.presheaf.stalk x)]

Tag 038O, a lemma

Tag 038O in the Stacks Project.

AlgebraicGeometry.geometricallyNormal_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/NormalTFAE.lean, line 211.

Stacks Project, Tag 038O. The six standard characterizations of geometric normality for a scheme over a field are equivalent.

public theorem geometricallyNormal_tfae
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    let geometricallyNormalSections := fun U : X.Opens ↦
      letI : Algebra k Γ(X, U) :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appLE ⊤ U (by simp)).hom.toAlgebra
      Algebra.IsGeometricallyNormal k Γ(X, U)
    List.TFAE
      [ IsGeometricallyNormal f,
        ∀ (k' : Type u) [Field k'] [Algebra k k'],
          IsNormal (pullback f (Spec.map (ofHom (algebraMap k k')))),
        ∀ (k' : Type u) [Field k'] [Algebra k k'] [Algebra.EssFiniteType k k'],
          IsNormal (pullback f (Spec.map (ofHom (algebraMap k k')))),
        ∀ (k' : Type u) [Field k'] [Algebra k k'] [Module.Finite k k']
          [IsPurelyInseparable k k'],
          IsNormal (pullback f (Spec.map (ofHom (algebraMap k k')))),
        ∀ U : X.affineOpens, geometricallyNormalSections U.1,
        IsNormal (pullback f (Spec.map
          (ofHom (algebraMap k (perfectClosure k (AlgebraicClosure k)))))) ]

Tag 038P, a lemma

Tag 038P in the Stacks Project.

AlgebraicGeometry.isGeometricallyNormal_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NormalMorphism/BaseFieldExtension.lean, line 93. The attribute's comment: “global equivalence”. References: EGA IV (6.7.8), “(vi) global”.

Stacks Project, Tag 038P. Geometric normality of a scheme over a field is invariant under extension of the ground field.

public theorem isGeometricallyNormal_iff_baseChange (k K : Type u) [Field k] [Field K]
    [Algebra k K] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    IsGeometricallyNormal f ↔
      IsGeometricallyNormal (pullback.snd f (Spec.map (ofHom (algebraMap k K))))

AlgebraicGeometry.isGeometricallyNormalAt_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/Normal.lean, line 292. The attribute's comment: “pointwise equivalence”. References: EGA IV (6.7.8), “(vi)”.

Geometric normality at a point is invariant under extension of the base field.

theorem isGeometricallyNormalAt_iff_baseChange
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    (K : Type u) [Field K] [Algebra k K]
    (x : X) (x' : (pullback f (Spec.map (ofHom (algebraMap k K))) : Scheme.{u}))
    (hx' : (pullback.fst f (Spec.map (ofHom (algebraMap k K)))).base x' = x) :
    IsGeometricallyNormalAt f x ↔
      IsGeometricallyNormalAt
        (pullback.snd f (Spec.map (ofHom (algebraMap k K)))) x'

AlgebraicGeometry.isGeometricallyNormal_iff_baseChange_of_isGeometricallyNormalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/Normal.lean, line 323. The attribute's comment: “global equivalence”. References: EGA IV (6.7.8), “(vi) global”; EGA IV (7.3.8), “partial”.

A scheme is geometrically normal exactly when any base field extension is.

theorem isGeometricallyNormal_iff_baseChange_of_isGeometricallyNormalAt
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    (K : Type u) [Field K] [Algebra k K] :
    IsGeometricallyNormal f ↔
      IsGeometricallyNormal
        (pullback.snd f (Spec.map (ofHom (algebraMap k K))))

Tag 06DG, a lemma

Tag 06DG in the Stacks Project.

AlgebraicGeometry.isNormal_pullback_of_isGeometricallyNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcDescentProperties/PullbackNormal.lean, line 177. References: EGA IV (6.14.1), “base = Spec of a field”; EGA IV (21.14.4), “more general”; EGA IV (7.3.9), “more general”.

Stacks Project, Tag 06DG. The fibre product over a field of a geometrically normal scheme and a normal scheme is normal.

public theorem isNormal_pullback_of_isGeometricallyNormal {k : Type u} [Field k]
    {X Y : Scheme.{u}} (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k))
    (hX : IsGeometricallyNormal f) [IsNormal Y] :
    IsNormal (pullback f g : Scheme.{u})

Tag 0C3M, a lemma

Tag 0C3M in the Stacks Project.

AlgebraicGeometry.isNormal_pullback_of_isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/Normal.lean, line 399. References: EGA IV (6.14.2); EGA IV (6.14.3), “Y = Spec K”; EGA IV (4.6.4), “Case where X is normal”; EGA IV (6.7.4), “c), special case”.

Stacks Project, Tag 0C3M. A normal scheme over a field stays normal after base change along a separable extension of the ground field.

Affine-locally the base change is Spec (Γ(N, U) ⊗[k] K), and the ring-level statement IsNormalRing.tensorProduct_of_isSeparableExtension applies.

theorem isNormal_pullback_of_isSeparableExtension
    (k K : Type u) [Field k] [Field K] [Algebra k K] [Algebra.IsSeparableExtension k K]
    {N : Scheme.{u}} (p : N ⟶ Spec (.of k)) [IsNormal N] :
    IsNormal (pullback p (Spec.map (CommRingCat.ofHom (algebraMap k K))))

Tag 0FD3, a lemma

Tag 0FD3 in the Stacks Project.

AlgebraicGeometry.isIso_globalSections_tfae_geometricallyConnected_irreducible_integral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/ProperGlobalSections.lean, line 117.

For a proper geometrically normal scheme over a field, having only constant global functions, geometric connectedness, geometric irreducibility, and geometric integrality are equivalent.

theorem isIso_globalSections_tfae_geometricallyConnected_irreducible_integral
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsProper f] (hnormal : IsGeometricallyNormal f) :
    List.TFAE [
      IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop),
      GeometricallyConnected f,
      GeometricallyIrreducible f,
      GeometricallyIntegral f]

Sources

LeanAlgebraicGeometry.IsGeometricallyNormalAt · AlgebraicGeometry.IsGeometricallyNormal · AlgebraicGeometry.geometricallyNormalAt_tfae · AlgebraicGeometry.geometricallyNormal_tfae · AlgebraicGeometry.isGeometricallyNormal_iff_baseChange · AlgebraicGeometry.isGeometricallyNormalAt_iff_baseChange · AlgebraicGeometry.isGeometricallyNormal_iff_baseChange_of_isGeometricallyNormalAt · AlgebraicGeometry.isNormal_pullback_of_isGeometricallyNormal

Section33.11 Change of fields and locally Noetherian schemes #

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

Tag 038R, a lemma

Tag 038R in the Stacks Project.

AlgebraicGeometry.isLocallyNoetherian_baseChange_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/RegularNoetherian.lean, line 80. References: EGA IV (4.7.3), “(i)”; EGA IV (6.7.1), “k'/k finitely generated”.

Extending the base field by a finitely generated field extension preserves and reflects the property that a scheme is locally Noetherian.

public theorem isLocallyNoetherian_baseChange_iff
    (k k' : Type u) [Field k] [Field k'] [Algebra k k']
    [Algebra.EssFiniteType k k']
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    IsLocallyNoetherian X ↔
      IsLocallyNoetherian
        (pullback f (Spec.map (ofHom (algebraMap k k'))))

Sources

LeanAlgebraicGeometry.isLocallyNoetherian_baseChange_iff

Section33.12 Geometrically regular schemes #

Section 33.12 of the Stacks Project, Tag 038S. 7 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 038T, a definition

Tag 038T in the Stacks Project.

AlgebraicGeometry.IsGeometricallyRegularAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Regular.lean, line 67. The attribute's comment: “part (1)”. References: EGA IV (6.7.6), “geom. regular at x”; EGA IV (6.7.8).

Stacks Project, Tag 038T, part (1). A scheme X over a field k is geometrically regular at x if, after every finitely generated field extension K/k, every point above x has a regular local ring.

public abbrev IsGeometricallyRegularAt {k : Type u} [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (x : X) : Prop

AlgebraicGeometry.IsGeometricallyRegular, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Regular.lean, line 82. The attribute's comment: “part (2)”. References: EGA IV (6.7.6), “geometrically regular”.

Stacks Project, Tag 038T, part (2). A scheme over a field is geometrically regular if it is geometrically regular at every point.

public abbrev IsGeometricallyRegular {k : Type u} [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) : Prop

Tag 038U, a lemma

Tag 038U in the Stacks Project.

AlgebraicGeometry.geometricallyRegularAt_tfae, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/Regular.lean, line 275.

For a locally Noetherian scheme over a field, geometric regularity at a point is equivalent both to regularity at every point above it after every finite purely inseparable field extension, and to geometric regularity of its local ring over the ground field.

public lemma geometricallyRegularAt_tfae
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [IsLocallyNoetherian X] (x : X) :
    List.TFAE [
      IsGeometricallyRegularAt f x,
      ∀ (K : Type u) [Field K] [Algebra k K] [Module.Finite k K]
        [IsPurelyInseparable k K],
        ∀ (x' : (pullback f
            (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u})),
          pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K))) x' = x →
            IsRegularLocalRing
              ((pullback f
                (Spec.map
                  (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}).presheaf.stalk x'),
      let : Algebra k (X.presheaf.stalk x) :=
        let : Algebra k ((Spec (.of k)).presheaf.stalk (f.base x)) :=
          StructureSheaf.stalkAlgebra k (f.base x)
        ((f.stalkMap x).hom.comp
          (algebraMap k ((Spec (.of k)).presheaf.stalk (f.base x)))).toAlgebra
      Algebra.IsGeometricallyRegular k (X.presheaf.stalk x)]

Tag 038V, a lemma

Tag 038V in the Stacks Project.

AlgebraicGeometry.geometricallyRegular_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/Regular.lean, line 162.

Stacks Project, Tag 038V. The five standard characterizations of geometric regularity for a locally Noetherian scheme over a field are equivalent.

theorem geometricallyRegular_tfae
    (k : Type u) [Field k] (X : Scheme.{u}) [IsLocallyNoetherian X]
    (f : X ⟶ Spec (.of k)) :
    let geometricallyRegularSections := fun U : X.Opens ↦
      letI : Algebra k Γ(X, U) :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appLE ⊤ U (by simp)).hom.toAlgebra
      Algebra.IsGeometricallyRegular k Γ(X, U)
    List.TFAE
      [ IsGeometricallyRegular f,
        ∀ (k' : Type u) [Field k'] [Algebra k k'] [Algebra.EssFiniteType k k'],
          IsRegular
            (pullback f (Spec.map (ofHom (algebraMap k k')))),
        ∀ (k' : Type u) [Field k'] [Algebra k k'] [Module.Finite k k']
          [IsPurelyInseparable k k'],
          IsRegular
            (pullback f (Spec.map (ofHom (algebraMap k k')))),
        ∀ U : X.affineOpens, geometricallyRegularSections U.1,
        ∃ (I : Type u) (U : I → X.affineOpens),
          (⨆ i, (U i).1) = ⊤ ∧ ∀ i, geometricallyRegularSections (U i).1 ]

Tag 038W, a lemma

Tag 038W in the Stacks Project.

AlgebraicGeometry.geometricallyRegularAt_baseChange_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/RegularBaseChange.lean, line 148. The attribute's comment: “pointwise equivalence”.

Stacks Project, Tag 038W, pointwise assertion. Geometric regularity at a point is equivalent to geometric regularity at any point above it after a finitely generated extension of the ground field.

public theorem geometricallyRegularAt_baseChange_iff
    (k k' : Type u) [Field k] [Field k'] [Algebra k k']
    [Algebra.EssFiniteType k k']
    (X : Scheme.{u}) [IsLocallyNoetherian X]
    (f : X ⟶ Spec (.of k)) (x : X) :
    let g : Spec (.of k') ⟶ Spec (.of k) :=
      Spec.map (ofHom (algebraMap k k'))
    ∀ (x' : (pullback f g : Scheme.{u})),
      pullback.fst f g x' = x →
        (IsGeometricallyRegularAt f x ↔
          IsGeometricallyRegularAt (pullback.snd f g) x')

AlgebraicGeometry.geometricallyRegular_baseChange_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/RegularBaseChange.lean, line 166. The attribute's comment: “global equivalence”.

Stacks Project, Tag 038W, global assertion. Geometric regularity is invariant under finitely generated extension of the ground field.

public theorem geometricallyRegular_baseChange_iff
    (k k' : Type u) [Field k] [Field k'] [Algebra k k']
    [Algebra.EssFiniteType k k']
    (X : Scheme.{u}) [IsLocallyNoetherian X]
    (f : X ⟶ Spec (.of k)) :
    let g : Spec (.of k') ⟶ Spec (.of k) :=
      Spec.map (ofHom (algebraMap k k'))
    IsGeometricallyRegular f ↔
      IsGeometricallyRegular (pullback.snd f g)

AlgebraicGeometry.isGeometricallyRegularAt_baseChange_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/RegularUpstairs.lean, line 233. The attribute's comment: “the equivalence of (1) and (2), for any scheme over k”. References: EGA IV (6.7.8), “clause (iv)”.

Stacks Project, Tag 038W, the equivalence. Let k be a field, X a scheme over k, k'/k a finitely generated field extension, x ∈ X, and x' ∈ X_{k'} a point lying over x. Then X is geometrically regular at x over k if and only if X_{k'} is geometrically regular at x' over k'.

public theorem isGeometricallyRegularAt_baseChange_iff
    (k k' : Type u) [Field k] [Field k'] [Algebra k k'] [Algebra.EssFiniteType k k']
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) (x : X)
    (x' : (pullback f (Spec.map (ofHom (algebraMap k k'))) : Scheme.{u}))
    (hx' : pullback.fst f (Spec.map (ofHom (algebraMap k k'))) x' = x) :
    IsGeometricallyRegularAt f x ↔
      IsGeometricallyRegularAt (pullback.snd f (Spec.map (ofHom (algebraMap k k')))) x'

AlgebraicGeometry.isGeometricallyRegular_baseChange_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/RegularUpstairs.lean, line 249. The attribute's comment: “in particular: X geometrically regular over k iff X_{k'} is over k'”. References: EGA IV (7.3.10), “special case”; EGA IV (7.3.8), “partial”.

Stacks Project, Tag 038W, the consequence for schemes. Let k be a field, X a scheme over k and k'/k a finitely generated field extension. Then X is geometrically regular over k if and only if X_{k'} is geometrically regular over k'.

public theorem isGeometricallyRegular_baseChange_iff
    (k k' : Type u) [Field k] [Field k'] [Algebra k k'] [Algebra.EssFiniteType k k']
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    IsGeometricallyRegular f ↔
      IsGeometricallyRegular (pullback.snd f (Spec.map (ofHom (algebraMap k k'))))

Tag 05AW, a lemma

Tag 05AW in the Stacks Project.

AlgebraicGeometry.isGeometricallyRegularAt_of_flatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/RegularDescent.lean, line 40. The attribute's comment: “pointwise statement”.

Stacks Project, Tag 05AW (pointwise statement). Geometric regularity at a point descends along a morphism which is flat at that point.

public theorem isGeometricallyRegularAt_of_flatAt {k : Type u} [Field k]
    {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Spec (.of k))
    [IsLocallyNoetherian X] [IsLocallyNoetherian Y] (x : X)
    (hX : IsGeometricallyRegularAt (f ≫ g) x)
    (hf : AlgebraicGeometry.IsFlatAt f.toLRSHom.toShHom x) :
    IsGeometricallyRegularAt g (f x)

AlgebraicGeometry.isGeometricallyRegular_of_flat_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/RegularDescent.lean, line 75. The attribute's comment: “global statement”.

Stacks Project, Tag 05AW (global statement). A flat surjective image of a geometrically regular scheme over a field is geometrically regular.

public theorem isGeometricallyRegular_of_flat_surjective {k : Type u} [Field k]
    {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Spec (.of k))
    [IsLocallyNoetherian X] [IsLocallyNoetherian Y] [Flat f] [Surjective f]
    (hX : IsGeometricallyRegular (f ≫ g)) :
    IsGeometricallyRegular g

Tag 038X, a lemma

Tag 038X in the Stacks Project.

AlgebraicGeometry.isGeometricallyRegularAt_iff_smoothAt, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/RegularSmooth.lean, line 140. References: EGA IV (17.5.2), “base a field, pointwise”; EGA IV (17.5.5), “base = Spec k”; EGA IV (17.15.2), “more general”; SGA 1 II (5.4), “more general”.

Stacks Project, Tag 038X. For a scheme locally of finite type over a field, geometric regularity at a point is equivalent to smoothness of the structure morphism at that point.

public lemma isGeometricallyRegularAt_iff_smoothAt
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (x : X) :
    IsGeometricallyRegularAt f x ↔ InfinitesimalLifting.SmoothAt f x

Tag 038Y, an example

Tag 038Y in the Stacks Project.

AlgebraicGeometry.curve_isVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/CuspidalCurve.lean, line 322. The attribute's comment: “geometrically_reduced_not_geometrically_normal”. References: EGA IV (6.7.5), “(i) X integral curve”.

Stacks Project, Tag 038Y. The curve is a variety over 𝔽ₚ(t).

theorem curve_isVariety (hp : 2 < p) :
    IsVariety (RatFunc (ZMod p)) (curveToBase p)

AlgebraicGeometry.curve_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/CuspidalCurve.lean, line 336. The attribute's comment: “geometrically_reduced_not_geometrically_normal”. References: EGA IV (6.7.5), “(i) X regular”.

Stacks Project, Tag 038Y. The curve is regular.

theorem curve_isRegular (_hp : 2 < p) :
    IsRegular (curve p)

AlgebraicGeometry.curve_geometricallyReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/CuspidalCurve.lean, line 348. The attribute's comment: “geometrically_reduced_not_geometrically_normal”. References: EGA IV (6.7.5), “(i) X geom. integral”.

Stacks Project, Tag 038Y. The curve is geometrically reduced.

theorem curve_geometricallyReduced (hp : 2 < p) :
    GeometricallyReduced (curveToBase p)

AlgebraicGeometry.curve_not_isGeometricallyNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/CuspidalCurve.lean, line 448. The attribute's comment: “geometrically_reduced_not_geometrically_normal”.

Stacks Project, Tag 038Y. The curve is not geometrically normal.

theorem curve_not_isGeometricallyNormal (hp : 2 < p) :
    ¬ IsGeometricallyNormal (curveToBase p)

AlgebraicGeometry.hypersurface_isVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/InseparableHypersurface.lean, line 114. The attribute's comment: “regular_not_geometrically_reduced”.

Stacks Project, Tag 038Y. The hypersurface is a variety over 𝔽ₚ(t).

theorem hypersurface_isVariety :
    IsVariety (RatFunc (ZMod p)) (hypersurfaceToBase p)

AlgebraicGeometry.hypersurface_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/InseparableHypersurface.lean, line 127. The attribute's comment: “regular_not_geometrically_reduced”.

Stacks Project, Tag 038Y. The hypersurface is regular.

theorem hypersurface_isRegular :
    IsRegular (hypersurface p)

AlgebraicGeometry.hypersurface_not_geometricallyReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/InseparableHypersurface.lean, line 141. The attribute's comment: “regular_not_geometrically_reduced”.

Stacks Project, Tag 038Y. The hypersurface is not geometrically reduced.

theorem hypersurface_not_geometricallyReduced :
    ¬ GeometricallyReduced (hypersurfaceToBase p)

Sources

LeanAlgebraicGeometry.IsGeometricallyRegularAt · AlgebraicGeometry.IsGeometricallyRegular · AlgebraicGeometry.geometricallyRegularAt_tfae · AlgebraicGeometry.geometricallyRegular_tfae · AlgebraicGeometry.geometricallyRegularAt_baseChange_iff · AlgebraicGeometry.geometricallyRegular_baseChange_iff · AlgebraicGeometry.isGeometricallyRegularAt_baseChange_iff · AlgebraicGeometry.isGeometricallyRegular_baseChange_iff

Section33.13 Change of fields and the Cohen-Macaulay property #

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

Tag 045P, a lemma

Tag 045P in the Stacks Project.

AlgebraicGeometry.isCohenMacaulayLocalRing_stalk_iff_of_finiteType_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/CohenMacaulayFieldChange/FieldExtension.lean, line 374. The attribute's comment: “finitely generated field extension”. References: EGA IV (6.7.8), “(ii)”; EGA IV (6.7.1), “F = O_X, CM clause”; EGA IV (6.7.2), “special case”; SGA 3 VIA (1.1.1), “more general”.

Stacks Project, Tag 045P. Cohen-Macaulayness of local rings is unchanged after a finitely generated extension of the ground field of a locally Noetherian scheme.

The extension may be transcendental: K = k(x₁, …, xₙ) is finitely generated as a field extension, which is Algebra.EssFiniteType k K by IntermediateField.fg_top_iff, and not finitely generated as a k-algebra. The base change is again locally Noetherian, by Tag 038R; that is what makes the local ring on the right a Noetherian local ring.

public theorem isCohenMacaulayLocalRing_stalk_iff_of_finiteType_fieldExtension
    (k K : Type u) [Field k] [Field K] [Algebra k K] [Algebra.EssFiniteType k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [IsLocallyNoetherian X] (x : X)
    (x' : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme))
    (hx' : (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base x' = x) :
    letI : IsLocallyNoetherian
        (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme) :=
      (isLocallyNoetherian_baseChange_iff k K X f).mp inferInstance
    IsCohenMacaulayLocalRing (X.presheaf.stalk x) ↔
      IsCohenMacaulayLocalRing
        ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).presheaf.stalk x')

AlgebraicGeometry.isCohenMacaulayLocalRing_stalk_iff_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/CohenMacaulayFieldChange/FieldExtension.lean, line 398. The attribute's comment: “arbitrary field extension for a locally finite type scheme”. References: EGA IV (6.7.8), “(ii)”; EGA IV (6.7.1), “F = O_X, CM clause”.

Stacks Project, Tag 045P. Cohen-Macaulayness of local rings is unchanged after an arbitrary extension of the ground field when the scheme is locally of finite type over that field.

public theorem isCohenMacaulayLocalRing_stalk_iff_of_locallyOfFiniteType
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] (x : X)
    (x' : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme))
    (hx' : (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base x' = x) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    IsCohenMacaulayLocalRing (X.presheaf.stalk x) ↔
      IsCohenMacaulayLocalRing
        ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).presheaf.stalk x')

Sources

LeanAlgebraicGeometry.isCohenMacaulayLocalRing_stalk_iff_of_finiteType_fieldExtension · AlgebraicGeometry.isCohenMacaulayLocalRing_stalk_iff_of_locallyOfFiniteType

Section33.14 Change of fields and the Jacobson property #

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

Tag 0478, a lemma

Tag 0478 in the Stacks Project.

AlgebraicGeometry.isAlgebraic_residueField_and_jacobsonSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/JacobsonClosedPoints.lean, line 77. References: SGA 4 VIII (3.13), “partial”.

Let X be a scheme locally of finite type over a field k. Then (1) for every closed point x of X the extension κ(x)/k is algebraic, and (2) X is a Jacobson scheme, that is, its underlying space is a Jacobson space.

public theorem isAlgebraic_residueField_and_jacobsonSpace (p : X ⟶ Spec (.of k))
    [LocallyOfFiniteType p] :
    (∀ x : X, IsClosed ({x} : Set X) →
        letI : Algebra k (X.residueField x) :=
          ((Scheme.ΓSpecIso (.of k)).inv ≫ p.appTop ≫ X.Γevaluation x).hom.toAlgebra
        Algebra.IsAlgebraic k (X.residueField x)) ∧ JacobsonSpace X

Tag 0479, a lemma

Tag 0479 in the Stacks Project.

AlgebraicGeometry.jacobsonSpace_pullback_of_large_cardinality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Jacobson.lean, line 270. The attribute's comment: “base_change_jacobson”.

The base change of a scheme to every sufficiently large extension of its ground field is a Jacobson scheme.

theorem jacobsonSpace_pullback_of_large_cardinality
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    ∃ κ : Cardinal.{u}, ∀ (K : Type u) [Field K] [Algebra k K],
      κ ≤ Cardinal.mk K →
        JacobsonSpace ↑(pullback f (Spec.map (ofHom (algebraMap k K))))

Stacks.AlgebraicGeometry.ClosedPointResidue.exists_cardinal_isAlgebraic_residueField_of_mem_closedPoints_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Varieties/ClosedPointResidue.lean, line 330. The attribute's comment: “closed_point_residue_algebraic”.

For every scheme over a field, after extending the field to one of sufficiently large cardinality, the residue field of every closed point of the base change is algebraic over the extended field.

theorem exists_cardinal_isAlgebraic_residueField_of_mem_closedPoints_baseChange
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    ∃ κ : Cardinal.{u}, ∀ (K : Type u) [Field K] [Algebra k K], κ ≤ Cardinal.mk K →
      ∀ x : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}),
        x ∈ closedPoints
            (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}) →
          let p := pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k K)))
          letI : (p x).asIdeal.IsPrime := (p x).isPrime
          letI := ((CommRingCat.ofHom (algebraMap K (p x).asIdeal.ResidueField)) ≫
            (Scheme.Spec.residueFieldIso (.of K) (p x)).inv ≫
            p.residueFieldMap x).hom.toAlgebra
          Algebra.IsAlgebraic K
            ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) :
              Scheme.{u}).residueField x)

Sources

LeanAlgebraicGeometry.isAlgebraic_residueField_and_jacobsonSpace · AlgebraicGeometry.jacobsonSpace_pullback_of_large_cardinality · Stacks.AlgebraicGeometry.ClosedPointResidue.exists_cardinal_isAlgebraic_residueField_of_mem_closedPoints_baseChange

Section33.15 Change of fields and ample invertible sheaves #

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

Tag 0BDC, a lemma

Tag 0BDC in the Stacks Project.

AlgebraicGeometry.exists_isAmple_of_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FieldExtensionDescent/Unconditional.lean, line 91.

Let k be a field and X a scheme over k. If there exists an ample invertible sheaf on X_K for some field extension K/k, then X has an ample invertible sheaf.

public theorem exists_isAmple_of_fieldExtension
    (h : ∃ L : (pullback (Spec.map (CommRingCat.ofHom (algebraMap k K))) f).Modules,
        ∃ _ : AlgebraicGeometry.SheafOfModules.IsInvertible
          (pullback (Spec.map (CommRingCat.ofHom (algebraMap k K))) f).toRingedSpace.presheaf
          (structureSheafRing
            (pullback (Spec.map (CommRingCat.ofHom (algebraMap k K))) f).toRingedSpace).property L,
          Scheme.Modules.IsAmple
            (pullback (Spec.map (CommRingCat.ofHom (algebraMap k K))) f) L) :
    ∃ M : X.Modules, ∃ _ : AlgebraicGeometry.SheafOfModules.IsInvertible
        X.toRingedSpace.presheaf (structureSheafRing X.toRingedSpace).property M,
      Scheme.Modules.IsAmple X M

Tag 0BDD, a lemma

Tag 0BDD in the Stacks Project.

AlgebraicGeometry.isQuasiAffine_of_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FieldExtensionDescent/QuasiAffine.lean, line 123.

Let k be a field and X a scheme over k. If X_K is quasi-affine for some field extension K/k, then X is quasi-affine.

public theorem isQuasiAffine_of_fieldExtension
    (h : Scheme.IsQuasiAffine
      (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))))) :
    Scheme.IsQuasiAffine X

AlgebraicGeometry.isQuasiAffine_of_isQuasiAffine_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/QuasiAffine.lean, line 49.

Stacks Project, Tag 0BDD. Quasi-affineness descends along an extension of the base field: if the base change of X to K is quasi-affine, then so is X.

theorem isQuasiAffine_of_isQuasiAffine_baseChange
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    (h : Scheme.IsQuasiAffine
      (pullback f (Spec.map (ofHom (algebraMap k K))))) :
    Scheme.IsQuasiAffine X

Tag 0BDE, a lemma

Tag 0BDE in the Stacks Project.

AlgebraicGeometry.isQuasiProjective_of_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FieldExtensionDescent/Unconditional.lean, line 114. References: EGA IV (9.1.5), “quasi-projective case”; EGA II (6.6.5), “quasi-proj. descent”.

Let k be a field and X a scheme over k. If X_K is quasi-projective over K for some field extension K/k, then X is quasi-projective over k.

public theorem isQuasiProjective_of_fieldExtension
    (h : IsQuasiProjective (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k K))))) :
    IsQuasiProjective f

Tag 0BDF, a lemma

Tag 0BDF in the Stacks Project.

AlgebraicGeometry.isProper_of_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FieldExtensionDescent/Proper.lean, line 96.

[Stacks Project, Tag 0BDF]. Let k be a field and X a scheme over k. If X_K is proper over K for some field extension K/k, then X is proper over k.

The field extension is faithfully flat, so Spec(K) → Spec(k) is a surjective flat quasi-compact morphism and the statement is the descent of properness along one; that descent is [Stacks Project, Tag 02L1], of which the source says this lemma is a special case.

public theorem isProper_of_fieldExtension
    (h : IsProper (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k K))))) :
    IsProper f

Tag 0BDG, a lemma

Tag 0BDG in the Stacks Project.

AlgebraicGeometry.isProjective_of_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FieldExtensionDescent/Projective.lean, line 161.

[Stacks Project, Tag 0BDG]. Let k be a field and X a scheme over k. If X_K is projective over K for some field extension K/k, then X is projective over k.

This is the source proof verbatim: projectivity over a field is quasi-projectivity together with properness, and each of those descends along an arbitrary field extension by [Stacks Project, Tag 0BDE] and [Stacks Project, Tag 0BDF]. The identification of projectivity with the conjunction is clause (1) of [Stacks Project, Tag 0BCL], applied at the two affine bases Spec K and Spec k, where it is AlgebraicGeometry.isProjective_iff_isQuasiProjective_and_isProper_of_isAffine.

public theorem isProjective_of_fieldExtension
    (h : IsProjective (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k K))))) :
    IsProjective f

Sources

LeanAlgebraicGeometry.exists_isAmple_of_fieldExtension · AlgebraicGeometry.isQuasiAffine_of_fieldExtension · AlgebraicGeometry.isQuasiAffine_of_isQuasiAffine_baseChange · AlgebraicGeometry.isQuasiProjective_of_fieldExtension · AlgebraicGeometry.isProper_of_fieldExtension · AlgebraicGeometry.isProjective_of_fieldExtension

Section33.16 Tangent spaces #

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

Tag 0B29, a definition

Tag 0B29 in the Stacks Project.

Declarations registered for the tag:

DualNumber registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch33.lean, line 41 (StacksFrontier): “the dual numbers R[ε]; as an R-module R × R, free on 1 and ε”. References: EGA 0 (22.1.3); EGA 0 (22.1.3.2); SGA 3 II (2.1), “special case”; SGA 3 II (3.14), “partial”; SGA 3 II (4.5.1); SGA 3 II (4.7.1), “special case”; SGA 3 III (4.38); SGA 3 VIIA (1.2.0), “partial”; SGA 3 VIIB (2.6); SGA 3 XI (1.9), “partial”; SGA 4½ Fonctions L (4.5); SGA 7 VI (1.2); SGA 7 VI (1.15), “special case”; SGA 7 VI (1.3(c)), “dual numbers k[ε] = k[k]”.
DualNumber.eps registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch33.lean, line 43 (StacksFrontier): “the element ε”. References: SGA 3 II (4.5.1); SGA 3 II (4.7.1), “partial”.
DualNumber.eps_mul_eps registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch33.lean, line 44 (StacksFrontier): “ε² = 0”. References: SGA 3 II (4.7.1), “partial”; SGA 7 VI (1.15), “relation ε² = 0”.

Tag 0B2A, an equation

Tag 0B2A in the Stacks Project.

AlgebraicGeometry.DottedTangentArrow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/Defs.lean, line 90. The attribute's comment: “the dotted arrows”.

A dotted arrow in the tangent-space diagram: a morphism from the spectrum of the dual numbers which restricts to the point x and is a morphism over S. Carrying the canonical κ(x)-vector space structure below, this is the tangent space T_{X/S, x} of X over S at x, and its elements are the tangent vectors of X/S at x.

def DottedTangentArrow {X S : Scheme.{u}} (f : X ⟶ S) (x : X)

Tag 0B2B, a lemma

Tag 0B2B in the Stacks Project.

AlgebraicGeometry.dottedTangentArrowModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/Defs.lean, line 537.

The dotted arrows in the tangent-space diagram carry a canonical vector space structure over the residue field κ(x). Its operations are characterized by the square-zero pushout and by scaling the infinitesimal generator.

noncomputable def dottedTangentArrowModule {X S : Scheme.{u}} (f : X ⟶ S) (x : X) :
    TangentSpaceStructure f x

Tag 0B2C, a definition

Tag 0B2C in the Stacks Project.

AlgebraicGeometry.DottedTangentArrow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/Defs.lean, line 90. The attribute's comment: “the tangent space as a set”.

A dotted arrow in the tangent-space diagram: a morphism from the spectrum of the dual numbers which restricts to the point x and is a morphism over S. Carrying the canonical κ(x)-vector space structure below, this is the tangent space T_{X/S, x} of X over S at x, and its elements are the tangent vectors of X/S at x.

def DottedTangentArrow {X S : Scheme.{u}} (f : X ⟶ S) (x : X)

AlgebraicGeometry.dottedTangentArrowAddCommGroup, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/Defs.lean, line 610. The attribute's comment: “the additive group of tangent vectors”.

The canonical additive commutative group structure on dotted tangent arrows, i.e. the addition of tangent vectors of X/S at x.

noncomputable instance dottedTangentArrowAddCommGroup {X S : Scheme.{u}}
    (f : X ⟶ S) (x : X) : AddCommGroup (DottedTangentArrow f x)

AlgebraicGeometry.dottedTangentArrowModuleInstance, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/Defs.lean, line 617. The attribute's comment: “the canonical κ(x)-vector space structure on the tangent space”.

The canonical κ(x)-vector space structure on dotted tangent arrows; with it the dotted arrows are the tangent space T_{X/S, x}.

noncomputable instance dottedTangentArrowModuleInstance {X S : Scheme.{u}}
    (f : X ⟶ S) (x : X) : Module (X.residueField x) (DottedTangentArrow f x)

Tag 0BEA, an equation

Tag 0BEA in the Stacks Project.

AlgebraicGeometry.tangentSpaceEquivFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/TangentFibre.lean, line 767.

The tangent space of X over S at x is canonically identified with the tangent space of the fibre X_{f(x)} at its corresponding point.

noncomputable def tangentSpaceEquivFiber : TangentSpaceFiberEquiv f x

Tag 0B2D, a lemma

Tag 0B2D in the Stacks Project.

AlgebraicGeometry.tangentSpaceEquivCotangentSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/Cotangent.lean, line 279. References: EGA IV (16.5.13), “(16.5.13.1)”.

Stacks Project, Tag 0B2D. The relative tangent space at a point is canonically the 𝒪_{X,x}-linear dual of the stalk of relative differentials, as a vector space over the residue field: T_{X/S,x} = Hom_{𝒪_{X,x}}(Ω_{X/S,x}, κ(x)).

noncomputable def tangentSpaceEquivCotangentSpace :
    DottedTangentArrow f x ≃ₗ[X.residueField x] CotangentSpace f x

AlgebraicGeometry.tangentSpaceEquivCotangentSpace_apply_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/Cotangent.lean, line 298. The attribute's comment: “characterization”.

Stacks Project, Tag 0B2D. The canonical equivalence sends a dual-number arrow to the functional which, on the germ d a of a universal relative differential, returns the coefficient of ε in the pullback of a along the arrow. This is what makes it canonical.

theorem tangentSpaceEquivCotangentSpace_apply_germ (θ : DottedTangentArrow f x)
    (U : X.Opens) (hx : x ∈ U) (hU : ⊤ ≤ θ.val ⁻¹ᵁ U) (a : X.presheaf.obj (op U)) :
    tangentSpaceEquivCotangentSpace f x θ
        (TopCat.Presheaf.germ (C := AddCommGrpCat.{u})
          (Scheme.Hom.relativeDifferentials f).val.presheaf U x hx
          ((Scheme.Hom.universalRelativeDerivation f).d a)) =
      pullbackInfinitesimalCoefficient θ U hU a

Tag 0B2E, a lemma

Tag 0B2E in the Stacks Project.

AlgebraicGeometry.relativeCotangentSpaceEquivDifferentialFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/MaximalIdealCotangent.lean, line 128. The attribute's comment: “cotangent space”. References: EGA IV (16.5.13), “partial”.

Let f : X ⟶ S be a morphism of schemes and let x be a point of X whose residue field extension κ(f x) → κ(x) is separable. The relative cotangent space 𝔪_x / (𝔪_x² + 𝔪_{f x} 𝒪_{X,x}) of the stalk map of f is canonically the residue-field fibre κ(x) ⊗_{𝒪_{X,x}} Ω_{X/S,x} of the stalk of the sheaf of relative differentials.

noncomputable def relativeCotangentSpaceEquivDifferentialFiber
    (hsep : Algebra.IsSeparable (S.residueField (f.base x)) (X.residueField x)) :
    Deformation.relativeCotangentSpace (f.stalkMap x).hom ≃ₗ[X.residueField x]
      X.residueField x ⊗[X.presheaf.stalk x] relativeDifferentialStalk f x

AlgebraicGeometry.relativeCotangentSpaceEquivDifferentialFiber_apply_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/MaximalIdealCotangent.lean, line 155. The attribute's comment: “canonical map on differentials”.

The identification of the relative cotangent space with the residue-field fibre of the relative differentials carries the class of the germ at x of a local section of 𝒪_X vanishing at x to the germ of the universal relative differential of that section. This is what makes it canonical.

theorem relativeCotangentSpaceEquivDifferentialFiber_apply_germ
    (hsep : Algebra.IsSeparable (S.residueField (f.base x)) (X.residueField x))
    (U : X.Opens) (hx : x ∈ U) (a : X.presheaf.obj (op U))
    (ha : (X.presheaf.germ U x hx).hom a ∈
      maximalIdeal (ToType (X.presheaf.stalk x))) :
    relativeCotangentSpaceEquivDifferentialFiber f x hsep
        (Submodule.Quotient.mk ⟨(X.presheaf.germ U x hx).hom a, ha⟩) =
      (1 : X.residueField x) ⊗ₜ[X.presheaf.stalk x]
        (show relativeDifferentialStalk f x from
          TopCat.Presheaf.germ (C := AddCommGrpCat.{u})
            (Scheme.Hom.relativeDifferentials f).val.presheaf U x hx
            ((Scheme.Hom.universalRelativeDerivation f).d a))

AlgebraicGeometry.dottedTangentArrowEquivDualRelativeCotangentSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/MaximalIdealCotangent.lean, line 191. The attribute's comment: “tangent space”.

If the residue field extension κ(f x) → κ(x) is separable, the relative tangent space at x — the space of dual-number arrows into X over S extending the residue-field point x — is canonically the κ(x)-linear dual of the relative cotangent space 𝔪_x / (𝔪_x² + 𝔪_{f x} 𝒪_{X,x}).

noncomputable def dottedTangentArrowEquivDualRelativeCotangentSpace
    (hsep : Algebra.IsSeparable (S.residueField (f.base x)) (X.residueField x)) :
    DottedTangentArrow f x ≃ₗ[X.residueField x]
      (Deformation.relativeCotangentSpace (f.stalkMap x).hom →ₗ[X.residueField x]
        X.residueField x)

AlgebraicGeometry.dottedTangentArrowEquivDualRelativeCotangentSpace_apply_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/MaximalIdealCotangent.lean, line 206. The attribute's comment: “canonical map on tangent vectors”.

The identification of the relative tangent space with the dual of the relative cotangent space evaluates a dual-number arrow on the class of the germ of a local section vanishing at x by the coefficient of ε in the pullback of that section along the arrow.

theorem dottedTangentArrowEquivDualRelativeCotangentSpace_apply_germ
    (hsep : Algebra.IsSeparable (S.residueField (f.base x)) (X.residueField x))
    (θ : DottedTangentArrow f x) (U : X.Opens) (hx : x ∈ U) (hU : ⊤ ≤ θ.val ⁻¹ᵁ U)
    (a : X.presheaf.obj (op U))
    (ha : (X.presheaf.germ U x hx).hom a ∈
      maximalIdeal (ToType (X.presheaf.stalk x))) :
    dottedTangentArrowEquivDualRelativeCotangentSpace f x hsep θ
        (Submodule.Quotient.mk ⟨(X.presheaf.germ U x hx).hom a, ha⟩) =
      pullbackInfinitesimalCoefficient θ U hU a

Tag 0B2F, a lemma

Tag 0B2F in the Stacks Project.

AlgebraicGeometry.tangentMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/Functorial.lean, line 200. The attribute's comment: “canonical tangent map”. References: EGA IV (16.5.13), “(16.5.13.5)”.

The tangent map of a morphism over S, with the scalar fields identified by the canonical residue-field isomorphism.

noncomputable def tangentMap (h : f ≫ q = p) (x : X) [IsIso (f.residueFieldMap x)] :
    DottedTangentArrow p x →ₛₗ[(inv (f.residueFieldMap x)).hom]
      DottedTangentArrow q (f x)

AlgebraicGeometry.tangentMap_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/Functorial.lean, line 216. The attribute's comment: “characterization by composition of dual-number arrows”.

The tangent map is induced by composition of dual-number arrows: a tangent arrow is sent to its composite with f, pulled back along any ring homomorphism of dual numbers whose two components are the residue-field identification.

theorem tangentMap_apply (h : f ≫ q = p) (x : X) [IsIso (f.residueFieldMap x)]
    (θ : DottedTangentArrow p x)
    (α : DualNumber (X.residueField x) →+* DualNumber (Y.residueField (f x)))
    (hα₀ : ∀ z, TrivSqZeroExt.fst (α z) =
      (inv (f.residueFieldMap x)).hom (TrivSqZeroExt.fst z))
    (hα₁ : ∀ z, TrivSqZeroExt.snd (α z) =
      (inv (f.residueFieldMap x)).hom (TrivSqZeroExt.snd z)) :
    (tangentMap f p q h x θ).val =
      Spec.map (CommRingCat.ofHom α) ≫ θ.val ≫ f

AlgebraicGeometry.tangentSpaceEquivDualDifferentialFiber_tangentMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/TangentMapDual.lean, line 405. The attribute's comment: “dual to the map Ω_{Y/S,y} ⊗ κ(y) → Ω_{X/S,x} ⊗ κ(x) via the identifications of Tag 0B2D”. References: EGA IV (16.5.13), “partial, special case”.

The tangent map is dual to the map on residue-field fibres. Let f : X ⟶ Y be a morphism of schemes over S, let x be a point of X with κ(f x) = κ(x). Under the identifications T_{X/S,x} = Hom_{κ(x)}(κ(x) ⊗ Ω_{X/S,x}, κ(x)) and T_{Y/S,f x} = Hom_{κ(f x)}(κ(f x) ⊗ Ω_{Y/S,f x}, κ(f x)) of Tag 0B2D, the tangent map d f : T_{X/S,x} → T_{Y/S,f x} is the dual of the natural map κ(f x) ⊗ Ω_{Y/S,f x} → κ(x) ⊗ Ω_{X/S,x}.

theorem tangentSpaceEquivDualDifferentialFiber_tangentMap (h : f ≫ q = p) (x : X)
    [IsIso (f.residueFieldMap x)] (θ : DottedTangentArrow p x) :
    tangentSpaceEquivDualDifferentialFiber q (f.base x) (tangentMap f p q h x θ) =
      differentialFiberMapDual f p q h x (tangentSpaceEquivDualDifferentialFiber p x θ)

Tag 0BEB, a lemma

Tag 0BEB in the Stacks Project.

AlgebraicGeometry.tangentSpaceProductEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/TangentProduct.lean, line 545.

The tangent space of a fibre product at a pair of points rational over the same base point is the direct sum of the tangent spaces of the factors. The equivalence is induced by the projections.

noncomputable def tangentSpaceProductEquiv {X Y S : Scheme.{u}}
    (f : X ⟶ S) (g : Y ⟶ S) (z : ↑(pullback f g))
    [IsIso (f.residueFieldMap (pullback.fst f g z))]
    [IsIso (g.residueFieldMap (pullback.snd f g z))] :
    TangentSpaceProductEquiv f g z

AlgebraicGeometry.tangentSpaceProductFiberEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/TangentProductFibre.lean, line 404. The attribute's comment: “T_{X ×_S Y/S,(x,y)} = T_{X/S,x} ⊕ T_{Y/S,y} at the unique point (x,y): left to right by the projections, right to left by 1 × y and x × 1 on the fibres via 0BEA”. References: SGA 3 V (4.1.2), “more general”.

Stacks Project, Tag 0BEB. Let X, Y be schemes over S and let z = (x, y) be a point of X ×_S Y whose projections x ∈ X, y ∈ Y have residue fields κ(x) = κ(s) = κ(y), where s is their common image in S (every such pair x, y comes from a point z, by AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback). Then z is the only point over x and y, and T_{X ×_S Y/S, (x, y)} = T_{X/S, x} ⊕ T_{Y/S, y} canonically: from left to right by the tangent maps of the projections, from right to left by 1 × y : X_s → X_s ×_s Y_s and x × 1 : Y_s → X_s ×_s Y_s via the identification of tangent spaces with tangent spaces of fibres (Stacks, Tag 0BEA).

noncomputable def tangentSpaceProductFiberEquiv {X Y S : Scheme.{u}}
    (f : X ⟶ S) (g : Y ⟶ S) (z : ↑(pullback f g))
    [IsIso (f.residueFieldMap (pullback.fst f g z))]
    [IsIso (g.residueFieldMap (pullback.snd f g z))] :
    TangentSpaceProductFiberEquiv f g z

Tag 0B2G, a lemma

Tag 0B2G in the Stacks Project.

AlgebraicGeometry.injective_tangentMap_iff_unramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/Unramified.lean, line 212.

Stacks Project, Tag 0B2G. Let f : X ⟶ Y be a morphism of schemes over S, locally of finite type, and let x be a point of X whose residue field agrees with that of f x. Then the tangent map d f : T_{X/S, x} ⟶ T_{Y/S, f x} is injective if and only if f is unramified at x.

theorem injective_tangentMap_iff_unramifiedAt (h : f ≫ q = p) [LocallyOfFiniteType f]
    [IsIso (f.residueFieldMap x)] :
    Function.Injective (tangentMap f p q h x) ↔ UnramifiedAt f x

AlgebraicGeometry.injective_tangentMap_iff_unramifiedAt_of_locallyOfFiniteType_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/Unramified.lean, line 223. The attribute's comment: “with the source locally of finite type over the base”.

Stacks Project, Tag 0B2G under the hypotheses of the source: for X locally of finite type over S, the tangent map of a morphism f : X ⟶ Y over S is injective at a point where the residue field is unchanged if and only if f is unramified there. Local finite type of f itself is Tag 01T8.

theorem injective_tangentMap_iff_unramifiedAt_of_locallyOfFiniteType_base (h : f ≫ q = p)
    [LocallyOfFiniteType p] [IsIso (f.residueFieldMap x)] :
    Function.Injective (tangentMap f p q h x) ↔ UnramifiedAt f x

Sources

LeanDualNumber · DualNumber.eps · DualNumber.eps_mul_eps · AlgebraicGeometry.DottedTangentArrow · AlgebraicGeometry.dottedTangentArrowModule · AlgebraicGeometry.dottedTangentArrowAddCommGroup · AlgebraicGeometry.dottedTangentArrowModuleInstance · AlgebraicGeometry.tangentSpaceEquivFiber

Section33.17 Generically finite morphisms #

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

Tag 0AB6, a lemma

Tag 0AB6 in the Stacks Project.

AlgebraicGeometry.quasiFiniteAt_of_target_stalk_dimension_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/QuasiFiniteCodimensionOne.lean, line 157.

Stacks Project, Tag 0AB6. A locally finite type morphism which is generically quasi-finite is quasi-finite above a point with Noetherian local ring of dimension at most one. It suffices to impose the generic condition only on components whose generic points specialize to the chosen point, or alternatively to assume quasi-finiteness at every generic point or on a dense set over a locally Noetherian target.

theorem quasiFiniteAt_of_target_stalk_dimension_le_one
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] (y : Y)
    (hyNoetherian : IsNoetherianRing (Y.presheaf.stalk y))
    (hyDimension : ringKrullDim (Y.presheaf.stalk y) ≤ 1)
    (hgeneric :
      (∀ η : X, η ∈ genericPoints X →
        letI := (f.residueFieldMap η).hom.toAlgebra
        Algebra.IsAlgebraic (Y.residueField (f η)) (X.residueField η)) ∨
      (∀ η : X, η ∈ genericPoints X → Specializes (f η) y →
        letI := (f.residueFieldMap η).hom.toAlgebra
        Algebra.IsAlgebraic (Y.residueField (f η)) (X.residueField η)) ∨
      (∀ η : X, η ∈ genericPoints X → quasiFiniteAt f η) ∨
      (IsLocallyNoetherian Y ∧ Dense {x : X | quasiFiniteAt f x})) :
    ∀ x : X, f x = y → quasiFiniteAt f x

Tag 0AB7, a lemma

Tag 0AB7 in the Stacks Project.

AlgebraicGeometry.exists_isFinite_morphismRestrict_of_ringKrullDim_stalk_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/QuasiFiniteCodimensionOne.lean, line 190.

Stacks Project, Tag 0AB7. A proper morphism which is generically quasi-finite is finite over a neighbourhood of a point whose local ring is Noetherian of dimension at most one.

theorem exists_isFinite_morphismRestrict_of_ringKrullDim_stalk_le_one
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f] (y : Y)
    [IsNoetherianRing (Y.presheaf.stalk y)] (hy : ringKrullDim (Y.presheaf.stalk y) ≤ 1)
    (h : (∀ (η : X), η ∈ genericPoints X → letI := (f.residueFieldMap η).hom.toAlgebra
        Algebra.IsAlgebraic (Y.residueField (f η)) (X.residueField η)) ∨
      ((∀ (η : X), η ∈ genericPoints X → Specializes (f η) y →
          letI := (f.residueFieldMap η).hom.toAlgebra
          Algebra.IsAlgebraic (Y.residueField (f η)) (X.residueField η)) ∨
        ((∀ (η : X), η ∈ genericPoints X → quasiFiniteAt f η) ∨
          (IsLocallyNoetherian Y ∧ Dense {x : X | quasiFiniteAt f x})))) :
    ∃ V : Y.Opens, y ∈ V ∧ IsFinite (f ∣_ V)

Tag 0BFP, a lemma

Tag 0BFP in the Stacks Project.

AlgebraicGeometry.exists_isIso_restrict_of_finite_fiber_of_normal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/BirationalIsomorphismLocus.lean, line 369. The attribute's comment: “finite_fibre_normal”. References: EGA III (4.4.9), “proper case”.

Stacks Project, Tag 0BFP (finite fibre, normal local ring). Let f : Y ⟶ X be a proper birational morphism, where X is Noetherian and Y is reduced. The morphism is an isomorphism over a neighbourhood of every point whose fibre is finite and whose local ring is a normal domain.

public theorem exists_isIso_restrict_of_finite_fiber_of_normal
    {X Y : Scheme.{u}} [IsNoetherian X] (f : Y ⟶ X) [IsProper f] [IsReduced Y]
    (hf : IsBirational f) (x : X) (hfinite : (f ⁻¹' {x}).Finite)
    [IsDomain (X.presheaf.stalk x)] [IsIntegrallyClosed (X.presheaf.stalk x)] :
    ∃ U : X.Opens, x ∈ U ∧ IsIso (f ∣_ U)

AlgebraicGeometry.mem_maximal_isomorphism_open_of_quasiFiniteAt_of_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/BirationalIsomorphismLocus.lean, line 729. The attribute's comment: “quasi_finite_point_normal”. References: EGA III (4.4.9), “proper case”.

Stacks Project, Tag 0BFP (quasi-finite point over a normal point). The maximal open over which a proper birational morphism with reduced source is an isomorphism contains every normal point admitting a preimage at which the morphism is quasi-finite.

public theorem mem_maximal_isomorphism_open_of_quasiFiniteAt_of_isNormal
    {X Y : Scheme.{u}} [IsNoetherian X] (f : Y ⟶ X) [IsProper f] [IsReduced Y]
    (hf : IsBirational f) (U : X.Opens)
    (hU : IsGreatest { V : X.Opens | IsIso (f ∣_ V) } U) (x : X)
    (hnormal : IsNormalRing (X.presheaf.stalk x)) (y : Y) (hy : f y = x)
    (hqf : quasiFiniteAt f y) :
    x ∈ U

AlgebraicGeometry.mem_maximal_isomorphism_open_of_mem_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/BirationalIsomorphismLocusCodimensionZero.lean, line 127. The attribute's comment: “item (1): a point of codimension zero, a generic point of a component”.

Stacks Project, Tag 0BFP (codimension zero). Let f : Y ⟶ X be a proper birational morphism, where X is Noetherian and Y is reduced. The maximal open over which f is an isomorphism contains every point of codimension zero on X, that is, every generic point of an irreducible component of X.

public theorem mem_maximal_isomorphism_open_of_mem_genericPoints
    {X Y : Scheme.{u}} [IsNoetherian X] (f : Y ⟶ X) [IsProper f] [IsReduced Y]
    (hf : IsBirational f) (U : X.Opens)
    (hU : IsGreatest { V : X.Opens | IsIso (f ∣_ V) } U) (x : X)
    (hx : x ∈ genericPoints X) :
    x ∈ U

AlgebraicGeometry.mem_maximal_isomorphism_open_of_isDiscreteValuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/BirationalIsomorphismLocusDVR.lean, line 101. The attribute's comment: “item (2): a codimension-one point whose local ring is a discrete valuation ring”.

Let f : Y ⟶ X be a proper birational morphism, where X is Noetherian and Y is reduced. The maximal open over which f is an isomorphism contains every point whose local ring is a discrete valuation ring. Such a point has codimension one on X, the dimension of a discrete valuation ring being one.

public theorem mem_maximal_isomorphism_open_of_isDiscreteValuationRing
    {X Y : Scheme.{u}} [IsNoetherian X] (f : Y ⟶ X) [IsProper f] [IsReduced Y]
    (hf : IsBirational f) (U : X.Opens)
    (hU : IsGreatest { V : X.Opens | IsIso (f ∣_ V) } U) (x : X)
    [IsDomain (X.presheaf.stalk x)]
    [IsDiscreteValuationRing (X.presheaf.stalk x)] :
    x ∈ U

Sources

LeanAlgebraicGeometry.quasiFiniteAt_of_target_stalk_dimension_le_one · AlgebraicGeometry.exists_isFinite_morphismRestrict_of_ringKrullDim_stalk_le_one · AlgebraicGeometry.exists_isIso_restrict_of_finite_fiber_of_normal · AlgebraicGeometry.mem_maximal_isomorphism_open_of_quasiFiniteAt_of_isNormal · AlgebraicGeometry.mem_maximal_isomorphism_open_of_mem_genericPoints · AlgebraicGeometry.mem_maximal_isomorphism_open_of_isDiscreteValuationRing

Section33.18 Variants of Noether normalization #

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

Tag 0CBH, a lemma

Tag 0CBH in the Stacks Project.

AlgebraicGeometry.exists_affineOpen_quasiFinite_affineSpace_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/NoetherNormalization.lean, line 155. References: EGA IV (13.3.1.1), “quasi-finite factoriz.”.

Relative Noether normalization on an affine neighbourhood of a point.

theorem exists_affineOpen_quasiFinite_affineSpace_factorization
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (x : X) (V : S.affineOpens) (hxV : f x ∈ V.1) (d : ℕ)
    (hd : topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = (d : WithBot ℕ∞)) :
    ∃ (U : X.affineOpens) (_hxU : x ∈ U.1)
      (_hUV : U.1 ≤ f ⁻¹ᵁ V.1)
      (π : U.1.toScheme ⟶ AffineSpace (ULift.{u} (Fin d)) V.1.toScheme),
      (π ≫ (AffineSpace.over (ULift.{u} (Fin d)) V.1.toScheme).hom ≫ V.1.ι =
        U.1.ι ≫ f) ∧
      ((LocallyOfFiniteType π ∧ QuasiCompact π) ∧ LocallyQuasiFinite π)

Tag 0CBI, a lemma

Tag 0CBI in the Stacks Project.

AlgebraicGeometry.exists_factorization_finite_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/NoetherNormalization.lean, line 407.

Noether normalization for a finite-type map of affine schemes at a chosen fibre.

theorem exists_factorization_finite_fiber {X S : Scheme.{u}} (f : X ⟶ S)
    [IsAffine X] [IsAffine S] [LocallyOfFiniteType f] [QuasiCompact f]
    (s : S) (d : ℕ) (hd : topologicalKrullDim (f.fiber s) = d) :
    ∃ π : X ⟶ 𝔸(ULift (Fin d); S),
      (π ≫ 𝔸(ULift (Fin d); S) ↘ S = f) ∧
      ∃ πs : f.fiber s ⟶ (𝔸(ULift (Fin d); S) ↘ S).fiber s,
        (πs ≫ (𝔸(ULift (Fin d); S) ↘ S).fiberι s = f.fiberι s ≫ π) ∧
        (πs ≫ (𝔸(ULift (Fin d); S) ↘ S).fiberToSpecResidueField s =
          f.fiberToSpecResidueField s) ∧
        IsFinite πs

Tag 0CBJ, a lemma

Tag 0CBJ in the Stacks Project.

AlgebraicGeometry.exists_isImmersion_specMap_derivativePair_of_unramifiedAt, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Unramified/LocalStructure.lean, line 346. The attribute's comment: “unramified case; the étale case is AlgebraicGeometry.exists_isOpenImmersion_specMap_derivativePair_of_etaleAt”.

Stacks Project, Tag 0CBJ, unramified case. A morphism of schemes unramified at x factors, on an affine open neighbourhood of x lying over a prescribed affine open V of the target, as an immersion into the spectrum of the derivative-localized monic hypersurface Γ(S, V)[t]_{g'}/(g), followed by the canonical map to the affine line over V.

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

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

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

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

Tag 0CBK, a lemma

Tag 0CBK in the Stacks Project.

AlgebraicGeometry.finiteDimensional_relativeCotangentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/NoetherNormalization.lean, line 762. The attribute's comment: “finiteness of r”.

Stacks Project, Tag 0CBK, finiteness of r. For a morphism locally of finite type the residue-field fibre at x of the stalk of the sheaf of relative differentials is a finite-dimensional κ(x)-vector space, so the integer r of the tag is defined.

theorem finiteDimensional_relativeCotangentSpace {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (x : X) :
    FiniteDimensional (X.residueField x) (relativeCotangentSpace f x)

AlgebraicGeometry.finrank_relativeCotangentSpace_eq_fiberRelativeCotangentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/NoetherNormalization.lean, line 774. The attribute's comment: “first equality”.

Stacks Project, Tag 0CBK, first equality defining r. The residue-field fibre of the stalk of Ω_{X/S} at x and the corresponding fibre computed on the scheme-theoretic fibre through x have the same dimension over κ(x): dim_{κ(x)} Ω_{X/S,x} ⊗ κ(x) = dim_{κ(x)} Ω_{X_s/s,x} ⊗ κ(x).

theorem finrank_relativeCotangentSpace_eq_fiberRelativeCotangentSpace
    {X S : Scheme.{u}} (f : X ⟶ S) (x : X) :
    Module.finrank (X.residueField x) (relativeCotangentSpace f x) =
      Module.finrank (X.residueField x) (fiberRelativeCotangentSpace f x)

AlgebraicGeometry.finrank_relativeCotangentSpace_eq_finrank_dottedTangentArrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/NoetherNormalization.lean, line 786. The attribute's comment: “second equality”.

Stacks Project, Tag 0CBK, second equality defining r. The residue-field fibre of the stalk of Ω_{X/S} at x and the relative tangent space at x have the same dimension over κ(x): dim_{κ(x)} Ω_{X/S,x} ⊗ κ(x) = dim_{κ(x)} T_{X/S,x}. The tangent space is the 𝒪_{X,x}-linear dual of the stalk, which is the κ(x)-linear dual of the fibre.

theorem finrank_relativeCotangentSpace_eq_finrank_dottedTangentArrow
    {X S : Scheme.{u}} (f : X ⟶ S) (x : X) :
    Module.finrank (X.residueField x) (relativeCotangentSpace f x) =
      Module.finrank (X.residueField x) (DottedTangentArrow f x)

AlgebraicGeometry.exists_factorization_unramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/NoetherNormalization.lean, line 986.

Stacks Project, Tag 0CBK. Let f : X ⟶ S be a finite type morphism of affine schemes and let x be a point of X. If r is the dimension over κ(x) of the residue-field fibre at x of the stalk of the sheaf of relative differentials, then f factors as X ⟶ 𝐀^r_S ⟶ S with the first morphism unramified at x.

The coordinates of the factorization are r global sections of X whose differentials span that fibre.

theorem exists_factorization_unramifiedAt {X S : Scheme.{u}} (f : X ⟶ S)
    [IsAffine X] [IsAffine S] [LocallyOfFiniteType f] [QuasiCompact f]
    (x : X) (r : ℕ)
    (hr : Module.finrank (X.residueField x) (relativeCotangentSpace f x) = r) :
    ∃ π : X ⟶ 𝔸(ULift.{u} (Fin r); S),
      (π ≫ 𝔸(ULift.{u} (Fin r); S) ↘ S = f) ∧ UnramifiedAt π x

Tag 0CBL, a lemma

Tag 0CBL in the Stacks Project.

AlgebraicGeometry.exists_affineOpen_immersion_into_affineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/NoetherNormalization.lean, line 1463. The attribute's comment: “clause (1): the immersion into affine (r+1)-space”.

Stacks Project, Tag 0CBL, first clause. Let f : X ⟶ S be locally of finite type, let x be a point of X and let V be an affine open neighbourhood of its image. If r is the dimension over κ(x) of the residue-field fibre at x of the stalk of the sheaf of relative differentials, then f restricted to some affine open U ∋ x lying over V factors as an immersion into relative affine (r+1)-space over V followed by the projection.

theorem exists_affineOpen_immersion_into_affineSpace {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (x : X) (V : S.affineOpens) (hxV : f x ∈ V.1) (r : ℕ)
    (hr : Module.finrank (X.residueField x) (relativeCotangentSpace f x) = r) :
    ∃ (U : X.affineOpens) (_ : x ∈ U.1) (hUV : U.1 ≤ f ⁻¹ᵁ V.1)
      (j : U.1.toScheme ⟶ 𝔸(ULift.{u} (Fin (r + 1)); V.1.toScheme)),
      IsImmersion j ∧
        j ≫ 𝔸(ULift.{u} (Fin (r + 1)); V.1.toScheme) ↘ V.1.toScheme =
          f.resLE V.1 U.1 hUV

AlgebraicGeometry.exists_closedImmersion_smoothFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/GeometricFieldChange/NoetherNormalization.lean, line 1481. The attribute's comment: “clause (2): the closed immersion into a smooth scheme”.

Stacks Project, Tag 0CBL, second clause. In the situation of AlgebraicGeometry.exists_affineOpen_immersion_into_affineSpace, the affine open U may instead be taken to be a closed subscheme of a scheme smooth of relative dimension r over V, through which the restriction of f factors.

theorem exists_closedImmersion_smoothFactorization {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (x : X) (V : S.affineOpens) (hxV : f x ∈ V.1) (r : ℕ)
    (hr : Module.finrank (X.residueField x) (relativeCotangentSpace f x) = r) :
    ∃ (U : X.affineOpens) (_ : x ∈ U.1) (hUV : U.1 ≤ f ⁻¹ᵁ V.1) (D : Scheme.{u})
      (j : U.1.toScheme ⟶ D) (g : D ⟶ V.1.toScheme),
      IsClosedImmersion j ∧ SmoothOfRelativeDimension r g ∧
        j ≫ g = f.resLE V.1 U.1 hUV

Sources

LeanAlgebraicGeometry.exists_affineOpen_quasiFinite_affineSpace_factorization · AlgebraicGeometry.exists_factorization_finite_fiber · AlgebraicGeometry.exists_isImmersion_specMap_derivativePair_of_unramifiedAt · AlgebraicGeometry.exists_isOpenImmersion_specMap_derivativePair_of_etaleAt · AlgebraicGeometry.finiteDimensional_relativeCotangentSpace · AlgebraicGeometry.finrank_relativeCotangentSpace_eq_fiberRelativeCotangentSpace · AlgebraicGeometry.finrank_relativeCotangentSpace_eq_finrank_dottedTangentArrow · AlgebraicGeometry.exists_factorization_unramifiedAt

Section33.19 Dimension of fibres #

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

Tag 0B2I, a lemma

Tag 0B2I in the Stacks Project.

AlgebraicGeometry.topologicalKrullDimAt_fiber_eq_of_target_dim_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/HigherCodimension.lean, line 366. References: EGA IV (7.1.13).

Stacks Project, Tag 0B2I. If the local ring of the target at y is Noetherian of dimension at most one, and the fibre dimension at every generic point of an irreducible component of X through x is d, then the fibre dimension at x is d.

theorem topologicalKrullDimAt_fiber_eq_of_target_dim_le_one (f : X ⟶ Y) [LocallyOfFiniteType f]
    (x : X) (hY : IsNoetherianRing (Y.presheaf.stalk (f x)))
    (hYdim : ringKrullDim (Y.presheaf.stalk (f x)) ≤ 1) (d : ℕ)
    (hgeneric : ∀ η : X, closure {η} ∈ irreducibleComponents X → x ∈ closure {η} →
      topologicalKrullDimAt (f.fiber (f η)) (f.asFiber η) = d) :
    topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = d

Tag 0B2J, a lemma

Tag 0B2J in the Stacks Project.

AlgebraicGeometry.specialFiber_equidimensional, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/ValuationFibreDimension.lean, line 498. The attribute's comment: “equidimensionality”.

Stacks Project, Tag 0B2J (equidimensionality). The special fibre of a surjective, locally finite type morphism from an irreducible scheme to the spectrum of a valuation ring is equidimensional.

lemma specialFiber_equidimensional {R : Type u} [CommRing R] [IsDomain R] [ValuationRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IrreducibleSpace X]
    [LocallyOfFiniteType f] [Surjective f] :
    TopologicalSpace.Equidimensional
      (f.fiber (⟨IsLocalRing.maximalIdeal R, inferInstance⟩ : PrimeSpectrum R))

AlgebraicGeometry.topologicalKrullDim_specialFiber_eq_genericFiber, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/ValuationFibreDimension.lean, line 527. The attribute's comment: “equality of fibre dimensions”. References: EGA IV (14.3.10), “surjective f”; SGA 3 XXV (4.3), “special case”.

Stacks Project, Tag 0B2J (dimension). The special and generic fibres of a surjective, locally finite type morphism from an irreducible scheme to the spectrum of a valuation ring have the same dimension.

lemma topologicalKrullDim_specialFiber_eq_genericFiber
    {R : Type u} [CommRing R] [IsDomain R] [ValuationRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IrreducibleSpace X]
    [LocallyOfFiniteType f] [Surjective f] :
    topologicalKrullDim
        (f.fiber (⟨IsLocalRing.maximalIdeal R, inferInstance⟩ : PrimeSpectrum R)) =
      topologicalKrullDim (f.fiber (⟨⊥, inferInstance⟩ : PrimeSpectrum R))

Tag 0B2K, a lemma

Tag 0B2K in the Stacks Project.

AlgebraicGeometry.topologicalKrullDimAt_fiber_add_one_le_of_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FibreDimension/HigherCodimension.lean, line 216.

Stacks Project, Tag 0B2K. The dimension at a point of a fibre is bounded by the generic fibre dimension plus the dimension of the base local ring minus one, provided every irreducible component through the point dominates a nonclosed generalization of its image.

theorem topologicalKrullDimAt_fiber_add_one_le_of_genericPoints (f : X ⟶ Y)
    [LocallyOfFiniteType f] (x : X) [IsNoetherianRing (Y.presheaf.stalk (f x))] (d : ℕ)
    (h : ∀ Z ∈ irreducibleComponents X, x ∈ Z → ∀ η : X, IsGenericPoint η Z →
      (f η ≠ f x ∧
        topologicalKrullDimAt (f.fiber (f η)) (f.asFiber η) = (d : WithBot ℕ∞))) :
    topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) + 1 ≤
      (d : WithBot ℕ∞) + ringKrullDim (Y.presheaf.stalk (f x))

Sources

LeanAlgebraicGeometry.topologicalKrullDimAt_fiber_eq_of_target_dim_le_one · AlgebraicGeometry.specialFiber_equidimensional · AlgebraicGeometry.topologicalKrullDim_specialFiber_eq_genericFiber · AlgebraicGeometry.topologicalKrullDimAt_fiber_add_one_le_of_genericPoints

Section33.20 Algebraic schemes #

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

Tag 06LG, a definition

Tag 06LG in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.LocallyOfFiniteType registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteTypePoint.lean, line 92 (StacksFrontier): “locally algebraic k-scheme, and the local half of algebraic k-scheme”. References: EGA I (6.3.1), “partial”; EGA I (6.6.2); EGA IV (1.3.2); SGA 3 VIB (1.3); SGA 4 Vbis (5.2.0), “partial”.
AlgebraicGeometry.QuasiCompact registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteTypePoint.lean, line 103 (StacksFrontier): “the quasi-compact half of algebraic k-scheme”. References: EGA 0 (9.1.1), “special case”; EGA I (6.6.1); EGA IV (1.1.1); SGA 1 XIII (1.5); SGA 4 Vbis (4.2.0), “partial”; SGA 6 II (3.0); SGA 7 VII (1.3.8), “partial”.

Tag 06LH, a lemma

Tag 06LH in the Stacks Project.

AlgebraicGeometry.exists_iso_coproduct_spec_local_artinian_of_dimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Zero.lean, line 70. The attribute's comment: “locally algebraic case”.

A zero-dimensional scheme locally of finite type over a field is, over that field, a coproduct of spectra of finite-dimensional local Artinian algebras.

theorem exists_iso_coproduct_spec_local_artinian_of_dimension_zero
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (hdim : topologicalKrullDim X = 0) :
    ∃ (I : Type u) (A : I → Type u)
      (_ : ∀ i, CommRing (A i))
      (_ : ∀ i, Algebra k (A i))
      (_ : ∀ i, IsLocalRing (A i))
      (_ : ∀ i, IsArtinianRing (A i))
      (_ : ∀ i, Module.Finite k (A i))
      (e : X ≅ ∐ fun i ↦ Spec (.of (A i))),
      e.hom ≫ Sigma.desc (fun i ↦ Spec.map (CommRingCat.ofHom (algebraMap k (A i)))) = f

AlgebraicGeometry.isAffine_of_finiteType_of_dimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Zero.lean, line 116. The attribute's comment: “affineness in the algebraic case”.

A zero-dimensional scheme of finite type over a field is affine.

theorem isAffine_of_finiteType_of_dimension_zero
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [QuasiCompact f]
    (hdim : topologicalKrullDim X = 0) : IsAffine X

AlgebraicGeometry.isFinite_of_finiteType_of_dimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Zero.lean, line 125. The attribute's comment: “finiteness in the algebraic case”.

The structure morphism of a zero-dimensional scheme of finite type over a field is finite.

theorem isFinite_of_finiteType_of_dimension_zero
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [QuasiCompact f]
    (hdim : topologicalKrullDim X = 0) : IsFinite f

Tag 0A21, a lemma

Tag 0A21 in the Stacks Project.

AlgebraicGeometry.isCatenarySpace_of_locallyOfFiniteType_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Catenary.lean, line 81. The attribute's comment: “catenary”.

The underlying topological space of a scheme locally of finite type over a field is catenary.

theorem isCatenarySpace_of_locallyOfFiniteType_over_field
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] :
    IrreducibleClosedsCodim.IsCatenarySpace X

AlgebraicGeometry.topologicalKrullDimAt_eq_krullDimOfRing_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/ClosedPoint.lean, line 43. The attribute's comment: “dimension_at_closed_point”.

At a closed point of a scheme locally of finite type over a field, the local dimension of the scheme equals the Krull dimension of its local ring.

theorem topologicalKrullDimAt_eq_krullDimOfRing_stalk
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (x : X) (hx : IsClosed ({x} : Set X)) :
    topologicalKrullDimAt X x = ringKrullDim (X.presheaf.stalk x)

AlgebraicGeometry.topologicalKrullDimAt_eq_iSup_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Components.lean, line 181. The attribute's comment: “local_dimension_components”.

For a scheme locally of finite type over a field, the local dimension at a point is the largest dimension of an irreducible component containing that point.

theorem topologicalKrullDimAt_eq_iSup_irreducibleComponents
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (x : X) :
    topologicalKrullDimAt X x =
      ⨆ Z ∈ {Z ∈ irreducibleComponents X | x ∈ Z}, topologicalKrullDim Z

AlgebraicGeometry.exists_mem_irreducibleComponents_topologicalKrullDim_eq_topologicalKrullDimAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Components.lean, line 190. The attribute's comment: “local_dimension_components”. References: EGA IV (10.6.3), “sup_i dim(Y_i)”.

The maximum dimension among the irreducible components through a point is attained.

theorem exists_mem_irreducibleComponents_topologicalKrullDim_eq_topologicalKrullDimAt
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (x : X) :
    ∃ Z ∈ irreducibleComponents X,
      x ∈ Z ∧ topologicalKrullDim Z = topologicalKrullDimAt X x

AlgebraicGeometry.topologicalKrullDimAt_eq_trdeg_add_krullDim_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Formula.lean, line 99. The attribute's comment: “dimension_formula”. References: EGA IV (13.3.4), “special case”; EGA IV (17.15.8); EGA IV (5.2.3); SGA 1 II (5.8), “partial”; SGA 1 II (5.9), “n = trdeg_k κ(x) + p”.

Stacks Project, Tag 0A21. The dimension at a point of a scheme locally of finite type over a field is the transcendence degree of its residue field plus the dimension of its local ring.

theorem topologicalKrullDimAt_eq_trdeg_add_krullDim_stalk
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    (x : X) :
    letI : Algebra k (X.residueField x) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
    topologicalKrullDimAt X x =
      (Cardinal.toENat (Algebra.trdeg k (X.residueField x)) : WithBot ℕ∞) +
        ringKrullDim (X.presheaf.stalk x)

AlgebraicGeometry.trdeg_residueField_eq_add_one_of_isImmediateSpecialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/ImmediateSpecialization.lean, line 57. The attribute's comment: “immediate_specialization_trdeg”.

Stacks Project, Tag 0A21. For an immediate specialization in a scheme locally of finite type over a field, the transcendence degree of the residue field at the more general point is one greater than that at the more special point.

theorem trdeg_residueField_eq_add_one_of_isImmediateSpecialization
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] {x x' : X} (h : IsImmediateSpecialization x x') :
    letI : Algebra k (X.residueField x) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
    letI : Algebra k (X.residueField x') :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x').hom.toAlgebra
    Algebra.trdeg k (X.residueField x) = Algebra.trdeg k (X.residueField x') + 1

AlgebraicGeometry.krullDimOfRing_stalk_eq_add_one_of_isImmediateSpecialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/ImmediateSpecialization.lean, line 222. The attribute's comment: “immediate_specialization_local_ring”.

For an irreducible or equidimensional scheme locally of finite type over a field, local-ring dimension increases by one under an immediate specialization.

theorem krullDimOfRing_stalk_eq_add_one_of_isImmediateSpecialization
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (x x' : X) (hxx' : IsImmediateSpecialization x x')
    (hX : IrreducibleSpace X ∨ TopologicalSpace.Equidimensional X) :
    ringKrullDim (X.presheaf.stalk x') =
      ringKrullDim (X.presheaf.stalk x) + 1

AlgebraicGeometry.exists_maximalChain_extending, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/MaximalChain.lean, line 121. The attribute's comment: “extend_irreducible_chain”.

Any finite chain of irreducible closed subsets of an irreducible locally algebraic scheme over a field extends to a maximal chain.

lemma exists_maximalChain_extending
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [IrreducibleSpace X]
    (p : LTSeries (IrreducibleCloseds X)) :
    ∃ q : RelSeries {(Y, Z) : IrreducibleCloseds X × IrreducibleCloseds X | Y ⋖ Z},
      IsMin q.head ∧ IsMax q.last ∧ Set.range p ⊆ Set.range q

AlgebraicGeometry.maximalChain_length_eq_topologicalKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/MaximalChain.lean, line 255. The attribute's comment: “maximal_chain_length”.

Every maximal chain of irreducible closed subsets of an irreducible locally algebraic scheme over a field has length equal to the dimension of the scheme.

theorem maximalChain_length_eq_topologicalKrullDim
    (k : Type u) [Field k] (X : Scheme.{u})
    (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] [IrreducibleSpace X]
    (s : RelSeries {p : IrreducibleCloseds X × IrreducibleCloseds X | p.1 ⋖ p.2})
    (hmin : IsMin s.head) (hmax : IsMax s.last) :
    (s.length : WithBot ℕ∞) = topologicalKrullDim X

AlgebraicGeometry.topologicalKrullDim_eq_of_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/NonemptyOpen.lean, line 129. The attribute's comment: “dimension_nonempty_open”. References: SGA 3 VIB (1.5), “more general”.

A nonempty open subset of an irreducible scheme locally of finite type over a field has the same Krull dimension as the whole scheme.

theorem topologicalKrullDim_eq_of_isOpen
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [IrreducibleSpace X] (U : Set X) (hU : IsOpen U)
    (hne : U.Nonempty) :
    topologicalKrullDim X = topologicalKrullDim U

AlgebraicGeometry.topologicalKrullDim_eq_topologicalKrullDimAt_of_irreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/NonemptyOpen.lean, line 170. The attribute's comment: “dimension_at_point_irreducible”.

The dimension of an irreducible scheme locally of finite type over a field equals its dimension at every point.

theorem topologicalKrullDim_eq_topologicalKrullDimAt_of_irreducible
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [IrreducibleSpace X] (x : X) :
    topologicalKrullDim X = topologicalKrullDimAt X x

AlgebraicGeometry.topologicalKrullDimAt_le_of_specialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Specialization.lean, line 56. The attribute's comment: “specialization_local_dimension”.

Local Krull dimension cannot decrease along a specialization.

theorem topologicalKrullDimAt_le_of_specialization {X : Type*} [TopologicalSpace X] {x x' : X}
    (h : x ⤳ x') :
    topologicalKrullDimAt X x ≤ topologicalKrullDimAt X x'

AlgebraicGeometry.krullDimOfRing_stalk_lt_of_specialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Specialization.lean, line 65. The attribute's comment: “specialization_stalk_dimension”.

A nontrivial specialization on a scheme locally of finite type over a field strictly increases the Krull dimension of the local ring.

theorem krullDimOfRing_stalk_lt_of_specialization
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    {x x' : X} (hxx' : x ⤳ x') (hne : x ≠ x') :
    ringKrullDim (X.presheaf.stalk x) < ringKrullDim (X.presheaf.stalk x')

AlgebraicGeometry.topologicalKrullDimAt_eq_iInf_closedSpecializations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Specialization.lean, line 126. The attribute's comment: “local_dimension_closed_specializations”.

For a scheme locally of finite type over a field, its local dimension at a point is the minimum of the dimensions of the local rings at the closed specializations of that point.

theorem topologicalKrullDimAt_eq_iInf_closedSpecializations
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (x : X) :
    topologicalKrullDimAt X x =
      ⨅ (x' : {x' : X // x ⤳ x' ∧ IsClosed ({x'} : Set X)}),
        ringKrullDim (X.presheaf.stalk x')

AlgebraicGeometry.length_eq_trdeg_sub_of_maximalSpecializationChain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/SpecializationChain.lean, line 100. The attribute's comment: “specialization_chain_length”.

The length of a maximal chain of nontrivial specializations on a scheme locally of finite type over a field is the drop in transcendence degree of the residue fields at its endpoints.

theorem length_eq_trdeg_sub_of_maximalSpecializationChain
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (x x' : X) (_hxx' : x ⤳ x') (_hne : x ≠ x')
    (c : RelSeries {p : X × X | p.1 ⤳ p.2 ∧ p.1 ≠ p.2})
    (hc : IsMaximalSpecializationChain c) (hhead : c.head = x) (hlast : c.last = x') :
    letI : Algebra k (X.residueField x) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
    letI : Algebra k (X.residueField x') :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x').hom.toAlgebra
    c.length = Cardinal.toNat (Algebra.trdeg k (X.residueField x)) -
      Cardinal.toNat (Algebra.trdeg k (X.residueField x'))

AlgebraicGeometry.trdeg_residueField_lt_of_specialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/SpecializationTrdeg.lean, line 51. The attribute's comment: “specialization_trdeg”.

On a scheme locally of finite type over a field, residue-field transcendence degree strictly decreases along a nontrivial specialization.

theorem trdeg_residueField_lt_of_specialization
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    {x x' : X} (hxx' : x ⤳ x') (hne : x ≠ x') :
    letI : Algebra k (X.residueField x) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
    letI : Algebra k (X.residueField x') :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x').hom.toAlgebra
    Algebra.trdeg k (X.residueField x') < Algebra.trdeg k (X.residueField x)

AlgebraicGeometry.topologicalKrullDim_eq_trdeg_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Trdeg.lean, line 100. The attribute's comment: “irreducible_dimension_trdeg”. References: EGA IV (4.1.1), “special case”; EGA IV (5.2.1).

Stacks Project, Tag 0A21. The dimension of an irreducible scheme locally of finite type over a field equals the transcendence degree of its residue field at a generic point.

theorem topologicalKrullDim_eq_trdeg_residueField
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [IrreducibleSpace X] [LocallyOfFiniteType f] (x : X)
    (hx : IsGenericPoint x Set.univ) :
    letI : Algebra k (X.residueField x) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
    topologicalKrullDim X =
      (Cardinal.toENat (Algebra.trdeg k (X.residueField x)) : WithBot ℕ∞)

AlgebraicGeometry.topologicalKrullDim_eq_iSup_trdeg_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/Trdeg.lean, line 202. The attribute's comment: “dimension_sup_trdeg”. References: EGA IV (4.1.1); EGA IV (5.2.1), “more general”; EGA IV (5.2.2).

Stacks Project, Tag 0A21. The dimension of a scheme locally of finite type over a field is the supremum of the transcendence degrees of the residue fields at the generic points of its irreducible components.

theorem topologicalKrullDim_eq_iSup_trdeg_residueField
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] :
    topologicalKrullDim X =
      ⨆ x : genericPoints X,
        letI : Algebra k (X.residueField x.1) :=
          ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x.1).hom.toAlgebra
        (Cardinal.toENat (Algebra.trdeg k (X.residueField x.1)) : WithBot ℕ∞)

AlgebraicGeometry.topologicalKrullDimAt_eq_add_ringKrullDim_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Correspondences/GraphCodimension.lean, line 107. The attribute's comment: “local dimension, point closure and local ring”. References: EGA IV (10.6.3), “special case”.

Stacks 0A21. On a scheme locally of finite type over a field the dimension at a point is the dimension of the closure of that point plus the dimension of the local ring there. Both summands are read off the dimension formula of Stacks 0A21 at the same point.

theorem topologicalKrullDimAt_eq_add_ringKrullDim_stalk (k : Type u) [Field k] {T : Scheme.{u}}
    (q : T ⟶ Spec (.of k)) [LocallyOfFiniteType q] (t : T) :
    topologicalKrullDimAt T t =
      topologicalKrullDim (closure ({t} : Set T)) + ringKrullDim (T.presheaf.stalk t)

Tag 0B2L, a lemma

Tag 0B2L in the Stacks Project.

AlgebraicGeometry.locallyOfFiniteType_fiberToSpecResidueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Fibre.lean, line 66. The attribute's comment: “locally_algebraic_fibre”.

A fibre of a morphism between locally algebraic schemes is locally algebraic over the residue field of the corresponding point.

public theorem locallyOfFiniteType_fiberToSpecResidueField
    (k : Type u) [Field k] {X Y : Scheme.{u}}
    (pX : X ⟶ Spec (.of k)) (pY : Y ⟶ Spec (.of k))
    [LocallyOfFiniteType pX]
    (f : X ⟶ Y) (hf : f ≫ pY = pX) (y : Y) :
    LocallyOfFiniteType (f.fiberToSpecResidueField y)

AlgebraicGeometry.topologicalKrullDim_le_fiber_add_imageClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/FibreDimension.lean, line 325. The attribute's comment: “part (2a): dim_x(X_{f(x)}) ≥ d”. References: EGA IV (10.6.1), “(iii), special case”.

Lower bound for the fibre dimension. For a morphism f : X ⟶ Y of schemes locally of finite type over a field with X irreducible, the local dimension of every fibre of f is at least the dimension of X minus the dimension of the reduced closure of the image of f. The bound is stated additively, since WithBot ℕ∞ has no subtraction.

public theorem topologicalKrullDim_le_fiber_add_imageClosure
    (k : Type u) [Field k] {X Y : Scheme.{u}}
    (pX : X ⟶ Spec (.of k)) (pY : Y ⟶ Spec (.of k))
    [LocallyOfFiniteType pX] [LocallyOfFiniteType pY] [IrreducibleSpace X]
    (f : X ⟶ Y) (hf : f ≫ pY = pX) (x : X) :
    topologicalKrullDim X ≤
      topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) +
        topologicalKrullDim
        (Scheme.IdealSheafData.vanishingIdeal
            (Closeds.closure (Set.range (fun x : X => f x)))).subscheme

AlgebraicGeometry.isOpen_and_dense_setOf_topologicalKrullDimAt_fiber_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/FibreDimension.lean, line 404. The attribute's comment: “part (2b): {x | dim_x(X_{f(x)}) = d} is dense open”.

The fibre dimension is generically the expected one. For a morphism f : X ⟶ Y of schemes locally of finite type over a field with X irreducible, the set of points at which the local fibre dimension attains the value d = dim X - dim Z is a dense open subset of X. Here Z is the reduced closure of the image of f, and d is the difference of the two dimensions taken in ℕ, since WithBot ℕ∞ has no subtraction.

public theorem isOpen_and_dense_setOf_topologicalKrullDimAt_fiber_eq
    (k : Type u) [Field k] {X Y : Scheme.{u}}
    (pX : X ⟶ Spec (.of k)) (pY : Y ⟶ Spec (.of k))
    [LocallyOfFiniteType pX] [LocallyOfFiniteType pY] [IrreducibleSpace X]
    (f : X ⟶ Y) (hf : f ≫ pY = pX) (d : ℕ)
    (hd : d = ((topologicalKrullDim X).unbotD 0).toNat -
      ((topologicalKrullDim
        (Scheme.IdealSheafData.vanishingIdeal
          (Closeds.closure (Set.range (fun x : X => f x)))).subscheme).unbotD 0).toNat) :
    IsOpen {x : X | topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = (d : WithBot ℕ∞)} ∧
      Dense {x : X |
        topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = (d : WithBot ℕ∞)}

AlgebraicGeometry.topologicalKrullDimAt_fiber_add_one_le_of_one_le_ringKrullDim_imageClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/FibreDimension.lean, line 571. The attribute's comment: “part (2c): dim_x(X_{f(x)}) ≤ d + dim O_{Z,f(x)} - 1”.

Upper bound for the fibre dimension over a point of higher codimension. For a morphism f : X ⟶ Y of schemes locally of finite type over a field with X irreducible, if the local ring of the reduced closure Z of the image of f at f x has dimension at least one, then

dim_x(X_{f(x)}) ≤ d + dim 𝒪_{Z, f(x)} - 1,

where d = dim X - dim Z. Since WithBot ℕ∞ has no subtraction, the bound is stated by adding one to the left-hand side, as in Tag 0B2K. The point of Z over f x is given by z.

public theorem topologicalKrullDimAt_fiber_add_one_le_of_one_le_ringKrullDim_imageClosure
    (k : Type u) [Field k] {X Y : Scheme.{u}}
    (pX : X ⟶ Spec (.of k)) (pY : Y ⟶ Spec (.of k))
    [LocallyOfFiniteType pX] [LocallyOfFiniteType pY] [IrreducibleSpace X]
    (f : X ⟶ Y) (hf : f ≫ pY = pX) (d : ℕ)
    (hd : d = ((topologicalKrullDim X).unbotD 0).toNat -
      ((topologicalKrullDim
        (Scheme.IdealSheafData.vanishingIdeal
          (Closeds.closure (Set.range (fun x : X => f x)))).subscheme).unbotD 0).toNat)
    (x : X)
    (z : (Scheme.IdealSheafData.vanishingIdeal
      (Closeds.closure (Set.range (fun x : X => f x)))).subscheme)
    (hz : (Scheme.IdealSheafData.vanishingIdeal
      (Closeds.closure (Set.range (fun x : X => f x)))).subschemeι z = f x)
    (h1 : 1 ≤ ringKrullDim
      ((Scheme.IdealSheafData.vanishingIdeal
        (Closeds.closure (Set.range (fun x : X => f x)))).subscheme.presheaf.stalk z)) :
    topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) + 1 ≤
      (d : WithBot ℕ∞) + ringKrullDim
        ((Scheme.IdealSheafData.vanishingIdeal
          (Closeds.closure (Set.range (fun x : X => f x)))).subscheme.presheaf.stalk z)

AlgebraicGeometry.topologicalKrullDimAt_fiber_eq_of_ringKrullDim_imageClosure_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/FibreDimension.lean, line 621. The attribute's comment: “part (2d): dim O_{Z,f(x)} = 1 implies dim_x(X_{f(x)}) = d”.

The fibre dimension over a point of codimension one. For a morphism f : X ⟶ Y of schemes locally of finite type over a field with X irreducible, if the local ring of the reduced closure Z of the image of f at f x has dimension exactly one, then dim_x(X_{f(x)}) = d, where d = dim X - dim Z. The point of Z over f x is given by z.

public theorem topologicalKrullDimAt_fiber_eq_of_ringKrullDim_imageClosure_eq_one
    (k : Type u) [Field k] {X Y : Scheme.{u}}
    (pX : X ⟶ Spec (.of k)) (pY : Y ⟶ Spec (.of k))
    [LocallyOfFiniteType pX] [LocallyOfFiniteType pY] [IrreducibleSpace X]
    (f : X ⟶ Y) (hf : f ≫ pY = pX) (d : ℕ)
    (hd : d = ((topologicalKrullDim X).unbotD 0).toNat -
      ((topologicalKrullDim
        (Scheme.IdealSheafData.vanishingIdeal
          (Closeds.closure (Set.range (fun x : X => f x)))).subscheme).unbotD 0).toNat)
    (x : X)
    (z : (Scheme.IdealSheafData.vanishingIdeal
      (Closeds.closure (Set.range (fun x : X => f x)))).subscheme)
    (hz : (Scheme.IdealSheafData.vanishingIdeal
      (Closeds.closure (Set.range (fun x : X => f x)))).subschemeι z = f x)
    (h1 : ringKrullDim
      ((Scheme.IdealSheafData.vanishingIdeal
        (Closeds.closure (Set.range (fun x : X => f x)))).subscheme.presheaf.stalk z) = 1) :
    topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = (d : WithBot ℕ∞)

AlgebraicGeometry.topologicalKrullDimAt_le_fiber_add_topologicalKrullDimAt_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/FibreDimension.lean, line 686. The attribute's comment: “part (3): dim_x(X_y) ≥ dim_x(X) - dim_y(Y)”.

Local lower bound for the fibre dimension. For a morphism f : X ⟶ Y of schemes locally of finite type over a field and any point x of X with image y = f x,

dim_x(X_y) ≥ dim_x(X) - dim_y(Y).

The source is not assumed irreducible: the bound is obtained by applying part (2a) to each irreducible component of X through x, carrying the reduced induced structure. As elsewhere, the statement is additive because WithBot ℕ∞ has no subtraction.

public theorem topologicalKrullDimAt_le_fiber_add_topologicalKrullDimAt_target
    (k : Type u) [Field k] {X Y : Scheme.{u}}
    (pX : X ⟶ Spec (.of k)) (pY : Y ⟶ Spec (.of k))
    [LocallyOfFiniteType pX] [LocallyOfFiniteType pY]
    (f : X ⟶ Y) (hf : f ≫ pY = pX) (x : X) :
    topologicalKrullDimAt X x ≤
      topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) + topologicalKrullDimAt Y (f x)

Tag 0B2M, a lemma

Tag 0B2M in the Stacks Project.

AlgebraicGeometry.topologicalKrullDimAt_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/Product.lean, line 112. The attribute's comment: “part (1)”.

Stacks Project, Tag 0B2M, part (1). Let X and Y be locally algebraic schemes over a field k. At a point z of the product X ×_{Spec k} Y, the local dimension of the product is the sum of the local dimensions of X and of Y at the two images of z.

theorem topologicalKrullDimAt_pullback (k : Type u) [Field k] {X Y : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [LocallyOfFiniteType g] (z : ↑(pullback f g)) :
    topologicalKrullDimAt ↑(pullback f g) z =
      topologicalKrullDimAt X ((pullback.fst f g) z) +
        topologicalKrullDimAt Y ((pullback.snd f g) z)

AlgebraicGeometry.topologicalKrullDim_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/Product.lean, line 131. The attribute's comment: “part (2)”. References: EGA IV (4.1.5).

Stacks Project, Tag 0B2M, part (2). Let X and Y be locally algebraic schemes over a field k. The dimension of the product X ×_{Spec k} Y is the sum of the dimensions of X and of Y.

theorem topologicalKrullDim_pullback (k : Type u) [Field k] {X Y : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [LocallyOfFiniteType g] :
    topologicalKrullDim ↑(pullback f g) = topologicalKrullDim X + topologicalKrullDim Y

Sources

LeanAlgebraicGeometry.LocallyOfFiniteType · AlgebraicGeometry.QuasiCompact · AlgebraicGeometry.exists_iso_coproduct_spec_local_artinian_of_dimension_zero · AlgebraicGeometry.isAffine_of_finiteType_of_dimension_zero · AlgebraicGeometry.isFinite_of_finiteType_of_dimension_zero · AlgebraicGeometry.isCatenarySpace_of_locallyOfFiniteType_over_field · AlgebraicGeometry.topologicalKrullDimAt_eq_krullDimOfRing_stalk · AlgebraicGeometry.topologicalKrullDimAt_eq_iSup_irreducibleComponents

Section33.21 Complete local rings #

Section 33.21 of the Stacks Project, Tag 0C51. 3 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 0C52, a lemma

Tag 0C52 in the Stacks Project.

AlgebraicGeometry.exists_no_quotient_mvPowerSeries_algEquiv_completedLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/CompleteLocal/NoBasePresentation.lean, line 487. The attribute's comment: “presentation_not_always_over_base_field”. References: EGA IV (18.11.6), “counterexample”; EGA 0 (19.6.5.2), “not k-iso to K[[T]]”.

A completed local ring can admit no presentation over its residue field compatible with the ground field, even when the scheme is locally Noetherian.

public theorem exists_no_quotient_mvPowerSeries_algEquiv_completedLocalRing :
    ∃ (k : Type u) (_ : Field k) (X : Scheme.{u})
      (f : X ⟶ Spec (.of k)) (_ : IsLocallyNoetherian X) (x : X),
      letI : Algebra k (X.residueField x) :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
      letI : Algebra k (Scheme.completedLocalRing X x) :=
        Scheme.completedLocalRingAlgebra f x
      ¬ ∃ (n : ℕ) (I : Ideal (MvPowerSeries (Fin n) (X.residueField x))),
          Nonempty ((MvPowerSeries (Fin n) (X.residueField x) ⧸ I) ≃ₐ[k]
            Scheme.completedLocalRing X x)

AlgebraicGeometry.exists_quotient_mvPowerSeries_algEquiv_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/CompleteLocal/SeparablePresentation.lean, line 56. The attribute's comment: “separable_completed_local_ring_presentation”. References: EGA 0 (19.6.3), “(a) ⇒ (c), special case”; EGA 0 (19.8.8), “(i), special case”.

If the residue field at a point of a locally Noetherian scheme over k is separable over k, then the completed local ring is a quotient of a formal power series ring over the residue field, as a k-algebra, and the equivalence induces the identity on residue fields.

public theorem exists_quotient_mvPowerSeries_algEquiv_adicCompletion
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [IsLocallyNoetherian X] (x : X) :
    let R := X.presheaf.stalk x
    let κ := X.residueField x
    letI : Algebra k R :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.presheaf.germ ⊤ x (by simp)).hom.toAlgebra
    letI : Algebra k κ :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
    Algebra.IsSeparableExtension k κ →
      ∃ (n : ℕ) (I : Ideal (MvPowerSeries (Fin n) κ))
        (hI : I ≤ RingHom.ker
          (MvPowerSeries.constantCoeff : MvPowerSeries (Fin n) κ →+* κ)),
        ∃ e : (MvPowerSeries (Fin n) κ ⧸ I) ≃ₐ[k]
            AdicCompletion (maximalIdeal R) R,
          (AdicCompletion.evalOneₐ (maximalIdeal R)).toRingHom.comp
              e.toRingEquiv.toRingHom =
            Ideal.Quotient.lift I
              (MvPowerSeries.constantCoeff : MvPowerSeries (Fin n) κ →+* κ) hI

Declarations registered for the tag:

AlgebraicGeometry.exists_powerSeries_quotient_ringEquiv_adicCompletion, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Variety/CompleteLocal/PowerSeriesPresentation.lean, line 273 (StacksFrontier): “completed_local_ring_presentation”.

Tag 0C53, an equation

Tag 0C53 in the Stacks Project.

AlgebraicGeometry.exists_powerSeries_quotient_ringEquiv_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/CompleteLocal/PowerSeriesPresentation.lean, line 147. The attribute's comment: “power-series presentation”.

The completed local ring at a point of a locally Noetherian scheme is a quotient of a formal power series ring over its residue field, with the presentation inducing the canonical identification on residue fields.

theorem exists_powerSeries_quotient_ringEquiv_adicCompletion
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [IsLocallyNoetherian X] (x : X) :
    ∃ (n : ℕ) (I : Ideal (MvPowerSeries (Fin n) (X.residueField x)))
      (e : (MvPowerSeries (Fin n) (X.residueField x) ⧸ I) ≃+*
        AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)),
      ∀ a : X.residueField x,
        residue (AdicCompletion (maximalIdeal (X.presheaf.stalk x))
            (X.presheaf.stalk x))
            (e (Ideal.Quotient.mk I (MvPowerSeries.C a))) =
          IsLocalRing.ResidueField.map
            (algebraMap (X.presheaf.stalk x)
              (AdicCompletion (maximalIdeal (X.presheaf.stalk x))
                (X.presheaf.stalk x))) a

AlgebraicGeometry.exists_powerSeries_quotient_ringEquiv_adicCompletion_of_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/CompleteLocal/PowerSeriesPresentation.lean, line 191. The attribute's comment: “separable ground-field compatibility”.

If the residue field at the point is separable over the ground field, the power-series presentation of the completed local ring can be chosen to respect the ground-field maps.

theorem exists_powerSeries_quotient_ringEquiv_adicCompletion_of_isSeparable
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [IsLocallyNoetherian X] (x : X)
    (hsep :
      let kToStalk : k →+* X.presheaf.stalk x :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.presheaf.germ ⊤ x trivial).hom
      letI : Algebra k (X.residueField x) :=
        ((X.residue x).hom.comp kToStalk).toAlgebra
      Algebra.IsSeparable k (X.residueField x)) :
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.presheaf.germ ⊤ x trivial).hom
    let kToResidue : k →+* X.residueField x := (X.residue x).hom.comp kToStalk
    ∃ (n : ℕ) (I : Ideal (MvPowerSeries (Fin n) (X.residueField x)))
      (e : (MvPowerSeries (Fin n) (X.residueField x) ⧸ I) ≃+*
        AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)),
      (∀ a : X.residueField x,
        residue (AdicCompletion (maximalIdeal (X.presheaf.stalk x))
            (X.presheaf.stalk x))
            (e (Ideal.Quotient.mk I (MvPowerSeries.C a))) =
          IsLocalRing.ResidueField.map
            (algebraMap (X.presheaf.stalk x)
              (AdicCompletion (maximalIdeal (X.presheaf.stalk x))
                (X.presheaf.stalk x))) a) ∧
      (∀ a : k,
        e (Ideal.Quotient.mk I (MvPowerSeries.C (kToResidue a))) =
          algebraMap (X.presheaf.stalk x)
            (AdicCompletion (maximalIdeal (X.presheaf.stalk x))
              (X.presheaf.stalk x)) (kToStalk a))

Tag 0C54, a lemma

Tag 0C54 in the Stacks Project.

AlgebraicGeometry.exists_baseChanged_powerSeries_quotient_algEquiv_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/CompletedLocalRingFieldChange.lean, line 525.

A power-series presentation of a completed local ring over k gives, after extending scalars to K, the presentation by the same equations over the residue field upstairs.

theorem exists_baseChanged_powerSeries_quotient_algEquiv_adicCompletion
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}))
    (hdim :
      ringKrullDim
          (X.presheaf.stalk
            ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y)) =
        ringKrullDim
          ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).presheaf.stalk y))
    (hsep :
      let x :=
        (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y
      letI : Algebra k (X.residueField x) :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
      Algebra.IsSeparableExtension k (X.residueField x))
    (n : ℕ)
    (I : Ideal
      (MvPowerSeries (Fin n)
        (X.residueField
          ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y))))
    (hI : I ≤ RingHom.ker
      (MvPowerSeries.constantCoeff :
        MvPowerSeries (Fin n)
            (X.residueField
              ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y)) →+*
          X.residueField
            ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y)))
    (e :
      let x :=
        (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y
      let R := X.presheaf.stalk x
      let κ := X.residueField x
      letI : Algebra k R :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.presheaf.germ ⊤ x (by simp)).hom.toAlgebra
      letI : Algebra k κ :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
      (MvPowerSeries (Fin n) κ ⧸ I) ≃ₐ[k]
        AdicCompletion (maximalIdeal R) R)
    (he :
      let x :=
        (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y
      let R := X.presheaf.stalk x
      let κ := X.residueField x
      letI : Algebra k R :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.presheaf.germ ⊤ x (by simp)).hom.toAlgebra
      letI : Algebra k κ :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
      (AdicCompletion.evalOneₐ (maximalIdeal R)).toRingHom.comp
          e.toRingEquiv.toRingHom =
        Ideal.Quotient.lift I
          (MvPowerSeries.constantCoeff : MvPowerSeries (Fin n) κ →+* κ) hI) :
    let Y := pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K)))
    let p : Y ⟶ X := pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))
    let g : Y ⟶ Spec (.of K) := pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k K)))
    let x := p.base y
    let RY := Y.presheaf.stalk y
    let κy := Y.residueField y
    let κMap : X.residueField x →+* κy := (p.residueFieldMap y).hom
    let J : Ideal (MvPowerSeries (Fin n) κy) := I.map (MvPowerSeries.map κMap)
    let : Algebra K RY :=
      ((Scheme.ΓSpecIso (.of K)).inv ≫ g.appTop ≫ Y.presheaf.germ ⊤ y (by simp)).hom.toAlgebra
    let : Algebra K κy :=
      ((Scheme.ΓSpecIso (.of K)).inv ≫ g.appTop ≫ Y.Γevaluation y).hom.toAlgebra
    ∃ (hJ : J ≤ RingHom.ker
        (MvPowerSeries.constantCoeff : MvPowerSeries (Fin n) κy →+* κy))
      (eY : (MvPowerSeries (Fin n) κy ⧸ J) ≃ₐ[K]
        AdicCompletion (maximalIdeal RY) RY),
      (AdicCompletion.evalOneₐ (maximalIdeal RY)).toRingHom.comp
          eY.toRingEquiv.toRingHom =
        Ideal.Quotient.lift J
          (MvPowerSeries.constantCoeff : MvPowerSeries (Fin n) κy →+* κy) hJ

Sources

LeanAlgebraicGeometry.exists_no_quotient_mvPowerSeries_algEquiv_completedLocalRing · AlgebraicGeometry.exists_quotient_mvPowerSeries_algEquiv_adicCompletion · AlgebraicGeometry.exists_powerSeries_quotient_ringEquiv_adicCompletion · AlgebraicGeometry.exists_powerSeries_quotient_ringEquiv_adicCompletion_of_isSeparable · AlgebraicGeometry.exists_baseChanged_powerSeries_quotient_algEquiv_adicCompletion

Section33.22 Global generation #

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

Tag 0B57, a lemma

Tag 0B57 in the Stacks Project.

Stacks.AlgebraicGeometry.FlatBaseChange.nonempty_generatingSections_pullback_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FlatBaseChange/GlobalGeneration.lean, line 324. The attribute's comment: “corrected: for X ⟶ Spec A quasi-compact and quasi-separated; without quasi-compactness the statement is false, see not_forall_nonempty_generatingSections_pullback_iff”.

[Stacks, Tag 0B57], corrected. Let f : X ⟶ Spec A be a quasi-compact quasi-separated morphism, let g : Spec B ⟶ Spec A be flat and surjective — equivalently, a faithfully flat ring map A ⟶ B — and let F be a quasi-coherent 𝒪_X-module. Then F is generated by global sections if and only if its base change along g is.

The correction is the quasi-compactness and quasi-separatedness of f, which the Stacks Project does not assume. Without quasi-compactness the equivalence fails: not_forall_nonempty_generatingSections_pullback_iff gives a quasi-coherent module on a scheme over Spec ℤ which is not generated by global sections, while its base change along the faithfully flat ℤ ⟶ ℤ[1/3] × ℤ[1/2] is. That scheme is quasi-separated, so it does not show that quasi-separatedness of f is needed; it is the hypothesis of [Stacks, Tag 02KH].

theorem nonempty_generatingSections_pullback_iff (H : IsPullback g' f' f g) [Flat g]
    [Surjective g] [QuasiCompact f] [QuasiSeparated f] (F : X.Modules) [F.IsQuasicoherent] :
    Nonempty F.GeneratingSections ↔
      Nonempty ((Scheme.Modules.pullback g').obj F).GeneratingSections

Stacks.AlgebraicGeometry.FlatBaseChange.nonempty_generatingSections_pullback_iff_specMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FlatBaseChange/GlobalGeneration.lean, line 346. The attribute's comment: “corrected, on a faithfully flat ring map: for X ⟶ Spec A quasi-compact and quasi-separated; without quasi-compactness the statement is false, see not_forall_nonempty_generatingSections_pullback_iff_specMap”.

[Stacks, Tag 0B57], corrected, read on a faithfully flat ring map. For a faithfully flat ring map φ : A ⟶ B and a quasi-coherent module F on a scheme quasi-compact and quasi-separated over Spec A, global generation of F is equivalent to global generation of the base change of F to X ×_{Spec A} Spec B.

The correction is the quasi-compactness and quasi-separatedness of X ⟶ Spec A, which the Stacks Project does not assume. Without quasi-compactness the equivalence fails: not_forall_nonempty_generatingSections_pullback_iff_specMap is the negation of this statement with those two hypotheses removed.

theorem nonempty_generatingSections_pullback_iff_specMap {A B : CommRingCat.{u}} (φ : A ⟶ B)
    (hφ : φ.hom.FaithfullyFlat) {X : Scheme.{u}} (f : X ⟶ Spec A) [QuasiCompact f]
    [QuasiSeparated f] (F : X.Modules) [F.IsQuasicoherent] :
    Nonempty F.GeneratingSections ↔
      Nonempty (((Scheme.Modules.pullback
        (Limits.pullback.fst f (Spec.map φ))).obj F).GeneratingSections)

Tag 0B58, a lemma

Tag 0B58 in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_homogeneousSection_vanishing_at_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/RationalPointHyperplane.lean, line 354. The attribute's comment: “the case X = 𝐏(V), ℒ = 𝒪(1) that the source's proof reduces the lemma to; the reduction itself is not formalized”.

Stacks Tag 0B58 for X = 𝐏(V) and ℒ = 𝒪(1). Let k be an infinite field, q a k-rational point of P(V) and q₁, …, qₙ finitely many points of P(V) distinct from q. Then some vector v of V gives a global section ι v / 1 of 𝒪_{P(V)}(1) that vanishes at q but at none of the qⱼ.

This is the case the source's proof reduces the lemma to; the reduction, which unfolds the definition of a very ample invertible sheaf, is not formalized here.

theorem exists_homogeneousSection_vanishing_at_point
    (k V : Type u) [Field k] [Infinite k] [AddCommGroup V] [Module k V]
    {ι : Type v} [Finite ι] (q : projectiveSpaceOfModule k V)
    (qs : ι → projectiveSpaceOfModule k V)
    (hq : IsRationalPoint (projectiveSpaceOfModuleToSpec k V) q)
    (hne : ∀ j, q ≠ qs j) :
    ∃ v : V,
      q ∉ Stacks.SheafOfModules.nonvanishingLocus
          (X := (AlgebraicGeometry.Proj (fun n => SymPow.symmetricPower n k V)).toRingedSpace)
          (Stacks.ProjTwistSection.twistingModule (fun n => SymPow.symmetricPower n k V) 1)
          (Stacks.ProjTwistSection.homogeneousSection (fun n => SymPow.symmetricPower n k V)
            (SymmetricAlgebra.ι k V v) (ι_mem_symmetricPower_one k V v)) ∧
      ∀ j, qs j ∈ Stacks.SheafOfModules.nonvanishingLocus
          (X := (AlgebraicGeometry.Proj (fun n => SymPow.symmetricPower n k V)).toRingedSpace)
          (Stacks.ProjTwistSection.twistingModule (fun n => SymPow.symmetricPower n k V) 1)
          (Stacks.ProjTwistSection.homogeneousSection (fun n => SymPow.symmetricPower n k V)
            (SymmetricAlgebra.ι k V v) (ι_mem_symmetricPower_one k V v))

AlgebraicGeometry.exists_globalSection_vanishing_at_rationalPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/VeryAmpleVanishAtPoint.lean, line 105.

Stacks Tag 0B58. Let k be an infinite field, X a scheme of finite type over k, L a very ample invertible 𝒪_X-module, x a k-rational point of X and xs finitely many points of X distinct from x. Then some global section of L vanishes at x and at none of the xs j.

Very ampleness is Stacks Tag 01VM, Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple, for the structure morphism X ⟶ Spec k; a k-rational point is AlgebraicGeometry.IsRationalPoint, the condition κ(x) = k; and "vanishes at" is the complement of Stacks.Ample.nonvanishingLocus, the X_s of Stacks Tag 01CY.

theorem exists_globalSection_vanishing_at_rationalPoint
    {k : Type u} [Field k] [Infinite k] {X : Scheme.{u}}
    (fX : X ⟶ Spec (CommRingCat.of k)) (L : X.Modules) [IsInvertibleModule X L]
    [LocallyOfFiniteType fX] [QuasiCompact fX]
    (hL : Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple fX L)
    {ι : Type w} [Finite ι] (x : X) (xs : ι → X)
    (hx : AlgebraicGeometry.IsRationalPoint fX x) (hne : ∀ j, x ≠ xs j) :
    ∃ s : Γ(L, ⊤), x ∉ nonvanishingLocus L s ∧ ∀ j, xs j ∈ nonvanishingLocus L s

Tag 0B3Z, a lemma

Tag 0B3Z in the Stacks Project.

AlgebraicGeometry.exists_submodule_generatingSections_finrank_le_dimension_add_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/InvertibleGlobalGeneration.lean, line 465.

An invertible sheaf generated by a linear family of sections is generated by a subspace of dimension at most one more than the dimension of the scheme.

theorem exists_submodule_generatingSections_finrank_le_dimension_add_one
    (k : Type u) [Field k] [Infinite k] (X : Scheme.{u})
    (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] [QuasiCompact f]
    (L : X.Modules)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (V : Type u) [AddCommGroup V] [Module k V] :
    letI : Algebra k Γ(X, ⊤) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    letI : Module k Γ(L, ⊤) :=
      Module.compHom Γ(L, ⊤) (algebraMap k Γ(X, ⊤))
    ∀ (s : V →ₗ[k] Γ(L, ⊤)),
      Epi (L.freeHomEquiv.symm (fun v : V ↦ Stacks.SheafOfModules.sectionsOfTop L (s v))) →
      ∃ W : Submodule k V,
        FiniteDimensional k W ∧
        Module.finrank k W ≤ ((topologicalKrullDim X).unbotD 0).toNat + 1 ∧
        Epi (L.freeHomEquiv.symm (fun w : W ↦ Stacks.SheafOfModules.sectionsOfTop L (s w.1)))

Sources

LeanStacks.AlgebraicGeometry.FlatBaseChange.nonempty_generatingSections_pullback_iff · Stacks.AlgebraicGeometry.FlatBaseChange.nonempty_generatingSections_pullback_iff_specMap · AlgebraicGeometry.ProjectiveSpaceOfModule.exists_homogeneousSection_vanishing_at_point · AlgebraicGeometry.exists_globalSection_vanishing_at_rationalPoint · AlgebraicGeometry.exists_submodule_generatingSections_finrank_le_dimension_add_one

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

33.3 Varieties to 33.22 Global generation

Section33.3 Varieties#

Tag 020D, a definition

Tag 020G, an example

Tag 05P3, a lemma

Sources

Section33.4 Varieties and rational maps#

Tag 0BXN, a theorem

Tag 0BXP, a lemma

Sources

Section33.5 Change of fields and local rings#

Tag 0C4Y, a lemma

Tag 0C4Z, a lemma

Tag 0C50, a lemma

Sources

Section33.6 Geometrically reduced schemes#

Tag 035V, a definition

Tag 035W, a lemma

Tag 020I, a lemma

Tag 035X, a lemma

Tag 035Y, a lemma

Tag 0384, a lemma

Tag 035Z, a lemma

Tag 04KS, a lemma

Tag 0360, a lemma

Tag 020F, an example

Tag 04KT, a lemma

Sources

Section33.7 Geometrically connected schemes#

Tag 0362, a definition

Tag 054N, a lemma

Tag 0385, a lemma

Tag 0386, a lemma

Tag 0363, a lemma

Tag 0387, a lemma

Tag 0388, a lemma

Tag 038A, an equation

Tag 04KU, a lemma

Tag 038B, a lemma

Tag 0389, a lemma

Tag 038C, a lemma

Tag 056R, a lemma

Tag 04KV, a lemma

Tag 04PY, a lemma

Tag 07VM, a lemma

Tag 04PZ, a lemma

Tag 038D, a lemma

Tag 038E, a lemma

Sources

Section33.8 Geometrically irreducible schemes#

Tag 0365, a definition

Tag 054P, a lemma

Tag 020J, a lemma

Tag 038F, a lemma

Tag 038G, a lemma

Tag 054Q, a lemma

Tag 0H8G, a lemma

Tag 038H, a lemma

Tag 038I, a lemma

Tag 04KW, a lemma

Tag 04KX, a lemma

Tag 0G69, a lemma

Tag 038J, a lemma

Tag 04KY, a lemma

Tag 04KZ, a lemma

Tag 054R, a lemma

Tag 054S, a lemma

Sources

Section33.9 Geometrically integral schemes#

Tag 020H, a definition

Tag 038K, a lemma

Tag 0BUG, a lemma

Tag 0FD1, a lemma

Tag 0FD2, a lemma

Sources

Section33.10 Geometrically normal schemes#

Tag 038M, a definition

Tag 038N, a lemma

Tag 038O, a lemma

Tag 038P, a lemma

Section33.3 Varieties #

Section33.4 Varieties and rational maps #

Section33.5 Change of fields and local rings #

Section33.6 Geometrically reduced schemes #

Section33.7 Geometrically connected schemes #

Section33.8 Geometrically irreducible schemes #

Section33.9 Geometrically integral schemes #

Section33.10 Geometrically normal schemes #

Section33.11 Change of fields and locally Noetherian schemes #

Section33.12 Geometrically regular schemes #

Section33.13 Change of fields and the Cohen-Macaulay property #

Section33.14 Change of fields and the Jacobson property #

Section33.15 Change of fields and ample invertible sheaves #

Section33.16 Tangent spaces #

Section33.17 Generically finite morphisms #

Section33.18 Variants of Noether normalization #

Section33.19 Dimension of fibres #

Section33.20 Algebraic schemes #

Section33.21 Complete local rings #