33.23 Separating points and… to 33.38 One dimensional…

Section33.23 Separating points and tangent vectors#

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

Tag 0E8S, a lemma

Tag 0E8S in the Stacks Project.

AlgebraicGeometry.isRelativelyVeryAmple_and_isClosedImmersion_toProjectiveSpaceOfModule_of_separates, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SeparatingPointsTangentVectors/Canonical.lean, line 454.

Stacks, Tag 0E8S. Let k be an algebraically closed field, let X be a proper k-scheme, let ℒ be an invertible 𝒪_X-module and let V ⊂ H⁰(X, ℒ) be a k-subvector space. If

  1. for every pair of distinct closed points x, y ∈ X there is a section s ∈ V which vanishes at x but not at y, and
  2. for every closed point x ∈ X and nonzero tangent vector θ ∈ T_{X/k, x} there exists a section s ∈ V which vanishes at x but whose pullback by θ is nonzero,

then ℒ is very ample and the canonical morphism φ_{ℒ, V} : X ⟶ 𝐏(V) is a closed immersion.

The conclusion is the conjunction of four assertions: V is finite-dimensional over k; ℒ is very ample relative to the structure morphism; V generates ℒ, provided no closed point of X is its only one; and for every basis of V whose family of images generates ℒ the canonical morphism φ_{ℒ, V} : X ⟶ 𝐏(V) of [Stacks, Tag 0FCY] read in that basis is a closed immersion.

Finite-dimensionality of V is not assumed but derived, from [Stacks, Tag 02O6] for the invertible module ℒ on the proper scheme X; so is generation, and so is the canonical morphism itself, together with the identification of the pulled-back hyperplane sheaf with ℒ. The side condition on the third assertion is the gap in the source's proof, discussed in the module documentation: on a scheme with exactly one closed point condition (1) is vacuous and V can generate nothing.

theorem isRelativelyVeryAmple_and_isClosedImmersion_toProjectiveSpaceOfModule_of_separates
    (p : X ⟶ Spec (.of k)) [IsProper p] (L : X.Modules) [IsInvertibleModule X L] :
    letI : Module k Γ(L, ⊤) := Module.compHom _ (baseRingMap p)
    ∀ V : Submodule k Γ(L, ⊤),
      SeparatesClosedPoints (fun v : V => (v : Γ(L, ⊤))) →
      SeparatesTangentVectors p (fun v : V => (v : Γ(L, ⊤))) →
      Module.Finite k V ∧
      Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple p L ∧
      ((∀ x : X, IsClosed ({x} : Set X) → ∃ y : X, IsClosed ({y} : Set X) ∧ y ≠ x) →
        GeneratesStalks (fun v : V => (v : Γ(L, ⊤)))) ∧
      ∀ (n : ℕ) (b : Module.Basis (Fin (n + 1)) k V)
        (hb : GeneratesStalks fun i => ((b i : V) : Γ(L, ⊤))),
        IsClosedImmersion (toProjectiveSpaceOfModule b (fun i => ((b i : V) : Γ(L, ⊤))) hb p)
Tag 0E8T, a lemma

Tag 0E8T in the Stacks Project.

AlgebraicGeometry.isRelativelyVeryAmple_of_surjectsOnDegreeTwo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SeparatingPointsTangentVectors/DegreeTwo.lean, line 196. The attribute's comment: “the degree-two hypothesis is stated with the degree of a zero-dimensional subscheme as finrank over k; the classification of degree-two subschemes into point pairs and fat points is a hypothesis, as is the Tag 0FCY morphism to 𝐏(E) inherited from Tag 0E8S, and the linear system is required to be complete”.

Stacks, Tag 0E8T. Let k be an algebraically closed field, let X be proper over k through p, let E be a quasi-coherent k-module and let i : X ⟶ 𝐏(E) be a morphism over k with i^* 𝒪_{𝐏(E)}(1) ≅ ℒ realizing the complete linear system of an invertible ℒ. If H⁰(X, ℒ) ⟶ H⁰(Z, ℒ|_Z) is surjective for every closed subscheme Z ⊆ X which is zero-dimensional of degree two over k, then ℒ is very ample relative to p.

The two kinds of degree-two subscheme give the two separation conditions of Stacks, Tag 0E8S, whose very-ampleness clause then applies.

theorem isRelativelyVeryAmple_of_surjectsOnDegreeTwo [IsAlgClosed k]
    {E : (Spec (CommRingCat.of k)).Modules} [E.IsQuasicoherent]
    (p : X ⟶ Spec (CommRingCat.of k)) [IsProper p]
    (i : X ⟶ (relativeProj (symAlgebra E)).scheme)
    (h : i ≫ (relativeProj (symAlgebra E)).toBase = p)
    {L : X.Modules} [IsInvertibleModule X L]
    (e : (Scheme.Modules.pullback i).obj (twistOne E) ≅ L)
    {V : Type v} {t : V → (twistOne E).val.obj (op ⊤)} {ψ : V → L.val.obj (op ⊤)}
    (htψ : ∀ v, e.hom.val.app (op ⊤) (pullbackSectionTop i (twistOne E) (t v)) = ψ v)
    (hfull : Function.Surjective ψ) (hsurj : SurjectsOnDegreeTwo p L)
    (hpair : HasDegreeTwoPointPairs p L) (htan : HasDegreeTwoFatPoints p L) :
    IsRelativelyVeryAmple p L

AlgebraicGeometry.isRelativelyVeryAmple_of_surjectsOnDegreeTwo_of_complete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SeparatingPointsTangentVectors/DegreeTwoClassification.lean, line 646. The attribute's comment: “the degree-two criterion with the classification of the degree-two zero-dimensional subschemes into point pairs and fat points PROVED; what is still assumed is the Tag 0FCY morphism to 𝐏(E) with its twist identification, inherited from Tag 0E8S, and completeness of the linear system it realizes”.

Stacks, Tag 0E8T, with the classification of the degree-two subschemes proved. Let k be algebraically closed, let X be proper over k through p, let E be a quasi-coherent k-module and let i : X ⟶ 𝐏(E) be a morphism over k with i^* 𝒪_{𝐏(E)}(1) ≅ ℒ realizing the complete linear system of an invertible ℒ. If H⁰(X, ℒ) ⟶ H⁰(Z, ℒ|_Z) is surjective for every closed subscheme Z ⊆ X which is zero-dimensional of degree two over k, then ℒ is very ample relative to p.

This is AlgebraicGeometry.isRelativelyVeryAmple_of_surjectsOnDegreeTwo with its two classification hypotheses supplied: AlgebraicGeometry.hasDegreeTwoPointPairs and AlgebraicGeometry.hasDegreeTwoFatPoints. What is still a hypothesis is the morphism to 𝐏(E) with its identification of the pulled-back twist, which is the morphism of Stacks, Tag 0FCY inherited from the criterion of Stacks, Tag 0E8S, together with completeness of the linear system it realizes.

theorem isRelativelyVeryAmple_of_surjectsOnDegreeTwo_of_complete
    {E : (Spec (CommRingCat.of k)).Modules} [E.IsQuasicoherent]
    (p : X ⟶ Spec (CommRingCat.of k)) [IsProper p]
    (i : X ⟶ (relativeProj (symAlgebra E)).scheme)
    (h : i ≫ (relativeProj (symAlgebra E)).toBase = p)
    {L : X.Modules} [IsInvertibleModule X L]
    (e : (Scheme.Modules.pullback i).obj (twistOne E) ≅ L)
    {V : Type v} {t : V → (twistOne E).val.obj (op ⊤)} {ψ : V → L.val.obj (op ⊤)}
    (htψ : ∀ v, e.hom.val.app (op ⊤) (pullbackSectionTop i (twistOne E) (t v)) = ψ v)
    (hfull : Function.Surjective ψ) (hsurj : SurjectsOnDegreeTwo p L) :
    IsRelativelyVeryAmple p L

AlgebraicGeometry.isRelativelyVeryAmple_of_surjectsOnDegreeTwo', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SeparatingPointsTangentVectors/DegreeTwoComplete.lean, line 374. The attribute's comment: “the full statement, with no assumed data: the dimension of a zero-dimensional closed subscheme is the topological Krull dimension of its space and its degree is the dimension over k of its ring of global sections”.

Stacks, Tag 0E8T. Let k be an algebraically closed field, let X be a proper k-scheme and let ℒ be an invertible 𝒪_X-module. If H⁰(X, ℒ) ⟶ H⁰(Z, ℒ|_Z) is surjective for every closed subscheme Z ⊆ X of dimension zero and degree two over k, then ℒ is very ample on X over k.

The pairs of distinct closed points and the fat points among those subschemes give the two separation conditions of Stacks, Tag 0E8S; the same hypothesis makes the global sections generate ℒ, so a basis of the finite-dimensional space H⁰(X, ℒ) defines a morphism to ℙⁿ_k realizing the complete linear system, and that morphism is a closed immersion. Projective space over the affine base is the projective bundle of a free module, which turns the immersion into the datum relative very ampleness asks for.

theorem isRelativelyVeryAmple_of_surjectsOnDegreeTwo' {k : Type u} [Field k] [IsAlgClosed k]
    {X : Scheme.{u}} (p : X ⟶ Spec (.of k)) [IsProper p] (L : X.Modules)
    [IsInvertibleModule X L] (hsurj : SurjectsOnDegreeTwo p L) :
    Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple p L
Sources
LeanAlgebraicGeometry.isRelativelyVeryAmple_and_isClosedImmersion_toProjectiveSpaceOfModule_of_separates · AlgebraicGeometry.isRelativelyVeryAmple_of_surjectsOnDegreeTwo · AlgebraicGeometry.isRelativelyVeryAmple_of_surjectsOnDegreeTwo_of_complete · AlgebraicGeometry.isRelativelyVeryAmple_of_surjectsOnDegreeTwo'

Section33.24 Closures of products#

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

Tag 047B, a lemma

Tag 047B in the Stacks Project.

AlgebraicGeometry.closure_product, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/ClosureProduct.lean, line 111. References: EGA IV (2.4.11), “more general”.

Stacks Project, Tag 047B. The set-theoretic fibre product of the closures of two subsets of schemes over a field is the closure of their set-theoretic fibre product.

theorem closure_product {k : Type u} [Field k] {X Y : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k)) (A : Set X) (B : Set Y) :
    (pullback.fst f g).base ⁻¹' closure A ∩ (pullback.snd f g).base ⁻¹' closure B =
      closure ((pullback.fst f g).base ⁻¹' A ∩ (pullback.snd f g).base ⁻¹' B)
Tag 04Q0, a lemma

Tag 04Q0 in the Stacks Project.

AlgebraicGeometry.closure_range_pullback_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/ClosureProduct.lean, line 169.

Stacks Project, Tag 04Q0. For morphisms f : A ⟶ X and g : B ⟶ Y of schemes over a field, the closure of the image of the induced morphism A ×ₖ B ⟶ X ×ₖ Y is the set-theoretic fibre product of the closures of the two images.

theorem closure_range_pullback_map {k : Type u} [Field k] {A B X Y : Scheme.{u}}
    (pA : A ⟶ Spec (.of k)) (pB : B ⟶ Spec (.of k))
    (pX : X ⟶ Spec (.of k)) (pY : Y ⟶ Spec (.of k))
    (f : A ⟶ X) (g : B ⟶ Y) (hf : f ≫ pX = pA) (hg : g ≫ pY = pB) :
    (pullback.fst pX pY).base ⁻¹' closure (Set.range f.base) ∩
        (pullback.snd pX pY).base ⁻¹' closure (Set.range g.base) =
      closure (Set.range
        (pullback.map pA pB pX pY f g (𝟙 _)
          (by simpa using hf.symm) (by simpa using hg.symm)).base)
Tag 04Q1, a lemma

Tag 04Q1 in the Stacks Project.

AlgebraicGeometry.existsUnique_imageProductMapIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/SchemeTheoreticImage.lean, line 100.

The image of the product of two quasi-compact maps over a field is canonically isomorphic, over the product of their targets, to the product of their scheme-theoretic images.

public theorem existsUnique_imageProductMapIso
    {k : Type u} [Field k] {A B X Y : Scheme.{u}}
    (pX : X ⟶ Spec (.of k)) (pY : Y ⟶ Spec (.of k))
    (f : A ⟶ X) (g : B ⟶ Y) [QuasiCompact f] [QuasiCompact g] :
    ∃! e : (productMap pX pY f g).image ≅
        pullback (f.imageι ≫ pX) (g.imageι ≫ pY),
      e.hom ≫ productMap pX pY f.imageι g.imageι =
        (productMap pX pY f g).imageι
Sources
LeanAlgebraicGeometry.closure_product · AlgebraicGeometry.closure_range_pullback_map · AlgebraicGeometry.existsUnique_imageProductMapIso

Section33.25 Schemes smooth over fields#

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

Tag 04QN, a lemma

Tag 04QN in the Stacks Project.

AlgebraicGeometry.smooth_of_isLocallyFree_relativeDifferentials_of_charZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/LocallyFreeDifferentials.lean, line 133. References: EGA IV (17.15.6), “characteristic zero”; EGA IV (16.12.2), “base field, finite type”; EGA IV (17.15.7), “free ⇒ smooth”.

Stacks Project, Tag 04QN. A scheme locally of finite type over a field of characteristic zero is smooth if its sheaf of relative differentials is locally free.

theorem smooth_of_isLocallyFree_relativeDifferentials_of_charZero
    {k : Type u} [Field k] [CharZero k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f]
    (hΩ : _root_.SheafOfModules.IsLocallyFree.{u, u, u} f.relativeDifferentials) :
    Smooth f
Tag 04QP, a lemma

Tag 04QP in the Stacks Project.

AlgebraicGeometry.smooth_of_isLocallyFree_relativeDifferentials_of_perfectField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/LocallyFreeDifferentialsPerfectField.lean, line 230. References: EGA IV (17.15.6), “perfect k, reduced X”; SGA 1 II (5.7), “k perfect, X reduced”; SGA 1 II (5.5), “(ii)=>(i), X reduced”.

Stacks Project, Tag 04QP. A reduced scheme locally of finite type over a perfect field is smooth if its sheaf of relative differentials is locally free.

theorem smooth_of_isLocallyFree_relativeDifferentials_of_perfectField
    {k : Type u} [Field k] [PerfectField k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsReduced X] [LocallyOfFiniteType f]
    (hΩ : _root_.SheafOfModules.IsLocallyFree.{u, u, u} f.relativeDifferentials) :
    Smooth f
Tag 056S, a lemma

Tag 056S in the Stacks Project.

AlgebraicGeometry.isRegular_of_smooth_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Smooth/Regular.lean, line 42. References: EGA IV (17.15.2), “smooth ⇒ regular”.

Stacks Project, Tag 056S. A scheme smooth over a field is regular.

public theorem isRegular_of_smooth_over_field
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [Smooth f] :
    IsRegular X
Tag 056T, a lemma

Tag 056T in the Stacks Project.

AlgebraicGeometry.isGeometricallyRegular_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Smooth/GeometricallyRegularNormal.lean, line 83. The attribute's comment: “geometrically regular”. References: EGA IV (17.15.2), “necessity”; EGA IV (17.5.2), “field base, smooth⇒reg”; SGA 1 II (3.1), “base a field, regular”; SGA 3 XI (1.2), “Proposition 1.2(i)”.

Stacks Project, Tag 056T, the geometric-regularity conclusion: a scheme smooth over a field k is geometrically regular over k.

Proved at every point of the base change, not only at the points lying over the given point.

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

AlgebraicGeometry.isGeometricallyNormal_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Smooth/GeometricallyRegularNormal.lean, line 94. The attribute's comment: “geometrically normal”. References: EGA IV (7.3.9), “special case”; SGA 1 II (3.1), “base a field, normal”.

Stacks Project, Tag 056T, the geometric-normality conclusion: a scheme smooth over a field k is geometrically normal over k.

public theorem isGeometricallyNormal_of_smooth {k : Type u} [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [Smooth f] : IsGeometricallyNormal f

AlgebraicGeometry.geometricallyReduced_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Smooth/GeometricallyReducedFibres.lean, line 82. The attribute's comment: “geometrically reduced”. References: EGA IV (17.15.2), “smooth ⇒ reduced”; EGA IV (7.3.9), “special case”; SGA 1 II (3.1), “base a field, reduced”.

Stacks Project, Tag 056T, the geometric-reducedness conclusion: a smooth morphism of schemes is geometrically reduced, that is, its base change to every field-valued point of the target is a reduced scheme.

The source fixes a field k as the base; no base field is needed, a morphism Spec K ⟶ Spec k being the same thing as a field extension of k.

public theorem geometricallyReduced_of_smooth {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] :
    GeometricallyReduced f
Tag 055T, a lemma

Tag 055T in the Stacks Project.

AlgebraicGeometry.exists_closedPoint_finite_separable_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/SeparableClosedPoints.lean, line 54.

Stacks Project, Tag 055T. A nonempty open subset of affine space over a field contains a closed point whose residue field is a finite separable extension of the field.

theorem exists_closedPoint_finite_separable_residueField
    {k : Type u} [Field k] {d : ℕ}
    (W : Set (AffineSpace (ULift.{u} (Fin d)) (Spec (.of k))))
    (hWopen : IsOpen W) (hWnonempty : W.Nonempty) :
    ∃ w : AffineSpace (ULift.{u} (Fin d)) (Spec (.of k)),
      w ∈ W ∧ w ∈ closedPoints (AffineSpace (ULift.{u} (Fin d)) (Spec (.of k))) ∧
        let X := AffineSpace (ULift.{u} (Fin d)) (Spec (.of k))
        let f := X ↘ Spec (.of k)
        letI := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation w).hom.toAlgebra
        Module.Finite k (X.residueField w) ∧
          Algebra.IsSeparable k (X.residueField w)
Tag 056U, a lemma

Tag 056U in the Stacks Project.

AlgebraicGeometry.dense_closedPoints_with_finite_separable_residueField_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/DenseSeparableClosedPoints.lean, line 142.

Stacks Project, Tag 056U. If X is smooth over a field k, then the closed points of X whose residue fields are finite separable extensions of k are dense in X.

theorem dense_closedPoints_with_finite_separable_residueField_of_smooth
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [Smooth f] :
    Dense {x : X | x ∈ closedPoints X ∧
      letI := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
      Module.Finite k (X.residueField x) ∧
        Algebra.IsSeparable k (X.residueField x)}
Tag 056V, a lemma

Tag 056V in the Stacks Project.

AlgebraicGeometry.geometricallyReduced_iff_exists_dense_open_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Smooth/DenseSmoothOpen.lean, line 88. References: EGA IV (17.15.12), “X reduced, 1st equiv”.

A reduced scheme locally of finite type over a field is geometrically reduced if and only if it contains a dense open subscheme smooth over that field.

public theorem geometricallyReduced_iff_exists_dense_open_smooth
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsReduced X] [LocallyOfFiniteType f] :
    GeometricallyReduced f ↔
      ∃ U : X.Opens, Dense (U : Set X) ∧ Smooth (U.ι ≫ f)
Tag 0B8X, a lemma

Tag 0B8X in the Stacks Project.

AlgebraicGeometry.smoothAt_locus_eq_regular_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Smooth/SmoothLocus.lean, line 64. The attribute's comment: “equality of the smooth and regular loci”. References: EGA IV (17.15.2), “k perfect case”; EGA 0 (19.0.2), “more general”; EGA IV (17.15.5), “special case”; SGA 1 II (5.4), “perfect k”; SGA 6 XIV (4.2), “Clause”.

Over a perfect field, the points where a locally finite type scheme is smooth are exactly the points whose local rings are regular.

public theorem smoothAt_locus_eq_regular_locus
    (k : Type u) [Field k] [PerfectField k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] :
    {x : X | InfinitesimalLifting.SmoothAt f x} =
      {x : X | IsRegularLocalRing (X.presheaf.stalk x)}

AlgebraicGeometry.isOpen_smoothAt_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Smooth/SmoothLocus.lean, line 103. The attribute's comment: “openness of the smooth locus”.

The locus where a morphism of schemes is smooth is open.

public theorem isOpen_smoothAt_locus
    {X S : Scheme.{u}} (f : X ⟶ S) :
    IsOpen {x : X | InfinitesimalLifting.SmoothAt f x}

AlgebraicGeometry.dense_smoothAt_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Smooth/SmoothLocus.lean, line 121. The attribute's comment: “density of the smooth locus”. References: SGA 4½ Th finitude (2.7), “Perfect-field clause”.

Over a perfect field, the points where a reduced scheme locally of finite type is smooth are dense.

public theorem dense_smoothAt_locus
    (k : Type u) [Field k] [PerfectField k] {X : Scheme.{u}} [IsReduced X]
    (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] :
    Dense {x : X | InfinitesimalLifting.SmoothAt f x}

AlgebraicGeometry.smoothAt_locus_eq_regular_locus_and_isOpen_and_dense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Smooth/SmoothLocus.lean, line 142. References: EGA 0 (19.0.2), “IV, special case”; EGA IV (17.15.12), “special case”; EGA IV (6.12.5), “special case”; EGA IV (6.8.7), “special case”; EGA IV (7.8.3), “(iv), openness of Reg(X)”; EGA IV (7.8.6), “(iii), special case”; SGA 1 II (4.14), “special case”; SGA 1 II (5.4), “more general”; SGA 4½ Th finitude (2.7), “Perfect-field clause”; SGA 6 XIV (4.2), “Clause”.

Let k be a perfect field and let X be a reduced scheme locally of finite type over k. Then the set of points at which X is smooth over k is the set of points whose local ring is regular, and that set is a dense open subset of X.

public theorem smoothAt_locus_eq_regular_locus_and_isOpen_and_dense
    (k : Type u) [Field k] [PerfectField k] {X : Scheme.{u}} [IsReduced X]
    (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] :
    {x : X | InfinitesimalLifting.SmoothAt f x} =
        {x : X | IsRegularLocalRing (X.presheaf.stalk x)} ∧
      IsOpen {x : X | InfinitesimalLifting.SmoothAt f x} ∧
      Dense {x : X | InfinitesimalLifting.SmoothAt f x}

Declarations registered for the tag:

Tag 05AX, a lemma

Tag 05AX in the Stacks Project.

AlgebraicGeometry.smoothAt_of_flatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Smooth/FlatDescent.lean, line 44. The attribute's comment: “pointwise statement”.

Smoothness over a field descends at a point through a morphism which is flat there, provided both schemes are locally of finite type over the field.

public theorem smoothAt_of_flatAt
    {k : Type u} [Field k] {X Y : Scheme.{u}} (f : X ⟶ Y)
    (p : Y ⟶ Spec (.of k)) [LocallyOfFiniteType (f ≫ p)] [LocallyOfFiniteType p]
    (x : X) (hX : InfinitesimalLifting.SmoothAt (f ≫ p) x)
    (hf : AlgebraicGeometry.IsFlatAt f.toLRSHom.toShHom x) :
    InfinitesimalLifting.SmoothAt p (f x)

AlgebraicGeometry.smooth_of_flat_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Smooth/FlatDescent.lean, line 59. The attribute's comment: “global consequence”.

A flat surjective image of a scheme smooth over a field is smooth, when both schemes are locally of finite type over that field.

public theorem smooth_of_flat_of_surjective
    {k : Type u} [Field k] {X Y : Scheme.{u}} (f : X ⟶ Y)
    (p : Y ⟶ Spec (.of k)) [LocallyOfFiniteType p] [Smooth (f ≫ p)]
    [Flat f] [Surjective f] : Smooth p
Tag 0CDW, a lemma

Tag 0CDW in the Stacks Project.

AlgebraicGeometry.geometricallyIntegral_of_isVariety_of_smoothAt_rationalPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/SmoothRationalPoint.lean, line 81.

Stacks Project, Tag 0CDW. A variety over a field with a rational point at which its structure morphism is smooth is geometrically integral.

theorem geometricallyIntegral_of_isVariety_of_smoothAt_rationalPoint
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsVariety k f]
    (s : Spec (.of k) ⟶ X) (hs : s ≫ f = 𝟙 _)
    (hsm : InfinitesimalLifting.SmoothAt f (s.base (genericPoint (Spec (.of k))))) :
    GeometricallyIntegral f
Tag 0H3W, a lemma

Tag 0H3W in the Stacks Project.

AlgebraicGeometry.exists_finite_purelyInseparable_extension_smooth_stratification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/SmoothStratification.lean, line 728. References: EGA IV (17.15.13).

A finite-type scheme over a field has a finite smooth stratification after a finite purely inseparable extension of the field.

theorem exists_finite_purelyInseparable_extension_smooth_stratification
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [QuasiCompact f] :
    ∃ (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 Y : Scheme.{u} := pullback f g
      let p : Y ⟶ Spec (.of k') := pullback.snd f g
      ∃ (t : ℕ) (Z : Fin (t + 1) → Y.IdealSheafData),
        Z 0 = Scheme.IdealSheafData.vanishingIdeal (⊤ : Closeds Y) ∧
        Z ⟨t, Nat.lt_succ_self t⟩ = ⊤ ∧
        (∀ i : Fin t, Z i.castSucc ≤ Z i.succ) ∧
        (∀ i : Fin t, ∃ U : (Z i.castSucc).subscheme.Opens,
          (U : Set (Z i.castSucc).subscheme) =
            {x | (Z i.castSucc).subschemeι x ∉ (Z i.succ).support} ∧
          Smooth (U.ι ≫ (Z i.castSucc).subschemeι ≫ p))
Sources
LeanAlgebraicGeometry.smooth_of_isLocallyFree_relativeDifferentials_of_charZero · AlgebraicGeometry.smooth_of_isLocallyFree_relativeDifferentials_of_perfectField · AlgebraicGeometry.isRegular_of_smooth_over_field · AlgebraicGeometry.isGeometricallyRegular_of_smooth · AlgebraicGeometry.isGeometricallyNormal_of_smooth · AlgebraicGeometry.geometricallyReduced_of_smooth · AlgebraicGeometry.exists_closedPoint_finite_separable_residueField · AlgebraicGeometry.dense_closedPoints_with_finite_separable_residueField_of_smooth

Section33.26 Types of varieties#

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

Tag 04L1, a definition

Tag 04L1 in the Stacks Project.

AlgebraicGeometry.IsProperVariety, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Basic.lean, line 59. The attribute's comment: “proper_variety”.

A variety over a field is proper when its structure morphism to the spectrum of the field is proper.

class IsProperVariety (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) : Prop
    extends IsVariety k f, IsProper f

AlgebraicGeometry.IsSmoothVariety, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Basic.lean, line 81. The attribute's comment: “smooth_variety”.

A variety over a field is smooth when its structure morphism to the spectrum of the field is smooth.

class IsSmoothVariety (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) : Prop extends IsVariety k f, Smooth f

AlgebraicGeometry.IsProjectiveVariety, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Projective.lean, line 83. The attribute's comment: “projective_variety”.

Stacks Project, Tag 04L1. A variety over a field is projective when its structure morphism to the spectrum of the field is H-projective, equivalently projective.

class IsProjectiveVariety (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) : Prop extends IsVariety k f

AlgebraicGeometry.isProjectiveVariety_iff_isProjectiveMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Projective.lean, line 99. The attribute's comment: “projective_variety_closed_subscheme”.

Stacks Project, Tag 04L1, clause (2), the form cited to [Stacks, Tag 01WB]. For a variety, being a projective variety is equivalent to H-projectivity of its structure morphism, that is, to X being isomorphic over k to a closed subscheme of ℙⁿ_k for some n.

theorem isProjectiveVariety_iff_isProjectiveMorphism (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsVariety k f] :
    IsProjectiveVariety k f ↔ IsProjectiveMorphism f

AlgebraicGeometry.isProjectiveVariety_iff_isProjective', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Projective.lean, line 112. The attribute's comment: “projective_variety_2”.

Stacks Project, Tag 04L1, clause (2). A projective variety is exactly a variety whose structure morphism to the spectrum of the field is projective.

The source defines the notion by projectivity of the structure morphism and observes, citing [Stacks, Tag 01WB], that it amounts to X being isomorphic to a closed subscheme of ℙⁿ_k for some n, which is the H-projectivity carried by the class. The two agree over the affine base Spec k by AlgebraicGeometry.isProjective_iff_isProjectiveMorphism_of_isAffine.

theorem isProjectiveVariety_iff_isProjective' (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) :
    IsProjectiveVariety k f ↔ IsVariety k f ∧ IsProjective f

AlgebraicGeometry.IsQuasiProjectiveVariety, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Projective.lean, line 134. The attribute's comment: “quasi_projective_variety”.

Stacks Project, Tag 04L1. A variety over a field is quasi-projective when its structure morphism to the spectrum of the field is quasi-projective.

class IsQuasiProjectiveVariety (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) : Prop extends IsVariety k f

AlgebraicGeometry.isQuasiProjectiveVariety_iff_isHQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Projective.lean, line 162. The attribute's comment: “quasi_projective_variety_locally_closed_subscheme”.

Stacks Project, Tag 04L1, clause (3). A quasi-projective variety is exactly a variety whose structure morphism is H-quasi-projective, that is, admits a quasi-compact immersion into ℙⁿ_k over k for some n, which realizes X as a locally closed subscheme of ℙⁿ_k.

This is the identification the source records by citing [Stacks, Tag 01VZ]; over the affine base Spec k it is AlgebraicGeometry.isQuasiProjective_iff_isHQuasiProjective_of_isAffine.

theorem isQuasiProjectiveVariety_iff_isHQuasiProjective (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) :
    IsQuasiProjectiveVariety k f ↔ IsVariety k f ∧ IsHQuasiProjective f

Declarations registered for the tag:

Tag 04L2, a lemma

Tag 04L2 in the Stacks Project.

AlgebraicGeometry.isSeparable_globalSections_of_isProperVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/ProperVarietyGlobalSections.lean, line 76. The attribute's comment: “part (2)”.

Stacks Project, Tag 04L2, part (2). For a geometrically reduced proper variety over a field k, the field of global functions is separable over k.

theorem isSeparable_globalSections_of_isProperVariety
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsProperVariety k f] [GeometricallyReduced f] :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    Algebra.IsSeparable k Γ(X, ⊤)

AlgebraicGeometry.isPurelyInseparable_globalSections_of_isProperVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/SmoothOverField/ProperVarietyGlobalSections.lean, line 94. The attribute's comment: “part (3)”.

Stacks Project, Tag 04L2, part (3). For a geometrically irreducible proper variety over a field k, the field of global functions is purely inseparable over k.

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

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.IsProperVariety · AlgebraicGeometry.IsSmoothVariety · AlgebraicGeometry.IsProjectiveVariety · AlgebraicGeometry.isProjectiveVariety_iff_isProjectiveMorphism · AlgebraicGeometry.isProjectiveVariety_iff_isProjective' · AlgebraicGeometry.IsQuasiProjectiveVariety · AlgebraicGeometry.isQuasiProjectiveVariety_iff_isHQuasiProjective · AlgebraicGeometry.IsAffine

Section33.27 Normalization#

Section 33.27 of the Stacks Project, Tag 0BXQ. 6 tags here are carried by 13 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BXR, a lemma

Tag 0BXR in the Stacks Project.

AlgebraicGeometry.exists_iso_normalizationSchemeOverField_coproduct_normal_irreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/NormalizationOverField.lean, line 81. The attribute's comment: “finite_normal_components”.

Stacks Project, Tag 0BXR. The normalization of a scheme locally of finite type over a field is a coproduct of normal irreducible schemes, each locally of finite type over the field via its induced structure morphism.

public theorem exists_iso_normalizationSchemeOverField_coproduct_normal_irreducible
    (k : Type u) [Field k] {X : Scheme.{u}} (p : X ⟶ Spec (.of k)) [LocallyOfFiniteType p] :
    ∃ (I : Type u) (Z : I → Scheme.{u})
      (_ : ∀ i, IrreducibleSpace (Z i)) (_ : ∀ i, IsNormal (Z i))
      (e : normalizationSchemeOverField k p ≅ ∐ Z),
      ∀ i, LocallyOfFiniteType (Sigma.ι Z i ≫ e.inv ≫ normalizationOverField k p ≫ p)

AlgebraicGeometry.isVariety_normalizationOverField, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/NormalizationOverField.lean, line 101. The attribute's comment: “normalization_of_variety”.

Stacks Project, Tag 0BXR. The normalization of a variety is a variety over the same field.

public instance isVariety_normalizationOverField (k : Type u) [Field k] {X : Scheme.{u}}
    (p : X ⟶ Spec (.of k)) [IsVariety k p] :
    IsVariety k (normalizationOverField k p ≫ p)

Declarations registered for the tag:

Tag 0GK4, a lemma

Tag 0GK4 in the Stacks Project.

AlgebraicGeometry.isProper_and_isProjective_normalizationOverField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/NormalizationProperProjective.lean, line 81.

Stacks Project, Tag 0GK4. Let k be a field, let X be a proper scheme over k and let ν : X^ν ⟶ X be the normalization morphism. Then X^ν is proper over k, and if X is projective over k then X^ν is projective over k.

Projectivity of X is an implication inside the conclusion: the properness assertion holds at the source's own hypotheses, with nothing assumed about projectivity. Over the affine base Spec k projectivity and H-projectivity agree ([Stacks, Tag 01WB]), so the implication may be read with either notion.

public theorem isProper_and_isProjective_normalizationOverField (k : Type u) [Field k]
    {X : Scheme.{u}} (p : X ⟶ Spec (.of k)) [IsProper p] :
    IsProper (normalizationOverField k p ≫ p) ∧
      (IsProjective p → IsProjective (normalizationOverField k p ≫ p))
Tag 0BXS, a lemma

Tag 0BXS in the Stacks Project.

AlgebraicGeometry.isFinite_fromNormalization_of_locallyOfFiniteType_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/NormalizationOverField.lean, line 145.

Stacks Project, Tag 0BXS. The relative normalization of a scheme locally of finite type over a field in a reduced scheme locally of finite type over the same field is finite, as soon as the morphism between them is quasi-compact.

public theorem isFinite_fromNormalization_of_locallyOfFiniteType_over_field
    (k : Type u) [Field k] {X Y : Scheme.{u}}
    (pX : X ⟶ Spec (.of k)) (pY : Y ⟶ Spec (.of k))
    (f : Y ⟶ X) (hf : f ≫ pX = pY)
    [LocallyOfFiniteType pX] [LocallyOfFiniteType pY]
    [QuasiCompact f] [IsReduced Y] :
    letI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian pY
    letI : QuasiSeparated f := QuasiSeparated.of_comp f (terminal.from X)
    IsFinite f.fromNormalization
Tag 0BXT, a lemma

Tag 0BXT in the Stacks Project.

AlgebraicGeometry.exists_isPurelyInseparable_isGeometricallyNormal_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometrically/NormalizationPurelyInseparable.lean, line 557.

Stacks Project, Tag 0BXT. Let k be a field and X an algebraic k-scheme. There is a finite purely inseparable extension k'/k such that the normalization of X_{k'} is geometrically normal over k'.

public theorem exists_isPurelyInseparable_isGeometricallyNormal_normalization
    (k : Type u) [Field k] {X : Scheme.{u}} (p : X ⟶ Spec (.of k))
    [LocallyOfFiniteType p] [QuasiCompact p] :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k') (_ : Module.Finite k k')
      (_ : IsPurelyInseparable k k'),
      IsGeometricallyNormal (normalizationOverField k' (pullback.fst (spectrumMap k k') p) ≫
        pullback.fst (spectrumMap k k') p)
Tag 0C3N, a lemma

Tag 0C3N in the Stacks Project.

AlgebraicGeometry.normalizationBaseChangeComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/Basic.lean, line 202. The attribute's comment: “canonical morphism”.

Stacks Project, Tag 0C3N. The canonical morphism from the normalization after extending the ground field to the base change of the original normalization.

noncomputable def normalizationBaseChangeComparison
    (X : Over (Spec (.of k))) [LocallyOfFiniteType X.hom] :
    let σ := Spec.map (CommRingCat.ofHom (algebraMap k K))
    let Y := (Over.pullback σ).obj X
    letI : LocallyOfFiniteType Y.hom := by
      dsimp [Y, σ]
      infer_instance
    let hX := finite_irreducibleComponents_of_locallyOfFiniteType k X.hom
    let hY := finite_irreducibleComponents_of_locallyOfFiniteType K Y.hom
    Y.left.normalizationScheme hY ⟶
      ((Over.pullback σ).obj
        (Over.mk (X.left.normalization hX ≫ X.hom))).left

AlgebraicGeometry.normalizationBaseChangeComparison_comp_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/Basic.lean, line 227. The attribute's comment: “projection to the original normalization”.

Stacks Project, Tag 0C3N. The projection of the comparison to the original normalization is the canonical map induced by functoriality of relative normalization. The map on generic-point residue spectra is over the projection X_K ⟶ X.

theorem normalizationBaseChangeComparison_comp_fst
    (X : Over (Spec (.of k))) [LocallyOfFiniteType X.hom] :
    let σ := Spec.map (CommRingCat.ofHom (algebraMap k K))
    let Y := (Over.pullback σ).obj X
    letI : LocallyOfFiniteType Y.hom := by
      dsimp [Y, σ]
      infer_instance
    let hX := finite_irreducibleComponents_of_locallyOfFiniteType k X.hom
    let hY := finite_irreducibleComponents_of_locallyOfFiniteType K Y.hom
    let fX := Scheme.fromGenericPointResidueFields X.left
    let fY := Scheme.fromGenericPointResidueFields Y.left
    letI : QuasiCompact fX := Scheme.quasiCompactFromGenericPointResidueFields X.left hX
    letI : QuasiSeparated fX := Scheme.quasiSeparatedFromGenericPointResidueFields X.left
    letI : QuasiCompact fY := Scheme.quasiCompactFromGenericPointResidueFields Y.left hY
    letI : QuasiSeparated fY := Scheme.quasiSeparatedFromGenericPointResidueFields Y.left
    ∃ (gY : Scheme.genericPointResidueSpectrum Y.left ⟶
        Scheme.genericPointResidueSpectrum X.left)
      (sq : gY ≫ fX = fY ≫ pullback.fst X.hom σ),
      normalizationBaseChangeComparison X ≫
          pullback.fst (X.left.normalization hX ≫ X.hom) σ =
        Scheme.Hom.normalizationMap fX fY gY (pullback.fst X.hom σ) sq

AlgebraicGeometry.normalizationBaseChangeComparison_comp_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/Basic.lean, line 258. The attribute's comment: “projection to the extended base field”.

Stacks Project, Tag 0C3N. The projection of the comparison to Spec K is the structural morphism of the normalized base change. Together with the preceding projection formula, this characterizes the map into the fibre product.

theorem normalizationBaseChangeComparison_comp_snd
    (X : Over (Spec (.of k))) [LocallyOfFiniteType X.hom] :
    let σ := Spec.map (CommRingCat.ofHom (algebraMap k K))
    let Y := (Over.pullback σ).obj X
    letI : LocallyOfFiniteType Y.hom := by
      dsimp [Y, σ]
      infer_instance
    let hX := finite_irreducibleComponents_of_locallyOfFiniteType k X.hom
    normalizationBaseChangeComparison X ≫
        pullback.snd (X.left.normalization hX ≫ X.hom) σ =
      Y.left.normalization (finite_irreducibleComponents_of_locallyOfFiniteType K Y.hom) ≫
        Y.hom

AlgebraicGeometry.normalizationBaseChangeComparison_comp_baseChangeNormalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/Basic.lean, line 277. The attribute's comment: “compatibility with normalization morphisms”.

Stacks Project, Tag 0C3N. The canonical comparison commutes with the normalization morphisms to the base-changed scheme.

theorem normalizationBaseChangeComparison_comp_baseChangeNormalization
    (X : Over (Spec (.of k))) [LocallyOfFiniteType X.hom] :
    let σ := Spec.map (CommRingCat.ofHom (algebraMap k K))
    let Y := (Over.pullback σ).obj X
    letI : LocallyOfFiniteType Y.hom := by
      dsimp [Y, σ]
      infer_instance
    normalizationBaseChangeComparison X ≫ baseChangeNormalization X =
      Y.left.normalization (finite_irreducibleComponents_of_locallyOfFiniteType K Y.hom)

AlgebraicGeometry.normalizationBaseChangeComparison_isUniversalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/UniversalHomeomorphism.lean, line 930. The attribute's comment: “universal homeomorphism”.

Stacks Project, Tag 0C3N. The normalization comparison for an arbitrary extension of fields is a universal homeomorphism.

The comparison lands in the reduction of its target (its source is reduced), and the resulting morphism d is integral and birational onto a scheme whose normalization morphism is a universal homeomorphism — because that scheme is the reduction of a base change of the normal scheme X.normalizationScheme.

theorem normalizationBaseChangeComparison_isUniversalHomeomorphism
    (X : Over (Spec (.of k))) [LocallyOfFiniteType X.hom] :
    UniversalHomeomorphism (normalizationBaseChangeComparison (k := k) (K := K) X)

AlgebraicGeometry.normalizationBaseChangeComparison_isIso_of_isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationBaseChange/UniversalHomeomorphism.lean, line 992. The attribute's comment: “separable extension”.

Stacks Project, Tag 0C3N. For a separable extension of fields, the normalization comparison is an isomorphism.

The target of the comparison is normal, by Tag 0C3M, so the universal property of the normalization of X_K produces a two-sided inverse.

theorem normalizationBaseChangeComparison_isIso_of_isSeparableExtension
    [Algebra.IsSeparableExtension k K] (X : Over (Spec (.of k))) [LocallyOfFiniteType X.hom] :
    IsIso (normalizationBaseChangeComparison (k := k) (K := K) X)
Tag 0C3P, a lemma

Tag 0C3P in the Stacks Project.

AlgebraicGeometry.isGeometricallyReducedAt_of_normalization_residueField_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/NormalizationSeparableResidue.lean, line 577. The attribute's comment: “geometrically reduced at the original point”.

A reduced one-dimensional point is geometrically reduced if all residue fields above it in the normalization are separable over the ground field.

public theorem isGeometricallyReducedAt_of_normalization_residueField_isSeparable
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (x : X)
    (hred : _root_.IsReduced (X.presheaf.stalk x))
    (hdim : ringKrullDim (X.presheaf.stalk x) = 1)
    (hsep :
      let Xnorm := normalizationSchemeOverField k f
      let ν := normalizationOverField k f
      ∀ x' : Xnorm, ν x' = x →
        letI : Algebra k (Xnorm.residueField x') :=
          ((Scheme.ΓSpecIso (.of k)).inv ≫ (ν ≫ f).appTop ≫ Xnorm.Γevaluation x').hom.toAlgebra
        Algebra.IsSeparableExtension k (Xnorm.residueField x')) :
    IsGeometricallyReducedAt f x

AlgebraicGeometry.isGeometricallyRegularAt_normalization_of_residueField_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/NormalizationSeparableResidue.lean, line 595. The attribute's comment: “geometrically regular on the normalization”.

Every point of the normalization above a one-dimensional point is geometrically regular when its residue field is separable over the ground field.

public theorem isGeometricallyRegularAt_normalization_of_residueField_isSeparable
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] (x : X)
    (hdim : ringKrullDim (X.presheaf.stalk x) = 1)
    (hsep :
      let Xnorm := normalizationSchemeOverField k f
      let ν := normalizationOverField k f
      ∀ x' : Xnorm, ν x' = x →
        letI : Algebra k (Xnorm.residueField x') :=
          ((Scheme.ΓSpecIso (.of k)).inv ≫ (ν ≫ f).appTop ≫ Xnorm.Γevaluation x').hom.toAlgebra
        Algebra.IsSeparableExtension k (Xnorm.residueField x')) :
    let Xnorm := normalizationSchemeOverField k f
    let ν := normalizationOverField k f
    ∀ x' : Xnorm, ν x' = x → IsGeometricallyRegularAt (ν ≫ f) x'
Sources
LeanAlgebraicGeometry.exists_iso_normalizationSchemeOverField_coproduct_normal_irreducible · AlgebraicGeometry.isVariety_normalizationOverField · AlgebraicGeometry.isFinite_normalizationOverField · AlgebraicGeometry.isDominant_normalizationOverField · AlgebraicGeometry.Scheme.isBirational_normalization · AlgebraicGeometry.Scheme.exists_normalizationScheme_iso_reduction · AlgebraicGeometry.isProper_and_isProjective_normalizationOverField · AlgebraicGeometry.isFinite_fromNormalization_of_locallyOfFiniteType_over_field

Section33.28 Groups of invertible functions#

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

Tag 04L4, a lemma

Tag 04L4 in the Stacks Project.

AlgebraicGeometry.fg_units_quotient_of_isOpenImmersion_into_properVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleFunctions/NormalModel.lean, line 44.

Stacks Project, Tag 04L4. Let k be an algebraically closed field, let Xbar be a proper variety over k, and let X be a normal open subscheme of Xbar. Then the group of invertible global functions on X, modulo the constants coming from k, is finitely generated.

The ambient proper variety may be replaced by its normalization, which is again a proper variety over k and is normal, and over the normal open X the normalization morphism is an isomorphism; so the statement follows from the case of a normal ambient variety.

theorem fg_units_quotient_of_isOpenImmersion_into_properVariety
    (k : Type u) [Field k] [IsAlgClosed k] {X Xbar : Scheme.{u}}
    (f : Xbar ⟶ Spec (.of k)) [IsProperVariety k f]
    (i : X ⟶ Xbar) [IsOpenImmersion i] [IsNormal X] :
    let φ : k →+* Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ (i ≫ f).appTop).hom
    Group.FG (Units Γ(X, ⊤) ⧸ (Units.map φ.toMonoidHom).range)
Tag 04L5, a lemma

Tag 04L5 in the Stacks Project.

AlgebraicGeometry.fg_units_quotient_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleFunctions/FiniteType.lean, line 178.

Stacks Project, Tag 04L5. Let k be an algebraically closed field and let X be an integral scheme locally of finite type over k. Then the group of invertible global functions on X modulo the constants coming from k is a finitely generated abelian group.

The normalization ν : X^ν ⟶ X is finite, X^ν is a normal integral scheme locally of finite type over k, and ν is dominant, hence injective on global sections; so the statement follows from the normal case.

theorem fg_units_quotient_of_locallyOfFiniteType (k : Type u) [Field k] [IsAlgClosed k]
    {X : Scheme.{u}} [IsIntegral X] (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] :
    let φ : k →+* Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom
    Group.FG (Γ(X, ⊤)ˣ ⧸ (Units.map φ.toMonoidHom).range)
Tag 04L6, a lemma

Tag 04L6 in the Stacks Project.

AlgebraicGeometry.fg_units_quotient_of_connectedSpace_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleFunctions/ConnectedReduced.lean, line 228.

Let k be an algebraically closed field and let X be a connected reduced scheme which is locally of finite type over k and has finitely many irreducible components. Then 𝒪^*(X)/k^*, the group of invertible global functions on X modulo the constants coming from k, is a finitely generated abelian group.

theorem fg_units_quotient_of_connectedSpace_of_isReduced (k : Type u) [Field k] [IsAlgClosed k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [ConnectedSpace X] [IsReduced X]
    [LocallyOfFiniteType f] (hX : (irreducibleComponents (X : Type u)).Finite) :
    Group.FG (Γ(X, ⊤)ˣ ⧸ (Units.map
      (((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom).toMonoidHom).range)
Tag 04MI, a lemma

Tag 04MI in the Stacks Project.

AlgebraicGeometry.integralClosure_globalSections_isField, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/GlobalSections.lean, line 49.

The integral closure of the ground field in the global sections of a connected reduced scheme over that field is a field.

public lemma integralClosure_globalSections_isField
    (k : Type u) [Field k] (X : Scheme.{u})
    (f : X ⟶ Spec (.of k)) [ConnectedSpace X] [IsReduced X] :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    IsField (integralClosure k Γ(X, ⊤))
Tag 04L7, a proposition

Tag 04L7 in the Stacks Project.

AlgebraicGeometry.fg_units_quotient_of_integrallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleFunctions/ConnectedReducedBaseChange.lean, line 234. The attribute's comment: “integral_closure_of_ground_field_is_ground_field”.

Stacks Project, Tag 04L7 under its condition (1). Let k be a field and let X be a connected reduced scheme, locally of finite type over k, with finitely many irreducible components, and assume that every global section of X integral over k is a constant — that is, that the integral closure of k in Γ(X, 𝒪_X) is k. Then the group of invertible global functions on X modulo the constants coming from k is a finitely generated abelian group.

The base change X̄ = X ×_k \bar k is surjective over X and has finitely many irreducible components; each of them with its reduced induced structure is integral and locally of finite type over \bar k, so Tag 04L5 applies to it. A unit of Γ(X, 𝒪_X) which is a constant from \bar k on every component of X̄ is killed by the product of the minimal polynomials of those constants over k, hence is integral over k, hence is a constant from k by the hypothesis.

Connectedness of X is one of the source's hypotheses and is kept here, but this proof does not use it: in the source connectedness is what forces the constants on the components to agree, whereas here condition (1) does that work.

theorem fg_units_quotient_of_integrallyClosed (k : Type u) [Field k] (X : Scheme.{u})
    (f : X ⟶ Spec (.of k)) [ConnectedSpace X] [IsReduced X] [LocallyOfFiniteType f]
    (hX : (irreducibleComponents (X : Type u)).Finite)
    (h1 : ∀ a : Γ(X, ⊤), (((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom).IsIntegralElem a →
      a ∈ Set.range ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom) :
    Group.FG (Γ(X, ⊤)ˣ ⧸ (Units.map
      (((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom).toMonoidHom).range)

AlgebraicGeometry.fg_units_quotient_of_rationalPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleFunctions/ConnectedReducedBaseChange.lean, line 438. The attribute's comment: “rational_point”.

Stacks Project, Tag 04L7 under its condition (2). Let k be a field and let X be a connected reduced scheme, locally of finite type over k, with finitely many irreducible components, and suppose X has a k-rational point. Then the group of invertible global functions on X modulo the constants coming from k is a finitely generated abelian group.

Condition (2) implies condition (1) by mem_range_of_isIntegralElem_of_rationalPoint, which is the source's own argument.

theorem fg_units_quotient_of_rationalPoint (k : Type u) [Field k] (X : Scheme.{u})
    (f : X ⟶ Spec (.of k)) [ConnectedSpace X] [IsReduced X] [LocallyOfFiniteType f]
    (hX : (irreducibleComponents (X : Type u)).Finite) (e : Spec (.of k) ⟶ X)
    (he : e ≫ f = 𝟙 (Spec (.of k))) :
    Group.FG (Γ(X, ⊤)ˣ ⧸ (Units.map
      (((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom).toMonoidHom).range)

AlgebraicGeometry.fg_units_quotient_of_geometricallyIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleFunctions/ConnectedReducedGeometricallyIntegral.lean, line 92. The attribute's comment: “geometrically_integral”.

Stacks Project, Tag 04L7 under its condition (3). Let k be a field and let X be a connected reduced scheme, locally of finite type over k, with finitely many irreducible components, and suppose X is geometrically integral over k. Then the group of invertible global functions on X modulo the constants coming from k is a finitely generated abelian group.

Condition (3) implies condition (1) by mem_range_of_isIntegralElem_of_geometricallyIntegral, and fg_units_quotient_of_integrallyClosed is the proposition under condition (1).

theorem fg_units_quotient_of_geometricallyIntegral (k : Type u) [Field k] (X : Scheme.{u})
    (f : X ⟶ Spec (.of k)) [ConnectedSpace X] [IsReduced X] [LocallyOfFiniteType f]
    (hX : (irreducibleComponents (X : Type u)).Finite) (hgi : GeometricallyIntegral f) :
    Group.FG (Γ(X, ⊤)ˣ ⧸ (Units.map
      (((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom).toMonoidHom).range)
Tag 04L8, a lemma

Tag 04L8 in the Stacks Project.

AlgebraicGeometry.integralClosure_globalSections_eq_bot_of_isAlgClosedIn_functionField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleFunctions/VarietyFieldConditions.lean, line 149. The attribute's comment: “condition (2) implies condition (1); the source omits this verification”.

Stacks Project, Tag 04L8, condition (2) implies condition (1). Let k be a field and let X be an integral scheme over k. If k is algebraically closed in the function field of X, then the integral closure of k in Γ(X, 𝒪_X) is k.

The germ map from the global sections to the stalk at the generic point is injective on an integral scheme, so this is the field-theoretic statement integralClosure_eq_bot_of_isAlgClosedIn_of_injective.

theorem integralClosure_globalSections_eq_bot_of_isAlgClosedIn_functionField
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [IsIntegral X] :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    letI : Algebra k X.functionField :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫
        X.presheaf.germ ⊤ (genericPoint X) trivial).hom.toAlgebra
    IsAlgClosedIn k X.functionField → integralClosure k Γ(X, ⊤) = ⊥

AlgebraicGeometry.integralClosure_globalSections_eq_bot_of_closedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleFunctions/VarietyFieldConditions.lean, line 176. The attribute's comment: “condition (4) implies condition (1); the source omits this verification”.

Stacks Project, Tag 04L8, condition (4) implies condition (1). Let k be a field and let X be a connected reduced scheme over k. Suppose that every field extension L of k which admits at each closed point x of X a ring map to the residue field κ(x) compatible with the maps out of k is already equal to k. Then the integral closure of k in Γ(X, 𝒪_X) is k.

The integral closure is a field by Tag 04MI, and evaluation at a point restricts to a ring map from it to the residue field there which is compatible with the maps out of k. So the hypothesis applies to it and makes it k.

theorem integralClosure_globalSections_eq_bot_of_closedPoints
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [ConnectedSpace X] [IsReduced X] :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    (∀ (L : Type u) [Field L] [Algebra k L],
      (∀ x ∈ closedPoints X, ∃ ι : L →+* X.residueField x,
        ∀ a : k, ι (algebraMap k L a) = X.Γevaluation x (algebraMap k Γ(X, ⊤) a)) →
      Function.Surjective (algebraMap k L)) →
    integralClosure k Γ(X, ⊤) = ⊥

AlgebraicGeometry.integralClosure_globalSections_eq_bot_of_geometricallyIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleFunctions/VarietyFieldConditions.lean, line 231. The attribute's comment: “condition (3) implies condition (1); the source omits this verification”.

Stacks Project, Tag 04L8, condition (3) implies condition (1). Let k be a field and let X be an integral scheme over k which is geometrically integral. Then the integral closure of k in Γ(X, 𝒪_X) is k.

Geometric integrality is geometric reducedness together with geometric irreducibility. The first says the function field is a separable extension of k (Tag 04KS) and the second says k is separably closed in the residue field at the generic point (Tag 054Q), which is the same field; so k is algebraically closed in the function field, which is condition (2).

theorem integralClosure_globalSections_eq_bot_of_geometricallyIntegral
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [IsIntegral X]
    (hgi : GeometricallyIntegral f) :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    integralClosure k Γ(X, ⊤) = ⊥

AlgebraicGeometry.fg_units_quotient_of_isVariety_of_field_conditions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleFunctions/VarietyFieldConditions.lean, line 279.

Stacks Project, Tag 04L8. Let k be a field and let X be a variety over k. Then the group of invertible global functions on X modulo the constants coming from k is finitely generated as soon as one of the following holds: the integral closure of k in Γ(X, 𝒪_X) is k; k is algebraically closed in the function field of X; X is geometrically integral over k; or no field extension of k other than k itself admits at every closed point a map to the residue field there compatible with the maps out of k.

A variety is integral, hence connected and reduced with a single irreducible component, and its structure morphism is locally of finite type, so Proposition 04L7 under its condition (1) — AlgebraicGeometry.fg_units_quotient_of_integrallyClosed — applies. Each of the other three conditions is turned into condition (1) by the three lemmas above.

theorem fg_units_quotient_of_isVariety_of_field_conditions
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsVariety k f] :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    (integralClosure k Γ(X, ⊤) = ⊥ ∨
      (letI : Algebra k X.functionField :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫
          X.presheaf.germ ⊤ (genericPoint X) trivial).hom.toAlgebra
       IsAlgClosedIn k X.functionField) ∨
      GeometricallyIntegral f ∨
      (∀ (L : Type u) [Field L] [Algebra k L],
        (∀ x ∈ closedPoints X, ∃ ι : L →+* X.residueField x,
          ∀ a : k, ι (algebraMap k L a) = X.Γevaluation x (algebraMap k Γ(X, ⊤) a)) →
        Function.Surjective (algebraMap k L))) →
    Group.FG (Γ(X, ⊤)ˣ ⧸ (Units.map
      (((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom).toMonoidHom).range)
Sources
LeanAlgebraicGeometry.fg_units_quotient_of_isOpenImmersion_into_properVariety · AlgebraicGeometry.fg_units_quotient_of_locallyOfFiniteType · AlgebraicGeometry.fg_units_quotient_of_connectedSpace_of_isReduced · AlgebraicGeometry.integralClosure_globalSections_isField · AlgebraicGeometry.fg_units_quotient_of_integrallyClosed · AlgebraicGeometry.fg_units_quotient_of_rationalPoint · AlgebraicGeometry.fg_units_quotient_of_geometricallyIntegral · AlgebraicGeometry.integralClosure_globalSections_eq_bot_of_isAlgClosedIn_functionField

Section33.29 Künneth formula, I#

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

Tag 0BED, a lemma

Tag 0BED in the Stacks Project.

Stacks.CechKunneth.kunnethIsoOfAffineDiagonal_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/CechKunneth/KunnethCanonical.lean, line 139. The attribute's comment: “the isomorphism is canonical: independent of the chosen finite affine covers, and on Cech classes given by the cup product of the pulled-back cocycles”.

The Künneth isomorphism is canonical: it is the isomorphism Stacks.CechKunneth.kunnethIsoOfCovers of any pair of finite affine coverings of X and Y, which on Čech classes is the Alexander–Whitney product of the pulled-back cocycles (Stacks.CechKunneth.kunnethIsoOfCovers_symm_lof_tmul).

theorem kunnethIsoOfAffineDiagonal_eq [CompactSpace X] [CompactSpace Y] (n : ℕ) :
    kunnethIsoOfAffineDiagonal k f g F G n = kunnethIsoOfCovers f g CX CY F G n

Stacks.CechKunneth.kunnethIsoOfAffineDiagonal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/CechKunneth/KunnethFormula.lean, line 376. The attribute's comment: “for X and Y quasi-compact with affine diagonal over a field k and F, G quasi-coherent: H^n(X x_k Y, pr_1^F (x) pr_2^G) is the direct sum over p + q = n of H^p(X, F) (x)_k H^q(Y, G), the isomorphism being the Cech-level cup product of pulled-back cocycles”.

The Künneth formula [Stacks, Tag 0BED]. For a field k, quasi-compact schemes X and Y over k with affine diagonal, a quasi-coherent 𝒪_X-module ℱ and a quasi-coherent 𝒪_Y-module 𝒢, Hⁿ(X ×_k Y, pr₁^*ℱ ⊗_{𝒪_{X ×_k Y}} pr₂^*𝒢) ≅ ⨁_{p + q = n} Hᵖ(X, ℱ) ⊗_k H^q(Y, 𝒢).

The isomorphism is the one of the source: computed on finite affine coverings 𝒰 of X and 𝒱 of Y (chosen by Stacks.CechKunneth.finiteAffineCover), it carries the class of the Alexander–Whitney product of the pullbacks of two Čech cocycles — the Čech form of pr₁^*α ∪ pr₂^*β, [Stacks, Tag 0BEE] — to α ⊗ β; see Stacks.CechKunneth.kunnethIsoOfCovers_symm_lof_tmul. The cohomology groups are Mathlib's right derived functors of global sections, regarded as k-modules through the structure morphisms (Stacks.CechKunneth.cohomologyK).

def kunnethIsoOfAffineDiagonal [CompactSpace X] [CompactSpace Y] (n : ℕ) :
    cohomologyK (pullback.fst f g ≫ f) (externalTensorProduct f g F G) n ≃ₗ[k]
      DirectSum {pq : ℕ × ℕ // pq.1 + pq.2 = n}
        (fun pq => cohomologyK f F pq.1.1 ⊗[k] cohomologyK g G pq.1.2)

AlgebraicGeometry.nonempty_kunnethIso_of_isAffineHom_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Varieties/KunnethAffineDiagonal.lean, line 96. The attribute's comment: “granted the derived global Künneth comparison of Tag 0FLQ, carried as HasKunnethDerivedData”.

The Künneth formula, I. For quasi-coherent modules F on X and G on Y, with X and Y quasi-compact schemes over a field k whose diagonals are affine, the cohomology of the external tensor product pr₁^*F ⊗ pr₂^*G on X ×_{Spec k} Y is the direct sum of the tensor products Hᵖ(X, F) ⊗_k Hᑫ(Y, G) over the pairs with p + q = n.

theorem nonempty_kunnethIso_of_isAffineHom_diagonal
    (hK : HasKunnethDerivedData.{u}) (k : Type u) [Field k] {X Y : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k))
    [CompactSpace X] [IsAffineHom (pullback.diagonal (terminal.from X))]
    [CompactSpace Y] [IsAffineHom (pullback.diagonal (terminal.from Y))]
    (F : X.Modules) (G : Y.Modules) [F.IsQuasicoherent] [G.IsQuasicoherent] (n : ℕ) :
    Nonempty
      (cohomologyOverField k (pullback.fst f g ≫ f) (externalTensorSheaf f g F G) n ≅
        ModuleCat.of k
          (⨁ pq : {pq : ℕ × ℕ // pq.1 + pq.2 = n},
            TensorProduct k (cohomologyOverField k f F pq.1.1)
              (cohomologyOverField k g G pq.1.2)))
Tag 0BEF, a lemma

Tag 0BEF in the Stacks Project.

AlgebraicGeometry.nonempty_kunnethIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Varieties/Kunneth.lean, line 382. The attribute's comment: “granted the derived global Künneth isomorphism of Tag 0FLQ, carried as KunnethDerivedData”.

The Künneth formula. For quasi-coherent modules on quasi-compact, quasi-separated schemes over a field, the cohomology of the external tensor product on X ×_k Y is the direct sum of the tensor products Hᵖ(X, F) ⊗_k Hᑫ(Y, G) over the pairs with p + q = n.

theorem nonempty_kunnethIso (k : Type u) [Field k] {X Y : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) (g : Y ⟶ Spec (.of k))
    [CompactSpace X] [QuasiSeparatedSpace X] [CompactSpace Y] [QuasiSeparatedSpace Y]
    (F : X.Modules) (G : Y.Modules) [F.IsQuasicoherent] [G.IsQuasicoherent] (n : ℕ)
    (d : KunnethDerivedData k f g F G) :
    Nonempty
      (cohomologyOverField k (pullback.fst f g ≫ f) (externalTensorSheaf f g F G) n ≅
        ModuleCat.of k
          (⨁ pq : {pq : ℕ × ℕ // pq.1 + pq.2 = n},
            TensorProduct k (cohomologyOverField k f F pq.1.1)
              (cohomologyOverField k g G pq.1.2)))

AlgebraicGeometry.KunnethQcqs.isIso_kunnethMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Varieties/KunnethQcqs.lean, line 481.

[Stacks, Tag 0BEF], the Künneth formula. Let k be a field, let X and Y be schemes over k and let F, G be quasi-coherent modules on X, Y. If X and Y are quasi-compact and quasi-separated, the canonical map

⨁_{p + q = n} Hᵖ(X, F) ⊗_k Hᑫ(Y, G) ⟶ Hⁿ(X ×_{Spec k} Y, pr₁^*F ⊗_{𝒪_{X ×_k Y}} pr₂^*G)

of AlgebraicGeometry.KunnethQcqs.kunnethMap is an isomorphism for every n.

theorem isIso_kunnethMap [CompactSpace Y] [QuasiSeparatedSpace Y] :
    IsIso (kunnethMap f g F G n)
Sources
LeanStacks.CechKunneth.kunnethIsoOfAffineDiagonal_eq · Stacks.CechKunneth.kunnethIsoOfAffineDiagonal · AlgebraicGeometry.nonempty_kunnethIso_of_isAffineHom_diagonal · AlgebraicGeometry.nonempty_kunnethIso · AlgebraicGeometry.KunnethQcqs.isIso_kunnethMap

Section33.30 Picard groups of varieties#

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

Tag 0CDX, a lemma

Tag 0CDX in the Stacks Project.

Stacks.AlgebraicGeometry.PicardBaseChange.exists_mulEquiv_globalSections_coherentMul_of_faithfullyFlat_trivialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardBaseChange/CoherentMul.lean, line 85. The attribute's comment: “multiplication is an isomorphism”.

Stacks Project, Tag 0CDX, the clause that the multiplication is an isomorphism. For a quasi-compact, quasi-separated scheme X over A, a faithfully flat ring map φ : A →+* B and an invertible 𝒪_X-module L whose pullback to X_B is trivial, the canonical multiplication

Γ(X, L) ⊗_{Γ(X, 𝒪_X)} Γ(X, L^{⊗ -1}) ⟶ Γ(X, 𝒪_X)

is an isomorphism. The multiplication is the coherent multiplication of Tag 01CU in degrees (1, -1), written out on pure tensors.

theorem exists_mulEquiv_globalSections_coherentMul_of_faithfullyFlat_trivialization
    {A B : Type u} [CommRing A] [CommRing B] (φ : A →+* B) (hφ : φ.FaithfullyFlat)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [CompactSpace X] [QuasiSeparatedSpace X]
    (L : X.Modules)
    [_root_.AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.property L]
    (hL : _root_.AlgebraicGeometry.SheafOfModules.IsTrivial
      (Limits.pullback f (Spec.map (CommRingCat.ofHom φ))).presheaf
      (Limits.pullback f (Spec.map (CommRingCat.ofHom φ))).ringCatSheaf.property
      ((Scheme.Modules.pullback
        (Limits.pullback.fst f (Spec.map (CommRingCat.ofHom φ)))).obj L)) :
    letI : Module Γ(X, ⊤)
        ((tensorPower X.presheaf X.ringCatSheaf.property L (-1)).val.obj (.op ⊤)) :=
      ((tensorPower X.presheaf X.ringCatSheaf.property L (-1)).val.obj (.op ⊤)).isModule
    ∃ e : TensorProduct Γ(X, ⊤) Γ(L, ⊤)
        ((tensorPower X.presheaf X.ringCatSheaf.property L (-1)).val.obj (.op ⊤))
        ≃ₗ[Γ(X, ⊤)] Γ(X, ⊤),
      ∀ s t, e (TensorProduct.tmul Γ(X, ⊤) s t) =
        (((tensorPowerCoherence X.presheaf X.ringCatSheaf.property L).mulIso 1 (-1)).hom.val.app
            (.op ⊤)).hom
          (((Stacks.SheafOfModules.TensorSheafification.toSheafify X.presheaf
            X.ringCatSheaf.property
            ((PresheafOfModules.tensorObj (O := X.presheaf)
              ((tensorPower X.presheaf X.ringCatSheaf.property L 1).val)
              ((tensorPower X.presheaf X.ringCatSheaf.property L (-1)).val)))).app (.op ⊤)).hom
            ((((tensorPowerOneIso X.presheaf X.ringCatSheaf.property L).inv.val.app
              (.op ⊤)).hom s) ⊗ₜ[Γ(X, ⊤)] t))

Stacks.AlgebraicGeometry.PicardBaseChange.invertible_globalSections_tensorInverse_of_faithfullyFlat_trivialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardBaseChange/InverseSections.lean, line 189. The attribute's comment: “global sections of the inverse sheaf”.

Stacks Project, Tag 0CDX, the clause about the global sections of the inverse sheaf. For a quasi-compact, quasi-separated scheme X over A, a faithfully flat ring map φ : A →+* B and an invertible 𝒪_X-module L whose pullback to X_B is trivial, the global sections Γ(X, L^{⊗ -1}) of the inverse tensor power form an invertible module over the global functions Γ(X, 𝒪_X).

theorem invertible_globalSections_tensorInverse_of_faithfullyFlat_trivialization
    {A B : Type u} [CommRing A] [CommRing B] (φ : A →+* B) (hφ : φ.FaithfullyFlat)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [CompactSpace X] [QuasiSeparatedSpace X]
    (L : X.Modules)
    [hinv : IsInvertible X.presheaf X.ringCatSheaf.property L]
    (hL : IsTrivial
      (Limits.pullback f (Spec.map (CommRingCat.ofHom φ))).presheaf
      (Limits.pullback f (Spec.map (CommRingCat.ofHom φ))).ringCatSheaf.property
      ((Scheme.Modules.pullback
        (Limits.pullback.fst f (Spec.map (CommRingCat.ofHom φ)))).obj L)) :
    letI : Module Γ(X, ⊤)
        ((tensorPower X.presheaf X.ringCatSheaf.property L (-1)).val.obj (.op ⊤)) :=
      ((tensorPower X.presheaf X.ringCatSheaf.property L (-1)).val.obj (.op ⊤)).isModule
    Module.Invertible Γ(X, ⊤)
      ((tensorPower X.presheaf X.ringCatSheaf.property L (-1)).val.obj (.op ⊤))

Stacks.AlgebraicGeometry.PicardBaseChange.invertible_globalSections_of_faithfullyFlat_trivialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardBaseChange/Sections.lean, line 157. The attribute's comment: “global sections of the sheaf”.

Stacks Project, Tag 0CDX, the clause about the global sections of the sheaf. For a quasi-compact, quasi-separated scheme X over A, a faithfully flat ring map φ : A →+* B and an invertible 𝒪_X-module L whose pullback to X_B is trivial, the global sections Γ(X, L) form an invertible module over the global functions Γ(X, 𝒪_X).

theorem invertible_globalSections_of_faithfullyFlat_trivialization
    {A B : Type u} [CommRing A] [CommRing B] (φ : A →+* B) (hφ : φ.FaithfullyFlat)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [CompactSpace X] [QuasiSeparatedSpace X]
    (L : X.Modules)
    [hinv : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.property L]
    (hL : AlgebraicGeometry.SheafOfModules.IsTrivial
      (Limits.pullback f (Spec.map (CommRingCat.ofHom φ))).presheaf
      (Limits.pullback f (Spec.map (CommRingCat.ofHom φ))).ringCatSheaf.property
      ((Scheme.Modules.pullback
        (Limits.pullback.fst f (Spec.map (CommRingCat.ofHom φ)))).obj L)) :
    Module.Invertible Γ(X, ⊤) Γ(L, ⊤)
Tag 0CDY, a lemma

Tag 0CDY in the Stacks Project.

Stacks.AlgebraicGeometry.PicardBaseChange.injective_picardPullback_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardBaseChange/Injectivity.lean, line 222.

Stacks Project, Tag 0CDY. Let A → B be a faithfully flat ring map and let X be a scheme over A which is quasi-compact and quasi-separated and whose ring of global functions H⁰(X, 𝒪_X) is semi-local. Then the pullback map Pic(X) → Pic(X_B) is injective.

theorem injective_picardPullback_of_faithfullyFlat
    {A B : Type u} [CommRing A] [CommRing B] (φ : A →+* B) (hφ : φ.FaithfullyFlat)
    (f : X ⟶ Spec (.of A)) [CompactSpace X] [QuasiSeparatedSpace X]
    [Finite (MaximalSpectrum Γ(X, ⊤))] :
    Function.Injective (Stacks.Picard.schemePullbackClassHom
      (Limits.pullback.fst f (Spec.map (CommRingCat.ofHom φ))))

Stacks.AlgebraicGeometry.PicardBaseChange.injective_schemePullbackClass_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardBaseChange/PuncturedSpectrumCompletion.lean, line 219.

Stacks Project, Tag 0CDY. Let A → B be faithfully flat and let X be a quasi-compact, quasi-separated scheme over A whose ring of global functions is semilocal. Then pullback to the base change X_B is injective on Picard groups.

theorem injective_schemePullbackClass_of_faithfullyFlat
    {R S : Type u} [CommRing R] [CommRing S] (φ : R →+* S) (hφ : φ.FaithfullyFlat)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [CompactSpace X] [QuasiSeparatedSpace X]
    [Finite (MaximalSpectrum Γ(X, ⊤))] :
    Function.Injective (Stacks.Picard.schemePullbackClass
      (pullback.fst f (Spec.map (CommRingCat.ofHom φ))))
Tag 0CC5, a lemma

Tag 0CC5 in the Stacks Project.

Stacks.AlgebraicGeometry.PicardBaseChange.injective_picardPullback_of_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardBaseChange/Injectivity.lean, line 293. The attribute's comment: “The lemma proper; the parenthetical sufficient condition dim_k H⁰(X, 𝒪_X) < ∞ for semi-locality is injective_picardPullback_of_finiteDimensional”.

Stacks Project, Tag 0CC5. Let k'/k be a field extension and let X be a scheme over k such that (1) X is quasi-compact and quasi-separated, and (2) R = H⁰(X, 𝒪_X) is semi-local. Then the pullback map Pic(X) → Pic(X_{k'}) is injective.

theorem injective_picardPullback_of_fieldExtension
    {k k' : Type u} [Field k] [Field k'] (φ : k →+* k')
    (f : X ⟶ Spec (.of k)) [CompactSpace X] [QuasiSeparatedSpace X]
    [Finite (MaximalSpectrum Γ(X, ⊤))] :
    Function.Injective (Stacks.Picard.schemePullbackClassHom
      (Limits.pullback.fst f (Spec.map (CommRingCat.ofHom φ))))

Stacks.AlgebraicGeometry.PicardBaseChange.injective_picardPullback_of_finiteDimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardBaseChange/Injectivity.lean, line 306. The attribute's comment: “The parenthetical sufficient condition dim_k H⁰(X, 𝒪_X) < ∞ for hypothesis (2); the lemma proper is injective_picardPullback_of_fieldExtension”.

Stacks Project, Tag 0CC5 with its parenthetical hypothesis: hypothesis (2) holds as soon as dim_k H⁰(X, 𝒪_X) is finite, H⁰(X, 𝒪_X) being then Artinian and hence semi-local.

theorem injective_picardPullback_of_finiteDimensional
    {k k' : Type u} [Field k] [Field k'] (φ : k →+* k')
    (f : X ⟶ Spec (.of k)) [CompactSpace X] [QuasiSeparatedSpace X]
    (hfd : letI := globalSectionsAlgebra f; FiniteDimensional k Γ(X, ⊤)) :
    Function.Injective (Stacks.Picard.schemePullbackClassHom
      (Limits.pullback.fst f (Spec.map (CommRingCat.ofHom φ))))
Tag 0CDP, an example

Tag 0CDP in the Stacks Project.

Stacks.ProjectiveLine.subsingleton_picardGroup_basicOpen_map_of_residueFieldAlgHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveLine/PicardComplement.lean, line 289. The attribute's comment: “clause (6): after enlarging k to a field k' admitting a k-embedding κ(t) → k', the Picard group of the base change of X = ℙ¹_k ∖ {t} is trivial”.

The Picard group of ℙ¹_k ∖ {t} dies over a field embedding κ(t). Let t = V₊(f) be the closed point of ℙ¹_k cut out by a homogeneous irreducible form f not divisible by T₁, and let X = ℙ¹_k ∖ {t}. If a field k' admits a k-embedding of the residue field κ(t), then Pic(X_{k'}) = 0.

theorem subsingleton_picardGroup_basicOpen_map_of_residueFieldAlgHom
    {k k' : Type u} [Field k] [Field k'] [Algebra k k'] {d : ℕ}
    {f : MvPolynomial (Fin 2) k} (hf : f.IsHomogeneous d) (hirr : Irreducible f)
    (hX : ¬ MvPolynomial.X (1 : Fin 2) ∣ f)
    [(Ideal.span {dehomogenize k f}).IsPrime]
    (ψ : (Ideal.span {dehomogenize k f}).ResidueField →ₐ[k] k') :
    Subsingleton (PicardGroup
      (Proj.basicOpen (grading k') (MvPolynomial.map (algebraMap k k') f)).toScheme.presheaf
      (Proj.basicOpen (grading k')
        (MvPolynomial.map (algebraMap k k') f)).toScheme.ringCatSheaf.2)

Stacks.ProjectiveLine.subsingleton_picardGroup_basicOpen_map_of_X_one_dvd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveLine/PicardComplement.lean, line 350. The attribute's comment: “clause (6) at the point at infinity t = V₊(T₁), i.e. for T₁ ∣ f: the Picard group of the base change of X = ℙ¹_k ∖ {t} to an arbitrary field extension k' is trivial, with no hypothesis on k'”.

The Picard group of ℙ¹_k ∖ {V₊(T₁)} dies over every field extension. If T₁ divides f, then the Picard group of the base change of D₊(f) to any field extension k' of k is trivial.

theorem subsingleton_picardGroup_basicOpen_map_of_X_one_dvd
    {k k' : Type u} [Field k] [Field k'] [Algebra k k']
    {f : MvPolynomial (Fin 2) k} (hdvd : MvPolynomial.X (1 : Fin 2) ∣ f) :
    Subsingleton (PicardGroup
      (Proj.basicOpen (grading k') (MvPolynomial.map (algebraMap k k') f)).toScheme.presheaf
      (Proj.basicOpen (grading k')
        (MvPolynomial.map (algebraMap k k') f)).toScheme.ringCatSheaf.2)

Stacks.ProjectiveLine.subsingleton_picardGroup_basicOpen_map_of_residueFieldAlgHom_of_isPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveLine/PicardComplement.lean, line 382. The attribute's comment: “clause (6) with the extra hypothesis t ≠ V₊(T₁) removed from the statement: for a closed point t of ℙ¹_k presented in the standard chart, a k-embedding κ(t) → k' makes the Picard group of the base change of X = ℙ¹_k ∖ {t} trivial”.

The Picard group of ℙ¹_k ∖ {t} dies over a field embedding κ(t). Let t = V₊(f) be the closed point of ℙ¹_k cut out by a homogeneous irreducible form f, with κ(t) the residue field of the prime ideal generated by the dehomogenization of f, and let X = ℙ¹_k ∖ {t}. If a field k' admits a k-embedding of κ(t), then Pic(X_{k'}) = 0.

theorem subsingleton_picardGroup_basicOpen_map_of_residueFieldAlgHom_of_isPrime
    {k k' : Type u} [Field k] [Field k'] [Algebra k k'] {d : ℕ}
    {f : MvPolynomial (Fin 2) k} (hf : f.IsHomogeneous d) (hirr : Irreducible f)
    [(Ideal.span {dehomogenize k f}).IsPrime]
    (ψ : (Ideal.span {dehomogenize k f}).ResidueField →ₐ[k] k') :
    Subsingleton (PicardGroup
      (Proj.basicOpen (grading k') (MvPolynomial.map (algebraMap k k') f)).toScheme.presheaf
      (Proj.basicOpen (grading k')
        (MvPolynomial.map (algebraMap k k') f)).toScheme.ringCatSheaf.2)

Stacks.ProjectiveLine.surjective_complementRestrictHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveLine/PicardQuotient.lean, line 207. The attribute's comment: “the displayed surjection ℤ = Pic(ℙ¹_k) → Pic(X) for X = ℙ¹_k ∖ {t}, by Tag 0BD9 for the surjectivity and Tag 0BXJ for the identification of Pic(ℙ¹_k) with ℤ”.

The restriction map ℤ = Pic(ℙ¹_k) → Pic(X) is surjective, for X = ℙ¹_k ∖ V₊(f).

theorem surjective_complementRestrictHom : Function.Surjective (complementRestrictHom f)

Stacks.ProjectiveLine.surjective_complementZModHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveLine/PicardQuotient.lean, line 239. The attribute's comment: “the computation Pic(X) = ℤ/dℤ for X = ℙ¹_k ∖ {t}, surjectivity half: the displayed map factors through ℤ/dℤ by a surjection, d = deg f = [κ(t) : k]”.

The map ℤ/dℤ → Pic(X) is surjective, for X = ℙ¹_k ∖ V₊(f) and d = deg f.

theorem surjective_complementZModHom {d : ℕ} (hf : f ∈ grading k d) :
    Function.Surjective (complementZModHom f hf)

Stacks.ProjectiveLine.nsmul_finrank_residueField_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveLine/PicardQuotient.lean, line 249. The attribute's comment: “Pic(X) is killed by d = [κ(t) : k] for X = ℙ¹_k ∖ {t}, the residue degree read in the standard chart”.

Pic(X) is killed by d = [κ(t) : k], the residue degree of the removed closed point t = V₊(f) of ℙ¹_k.

theorem nsmul_finrank_residueField_eq_zero {d : ℕ} {f : MvPolynomial (Fin 2) k}
    (hf : f.IsHomogeneous d) (hirr : Irreducible f)
    (hX : ¬ MvPolynomial.X (1 : Fin 2) ∣ f)
    [(Ideal.span {dehomogenize k f}).IsPrime]
    (c : (Proj.basicOpen (grading k) f).toScheme.picardGroup) :
    Module.finrank k (Ideal.span {dehomogenize k f}).ResidueField • c = 0

Stacks.ProjectiveLine.complementZModEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveLine/PicardQuotient.lean, line 332. The attribute's comment: “the computation Pic(X) = ℤ/dℤ for X = ℙ¹_k ∖ {t}, as the isomorphism ℤ/dℤ ≃+ Pic(X) induced by the displayed surjection, d = deg f = [κ(t) : k]”.

Pic(X) = ℤ/dℤ. Let t = V₊(f) be the closed point of ℙ¹_k cut out by a homogeneous irreducible form f of degree d, and let X = ℙ¹_k ∖ {t}. The surjection ℤ = Pic(ℙ¹_k) ↠ Pic(X) has kernel dℤ, so it induces an isomorphism ℤ/dℤ ≃ Pic(X).

def complementZModEquiv {d : ℕ} {f : MvPolynomial (Fin 2) k}
    (hf : f.IsHomogeneous d) (hirr : Irreducible f) :
    ZMod d ≃+ (Proj.basicOpen (grading k) f).toScheme.picardGroup

Stacks.ProjectiveLine.nontrivial_picardGroup_basicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveLine/PicardQuotient.lean, line 343. The attribute's comment: “Pic(X) ≠ 0 for X = ℙ¹_k ∖ {t} when t is not a k-rational point, i.e. when d = [κ(t) : k] > 1; this is what makes the example a counterexample to Tag 0CC5”.

Pic(X) ≠ 0 for a non-rational point. If the closed point t = V₊(f) of ℙ¹_k has degree d > 1, equivalently is not a k-rational point, then the Picard group of X = ℙ¹_k ∖ {t} is nonzero.

theorem nontrivial_picardGroup_basicOpen {d : ℕ} {f : MvPolynomial (Fin 2) k}
    (hf : f.IsHomogeneous d) (hirr : Irreducible f) (hd : 2 ≤ d) :
    Nontrivial (Proj.basicOpen (grading k) f).toScheme.picardGroup
Tag 0BEH, a lemma

Tag 0BEH in the Stacks Project.

Stacks.PicardGroup.nonempty_iso_pullback_sectionOfPoint_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardGroup/RationalEquivalenceNormalVariety.lean, line 260. The attribute's comment: “k a field, X a normal variety over k, U an open of affine n-space over k with two k-rational points: an invertible module on X ×_{Spec k} U has isomorphic restrictions to X × p and X × q”.

Stacks Project, Tag 0BEH. Let k be a field, X a normal variety over k, and U ⊆ 𝔸^n_k an open subscheme with k-rational points p, q ∈ U(k). For every invertible module ℒ on X ×_{Spec k} U the restrictions ℒ|_{X × p} and ℒ|_{X × q} are isomorphic.

Nothing is assumed beyond the source's hypotheses. The appeal to [Stacks, Tag 0BD7] at the projection pr : X ×_{Spec k} U → X is made through Stacks.InvertiblePullback.exists_isInvertible_pullback_iso_of_isTrivial_genericFiber_of_flat, whose hypotheses hold here: pr is the base change of U → Spec k, which is flat (an open immersion followed by the structure morphism of affine space) and, n being finite, locally of finite type; X is integral, normal and — being of finite type over a field — locally Noetherian, and so is X ×_{Spec k} U; and every fibre of pr is integral by Stacks.PicardGroup.isIntegral_fiber_fst. Its remaining hypothesis, triviality of ℒ on the generic fibre, is the one Stacks.PicardGroup.nonempty_iso_pullback_sectionOfPoint discharges from [Stacks, Tag 0BDA].

theorem nonempty_iso_pullback_sectionOfPoint_of_finite (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsVariety k f] [IsNormal X] {n : Type u} [Finite n]
    (U : (𝔸(n; Spec (.of k))).Opens) (p q : Spec (.of k) ⟶ U.toScheme)
    (hp : p ≫ openAffineSpaceOver k U = 𝟙 (Spec (.of k)))
    (hq : q ≫ openAffineSpaceOver k U = 𝟙 (Spec (.of k)))
    (L : (Limits.pullback f (openAffineSpaceOver k U)).Modules)
    [hL : IsInvertible (Limits.pullback f (openAffineSpaceOver k U)).presheaf
      (structureSheafRing
        (Limits.pullback f (openAffineSpaceOver k U)).toRingedSpace).property L] :
    Nonempty ((Scheme.Modules.pullback (sectionOfPoint f p hp)).obj L ≅
      (Scheme.Modules.pullback (sectionOfPoint f q hq)).obj L)
Sources
LeanStacks.AlgebraicGeometry.PicardBaseChange.exists_mulEquiv_globalSections_coherentMul_of_faithfullyFlat_trivialization · Stacks.AlgebraicGeometry.PicardBaseChange.invertible_globalSections_tensorInverse_of_faithfullyFlat_trivialization · Stacks.AlgebraicGeometry.PicardBaseChange.invertible_globalSections_of_faithfullyFlat_trivialization · Stacks.AlgebraicGeometry.PicardBaseChange.injective_picardPullback_of_faithfullyFlat · Stacks.AlgebraicGeometry.PicardBaseChange.injective_schemePullbackClass_of_faithfullyFlat · Stacks.AlgebraicGeometry.PicardBaseChange.injective_picardPullback_of_fieldExtension · Stacks.AlgebraicGeometry.PicardBaseChange.injective_picardPullback_of_finiteDimensional · Stacks.ProjectiveLine.subsingleton_picardGroup_basicOpen_map_of_residueFieldAlgHom

Section33.31 Uniqueness of base field#

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

Tag 04MK, a proposition

Tag 04MK in the Stacks Project.

AlgebraicGeometry.integralClosure_baseField_toSubring_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/BaseFieldUniqueness.lean, line 479.

Stacks Project, Tag 04MK (Uniqueness of base field). Let X be a reduced connected scheme which is locally of finite type over a field k₁ and also over a field k₂. Then the integral closure of k₁ in Γ(X, 𝒪_X) and the integral closure of k₂ in Γ(X, 𝒪_X) are the same subring of Γ(X, 𝒪_X).

Each inclusion is isIntegralElem_of_isIntegralElem: locally of finite type over a field makes X locally Noetherian, hence covered by quasi-compact connected opens, and on such an open the two closures agree because Tag 04L7 makes the invertible global functions modulo either closure finitely generated, which by the Hilbert Nullstellensatz forces each closure to be finite over their intersection. A monic polynomial over k₂ killing a section on one such open then kills it globally, since its value is everywhere locally zero or a unit — the closures are fields by Tag 04MI — so its nonvanishing locus is clopen and X is connected.

theorem integralClosure_baseField_toSubring_eq (k₁ k₂ : Type u) [Field k₁] [Field k₂]
    (X : Scheme.{u}) (a : X ⟶ Spec (.of k₁)) (b : X ⟶ Spec (.of k₂))
    [LocallyOfFiniteType a] [LocallyOfFiniteType b] [IsReduced X] [ConnectedSpace X] :
    letI : Algebra k₁ Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k₁)).inv ≫ a.appTop).hom.toAlgebra
    letI : Algebra k₂ Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k₂)).inv ≫ b.appTop).hom.toAlgebra
    (integralClosure k₁ Γ(X, ⊤)).toSubring = (integralClosure k₂ Γ(X, ⊤)).toSubring
Sources
LeanAlgebraicGeometry.integralClosure_baseField_toSubring_eq

Section33.32 Automorphisms#

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

Tag 0G05, a lemma

Tag 0G05 in the Stacks Project.

AlgebraicGeometry.eq_id_of_isIso_of_eq_on_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Automorphisms/PointwiseTrivialAut.lean, line 88. The attribute's comment: “clause (2) in full: an automorphism over k of a reduced scheme locally of finite type over k fixing every point of the underlying space is the identity when every irreducible component has positive dimension. No hypothesis on the base field and nothing carried. The automorphism hypothesis is necessary — for an endomorphism the statement fails over a finite field, by AlgHom.exists_comap_eq_ne_id_of_finite_field — which is why this stands beside AlgebraicGeometry.eq_id_of_eq_on_points, the endomorphism statement with the base field in a disjunctive hypothesis”.

Stacks Project, Tag 0G05, clause (2). Let X be a reduced scheme locally of finite type over a field k and let f : X ⟶ X be an automorphism over k which induces the identity map on the underlying topological space of X. If every irreducible component of X has positive dimension then f is the identity.

Nothing is carried and no hypothesis is put on k. The source's two cases are both handled by the curve case AlgebraicGeometry.eq_id_of_eq_on_points_of_isCurve, to which AlgebraicGeometry.eq_id_of_affine_curve_restrictions reduces the statement: an integral affine curve over k is a curve in the sense of AlgebraicGeometry.IsCurve, being integral, separated and of finite type over k of dimension one.

theorem eq_id_of_isIso_of_eq_on_points {k : Type u} [Field k] {X : Scheme.{u}} [IsReduced X]
    (p : X ⟶ Spec (.of k)) [LocallyOfFiniteType p] (f : X ⟶ X) [IsIso f] (hf : f ≫ p = p)
    (hpoints : ∀ x : X, f x = x)
    (hdim : ∀ Z ∈ irreducibleComponents X, 0 < topologicalKrullDim Z) :
    f = 𝟙 X

AlgebraicGeometry.exists_iso_pullback_of_isIso_of_eq_on_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Automorphisms/PointwiseTrivialAut.lean, line 232. The attribute's comment: “clause (1) in full: every module on a reduced scheme of finite type over k is isomorphic to its pullback along an automorphism over k fixing every point of the underlying space. No hypothesis on the base field, nothing carried, and the module is arbitrary rather than coherent. The connected components are clopen and finite in number; on each of them clause (2) applies, or the component is the spectrum of a finite extension of k and the twist of a module is isomorphic to it through a basis; the isomorphisms glue over the pairwise disjoint cover”.

Stacks Project, Tag 0G05, clause (1). Let X be a reduced scheme of finite type over a field k and let f : X ⟶ X be an automorphism over k which induces the identity map on the underlying topological space of X. Then every 𝒪_X-module is isomorphic to its pullback along f.

Nothing is carried and no hypothesis is put on k; coherence of the module is not needed. The source's proof is "part (1) follows from part (2) and the fact that the connected components of X of dimension 0 are spectra of fields": the scheme has finitely many connected components, each clopen, on each of them clause (2) applies unless it is a one-point scheme, where a module is isomorphic to its twist through a basis, and the isomorphisms glue because the components are pairwise disjoint.

theorem exists_iso_pullback_of_isIso_of_eq_on_points {k : Type u} [Field k] {X : Scheme.{u}}
    (p : X ⟶ Spec (.of k))
    [LocallyOfFiniteType p] [QuasiCompact p] [IsReduced X] (f : X ⟶ X) [IsIso f]
    (hf : f ≫ p = p) (hpoints : ∀ x : X, f x = x) (F : X.Modules) :
    Nonempty ((Scheme.Modules.pullback f).obj F ≅ F)
Sources
LeanAlgebraicGeometry.eq_id_of_isIso_of_eq_on_points · AlgebraicGeometry.exists_iso_pullback_of_isIso_of_eq_on_points

Section33.33 Euler characteristics#

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

Tag 0BEJ, a definition

Tag 0BEJ in the Stacks Project.

AlgebraicGeometry.eulerCharacteristic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/EulerCharacteristic.lean, line 49. References: EGA III (2.5.1), “field base”.

The alternating sum of the dimensions of the cohomology groups of a coherent sheaf on a proper scheme over a field.

public noncomputable def eulerCharacteristic (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] (F : X.Modules) [F.IsCoherent] : ℤ
Tag 08AA, a lemma

Tag 08AA in the Stacks Project.

AlgebraicGeometry.eulerCharacteristic_add_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/AdditivityUnconditional.lean, line 88. References: EGA III (2.5.2), “special case”.

[Stacks, Tag 08AA]. For a short exact sequence 0 ⟶ ℱ₁ ⟶ ℱ₂ ⟶ ℱ₃ ⟶ 0 of coherent modules on a scheme proper over a field, χ(X, ℱ₂) = χ(X, ℱ₁) + χ(X, ℱ₃).

The finiteness input [Stacks, Tag 02O6], which StacksFrontier/AlgebraicGeometry/Variety/EulerChar/CoherentFiniteness.lean carried as an explicit hypothesis hfin : CohomologyFiniteDimensionalOverField, is supplied here by AlgebraicGeometry.finiteDimensional_cohomologyOverField_of_isProper; the vanishing input [Stacks, Tag 01XJ] is discharged inside AlgebraicGeometry.eulerCharacteristic_add_of_shortExact_of_finiteDimensional'.

public theorem eulerCharacteristic_add_of_shortExact (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] {S : ShortComplex X.Modules} (hS : S.ShortExact)
    [S.X₁.IsCoherent] [S.X₂.IsCoherent] [S.X₃.IsCoherent] :
    eulerCharacteristic k f S.X₂ =
      eulerCharacteristic k f S.X₁ + eulerCharacteristic k f S.X₃
Tag 0AYT, a lemma

Tag 0AYT in the Stacks Project.

AlgebraicGeometry.nonempty_generatingSections_of_support_dim_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/GlobalGeneration/ZeroDimensionalSupport.lean, line 270. The attribute's comment: “(1), ℱ is generated by global sections. Stated for a locally Noetherian X, which is weaker than the clause's X proper over a field k (properness gives IsLocallyNoetherian via LocallyOfFiniteType.isLocallyNoetherian), so the clause follows by instantiation”.

A coherent sheaf with support of dimension at most zero on a locally Noetherian scheme is generated by global sections.

This is also clause (1) of Stacks 0AYT, in a form more general than that clause states it: Stacks 0AYT takes X proper over a field k, which gives IsLocallyNoetherian X through LocallyOfFiniteType.isLocallyNoetherian, so the condition here is strictly weaker than the clause's and the clause follows by instantiation.

public theorem nonempty_generatingSections_of_support_dim_le_zero
    {X : Scheme.{u}} [IsLocallyNoetherian X] (F : X.Modules) [F.IsCoherent]
    (hF : topologicalKrullDim (SheafOfModules.supp F) ≤ 0) :
    Nonempty F.GeneratingSections

AlgebraicGeometry.suppStalkDirectSumAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ZeroDimensionalSupport/Vanishing.lean, line 340. The attribute's comment: “(2), at the Γ(ℱ, ⊤) spelling of H⁰(X, ℱ); the H⁰ spelling is AlgebraicGeometry.cohomologyOverFieldZeroEquivDirectSumSuppStalk”.

[Stacks, Tag 0AYT] (2): H⁰(X, ℱ) is the direct sum of the stalks of ℱ along its support. For f : X ⟶ Spec k proper and ℱ coherent on X with dim (supp ℱ) ≤ 0,

Γ(X, ℱ) ≅ ⨁_{x ∈ Supp ℱ} ℱ_x

as abelian groups, the isomorphism being the one assembled from the germ maps (AlgebraicGeometry.suppGermHom) followed by the identification of the product of a finite family with its direct sum.

noncomputable def suppStalkDirectSumAddEquiv :
    Γ(F, ⊤) ≃+ ⨁ x : ↥(_root_.SheafOfModules.supp F), (Scheme.Modules.presheaf F).stalk x.1

AlgebraicGeometry.cohomologyOverFieldZeroEquivDirectSumSuppStalk, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ZeroDimensionalSupport/Vanishing.lean, line 362. The attribute's comment: “(2), at the H⁰(X, ℱ) spelling; the additive structure of the same decomposition is on AlgebraicGeometry.suppStalkDirectSumAddEquiv”.

[Stacks, Tag 0AYT] (2), read at H⁰(X, ℱ). Composing AlgebraicGeometry.suppStalkDirectSumAddEquiv with the identification of degree-zero cohomology with global sections gives

H⁰(X, ℱ) = ⨁_{x ∈ Supp ℱ} ℱ_x.

It is an Equiv rather than an additive equivalence because AlgebraicGeometry.cohomologyOverFieldZeroEquivSections, the only identification of H⁰(X, ℱ) with Γ(ℱ, ⊤) this library has, is one: Γ(ℱ, ⊤) carries no Module k instance and the comparison is stated at the level of types. The additive structure of the decomposition is in AlgebraicGeometry.suppStalkDirectSumAddEquiv.

noncomputable def cohomologyOverFieldZeroEquivDirectSumSuppStalk :
    (cohomologyOverField k f F 0 : Type u) ≃
      ⨁ x : ↥(_root_.SheafOfModules.supp F), (Scheme.Modules.presheaf F).stalk x.1

AlgebraicGeometry.isZero_cohomologyOverField_of_topologicalKrullDim_supp_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ZeroDimensionalSupport/Vanishing.lean, line 378. The attribute's comment: “(3)”.

[Stacks, Tag 0AYT] (3): the higher cohomology of a coherent module whose support has dimension at most zero vanishes. For f : X ⟶ Spec k proper and ℱ coherent on X with dim (supp ℱ) ≤ 0, the k-vector space Hⁱ(X, ℱ) is zero for every i > 0.

The module is the direct image of a coherent module on its scheme-theoretic support ([Stacks, Tag 02OM]), that support is affine, Serre vanishing ([Stacks, Tag 01XB]) kills the higher cohomology there, and a closed immersion does not change cohomology.

theorem isZero_cohomologyOverField_of_topologicalKrullDim_supp_le_zero (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] (F : X.Modules) [F.IsCoherent]
    (hF : topologicalKrullDim (_root_.SheafOfModules.supp F) ≤ 0) (i : ℕ) (hi : 0 < i) :
    IsZero (cohomologyOverField k f F i)

AlgebraicGeometry.eulerCharacteristic_eq_finrank_cohomologyOverField_zero_of_supp_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ZeroDimensionalSupport/Vanishing.lean, line 407. The attribute's comment: “(4)”.

[Stacks, Tag 0AYT] (4): the Euler characteristic of a coherent module whose support has dimension at most zero is the dimension of its space of global sections. For f : X ⟶ Spec k proper and ℱ coherent on X with dim (supp ℱ) ≤ 0,

χ(X, ℱ) = dim_k H⁰(X, ℱ).

This is the source's "we have (4) by definition of the Euler characteristic χ(X, ℱ) and (3)": AlgebraicGeometry.eulerCharacteristic is by definition the alternating sum ∑ⁿ (-1)ⁿ dim_k Hⁿ(X, ℱ), clause (3) kills every term with n > 0, and a sum supported on {0} is its value there.

theorem eulerCharacteristic_eq_finrank_cohomologyOverField_zero_of_supp_le_zero (k : Type u)
    [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] (F : X.Modules)
    [F.IsCoherent] (hF : topologicalKrullDim (_root_.SheafOfModules.supp F) ≤ 0) :
    eulerCharacteristic k f F = (Module.finrank k (cohomologyOverField k f F 0) : ℤ)

AlgebraicGeometry.exists_eulerCharacteristic_tensorSheaf_eq_rank_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorEulerZeroDim/FiniteRank.lean, line 343. The attribute's comment: “tensor_rank”.

Clause (5) of [Stacks, Tag 0AYT]. Let k be a field, X a proper scheme over k and ℱ a coherent sheaf with dim Supp ℱ ≤ 0. Then

χ(X, ℱ ⊗ ℰ) = n · χ(X, ℱ)

for every locally free module ℰ of rank n.

This is the clause in the argument order the source writes it in, with the coherent factor first; the Euler characteristic requires its argument to be coherent, so the conclusion also supplies that. The other order, which the chain above this clause consumes, is AlgebraicGeometry.exists_eulerCharacteristic_tensorSheaf_eq_mul_of_isFiniteLocallyFreeOfRank, and the two differ by Stacks.SheafOfModules.TensorPresentations.tensorSheafSwap.

The clause string is on the attribute because the other four clauses of Tag 0AYT are not proved here: clause (1) is registered on AlgebraicGeometry.nonempty_generatingSections_of_support_dim_le_zero, and clauses (2), (3) and (4) in StacksFrontier.AlgebraicGeometry.Cohomology.ZeroDimensionalSupport.Vanishing, on AlgebraicGeometry.suppStalkDirectSumAddEquiv together with AlgebraicGeometry.cohomologyOverFieldZeroEquivDirectSumSuppStalk, on AlgebraicGeometry.isZero_cohomologyOverField_of_topologicalKrullDim_supp_le_zero and on AlgebraicGeometry.eulerCharacteristic_eq_finrank_cohomologyOverField_zero_of_supp_le_zero.

theorem exists_eulerCharacteristic_tensorSheaf_eq_rank_mul [IsProper f] (F : X.Modules)
    [SheafOfModules.IsCoherent F]
    (hdim : topologicalKrullDim (_root_.SheafOfModules.supp F) ≤ 0) (E : X.Modules) (n : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E n] :
    ∃ h : ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X.toRingedSpace)).presheaf,
        ((X.toRingedSpace)).IsSheaf⟩).obj (F)).obj (E))).IsCoherent,
      @eulerCharacteristic k _ X f _ ((((Stacks.SheafOfModules.Tensor.sheafTensor
          ⟨((X.toRingedSpace)).presheaf, ((X.toRingedSpace)).IsSheaf⟩).obj (F)).obj (E))) h =
        (n : ℤ) * eulerCharacteristic k f F
Tag 08AB, a lemma

Tag 08AB in the Stacks Project.

AlgebraicGeometry.eulerCharacteristic_baseChange_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/BaseFieldInvariance.lean, line 78. References: EGA III (7.9.7), “special case”.

The Euler characteristic is unchanged by extension of the ground field. Let k'/k be an extension of fields, let X be a proper scheme over k, let ℱ be a coherent 𝒪_X-module and let ℱ' be the pullback of ℱ to a base change X' of X to k'. Then χ(X, ℱ) = χ(X', ℱ').

public theorem eulerCharacteristic_baseChange_field
    (h : IsPullback g' f' f (specMapAlgebraMap k k')) [IsProper f] (F : X.Modules)
    [F.IsCoherent] :
    eulerCharacteristic k f F =
      @eulerCharacteristic k' _ X' f' (isProper_of_isPullback_specMapAlgebraMap k k' g' f' f h)
        ((Scheme.Modules.pullback g').obj F)
        (isCoherent_pullback_of_isPullback_specMapAlgebraMap k k' g' f' f h F)
Tag 0BEK, a lemma

Tag 0BEK in the Stacks Project.

AlgebraicGeometry.eulerCharacteristic_eq_finsum_higherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/ProperPushforwardUnconditional.lean, line 72.

[Stacks, Tag 0BEK]. Let k be a field, let f : Y ⟶ X be a morphism of schemes proper over k and let G be a coherent 𝒪_Y-module. Then χ(Y, G) = ∑ᵢ (-1)ⁱ χ(X, Rⁱf_*G), the sum being over the nonnegative degrees, with no hypothesis.

The coherence of Rⁱf_*G that the right-hand side needs in order to name χ(X, Rⁱf_*G) is [Stacks, Tag 02O5], in the form AlgebraicGeometry.ProperCoherenceWitness.higherDirectImageIsCoherent.

public theorem eulerCharacteristic_eq_finsum_higherDirectImage
    (k : Type u) [Field k] {Y X : Scheme.{u}}
    (f : Y ⟶ X) (g : X ⟶ Spec (.of k))
    [IsProper g] [IsProper (f ≫ g)]
    (G : Y.Modules) [G.IsCoherent] :
    eulerCharacteristic k (f ≫ g) G =
      ∑ᶠ i : ℕ, (-1 : ℤ) ^ i *
        @eulerCharacteristic k _ X g _
          (((Scheme.Modules.pushforward f).rightDerivedPlus (i : ℤ)).obj G)
          (ProperCoherenceWitness.higherDirectImageIsCoherent Y X f
            (LocallyOfFiniteType.isLocallyNoetherian g) (IsProper.of_comp f g) G
            inferInstance i)
Sources
LeanAlgebraicGeometry.eulerCharacteristic · AlgebraicGeometry.eulerCharacteristic_add_of_shortExact · AlgebraicGeometry.nonempty_generatingSections_of_support_dim_le_zero · AlgebraicGeometry.suppStalkDirectSumAddEquiv · AlgebraicGeometry.cohomologyOverFieldZeroEquivDirectSumSuppStalk · AlgebraicGeometry.isZero_cohomologyOverField_of_topologicalKrullDim_supp_le_zero · AlgebraicGeometry.eulerCharacteristic_eq_finrank_cohomologyOverField_zero_of_supp_le_zero · AlgebraicGeometry.exists_eulerCharacteristic_tensorSheaf_eq_rank_mul

Section33.34 Projective space#

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

Tag 0B2P, a lemma

Tag 0B2P in the Stacks Project.

AlgebraicGeometry.topologicalKrullDim_projectiveSpaceOverRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Dimension/OverField.lean, line 36. The attribute's comment: “projective_space_dimension”.

Stacks Project, Tag 0B2P (dimension). Projective n-space over a field has Krull dimension n as a topological space.

theorem topologicalKrullDim_projectiveSpaceOverRing (k : Type u) [Field k] (n : ℕ) :
    topologicalKrullDim (projectiveSpaceOverRing n (CommRingCat.of k)) = (n : WithBot ℕ∞)

AlgebraicGeometry.projectiveSpaceOver.smooth, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/SmoothProjectiveVariety.lean, line 93. The attribute's comment: “projective_space_smooth”. References: EGA IV (17.3.9), “free E, P^n_S”.

Stacks Project, Tag 0B2P (smoothness). Projective n-space over a scheme S is smooth over S, being the base change of the integral model, which is smooth over the terminal scheme.

public instance smooth (n : ℕ) (S : Scheme.{u}) : Smooth (projectiveSpaceOver n S ↘ S)

AlgebraicGeometry.isProjectiveMorphism_projectiveSpaceOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/SmoothProjectiveVariety.lean, line 106. The attribute's comment: “projective_space_projective”.

Stacks Project, Tag 0B2P (projectivity). Projective n-space over a scheme S is projective over S: the identity is a closed immersion of ℙⁿ_S into ℙⁿ_S over S.

public theorem isProjectiveMorphism_projectiveSpaceOver (n : ℕ) (S : Scheme.{u}) :
    IsProjectiveMorphism (projectiveSpaceOver n S ↘ S)

AlgebraicGeometry.projectiveSpaceOverRing.isVariety, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/SmoothProjectiveVariety.lean, line 153. The attribute's comment: “projective_space_variety”.

Stacks Project, Tag 0B2P (variety). Projective n-space over a field is a variety over that field: it is integral, and its structure morphism is separated and of finite type because it is proper, and quasi-compact because projective space is quasi-compact.

public instance isVariety (k : Type u) [Field k] (n : ℕ) :
    IsVariety k (projectiveSpaceOverRing n (CommRingCat.of k) ↘ Spec (CommRingCat.of k))
Tag 0B2Q, a lemma

Tag 0B2Q in the Stacks Project.

AlgebraicGeometry.add_le_add_topologicalKrullDim_irreducibleComponent_inter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/AffineIntersection.lean, line 464.

Stacks Project, Tag 0B2Q. Let k be a field and let Xs and Ys be closed subsets of affine n-space over k, that is, of the prime spectrum of MvPolynomial (Fin n) k. If Xs and Ys are equidimensional of dimensions r and s, then every irreducible component Z of Xs ∩ Ys satisfies r + s ≤ n + dim Z, that is, has dimension at least r + s - n.

theorem add_le_add_topologicalKrullDim_irreducibleComponent_inter (k : Type u) [Field k]
    (n r s : ℕ) (Xs Ys : Set (PrimeSpectrum (MvPolynomial (Fin n) k)))
    (hXc : IsClosed Xs) (hYc : IsClosed Ys)
    (hXe : Equidimensional Xs) (hYe : Equidimensional Ys)
    (hXd : topologicalKrullDim Xs = r) (hYd : topologicalKrullDim Ys = s)
    (Z : Set ↥(Xs ∩ Ys)) (hZ : Z ∈ irreducibleComponents ↥(Xs ∩ Ys)) :
    (r : WithBot ℕ∞) + s ≤ n + topologicalKrullDim Z
Tag 0B2R, a lemma

Tag 0B2R in the Stacks Project.

AlgebraicGeometry.inter_nonempty_projectiveSpaceOverRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/ProjectiveIntersection.lean, line 394. The attribute's comment: “nonemptiness”.

Let k be a field and let X and Y be nonempty closed subsets of ℙⁿ_k of dimensions r and s. If n ≤ r + s then X and Y meet.

theorem inter_nonempty_projectiveSpaceOverRing
    (X Y : Set (AlgebraicGeometry.projectiveSpaceOverRing n (CommRingCat.of k)))
    (hXc : IsClosed X) (hYc : IsClosed Y) (hXne : X.Nonempty) (hYne : Y.Nonempty)
    (hXd : topologicalKrullDim ↥X = (r : WithBot ℕ∞))
    (hYd : topologicalKrullDim ↥Y = (s : WithBot ℕ∞))
    (hrs : n ≤ r + s) : (X ∩ Y).Nonempty

AlgebraicGeometry.le_topologicalKrullDim_inter_projectiveSpaceOverRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Dimension/ProjectiveIntersection.lean, line 410. The attribute's comment: “dimension bound”.

Let k be a field and let X and Y be nonempty closed subsets of ℙⁿ_k of dimensions r and s. If n ≤ r + s then X ∩ Y has dimension at least r + s - n.

theorem le_topologicalKrullDim_inter_projectiveSpaceOverRing
    (X Y : Set (AlgebraicGeometry.projectiveSpaceOverRing n (CommRingCat.of k)))
    (hXc : IsClosed X) (hYc : IsClosed Y) (hXne : X.Nonempty) (hYne : Y.Nonempty)
    (hXd : topologicalKrullDim ↥X = (r : WithBot ℕ∞))
    (hYd : topologicalKrullDim ↥Y = (s : WithBot ℕ∞))
    (hrs : n ≤ r + s) : ((r + s - n : ℕ) : WithBot ℕ∞) ≤ topologicalKrullDim ↥(X ∩ Y)
Tag 0BXU, a lemma

Tag 0BXU in the Stacks Project.

AlgebraicGeometry.ProjectiveSpectrum.Proj.projectiveSpace_idealOfClosedSubscheme_isPrincipal_of_dimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CodimOneSubscheme/ProjHeightOne.lean, line 365.

Stacks Project, Tag 0BXU. Let k be a field and let Z be a closed subscheme of P^n_k = Proj k[T₀, …, Tₙ] which has no embedded points and every irreducible component of which has dimension n - 1. Then the homogeneous ideal I(Z) ⊆ k[T₀, …, Tₙ] corresponding to Z is principal.

The dimension hypothesis is written without subtraction as dim W + 1 = n. A field is a Noetherian unique factorization domain, and in projective space over a field a component of dimension n - 1 has codimension one, so this is a special case of Tag 0BXL in the form projectiveSpace_idealOfClosedSubscheme_isPrincipal_of_codimension_one.

theorem projectiveSpace_idealOfClosedSubscheme_isPrincipal_of_dimension (k : Type u) [Field k]
    (n : ℕ) {Z : Scheme.{u}} (i : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
    [IsClosedImmersion i] (hno : HasNoEmbeddedPoints Z)
    (hdim : ∀ W ∈ irreducibleComponents Z, topologicalKrullDim W + 1 = (n : WithBot ℕ∞)) :
    (idealOfClosedSubscheme
      (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) i).IsPrincipal
Sources
LeanAlgebraicGeometry.topologicalKrullDim_projectiveSpaceOverRing · AlgebraicGeometry.projectiveSpaceOver.smooth · AlgebraicGeometry.isProjectiveMorphism_projectiveSpaceOver · AlgebraicGeometry.projectiveSpaceOverRing.isVariety · AlgebraicGeometry.add_le_add_topologicalKrullDim_irreducibleComponent_inter · AlgebraicGeometry.inter_nonempty_projectiveSpaceOverRing · AlgebraicGeometry.le_topologicalKrullDim_inter_projectiveSpaceOverRing · AlgebraicGeometry.ProjectiveSpectrum.Proj.projectiveSpace_idealOfClosedSubscheme_isPrincipal_of_dimension

Section33.35 Coherent sheaves on projective space#

Section 33.35 of the Stacks Project, Tag 089X. 14 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 089Z, a lemma

Tag 089Z in the Stacks Project.

Stacks.ProjectiveSpace.exists_iso_projectiveSpace_hyperplane, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/HyperplaneIsProjectiveSpace.lean, line 530. The attribute's comment: “for the hyperplane presented by a nonzero degree-one form”.

A hyperplane in ℙⁿ_k is ℙ^{n-1}_k, and 𝒪(1) pulls back to 𝒪(1).

For a nonzero homogeneous form l of degree one on ℙⁿ_k = Proj k[T₀, …, Tₙ] with n = m + 1, there is an isomorphism φ : ℙ^{n-1}_k ⟶ H onto the hyperplane H = Z(l) under which the pullback of 𝒪(1) along φ composed with the inclusion i : H ⟶ ℙⁿ_k is 𝒪(1).

The last clause says that φ composed with the inclusion is a morphism over Spec k: it carries the structure morphism of ℙⁿ_k to that of ℙ^{n-1}_k, both written as AlgebraicGeometry.Proj.toSpecZero followed by Spec of the inclusion of the constants. This is Stacks.ProjectiveCohomology.projModelToSpec in the spelling of that file, unfolded here so that no import of it is needed; it holds because φ.hom composed with the inclusion is Proj of the graded surjection of Stacks.ProjectiveSpace.exists_gradedHom_ker_span_degreeOne, which is a k-algebra map. Without it the identification of the hyperplane with ℙ^{n-1}_k says nothing about k-vector-space dimensions of cohomology, so no Euler characteristic can be transported across it.

theorem exists_iso_projectiveSpace_hyperplane
    (l : MvPolynomial.homogeneousSubmodule (Fin (m + 2)) k 1)
    (hl : (l : MvPolynomial (Fin (m + 2)) k) ≠ 0) :
    ∃ φ : AlgebraicGeometry.Proj (MvPolynomial.homogeneousSubmodule (Fin (m + 1)) k)
        ≅ (hyperplane l).subscheme,
      Nonempty ((Scheme.Modules.pullback (φ.hom ≫ (hyperplane l).subschemeι)).obj
          (twistingSheafModule (MvPolynomial.homogeneousSubmodule (Fin (m + 2)) k) ((1 : ℕ) : ℤ))
        ≅ twistingSheafModule
            (MvPolynomial.homogeneousSubmodule (Fin (m + 1)) k) ((1 : ℕ) : ℤ)) ∧
      φ.hom ≫ (hyperplane l).subschemeι ≫
          Proj.toSpecZero (MvPolynomial.homogeneousSubmodule (Fin (m + 2)) k) ≫
            Spec.map (CommRingCat.ofHom (algebraMap k
              ↥(MvPolynomial.homogeneousSubmodule (Fin (m + 2)) k 0))) =
        Proj.toSpecZero (MvPolynomial.homogeneousSubmodule (Fin (m + 1)) k) ≫
          Spec.map (CommRingCat.ofHom (algebraMap k
            ↥(MvPolynomial.homogeneousSubmodule (Fin (m + 1)) k 0)))

Stacks.ProjectiveSpace.exists_iso_projectiveSpace_hyperplaneOfSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/HyperplaneIsProjectiveSpace.lean, line 575.

A hyperplane in ℙⁿ_k is ℙ^{n-1}_k, and 𝒪(1) pulls back to 𝒪(1).

A hyperplane in ℙⁿ_k = Proj k[T₀, …, Tₙ], with n = m + 1, is the zero scheme H = Z(s) of a nonzero global section s of 𝒪(1). There is an isomorphism φ : ℙ^{n-1}_k ⟶ H under which the pullback of 𝒪(1) along φ composed with the inclusion i : H ⟶ ℙⁿ_k is 𝒪(1), and φ composed with that inclusion is a morphism over Spec k.

Such an s is the section of a nonzero homogeneous form of degree one, by Stacks.ProjectiveSpace.Cohomology.exists_degreeSection_eq, so this is Stacks.ProjectiveSpace.exists_iso_projectiveSpace_hyperplane with the form produced from the section.

The over-Spec k clause is carried because the consumers of this tag in the hyperplane restriction data of [Stacks, Tag 08A7] need the identification to respect the base: without it the pushforward along H ⟶ ℙⁿ_k cannot be compared with one over Spec k.

theorem exists_iso_projectiveSpace_hyperplaneOfSection
    (s : twistGlobalSections (MvPolynomial.homogeneousSubmodule (Fin (m + 2)) k) 1)
    (hs : s ≠ 0) :
    ∃ φ : AlgebraicGeometry.Proj (MvPolynomial.homogeneousSubmodule (Fin (m + 1)) k)
        ≅ (hyperplaneOfSection s).subscheme,
      Nonempty ((Scheme.Modules.pullback (φ.hom ≫ (hyperplaneOfSection s).subschemeι)).obj
          (twistingSheafModule (MvPolynomial.homogeneousSubmodule (Fin (m + 2)) k) ((1 : ℕ) : ℤ))
        ≅ twistingSheafModule
            (MvPolynomial.homogeneousSubmodule (Fin (m + 1)) k) ((1 : ℕ) : ℤ)) ∧
        φ.hom ≫ (hyperplaneOfSection s).subschemeι ≫
            Proj.toSpecZero (MvPolynomial.homogeneousSubmodule (Fin (m + 2)) k) ≫
              Spec.map (CommRingCat.ofHom (algebraMap k
                ↥(MvPolynomial.homogeneousSubmodule (Fin (m + 2)) k 0))) =
          Proj.toSpecZero (MvPolynomial.homogeneousSubmodule (Fin (m + 1)) k) ≫
            Spec.map (CommRingCat.ofHom (algebraMap k
              ↥(MvPolynomial.homogeneousSubmodule (Fin (m + 1)) k 0)))
Tag 08A0, a lemma

Tag 08A0 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjectiveSpaceHyperplaneSection.exists_homogeneousSection_nonvanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjectiveSpaceHyperplaneSection.lean, line 106. The attribute's comment: “the choice of the hyperplane section — a nonzero s vanishing at no associated point of ℱ, which is the one step needing k infinite; not the exact sequence”.

Let k be an infinite field and let ℱ be a coherent module on ℙⁿ_k = Proj k[T₀, …, Tₙ]. Then some nonzero linear form f gives a nonzero global section f / 1 of 𝒪(1) whose nonvanishing locus contains every associated point of ℱ.

theorem exists_homogeneousSection_nonvanishing [Infinite k]
    (F : (AlgebraicGeometry.Proj (polyGrading k n)).Modules) [F.IsCoherent] :
    ∃ (f : MvPolynomial (Fin (n + 1)) k) (hf : f ∈ polyGrading k n 1), f ≠ 0 ∧
      (homogeneousSection (polyGrading k n) f hf).eval (op ⊤) ≠ 0 ∧
      Stacks.Divisors.associatedPoints F ⊆
        (Stacks.SheafOfModules.nonvanishingOpen
          (X := (AlgebraicGeometry.Proj (polyGrading k n)).toRingedSpace)
          (twistingModule (polyGrading k n) 1)
          (homogeneousSection (polyGrading k n) f hf) :
            Set ↥(AlgebraicGeometry.Proj (polyGrading k n)))

Stacks.AlgebraicGeometry.ProjectiveSpaceHyperplaneSection.shortExact_hyperplaneUnit_of_nonvanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjectiveSpaceHyperplaneSection.lean, line 218. The attribute's comment: “the short exact sequence for an arbitrary coherent module”.

Let S be a scheme with ℙⁿ_S locally Noetherian, let ℱ be an 𝒪-module on ℙⁿ_S with ℱ(-1) and ℱ(-1) ⊗ 𝒪(1) quasi-coherent, and let s be a global section of 𝒪(1) that does not vanish near any associated point of ℱ(-1). Writing i : H ⟶ ℙⁿ_S for the hyperplane cut out by s, the sequence

0 ⟶ ℱ(-1) ⟶ ℱ ⟶ i_* i^* ℱ ⟶ 0

is short exact, the first arrow being multiplication by s and the second the restriction to H.

theorem shortExact_hyperplaneUnit_of_nonvanishing (S : Scheme.{u})
    [IsLocallyNoetherian (projectiveSpaceOver n S)]
    (F : (projectiveSpaceOver n S).Modules) (s : (twistOver n S 1).sections)
    [(tensorModules (projectiveSpaceOver n S) F (twistOver n S (-1))).IsQuasicoherent]
    [(tensorModules (projectiveSpaceOver n S) F (twistOver n S (-1)) ⊗
        twistOver n S 1).IsQuasicoherent]
    (hW : ∀ x ∈ Stacks.Divisors.associatedPoints
        (tensorModules (projectiveSpaceOver n S) F (twistOver n S (-1))),
      ∃ W : (projectiveSpaceOver n S).Opens, x ∈ W ∧ ∀ y ∈ W,
        y ∈ Stacks.SheafOfModules.nonvanishingLocus
          (X := (projectiveSpaceOver n S).toRingedSpace) (twistOver n S 1) s) :
    ∃ h : twistSectionMulNegOne n S F s ≫ hyperplaneUnit n S F s = 0,
      (CategoryTheory.ShortComplex.mk (twistSectionMulNegOne n S F s)
        (hyperplaneUnit n S F s) h).ShortExact

AlgebraicGeometry.exists_section_shortExact_hyperplaneUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/HyperplaneSequenceCoherent.lean, line 128.

[Stacks, Tag 08A0]. Let k be an infinite field and let ℱ be a coherent sheaf on ℙⁿ_k. Then there is a nonzero global section s of 𝒪(1) such that, with i : H ⟶ ℙⁿ_k the hyperplane cut out by s, the sequence

0 ⟶ ℱ(-1) ⟶ ℱ ⟶ i_* i^* ℱ ⟶ 0

is short exact — the first arrow being multiplication by s (…ProjectiveSpaceSectionMultiplication.twistSectionMulNegOne) and the second the restriction to H (…ProjectiveSpaceSectionMultiplication.hyperplaneUnit).

The section is produced by AlgebraicGeometry.exists_form_section_nonvanishing applied to the coherent module ℱ(-1), which is the only step at which k has to be infinite, and the sequence is …ProjectiveSpaceHyperplaneSection.shortExact_hyperplaneUnit_of_nonvanishing; the quasi-coherence that the latter asks of ℱ(-1) and of ℱ(-1) ⊗ 𝒪(1) holds for every coherent ℱ, by [Stacks, Tag 0GQM].

theorem exists_section_shortExact_hyperplaneUnit (k : Type u) [Field k] [Infinite k] (n : ℕ)
    (F : (projectiveSpaceOverRing n (CommRingCat.of k)).Modules) [F.IsCoherent] :
    ∃ s : (twistOver n (Spec (CommRingCat.of k)) 1).sections,
      PresheafOfModules.sections.eval s (op ⊤) ≠ 0 ∧
      ∃ w : twistSectionMulNegOne n (Spec (CommRingCat.of k)) F s ≫
          hyperplaneUnit n (Spec (CommRingCat.of k)) F s = 0,
        (ShortComplex.mk (twistSectionMulNegOne n (Spec (CommRingCat.of k)) F s)
          (hyperplaneUnit n (Spec (CommRingCat.of k)) F s) w).ShortExact
Tag 08A1, a remark

Tag 08A1 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjectiveSpaceSectionFiniteFamily.exists_section_forall_shortExact_coherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/HyperplaneSequenceFiniteFamily.lean, line 116. The attribute's comment: “one section of O(1) works for a whole finite family of coherent modules”.

[Stacks, Tag 08A1]. Let k be an infinite field, let n ≥ 1 and let ℱ_i be a finite family of coherent 𝒪-modules on ℙⁿ_k. Then a single nonzero global section s of 𝒪(1) serves all of them: with i : H ⟶ ℙⁿ_k the hyperplane cut out by s, the sequence

0 ⟶ ℱ_i(-1) ⟶ ℱ_i ⟶ i_* i^* ℱ_i ⟶ 0

of [Stacks, Tag 08A0] is short exact for every member of the family, the first arrow being multiplication by s and the second the restriction to H.

This is the source's argument: [Stacks, Tag 08A0] (AlgebraicGeometry.exists_section_shortExact_hyperplaneUnit) is applied to the coherent module ⨁ ℱ_i, and the resulting conditions descend to each summand by sectionWorksFor_of_retract.

theorem exists_section_forall_shortExact_coherent {k : Type u} [Field k] [Infinite k]
    (_hn : 1 ≤ n) {ι : Type*} [Finite ι]
    (F : ι → (projectiveSpaceOver n (Spec (CommRingCat.of k))).Modules)
    (hF : ∀ i, (F i).IsCoherent) :
    ∃ s : (twistOver n (Spec (CommRingCat.of k)) 1).sections,
      PresheafOfModules.sections.eval s (op ⊤) ≠ 0 ∧ ∀ i : ι,
      ∃ hz : twistSectionMulNegOne n (Spec (CommRingCat.of k)) (F i) s ≫
          hyperplaneUnit n (Spec (CommRingCat.of k)) (F i) s = 0,
        (ShortComplex.mk (twistSectionMulNegOne n (Spec (CommRingCat.of k)) (F i) s)
          (hyperplaneUnit n (Spec (CommRingCat.of k)) (F i) s) hz).ShortExact
Tag 0EGK, a remark

Tag 0EGK in the Stacks Project.

Stacks.AlgebraicGeometry.HyperplaneTwistSequence.pullbackTwistModuleIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/HyperplaneTwistSequence.lean, line 362. The attribute's comment: “the twist of a module restricted to the hyperplane: i^(F(d)) = (i^F)(d)”.

[Stacks, Tag 0EGK], the twist of a module restricted to the closed subscheme. i^*(ℱ(d)) ≅ (i^*ℱ)(d), the twist on H being taken with respect to i^*L. This is [Stacks, Tag 01CD] for the tensor product followed by pullbackTensorPowModuleIntIso for the tensor power.

def pullbackTwistModuleIso (d : ℤ) :
    (Scheme.Modules.pullback i).obj (twistModule X L F d) ≅
      twistModule Hy ((Scheme.Modules.pullback i).obj L)
        ((Scheme.Modules.pullback i).obj F) d

Stacks.AlgebraicGeometry.HyperplaneTwistSequence.pushforwardTwistModuleIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/HyperplaneTwistSequence.lean, line 379. The attribute's comment: “the projection formula clause: i_(G(d)) = i_G ⊗ O(d), by [Stacks, Tag 01E8] at a closed immersion”.

[Stacks, Tag 0EGK], the projection formula clause. i_*𝒢 ⊗_{𝒪_X} L^{⊗ d} ≅ i_*(𝒢(d)), which is what makes the third term of the twisted sequence the direct image of a twist on H.

This is [Stacks, Tag 01E8] at a closed immersion — available with no quasi-coherence hypothesis as Stacks.AffineProjectionFormula.closedImmersionProjectionFormulaIso — followed by pullbackTensorPowModuleIntIso, which rewrites i^*(L^{⊗ d}) as (i^*L)^{⊗ d} so that the twist on H is taken with respect to i^*L.

def pushforwardTwistModuleIso (d : ℤ) :
    (tensorRightModules X (tensorPowModule X L d)).obj
        ((Scheme.Modules.pushforward i).obj G) ≅
      (Scheme.Modules.pushforward i).obj
        (twistModule Hy ((Scheme.Modules.pullback i).obj L) G d)

AlgebraicGeometry.exists_iso_pullbackTwistOver_zeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/HyperplaneTwistUnconditional.lean, line 121. The attribute's comment: “the Serre twists on the hyperplane in every degree, the degree-one case being this chapter's own [Stacks, Tag 089Z] on the base-change model”.

[Stacks, Tag 0EGK], the Serre twists on a hyperplane of ℙ^{m+1}_k, in every integer degree.

Let v be a global section of 𝒪(1) on ℙ^{m+1}_k corresponding to a nonzero degree-one form f on Proj k[T₀, …, T_{m+1}]. Then the zero scheme H = Z(v) admits an isomorphism φ : ℙᵐ_k ≅ H along which, for every d ∈ ℤ, the pullback of 𝒪_{ℙ^{m+1}}(d) is 𝒪_{ℙᵐ}(d).

The degree-one case is [Stacks, Tag 089Z] on the base-change model, AlgebraicGeometry.exists_iso_zeroScheme_projectiveSpaceOverRing; the passage from it to every degree is Stacks.AlgebraicGeometry.HyperplaneTwistSequence.pullbackTwistOverIso.

theorem exists_iso_pullbackTwistOver_zeroScheme (k : Type u) [Field k] (m : ℕ)
    (f : MvPolynomial (Fin (m + 2)) k) (hf : f ∈ polyGrading k (m + 1) 1) (hf0 : f ≠ 0)
    (v : Γ(twistOver (m + 1) (Spec (CommRingCat.of k)) 1, ⊤))
    (hv : ConcreteCategory.hom (twistGammaTopIso k (m + 1)).hom v
      = degreeSection (polyGrading k (m + 1)) 1 ⟨f, hf⟩) :
    ∃ φ : projectiveSpaceOverRing m (CommRingCat.of k) ≅
        (AlgebraicGeometry.zeroScheme (projectiveSpaceOverRing (m + 1) (CommRingCat.of k))
          (twistOver (m + 1) (Spec (CommRingCat.of k)) 1) v).subscheme,
      ∀ d : ℤ, Nonempty ((Scheme.Modules.pullback (φ.hom ≫
          (AlgebraicGeometry.zeroScheme (projectiveSpaceOverRing (m + 1) (CommRingCat.of k))
            (twistOver (m + 1) (Spec (CommRingCat.of k)) 1) v).subschemeι)).obj
        (twistOver (m + 1) (Spec (CommRingCat.of k)) d)
          ≅ twistOver m (Spec (CommRingCat.of k)) d)

AlgebraicGeometry.exists_hyperplane_twistedSequence_cohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/HyperplaneTwistUnconditional.lean, line 434. The attribute's comment: “the whole remark in the situation of Tags 089Z and 08A0: the hyperplane is P^m_k with O_H(d) = i^O(d) in every degree, the twisted sequence 0 → F(d-1) → F(d) → i_(G(d)) → 0 is short exact for every d, and its long exact cohomology sequence has H^j(H, G(d)) as its third term”.

[Stacks, Tag 0EGK] in full. Let k be an infinite field and let ℱ be a coherent sheaf on ℙ^{m+1}_k. Then there are a nonzero global section s of 𝒪(1), an isomorphism φ : ℙᵐ_k ≅ H of ℙᵐ_k with the hyperplane H = Z(s) and, writing i : H ⟶ ℙ^{m+1}_k for the inclusion and 𝒢 = i^*ℱ, a short exact sequence

0 ⟶ ℱ(-1) ⟶ ℱ ⟶ i_*𝒢 ⟶ 0

such that

  • 𝒪_H(d) = i^*𝒪_{ℙ^{m+1}}(d) along φ, for every d ∈ ℤ;
  • for every d ∈ ℤ the twisted sequence 0 ⟶ ℱ(d-1) ⟶ ℱ(d) ⟶ i_*(𝒢(d)) ⟶ 0 is short exact;
  • and for every d ∈ ℤ and every j the four-term sequence

H^j(ℙ^{m+1}_k, ℱ(d-1)) ⟶ H^j(ℙ^{m+1}_k, ℱ(d)) ⟶ H^j(H, 𝒢(d)) ⟶ H^{j+1}(ℙ^{m+1}_k, ℱ(d-1))

is exact at each of its three inner spots, its third term being cohomology on H and its connecting map the canonical one of the cohomological δ-functor of [Stacks, Tag 071H] read through the comparison of [Stacks, Tag 089W].

The index is written m + 1 rather than n with 1 ≤ n so that the hyperplane is ℙᵐ_k with no truncated subtraction. The first clause is exists_iso_pullbackTwistOver_zeroScheme, the untwisted sequence is [Stacks, Tag 08A0] and the two remaining clauses are Stacks.AlgebraicGeometry.HyperplaneTwistSequence.shortExact_twistedSequence and …HyperplaneTwistSequence.exact_cohomology_twistedSequence, whose quasi-coherence input is isQuasicoherent_twistModule_pullback.

theorem exists_hyperplane_twistedSequence_cohomology (k : Type u) [Field k] [Infinite k]
    (m : ℕ) (F : (projectiveSpaceOverRing (m + 1) (CommRingCat.of k)).Modules)
    [F.IsCoherent] :
    ∃ (s : (twistOver (m + 1) (Spec (CommRingCat.of k)) 1).sections)
      (φ : projectiveSpaceOverRing m (CommRingCat.of k) ≅
        (hyperplane (m + 1) (Spec (CommRingCat.of k)) s).subscheme)
      (a : twistModule (projectiveSpaceOverRing (m + 1) (CommRingCat.of k))
          (twistOver (m + 1) (Spec (CommRingCat.of k)) 1) F (-1) ⟶ F)
      (w : a ≫ hyperplaneUnit (m + 1) (Spec (CommRingCat.of k)) F s = 0)
      (hS : (ShortComplex.mk a
        (hyperplaneUnit (m + 1) (Spec (CommRingCat.of k)) F s) w).ShortExact),
      let X := projectiveSpaceOverRing (m + 1) (CommRingCat.of k)
      let G := (Scheme.Modules.pullback
        (hyperplaneι (m + 1) (Spec (CommRingCat.of k)) s)).obj F
      let g := hyperplaneUnit (m + 1) (Spec (CommRingCat.of k)) F s
      let hG := fun d : ℤ => isQuasicoherent_twistModule_pullback
        (hyperplaneι (m + 1) (Spec (CommRingCat.of k)) s)
        (twistOver (m + 1) (Spec (CommRingCat.of k)) 1) F (isQuasicoherent_of_isCoherent F) d
      PresheafOfModules.sections.eval s (op ⊤) ≠ 0 ∧
      (∀ d : ℤ, Nonempty ((Scheme.Modules.pullback
            (φ.hom ≫ hyperplaneι (m + 1) (Spec (CommRingCat.of k)) s)).obj
          (twistOver (m + 1) (Spec (CommRingCat.of k)) d)
            ≅ twistOver m (Spec (CommRingCat.of k)) d)) ∧
      ∀ d : ℤ,
        (twistedSequence (hyperplaneι (m + 1) (Spec (CommRingCat.of k)) s)
          (twistOver (m + 1) (Spec (CommRingCat.of k)) 1) F G a g w d).ShortExact ∧
        ∀ j : ℕ,
          Function.Exact (((cohomologyDeltaFunctor X).functor j).map
              (twistedSequence (hyperplaneι (m + 1) (Spec (CommRingCat.of k)) s)
                (twistOver (m + 1) (Spec (CommRingCat.of k)) 1) F G a g w d).f)
            (cohomologyToHyperplaneMap (hyperplaneι (m + 1) (Spec (CommRingCat.of k)) s)
              (twistOver (m + 1) (Spec (CommRingCat.of k)) 1) F G a g w d (hG d) j) ∧
          Function.Exact
              (cohomologyToHyperplaneMap (hyperplaneι (m + 1) (Spec (CommRingCat.of k)) s)
                (twistOver (m + 1) (Spec (CommRingCat.of k)) 1) F G a g w d (hG d) j)
              (cohomologyConnectingMap (hyperplaneι (m + 1) (Spec (CommRingCat.of k)) s)
                (twistOver (m + 1) (Spec (CommRingCat.of k)) 1) F G a g w hS d (hG d) j) ∧
          Function.Exact
              (cohomologyConnectingMap (hyperplaneι (m + 1) (Spec (CommRingCat.of k)) s)
                (twistOver (m + 1) (Spec (CommRingCat.of k)) 1) F G a g w hS d (hG d) j)
              (((cohomologyDeltaFunctor X).functor (j + 1)).map
                (twistedSequence (hyperplaneι (m + 1) (Spec (CommRingCat.of k)) s)
                  (twistOver (m + 1) (Spec (CommRingCat.of k)) 1) F G a g w d).f)
Tag 08A3, a definition

Tag 08A3 in the Stacks Project.

AlgebraicGeometry.IsMRegular, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/Regularity.lean, line 53.

A coherent sheaf on projective n-space over k is m-regular if its cohomology in degree i vanishes after the twist by m - i, for 1 ≤ i ≤ n.

public noncomputable abbrev IsMRegular (k : Type u) [Field k] (n : ℕ)
    (F : (projectiveSpaceOverRing n (.of k)).Modules) [F.IsCoherent] (m : ℤ) : Prop
Tag 08A4, a lemma

Tag 08A4 in the Stacks Project.

AlgebraicGeometry.isMRegular_iff_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpaceBaseChange/FieldExtension.lean, line 267.

[Stacks, Tag 08A4]. Let k ⊆ K be an extension of fields and let ℱ be a coherent sheaf on ℙⁿ_k. Then ℱ is m-regular if and only if its pullback to ℙⁿ_K is m-regular.

public theorem isMRegular_iff_fieldExtension (k K : Type u) [Field k] [Field K] [Algebra k K]
    (n : ℕ) (F : (projectiveSpaceOverRing n (.of k)).Modules) [F.IsCoherent] (m : ℤ) :
    letI : IsLocallyNoetherian (projectiveSpaceOverRing n (.of K)) :=
      projectiveSpaceOver_isLocallyNoetherian n (Spec (.of K))
    letI : ((Scheme.Modules.pullback
      (projectiveSpaceFieldExtensionMap k K n)).obj F).IsCoherent :=
      isCoherent_pullback (projectiveSpaceFieldExtensionMap k K n) F
    IsMRegular k n F m ↔
      IsMRegular K n
        ((Scheme.Modules.pullback (projectiveSpaceFieldExtensionMap k K n)).obj F) m
Tag 08A5, a lemma

Tag 08A5 in the Stacks Project.

AlgebraicGeometry.isMRegular_hyperplaneRestriction_of_nonvanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/HyperplaneRestrictionRegularity.lean, line 304. The attribute's comment: “in the situation of Tag 08A0, for every nonzero section s of O(1) avoiding the associated points of F: the sequence of Tag 08A0 is short exact, H(s) ≅ P^{n-1}_k as in Tag 089Z, and along every such identification the restriction of an m-regular F is m-regular”.

[Stacks, Tag 08A5]. Let k be a field, n ≥ 1, ℱ a coherent sheaf on ℙⁿ_k, and let s be a nonzero global section of 𝒪(1) vanishing at no associated point of ℱ — the hyperplane section of [Stacks, Tag 08A0], which over an infinite field always exists (AlgebraicGeometry.exists_hyperplane_isMRegular_pullback). Write i : H ⟶ ℙⁿ_k for its hyperplane and 𝒢 = i^*ℱ. Then

  • the sequence 0 ⟶ ℱ(-1) ⟶ ℱ ⟶ i_*𝒢 ⟶ 0 of Tag 08A0 is short exact, its arrows being multiplication by s and restriction to H;
  • H ≅ ℙ^{n-1}_k as in [Stacks, Tag 089Z]: there is an identification φ : ℙ^{n-1}_k ≅ H, over Spec k, along which 𝒪(1) restricts to 𝒪(1);
  • and, for every such identification φ (one along which 𝒪(1) restricts to 𝒪(1)) and every m, if ℱ is m-regular then 𝒢 is m-regular on H ≅ ℙ^{n-1}_k, that is φ^*𝒢 = (φ ≫ i)^*ℱ is m-regular on ℙ^{n-1}_k.

The identification of Tag 089Z is not unique — it depends on a choice of coordinates on the hyperplane — so the regularity is asserted for all of them rather than for one. The field need not be infinite once s is given: that hypothesis of Tag 08A0 is used only to choose s.

The sequence is …ProjectiveSpaceHyperplaneSection.shortExact_hyperplaneUnit_of_nonvanishing; the identification is AlgebraicGeometry.exists_iso_zeroScheme_projectiveSpaceOverRing applied to the degree-one form presenting s (Stacks.ProjectiveSpace.Cohomology.exists_degreeSection_eq); the regularity is AlgebraicGeometry.isMRegular_pullback_hyperplaneι_of_nonvanishing.

theorem isMRegular_hyperplaneRestriction_of_nonvanishing (k : Type u) [Field k] (n : ℕ)
    (hn : 1 ≤ n) (F : (projectiveSpaceOverRing n (CommRingCat.of k)).Modules) [F.IsCoherent]
    (s : (twistOver n (Spec (CommRingCat.of k)) 1).sections)
    (hs0 : PresheafOfModules.sections.eval s (op ⊤) ≠ 0)
    (hs : Stacks.Divisors.associatedPoints F ⊆
      Stacks.SheafOfModules.nonvanishingLocus (twistOver n (Spec (CommRingCat.of k)) 1) s) :
    (∃ w : twistSectionMulNegOne n (Spec (CommRingCat.of k)) F s ≫
          hyperplaneUnit n (Spec (CommRingCat.of k)) F s = 0,
        (ShortComplex.mk (twistSectionMulNegOne n (Spec (CommRingCat.of k)) F s)
          (hyperplaneUnit n (Spec (CommRingCat.of k)) F s) w).ShortExact) ∧
      (∃ φ : projectiveSpaceOverRing (n - 1) (CommRingCat.of k) ≅
          (hyperplane n (Spec (CommRingCat.of k)) s).subscheme,
        Nonempty ((Scheme.Modules.pullback
            (φ.hom ≫ hyperplaneι n (Spec (CommRingCat.of k)) s)).obj
              (twistOver n (Spec (CommRingCat.of k)) 1) ≅
            twistOver (n - 1) (Spec (CommRingCat.of k)) 1) ∧
          φ.hom ≫ hyperplaneι n (Spec (CommRingCat.of k)) s ≫
              (projectiveSpaceOverRing n (CommRingCat.of k) ↘ Spec (CommRingCat.of k)) =
            projectiveSpaceOverRing (n - 1) (CommRingCat.of k) ↘ Spec (CommRingCat.of k)) ∧
      ∀ φ : projectiveSpaceOverRing (n - 1) (CommRingCat.of k) ≅
          (hyperplane n (Spec (CommRingCat.of k)) s).subscheme,
        Nonempty ((Scheme.Modules.pullback
            (φ.hom ≫ hyperplaneι n (Spec (CommRingCat.of k)) s)).obj
              (twistOver n (Spec (CommRingCat.of k)) 1) ≅
            twistOver (n - 1) (Spec (CommRingCat.of k)) 1) →
        ∀ m : ℤ, IsMRegular k n F m →
          haveI := projectiveSpaceOver_isLocallyNoetherian (n - 1) (Spec (CommRingCat.of k))
          haveI := isCoherent_pullback (φ.hom ≫ hyperplaneι n (Spec (CommRingCat.of k)) s) F
          IsMRegular k (n - 1)
            ((Scheme.Modules.pullback
              (φ.hom ≫ hyperplaneι n (Spec (CommRingCat.of k)) s)).obj F) m
Tag 08A6, a lemma

Tag 08A6 in the Stacks Project.

AlgebraicGeometry.isMRegular_add_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/HyperplaneRegularity.lean, line 276. The attribute's comment: “an m-regular coherent sheaf on projective space is (m+1)-regular”.

[Stacks, Tag 08A6]. Let k be a field, let n ≥ 0 and let ℱ be a coherent sheaf on ℙⁿ_k. If ℱ is m-regular then ℱ is (m + 1)-regular.

The argument is an induction on n, vacuous for n = 0. Passing to k(t), which is infinite, changes nothing by [Stacks, Tag 08A4]; there a hyperplane j : ℙ^{n-1} ⟶ ℙⁿ is available, the restriction 𝒢 of ℱ to it is m-regular by [Stacks, Tag 08A5] and hence (m+1)-regular by induction, and the segment H^i(ℙⁿ, ℱ(m-i)) ⟶ H^i(ℙⁿ, ℱ(m+1-i)) ⟶ H^i(ℙ^{n-1}, 𝒢(m+1-i)) of the long exact sequence has both ends zero — the right one by (m+1)-regularity of 𝒢 for i ≤ n-1, and by vanishing above the dimension for i = n.

public theorem isMRegular_add_one
    (k : Type u) [Field k] (n : ℕ)
    (F : (projectiveSpaceOverRing n (.of k)).Modules) [F.IsCoherent] (m : ℤ)
    (hF : IsMRegular k n F m) :
    IsMRegular k n F (m + 1)
Tag 08A7, a lemma

Tag 08A7 in the Stacks Project.

AlgebraicGeometry.span_mulSections_eq_top_of_isMRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/RegularitySectionMultiplication.lean, line 386. The attribute's comment: “for an arbitrary field, with the hyperplane restriction data of Tags 08A0, 0EGK and 089Z carried in HyperplaneRestrictionPackage; the induction on n, the base case and the use of m-regularity to lift a section off the hyperplane are proved. Over an infinite field every clause of that package but liftSection is proved too -- see AlgebraicGeometry.exists_hyperplaneRestrictionData. Surjectivity out of the tensor product is stated as the k-span of the products being ⊤.”.

[Stacks, Tag 08A7]. Let k be a field, n ≥ 0 and ℱ a coherent sheaf on ℙⁿ_k. If ℱ is m-regular then the multiplication map

H⁰(ℙⁿ_k, ℱ(m)) ⊗_k H⁰(ℙⁿ_k, 𝒪(1)) ⟶ H⁰(ℙⁿ_k, ℱ(m+1))

is surjective — equivalently, the k-span of the products is everything.

The proof is the source's induction on n. For n = 0 multiplication by a generator of the trivial sheaf 𝒪(1) is already an isomorphism. For the step, the inductive hypothesis writes the restriction of a class t ∈ H⁰(ℱ(m+1)) to the hyperplane as a combination of products σ · g; each g lifts to ℙ^{n+1}_k because m-regularity makes H¹(ℱ(m-1)) vanish, each σ lifts by [Stacks, Tag 089Z], and subtracting the lifted combination leaves a class restricting to zero, which by exactness of the restriction sequence is s times a class in H⁰(ℱ(m)).

theorem span_mulSections_eq_top_of_isMRegular (k : Type u) [Field k]
    (pkg : ∀ (n : ℕ) (F : (projectiveSpaceOverRing (n + 1) (.of k)).Modules),
      F.IsCoherent → Nonempty (HyperplaneRestrictionPackage k n F)) :
    ∀ (n : ℕ) (F : (projectiveSpaceOverRing n (.of k)).Modules) (hFc : F.IsCoherent) (m : ℤ),
      @IsMRegular k _ n F hFc m → mulSectionsSpan k n F m = ⊤

AlgebraicGeometry.span_mulSections_eq_top_of_isMRegular_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/RegularitySectionMultiplicationArbitraryField.lean, line 65. References: SGA 6 XIII (1.3), “(ii), special case”.

[Stacks, Tag 08A7] over an arbitrary field. Let k be a field, n ≥ 0, and let ℱ be a coherent sheaf on ℙⁿ_k which is m-regular. Then the k-span of the products of global sections of ℱ(m) with global sections of 𝒪(1) is all of H⁰(ℙⁿ_k, ℱ(m+1)), i.e. the multiplication map out of H⁰(ℱ(m)) ⊗_k H⁰(𝒪(1)) is surjective.

AlgebraicGeometry.span_mulSections_eq_top_of_isMRegular proves this from the hyperplane restriction data of [Stacks, Tag 08A7], which AlgebraicGeometry.nonempty_hyperplaneRestrictionPackage supplies over an infinite field; AlgebraicGeometry.span_mulSections_eq_top_of_isMRegular_of_infinite is the source's reduction to that case.

Surjectivity of a k-bilinear multiplication out of a tensor product is the same statement as the span of the products being everything — the image of the induced linear map on H⁰(ℱ(m)) ⊗_k H⁰(𝒪(1)) is generated by the images of the pure tensors — so the conclusion below is the source's, not a weakening of it. The field is arbitrary, as in the source: [Infinite k] appears only inside the proof.

theorem span_mulSections_eq_top_of_isMRegular_field (k : Type u) [Field k] (n : ℕ)
    (F : (projectiveSpaceOverRing n (.of k)).Modules) [F.IsCoherent] (m : ℤ)
    (hF : IsMRegular k n F m) :
    mulSectionsSpan k n F m = ⊤
Tag 08A8, a lemma

Tag 08A8 in the Stacks Project.

AlgebraicGeometry.isGeneratedByGlobalSections_projectiveTwist_of_isMRegular_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/RegularityGlobalGenerationUnconditional.lean, line 97. The attribute's comment: “an m-regular coherent sheaf on projective space over a field is globally generated after the twist by m. Everything the source's proof uses is proved: that ℱ(d) is globally generated for all d ≫ 0 is Stacks.ProjectiveSpace.exists_isGeneratedByGlobalSections_projectiveTwist_of_isCoherent, clause (7) of Tag 01Q3 read through the comparison of projectiveTwist with the tensor powers of the hyperplane sheaf; the surjectivity of the multiplication map on global sections is Tag 08A7 over an arbitrary field, AlgebraicGeometry.span_mulSections_eq_top_of_isMRegular_field; and the regularity at each twist the descent passes through is Tag 08A6, AlgebraicGeometry.isMRegular_add_one. The descent is organized as a sequence of single-twist steps rather than the source's one-shot use of degree-d-m forms, so that only the degree-one multiplication of Tag 08A7 is needed. Globally generated is SheafOfModules.IsGeneratedByGlobalSections, Stacks 03DE (3).”. References: SGA 6 XIII (1.3), “(iii), special case”.

Let k be a field, let n ≥ 0, and let ℱ be a coherent sheaf on ℙⁿ_k. If ℱ is m-regular then ℱ(m) is globally generated.

theorem isGeneratedByGlobalSections_projectiveTwist_of_isMRegular_field (k : Type u) [Field k]
    (n : ℕ) (F : (projectiveSpaceOverRing n (.of k)).Modules) [F.IsCoherent] (m : ℤ)
    (hF : IsMRegular k n F m) :
    SheafOfModules.IsGeneratedByGlobalSections (projectiveTwist n F m)
Tag 08AC, a lemma

Tag 08AC in the Stacks Project.

AlgebraicGeometry.exists_polynomial_eval_eq_hilbertPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/HilbertPolynomialFiniteDetermination.lean, line 234.

[Stacks, Tag 08AC]. Let k be a field, let n ≥ 0 and let ℱ be a coherent sheaf on ℙⁿ_k. Then the function d ↦ χ(ℙⁿ_k, ℱ(d)) is a polynomial: there is a P ∈ ℚ[X] with χ(ℙⁿ_k, ℱ(d)) = P(d) for every d ∈ ℤ. No hypothesis.

The n-th backward difference of the Hilbert polynomial is constant (AlgebraicGeometry.isDifferenceBounded_hilbertPolynomial, the source's induction on n), and a function on ℤ with a constant iterated backward difference is a polynomial at every integer (exists_polynomial_of_isDifferenceBounded, the every-integer form of [Stacks, Tag 00JZ] the source's proof ends with).

The weaker eventual reading of "is a polynomial", [Stacks, Tag 00JX]'s IsNumericalPolynomial, is AlgebraicGeometry.isNumericalPolynomial_hilbertPolynomial'.

theorem exists_polynomial_eval_eq_hilbertPolynomial (k : Type u) [Field k] (n : ℕ)
    (F : (projectiveSpaceOverRing n (.of k)).Modules) [F.IsCoherent] :
    ∃ P : Polynomial ℚ, ∀ d : ℤ, (hilbertPolynomial k n F d : ℚ) = P.eval (d : ℚ)

AlgebraicGeometry.isNumericalPolynomial_hilbertPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/HilbertPolynomialNumerical.lean, line 369. The attribute's comment: “the induction on n of the source's proof together with its base case, the triviality of the twists on P^0; its one geometric input is the hypothesis hstep, the hyperplane difference formula of Stacks 0EGK, 08A0, 089Z and 08AA, which is discharged by AlgebraicGeometry.exists_coherent_hilbertPolynomial_sub_eq”.

[Stacks, Tag 08AC], granted the hyperplane difference formula. For a field k, an integer n ≥ 0 and a coherent sheaf ℱ on ℙⁿ_k, the function d ↦ χ(ℙⁿ_k, ℱ(d)) is a numerical polynomial.

The one hypothesis is the geometric fact the source's inductive step consumes, for the given field: for a coherent sheaf on ℙ^{m+1}_k there is a coherent sheaf on ℙ^m_k whose Hilbert polynomial is the first difference of the given one — the displayed equation of the source's proof, read through the identification of the hyperplane with ℙ^m_k. Everything else is proved: the base case is constant because the twists on ℙ⁰_k are trivial (AlgebraicGeometry.projectiveTwistZeroIso), the induction on n is carried out, and [Stacks, Tag 00JZ] in the form main_00JZ turns each difference back into the function.

hstep is itself a theorem, AlgebraicGeometry.exists_coherent_hilbertPolynomial_sub_eq; the hypothesis-free form of the tag is AlgebraicGeometry.isNumericalPolynomial_hilbertPolynomial'.

public theorem isNumericalPolynomial_hilbertPolynomial
    (hstep : ∀ (m : ℕ) (G : (projectiveSpaceOverRing (m + 1) (.of k)).Modules)
      (_ : G.IsCoherent), ∃ (H : (projectiveSpaceOverRing m (.of k)).Modules)
        (hH : H.IsCoherent), ∀ d : ℤ,
          hilbertPolynomial k (m + 1) G d - hilbertPolynomial k (m + 1) G (d - 1) =
            @hilbertPolynomial k _ m H hH d)
    (F : (projectiveSpaceOverRing n (.of k)).Modules) [F.IsCoherent] :
    IsNumericalPolynomial (hilbertPolynomial k n F)

AlgebraicGeometry.isNumericalPolynomial_hilbertPolynomial', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/HilbertPolynomialPolynomial.lean, line 243. The attribute's comment: “the conclusion in the eventual reading of Tag 00JX: the Hilbert polynomial agrees with a sum of binomial coefficients for d >> 0; the tag's own every-integer reading is AlgebraicGeometry.exists_polynomial_eval_eq_hilbertPolynomial”.

[Stacks, Tag 08AC] in its eventual reading. For a field k, an integer n ≥ 0 and a coherent sheaf ℱ on ℙⁿ_k, the function d ↦ χ(ℙⁿ_k, ℱ(d)) is a numerical polynomial. No hypothesis.

The source reduces to an infinite base field by [Stacks, Tag 08AB], and so does this proof: the extension is RatFunc k, the Hilbert polynomial is unchanged by it (AlgebraicGeometry.hilbertPolynomial_pullback_fieldExtension), and over an infinite field the statement is AlgebraicGeometry.isNumericalPolynomial_hilbertPolynomial_of_infinite.

IsNumericalPolynomial is [Stacks, Tag 00JX]'s notion, which constrains the function only for d ≫ 0. The tag as stated — a polynomial identity at every d ∈ ℤ — is AlgebraicGeometry.exists_polynomial_eval_eq_hilbertPolynomial.

public theorem isNumericalPolynomial_hilbertPolynomial' (k : Type u) [Field k] (n : ℕ)
    (F : (projectiveSpaceOverRing n (CommRingCat.of k)).Modules) [F.IsCoherent] :
    IsNumericalPolynomial (hilbertPolynomial k n F)
Tag 08AD, a definition

Tag 08AD in the Stacks Project.

AlgebraicGeometry.hilbertPolynomial, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/HilbertPolynomial.lean, line 43. References: SGA 6 XIII (6.1), “partial”.

The Hilbert polynomial, viewed as an integer-valued function of the twist degree, of a coherent sheaf on projective space over a field.

noncomputable def hilbertPolynomial (k : Type u) [Field k] (n : ℕ)
    (F : (projectiveSpaceOverRing n (.of k)).Modules) [F.IsCoherent] : ℤ → ℤ
Tag 08AE, a lemma

Tag 08AE in the Stacks Project.

Stacks.ProjectiveSpace.Cohomology.exists_eval_eq_finrank_cohomologyOverField_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveSpace/Cohomology/HilbertPolynomial.lean, line 126.

[Stacks, Tag 08AE]. Let k be a field, let n ≥ 0, let ℱ be a coherent sheaf on ℙⁿ_k = Proj k[T₀, …, Tₙ] and let P ∈ ℚ[t] be its Hilbert polynomial, that is, a polynomial agreeing at every integer d with the Euler characteristic χ(ℙⁿ_k, ℱ(d)) of the d-th twist. Then

P(d) = dim_k H⁰(ℙⁿ_k, ℱ(d))

for all d large enough.

The proof is the source's one sentence: the higher cohomology of a high enough twist vanishes ([Stacks, Tag 01YS] clause (4), Stacks.ProjectiveSpace.SerreVanishing.exists_isZero_Hgroup_twist_of_isCoherent), so the alternating sum defining the Euler characteristic collapses to its degree-zero term. The hypothesis hP is the definition of the Hilbert polynomial, [Stacks, Tag 08AD]; see the module docstring for why it is written out here rather than cited as AlgebraicGeometry.hilbertPolynomial.

public theorem exists_eval_eq_finrank_cohomologyOverField_zero (k : Type u) [Field k] (n : ℕ)
    (F : (AlgebraicGeometry.Proj (polyGrading k n)).Modules)
    (hF : _root_.SheafOfModules.IsCoherent F) (P : Polynomial ℚ)
    (hP : ∀ d : ℤ, P.eval (d : ℚ) = (((∑ᶠ i : ℕ, (-1 : ℤ) ^ i *
      (Module.finrank k (cohomologyOverField k (projModelToSpec k n)
        (twistSheafOfModules (polyGrading k n) F d) i) : ℤ) : ℤ)) : ℚ)) :
    ∃ d₀ : ℤ, ∀ d : ℤ, d₀ ≤ d →
      P.eval (d : ℚ) = (Module.finrank k (cohomologyOverField k (projModelToSpec k n)
        (twistSheafOfModules (polyGrading k n) F d) 0) : ℚ)
Tag 08AG, a lemma

Tag 08AG in the Stacks Project.

AlgebraicGeometry.exists_isMRegular_kernel_free_of_hilbertPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/KernelRegularityInduction.lean, line 273. The attribute's comment: “with the free sheaf of the source, the short exact sequence read as an epimorphism from it, and the Hilbert polynomial of Tag 08AD compared with a rational polynomial at every integer”.

[Stacks, Tag 08AG]. Let n ≥ 0, r ≥ 1 and P ∈ ℚ[t]. There is a single integer m such that for every field k, every coherent sheaf 𝒬 on ℙⁿ_k with Hilbert polynomial P and every epimorphism q : 𝒪^{⊕r} ⟶ 𝒬, the kernel of q is m-regular.

The quantifier order is the statement: m is produced from n, r and P alone, before the field and before the sequence.

Over an infinite field this is AlgebraicGeometry.exists_isMRegular_kernel_free_of_hilbertPolynomial_of_infinite, the source's induction on the dimension. An arbitrary field is reduced to that case by base change to the rational function field k(t), which is infinite (AlgebraicGeometry.infinite_ratFunc): ℙⁿ_{k(t)} ⟶ ℙⁿ_k is flat, so the kernel sequence base-changes to the kernel sequence of a surjection of 𝒪^{⊕r} onto the base change of 𝒬; the Hilbert polynomial is unchanged ([Stacks, Tag 08AB], AlgebraicGeometry.hilbertPolynomial_pullback_fieldExtension); and m-regularity descends along the extension by [Stacks, Tag 08A4], AlgebraicGeometry.isMRegular_iff_fieldExtension.

theorem exists_isMRegular_kernel_free_of_hilbertPolynomial (n r : ℕ) (hr : 1 ≤ r)
    (P : Polynomial ℚ) :
    ∃ m : ℤ, ∀ (k : Type u) [Field k]
      (Q : (projectiveSpaceOverRing n (.of k)).Modules) [Q.IsCoherent]
      (q : freeModules k n r ⟶ Q) [Epi q],
      (∀ d : ℤ, (hilbertPolynomial k n Q d : ℚ) = P.eval (d : ℚ)) →
      @IsMRegular k _ n (kernel q) (CoherentAbelian.isCoherent_kernel q) m
Sources
LeanStacks.ProjectiveSpace.exists_iso_projectiveSpace_hyperplane · Stacks.ProjectiveSpace.exists_iso_projectiveSpace_hyperplaneOfSection · Stacks.AlgebraicGeometry.ProjectiveSpaceHyperplaneSection.exists_homogeneousSection_nonvanishing · Stacks.AlgebraicGeometry.ProjectiveSpaceHyperplaneSection.shortExact_hyperplaneUnit_of_nonvanishing · AlgebraicGeometry.exists_section_shortExact_hyperplaneUnit · Stacks.AlgebraicGeometry.ProjectiveSpaceSectionFiniteFamily.exists_section_forall_shortExact_coherent · Stacks.AlgebraicGeometry.HyperplaneTwistSequence.pullbackTwistModuleIso · Stacks.AlgebraicGeometry.HyperplaneTwistSequence.pushforwardTwistModuleIso

Section33.36 Frobenii#

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

Tag 03SM, a definition

Tag 03SM in the Stacks Project.

Stacks.Frobenius.absoluteFrobenius, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Frobenius.lean, line 157. References: SGA 3 VIIA (4.1), “absolute Frobenius fr(X)”; SGA 5 XV (1.Definition2); SGA 4½ Fonctions L (3.4), “F_abs definition”; SGA 4½ Rapport (1.1), “q = p”; SGA 3 VIIB (4.1.1); SGA 7 IX (4.3.2), “special case”; SGA 7 XXI (1.0); SGA 7 XXII (6.2), “(6.2.1) F_q for q = p”.

Stacks Project, Tag 03SM. The absolute Frobenius of a scheme in characteristic p: it is the identity on points and the p-th power map on the structure sheaf.

noncomputable def absoluteFrobenius (X : Scheme.{u}) (p : ℕ) [Fact p.Prime]
    (hX : IsInCharacteristic X p) : X ⟶ X
Tag 0CC7, a lemma

Tag 0CC7 in the Stacks Project.

Stacks.Frobenius.absoluteFrobenius_naturality, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/Absolute.lean, line 39. References: EGA 0 (21.2.6), “more general”; SGA 3 VIIA (4.1); SGA 4½ Rapport (1.3), “special case”; SGA 7 IX (4.3.2), “partial”.

The absolute Frobenius is natural with respect to morphisms of schemes in characteristic p.

public lemma absoluteFrobenius_naturality {X Y : Scheme.{u}} (f : X ⟶ Y) (p : ℕ)
    [Fact p.Prime] (hX : IsInCharacteristic X p) (hY : IsInCharacteristic Y p) :
    absoluteFrobenius X p hX ≫ f = f ≫ absoluteFrobenius Y p hY
Tag 0CC8, a lemma

Tag 0CC8 in the Stacks Project.

AlgebraicGeometry.absoluteFrobenius_universalHomeomorphism, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/AbsoluteUniversalHomeomorphism.lean, line 109.

The absolute Frobenius of a scheme in positive prime characteristic is a universal homeomorphism.

instance absoluteFrobenius_universalHomeomorphism
    (X : Scheme.{u}) (p : ℕ) [Fact p.Prime] (hX : IsInCharacteristic X p) :
    UniversalHomeomorphism (absoluteFrobenius X p hX)

AlgebraicGeometry.absoluteFrobenius_isIntegralHom, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/AbsoluteUniversalHomeomorphism.lean, line 131.

The absolute Frobenius of a scheme in positive prime characteristic is integral.

instance absoluteFrobenius_isIntegralHom
    (X : Scheme.{u}) (p : ℕ) [Fact p.Prime] (hX : IsInCharacteristic X p) :
    IsIntegralHom (absoluteFrobenius X p hX)

AlgebraicGeometry.absoluteFrobenius_residueFieldMap_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/AbsoluteUniversalHomeomorphism.lean, line 139.

The map on residue fields induced by the absolute Frobenius is purely inseparable at every point.

theorem absoluteFrobenius_residueFieldMap_isPurelyInseparable
    (X : Scheme.{u}) (p : ℕ) [Fact p.Prime] (hX : IsInCharacteristic X p)
    (x : X) :
    ((absoluteFrobenius X p hX).residueFieldMap x).hom.IsPurelyInseparable
Tag 0CC9, a definition

Tag 0CC9 in the Stacks Project.

AlgebraicGeometry.frobeniusTwist, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/Twist.lean, line 69. The attribute's comment: “frobenius_twist”. References: SGA 3 VIIA (4.1), “special case”; SGA 3 VIIA (4.3.2); SGA 3 VIIB (4.1.1); SGA 3 XVII (4.3.2), “partial”.

Stacks Project, Tag 0CC9. Frobenius twisting is base change along the absolute Frobenius of the base scheme. Its value at X : Over S is X ×_S S, regarded as an S-scheme through the second projection.

public noncomputable def frobeniusTwist (S : Scheme.{u}) (p : ℕ) [Fact p.Prime]
    (hS : IsInCharacteristic S p) : Over S ⥤ Over S

AlgebraicGeometry.relativeFrobenius_existsUnique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/Twist.lean, line 95. The attribute's comment: “relative_frobenius_characterization”.

Stacks Project, Tag 0CC9. The relative Frobenius is the unique morphism over S whose first projection is the absolute Frobenius of X and whose second projection is the structure morphism of X.

public theorem relativeFrobenius_existsUnique (S : Scheme.{u}) (p : ℕ) [Fact p.Prime]
    (hS : IsInCharacteristic S p) (X : Over S) :
    ∃! g : X ⟶ (frobeniusTwist S p hS).obj X,
      (g.left ≫ pullback.fst X.hom (absoluteFrobenius S p hS) =
          absoluteFrobenius X.left p (isInCharacteristic_of_hom X.hom p hS)) ∧
      (g.left ≫ pullback.snd X.hom (absoluteFrobenius S p hS) = X.hom)

AlgebraicGeometry.relativeFrobenius, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/Twist.lean, line 114. The attribute's comment: “relative_frobenius”. References: SGA 5 XV (1.Definition3); SGA 3 VIIA (4.1), “Fr(X/S) for S-schemes”; SGA 3 VIIA (4.1.3), “Case n=1”; SGA 5 XII (7.3).

Stacks Project, Tag 0CC9. The relative Frobenius morphism of an S-scheme.

public noncomputable def relativeFrobenius (S : Scheme.{u}) (p : ℕ) [Fact p.Prime]
    (hS : IsInCharacteristic S p) (X : Over S) : X ⟶ (frobeniusTwist S p hS).obj X
Tag 0CCA, a lemma

Tag 0CCA in the Stacks Project.

AlgebraicGeometry.relativeFrobenius_naturality, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/Twist.lean, line 147. References: SGA 3 VIIA (4.1), “special case”; SGA 3 VIIA (4.1.3), “special case”; SGA 4½ Rapport (1.3), “special case”; SGA 5 XV (1.Proposition1), “partial”.

Stacks Project, Tag 0CCA. The relative Frobenius is natural in an S-scheme.

public lemma relativeFrobenius_naturality (S : Scheme.{u}) (p : ℕ) [Fact p.Prime]
    (hS : IsInCharacteristic S p) {X Y : Over S} (f : X ⟶ Y) :
    relativeFrobenius S p hS X ≫ (frobeniusTwist S p hS).map f =
      f ≫ relativeFrobenius S p hS Y
Tag 0CCB, a lemma

Tag 0CCB in the Stacks Project.

AlgebraicGeometry.relativeFrobenius_universalHomeomorphism, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/RelativeUniversalHomeomorphism.lean, line 67. References: SGA 5 XV (1.Proposition2), “a) univ. homeo”.

The relative Frobenius is a universal homeomorphism.

instance relativeFrobenius_universalHomeomorphism
    (S : Scheme.{u}) (p : ℕ) [Fact p.Prime] (hS : IsInCharacteristic S p)
    (X : Over S) :
    UniversalHomeomorphism (relativeFrobenius S p hS X).left

AlgebraicGeometry.relativeFrobenius_isIntegralHom, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/RelativeUniversalHomeomorphism.lean, line 84. References: SGA 5 XV (1.Proposition2), “a) integral”; SGA 3 VIIA (7.4.2), “more general”.

The relative Frobenius is integral.

instance relativeFrobenius_isIntegralHom
    (S : Scheme.{u}) (p : ℕ) [Fact p.Prime] (hS : IsInCharacteristic S p)
    (X : Over S) :
    IsIntegralHom (relativeFrobenius S p hS X).left

AlgebraicGeometry.relativeFrobenius_residueFieldMap_isPurelyInseparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/RelativeUniversalHomeomorphism.lean, line 93. References: SGA 5 XV (1.Proposition2), “a) radicial”.

Every residue-field extension induced by the relative Frobenius is purely inseparable.

theorem relativeFrobenius_residueFieldMap_isPurelyInseparable
    (S : Scheme.{u}) (p : ℕ) [Fact p.Prime] (hS : IsInCharacteristic S p)
    (X : Over S) (x : X.left) :
    (((relativeFrobenius S p hS X).left).residueFieldMap x).hom.IsPurelyInseparable
Tag 0CCC, a lemma

Tag 0CCC in the Stacks Project.

AlgebraicGeometry.relativeFrobenius_toRelativeDifferentials_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Differentials/RelativeFrobenius.lean, line 352. References: EGA 0 (21.3.2), “more general”.

Stacks Project, Tag 0CCC. The canonical map from the differentials of X over S to the differentials of X over its Frobenius twist is an isomorphism.

theorem relativeFrobenius_toRelativeDifferentials_isIso
    (S : Scheme.{u}) (p : ℕ) [Fact p.Prime] (hS : IsInCharacteristic S p) (X : Over S) :
    IsIso (Scheme.Hom.toRelativeDifferentials
      (relativeFrobenius S p hS X).left ((frobeniusTwist S p hS).obj X).hom)
Tag 0CCD, a lemma

Tag 0CCD in the Stacks Project.

AlgebraicGeometry.relativeFrobenius_isFinite, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/RelativeUniversalHomeomorphism.lean, line 106. References: SGA 5 XV (1.Proposition2), “Clause a), special case”.

Stacks Project, Tag 0CCD. The relative Frobenius of an S-scheme locally of finite type over S is finite.

instance relativeFrobenius_isFinite (S : Scheme.{u}) (p : ℕ) [Fact p.Prime]
    (hS : IsInCharacteristic S p) (X : Over S) [LocallyOfFiniteType X.hom] :
    IsFinite (relativeFrobenius S p hS X).left
Tag 0CCE, a lemma

Tag 0CCE in the Stacks Project.

AlgebraicGeometry.geometricallyReduced_iff_isReduced_frobeniusTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/ReducedFrobeniusTwist.lean, line 68.

Stacks Project, Tag 0CCE. A scheme over a field of characteristic p > 0 is geometrically reduced if and only if its Frobenius twist is reduced.

public theorem geometricallyReduced_iff_isReduced_frobeniusTwist
    {k : Type u} [Field k] (p : ℕ) [Fact p.Prime] [CharP k p]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) :
    let hS : IsInCharacteristic (Spec (.of k)) p :=
      Stacks.Frobenius.isInCharacteristic_of_over (Over.mk (𝟙 (Spec (.of k))))
    GeometricallyReduced f ↔
      IsReduced (((frobeniusTwist (Spec (.of k)) p hS).obj (Over.mk f)).left)
Tag 0CCF, a lemma

Tag 0CCF in the Stacks Project.

AlgebraicGeometry.isReduced_frobeniusTwist_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/ReducedTwistTFAE.lean, line 56. The attribute's comment: “reduced_twist_tfae”.

Stacks Project, Tag 0CCF. For a reduced scheme X locally of finite type over a field k of characteristic p > 0, the following are equivalent: the Frobenius twist of X is reduced, X is geometrically reduced over k, and X has a dense open subscheme smooth over k.

theorem isReduced_frobeniusTwist_tfae
    {k : Type u} [Field k] (p : ℕ) [Fact p.Prime] [CharP k p]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsReduced X] [LocallyOfFiniteType f] :
    let hS : IsInCharacteristic (Spec (.of k)) p :=
      Stacks.Frobenius.isInCharacteristic_of_over (Over.mk (𝟙 (Spec (.of k))))
    List.TFAE
      [IsReduced (((frobeniusTwist (Spec (.of k)) p hS).obj (Over.mk f)).left),
        GeometricallyReduced f,
        ∃ U : X.Opens, Dense (U : Set X) ∧ Smooth (U.ι ≫ f)]

AlgebraicGeometry.isReduced_frobeniusTwist_tfae_of_isVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/ReducedTwistTFAE.lean, line 85. The attribute's comment: “reduced_twist_tfae, the variety form with a nonempty smooth open”.

Stacks Project, Tag 0CCF. For a variety X over a field k of characteristic p > 0, the following are equivalent: the Frobenius twist of X is reduced, X is geometrically reduced over k, and there is a nonempty open subscheme of X smooth over k.

theorem isReduced_frobeniusTwist_tfae_of_isVariety
    {k : Type u} [Field k] (p : ℕ) [Fact p.Prime] [CharP k p]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsVariety k f] :
    let hS : IsInCharacteristic (Spec (.of k)) p :=
      Stacks.Frobenius.isInCharacteristic_of_over (Over.mk (𝟙 (Spec (.of k))))
    List.TFAE
      [IsReduced (((frobeniusTwist (Spec (.of k)) p hS).obj (Over.mk f)).left),
        GeometricallyReduced f,
        ∃ U : X.Opens, (U : Set X).Nonempty ∧ Smooth (U.ι ≫ f)]

AlgebraicGeometry.residueDegree_relativeFrobenius_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/RelativeFrobeniusDegree.lean, line 86. The attribute's comment: “frobenius_degree, as the residue degree at the generic point”.

Stacks Project, Tag 0CCF. For a geometrically reduced integral scheme of dimension d, locally of finite type over a field k of characteristic p, the residue degree of the relative Frobenius at the generic point is p ^ d.

theorem residueDegree_relativeFrobenius_genericPoint
    {k : Type u} [Field k] {X : Scheme.{u}} (pX : X ⟶ Spec (.of k))
    (p : ℕ) [Fact p.Prime] [CharP k p] [IsIntegral X] [LocallyOfFiniteType pX]
    (hS : IsInCharacteristic (Spec (.of k)) p) (hgeom : GeometricallyReduced pX)
    (d : ℕ) (hd : topologicalKrullDim X = d) :
    (relativeFrobenius (Spec (.of k)) p hS (Over.mk pX)).left.residueDegree (genericPoint X) =
      p ^ d

AlgebraicGeometry.degreeOver_relativeFrobenius, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/RelativeFrobeniusDegree.lean, line 132. The attribute's comment: “frobenius_degree”.

Stacks Project, Tag 0CCF. For a variety X of dimension d over a field k of characteristic p whose Frobenius twist is reduced, the relative Frobenius of X has degree p ^ d over the twist.

theorem degreeOver_relativeFrobenius
    {k : Type u} [Field k] {X : Scheme.{u}} (pX : X ⟶ Spec (.of k)) [IsVariety k pX]
    (p : ℕ) [Fact p.Prime] [CharP k p] (hS : IsInCharacteristic (Spec (.of k)) p)
    (hred : IsReduced (((frobeniusTwist (Spec (.of k)) p hS).obj (Over.mk pX)).left))
    (d : ℕ) (hd : topologicalKrullDim X = d) :
    letI : LocallyOfFiniteType (Over.mk pX).hom := inferInstanceAs (LocallyOfFiniteType pX)
    letI : IsVariety k ((frobeniusTwist (Spec (.of k)) p hS).obj (Over.mk pX)).hom :=
      isVariety_frobeniusTwist_of_isReduced pX p hred
    degreeOver (relativeFrobenius (Spec (.of k)) p hS (Over.mk pX)).left = p ^ d

AlgebraicGeometry.relativeFrobenius_isDominant, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/RelativeUniversalHomeomorphism.lean, line 117. The attribute's comment: “finite_dominant”.

The relative Frobenius is dominant over a base of prime characteristic.

instance relativeFrobenius_isDominant (S : Scheme.{u}) (p : ℕ) [Fact p.Prime]
    (hS : IsInCharacteristic S p) (X : Over S) :
    IsDominant (relativeFrobenius S p hS X).left

AlgebraicGeometry.isVariety_frobeniusTwist_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/RelativeUniversalHomeomorphism.lean, line 125. The attribute's comment: “twist_variety”.

A reduced Frobenius twist of a variety over a field is a variety.

theorem isVariety_frobeniusTwist_of_isReduced
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsVariety k f] (p : ℕ) [Fact p.Prime] [CharP k p] :
    let hchar : IsInCharacteristic (Spec (.of k)) p := by
      let φ : k →+* Γ(Spec (.of k), ⊤) := (Scheme.ΓSpecIso (.of k)).inv.hom
      change (p : Γ(Spec (.of k), ⊤)) = 0
      rw [← map_natCast φ, CharP.cast_eq_zero k p]
      exact map_zero φ
    IsReduced (((frobeniusTwist (Spec (.of k)) p hchar).obj (Over.mk f)).left) →
      IsVariety k (((frobeniusTwist (Spec (.of k)) p hchar).obj (Over.mk f)).hom)

Declarations registered for the tag:

Tag 0CCG, a remark

Tag 0CCG in the Stacks Project.

AlgebraicGeometry.nFoldFrobeniusTwist, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/Iterated.lean, line 75. The attribute's comment: “n_fold_frobenius_twist”. References: SGA 3 VIIA (4.1), “X^{(p/S)} for S-schemes”; SGA 3 VIIA (4.1.3), “special case”; SGA 3 VIIA (4.3.1); SGA 3 VIIB (4.1.1), “more general”; SGA 3 XVII (4.3.2), “Notation X^(p^n)”.

The n-fold Frobenius twist of an S-scheme is its base change along the n-fold absolute Frobenius of S, regarded as an S-scheme via the second projection.

public noncomputable abbrev nFoldFrobeniusTwist (S : Scheme.{u}) (p : ℕ) [Fact p.Prime]
    (hS : IsInCharacteristic S p) (n : ℕ) (X : Over S) : Over S

AlgebraicGeometry.nFoldRelativeFrobenius, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/Iterated.lean, line 89. The attribute's comment: “n_fold_relative_frobenius”. References: SGA 3 VIIA (4.1), “Fr(X/S) for S-schemes”; SGA 3 VIIA (4.1.3), “special case”; SGA 5 XII (7.3), “more general”; SGA 5 XV (1.Definition3), “more general”.

The morphism from an S-scheme to its n-fold Frobenius twist, with components the n-fold absolute Frobenius and the structure morphism.

public noncomputable def nFoldRelativeFrobenius (S : Scheme.{u}) (p : ℕ) [Fact p.Prime]
    (hS : IsInCharacteristic S p) (n : ℕ) (X : Over S) :
    X ⟶ nFoldFrobeniusTwist S p hS n X

AlgebraicGeometry.nFoldRelativeFrobenius_eq_successiveRelativeFrobenius, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/Iterated.lean, line 313. The attribute's comment: “successive_composition”.

The (n+1)-fold relative Frobenius is the composite of the relative Frobenius morphisms of X and its first n successive twists, under the canonical identifications.

public theorem nFoldRelativeFrobenius_eq_successiveRelativeFrobenius
    (S : Scheme.{u}) (p : ℕ)
    [Fact p.Prime] (hS : IsInCharacteristic S p) (n : ℕ) (X : Over S) :
    nFoldRelativeFrobenius S p hS (n + 1) X =
      successiveRelativeFrobenius S p hS X n

AlgebraicGeometry.relativeFrobenius_nFoldFrobeniusTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/Iterated.lean, line 358. The attribute's comment: “frobenius_on_twists”. References: SGA 3 VIIA (4.3.2), “more general”.

Under the canonical identification of the two orders of Frobenius twisting, relative Frobenius on the m-fold twist is the m-fold base change of relative Frobenius on X.

public theorem relativeFrobenius_nFoldFrobeniusTwist (S : Scheme.{u}) (p : ℕ)
    [Fact p.Prime] (hS : IsInCharacteristic S p) (m : ℕ) (X : Over S) :
    (Over.pullback (absoluteFrobeniusPow S p hS m)).map
        (relativeFrobenius S p hS X) ≫
      (frobeniusTwistCommIso S p hS m X).hom =
        relativeFrobenius S p hS (nFoldFrobeniusTwist S p hS m X)

AlgebraicGeometry.nFoldRelativeFrobenius_eq_twistedRelativeFrobeniusComposite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Frobenius/Iterated.lean, line 441. The attribute's comment: “twisted_composition”.

The (n+1)-fold relative Frobenius is the composite of the first n+1 Frobenius base changes of the relative Frobenius of X.

public theorem nFoldRelativeFrobenius_eq_twistedRelativeFrobeniusComposite
    (S : Scheme.{u}) (p : ℕ) [Fact p.Prime]
    (hS : IsInCharacteristic S p) (n : ℕ) (X : Over S) :
    nFoldRelativeFrobenius S p hS (n + 1) X =
      twistedRelativeFrobeniusComposite S p hS X n

Declarations registered for the tag:

Sources
LeanStacks.Frobenius.absoluteFrobenius · Stacks.Frobenius.absoluteFrobenius_naturality · AlgebraicGeometry.absoluteFrobenius_universalHomeomorphism · AlgebraicGeometry.absoluteFrobenius_isIntegralHom · AlgebraicGeometry.absoluteFrobenius_residueFieldMap_isPurelyInseparable · AlgebraicGeometry.frobeniusTwist · AlgebraicGeometry.relativeFrobenius_existsUnique · AlgebraicGeometry.relativeFrobenius

Section33.37 Glueing dimension one rings#

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

Tag 09MY, a situation

Tag 09MY in the Stacks Project.

Ring.GluingSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GluingSituation.lean, line 60. The attribute's comment: “the standing data”.

Stacks Project, Tag 09MY. The standing data for glueing two rings along a common fraction field: a field K together with two subrings A and B of K, each of which has K as its fraction field. These fit into a commutative square whose fourth corner is the ring R = A ×_K B = A ∩ B.

public structure GluingSituation

Ring.GluingSituation.R, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GluingSituation.lean, line 84. The attribute's comment: “the fourth corner of the square”.

The fourth corner R = A ×_K B of the commutative square, realized as the intersection of A and B in K.

public def R (S : GluingSituation) : Subring S.K

Ring.GluingSituation.coe_R, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GluingSituation.lean, line 108. The attribute's comment: “the identification R = A ∩ B”.

The fourth corner of the square is the intersection A ∩ B inside the common field.

public lemma coe_R (S : GluingSituation) : (S.R : Set S.K) = (S.A : Set S.K) ∩ S.B

Ring.GluingSituation.subtype_comp_algebraMap_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GluingSituation.lean, line 113. The attribute's comment: “commutativity of the square”.

The square commutes: the two composites R → A → K and R → B → K agree.

public lemma subtype_comp_algebraMap_eq (S : GluingSituation) :
    S.A.subtype.comp (algebraMap S.R S.A) = S.B.subtype.comp (algebraMap S.R S.B)

Ring.GluingSituation.equivPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GluingSituation.lean, line 128. The attribute's comment: “the identification R = A ×_K B”.

The fourth corner of the square is the fibre product A ×_K B: the intersection of A and B in K is canonically isomorphic to the subring of A × B of pairs having the same image in K.

public def equivPullback (S : GluingSituation) :
    S.R ≃+* RingHom.pullback S.A.subtype S.B.subtype
Tag 09N0, a lemma

Tag 09N0 in the Stacks Project.

Subring.not_surjective_tensorProduct_iff_exists_isDiscreteValuationRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/TensorProductCriterion.lean, line 97.

For two subrings of a field that is the fraction field of the first, with the first Noetherian and one-dimensional, the multiplication map from their tensor product is not surjective if and only if they are contained in a common discrete valuation subring.

public theorem not_surjective_tensorProduct_iff_exists_isDiscreteValuationRing
    {K : Type u} [Field K] (A B : Subring K)
    [IsFractionRing A K] [IsNoetherianRing A]
    (h_dim : ringKrullDim A = 1) :
    (¬ Function.Surjective
      (Algebra.TensorProduct.lift (B := B) A.subtype.toIntAlgHom
        B.subtype.toIntAlgHom (fun _ _ ↦ Commute.all _ _))) ↔
      ∃ O : Subring K, IsDiscreteValuationRing O ∧ A ≤ O ∧ B ≤ O
Tag 09N1, a lemma

Tag 09N1 in the Stacks Project.

Ring.SemilocalDVRGluingSituation.exists_maximalIdeal_localization_le_of_units_mem_inf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueDVR.lean, line 284. The attribute's comment: “all_units_in_r”.

If every unit of A belongs to A ∩ B, then the DVR B dominates the localization of A at some maximal ideal.

theorem exists_maximalIdeal_localization_le_of_units_mem_inf
    (h_units : ∀ u : S.Aˣ, (((u : S.A) : S.K) ∈ S.R)) :
    ∃ p : MaximalSpectrum S.A,
      LocalSubring.ofPrime S.A p.asIdeal ≤
        ({ toSubring := S.B } : LocalSubring S.K)

Ring.SemilocalDVRGluingSituation.not_surjective_tensorProduct_of_units_mem_inf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueDVR.lean, line 312. The attribute's comment: “all_units_in_r”.

If every unit of A belongs to A ∩ B, then the canonical multiplication map A ⊗[ℤ] B → K is not surjective.

theorem not_surjective_tensorProduct_of_units_mem_inf
    (h_units : ∀ u : S.Aˣ, (((u : S.A) : S.K) ∈ S.R)) :
    ¬ Function.Surjective
      (Algebra.TensorProduct.lift (B := S.B) S.A.subtype.toIntAlgHom
        S.B.subtype.toIntAlgHom (fun _ _ ↦ Commute.all _ _))

Ring.SemilocalDVRGluingSituation.isOpenImmersion_specMap_R_A_of_unit_not_mem_R, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueDVR.lean, line 530. The attribute's comment: “unit_outside_r”.

If a unit of A lies outside R, the map from Spec A to Spec R is an open immersion.

public theorem isOpenImmersion_specMap_R_A_of_unit_not_mem_R
    (h : ¬ ∀ a : S.Aˣ, (((a : S.A) : S.K) ∈ S.R)) :
    IsOpenImmersion
      (Scheme.Spec.map
        (CommRingCat.ofHom ((S.A ⊓ S.B : Subring S.K).inclusion inf_le_left)).op)

Ring.SemilocalDVRGluingSituation.isOpenImmersion_specMap_R_B_of_unit_not_mem_R, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueDVR.lean, line 544. The attribute's comment: “unit_outside_r”.

If a unit of A lies outside R, the map from Spec B to Spec R is an open immersion.

public theorem isOpenImmersion_specMap_R_B_of_unit_not_mem_R
    (h : ¬ ∀ a : S.Aˣ, (((a : S.A) : S.K) ∈ S.R)) :
    IsOpenImmersion
      (Scheme.Spec.map
        (CommRingCat.ofHom ((S.A ⊓ S.B : Subring S.K).inclusion inf_le_right)).op)

Ring.SemilocalDVRGluingSituation.range_specMap_R_A_union_R_B_of_unit_not_mem_R, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueDVR.lean, line 559. The attribute's comment: “unit_outside_r”.

If a unit of A lies outside R, the images of Spec A and Spec B cover Spec R.

public theorem range_specMap_R_A_union_R_B_of_unit_not_mem_R
    (h : ¬ ∀ a : S.Aˣ, (((a : S.A) : S.K) ∈ S.R)) :
    Set.range
        (Scheme.Spec.map
          (CommRingCat.ofHom ((S.A ⊓ S.B : Subring S.K).inclusion inf_le_left)).op).base ∪
      Set.range
        (Scheme.Spec.map
          (CommRingCat.ofHom ((S.A ⊓ S.B : Subring S.K).inclusion inf_le_right)).op).base =
      Set.univ

Ring.SemilocalDVRGluingSituation.tensorProductTo_bijective_of_unit_not_mem_R, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueDVR.lean, line 601. The attribute's comment: “unit_outside_r”.

If a unit of A lies outside R, multiplication identifies A ⊗[R] B with the common fraction field.

public theorem tensorProductTo_bijective_of_unit_not_mem_R
    (h : ¬ ∀ a : S.Aˣ, (((a : S.A) : S.K) ∈ S.R)) :
    Function.Bijective (tensorProductTo S)
Tag 09N2, a lemma

Tag 09N2 in the Stacks Project.

IsIntegralClosure.finite_maximalSpectrum, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/IntegralClosure.lean, line 130. The attribute's comment: “the semilocal assertion”. References: EGA 0 (23.2.6), “K' = K case”.

The integral closure of a semilocal Noetherian domain of dimension at most one in its fraction field is semilocal.

public lemma finite_maximalSpectrum (B : Type u) (K : Type v) (C : Type w)
    [CommRing B] [IsDomain B] [IsNoetherianRing B]
    [Ring.DimensionLEOne B] [Finite (MaximalSpectrum B)] [Field K] [Algebra B K]
    [IsFractionRing B K] [CommRing C] [Algebra B C] [Algebra C K] [IsScalarTower B C K]
    [IsIntegralClosure C B K] :
    Finite (MaximalSpectrum C)

IsIntegralClosure.exists_pow_mul_mem_range, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/IntegralClosure.lean, line 155. The attribute's comment: “the conductor assertion”.

A nonzero element of the Jacobson radical of the integral closure eventually carries every element of the integral closure into the original domain.

public lemma exists_pow_mul_mem_range (B : Type u) (K : Type v) (C : Type w)
    [CommRing B] [IsDomain B] [IsNoetherianRing B]
    [Ring.DimensionLEOne B] [Finite (MaximalSpectrum B)] [Field K] [Algebra B K]
    [IsFractionRing B K] [CommRing C] [Algebra B C] [Algebra C K] [IsScalarTower B C K]
    [IsIntegralClosure C B K]
    (x : C) (hx : x ≠ 0) (hxj : x ∈ Ring.jacobson C) (y : C) :
    ∃ n : ℕ, x ^ n * y ∈ RingHom.range (algebraMap B C)

Declarations registered for the tag:

Tag 09N3, a lemma

Tag 09N3 in the Stacks Project.

Subring.isOpenImmersion_specMap_inf_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueTwo.lean, line 279. The attribute's comment: “the open immersion from A”.

The left-hand subring gives an open immersion into the spectrum of the intersection.

public theorem isOpenImmersion_specMap_inf_left
    (hA : ringKrullDim A = 1) (hB : ringKrullDim B = 1)
    (h_surj : Function.Surjective
      (Algebra.TensorProduct.lift (B := B) A.subtype.toIntAlgHom
        B.subtype.toIntAlgHom (fun _ _ ↦ Commute.all _ _))) :
    IsOpenImmersion
      (Scheme.Spec.map
        (CommRingCat.ofHom ((A ⊓ B : Subring K).inclusion inf_le_left)).op)

Subring.isOpenImmersion_specMap_inf_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueTwo.lean, line 299. The attribute's comment: “the open immersion from B”.

The right-hand subring gives an open immersion into the spectrum of the intersection.

public theorem isOpenImmersion_specMap_inf_right
    (hA : ringKrullDim A = 1) (hB : ringKrullDim B = 1)
    (h_surj : Function.Surjective
      (Algebra.TensorProduct.lift (B := B) A.subtype.toIntAlgHom
        B.subtype.toIntAlgHom (fun _ _ ↦ Commute.all _ _))) :
    IsOpenImmersion
      (Scheme.Spec.map
        (CommRingCat.ofHom ((A ⊓ B : Subring K).inclusion inf_le_right)).op)

Subring.range_specMap_inf_left_union_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueTwo.lean, line 319. The attribute's comment: “the covering assertion”.

The images of the two spectra cover the spectrum of the intersection.

public theorem range_specMap_inf_left_union_right
    (hA : ringKrullDim A = 1) (hB : ringKrullDim B = 1)
    (h_surj : Function.Surjective
      (Algebra.TensorProduct.lift (B := B) A.subtype.toIntAlgHom
        B.subtype.toIntAlgHom (fun _ _ ↦ Commute.all _ _))) :
    Set.range
        (Scheme.Spec.map
          (CommRingCat.ofHom ((A ⊓ B : Subring K).inclusion inf_le_left)).op).base ∪
      Set.range
        (Scheme.Spec.map
          (CommRingCat.ofHom ((A ⊓ B : Subring K).inclusion inf_le_right)).op).base =
      Set.univ

Subring.intersectionTensorProductTo_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueTwo.lean, line 364. The attribute's comment: “the tensor-product assertion”.

Multiplication identifies the tensor product over the intersection with the common fraction field.

public theorem intersectionTensorProductTo_bijective
    (hA : ringKrullDim A = 1) (hB : ringKrullDim B = 1)
    (h_surj : Function.Surjective
      (Algebra.TensorProduct.lift (B := B) A.subtype.toIntAlgHom
        B.subtype.toIntAlgHom (fun _ _ ↦ Commute.all _ _))) :
    Function.Bijective (intersectionTensorProductTo A B)
Tag 09N4, a lemma

Tag 09N4 in the Stacks Project.

Subring.isNoetherianRing_gluedSubring, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueFinite.lean, line 748. The attribute's comment: “the Noetherian assertion”.

The intersection is Noetherian.

lemma isNoetherianRing_gluedSubring : IsNoetherianRing (gluedSubring B)

Subring.finite_maximalSpectrum_gluedSubring, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueFinite.lean, line 755. The attribute's comment: “the semilocal assertion”.

The intersection is semilocal.

lemma finite_maximalSpectrum_gluedSubring : Finite (MaximalSpectrum (gluedSubring B))

Subring.ringKrullDim_gluedSubring, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueFinite.lean, line 762. The attribute's comment: “the dimension assertion”.

The intersection has Krull dimension one.

lemma ringKrullDim_gluedSubring : ringKrullDim (gluedSubring B) = 1

Subring.isOpenImmersion_specMap_gluedSubringInclusion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueFinite.lean, line 770. The attribute's comment: “part (1)”.

The map on affine spectra induced by inclusion of the intersection into each member is an open immersion.

lemma isOpenImmersion_specMap_gluedSubringInclusion (i : ι) :
    AlgebraicGeometry.IsOpenImmersion
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (gluedSubringInclusion B i)))

Subring.iUnion_range_comap_gluedSubringInclusion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueFinite.lean, line 780. The attribute's comment: “part (2)”.

The images of the spectra of the members cover the spectrum of the intersection.

lemma iUnion_range_comap_gluedSubringInclusion :
    (⋃ i, Set.range (PrimeSpectrum.comap (gluedSubringInclusion B i))) = Set.univ

Subring.existsUnique_range_comap_gluedSubringInclusion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/GlueFinite.lean, line 798. The attribute's comment: “part (3)”.

Every closed point of the spectrum of the intersection is in the image of exactly one member of the family.

lemma existsUnique_range_comap_gluedSubringInclusion
    (x : MaximalSpectrum (gluedSubring B)) :
    ∃! i, x.toPrimeSpectrum ∈ Set.range
      (PrimeSpectrum.comap (gluedSubringInclusion B i))
Tag 09N5, a lemma

Tag 09N5 in the Stacks Project.

Ring.exists_ne_zero_inverse_mem_jacobson_of_tensorProduct_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/JacobsonInverse.lean, line 47.

For finitely many Noetherian one-dimensional semilocal subrings of a common fraction field, surjectivity of the corresponding multiplication maps produces a nonzero element whose reciprocal belongs to all their Jacobson radicals.

public theorem exists_ne_zero_inverse_mem_jacobson_of_tensorProduct_surjective
    {K : Type u} [Field K] {ι : Type v} [Finite ι]
    (A : Subring K) (B : ι → Subring K)
    [IsFractionRing A K] [∀ i, IsFractionRing (B i) K]
    [∀ i, IsNoetherianRing (B i)] [∀ i, Finite (MaximalSpectrum (B i))]
    (h_dim : ∀ i, ringKrullDim (B i) = 1)
    (h_surj : ∀ i, Function.Surjective
      (Algebra.TensorProduct.lift (B := B i) A.subtype.toIntAlgHom
        (B i).subtype.toIntAlgHom (fun _ _ ↦ Commute.all _ _))) :
    ∃ x : A, x ≠ 0 ∧ ∀ i, ∃ y : B i,
      (y : K) = (x : K)⁻¹ ∧ y ∈ Ideal.jacobson (⊥ : Ideal (B i))
Tag 0AB2, a lemma

Tag 0AB2 in the Stacks Project.

IsLocalRing.exists_pow_eq_pow_of_eq_at_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/MinimalPrimes.lean, line 94.

Two elements of a Noetherian local ring of dimension at most one which agree at every minimal prime have equal positive powers if one lies in the maximal ideal.

public theorem exists_pow_eq_pow_of_eq_at_minimalPrimes
    {A : Type*} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (hdim : ringKrullDim A ≤ 1) (a₁ a₂ : A)
    (ha₂ : a₂ ∈ IsLocalRing.maximalIdeal A)
    (heq : ∀ p : minimalPrimes A,
      (algebraMap A (@Localization.AtPrime A _ p.1 p.2.isPrime)) a₁ =
        (algebraMap A (@Localization.AtPrime A _ p.1 p.2.isPrime)) a₂) :
    ∃ n : ℕ, 0 < n ∧ a₁ ^ n = a₂ ^ n
Tag 0AB3, a lemma

Tag 0AB3 in the Stacks Project.

IsLocalRing.exists_pow_mem_range_of_sub_mem_nilradical_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/MinimalPrimesPower.lean, line 124.

Stacks 0AB3. An element of the product of the minimal-prime localizations that is congruent, modulo the extended nilradical, to an element of the maximal ideal has a positive power in the image of the original ring.

public theorem exists_pow_mem_range_of_sub_mem_nilradical_map
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (hdim : ringKrullDim A = 1) :
    let L := ∀ p : {q : PrimeSpectrum A // q.asIdeal ∈ minimalPrimes A},
      Localization.AtPrime p.1.asIdeal
    let I : Ideal A := sInf (minimalPrimes A)
      ∀ (f : L) (a : A), a ∈ IsLocalRing.maximalIdeal A →
      f - algebraMap A L a ∈ I.map (algebraMap A L) →
        ∃ n : ℕ, 0 < n ∧ f ^ n ∈ Set.range (algebraMap A L)
Tag 0AB4, a lemma

Tag 0AB4 in the Stacks Project.

IsLocalRing.exists_mem_maximalIdeal_radical_span_eq_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Geometric/DimensionOneRings.lean, line 608.

Stacks Project, Tag 0AB4. An integral subring of the product of the minimal-prime localizations contains the image of a parameter of a one-dimensional Noetherian local ring.

public theorem exists_mem_maximalIdeal_radical_span_eq_of_isIntegral
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (hdim : ringKrullDim A = 1) :
    let L := ∀ p : {q : PrimeSpectrum A // q.asIdeal ∈ minimalPrimes A},
      Localization.AtPrime p.1.asIdeal
    ∀ (K : Type v) [CommRing K] (f : K →+* L), f.IsIntegral →
      ∃ a : A, a ∈ IsLocalRing.maximalIdeal A ∧
        (∃ x : K, f x = algebraMap A L a) ∧
        (Ideal.span {a}).radical = IsLocalRing.maximalIdeal A
Tag 09N6, a lemma

Tag 09N6 in the Stacks Project.

Ideal.primeFamilyCompl, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/Semilocalization.lean, line 45. The attribute's comment: “the multiplicative system”.

The elements outside every prime ideal in a finite family.

public abbrev primeFamilyCompl (s : Finset {p : Ideal A // p.IsPrime}) : Submonoid A

Ideal.finite_maximalSpectrum_localization_primeFamilyCompl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/Semilocalization.lean, line 120. The attribute's comment: “semilocality”.

Localization outside finitely many prime ideals is semilocal.

public theorem finite_maximalSpectrum_localization_primeFamilyCompl
    (s : Finset {p : Ideal A // p.IsPrime})
    {B : Type*} [CommRing B] [Algebra A B] [IsLocalization (primeFamilyCompl s) B] :
    Finite (MaximalSpectrum B)

Ideal.bijOn_under_maximalSpectrum_localization_primeFamilyCompl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/Semilocalization.lean, line 134. The attribute's comment: “the maximal ideals”. References: EGA I (8.1.2), “partial”.

Contraction identifies the maximal ideals of the localization with the maximal members of the finite family of prime ideals.

public theorem bijOn_under_maximalSpectrum_localization_primeFamilyCompl
    (s : Finset {p : Ideal A // p.IsPrime})
    {B : Type*} [CommRing B] [Algebra A B] [IsLocalization (primeFamilyCompl s) B] :
    Set.BijOn (fun m : MaximalSpectrum B => m.asIdeal.under A) Set.univ
      {p : Ideal A | (∃ q ∈ s, p = q.1) ∧
        ∀ q ∈ s, p ≤ q.1 → p = q.1}
Sources
LeanRing.GluingSituation · Ring.GluingSituation.R · Ring.GluingSituation.coe_R · Ring.GluingSituation.subtype_comp_algebraMap_eq · Ring.GluingSituation.equivPullback · Subring.not_surjective_tensorProduct_iff_exists_isDiscreteValuationRing · Ring.SemilocalDVRGluingSituation.exists_maximalIdeal_localization_le_of_units_mem_inf · Ring.SemilocalDVRGluingSituation.not_surjective_tensorProduct_of_units_mem_inf

Section33.38 One dimensional Noetherian schemes#

Section 33.38 of the Stacks Project, Tag 09N7. 14 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09N8, a lemma

Tag 09N8 in the Stacks Project.

Stacks.RetrocompactOneDimensional.isZero_rightDerived_pushforward_of_isRetrocompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RetrocompactOneDimensional/Basic.lean, line 32.

The positive higher direct images of a quasi-coherent module along the inclusion of a retrocompact open subscheme of a scheme whose local rings are Noetherian of dimension at most one vanish.

theorem isZero_rightDerived_pushforward_of_isRetrocompact
    (X : Scheme.{u}) (U : X.Opens)
    (hU : IsRetrocompact (U : Set X))
    (h_noetherian : ∀ x : X, IsNoetherianRing (X.presheaf.stalk x))
    (h_dimension : ∀ x : X, Ring.KrullDimLE 1 (X.presheaf.stalk x))
    (F : U.toScheme.Modules) (hF : F.IsQuasicoherent)
    (p : ℕ) (hp : 0 < p) :
    IsZero (((Scheme.Modules.pushforward U.ι).rightDerived p).obj F)
Tag 09N9, a lemma

Tag 09N9 in the Stacks Project.

AlgebraicGeometry.isAffineOpen_of_isCompact_of_krullDimLE_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/OneDimensionalLocal/QuasiCompactOpen.lean, line 245. References: EGA IV (21.12.9), “more general”.

[Stacks, Tag 09N9]. Let X be an affine scheme all of whose local rings are Noetherian of dimension at most one. Then every quasi-compact open V ⊆ X is affine.

The sections of 𝒪_X over V whose basic open is affine span Γ(X, V) by span_eq_top_of_isCompact, and they cover V by iSup_basicOpen_isAffineOpen_eq, so [Stacks, Tag 01QF] applies. The dimension hypothesis enters only through AlgebraicGeometry.isAffineOpen_of_krullDimLE_one, which makes every open of the spectrum of a local ring of X affine.

theorem isAffineOpen_of_isCompact_of_krullDimLE_one {X : Scheme.{u}} [IsAffine X]
    (hN : ∀ x : X, IsNoetherianRing (X.presheaf.stalk x))
    (hD : ∀ x : X, Ring.KrullDimLE 1 (X.presheaf.stalk x))
    (V : X.Opens) (hV : IsCompact (V : Set X)) : IsAffineOpen V

Stacks.RetrocompactOneDimensional.isAffineOpen_of_isCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RetrocompactOneDimensional/Affine.lean, line 164.

A quasi-compact open subset of an affine scheme is affine when every local ring is Noetherian and has Krull dimension at most one.

theorem isAffineOpen_of_isCompact (X : Scheme.{u}) [IsAffine X]
    (h_noetherian : ∀ x : X, IsNoetherianRing (X.presheaf.stalk x))
    (h_dim : ∀ x : X, Ring.KrullDimLE 1 (X.presheaf.stalk x))
    (U : X.Opens) (hU : IsCompact (U : Set X)) : IsAffineOpen U
Tag 09NA, a lemma

Tag 09NA in the Stacks Project.

Stacks.PicSurjectiveOpen.exists_isInvertible_modulePullback_iso_of_isRetrocompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicSurjectiveOpen/Retrocompact.lean, line 82. The attribute's comment: “surjectivity of the restriction Pic(X) -> Pic(U)”.

Clause (2) of Stacks Tag 09NA. For a retrocompact open U of a scheme X whose complement is discrete and along which the local rings of X are Noetherian of Krull dimension at most one, every invertible 𝒪_U-module is the pullback of an invertible 𝒪_X-module; that is, Pic(X) → Pic(U) is surjective.

theorem exists_isInvertible_modulePullback_iso_of_isRetrocompact
    (hU : IsRetrocompact (U : Set X)) [DiscreteTopology (Uᶜ : Set X)]
    (h_noetherian : ∀ x : X, x ∈ (U : Set X)ᶜ → IsNoetherianRing (X.presheaf.stalk x))
    (h_dimension : ∀ x : X, x ∈ (U : Set X)ᶜ → Ring.KrullDimLE 1 (X.presheaf.stalk x))
    (N : U.toScheme.Modules)
    [IsInvertible U.toScheme.presheaf
      (structureSheafRing U.toScheme.toRingedSpace).property N] :
    ∃ (L : X.Modules)
      (_ : IsInvertible X.presheaf (structureSheafRing X.toRingedSpace).property L),
      Nonempty ((modulePullback U.ι.toLRSHom.toShHom).obj L ≅ N)

AlgebraicGeometry.exists_isInvertible_nonvanishingOpen_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NoetherianDimensionOne/NonvanishingLocus.lean, line 865. The attribute's comment: “nonvanishing_locus”.

Stacks Project, Tag 09NA. A retrocompact open with discrete complement along which the local rings are Noetherian of Krull dimension at most one is the nonvanishing open of a global section of an invertible module.

theorem exists_isInvertible_nonvanishingOpen_eq
    (X : Scheme.{u}) (U : X.Opens)
    (hU : IsRetrocompact (U : Set X))
    [DiscreteTopology (Uᶜ : Set X)]
    (h_noetherian : ∀ x : X, x ∈ (U : Set X)ᶜ →
      IsNoetherianRing (X.presheaf.stalk x))
    (h_dimension : ∀ x : X, x ∈ (U : Set X)ᶜ →
      Ring.KrullDimLE 1 (X.presheaf.stalk x)) :
    ∃ (L : X.Modules)
      (hL : Stacks.SheafOfModules.IsInvertible X.toRingedSpace.presheaf
        (structureSheafRing X.toRingedSpace).property
          L)
      (s : L.sections),
      U = (letI := hL
           Stacks.SheafOfModules.nonvanishingOpen (X := X.toRingedSpace) L s)
Tag 09NB, a lemma

Tag 09NB in the Stacks Project.

AlgebraicGeometry.exists_isInvertible_generatingSections_nonvanishingOpen_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NoetherianDimensionOne/GloballyGenerated.lean, line 1311.

Stacks Project, Tag 09NB. On an integral separated scheme, a nonempty affine open with finite complement along which the local rings are Noetherian of dimension one is the nonvanishing open of a global section of a globally generated invertible module.

theorem exists_isInvertible_generatingSections_nonvanishingOpen_eq
    (X : Scheme.{u}) [IsIntegral X] [X.IsSeparated]
    (U : X.Opens) (hU : IsAffineOpen U) (hU_nonempty : U ≠ ⊥)
    (hfinite : ((U : Set X)ᶜ).Finite)
    (hnoetherian : ∀ x : X, x ∉ U → IsNoetherianRing (X.presheaf.stalk x))
    (hdim : ∀ x : X, x ∉ U → ringKrullDim (X.presheaf.stalk x) = 1) :
    ∃ (L : X.Modules)
      (hL : Stacks.SheafOfModules.IsInvertible X.toRingedSpace.presheaf
        (structureSheafRing X.toRingedSpace).property
          L)
      (s : L.sections),
      Nonempty L.GeneratingSections ∧
        U = (letI := hL
             Stacks.SheafOfModules.nonvanishingOpen (X := X.toRingedSpace) L s)
Tag 09NC, a lemma

Tag 09NC in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.exists_isAmple_of_globallyGenerated_affine_nonvanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleFromAffineNonvanishing/Basic.lean, line 410.

Stacks Project, Tag 09NC. A quasi-compact scheme every point of which lies in an affine nonvanishing locus of a global section of some globally generated invertible sheaf carries an ample invertible sheaf.

The proof is the Stacks Project's. Quasi-compactness gives finitely many pairs (L i, t i) with X = ⋃ X_{t i} and each X_{t i} affine; put B = L 0 ⊗ ⋯ ⊗ L n. For a point x, pick an index j with x ∈ X_{t j} and take σ = s 0 ⊗ ⋯ ⊗ s n where s j = t j and, for i ≠ j, s i is a member of the generating family of L i not vanishing at x (Stacks.SheafOfModules.exists_generatingSection_nonvanishing). Then X_σ = ⋂ X_{s i} contains x and is contained in X_{t j}, so Tag 01PV applied n + 1 times makes it affine. Ampleness is read at exponent 1 through Stacks.SheafOfModules.Invertible.tensorPowerOneIso.

Two invertibility predicates. The hypothesis is spelled with Stacks.SheafOfModules.IsInvertible, which is the one Stacks.SheafOfModules.nonvanishingOpen is defined for, and the conclusion with AlgebraicGeometry.SheafOfModules.IsInvertible, which is the one AlgebraicGeometry.Scheme.Modules.IsAmple is defined for. Both are Props, so the choice of witness does not affect what either statement says, and Stacks.SheafOfModules.isInvertible_iff_algebraicGeometry crosses between them.

public theorem exists_isAmple_of_globallyGenerated_affine_nonvanishing (Y : Scheme.{u})
    (hcpt : CompactSpace Y)
    (hcover : ∀ y : Y, ∃ (M : Y.Modules)
      (hM : Stacks.SheafOfModules.IsInvertible Y.toRingedSpace.sheaf.obj
        (structureSheaf Y.toRingedSpace.sheaf).property M),
      Nonempty M.GeneratingSections ∧
        ∃ t : M.sections,
          y ∈ @Stacks.SheafOfModules.nonvanishingOpen
              Y.toLocallyRingedSpace.toRingedSpace _ M hM t ∧
            IsAffineOpen (@Stacks.SheafOfModules.nonvanishingOpen
              Y.toLocallyRingedSpace.toRingedSpace _ M hM t)) :
    ∃ (M : Y.Modules)
      (hM : AlgebraicGeometry.SheafOfModules.IsInvertible Y.toRingedSpace.presheaf
        (structureSheafRing Y.toRingedSpace).property M),
      @AlgebraicGeometry.Scheme.Modules.IsAmple Y M hM
Tag 09ND, a lemma

Tag 09ND in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.exists_isAmple_of_topologicalKrullDim_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleFromAffineNonvanishing/Basic.lean, line 520.

Stacks Project, Tag 09ND. A Noetherian integral separated scheme of topological Krull dimension one has an ample invertible sheaf.

It is Stacks.AlgebraicGeometry.AmpleDimensionOne.exists_ample_invertible_of_09NC applied to exists_isAmple_of_globallyGenerated_affine_nonvanishing.

public theorem exists_isAmple_of_topologicalKrullDim_one (X : Scheme.{u})
    [IsNoetherian X] [IsIntegral X] [X.IsSeparated]
    (hdim : topologicalKrullDim X = 1) :
    ∃ (L : X.Modules)
      (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.toRingedSpace.presheaf
        (structureSheafRing X.toRingedSpace).property L),
      @AlgebraicGeometry.Scheme.Modules.IsAmple X L hL
Tag 0C0T, a lemma

Tag 0C0T in the Stacks Project.

Stacks.PicFinite.exists_isInvertible_modulePullback_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicSurjectiveFinite/Basic.lean, line 1038.

An invertible module descends along a finite morphism that is an isomorphism away from a discrete closed subset.

theorem exists_isInvertible_modulePullback_iso
    {X Y : AlgebraicGeometry.Scheme.{u}} (f : X ⟶ Y) [AlgebraicGeometry.IsFinite f]
    (V : Y.Opens) [IsIso (f ∣_ V)] [DiscreteTopology (Vᶜ : Set Y)]
    (L : X.Modules)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
      ((Presheaf.isSheaf_iff_isSheaf_comp _ X.presheaf
        (forget₂ CommRingCat RingCat)).mp X.IsSheaf) L) :
    ∃ M : Y.Modules,
      AlgebraicGeometry.SheafOfModules.IsInvertible Y.presheaf
          ((Presheaf.isSheaf_iff_isSheaf_comp _ Y.presheaf
            (forget₂ CommRingCat RingCat)).mp Y.IsSheaf) M ∧
        Nonempty ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M ≅ L)
Tag 09NE, a lemma

Tag 09NE in the Stacks Project.

StacksTag09NE.exists_invertible_of_closed_cover_discrete_intersections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedCoverGlue/Basic.lean, line 837. The attribute's comment: “existence of an invertible sheaf”.

Invertible sheaves on a finite closed cover of a reduced scheme extend when pairwise intersections are discrete.

public theorem exists_invertible_of_closed_cover_discrete_intersections
    {ι : Type v} [Finite ι] (X : Scheme.{u}) [IsReduced X]
    (Z : ι → Scheme.{u}) (f : ∀ i, Z i ⟶ X)
    [∀ i, IsClosedImmersion (f i)]
    (hcover : ∀ x : X, ∃ i z, f i z = x)
    (hdiscrete : ∀ i j, i ≠ j → DiscreteTopology
      (↥(Set.range (f i) ∩ Set.range (f j) : Set X)))
    (L : ∀ i, (Z i).Modules)
    [∀ i, AlgebraicGeometry.SheafOfModules.IsInvertible (Z i).presheaf (Z i).ringCatSheaf.2 (L i)] :
    ∃ (M : X.Modules)
      (_ : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 M),
      ∀ i, Nonempty ((modulePullback (f i).toLRSHom.toShHom).obj M ≅ L i)

StacksTag09NE.exists_invertible_with_sections_of_closed_cover_discrete_intersections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedCoverGlue/Sections.lean, line 782. The attribute's comment: “existence with prescribed sections”.

Sections nonvanishing along the pairwise intersections can be glued along with the invertible sheaves.

public theorem exists_invertible_with_sections_of_closed_cover_discrete_intersections
    {ι : Type v} [Finite ι] (X : Scheme.{u}) [IsReduced X]
    (Z : ι → Scheme.{u}) (f : ∀ i, Z i ⟶ X)
    [∀ i, IsClosedImmersion (f i)]
    (hcover : ∀ x : X, ∃ i z, f i z = x)
    (hdiscrete : ∀ i j, i ≠ j → DiscreteTopology
      (↥(Set.range (f i) ∩ Set.range (f j) : Set X)))
    (L : ∀ i, (Z i).Modules)
    [∀ i, AlgebraicGeometry.SheafOfModules.IsInvertible (Z i).presheaf (Z i).ringCatSheaf.2 (L i)]
    (s : ∀ i, (L i).sections)
    (hs : ∀ i j, i ≠ j → ∀ z : Z i,
      (f i) z ∈ Set.range (f j) →
        z ∈ Stacks.SheafOfModules.nonvanishingLocus (X := (Z i).toRingedSpace) (L i) (s i)) :
    ∃ (M : X.Modules)
      (_ : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 M)
      (t : M.sections),
      ∀ i, ∃ e : (modulePullback (f i).toLRSHom.toShHom).obj M ≅ L i,
        e.hom.val.app (op ⊤)
          (((modulePullbackPushforwardAdjunction (f i).toLRSHom.toShHom).unit.app M).val.app
            (op ⊤) (t.eval (op ⊤))) = (s i).eval (op ⊤)

AlgebraicGeometry.exists_invertible_of_closed_cover_discrete_intersections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleOnClosedCover/Basic.lean, line 542. The attribute's comment: “existence of an invertible sheaf”.

Invertible sheaves on a finite closed cover of a reduced scheme extend when pairwise intersections are discrete.

public theorem exists_invertible_of_closed_cover_discrete_intersections
    {ι : Type v} [Finite ι] (X : Scheme.{u}) [IsReduced X]
    (Z : ι → Scheme.{u}) (f : ∀ i, Z i ⟶ X)
    [∀ i, IsClosedImmersion (f i)]
    (hcover : ∀ x : X, ∃ i z, f i z = x)
    (hdiscrete : ∀ i j, i ≠ j → DiscreteTopology
      (↥(Set.range (f i) ∩ Set.range (f j) : Set X)))
    (L : ∀ i, (Z i).Modules)
    [∀ i, IsInvertible (Z i).presheaf (Z i).ringCatSheaf.2 (L i)] :
    ∃ (M : X.Modules)
      (_ : IsInvertible X.presheaf X.ringCatSheaf.2 M),
      ∀ i, Nonempty ((modulePullback (f i).toLRSHom.toShHom).obj M ≅ L i)

AlgebraicGeometry.exists_invertible_with_sections_of_closed_cover_discrete_intersections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleOnClosedCover/Basic.lean, line 982. The attribute's comment: “existence with prescribed sections”.

Sections nonvanishing along the pairwise intersections can be glued along with the invertible sheaves.

public theorem exists_invertible_with_sections_of_closed_cover_discrete_intersections
    {ι : Type v} [Finite ι] (X : Scheme.{u}) [IsReduced X]
    (Z : ι → Scheme.{u}) (f : ∀ i, Z i ⟶ X)
    [∀ i, IsClosedImmersion (f i)]
    (hcover : ∀ x : X, ∃ i z, f i z = x)
    (_hdiscrete : ∀ i j, i ≠ j → DiscreteTopology
      (↥(Set.range (f i) ∩ Set.range (f j) : Set X)))
    (L : ∀ i, (Z i).Modules)
    [∀ i, IsInvertible (Z i).presheaf (Z i).ringCatSheaf.2 (L i)]
    (s : ∀ i, (L i).sections)
    (hs : ∀ i j, i ≠ j → ∀ z : Z i,
      (f i) z ∈ Set.range (f j) →
        z ∈ Stacks.NonvanishingTrivialize.nonvanishingLocus (Z i).toRingedSpace (L i) (s i)) :
    ∃ (M : X.Modules)
      (_ : IsInvertible X.presheaf X.ringCatSheaf.2 M)
      (t : M.sections),
      ∀ i, ∃ e : (modulePullback (f i).toLRSHom.toShHom).obj M ≅ L i,
        e.hom.val.app (op ⊤)
          (((modulePullbackPushforwardAdjunction (f i).toLRSHom.toShHom).unit.app M).val.app
            (op ⊤) (t.eval (op ⊤))) = (s i).eval (op ⊤)
Tag 09NW, a remark

Tag 09NW in the Stacks Project.

Ideal.inf_eq_bot_of_zeroLocus_union_eq_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/Conductor.lean, line 56.

In a reduced ring, ideals whose zero loci cover the spectrum have zero intersection.

public theorem inf_eq_bot_of_zeroLocus_union_eq_univ
    {A : Type u} [CommRing A] [IsReduced A] (I J : Ideal A)
    (h : PrimeSpectrum.zeroLocus (I : Set A) ∪
      PrimeSpectrum.zeroLocus (J : Set A) = Set.univ) :
    I ⊓ J = ⊥

Ideal.idealMap_quotient_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/Conductor.lean, line 68.

If V(I) ∪ V(J) = Spec A in a reduced ring, the canonical map from I to its extension in A ⧸ J is an isomorphism of A-modules.

public theorem idealMap_quotient_bijective
    {A : Type u} [CommRing A] [IsReduced A] (I J : Ideal A)
    (h : PrimeSpectrum.zeroLocus (I : Set A) ∪
      PrimeSpectrum.zeroLocus (J : Set A) = Set.univ) :
    Function.Bijective (Algebra.idealMap (A ⧸ J) I)

Ideal.multipleQuotientMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DimensionOne/Conductor.lean, line 88.

If V(I) ∪ V(J) = Spec A, the quotient map induces an isomorphism I • P ≅ I • (P ⧸ J • P) for every flat A-module P. In particular this applies when P is projective.

public theorem multipleQuotientMap_bijective
    {A : Type u} [CommRing A] [IsReduced A] (I J : Ideal A)
    {P : Type v} [AddCommGroup P] [Module A P] [Module.Flat A P]
    (h : PrimeSpectrum.zeroLocus (I : Set A) ∪
      PrimeSpectrum.zeroLocus (J : Set A) = Set.univ) :
    Function.Bijective (multipleQuotientMap (P := P) I J)
Tag 09NX, a lemma

Tag 09NX in the Stacks Project.

Stacks.AmpleReducedDimensionOne.exists_isAmple_of_isReduced_of_topologicalKrullDim_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleReducedDimensionOne/Extension.lean, line 502.

[Stacks, Tag 09NX]. A Noetherian, reduced, separated scheme of topological Krull dimension at most one carries an ample invertible sheaf.

The sheaf is the M glued from the components by Tag 09NE: its distinguished global section t serves every point of the overlap T, at exponent one, and Stacks.AmpleReducedDimensionOne.exists_sections_of_notMem_componentOverlap serves every point off T.

The hypothesis is ≤ 1 rather than = 1, so this applies to schemes of dimension zero as well and is stronger than the source's statement.

The name carries isReduced because StacksTag09NX.exists_isAmple_of_topologicalKrullDim_le_one already exists and is a different theorem — Tag 09ND for an integral scheme, which is the first step of this proof rather than its conclusion. Two declarations with that name-tail, one of them in a namespace called StacksTag09NX, would be a twin-constant hazard, so the hypothesis that distinguishes them is in the name.

theorem exists_isAmple_of_isReduced_of_topologicalKrullDim_le_one (Y : Scheme.{u})
    [AlgebraicGeometry.IsNoetherian Y] [AlgebraicGeometry.IsReduced Y] [Y.IsSeparated]
    (hdim : topologicalKrullDim (Y : Type u) ≤ 1) :
    ∃ (M : Y.Modules)
      (_ : AlgebraicGeometry.SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.2 M),
      AlgebraicGeometry.Scheme.Modules.IsAmple Y M
Tag 09NY, a lemma

Tag 09NY in the Stacks Project.

Stacks.LiftInvertible.exists_modulePullback_iso_of_isClosedImmersion_of_dimension_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LiftInvertible/ClosedUnionGlue.lean, line 213.

An invertible module on a closed subscheme of a scheme whose underlying space is Noetherian and has dimension at most one is the pullback of an invertible module on the ambient scheme.

theorem exists_modulePullback_iso_of_isClosedImmersion_of_dimension_le_one
    (X Z : Scheme.{u}) (i : Z ⟶ X) [IsClosedImmersion i]
    [NoetherianSpace X] (hdim : topologicalKrullDim X ≤ 1)
    (L : SheafOfModules.{u} (structureSheafRing Z.toRingedSpace))
    [AlgebraicGeometry.SheafOfModules.IsInvertible Z.presheaf
      (Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat) Z.IsSheaf) L] :
    ∃ (M : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
      (_ : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
        (Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat) X.IsSheaf) M),
      Nonempty ((modulePullback i.toLRSHom.toShHom).obj M ≅ L)
Tag 09NZ, a proposition

Tag 09NZ in the Stacks Project.

Stacks.AmpleNoetherianDimensionOne.exists_isAmple_of_isNoetherian_of_topologicalKrullDim_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleNoetherianDimensionOne/Basic.lean, line 117. The attribute's comment: “with dimension at most one in place of the source's dimension one”.

[Stacks, Tag 09NZ]. A Noetherian separated scheme of topological Krull dimension at most one carries an ample invertible module.

The reduction Z of X is Noetherian, reduced, separated and of dimension at most one, so it has an ample invertible module by [Stacks, Tag 09NX]; that module is i^* L for an invertible module L on X by [Stacks, Tag 09NY]; and L is ample because i^* L is, by the converse half of [Stacks, Tag 09MS] applied to the surjective closed immersion i : Z ⟶ X.

theorem exists_isAmple_of_isNoetherian_of_topologicalKrullDim_le_one
    (X : Scheme.{u}) [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated]
    (hdim : topologicalKrullDim (X : Type u) ≤ 1) :
    ∃ (L : X.Modules)
      (_ : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L),
      AlgebraicGeometry.Scheme.Modules.IsAmple X L
Tag 09P0, a remark

Tag 09P0 in the Stacks Project.

Stacks.AmpleNoetherianReduction.exists_isAmple_of_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleNoetherianReduction/Basic.lean, line 234. The attribute's comment: “granted the converse half of Tag 09MW as AmpleDescendsAlongThickening”.

[Stacks, Tag 09P0]. A scheme whose reduction is a Noetherian separated scheme of dimension at most one has an ample invertible sheaf, granted the converse half of [Stacks, Tag 09MW].

The hypotheses are on the reduction only; X itself is not assumed Noetherian, which is exactly what distinguishes this from [Stacks, Tag 09NZ] and what forces Tag 09MW in place of [Stacks, Tag 09MS].

theorem exists_isAmple_of_reduction (X : Scheme.{u})
    (hdesc : AmpleDescendsAlongThickening.{u})
    [IsNoetherian (vanishingIdeal (⊤ : Closeds X)).subscheme]
    [(vanishingIdeal (⊤ : Closeds X)).subscheme.IsSeparated]
    (hdim : topologicalKrullDim ((vanishingIdeal (⊤ : Closeds X)).subscheme : Type u) ≤ 1) :
    ∃ (L : X.Modules) (hL : IsInvertibleModule X L), @IsAmple X L hL

Stacks.AmpleNoetherianReduction.exists_isAmple_of_reduction_of_topologicalKrullDim_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleNoetherianReduction/Unconditional.lean, line 68.

[Stacks, Tag 09P0]. A scheme whose reduction is a Noetherian separated scheme of dimension at most one has an ample invertible sheaf.

The hypotheses are on the reduction X_red = (vanishingIdeal ⊤).subscheme only; X itself is not assumed Noetherian.

theorem exists_isAmple_of_reduction_of_topologicalKrullDim_le_one (X : Scheme.{u})
    [IsNoetherian (vanishingIdeal (⊤ : Closeds X)).subscheme]
    [(vanishingIdeal (⊤ : Closeds X)).subscheme.IsSeparated]
    (hdim : topologicalKrullDim ((vanishingIdeal (⊤ : Closeds X)).subscheme : Type u) ≤ 1) :
    ∃ (L : X.Modules) (hL : IsInvertibleModule X L), @IsAmple X L hL
Tag 0C0U, a lemma

Tag 0C0U in the Stacks Project.

Stacks.PicFinite.exists_isInvertible_modulePullback_iso_of_isClosedImmersion_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicSurjectiveFinite/DenseClosedImmersion.lean, line 105.

Stacks Project, Tag 0C0U. Let f : X ⟶ Y be a finite morphism of schemes with Y of Noetherian underlying space and dimension at most one, and suppose f is a closed immersion over a dense open subset V of Y. Then every invertible 𝒪_X-module is the pullback of an invertible 𝒪_Y-module.

The morphism factors as f.toImage ≫ f.imageι through its scheme-theoretic image Z. Over U := f.imageι ⁻¹ᵁ V the first factor is a closed immersion with trivial kernel ideal sheaf, hence an isomorphism, and the part of Z outside U is discrete, so Tag 0C0T descends the module to Z; Tag 09NY then lifts it across the closed immersion f.imageι to Y.

theorem exists_isInvertible_modulePullback_iso_of_isClosedImmersion_restrict
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsFinite f] [NoetherianSpace Y]
    (hdim : topologicalKrullDim Y ≤ 1) (V : Y.Opens) (hV : Dense (V : Set Y))
    [IsClosedImmersion (f ∣_ V)]
    (L : X.Modules)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
      ((Presheaf.isSheaf_iff_isSheaf_comp _ X.presheaf
        (forget₂ CommRingCat RingCat)).mp X.IsSheaf) L) :
    ∃ M : Y.Modules,
      AlgebraicGeometry.SheafOfModules.IsInvertible Y.presheaf
          ((Presheaf.isSheaf_iff_isSheaf_comp _ Y.presheaf
            (forget₂ CommRingCat RingCat)).mp Y.IsSheaf) M ∧
        Nonempty ((AlgebraicGeometry.Scheme.Modules.pullback f).obj M ≅ L)
Sources
LeanStacks.RetrocompactOneDimensional.isZero_rightDerived_pushforward_of_isRetrocompact · AlgebraicGeometry.isAffineOpen_of_isCompact_of_krullDimLE_one · Stacks.RetrocompactOneDimensional.isAffineOpen_of_isCompact · Stacks.PicSurjectiveOpen.exists_isInvertible_modulePullback_iso_of_isRetrocompact · AlgebraicGeometry.exists_isInvertible_nonvanishingOpen_eq · AlgebraicGeometry.exists_isInvertible_generatingSections_nonvanishingOpen_eq · AlgebraicGeometry.Scheme.Modules.exists_isAmple_of_globallyGenerated_affine_nonvanishing · AlgebraicGeometry.Scheme.Modules.exists_isAmple_of_topologicalKrullDim_one

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.