53.15 Glueing and squishing to 53.25 Contracting to a stable…

Section53.15 Glueing and squishing #

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

Tag 0C1I, a lemma

Tag 0C1I in the Stacks Project.

Algebra.algEquiv_prod_or_dualNumber_of_natCard_subalgebra_eq_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SubalgebraClassification.lean, line 270.

Stacks Project, Tag 0C1I. An algebra over an algebraically closed field with exactly two subalgebras is isomorphic, as an algebra, either to the product algebra or to the dual numbers.

theorem algEquiv_prod_or_dualNumber_of_natCard_subalgebra_eq_two
    (k : Type u) (A : Type v) [Field k] [IsAlgClosed k] [CommRing A] [Algebra k A]
    (h : Nat.card (Subalgebra k A) = 2) :
    Nonempty (A ≃ₐ[k] k × k) ∨ Nonempty (A ≃ₐ[k] DualNumber k)

Algebra.algEquiv_prod_or_dualNumber_of_no_intermediateSubalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SubalgebraClassification.lean, line 285.

Stacks Project, Tag 0C1I. An algebra over an algebraically closed field with no proper intermediate subalgebra is either the product algebra or the algebra of dual numbers.

theorem algEquiv_prod_or_dualNumber_of_no_intermediateSubalgebra
    (k : Type u) (A : Type v) [Field k] [IsAlgClosed k] [CommRing A] [Algebra k A]
    (h_ne : (⊥ : Subalgebra k A) ≠ ⊤)
    (h : ∀ B : Subalgebra k A, B = ⊥ ∨ B = ⊤) :
    Nonempty (A ≃ₐ[k] k × k) ∨ Nonempty (A ≃ₐ[k] DualNumber k)

Tag 0C1J, an example

Tag 0C1J in the Stacks Project.

AlgebraicGeometry.IsGlueingTwoPoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/GlueingTwoPoints.lean, line 142. The attribute's comment: “glueing_two_points”.

A morphism of algebraic k-schemes glues the distinct rational points a and b if they have the same image, the morphism is finite and is an isomorphism off that image, and the additive difference of evaluation at a and b gives the skyscraper quotient of its pushforward structure sheaf.

def IsGlueingTwoPoints {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (a b : Spec (.of k) ⟶ X') : Prop

Stacks.GlueSquishUnits.isShortExact_units_of_isGlueingTwoPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/GlueingUnitsSequence.lean, line 839. The attribute's comment: “the units short exact sequence”.

The short exact sequence of sheaves of units of a glueing of two rational points. If f : X' ⟶ X glues the distinct rational points a and b of X' to the point x = f(a) = f(b) of X, then

1 ⟶ 𝒪_X^* ⟶ f_*𝒪_{X'}^* ⟶ (k^*)_x ⟶ 1

is a short exact sequence of sheaves of abelian groups on X, the first map being pullback of units along f and the second the ratio h ↦ h(a) h(b)⁻¹ of the two values of a unit. Both maps are pinned down on sections, so the sequence is the one of [Stacks, Tag 0C1J] and not merely some exact sequence with those terms.

This is the input from which [Stacks, Tag 0C1M] obtains the exact sequence k^* ⟶ Pic(X) ⟶ Pic(X') ⟶ 0: the five-term low-degree cohomology sequence over U = ⊤, Stacks.Cohomology.AbelianColimit.H'longExactSequence_exact, gives H⁰(X, f_*𝒪_{X'}^*) ⟶ k^* ⟶ H¹(X, 𝒪_X^*) ⟶ H¹(X, f_*𝒪_{X'}^*), and Stacks.Cohomology.Generators.h1UnitsAddEquivPicardGroup identifies the first cohomology of a units sheaf with the Picard group.

theorem isShortExact_units_of_isGlueingTwoPoints {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (a b : Spec (.of k) ⟶ X')
    (h : IsGlueingTwoPoints f a b) (hab : a ≫ f = b ≫ f) :
    ∃ (φ : unitsSheaf X.toLocallyRingedSpace.toRingedSpace ⟶
        (TopCat.Sheaf.pushforward AddCommGrpCat.{u} f.base).obj
          (unitsSheaf X'.toLocallyRingedSpace.toRingedSpace))
      (ψ : (TopCat.Sheaf.pushforward AddCommGrpCat.{u} f.base).obj
          (unitsSheaf X'.toLocallyRingedSpace.toRingedSpace) ⟶
        skyscraperUnitsSheaf (k := k) X (gluedPoint f a))
      (hzero : φ ≫ ψ = 0),
      (ShortComplex.mk φ ψ hzero).ShortExact ∧
      (∀ (U : X.Opens) (s : Γ(X, U)ˣ),
        φ.hom.app (op U) (Additive.ofMul s) =
          Additive.ofMul (Units.map (f.app U).hom.toMonoidHom s)) ∧
      (∀ (U : X.Opens) (hz : gluedPoint f a ∈ U)
        (ha : a.base (IsLocalRing.closedPoint k) ∈ f ⁻¹ᵁ U)
        (hb : b.base (IsLocalRing.closedPoint k) ∈ f ⁻¹ᵁ U) (s : Γ(X', f ⁻¹ᵁ U)ˣ),
        skyscraperUnitsEval X (gluedPoint f a) hz
            (ψ.hom.app (op U) (Additive.ofMul s)) =
          Additive.ofMul (unitRatioAt a b (f ⁻¹ᵁ U) ha hb s))

Tag 0C1K, an example

Tag 0C1K in the Stacks Project.

Stacks.SquishSheafSequence.shortExact_units_of_isSquishingTangentVector, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingPicardSequence.lean, line 671. The attribute's comment: “the units short exact sequence”.

The short exact sequence of sheaves of units of the squishing of a tangent vector. If f : X' ⟶ X squishes the tangent vector ϑ of X' to the rational point x of X, then

1 ⟶ 𝒪_X^* ⟶ f_*𝒪_{X'}^* ⟶ (k, +)_x ⟶ 1

is a short exact sequence of sheaves of abelian groups on X, the first map being pullback of units along f and the second the logarithmic ε-derivative along ϑ. Both maps are pinned down on sections — by Stacks.GlueSquishUnits.unitsPushforwardMap_app and Stacks.SquishSheafSequence.epsilonLogDerivSheafHom_app — so the sequence is the one of [Stacks, Tag 0C1N] and not merely some exact sequence with those terms.

Injectivity of the first map and exactness in the middle hold already on sections over every open. Surjectivity of the second is local at the contracted point, where it is the surjectivity of the logarithmic ε-derivative on the units of the stalk of f_*𝒪_{X'}; away from the contracted point the skyscraper has no sections.

theorem shortExact_units_of_isSquishingTangentVector {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (θ : Spec (.of (DualNumber k)) ⟶ X')
    (h : AlgebraicGeometry.IsSquishingTangentVector f θ) :
    (ShortComplex.mk (unitsPushforwardMap f) (epsilonLogDerivSheafHom f θ)
      (unitsPushforwardMap_comp_epsilonLogDerivSheafHom f θ h)).ShortExact

AlgebraicGeometry.IsSquishingTangentVector, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingTangentVector.lean, line 77. The attribute's comment: “squishing_tangent_vector”.

A morphism of algebraic k-schemes squishes a tangent vector if that vector is a closed immersion which is contracted to a rational point, the morphism is finite and an isomorphism off that point, and taking the coefficient of ε gives the skyscraper quotient of the pushforward structure sheaf.

def IsSquishingTangentVector {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (θ : Spec (.of (DualNumber k)) ⟶ X') : Prop

Stacks.SquishSheafSequence.shortExact_of_isSquishingTangentVector, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingUnitsSequence.lean, line 185. The attribute's comment: “the short exact sequence of sheaves”.

The short exact sequence of sheaves attached to the squishing of a tangent vector.

If f : X' ⟶ X squishes the tangent vector ϑ of X' to the rational point x of X, then there is a map of additive sheaves ψ : f_*𝒪_{X'} ⟶ (k, +)_x to the additive skyscraper at x for which

0 → 𝒪_X → f_*𝒪_{X'} → (k, +)_x → 0

is short exact, and ψ is given on every neighbourhood U of x by the coefficient of ε of the restriction along ϑ of a section of 𝒪_{X'} over f⁻¹U. This is the clause of [Stacks, Tag 0C1K] that the exactness statements of Tags 0C1M and 0C1N consume.

theorem shortExact_of_isSquishingTangentVector {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (θ : Spec (.of (DualNumber k)) ⟶ X')
    (h : AlgebraicGeometry.IsSquishingTangentVector f θ) :
    ∃ (ψ : pushforwardAddSheaf f ⟶ skyscraperAddSheaf (k := k) X
        ((θ ≫ f).base (IsLocalRing.closedPoint (DualNumber k))))
      (hzero : structureToPushforwardAddSheaf f ≫ ψ = 0),
      (ShortComplex.mk (structureToPushforwardAddSheaf f) ψ hzero).ShortExact ∧
        ∀ (U : X.Opens)
          (hx : (θ ≫ f).base (IsLocalRing.closedPoint (DualNumber k)) ∈ U)
          (s : Γ(X', f ⁻¹ᵁ U)),
          ψ.hom.app (op U) s =
            skyscraperAddSheafMk X ((θ ≫ f).base (IsLocalRing.closedPoint (DualNumber k))) hx
              (epsilonCoefficientAt θ (f ⁻¹ᵁ U) (by exact hx) s)

Tag 0C1L, a lemma

Tag 0C1L in the Stacks Project.

Stacks.GlueSquishFactor.algEquiv_prod_or_dualNumber_of_minimal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/ElementaryFactorization.lean, line 351. The attribute's comment: “the local algebra of a minimal step”.

The local algebra of a minimal step of [Stacks, Tag 0C1L]. Let k be an algebraically closed field, let A be a local k-algebra whose residue field is k (hypothesis hres: every element of A is a scalar modulo the maximal ideal), and let B be a module-finite A-algebra which is not generated by A (hypothesis hne) and admits no A-subalgebra strictly between A and B (hypothesis hmin). Then the fibre B ⧸ m_A B is, as a k-algebra, either the product k × k or the dual numbers k[ε].

In the source this is the whole of the case n = 1: with A = 𝒪_{X, x} and B = (f_*𝒪_{X'})_x, the absence of a proper intermediate subalgebra forces B = A + m_A B (Nakayama) and then forces the fibre C = B / m_A B to have exactly two k-subalgebras, so [Stacks, Tag 0C1I] applies. The two outcomes are what make the step a glueing of two points respectively a squishing of a tangent vector.

This is the mathematical heart of [Stacks, Tag 0C1L], but not the whole lemma: see the implementation notes of this file for the geometric statements that remain.

theorem algEquiv_prod_or_dualNumber_of_minimal (k : Type u) (A B : Type v) [Field k]
    [IsAlgClosed k] [CommRing A] [Algebra k A] [IsLocalRing A] [CommRing B] [Algebra k B]
    [Algebra A B] [IsScalarTower k A B] [Module.Finite A B]
    (hres : ∀ a : A, ∃ c : k, a - algebraMap k A c ∈ IsLocalRing.maximalIdeal A)
    (hne : (⊥ : Subalgebra A B) ≠ ⊤) (hmin : ∀ E : Subalgebra A B, E = ⊥ ∨ E = ⊤) :
    Nonempty ((B ⧸ (IsLocalRing.maximalIdeal A).map (algebraMap A B)) ≃ₐ[k] k × k) ∨
      Nonempty ((B ⧸ (IsLocalRing.maximalIdeal A).map (algebraMap A B)) ≃ₐ[k] DualNumber k)

Stacks.GlueSquishFactor.IsElementaryStep, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/ElementaryFactorization.lean, line 550. The attribute's comment: “the elementary modifications”.

One step of the factorization of [Stacks, Tag 0C1L]: a morphism of algebraic k-schemes which either glues two rational points ([Stacks, Tag 0C1J]) or squishes a tangent vector ([Stacks, Tag 0C1K]).

def IsElementaryStep {k : Type u} [Field k] [IsAlgClosed k] {Y' Y : Over (Spec (.of k))}
    (f : Y' ⟶ Y) : Prop

Stacks.GlueSquishFactor.IsElementaryChain, an inductive in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/ElementaryFactorization.lean, line 570. The attribute's comment: “the factorization, as an inductive predicate”.

The conclusion of [Stacks, Tag 0C1L], as a predicate on one morphism. f is a composite of finitely many elementary modifications and isomorphisms, which is the content of the source's chain X' = X_n ⟶ ⋯ ⟶ X_0 = X together with its endpoint identifications. The recursor is the induction on the length that the source's proof performs.

inductive IsElementaryChain (k : Type u) [Field k] [IsAlgClosed k] :
    {Y' Y : Over (Spec (.of k))} → (Y' ⟶ Y) → Prop

Stacks.GlueSquishFactor.toIntermediateOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/IntermediateFactorization.lean, line 136. The attribute's comment: “the intermediate factorization attached to a subalgebra”.

The morphism X' ⟶ Spec_X(A) over X attached to a morphism ψ : A ⟶ f_* 𝒪_{X'} of 𝒪_X-algebras. It is the morphism corresponding to ψ under the universal property of the relative spectrum, read through the identification (Spec_X(A) ⟶ X)_* 𝒪 ≅ A.

def toIntermediateOver : Over.mk f ⟶ Over.mk (relativeSpecToBase A)

Stacks.GlueSquishFactor.toIntermediate_comp_relativeSpecToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/IntermediateFactorization.lean, line 155. The attribute's comment: “the intermediate factorization attached to a subalgebra”.

The factorization of f attached to a morphism ψ : A ⟶ f_* 𝒪_{X'}. The morphism X' ⟶ Spec_X(A) of Stacks.GlueSquishFactor.toIntermediate, followed by the structure morphism of the relative spectrum, is f.

theorem toIntermediate_comp_relativeSpecToBase :
    toIntermediate f A ψ ≫ relativeSpecToBase A = f

Stacks.GlueSquishFactor.isoRelativeSpecOfAffine, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/IntermediateFactorization.lean, line 226. The attribute's comment: “every affine intermediate factorization comes from a subalgebra”.

A scheme affine over X is the relative spectrum of its algebra of functions over X. For g : Y ⟶ X affine, the comparison morphism Y ⟶ Spec_X(g_* 𝒪_Y) is an isomorphism of schemes over X. This is [Stacks, Tag 01SA] in the form used by [Stacks, Tag 0C1L]: an intermediate factorization with affine second half is a relative spectrum.

def isoRelativeSpecOfAffine :
    Over.mk g ≅ Over.mk (relativeSpecToBase (pushforwardAlgebra g))

Stacks.GlueSquishFactor.toIntermediateOver_factorizationAlgebraHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/IntermediateFactorization.lean, line 245. The attribute's comment: “every affine intermediate factorization comes from a subalgebra”.

Every intermediate factorization with affine second half comes from an algebra. For a factorization f = u ≫ g with g affine, the comparison isomorphism Y ≅ Spec_X(g_* 𝒪_Y) carries u to the morphism attached by Stacks.GlueSquishFactor.toIntermediateOver to the algebra map g_* 𝒪_Y ⟶ f_* 𝒪_{X'} of the factorization.

theorem toIntermediateOver_factorizationAlgebraHom :
    toIntermediateOver f (pushforwardAlgebra g) (factorizationAlgebraHom f u g hu) =
      (Over.homMk u hu : Over.mk f ⟶ Over.mk g) ≫ toRelativeSpecOfAffine g

Stacks.GlueSquishFactor.exists_split_of_algebraHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SplittingStep.lean, line 315. The attribute's comment: “the splitting attached to a finite intermediate subalgebra”.

The splitting step of [Stacks, Tag 0C1L]. Let f : X' ⟶ X be a finite morphism of schemes over a base S with 𝒪_X ⊂ f_*𝒪_{X'} which is an isomorphism over an open U of X, and let 𝒜 be a finite quasi-coherent sheaf of 𝒪_X-algebras with an injection ψ : 𝒜 ⟶ f_*𝒪_{X'} of 𝒪_X-algebras. Then f factors over S as p ≫ q with

q : Spec_X(𝒜) ⟶ X finite, with 𝒪_X ⊂ q_*𝒪, and an isomorphism over U;

p : X' ⟶ Spec_X(𝒜) finite, with 𝒪_{Spec_X(𝒜)} ⊂ p_*𝒪_{X'}, and an isomorphism over q⁻¹U.

Finiteness of q is the finiteness of 𝒜; finiteness of p is finiteness of f cancelled against it; 𝒪_X ⊂ q_*𝒪 is the chain 𝒪_X ⊂ 𝒜 ⊂ f_*𝒪_{X'}; 𝒪_{Spec_X(𝒜)} ⊂ p_*𝒪_{X'} is ψ propagated from the preimages of the affine opens of X to every open of Spec_X(𝒜) by Stacks.GlueSquishFactor.mono_hom_pushforwardAlgebra_toIntermediate; and the two statements over U are the squeeze Stacks.GlueSquishFactor.isIso_morphismRestrict_relativeSpecToBase together with cancellation of q ∣_ U out of f ∣_ U.

The last clause is the capture clause: over every open V of X the sections of 𝒜 are sections of the intermediate scheme, by Stacks.GlueSquishFactor.mem_range_appLE_toIntermediate. It is what makes the splitting nontrivial — without it a splitting is produced even by 𝒜 = 𝒪_X, for which q is an isomorphism and nothing has happened.

theorem exists_split_of_algebraHom {S : Scheme.{u}} {W' W : Over S} (f : W' ⟶ W)
    [IsFinite f.left] [Mono (pushforwardAlgebra f.left).hom] (A : AlgebraSheaf W.left)
    [AlgebraSheaf.IsQuasicoherent A] (hAfin : AlgebraSheaf.IsFinite A)
    (ψ : A ⟶ pushforwardAlgebra f.left)
    (hψ : ∀ V : W.left.Opens, Function.Injective (ψ.right.hom.app (op V)).hom)
    {U : W.left.Opens} (hU : IsIso (f.left ∣_ U)) :
    ∃ (Z : Over S) (p : W' ⟶ Z) (q : Z ⟶ W), p ≫ q = f ∧ IsFinite q.left ∧
      Mono (pushforwardAlgebra q.left).hom ∧ IsIso (q.left ∣_ U) ∧ IsFinite p.left ∧
      Mono (pushforwardAlgebra p.left).hom ∧ IsIso (p.left ∣_ (q.left ⁻¹ᵁ U)) ∧
      ∀ (V : W.left.Opens) (hle : f.left ⁻¹ᵁ V ≤ p.left ⁻¹ᵁ (q.left ⁻¹ᵁ V))
        (s : Γ(W'.left, f.left ⁻¹ᵁ V)), s ∈ Set.range (ψ.right.hom.app (op V)).hom →
          s ∈ Set.range (p.left.appLE (q.left ⁻¹ᵁ V) (f.left ⁻¹ᵁ V) hle).hom

Stacks.GlueSquishFactor.exists_split_isAlmostIso_of_algebraHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SplittingStep.lean, line 364. The attribute's comment: “the splitting, read against the hypotheses of the lemma”.

The splitting step of [Stacks, Tag 0C1L], read against the hypotheses of the lemma. An almost isomorphism of algebraic k-schemes and a finite quasi-coherent 𝒪_X-subalgebra 𝒜 of f_*𝒪_{X'} give a factorization f = p ≫ q over Spec k in which both halves are again almost isomorphisms, so both satisfy every hypothesis of the source.

Together with a measure which drops along this factorization, this is the hypothesis hsplit of Stacks.GlueSquishFactor.isElementaryChain_of_isAlmostIso. No measure is constructed here. The last clause records that the splitting captures the sections of 𝒜, which is what distinguishes it from the trivial splitting by 𝒜 = 𝒪_X.

theorem exists_split_isAlmostIso_of_algebraHom {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Over (Spec (.of k))} (f : X' ⟶ X) (hf : IsAlmostIso f) (A : AlgebraSheaf X.left)
    [AlgebraSheaf.IsQuasicoherent A] (hAfin : AlgebraSheaf.IsFinite A)
    (ψ : A ⟶ pushforwardAlgebra f.left)
    (hψ : ∀ V : X.left.Opens, Function.Injective (ψ.right.hom.app (op V)).hom) :
    ∃ (Z : Over (Spec (.of k))) (p : X' ⟶ Z) (q : Z ⟶ X),
      p ≫ q = f ∧ IsAlmostIso q ∧ IsAlmostIso p ∧
      ∀ (V : X.left.Opens) (hle : f.left ⁻¹ᵁ V ≤ p.left ⁻¹ᵁ (q.left ⁻¹ᵁ V))
        (s : Γ(X'.left, f.left ⁻¹ᵁ V)), s ∈ Set.range (ψ.right.hom.app (op V)).hom →
          s ∈ Set.range (p.left.appLE (q.left ⁻¹ᵁ V) (f.left ⁻¹ᵁ V) hle).hom

Stacks.GlueSquishFactor.IsAlmostIso.isElementaryChain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingProducer.lean, line 615.

[Stacks, Tag 0C1L]. A finite morphism of algebraic k-schemes which is injective on structure sheaves and an isomorphism away from a finite set of points is a composite of glueings of two rational points and squishings of tangent vectors.

theorem IsAlmostIso.isElementaryChain {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Over (Spec (.of k))} (f : X' ⟶ X) (hf : IsAlmostIso f) : IsElementaryChain k f

Tag 0C1M, a lemma

Tag 0C1M in the Stacks Project.

Stacks.GluePicard.surjective_schemePullbackClassHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/GlueingPicard.lean, line 99. The attribute's comment: “surjectivity”.

Pullback of invertible modules along the glueing of two rational points is surjective on Picard groups. The glueing is finite and is an isomorphism away from a single point, so [Stacks, Tag 0C0T] descends a representative of any class on X' to X.

theorem surjective_schemePullbackClassHom {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (a b : Spec (.of k) ⟶ X')
    (h : AlgebraicGeometry.IsGlueingTwoPoints f a b) :
    Function.Surjective (Stacks.Picard.schemePullbackClassHom f)

Stacks.GluePicard.exists_globalUnit_sectionAt_eq_of_ne_connectedComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/GlueingPicard.lean, line 224. The attribute's comment: “the lifting criterion for vanishing at points on different components”.

The first map of the sequence of Stacks Tag 0C1M is zero when the two glued points lie on different connected components of X', in the form that the connecting homomorphism consumes: every scalar c is the ratio of the values at a and at b of a unit on all of X', so the invertible module obtained by glueing the fibres at a and b with ratio c is trivial.

theorem exists_globalUnit_sectionAt_eq_of_ne_connectedComponents
    {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (a b : Spec (.of k) ⟶ X')
    (h : AlgebraicGeometry.IsGlueingTwoPoints f a b)
    (hab : ConnectedComponents.mk (a.base (IsLocalRing.closedPoint k)) ≠
      ConnectedComponents.mk (b.base (IsLocalRing.closedPoint k))) (c : kˣ) :
    ∃ s : Γ(X', ⊤)ˣ,
      AlgebraicGeometry.sectionAt a ⊤ (Opens.mem_top _) (s : Γ(X', ⊤)) = (c : k) ∧
        AlgebraicGeometry.sectionAt b ⊤ (Opens.mem_top _) (s : Γ(X', ⊤)) = 1

Stacks.GluePicard.schemePullbackClassHom_eq_zero_iff_exists_picardGluingHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/GlueingPicardExactness.lean, line 154. The attribute's comment: “exactness at Pic(X): the kernel of pullback is the image of k^*”.

Exactness at Pic(X) of the sequence of [Stacks, Tag 0C1M]. For k algebraically closed and f : X' ⟶ X the glueing of the two rational points a and b of X', a Picard class of X pulls back to zero on X' exactly when it is the value of the gluing homomorphism Stacks.GluePicard.picardGluingHom at a scalar; that is, the kernel of Pic(X) ⟶ Pic(X') is the image of k^* ⟶ Pic(X).

theorem schemePullbackClassHom_eq_zero_iff_exists_picardGluingHom {k : Type u} [Field k]
    [IsAlgClosed k] {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (a b : Spec (.of k) ⟶ X')
    (h : AlgebraicGeometry.IsGlueingTwoPoints f a b) (L : Stacks.Picard.ofScheme X) :
    Stacks.Picard.schemePullbackClassHom f L = 0 ↔
      ∃ c : Additive kˣ, picardGluingHom f a b h c = L

Stacks.GluePicard.exact_picardGluingHom_schemePullbackClassHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/GlueingPicardExactness.lean, line 179. The attribute's comment: “exactness at Pic(X): the kernel of pullback is the image of k^*”.

Exactness at Pic(X) of the sequence of [Stacks, Tag 0C1M], in the Function.Exact spelling: the kernel of pullback of Picard classes is the range of the gluing homomorphism.

theorem exact_picardGluingHom_schemePullbackClassHom {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (a b : Spec (.of k) ⟶ X')
    (h : AlgebraicGeometry.IsGlueingTwoPoints f a b) :
    Function.Exact (picardGluingHom f a b h) (Stacks.Picard.schemePullbackClassHom f)

Stacks.GluePicard.picardGluingHom_eq_zero_of_ne_connectedComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/GlueingPicardExactness.lean, line 253. The attribute's comment: “the first map is zero if a and b are on different connected components of X'”.

The first map of the sequence of [Stacks, Tag 0C1M] is zero when the two glued points lie on different connected components of X'.

theorem picardGluingHom_eq_zero_of_ne_connectedComponents {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (a b : Spec (.of k) ⟶ X')
    (h : AlgebraicGeometry.IsGlueingTwoPoints f a b)
    (hab : ConnectedComponents.mk (a.base (IsLocalRing.closedPoint k)) ≠
      ConnectedComponents.mk (b.base (IsLocalRing.closedPoint k))) :
    picardGluingHom f a b h = 0

Stacks.GluePicard.picardGluingHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/GlueingPicardSequence.lean, line 343. The attribute's comment: “the gluing homomorphism”.

Stacks Project, Tag 0C1M. The gluing homomorphism k^* ⟶ Pic(X).

def picardGluingHom {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (a b : Spec (.of k) ⟶ X')
    (h : AlgebraicGeometry.IsGlueingTwoPoints f a b) :
    Additive kˣ →+ Stacks.Picard.ofScheme X

Stacks.GluePicard.injective_picardGluingHom_of_connectedComponents_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/GlueingPicardSequence.lean, line 559. The attribute's comment: “injectivity if X' is proper and the two points lie on the same connected component”.

Stacks Project, Tag 0C1M. The gluing homomorphism is injective when X' is proper and the two glued points lie on the same connected component of X': a scalar in its kernel is the ratio of the two values of a unit on X', and on a connected component of a proper scheme over an algebraically closed field the two values of any function agree.

theorem injective_picardGluingHom_of_connectedComponents_eq
    {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (a b : Spec (.of k) ⟶ X')
    (h : AlgebraicGeometry.IsGlueingTwoPoints f a b) [IsProper (X' ↘ Spec (.of k))]
    (hab : ConnectedComponents.mk (a.base (IsLocalRing.closedPoint k)) =
      ConnectedComponents.mk (b.base (IsLocalRing.closedPoint k))) :
    Function.Injective (picardGluingHom f a b h)

Tag 0C1N, a lemma

Tag 0C1N in the Stacks Project.

Stacks.SquishPicard.picardPullback_zero_and_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingPicard.lean, line 97. The attribute's comment: “the Picard pullback homomorphism”.

Pullback of Picard classes is a homomorphism of abelian groups.

theorem picardPullback_zero_and_add {X' X : Scheme.{u}} (f : X' ⟶ X) :
    Stacks.Picard.schemePullbackClassHom f 0 = 0 ∧
      ∀ x y : Stacks.Picard.ofScheme X,
        Stacks.Picard.schemePullbackClassHom f (x + y) =
          Stacks.Picard.schemePullbackClassHom f x +
            Stacks.Picard.schemePullbackClassHom f y

Stacks.SquishPicard.surjective_schemePullbackClassHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingPicard.lean, line 107. The attribute's comment: “surjectivity”.

Pullback along the squishing of a tangent vector is surjective on Picard groups.

theorem surjective_schemePullbackClassHom {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (θ : Spec (.of (DualNumber k)) ⟶ X')
    (h : AlgebraicGeometry.IsSquishingTangentVector f θ) :
    Function.Surjective (Stacks.Picard.schemePullbackClassHom f)

Stacks.SquishPicard.epsilonCoefficientAt_eq_zero_of_isProper_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingPicard.lean, line 240. The attribute's comment: “the lifting criterion for injectivity on a proper reduced scheme”.

The first map of the sequence of Stacks Tag 0C1N is injective when X' is proper and reduced, in the form that the connecting homomorphism consumes: the ε-coefficient along the squished tangent vector of every global section of 𝒪_{X'} vanishes.

The global functions of a scheme proper over k are integral over k, and those of a reduced scheme are a reduced ring, so the minimal polynomial over k of a global section is squarefree. Its image in k[ε] therefore cannot be a double root of a linear polynomial, which is what a nonzero ε-coefficient would make it.

theorem epsilonCoefficientAt_eq_zero_of_isProper_of_isReduced
    {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (θ : Spec (.of (DualNumber k)) ⟶ X')
    (h : AlgebraicGeometry.IsSquishingTangentVector f θ)
    [IsProper (X' ↘ Spec (.of k))] [IsReduced X'] (s : Γ(X', ⊤)) :
    AlgebraicGeometry.epsilonCoefficientAt θ ⊤ trivial s = 0

Stacks.SquishPicard.epsilonCoefficientAt_unit_eq_zero_of_isProper_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingPicard.lean, line 258. The attribute's comment: “the lifting criterion for injectivity on a proper reduced scheme”.

The criterion of Stacks.SquishPicard.epsilonCoefficientAt_eq_zero_of_isProper_of_isReduced for a global unit: the logarithmic ε-derivative of a unit on a proper reduced X' vanishes, so no nonzero scalar is hit by the units sequence and the first map of Tag 0C1N is injective.

theorem epsilonCoefficientAt_unit_eq_zero_of_isProper_of_isReduced
    {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (θ : Spec (.of (DualNumber k)) ⟶ X')
    (h : AlgebraicGeometry.IsSquishingTangentVector f θ)
    [IsProper (X' ↘ Spec (.of k))] [IsReduced X'] (s : Γ(X', ⊤)ˣ) :
    AlgebraicGeometry.epsilonCoefficientAt θ ⊤ trivial (s : Γ(X', ⊤)) = 0

Stacks.SquishSheafSequence.schemePullbackClassHom_eq_zero_iff_exists_picardTangentHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingPicardExactness.lean, line 222. The attribute's comment: “exactness”.

Exactness at Pic(X) of the sequence of [Stacks, Tag 0C1N]. For k algebraically closed and f : X' ⟶ X the squishing of the tangent vector θ of X', a Picard class of X pulls back to zero on X' exactly when it is the value of the tangent homomorphism Stacks.SquishSheafSequence.picardTangentHom at a scalar; that is, the kernel of Pic(X) ⟶ Pic(X') is the image of (k, +) ⟶ Pic(X).

theorem schemePullbackClassHom_eq_zero_iff_exists_picardTangentHom (f : X' ⟶ X)
    (θ : Spec (.of (DualNumber k)) ⟶ X')
    (h : AlgebraicGeometry.IsSquishingTangentVector f θ) (L : Stacks.Picard.ofScheme X) :
    Stacks.Picard.schemePullbackClassHom f L = 0 ↔
      ∃ a : k, picardTangentHom f θ h a = L

Stacks.SquishSheafSequence.exact_picardTangentHom_schemePullbackClassHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingPicardExactness.lean, line 246. The attribute's comment: “exactness”.

Exactness at Pic(X) of the sequence of [Stacks, Tag 0C1N], in the Function.Exact spelling: the kernel of pullback of Picard classes is the range of the tangent homomorphism.

theorem exact_picardTangentHom_schemePullbackClassHom (f : X' ⟶ X)
    (θ : Spec (.of (DualNumber k)) ⟶ X')
    (h : AlgebraicGeometry.IsSquishingTangentVector f θ) :
    Function.Exact (picardTangentHom f θ h) (Stacks.Picard.schemePullbackClassHom f)

Stacks.SquishSheafSequence.picardTangentHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingPicardSequence.lean, line 901. The attribute's comment: “the tangent homomorphism”.

The tangent homomorphism (k, +) ⟶ Pic(X) of [Stacks, Tag 0C1N]. It is the connecting homomorphism of the short exact sequence of sheaves of units of a squishing, read through the five-term low-degree cohomology sequence over the whole space and through the identification of H¹(X, 𝒪_X^*) with the Picard group of [Stacks, Tag 09NU].

def picardTangentHom {k : Type u} [Field k] [IsAlgClosed k] {X' X : Scheme.{u}}
    [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))] (f : X' ⟶ X)
    (θ : Spec (.of (DualNumber k)) ⟶ X')
    (h : AlgebraicGeometry.IsSquishingTangentVector f θ) : k →+ Stacks.Picard.ofScheme X

Stacks.SquishSheafSequence.injective_picardTangentHom_of_isProper_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingPicardSequence.lean, line 975. The attribute's comment: “injectivity on a proper reduced scheme”.

The tangent homomorphism is injective when X' is proper and reduced. A scalar in its kernel is the logarithmic ε-derivative of a unit on X', and on a proper reduced X' the logarithmic ε-derivative of a global unit vanishes by Stacks.SquishSheafSequence.epsilonLogDeriv_eq_zero_of_isProper_of_isReduced.

theorem injective_picardTangentHom_of_isProper_of_isReduced {k : Type u} [Field k]
    [IsAlgClosed k] {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (θ : Spec (.of (DualNumber k)) ⟶ X')
    (h : AlgebraicGeometry.IsSquishingTangentVector f θ)
    [IsProper (X' ↘ Spec (.of k))] [IsReduced X'] :
    Function.Injective (picardTangentHom f θ h)

Stacks.SquishSheafSequence.epsilonLogDerivSheafHom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingUnitsSequence.lean, line 435. The attribute's comment: “the quotient map of the sequence of sheaves of units”.

The quotient map of the units sequence is the logarithmic ε-derivative on the units of the sections over every neighbourhood of the contracted point.

theorem epsilonLogDerivSheafHom_app {k : Type u} [Field k] {X' X : Scheme.{u}} (f : X' ⟶ X)
    (θ : Spec (.of (DualNumber k)) ⟶ X') (U : X.Opens)
    (hx : (θ ≫ f).base (IsLocalRing.closedPoint (DualNumber k)) ∈ U)
    (s : Γ(X', f ⁻¹ᵁ U)ˣ) :
    (epsilonLogDerivSheafHom f θ).hom.app (op U) (Additive.ofMul s) =
      skyscraperAddSheafMk X ((θ ≫ f).base (IsLocalRing.closedPoint (DualNumber k))) hx
        (epsilonLogDeriv θ (f ⁻¹ᵁ U) hx s)

Stacks.SquishSheafSequence.epsilonLogDeriv_eq_zero_of_isProper_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GlueingSquishing/SquishingUnitsSequence.lean, line 451. The attribute's comment: “vanishing of the logarithmic derivative on a proper reduced scheme”.

On a proper reduced X' the logarithmic ε-derivative of a global unit vanishes, so the arrow to (k, +) of the units sequence of [Stacks, Tag 0C1N] kills the global units and the connecting homomorphism (k, +) → Pic(X) is injective. The ε-coefficient of every global section already vanishes, by Stacks.SquishPicard.epsilonCoefficientAt_eq_zero_of_isProper_of_isReduced.

theorem epsilonLogDeriv_eq_zero_of_isProper_of_isReduced
    {k : Type u} [Field k] [IsAlgClosed k]
    {X' X : Scheme.{u}} [X'.Over (Spec (.of k))] [X.Over (Spec (.of k))]
    (f : X' ⟶ X) (θ : Spec (.of (DualNumber k)) ⟶ X')
    (h : AlgebraicGeometry.IsSquishingTangentVector f θ)
    [IsProper (X' ↘ Spec (.of k))] [IsReduced X'] (u : Γ(X', ⊤)ˣ) :
    epsilonLogDeriv θ ⊤ (Opens.mem_top _) u = 0

Sources

LeanAlgebra.algEquiv_prod_or_dualNumber_of_natCard_subalgebra_eq_two · Algebra.algEquiv_prod_or_dualNumber_of_no_intermediateSubalgebra · AlgebraicGeometry.IsGlueingTwoPoints · Stacks.GlueSquishUnits.isShortExact_units_of_isGlueingTwoPoints · Stacks.SquishSheafSequence.shortExact_units_of_isSquishingTangentVector · AlgebraicGeometry.IsSquishingTangentVector · Stacks.SquishSheafSequence.shortExact_of_isSquishingTangentVector · Stacks.GlueSquishFactor.algEquiv_prod_or_dualNumber_of_minimal

Section53.16 Multicross and nodal singularities #

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

Tag 0C1U, an equation

Tag 0C1U in the Stacks Project.

Stacks.Curves.multicross, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Node/Multicross.lean, line 56.

The ring of n-tuples of formal power series having the same constant coefficient.

def multicross (k : Type*) [CommRing k] (n : ℕ) : Subring (Fin n → PowerSeries k)

Tag 0C1V, a lemma

Tag 0C1V in the Stacks Project.

Ring.deltaInvariant_ge_numberOfBranches_sub_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/MulticrossBranches/BranchBound.lean, line 77. The attribute's comment: “delta invariant bound”.

The delta invariant of a reduced one-dimensional Nagata local algebra over a separably closed field is at least the number of branches minus one.

theorem deltaInvariant_ge_numberOfBranches_sub_one
    (k : Type u) (A : Type v) [Field k] [IsSepClosed k] [CommRing A] [Algebra k A]
    [IsLocalRing A] [IsReduced A] (hNagata : IsNagataRing A)
    (hdim : ringKrullDim A = 1) (_hres : Nonempty (ResidueField A ≃ₐ[k] k)) :
    numberOfBranchesOfLocalRing A - 1 ≤ Ring.deltaInvariant A

Ring.adicCompletion_algEquiv_multicross_of_deltaInvariant_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/MulticrossBranches/Completion.lean, line 49. The attribute's comment: “equality case”.

If equality holds in the branch bound, the completed local algebra is the multicross algebra with one power-series factor for each branch.

theorem adicCompletion_algEquiv_multicross_of_deltaInvariant_eq
    (k : Type u) (A : Type v) [Field k] [IsSepClosed k] [CommRing A] [Algebra k A]
    [IsLocalRing A] [IsReduced A] (hNagata : IsNagataRing A)
    (hdim : ringKrullDim A = 1) (_hres : Nonempty (ResidueField A ≃ₐ[k] k))
    (heq : Ring.deltaInvariant A = numberOfBranchesOfLocalRing A - 1) :
    ∃ n : ℕ, numberOfBranchesOfLocalRing A = n ∧
      ∃ e : AdicCompletion (maximalIdeal A) A ≃+* multicross k n,
        e.toRingHom.comp (algebraMap k (AdicCompletion (maximalIdeal A) A)) =
          (RingHom.pi fun _ : Fin n ↦ PowerSeries.C).codRestrict
            (multicross k n) (by
              intro a
              rw [mem_multicross]
              simp)

Ring.deltaInvariant_eq_numberOfBranches_sub_one_of_adicCompletion_algEquiv_multicross, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/MulticrossBranches/Completion.lean, line 333. The attribute's comment: “converse equality case”.

A coefficient-compatible multicross description of the completion, with one factor for each branch, forces equality in the delta-invariant bound.

theorem deltaInvariant_eq_numberOfBranches_sub_one_of_adicCompletion_algEquiv_multicross
    (k : Type u) (A : Type v) [Field k] [IsSepClosed k] [CommRing A] [Algebra k A]
    [IsLocalRing A] [IsReduced A] (hNagata : IsNagataRing A)
    (hdim : ringKrullDim A = 1) (_hres : Nonempty (ResidueField A ≃ₐ[k] k))
    (n : ℕ) (hn : numberOfBranchesOfLocalRing A = n)
    (e : AdicCompletion (maximalIdeal A) A ≃+* multicross k n)
    (_he : e.toRingHom.comp (algebraMap k (AdicCompletion (maximalIdeal A) A)) =
      (RingHom.pi fun _ : Fin n ↦ PowerSeries.C).codRestrict
        (multicross k n) (by
          intro a
          rw [mem_multicross]
          simp)) :
    Ring.deltaInvariant A = numberOfBranchesOfLocalRing A - 1

Tag 0C1W, a definition

Tag 0C1W in the Stacks Project.

Stacks.Curves.IsMulticrossSingularity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/IsNode.lean, line 111. The attribute's comment: “multicross singularity”.

Stacks 0C1W. A point is a multicross singularity if it is closed and its completed local ring is a multicross ring with at least two branches.

def IsMulticrossSingularity (k : Type u) [Field k] [IsAlgClosed k] (X : Scheme.{u})
    [X.Over (Spec (.of k))] (x : X) : Prop

Stacks.Curves.IsOrdinaryDoublePoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/IsNode.lean, line 123. The attribute's comment: “node (ordinary double point)”. References: SGA 7 VI (6.6), “dim 1, k alg. closed”; SGA 7 XV (1.2.1), “dim 1, alg. closed k”; SGA 7 XVII (1.1), “n=2, k alg. closed”; SGA 7 IX (10.5.4); SGA 7 IX (12.1.11).

Stacks 0C1W. A point is an ordinary double point — a node, or a nodal singularity — if it is closed and its completed local ring is the two-branch multicross ring.

def IsOrdinaryDoublePoint (k : Type u) [Field k] [IsAlgClosed k] (X : Scheme.{u})
    [X.Over (Spec (.of k))] (x : X) : Prop

Tag 0C1X, a lemma

Tag 0C1X in the Stacks Project.

Stacks.Curves.isMulticrossSingularity_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/MulticrossGlueingResolution.lean, line 3082. The attribute's comment: “all three clauses. The hypothesis that the local ring at x is not regular is an erratum repair, not a weakening: the source's displayed equivalence is false at a nonsingular closed point, where the delta invariant is 0 and the number of branches is 1, so clauses (2) and (3) hold while (1) fails because Definition 0C1W requires n ≥ 2 -- Lemma 0C1V, which the source cites for the equivalence of (1) and (2), puts no lower bound on n. That counterexample is proved, not asserted, in Stacks.Curves.exists_counterexample_to_displayed_statement_of_tag_0C1X_at_nonsingular_point, and at a concrete scheme -- the origin of the affine line -- in Stacks.Curves.exists_counterexample_to_displayed_statement_of_tag_0C1X_specPolynomial. The hypothesis excludes exactly the regular configurations, where the equivalence fails, and nothing else”.

Stacks 0C1X. Let k be an algebraically closed field, X a reduced algebraic one-dimensional k-scheme and x ∈ X a closed point whose local ring is not regular. The following are equivalent:

x defines a multicross singularity;

the delta invariant of X at x is the number of branches of X at x minus one;

there is a sequence of morphisms U_n ⟶ U_{n-1} ⟶ … ⟶ U_0 = U ⊆ X with U an open neighbourhood of x, with U_n nonsingular, and with every step a glueing of two points as in Example 0C1J.

The equivalence of (1) and (2) is Stacks.Curves.isMulticrossSingularity_iff_deltaInvariant_eq_of_not_isRegularLocalRing, which is Tag 0C1V read at a point of a scheme. For (3) implies (1) the completion at the point glued in each step is the pair pullback of the two completions above it, hence a multicross ring or a field, and over every other point the step is an isomorphism on stalks. For (1) implies (3) an open neighbourhood on which x is the only singular point is chosen, Tag 0C1L factors its normalization morphism into glueings of two points and squishings of tangent vectors, and no step is a squishing because a multicross completion is seminormal while a squishing produces a non-seminormal completion.

theorem isMulticrossSingularity_tfae
    (k : Type u) [Field k] [IsAlgClosed k] (X : Scheme.{u})
    [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    [QuasiCompact (X ↘ AlgebraicGeometry.Spec (.of k))] [IsReduced X]
    (hX : topologicalKrullDim X = 1) (x : X) (hx : IsClosed ({x} : Set X))
    (hsing : ¬ IsRegularLocalRing (X.presheaf.stalk x)) :
    List.TFAE
      [Stacks.Curves.IsMulticrossSingularity k X x,
        Ring.deltaInvariant (X.presheaf.stalk x) = numberOfBranches X x - 1,
        HasNonsingularGlueingResolution k X x]

Tag 0CDZ, a lemma

Tag 0CDZ in the Stacks Project.

Stacks.Curves.isOrdinaryDoublePoint_of_isGorenstein, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/MulticrossGorenstein.lean, line 550.

Stacks 0CDZ. A multicross singularity of a Gorenstein scheme over an algebraically closed field is a node.

theorem isOrdinaryDoublePoint_of_isGorenstein (k : Type u) [Field k] [IsAlgClosed k]
    (X : Scheme.{u}) [X.Over (Spec (.of k))] [IsGorenstein X] (x : X)
    (hx : IsMulticrossSingularity k X x) :
    IsOrdinaryDoublePoint k X x

Sources

LeanStacks.Curves.multicross · Ring.deltaInvariant_ge_numberOfBranches_sub_one · Ring.adicCompletion_algEquiv_multicross_of_deltaInvariant_eq · Ring.deltaInvariant_eq_numberOfBranches_sub_one_of_adicCompletion_algEquiv_multicross · Stacks.Curves.IsMulticrossSingularity · Stacks.Curves.IsOrdinaryDoublePoint · Stacks.Curves.isMulticrossSingularity_tfae · Stacks.Curves.isOrdinaryDoublePoint_of_isGorenstein

Section53.17 Torsion in the Picard group #

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

Tag 0C1Z, a lemma

Tag 0C1Z in the Stacks Project.

Stacks.Picard.nonempty_torsionBy_addEquiv_pi_zmod_of_smoothProjectiveCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/TorsionSmoothProjectiveCurve/Unconditional.lean, line 121. The attribute's comment: “clause (1)”.

Stacks Project, Tag 0C1Z (1). Let k be an algebraically closed field and X a smooth projective curve of genus g over k. If n ≥ 1 is invertible in k, then Pic(X)[n] ≅ (ℤ/nℤ)^{⊕2g}.

theorem nonempty_torsionBy_addEquiv_pi_zmod_of_smoothProjectiveCurve (k : Type u) [Field k]
    [IsAlgClosed k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsCurve k f]
    [IsProjectiveVariety k f] [Smooth f] (n : ℕ) (hn : 1 ≤ n) (hnk : IsUnit (n : k)) :
    Nonempty (Submodule.torsionBy ℤ (ofScheme X) (n : ℤ) ≃+ (Fin (2 * genus f) → ZMod n))

Stacks.Picard.exists_rank_torsionBy_prime_pow_addEquiv_pi_zmod_of_smoothProjectiveCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/TorsionSmoothProjectiveCurve/Unconditional.lean, line 134. The attribute's comment: “clause (2)”.

Stacks Project, Tag 0C1Z (2). Let k be an algebraically closed field of characteristic p > 0 and X a smooth projective curve of genus g over k. Then there is an integer 0 ≤ r ≤ g with Pic(X)[p^m] ≅ (ℤ/p^mℤ)^{⊕r} for all m ≥ 1 (the source's f).

theorem exists_rank_torsionBy_prime_pow_addEquiv_pi_zmod_of_smoothProjectiveCurve (k : Type u)
    [Field k] [IsAlgClosed k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsCurve k f]
    [IsProjectiveVariety k f] [Smooth f] (p : ℕ) [CharP k p] (hp : 0 < p) :
    ∃ r : ℕ, r ≤ genus f ∧ ∀ m : ℕ, 1 ≤ m →
      Nonempty (Submodule.torsionBy ℤ (ofScheme X) ((p : ℤ) ^ m) ≃+ (Fin r → ZMod (p ^ m)))

Tag 0CDU, a lemma

Tag 0CDU in the Stacks Project.

Stacks.Picard.exists_finite_separable_torsionBy_of_genus_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PicardTorsionVisible.lean, line 112. The attribute's comment: “(1)”.

Stacks Project, Tag 0CDU (1). Let k be a field, let n be prime to the characteristic of k, and let X be a smooth proper curve over k with H⁰(X, 𝒪_X) = k and of genus 1. Then there is a finite separable extension k'/k such that X_{k'} has a k'-rational point and Pic(X_{k'})[n] ≅ (ℤ/nℤ)^{⊕2}.

The point is a closed point with finite separable residue field, which exists by Tag 056U.

theorem exists_finite_separable_torsionBy_of_genus_eq_one [IsCurve k f] [Smooth f] [IsProper f]
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop)] (hg : genus f = 1) {n : ℕ}
    (hn : (n : k) ≠ 0) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k'), FiniteDimensional k k' ∧
      Algebra.IsSeparable k k' ∧
      (∃ t : Spec (.of k') ⟶ pullback f (Spec.map (CommRingCat.ofHom (algebraMap k k'))),
        t ≫ pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k k'))) = 𝟙 _) ∧
      Nonempty (Submodule.torsionBy ℤ
        (ofScheme (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k k'))))) (n : ℤ) ≃+
        (Fin 2 → ZMod n))

Stacks.Picard.exists_finite_separable_torsionBy_of_two_le_genus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PicardTorsionVisible.lean, line 137. The attribute's comment: “(2)”.

Stacks Project, Tag 0CDU (2). Let k be a field, let n be prime to the characteristic of k, and let X be a smooth proper curve over k with H⁰(X, 𝒪_X) = k and of genus g ≥ 2. Then there is a finite separable extension k'/k with [k' : k] ≤ (2g - 2)(n^{2g})! such that X_{k'} has a k'-rational point and Pic(X_{k'})[n] ≅ (ℤ/nℤ)^{⊕2g}.

The closed point of degree at most 2g - 2 with separable residue field is Tag 0CD4.

theorem exists_finite_separable_torsionBy_of_two_le_genus [IsCurve k f] [Smooth f] [IsProper f]
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop)] (hg : 2 ≤ genus f) {n : ℕ}
    (hn : (n : k) ≠ 0) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k'), FiniteDimensional k k' ∧
      Algebra.IsSeparable k k' ∧
      Module.finrank k k' ≤ (2 * genus f - 2) * (n ^ (2 * genus f)).factorial ∧
      (∃ t : Spec (.of k') ⟶ pullback f (Spec.map (CommRingCat.ofHom (algebraMap k k'))),
        t ≫ pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k k'))) = 𝟙 _) ∧
      Nonempty (Submodule.torsionBy ℤ
        (ofScheme (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k k'))))) (n : ℤ) ≃+
        (Fin (2 * genus f) → ZMod n))

Tag 0C20, a proposition

Tag 0C20 in the Stacks Project.

AlgebraicGeometry.finrank_picardTorsion_le_genus_add_geometricGenus_of_isReduced_dim_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/TorsionReducedProperCurve.lean, line 768. The attribute's comment: “the bound dim Pic(X)[l] ≤ g + g_geom (connectedness not needed)”.

Stacks Project, Tag 0C20, the bound.

Let k be an algebraically closed field, let X be a proper scheme over k which is reduced and of dimension one, let g = h¹(X, 𝒪_X) be its genus and let g_geom be the sum of the geometric genera of its irreducible components, and let ℓ be a prime different from the characteristic of k. Then the ℓ-torsion of Pic(X) is finite-dimensional over F_ℓ and

dim_{F_ℓ} Pic(X)[ℓ] ≤ g + g_geom.

Connectedness, which the source assumes, is not needed; the source's statement is the special case [ConnectedSpace X].

The proof is the source's: the normalization is factored by [Stacks, Tag 0C1L], the two invariants are compared along the factorization by the three lines of the source's table, and at the far end h¹(X^ν) = g_geom (AlgebraicGeometry.genus_normalizationOverField_eq_geometricGenus) and dim_{F_ℓ} Pic(X^ν)[ℓ] = 2 g_geom, the latter from clause (1) of [Stacks, Tag 0C1Z] (Stacks.Picard.nonempty_torsionBy_addEquiv_pi_zmod_of_smoothProjectiveCurve) by AlgebraicGeometry.rank_picardTorsion_normalizationSchemeOverField_eq_two_mul_geometricGenus.

theorem finrank_picardTorsion_le_genus_add_geometricGenus_of_isReduced_dim_one (k : Type u)
    [Field k] [IsAlgClosed k]
    (X : Scheme.{u}) [X.Over (Spec (.of k))] [IsProper (X ↘ Spec (.of k))] [IsReduced X]
    (hdim : topologicalKrullDim (X : Type u) = 1) (ℓ : ℕ) [Fact ℓ.Prime] (hℓ : (ℓ : k) ≠ 0) :
    FiniteDimensional (ZMod ℓ) (AddSubgroup.torsionBy (ofScheme X) (ℓ : ℤ)) ∧
      Module.finrank (ZMod ℓ) (AddSubgroup.torsionBy (ofScheme X) (ℓ : ℤ)) ≤
        genus (X ↘ Spec (.of k)) + geometricGenus k (X ↘ Spec (.of k))

AlgebraicGeometry.finrank_picardTorsion_eq_iff_forall_isMulticrossSingularity_of_isReduced_dim_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/TorsionReducedProperCurve.lean, line 802. The attribute's comment: “the equality criterion: equality iff all singularities are multicross”.

Stacks Project, Tag 0C20, the equality criterion.

In the situation of the bound AlgebraicGeometry.finrank_picardTorsion_le_genus_add_geometricGenus_of_isReduced_dim_one, the ℓ-torsion of Pic(X) is finite-dimensional over F_ℓ, and equality dim_{F_ℓ} Pic(X)[ℓ] = g + g_geom holds if and only if every singularity of X is multicross.

Equality holds exactly when the factorization of the normalization contains no squishing, in both directions — the forward direction from the strict drop a squishing causes, the backward direction from the equality case of the arithmetic along a glueing chain — and the factorization contains no squishing exactly when every singularity of X is multicross (Stacks.Curves.isGlueingChain_normalizationOver_iff_forall_isMulticrossSingularity, the step the source leaves out: "just glue the local sequences for each point to find one that works for all singular points").

theorem finrank_picardTorsion_eq_iff_forall_isMulticrossSingularity_of_isReduced_dim_one
    (k : Type u) [Field k]
    [IsAlgClosed k] (X : Scheme.{u}) [X.Over (Spec (.of k))] [IsProper (X ↘ Spec (.of k))]
    [IsReduced X] (hdim : topologicalKrullDim (X : Type u) = 1) (ℓ : ℕ) [Fact ℓ.Prime]
    (hℓ : (ℓ : k) ≠ 0) :
    FiniteDimensional (ZMod ℓ) (AddSubgroup.torsionBy (ofScheme X) (ℓ : ℤ)) ∧
      (Module.finrank (ZMod ℓ) (AddSubgroup.torsionBy (ofScheme X) (ℓ : ℤ)) =
        genus (X ↘ Spec (.of k)) + geometricGenus k (X ↘ Spec (.of k)) ↔
      ∀ x : X, ¬ IsRegularLocalRing (X.presheaf.stalk x) →
        Stacks.Curves.IsMulticrossSingularity k X x)

Sources

LeanStacks.Picard.nonempty_torsionBy_addEquiv_pi_zmod_of_smoothProjectiveCurve · Stacks.Picard.exists_rank_torsionBy_prime_pow_addEquiv_pi_zmod_of_smoothProjectiveCurve · Stacks.Picard.exists_finite_separable_torsionBy_of_genus_eq_one · Stacks.Picard.exists_finite_separable_torsionBy_of_two_le_genus · AlgebraicGeometry.finrank_picardTorsion_le_genus_add_geometricGenus_of_isReduced_dim_one · AlgebraicGeometry.finrank_picardTorsion_eq_iff_forall_isMulticrossSingularity_of_isReduced_dim_one

Section53.18 Genus versus geometric genus #

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

Tag 0CE0, the section

Tag 0CE0 in the Stacks Project.

AlgebraicGeometry.geometricGenus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusCurve/Geometric.lean, line 83. The attribute's comment: “definition of the geometric genus g_geom(X/k)”.

The geometric genus g_geom(X/k) of a proper scheme X over a field k: the sum, over the irreducible components of dimension one of the base change of X to an algebraic closure of k, of the genus of the normalization of that component with its reduced structure.

This is the invariant introduced in the preamble of the source's section on genus versus geometric genus.

public def geometricGenus (k : Type u) [Field k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k))
    [IsProper g] : ℕ

Tag 0CE1, a lemma

Tag 0CE1 in the Stacks Project.

AlgebraicGeometry.geometricGenus_eq_sum_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusCurve/GeometricComponents.lean, line 348.

Let k be a field and let X be a proper scheme of dimension at most one over k. The geometric genus of X over k is the sum of the geometric genera of the irreducible components of X of dimension one, each taken with its reduced closed subscheme structure; components of dimension zero contribute nothing.

public theorem geometricGenus_eq_sum_components {k : Type u} [Field k]
    {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsProper g]
    (hX : topologicalKrullDim X ≤ 1) :
    letI : IsNoetherian X :=
      { toIsLocallyNoetherian := LocallyOfFiniteType.isLocallyNoetherian g
        toCompactSpace := QuasiCompact.compactSpace_of_compactSpace g }
    letI : Finite (irreducibleComponents X) :=
      (finite_irreducibleComponents_of_isNoetherian (X := X)).to_subtype
    letI : Fintype (irreducibleComponents X) := Fintype.ofFinite _
    geometricGenus k g =
      ∑ C : irreducibleComponents X,
        if topologicalKrullDim (irreducibleComponentIdeal C).subscheme = 1 then
          geometricGenus k ((irreducibleComponentIdeal C).subschemeι ≫ g)
        else 0

Tag 0CE2, a lemma

Tag 0CE2 in the Stacks Project.

AlgebraicGeometry.geometricGenus_reduction_birational_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusCurve/GeometricGenusBirational.lean, line 215.

Let k be a field and let X be a proper scheme of dimension at most one over k. Then

the reduction X_red has the same geometric genus as X;

the source of a birational proper morphism X' ⟶ X has the same geometric genus as X; and

the normalization X^ν has the same geometric genus as X.

public theorem geometricGenus_reduction_birational_normalization {k : Type u} [Field k]
    {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsProper g]
    (hX : topologicalKrullDim (X : Type u) ≤ 1) :
    letI : IsProper (normalizationOverField k g ≫ g) :=
      isProper_normalizationOverField_comp k g
    geometricGenus k (X.reductionι ≫ g) = geometricGenus k g ∧
      (∀ (X' : Scheme.{u}) (f : X' ⟶ X) [IsProper f], IsBirational f →
        geometricGenus k (f ≫ g) = geometricGenus k g) ∧
      geometricGenus k (normalizationOverField k g ≫ g) = geometricGenus k g

Tag 0CE3, a lemma

Tag 0CE3 in the Stacks Project.

AlgebraicGeometry.genus_le_of_isAffineHom_of_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusCurve/GenusGoesDown.lean, line 282. The attribute's comment: “with the two cohomology vanishings and the finiteness of H¹(X,𝒪_X) as hypotheses”.

[Stacks, Tag 0CE3] with its three cohomological inputs as hypotheses. Let f : Y ⟶ X be an affine morphism of schemes over a field k, and let φ : 𝒪_X ⟶ f_*𝒪_Y be the canonical comparison map. If H¹(X, coker φ) = 0, if H²(X, ker φ) = 0 and if H¹(X, 𝒪_X) is finite dimensional over k, then the genus of Y is at most the genus of X, that is dim_k H¹(Y, 𝒪_Y) ≤ dim_k H¹(X, 𝒪_X).

The three hypotheses replace the properness of X over k, the bound on its dimension and the hypothesis that f is a closed immersion over a dense open, which the source uses only to produce them; see the implementation notes of this file.

theorem genus_le_of_isAffineHom_of_isZero (f : Y ⟶ X) [IsAffineHom f]
    (hcoker : IsZero (cohomologyOverField k g (cokernel (structureSheafToPushforward f)) 1))
    (hker : IsZero (cohomologyOverField k g (kernel (structureSheafToPushforward f)) 2))
    (hfin : FiniteDimensional k (cohomologyOverField k g (structureSheafModule X) 1)) :
    genus (f ≫ g) ≤ genus g

AlgebraicGeometry.genus_le_of_isFinite_of_isClosedImmersion_over_dense_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusCurve/GenusGoesDownUnconditional.lean, line 222.

[Stacks, Tag 0CE3]. Let k be a field, let g : X ⟶ Spec k be proper with dim X ≤ 1, and let f : Y ⟶ X be finite and a closed immersion over a dense open U ⊆ X. Then the genus of Y is at most the genus of X, that is dim_k H¹(Y, 𝒪_Y) ≤ dim_k H¹(X, 𝒪_X).

This is AlgebraicGeometry.genus_le_of_isAffineHom_of_isZero with its three cohomological hypotheses discharged; see the module docstring.

theorem genus_le_of_isFinite_of_isClosedImmersion_over_dense_open
    (k : Type u) [Field k] {X Y : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsProper g]
    (f : Y ⟶ X) [IsFinite f] (hdim : topologicalKrullDim (X : Type u) ≤ 1)
    (U : X.Opens) (hdense : Dense (U : Set X))
    (hclosed : IsClosedImmersion (pullback.snd f U.ι)) :
    genus (f ≫ g) ≤ genus g

Tag 0CE4, a lemma

Tag 0CE4 in the Stacks Project.

AlgebraicGeometry.genus_le_and_isIso_of_isProper_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusCurve/BirationalGenus.lean, line 239.

Let k be a field and let X be a proper scheme of dimension at most one over k. If f : X' ⟶ X is a birational proper morphism, then

dim_k H¹(X, 𝒪_X) ≥ dim_k H¹(X', 𝒪_{X'}),

and if moreover X is reduced, H⁰(X, 𝒪_X) ⟶ H⁰(X', 𝒪_{X'}) is surjective and equality holds, then X' = X.

Here dim_k H¹ is AlgebraicGeometry.genus of the structure morphism, and X' = X means that f is an isomorphism of schemes.

theorem genus_le_and_isIso_of_isProper_of_isBirational [IsProper g] (f : X' ⟶ X) [IsProper f]
    (hf : IsBirational f) (hX : topologicalKrullDim (X : Type u) ≤ 1) :
    genus (f ≫ g) ≤ genus g ∧
      (IsReduced X → Function.Surjective f.appTop → genus (f ≫ g) = genus g → IsIso f)

Tag 0CE5, a lemma

Tag 0CE5 in the Stacks Project.

AlgebraicGeometry.geometricGenus_le_finSepDegree_mul_genus_toSpecΓ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusCurve/GeometricGenusIrreducible.lean, line 233. The attribute's comment: “κ = k, geometrically integral of dim 1, 0CE3's vanishings and H¹ finite”.

Let k be a field and let X be a proper integral scheme over k whose global regular functions are exactly k and whose base change to an algebraic closure of k is irreducible, reduced and of dimension one. Writing κ = Γ(X, ⊤), the geometric genus of X over k is at most [κ : k]_s · dim_κ H¹(X, 𝒪_X).

public theorem geometricGenus_le_finSepDegree_mul_genus_toSpecΓ
    (k : Type u) [Field k] {X : Scheme.{u}} [IsIntegral X] (g : X ⟶ Spec (.of k)) [IsProper g]
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ g.appTop)]
    (hirr : IrreducibleSpace (pullback (C := Scheme.{u}) g
      (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k))))))
    (hred : IsReduced (pullback (C := Scheme.{u}) g
      (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k))))))
    (hdim : topologicalKrullDim (pullback (C := Scheme.{u}) g
      (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k))))) = 1)
    (hcoker : IsZero (cohomologyOverField (AlgebraicClosure k)
      (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k)))))
      (cokernel (structureSheafToPushforward (normalizationOverField (AlgebraicClosure k)
        (pullback.snd g
          (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k)))))))) 1))
    (hker : IsZero (cohomologyOverField (AlgebraicClosure k)
      (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k)))))
      (kernel (structureSheafToPushforward (normalizationOverField (AlgebraicClosure k)
        (pullback.snd g
          (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k)))))))) 2))
    (hfin : FiniteDimensional (AlgebraicClosure k) (cohomologyOverField (AlgebraicClosure k)
      (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k)))))
      (structureSheafModule (pullback (C := Scheme.{u}) g
        (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k)))))) 1)) :
    letI : Field Γ(X, ⊤) := (isField_of_universallyClosed k g).toField
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ g.appTop).hom.toAlgebra
    geometricGenus k g ≤ Field.finSepDegree k Γ(X, ⊤) * genus X.toSpecΓ

AlgebraicGeometry.geometricGenus_le_genus_of_irreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusCurve/GeometricGenusIrreducibleUnconditional.lean, line 73. The attribute's comment: “κ = k, geometrically irreducible of dimension one”.

Let k be a field and g : X ⟶ Spec k proper. If the base change X_{k̄} of X to an algebraic closure k̄ of k is irreducible, reduced and of dimension one, then g_geom(X/k) ≤ g(X).

theorem geometricGenus_le_genus_of_irreducible
    (k : Type u) [Field k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsProper g]
    (hirr : IrreducibleSpace (pullback (C := Scheme.{u}) g
      (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k))))))
    (hred : IsReduced (pullback (C := Scheme.{u}) g
      (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k))))))
    (hdim : topologicalKrullDim (pullback (C := Scheme.{u}) g
      (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k))))) = 1) :
    geometricGenus k g ≤ genus g

AlgebraicGeometry.geometricGenus_le_genus_of_dim_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusCurve/GeometricGenusLeGenusUnconditional.lean, line 139. The attribute's comment: “the per-fibre bound, over an algebraically closed field”.

The per-fibre bound of [Stacks, Tag 0CE5]. Over an algebraically closed field K, the geometric genus of a proper scheme of dimension at most one is at most its genus. No hypothesis is made on the irreducible components: the scheme may be reducible and non-reduced.

public theorem geometricGenus_le_genus_of_dim_le_one (K : Type u) [Field K] [IsAlgClosed K]
    {Z : Scheme.{u}} (q : Z ⟶ Spec (.of K)) [IsProper q]
    (hdim : topologicalKrullDim (Z : Type u) ≤ 1) :
    geometricGenus K q ≤ genus q

AlgebraicGeometry.geometricGenus_le_finSepDegree_mul_genus_toSpecΓ_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusCurve/SeparableDegreeFibreSum.lean, line 132.

Stacks Project, Tag 0CE5. Let C be a proper curve over a field k and let κ = Γ(C, ⊤) be its field of global regular functions. Then the geometric genus of C over k is at most [κ : k]_s · dim_κ H¹(C, 𝒪_C).

The sum over the k-embeddings κ → k̄ is AlgebraicGeometry.geometricGenus_eq_finsum_geometricGenus_pullback_snd_toSpecΓ, and each of its terms is bounded by the genus of the corresponding fibre by AlgebraicGeometry.geometricGenus_le_genus_of_dim_le_one, the fibre being a proper scheme of dimension one over the algebraically closed field k̄.

public theorem geometricGenus_le_finSepDegree_mul_genus_toSpecΓ_of_isCurve
    (k : Type u) [Field k] {C : Scheme.{u}} (f : C ⟶ Spec (.of k)) [IsCurve k f] [IsProper f] :
    letI : Field Γ(C, ⊤) := (isField_of_universallyClosed k f).toField
    letI : Algebra k Γ(C, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    letI : IsProper C.toSpecΓ := isProper_toSpecΓ f
    geometricGenus k f ≤ Field.finSepDegree k Γ(C, ⊤) * genus C.toSpecΓ

Tag 0CE6, a lemma

Tag 0CE6 in the Stacks Project.

AlgebraicGeometry.finrank_picardTorsion_le_genus_add_geometricGenus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/TorsionRankConnectedComponents.lean, line 203.

Stacks Project, Tag 0CE6. Let k be a field, let X be a proper scheme of dimension at most one over k and let ℓ be a prime invertible in k. Then the ℓ-torsion of Pic(X) is finite-dimensional over F_ℓ and

dim_{F_ℓ} Pic(X)[ℓ] ≤ dim_k H¹(X, 𝒪_X) + g_geom(X/k).

The proof is the source's: extend the ground field to an algebraic closure and pass to the reduction (AlgebraicGeometry.picardTorsion_bound_of_reducedBaseChange, which is Tag 0CC5, Tag 02KH, Tag 0CE2 (1) and Tag 0CE3), then decompose into connected components (AlgebraicGeometry.picardTorsion_bound_of_connectedComponents) and apply Tag 0C20 to the one-dimensional ones, the zero-dimensional ones having trivial Picard group.

theorem finrank_picardTorsion_le_genus_add_geometricGenus (k : Type u) [Field k]
    {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsProper g]
    (hdim : topologicalKrullDim (X : Type u) ≤ 1) (ℓ : ℕ) [Fact ℓ.Prime] (hℓ : IsUnit (ℓ : k)) :
    FiniteDimensional (ZMod ℓ) (AddSubgroup.torsionBy (ofScheme X) (ℓ : ℤ)) ∧
      Module.finrank (ZMod ℓ) (AddSubgroup.torsionBy (ofScheme X) (ℓ : ℤ)) ≤
        genus g + geometricGenus k g

Sources

Section53.19 Nodal curves #

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

Tag 0C47, a definition

Tag 0C47 in the Stacks Project.

Stacks.Curves.IsNode, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/IsNode.lean, line 194. The attribute's comment: “part (1)”.

Stacks 0C47. A point of a scheme over k is a node if it is closed and an ordinary double point lies above it after base change to an algebraic closure of k.

def IsNode (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))] (x : X) : Prop

Stacks.Curves.HasAtWorstNodalSingularities, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/IsNode.lean, line 206. The attribute's comment: “part (2)”.

Stacks 0C47. A scheme over k has at-worst-nodal singularities if each of its closed points is smooth over k or is a node.

def HasAtWorstNodalSingularities (k : Type u) [Field k] (X : Scheme.{u})
    [X.Over (Spec (.of k))] : Prop

Tag 0C48, a lemma

Tag 0C48 in the Stacks Project.

IsRegularLocalRing.eq_bot_or_eq_maximalIdeal_or_eq_span_singleton_of_quotient_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/QuotientNodal.lean, line 132. The attribute's comment: “reduced_quotient”.

An ideal with reduced quotient in a two-dimensional regular local ring is zero, maximal, or generated by a nonzero element of the maximal ideal.

public theorem eq_bot_or_eq_maximalIdeal_or_eq_span_singleton_of_quotient_isReduced
    {A : Type*} [CommRing A] [IsRegularLocalRing A] (hdim : ringKrullDim A = 2)
    (I : Ideal A) (hI : I ≤ IsLocalRing.maximalIdeal A) [IsReduced (A ⧸ I)] :
      I = ⊥ ∨ I = IsLocalRing.maximalIdeal A ∨
      ∃ f : A, f ≠ 0 ∧ f ∈ IsLocalRing.maximalIdeal A ∧ I = Ideal.span {f}

IsRegularLocalRing.exists_ne_zero_mem_maximalIdeal_and_eq_span_singleton_of_quotient_depth_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteLocalRing/QuotientNodal.lean, line 157. The attribute's comment: “depth_one_quotient”.

An ideal in a two-dimensional regular local ring whose quotient has depth one is generated by a nonzero element of the maximal ideal.

public theorem exists_ne_zero_mem_maximalIdeal_and_eq_span_singleton_of_quotient_depth_eq_one
    {A : Type u} [CommRing A] [IsRegularLocalRing A] (hdim : ringKrullDim A = 2)
    (I : Ideal A) (hI : I ≤ IsLocalRing.maximalIdeal A)
    (hdepth : Module.depth A (IsLocalRing.maximalIdeal A) (A ⧸ I) = 1) :
    ∃ f : A, f ≠ 0 ∧ f ∈ IsLocalRing.maximalIdeal A ∧ I = Ideal.span {f}

Tag 0C49, a lemma

Tag 0C49 in the Stacks Project.

Stacks.Curves.isNodalAlgebra_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Node/Algebra.lean, line 1762.

For a Noetherian local algebra over a field, the following are equivalent: it is reduced with a nondegenerate quadratic relation on its two-dimensional cotangent space; it has depth one with the same relation; and its completion is a two-variable power-series hypersurface defined by a nondegenerate quadratic form. In all three conditions the residue-field extension is separable.

public theorem isNodalAlgebra_tfae (k : Type u) (A : Type v) [Field k] [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] [Algebra k A] :
    List.TFAE [
      IsNodalAlgebra k A,
      Algebra.IsSeparableExtension k (ResidueField A) ∧
        Module.depth A (maximalIdeal A) A = 1 ∧ HasNodalQuadraticRelation A,
      Algebra.IsSeparableExtension k (ResidueField A) ∧ HasNodalCompletion k A]

Tag 0C4A, a lemma

Tag 0C4A in the Stacks Project.

Stacks.Curves.encard_maximalSpectrum_integralClosure_fractionRing_eq_one_or_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeQuadraticAlgebra/MaximalIdeals.lean, line 58. The attribute's comment: “number of maximal ideals”.

The normalization of a nodal Nagata local algebra in its total ring of fractions has one or two maximal ideals.

public theorem encard_maximalSpectrum_integralClosure_fractionRing_eq_one_or_two
    (k : Type u) (A : Type v) [Field k] [CommRing A] [IsLocalRing A] [Algebra k A]
    (hA : IsNagataRing A) (hNodal : IsNodalAlgebra k A) :
    Set.encard (Set.univ : Set (MaximalSpectrum ↥(integralClosure A (FractionRing A)))) = 1 ∨
      Set.encard
        (Set.univ : Set (MaximalSpectrum ↥(integralClosure A (FractionRing A)))) = 2

Stacks.Curves.isNodalAlgebra_iff_deltaInvariant_eq_one_and_two_geometricBranches, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeQuadraticAlgebra/NodalCharacterization.lean, line 96. The attribute's comment: “equivalence”. References: SGA 7 X (2.24), “more general”.

A Nagata local algebra over a field is nodal if and only if it is reduced and one-dimensional, its residue field is separable, its delta invariant is one, and it has two geometric branches.

public theorem isNodalAlgebra_iff_deltaInvariant_eq_one_and_two_geometricBranches
    (k : Type u) (A : Type v) [Field k] [CommRing A] [IsLocalRing A] [Algebra k A]
    (hA : IsNagataRing A) :
    IsNodalAlgebra k A ↔
      Algebra.IsSeparableExtension k (ResidueField A) ∧
        IsReduced A ∧
        ringKrullDim A = 1 ∧
        Ring.deltaInvariant A = 1 ∧
        numberOfGeometricBranchesOfLocalRing A = 2

Stacks.Curves.isSeparableExtension_residueField_integralClosure_fractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeQuadraticAlgebra/ResidueFields.lean, line 113. The attribute's comment: “residue field extensions”.

The residue field at every maximal ideal of the normalization of a nodal Nagata local algebra is separable over the ground field.

public theorem isSeparableExtension_residueField_integralClosure_fractionRing
    (k : Type u) (A : Type v) [Field k] [CommRing A] [IsLocalRing A] [Algebra k A]
    (hA : IsNagataRing A) (hNodal : IsNodalAlgebra k A)
    (m : MaximalSpectrum ↥(integralClosure A (FractionRing A))) :
    Algebra.IsSeparableExtension k m.asIdeal.ResidueField

Tag 0C4B, a lemma

Tag 0C4B in the Stacks Project.

Stacks.Curves.jacobianMinorIdealModulo_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/JacobianMinorIdeal.lean, line 338.

The ideal of Jacobian minors in a quotient of a finite-variable formal power-series ring is independent of both the finite family generating the defining ideal and the regular system of parameters used to form the Jacobian matrix.

theorem jacobianMinorIdealModulo_eq {n m l : ℕ}
    (I : Ideal (MvPowerSeries (Fin n) k))
    (f : Fin m → MvPowerSeries (Fin n) k) (g : Fin l → MvPowerSeries (Fin n) k)
    (hf : Ideal.span (Set.range f) = I) (hg : Ideal.span (Set.range g) = I)
    (y : Fin n → IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) k))
    (hy : IsRegularSystemOfParameters y) (r : ℕ) :
    jacobianMinorIdealModulo I f r = jacobianMinorIdealModuloInParameters I y hy g r

Tag 0C4C, a lemma

Tag 0C4C in the Stacks Project.

Stacks.Curves.isNodalAlgebra_jacobianMinorIdeal_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/JacobianCriterionReduction.lean, line 619.

The Jacobian criterion for a node. A quotient of a finite-variable formal power-series ring by equations in its maximal ideal is nodal if and only if it is reduced (equivalently, has depth one) and its next-to-maximal Jacobian minors generate the maximal ideal.

The Jacobian-minor ideal is the one of Tag 0C4B (Stacks.Curves.jacobianMinorIdealModulo). The source states the Jacobian condition as the minors generating I + 𝔪_A in the power-series ring; the equivalent intrinsic equality between their image and the maximal ideal of the quotient is used here, and the depth condition is likewise written over the quotient ring.

theorem isNodalAlgebra_jacobianMinorIdeal_tfae (k : Type u) [Field k] {n m : ℕ}
    (I : Ideal (MvPowerSeries (Fin n) k))
    (f : Fin m → MvPowerSeries (Fin n) k)
    (hf : Ideal.span (Set.range f) = I)
    (hI : I ≤ maximalIdeal (MvPowerSeries (Fin n) k)) :
    letI : Nontrivial (MvPowerSeries (Fin n) k ⧸ I) :=
      Ideal.Quotient.nontrivial_iff.mpr
        (ne_top_of_le_ne_top
          (maximalIdeal.isMaximal (MvPowerSeries (Fin n) k)).ne_top hI)
    letI : IsLocalRing (MvPowerSeries (Fin n) k ⧸ I) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
    List.TFAE [
      IsNodalAlgebra k (MvPowerSeries (Fin n) k ⧸ I),
      IsReduced (MvPowerSeries (Fin n) k ⧸ I) ∧
        jacobianMinorIdealModulo I f (n - 1) =
          maximalIdeal (MvPowerSeries (Fin n) k ⧸ I),
      Module.depth (MvPowerSeries (Fin n) k ⧸ I)
          (maximalIdeal (MvPowerSeries (Fin n) k ⧸ I))
          (MvPowerSeries (Fin n) k ⧸ I) = 1 ∧
        jacobianMinorIdealModulo I f (n - 1) =
          maximalIdeal (MvPowerSeries (Fin n) k ⧸ I)]

Tag 0C4D, a lemma

Tag 0C4D in the Stacks Project.

Stacks.Curves.isNode_tfae_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeFittingIdealClosedPoint.lean, line 481.

Stacks Project, Tag 0C4D. Let k be a field, let X be a one-dimensional scheme locally of finite type over k and let x be a closed point of X. The following are equivalent.

x is a node.

𝒪_{X,x} is a nodal k-algebra.

Every point of X_{k̄} above x is an ordinary double point.

κ(x)/k is separable, 𝒪_{X,x} is reduced, and the stalk at x of the first Fitting ideal sheaf of Ω_{X/k} is the maximal ideal of 𝒪_{X,x}.

The same with reducedness replaced by depth one.

κ(x)/k is separable and 𝒪_{X,x} is reduced of delta invariant one with two geometric branches.

Each of the six conditions implies that κ(x)/k is separable: conditions (2), (4), (5) and (6) say so outright, and conditions (1) and (3) by Stacks.Curves.isSeparableExtension_residueField_of_isNode. Under that separability the six are equivalent by Stacks.Curves.isNode_iff_and_isNode_of_depth_of_isSeparableExtension, which supplies the two Fitting-ideal equivalences that Stacks.Curves.isNode_tfae_of_fittingIdeal_equivalence leaves open; so the cycle of implications 1 → 2 → 3 → 4 → 5 → 6 → 1 may be run with the separability of its source clause in hand.

theorem isNode_tfae_of_isClosed
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [LocallyOfFiniteType (X ↘ Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) (hx : IsClosed ({x} : Set X)) :
    let f : X ⟶ Spec (.of k) := X ↘ Spec (.of k)
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.presheaf.germ ⊤ x (by simp)).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
    let fittingCondition : Prop :=
      IdealSheafData.stalk (fittingIdeal (Scheme.Hom.relativeDifferentials f) (1 : ℤ)) x =
        maximalIdeal (X.presheaf.stalk x)
    let c₁ : Prop := IsNode k X x
    let c₂ : Prop := IsNodalAlgebra k (X.presheaf.stalk x)
    let c₃ : Prop :=
      (let K := AlgebraicClosure k
       let g : Spec (.of K) ⟶ Spec (.of k) := Spec.map (CommRingCat.ofHom (algebraMap k K))
       let Y := (pullback f g : Scheme.{u})
       let p : Y ⟶ X := pullback.fst f g
       let q : Y ⟶ Spec (.of K) := pullback.snd f g
       letI : Y.Over (Spec (.of K)) := ⟨q⟩
       ∀ xbar : Y, p.base xbar = x → IsOrdinaryDoublePoint K Y xbar)
    let c₄ : Prop :=
      Algebra.IsSeparableExtension k (X.residueField x) ∧
        _root_.IsReduced (X.presheaf.stalk x) ∧ fittingCondition
    let c₅ : Prop :=
      Algebra.IsSeparableExtension k (X.residueField x) ∧
        Module.depth (X.presheaf.stalk x) (maximalIdeal (X.presheaf.stalk x))
            (X.presheaf.stalk x) = 1 ∧
          fittingCondition
    let c₆ : Prop :=
      Algebra.IsSeparableExtension k (X.residueField x) ∧
        _root_.IsReduced (X.presheaf.stalk x) ∧
          Ring.deltaInvariant (X.presheaf.stalk x) = 1 ∧
            AlgebraicGeometry.numberOfGeometricBranches X x = 2
    List.TFAE [c₁, c₂, c₃, c₄, c₅, c₆]

Stacks.Curves.isNodalAlgebra_stalk_iff_isReduced_and_stalk_fittingIdeal_eq_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeFittingIdealCriterion.lean, line 135. The attribute's comment: “clauses (2) and (4), at a closed point of an affine chart admitting a presentation centred there”.

Conditions (2) and (4) of Tag 0C4D are equivalent. The local ring at a closed point x is a nodal algebra over a base field k exactly when its residue field is separable over k, it is reduced, and the stalk at x of the first Fitting ideal sheaf of Ω_{X/S} is its maximal ideal.

The two conditions share their separability and reducedness clauses; what is proved here is that the nodal quadratic relation on 𝒪_{X,x} is the Fitting-ideal condition, which is Stacks.Curves.stalk_fittingIdeal_eq_maximalIdeal_iff_hasNodalQuadraticRelation. The base field k is not required to be the base of the morphism: no clause of either condition relates the two beyond the k-algebra structure on 𝒪_{X,x}, which is an argument.

theorem isNodalAlgebra_stalk_iff_isReduced_and_stalk_fittingIdeal_eq_maximalIdeal
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] (x : X)
    (U : X.affineOpens) (hxU : x ∈ U.1) (hx : IsClosed ({x} : Set X))
    {V : S.Opens} (hV : IsAffineOpen V) (hUV : (U : X.Opens) ≤ f ⁻¹ᵁ V)
    [IsNoetherianRing Γ(S, V)] (K : Type u) [Field K] (e : Γ(S, V) ≃+* K)
    (k : Type u) [Field k] [Algebra k (X.presheaf.stalk x)] :
    letI := Stacks.Smooth.algebraAppLE f hUV
    ∀ {n m : ℕ} (P : Algebra.Presentation Γ(S, V) Γ(X, U.1) (Fin n) (Fin m))
      (_hv : ∀ i, P.val i ∈ (U.2.primeIdealOf ⟨x, hxU⟩).asIdeal),
      (IsNodalAlgebra k (X.presheaf.stalk x) ↔
        Algebra.IsSeparableExtension k (ResidueField (X.presheaf.stalk x)) ∧
          IsReduced (X.presheaf.stalk x) ∧
            IdealSheafData.stalk (fittingIdeal (Scheme.Hom.relativeDifferentials f) (1 : ℤ)) x =
              maximalIdeal (X.presheaf.stalk x))

Stacks.Curves.isNode_tfae_of_rational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeFittingIdealRationalPoint.lean, line 184. The attribute's comment: “all six clauses, at a closed point whose residue field is the base field”.

All six conditions of Stacks Tag 0C4D are equivalent at a rational closed point.

Let k be a field, let X be a one-dimensional scheme locally of finite type over k and let x be a closed point of X whose residue field is k itself — the hypothesis hrat says that the structure map k → κ(x) is surjective. Then the six conditions of the tag are equivalent, with no further hypothesis.

The two equivalences that Stacks.Curves.isNode_tfae_of_fittingIdeal_equivalence leaves open are discharged by Stacks.Curves.stalk_fittingIdeal_eq_maximalIdeal_iff_hasNodalQuadraticRelation_of_rational, which turns the Fitting-ideal condition into the nodal quadratic relation: condition (1) becomes condition (4) through condition (2), and condition (5) becomes condition (4) because the exchange of depth one for reducedness in the presence of the nodal relation is Stacks Tag 0C49.

What keeps this short of the tag is only the rationality of κ(x): a presentation of an affine chart whose generators vanish at x exists exactly then, since generators lying in the prime of x generate κ(x) over k by zero.

A general closed point has κ(x) / k finite and, by Stacks.Curves.isSeparableExtension_residueField_of_isNode and the separability clause of conditions (2), (4), (5) and (6), separable in every case that matters. Reducing it to the rational case asks only for the Fitting-ideal condition to descend along the base change to the algebraic closure: Tag 0C3I (AlgebraicGeometry.fittingIdeal_relativeDifferentials_comap) together with AlgebraicGeometry.IdealSheafData.stalk_comap makes the stalk of the Fitting ideal upstairs the extension of the stalk downstairs, Tag 0C50 (AlgebraicGeometry.map_maximalIdeal_stalkMap_eq_of_isReduced_tensorProduct) makes the maximal ideal upstairs the extension of the maximal ideal downstairs, and faithful flatness of the stalk map retracts the extension of ideals. That descent is carried out in StacksFrontier.AlgebraicGeometry.Curves.NodeFittingIdealClosedPoint, where Stacks.Curves.isNode_tfae_of_isClosed states the six conditions at an arbitrary closed point; it also needs reducedness and depth one to cross between the two points, and they cross in opposite directions.

theorem isNode_tfae_of_rational
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) (hx : IsClosed ({x} : Set X))
    (hrat : Function.Surjective ((X.residue x).hom.comp
      ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ AlgebraicGeometry.Spec (.of k)).appTop ≫
        X.presheaf.germ ⊤ x (by simp)).hom)) :
    let f : X ⟶ AlgebraicGeometry.Spec (.of k) := X ↘ AlgebraicGeometry.Spec (.of k)
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.presheaf.germ ⊤ x (by simp)).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
    let omega := f.relativeDifferentials
    let fittingCondition : Prop :=
      AlgebraicGeometry.IdealSheafData.stalk (AlgebraicGeometry.fittingIdeal omega 1) x =
        maximalIdeal (X.presheaf.stalk x)
    let c₁ : Prop := IsNode k X x
    let c₂ : Prop := IsNodalAlgebra k (X.presheaf.stalk x)
    let c₃ : Prop :=
      (let K := AlgebraicClosure k
       let g : AlgebraicGeometry.Spec (.of K) ⟶ AlgebraicGeometry.Spec (.of k) :=
         AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K))
       let Y := (CategoryTheory.Limits.pullback f g : Scheme.{u})
       let p : Y ⟶ X := CategoryTheory.Limits.pullback.fst f g
       let q : Y ⟶ AlgebraicGeometry.Spec (.of K) := CategoryTheory.Limits.pullback.snd f g
       letI : Y.Over (AlgebraicGeometry.Spec (.of K)) := ⟨q⟩
       ∀ xbar : Y, p.base xbar = x → IsOrdinaryDoublePoint K Y xbar)
    let c₄ : Prop :=
      Algebra.IsSeparableExtension k (X.residueField x) ∧
        _root_.IsReduced (X.presheaf.stalk x) ∧ fittingCondition
    let c₅ : Prop :=
      Algebra.IsSeparableExtension k (X.residueField x) ∧
        Module.depth (X.presheaf.stalk x) (maximalIdeal (X.presheaf.stalk x))
            (X.presheaf.stalk x) = 1 ∧
          fittingCondition
    let c₆ : Prop :=
      Algebra.IsSeparableExtension k (X.residueField x) ∧
        _root_.IsReduced (X.presheaf.stalk x) ∧
          Ring.deltaInvariant (X.presheaf.stalk x) = 1 ∧
            AlgebraicGeometry.numberOfGeometricBranches X x = 2
    List.TFAE [c₁, c₂, c₃, c₄, c₅, c₆]

Stacks.Curves.ringKrullDim_stalk_eq_one_and_depth_eq_one_of_isNode, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeLocalRingDepth.lean, line 64. The attribute's comment: “the dimension and the depth of the local ring at a node, over an arbitrary base field: the depth clause of condition (5), from condition (1)”.

The local ring at a node of a one-dimensional scheme locally of finite type over an arbitrary field is one-dimensional of depth one.

The depth assertion is the depth clause of condition (5) of Stacks Tag 0C4D, derived from condition (1) over an arbitrary field; no separability of the residue field extension is used or asserted.

theorem ringKrullDim_stalk_eq_one_and_depth_eq_one_of_isNode
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) (hnode : IsNode k X x) :
    ringKrullDim (X.presheaf.stalk x) = 1 ∧
      Module.depth (X.presheaf.stalk x) (maximalIdeal (X.presheaf.stalk x))
        (X.presheaf.stalk x) = 1

Stacks.Curves.isNodalAlgebra_stalk_iff_isSeparableExtension_of_isNode, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeLocalRingDepth.lean, line 93. The attribute's comment: “conditions (1) and (2) over an arbitrary base field, at a point already known to be a node: the nodal-algebra condition on the local ring is exactly separability of the residue field extension”.

At a node of a one-dimensional scheme locally of finite type over an arbitrary field, the local ring is a nodal k-algebra exactly when the residue field extension is separable.

This is the whole of the gap between conditions (1) and (2) of Stacks Tag 0C4D over an arbitrary field: the implication from (1) to (2) holds as soon as κ(x)/k is separable, and separability is itself one of the clauses of (2).

theorem isNodalAlgebra_stalk_iff_isSeparableExtension_of_isNode
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) (hnode : IsNode k X x) :
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ AlgebraicGeometry.Spec (.of k)).appTop ≫
        X.presheaf.germ ⊤ x (by simp)).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
    (IsNodalAlgebra k (X.presheaf.stalk x) ↔
      Algebra.IsSeparableExtension k (X.residueField x))

Stacks.Curves.isNode_of_isNodalAlgebra_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeNodalAlgebraAscent.lean, line 88. The attribute's comment: “clause (2) implies clause (1), over an arbitrary base field”.

Condition (2) of Stacks Tag 0C4D implies condition (1), over an arbitrary field.

If the local ring at a point of a one-dimensional scheme locally of finite type over k is a nodal k-algebra, then the point is a node.

theorem isNode_of_isNodalAlgebra_stalk
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) :
    letI : Algebra k (X.presheaf.stalk x) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ AlgebraicGeometry.Spec (.of k)).appTop ≫
        X.presheaf.germ ⊤ x trivial).hom.toAlgebra
    IsNodalAlgebra k (X.presheaf.stalk x) → IsNode k X x

Stacks.Curves.isNode_iff_isNodalAlgebra_stalk_of_isSeparableExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeNodalAlgebraAscent.lean, line 160. The attribute's comment: “clauses (1) and (2), at a point whose residue field is separable over the base field”.

Conditions (1) and (2) of Stacks Tag 0C4D agree at a point whose residue field is separable over the base field.

Separability of κ(x)/k is a clause of condition (2); it is assumed here, and discharged in Stacks.Curves.isSeparableExtension_residueField_of_isNode, which makes Stacks.Curves.isNode_iff_isNodalAlgebra_stalk the unconditional equivalence. Everything else is proved: condition (1) with separability gives condition (2) by Stacks.Curves.isNodalAlgebra_stalk_of_isNode_of_isSeparableExtension, and condition (2) gives condition (1) by Stacks.Curves.isNode_of_isNodalAlgebra_stalk, over an arbitrary field.

theorem isNode_iff_isNodalAlgebra_stalk_of_isSeparableExtension
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) :
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ AlgebraicGeometry.Spec (.of k)).appTop ≫
        X.presheaf.germ ⊤ x trivial).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
    Algebra.IsSeparableExtension k (X.residueField x) →
      (IsNode k X x ↔ IsNodalAlgebra k (X.presheaf.stalk x))

Stacks.Curves.isNode_tfae_of_isSeparableExtension_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeNodalAlgebraAscent.lean, line 187. The attribute's comment: “clauses (1), (2), (3) and (6), at a point whose residue field is separable over the base field”.

The four conditions of Stacks Tag 0C4D that do not mention the Fitting ideal are equivalent, over an arbitrary field, at a point whose residue field is separable over the base field.

Conditions (1), (2), (3) and (6) of the tag. The hypothesis c₂ → c₁ of Stacks.Curves.isNode_tfae_of_isSeparableExtension is discharged by Stacks.Curves.isNode_of_isNodalAlgebra_stalk; what remains assumed is separability of κ(x)/k, which is a clause of conditions (2), (4), (5) and (6). That hypothesis is discharged in Stacks.Curves.isNode_tfae, the same equivalence with no hypothesis beyond closedness of the point.

theorem isNode_tfae_of_isSeparableExtension_residueField
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) (hx : IsClosed ({x} : Set X)) :
    let f : X ⟶ AlgebraicGeometry.Spec (.of k) := X ↘ AlgebraicGeometry.Spec (.of k)
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.presheaf.germ ⊤ x (by simp)).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
    let c₁ : Prop := IsNode k X x
    let c₂ : Prop := IsNodalAlgebra k (X.presheaf.stalk x)
    let c₃ : Prop :=
      (let K := AlgebraicClosure k
       let g : AlgebraicGeometry.Spec (.of K) ⟶ AlgebraicGeometry.Spec (.of k) :=
         AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K))
       let Y := (pullback f g : Scheme.{u})
       let p : Y ⟶ X := pullback.fst f g
       let q : Y ⟶ AlgebraicGeometry.Spec (.of K) := pullback.snd f g
       letI : Y.Over (AlgebraicGeometry.Spec (.of K)) := ⟨q⟩
       ∀ xbar : Y, p.base xbar = x → IsOrdinaryDoublePoint K Y xbar)
    let c₆ : Prop :=
      Algebra.IsSeparableExtension k (X.residueField x) ∧
        _root_.IsReduced (X.presheaf.stalk x) ∧
          Ring.deltaInvariant (X.presheaf.stalk x) = 1 ∧
            AlgebraicGeometry.numberOfGeometricBranches X x = 2
    Algebra.IsSeparableExtension k (X.residueField x) → List.TFAE [c₁, c₂, c₃, c₆]

Stacks.Curves.isSeparableExtension_residueField_of_isNode, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeResidueFieldSeparable.lean, line 134. The attribute's comment: “the separability of the residue field extension, from condition (1), over an arbitrary base field”.

The residue field at a node is separable over the base field.

This is the clause of conditions (2), (4), (5) and (6) of Stacks Tag 0C4D that conditions (1) and (3) do not display, and the source obtains it from the closed subscheme cut out by the first Fitting ideal of Ω_{X/k}. The route here is different and stays inside the delta invariant.

Base change to k^{1/p}. At a node the maximal ideal of 𝒪_{X,x} generates the maximal ideal upstairs (Stacks.Curves.isField_specialFibre_of_isNode), so the special fibre of the map on local rings is a field. That special fibre is the localization of κ(x) ⊗_k k^{1/p} at the prime cut out by the chosen point (Stacks Tag 0C4Y), so a nonzero reduced flat algebra over κ(x) ⊗_k k^{1/p} exists, which forces κ(x) ⊗_k k^{1/p} itself to be reduced — every element of it is a unit or nilpotent, so its maximal ideal acts as zero and flatness upgrades to faithful flatness. Reducedness of κ(x) ⊗_k k^{1/p} is separability of κ(x)/k by Stacks Tag 030W.

theorem isSeparableExtension_residueField_of_isNode
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) :
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ AlgebraicGeometry.Spec (.of k)).appTop ≫
        X.presheaf.germ ⊤ x (by simp)).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
    IsNode k X x → Algebra.IsSeparableExtension k (X.residueField x)

Stacks.Curves.isNode_iff_isNodalAlgebra_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeResidueFieldSeparable.lean, line 180. The attribute's comment: “clauses (1) and (2), over an arbitrary base field”.

Conditions (1) and (2) of Stacks Tag 0C4D agree over an arbitrary field.

A point of a one-dimensional scheme locally of finite type over k is a node exactly when its local ring is a nodal k-algebra. Separability of κ(x)/k, the one clause of condition (2) that condition (1) does not display, is supplied by Stacks.Curves.isSeparableExtension_residueField_of_isNode.

theorem isNode_iff_isNodalAlgebra_stalk
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) :
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ AlgebraicGeometry.Spec (.of k)).appTop ≫
        X.presheaf.germ ⊤ x (by simp)).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
    (IsNode k X x ↔ IsNodalAlgebra k (X.presheaf.stalk x))

Stacks.Curves.isNode_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeResidueFieldSeparable.lean, line 205. The attribute's comment: “clauses (1), (2), (3) and (6), over an arbitrary base field”.

The four conditions of Stacks Tag 0C4D that do not mention the first Fitting ideal are equivalent over an arbitrary field.

Conditions (1), (2), (3) and (6) of the tag, at a closed point of a one-dimensional scheme locally of finite type over an arbitrary field, with no hypothesis beyond closedness of the point. Each of the four implies that κ(x)/k is separable — conditions (2) and (6) say so outright, and conditions (1) and (3) by Stacks.Curves.isSeparableExtension_residueField_of_isNode — and under that separability the four are already known to be equivalent.

theorem isNode_tfae
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) (hx : IsClosed ({x} : Set X)) :
    let f : X ⟶ AlgebraicGeometry.Spec (.of k) := X ↘ AlgebraicGeometry.Spec (.of k)
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.presheaf.germ ⊤ x (by simp)).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
    let c₁ : Prop := IsNode k X x
    let c₂ : Prop := IsNodalAlgebra k (X.presheaf.stalk x)
    let c₃ : Prop :=
      (let K := AlgebraicClosure k
       let g : AlgebraicGeometry.Spec (.of K) ⟶ AlgebraicGeometry.Spec (.of k) :=
         AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K))
       let Y := (pullback f g : Scheme.{u})
       let p : Y ⟶ X := pullback.fst f g
       let q : Y ⟶ AlgebraicGeometry.Spec (.of K) := pullback.snd f g
       letI : Y.Over (AlgebraicGeometry.Spec (.of K)) := ⟨q⟩
       ∀ xbar : Y, p.base xbar = x → IsOrdinaryDoublePoint K Y xbar)
    let c₆ : Prop :=
      Algebra.IsSeparableExtension k (X.residueField x) ∧
        _root_.IsReduced (X.presheaf.stalk x) ∧
          Ring.deltaInvariant (X.presheaf.stalk x) = 1 ∧
            AlgebraicGeometry.numberOfGeometricBranches X x = 2
    List.TFAE [c₁, c₂, c₃, c₆]

Stacks.Curves.isNodalAlgebra_stalk_iff_deltaInvariant_eq_one_and_two_geometricBranches, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeStalkCharacterization.lean, line 160. The attribute's comment: “clauses (2) and (6)”.

The local ring at a point of a one-dimensional scheme locally of finite type over a field is a nodal algebra if and only if the residue field is separable, the local ring is reduced, its delta invariant is one and it has two geometric branches.

This is the equivalence of conditions (2) and (6) of Stacks Tag 0C4D. Its content is the algebraic equivalence of Stacks Tag 0C4A, whose two further hypotheses are discharged here: the local ring is Nagata because the scheme is locally of finite type over a field, and it is one-dimensional because its dimension is at most that of the scheme while a reduced local ring of delta invariant one is not a field.

theorem isNodalAlgebra_stalk_iff_deltaInvariant_eq_one_and_two_geometricBranches
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [LocallyOfFiniteType (X ↘ Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) :
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop ≫
        X.presheaf.germ ⊤ x (by simp)).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
    (IsNodalAlgebra k (X.presheaf.stalk x) ↔
      Algebra.IsSeparableExtension k (X.residueField x) ∧
        IsReduced (X.presheaf.stalk x) ∧
          Ring.deltaInvariant (X.presheaf.stalk x) = 1 ∧
            numberOfGeometricBranches X x = 2)

Stacks.Curves.isNode_iff_forall_isOrdinaryDoublePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeTFAE.lean, line 114. The attribute's comment: “clauses (1) and (3)”.

A closed point of a scheme locally of finite type over an arbitrary field is a node exactly when every point of the base change to the algebraic closure above it is an ordinary double point.

This is the equivalence of conditions (1) and (3) of Stacks Tag 0C4D, over an arbitrary field. The definition of a node asks only that some point above x be an ordinary double point; the two agree because the automorphisms of the algebraic closure act transitively on the points above x, which is Stacks.Curves.forall_isOrdinaryDoublePoint_of_isNode.

theorem isNode_iff_forall_isOrdinaryDoublePoint
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))] (x : X)
    (hx : IsClosed ({x} : Set X)) :
    let f : X ⟶ AlgebraicGeometry.Spec (.of k) := X ↘ AlgebraicGeometry.Spec (.of k)
    (IsNode k X x ↔
      (let K := AlgebraicClosure k
       let g : AlgebraicGeometry.Spec (.of K) ⟶ AlgebraicGeometry.Spec (.of k) :=
         AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K))
       let Y := (pullback f g : Scheme.{u})
       let p : Y ⟶ X := pullback.fst f g
       let q : Y ⟶ AlgebraicGeometry.Spec (.of K) := pullback.snd f g
       letI : Y.Over (AlgebraicGeometry.Spec (.of K)) := ⟨q⟩
       ∀ xbar : Y, p.base xbar = x → IsOrdinaryDoublePoint K Y xbar))

Stacks.Curves.isNode_tfae_of_isAlgClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeTFAE.lean, line 189. The attribute's comment: “clauses (1), (2), (3) and (6), for an algebraically closed base field”.

The four conditions of Stacks Tag 0C4D that do not mention the Fitting ideal are equivalent over an algebraically closed field.

Conditions (1), (2), (3) and (6) of the tag. The equivalence of (1) and (2) over an algebraically closed field is Stacks.Curves.isNode_iff_isNodalAlgebra_stalk_of_isAlgClosed, which is the only hypothesis of Stacks.Curves.isNode_tfae_of_isNode_iff_isNodalAlgebra_stalk.

theorem isNode_tfae_of_isAlgClosed
    (k : Type u) [Field k] [IsAlgClosed k] (X : Scheme.{u})
    [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (hX : topologicalKrullDim X = 1) (x : X) (hx : IsClosed ({x} : Set X)) :
    let f : X ⟶ AlgebraicGeometry.Spec (.of k) := X ↘ AlgebraicGeometry.Spec (.of k)
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫
        X.presheaf.germ ⊤ x (by simp)).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) :=
      ((X.residue x).hom.comp kToStalk).toAlgebra
    List.TFAE [
      IsNode k X x,
      IsNodalAlgebra k (X.presheaf.stalk x),
      (let K := AlgebraicClosure k
       let g : AlgebraicGeometry.Spec (.of K) ⟶ AlgebraicGeometry.Spec (.of k) :=
         AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K))
       let Y := (pullback f g : Scheme.{u})
       let p : Y ⟶ X := pullback.fst f g
       let q : Y ⟶ AlgebraicGeometry.Spec (.of K) := pullback.snd f g
       letI : Y.Over (AlgebraicGeometry.Spec (.of K)) := ⟨q⟩
       ∀ xbar : Y, p.base xbar = x → IsOrdinaryDoublePoint K Y xbar),
      Algebra.IsSeparableExtension k (X.residueField x) ∧
        IsReduced (X.presheaf.stalk x) ∧
          Ring.deltaInvariant (X.presheaf.stalk x) = 1 ∧
            AlgebraicGeometry.numberOfGeometricBranches X x = 2]

Tag 0CBT, a remark

Tag 0CBT in the Stacks Project.

Stacks.Curves.quadraticAlgebra_equiv_adjoinRoot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeQuadraticAlgebra/AdjoinRoot.lean, line 570. The attribute's comment: “three_descriptions”.

The quadratic algebra of a node is isomorphic over the residue field κ to κ[X]/(a X² + b X + c), where a, b, c are the residues of the coefficients of a quadratic relation a x² + b x y + c y² ∈ 𝔪³ in lifted cotangent coordinates.

public theorem quadraticAlgebra_equiv_adjoinRoot (k : Type u) (A : Type v) [Field k] [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] [Algebra k A]
    (hA : IsNodalAlgebra k A)
    (x y : maximalIdeal A)
    (e : Module.Basis (BinaryIndex (ResidueField A)) (ResidueField A) (CotangentSpace A))
    (hx : e ⟨0⟩ = (maximalIdeal A).toCotangent x)
    (hy : e ⟨1⟩ = (maximalIdeal A).toCotangent y)
    (a b c : A) (ha : residue A a ≠ 0)
    (hdisc : residue A (4 * a * c - b ^ 2) ≠ 0)
    (hrelation : a * x.1 ^ 2 + b * x.1 * y.1 + c * y.1 ^ 2 ∈ (maximalIdeal A) ^ 3) :
    Nonempty (quadraticAlgebra A ≃ₐ[ResidueField A]
      AdjoinRoot (Polynomial.C (residue A a) * Polynomial.X ^ 2 +
        Polynomial.C (residue A b) * Polynomial.X + Polynomial.C (residue A c)))

Stacks.Curves.quadraticAlgebra, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeQuadraticAlgebra/Defs.lean, line 40. The attribute's comment: “quadratic_algebra_associated_to_a_node”.

The quadratic algebra associated to a local ring: the closed fibre of its normalization inside its total ring of fractions.

public abbrev quadraticAlgebra (A : Type u) [CommRing A] [IsLocalRing A]

Stacks.Curves.isSeparable_quadraticAlgebra_of_isNodalAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeQuadraticAlgebra/DegreeSeparable.lean, line 133. The attribute's comment: “degree_separable”.

The quadratic algebra of a nodal local ring is separable over its residue field.

public theorem isSeparable_quadraticAlgebra_of_isNodalAlgebra (hA : IsNodalAlgebra k A) :
    Algebra.IsSeparable (ResidueField A) (quadraticAlgebra A)

Stacks.Curves.finrank_quadraticAlgebra_of_isNodalAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeQuadraticAlgebra/DegreeSeparable.lean, line 151. The attribute's comment: “degree_separable”.

The quadratic algebra of a nodal local ring has degree two over its residue field.

public theorem finrank_quadraticAlgebra_of_isNodalAlgebra (hA : IsNodalAlgebra k A) :
    Module.finrank (ResidueField A) (quadraticAlgebra A) = 2

Stacks.Curves.quadraticAlgebraSpecIsoNormalizationFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeQuadraticAlgebra/NormalizationFibre.lean, line 101. The attribute's comment: “normalization_fibre”.

The spectrum of the quadratic algebra associated to a node is the fibre of the normalization over that node.

public theorem quadraticAlgebraSpecIsoNormalizationFiber
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [IsLocallyNoetherian X] (x : X)
    (hnode :
      let kToStalk : k →+* X.presheaf.stalk x :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.presheaf.germ ⊤ x trivial).hom
      letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
      IsNodalAlgebra k (X.presheaf.stalk x)) :
    let hX : ∀ U : X.Opens, IsCompact (U : Set X) →
        (irreducibleComponents U).Finite := fun U hU ↦ by
      let : CompactSpace U := isCompact_iff_compactSpace.mp hU
      let : NoetherianSpace U :=
        noetherianSpace_of_isLocallyNoetherianSpace U
          ((isLocallyNoetherianSpace_of_isLocallyNoetherian X).subtype U)
      exact NoetherianSpace.finite_irreducibleComponents
    letI : Algebra (X.residueField x)
        (quadraticAlgebra (X.presheaf.stalk x)) := by
      change Algebra (IsLocalRing.ResidueField (X.presheaf.stalk x))
        (quadraticAlgebra (X.presheaf.stalk x))
      infer_instance
    Nonempty
      (Over.mk (Spec.map (
        let A := X.presheaf.stalk x
        let B := integralClosure A (FractionRing A)
        let J := (IsLocalRing.maximalIdeal A).map (algebraMap A B)
        let f : A →+* (B ⧸ J) := (Ideal.Quotient.mk J).comp (algebraMap A B)
        let g : IsLocalRing.ResidueField A →+* (B ⧸ J) :=
          Ideal.Quotient.lift (IsLocalRing.maximalIdeal A) f fun _a ha ↦
            Ideal.Quotient.eq_zero_iff_mem.mpr
              (Ideal.mem_map_of_mem (algebraMap A B) ha)
        let g' : @RingHom (IsLocalRing.ResidueField A) (B ⧸ J)
            (X.residueField x).commRing.toCommSemiring.toNonAssocSemiring
            (CommRingCat.of (B ⧸ J)).commRing.toCommSemiring.toNonAssocSemiring := {
          toFun := g
          map_one' := g.map_one
          map_mul' := g.map_mul
          map_zero' := g.map_zero
          map_add' := g.map_add }
        CommRingCat.ofHom g')) ≅
        Over.mk (pullback.snd (Scheme.normalization X hX)
          (X.fromSpecResidueField x)))

Stacks.Curves.proj_associatedGraded_iso_quadraticAlgebraSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeQuadraticAlgebra/ProjTangentCone.lean, line 569. The attribute's comment: “three_descriptions”.

The projectivized associated graded ring at a node is the spectrum of its normalization fibre. The grading is the one by the powers of the maximal ideal.

public theorem proj_associatedGraded_iso_quadraticAlgebraSpec
    (hA : IsNodalAlgebra k A)
    (𝒢 : ℕ → AddSubgroup (AssociatedGraded.gradedRing (maximalIdeal A)))
    [GradedRing 𝒢]
    (h𝒢 : ∀ n, 𝒢 n = AddMonoidHom.range
      (DirectSum.of (fun i => AssociatedGraded.piece (M := A) (maximalIdeal A) i) n)) :
    Nonempty (Proj 𝒢 ≅ Spec (.of
      (quadraticAlgebra A)))

Tag 0CBU, a remark

Tag 0CBU in the Stacks Project.

Stacks.Curves.isSplitNode_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeQuadraticAlgebra/SplitNode.lean, line 517. The attribute's comment: “conditions (1)-(4); the completion condition (5) is not formalized”.

Let A be a nodal local algebra over a field k, with residue field κ, and let κ' = Stacks.Curves.quadraticAlgebra A be the associated separable κ-algebra of degree two. Then the following are equivalent: κ' is κ × κ; the nondegenerate quadratic form of Stacks Tag 0C49 can be chosen to be x y; A has two branches; the integral closure of A in its total ring of fractions has two maximal ideals.

public theorem isSplitNode_tfae
    (k : Type u) (A : Type v) [Field k] [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [Algebra k A] (hA : IsNodalAlgebra k A) :
    List.TFAE [
      Nonempty (quadraticAlgebra A ≃ₐ[ResidueField A] (ResidueField A × ResidueField A)),
      ∃ (x y : maximalIdeal A)
        (e : Module.Basis (BinaryIndex (ResidueField A)) (ResidueField A) (CotangentSpace A)),
        e ⟨0⟩ = (maximalIdeal A).toCotangent x ∧
          e ⟨1⟩ = (maximalIdeal A).toCotangent y ∧
          (x : A) * (y : A) ∈ (maximalIdeal A) ^ 3,
      numberOfBranchesOfLocalRing A = 2,
      Set.encard
        (Set.univ : Set (MaximalSpectrum ↥(integralClosure A (FractionRing A)))) = 2]

Stacks.Curves.nonempty_algEquiv_adicCompletion_quotient_X_mul_X_iff_numberOfBranches_eq_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeQuadraticAlgebra/SplitNodeCompletion.lean, line 283. The attribute's comment: “condition (5), the completion condition”.

The completion condition for a split node. Let A be a nodal local algebra over a field k, with residue field κ. Then the completion of A at its maximal ideal is κ[[x, y]]/(x y) as a k-algebra if and only if A has two branches — hence if and only if any one of the four conditions of Stacks.Curves.isSplitNode_tfae holds.

public theorem nonempty_algEquiv_adicCompletion_quotient_X_mul_X_iff_numberOfBranches_eq_two
    (k : Type u) (A : Type v) [Field k] [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [Algebra k A] (hA : IsNodalAlgebra k A) :
    Nonempty (AdicCompletion (maximalIdeal A) A ≃ₐ[k]
        (MvPowerSeries (Fin 2) (ResidueField A) ⧸
          Ideal.span {(MvPowerSeries.X 0 : MvPowerSeries (Fin 2) (ResidueField A)) *
                        MvPowerSeries.X 1})) ↔
      numberOfBranchesOfLocalRing A = 2

Tag 0CBV, a definition

Tag 0CBV in the Stacks Project.

Stacks.Curves.IsSplitNode, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/IsSplitNode.lean, line 41.

A point of a scheme over k is a split node if it is a node, the structure map k → κ(x) is bijective, and the quadratic algebra of 𝒪_{X, x} is the trivial quadratic extension κ(x) × κ(x).

def IsSplitNode (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))] (x : X) : Prop

Tag 0CBW, a lemma

Tag 0CBW in the Stacks Project.

Stacks.Curves.isSplitNode_tfae_normalizationFibre_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalSingularitiesCharacterization.lean, line 358.

Stacks 0CBW. Let k be a field, let X be a one-dimensional algebraic k-scheme and let x ∈ X be a closed point. The following are equivalent:

x is a split node;

x is a node and there are exactly two points x₁, x₂ of the normalization X^ν lying over x, with k = κ(x₁) = κ(x₂);

𝒪^∧_{X,x} ≅ k[[x, y]]/(x y) as a k-algebra.

Clause (4) of the source is the placeholder "add more here" and carries no mathematical content, so the equivalence stated here is that of clauses (1), (2) and (3).

The two points of clause (2) are the branches of 𝒪_{X,x}, counted by the fibre of the normalization (Stacks Tag 0C1S) and by the splitting of the quadratic algebra (Stacks Tag 0CBU); their residue fields are computed in Stacks.Curves.bijective_fieldToResidue_normalization_of_isNodalAlgebra.

public theorem isSplitNode_tfae_normalizationFibre_adicCompletion
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [LocallyOfFiniteType (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1) (x : X) (hx : IsClosed ({x} : Set X)) :
    letI : Algebra k (X.presheaf.stalk x) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop ≫
        X.presheaf.germ ⊤ x trivial).hom.toAlgebra
    let ν := normalizationOverField k (X ↘ Spec (.of k))
    let c₁ : Prop := IsSplitNode k X x
    let c₂ : Prop :=
      IsNode k X x ∧
        ∃ x₁ x₂ : normalizationSchemeOverField k (X ↘ Spec (.of k)),
          x₁ ≠ x₂ ∧
            {y : normalizationSchemeOverField k (X ↘ Spec (.of k)) | ν y = x} = {x₁, x₂} ∧
              Function.Bijective (fieldToResidue (ν ≫ (X ↘ Spec (.of k))) x₁).hom ∧
                Function.Bijective (fieldToResidue (ν ≫ (X ↘ Spec (.of k))) x₂).hom
    let c₃ : Prop :=
      Nonempty (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x) ≃ₐ[k]
        (MvPowerSeries (Fin 2) k ⧸
          Ideal.span {(MvPowerSeries.X 0 : MvPowerSeries (Fin 2) k) * MvPowerSeries.X 1}))
    List.TFAE [c₁, c₂, c₃]

Tag 0C56, a lemma

Tag 0C56 in the Stacks Project.

Stacks.Curves.isNode_iff_of_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeFieldExtension.lean, line 482.

Stacks Project, Tag 0C56. Let K / k be an extension of fields and let X be a one-dimensional scheme locally of finite type over k. A point of the base change X_K is a closed point and a node exactly when its image in X is.

Closedness of the point is part of Stacks.Curves.IsNode, so the two conditions of the source are carried by the node predicates themselves rather than stated separately.

theorem isNode_iff_of_fieldExtension
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ AlgebraicGeometry.Spec (.of k)) [LocallyOfFiniteType f]
    (hdim : topologicalKrullDim X = 1) (x : X)
    (y : (pullback f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K))) :
      Scheme.{u}))
    (hy : (pullback.fst f
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y = x) :
    letI : X.Over (AlgebraicGeometry.Spec (.of k)) := ⟨f⟩
    letI : (pullback f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K))) :
        Scheme.{u}).Over (AlgebraicGeometry.Spec (.of K)) :=
      ⟨pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K)))⟩
    (IsNode k X x ↔
      IsNode K (pullback f
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}) y)

Tag 0C57, a lemma

Tag 0C57 in the Stacks Project.

Stacks.Curves.isNode_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeEtaleLocal.lean, line 247.

Stacks Project, Tag 0C57. For an étale morphism g : Y ⟶ X of schemes over a field with X of dimension one and locally of finite type, a point of Y is a node exactly when its image in X is a node.

theorem isNode_iff_of_etale
    (k : Type u) [Field k]
    (X Y : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    (_hdim : topologicalKrullDim X = 1)
    (g : Y ⟶ X) [Etale g] (y : Y) :
    letI : X.Over (Spec (.of k)) := ⟨f⟩
    letI : Y.Over (Spec (.of k)) := ⟨g ≫ f⟩
    IsNode k X (g.base y) ↔ IsNode k Y y

Tag 0CD6, a lemma

Tag 0CD6 in the Stacks Project.

Stacks.Curves.isNode_iff_of_finiteSeparable_baseField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodeFieldExtension.lean, line 614. References: SGA 7 XV (1.2.5), “ordinary case”.

Stacks Project, Tag 0CD6. Let k' / k be a finite separable field extension and let X be a one-dimensional scheme locally of finite type over k'. A point of X is a node over k' exactly when it is a node for the k-scheme structure obtained by composing with Spec k' ⟶ Spec k.

The two conditions are joined through the base change X ×_{Spec k} Spec k'. Its first projection is étale, being a base change of the étale morphism Spec k' ⟶ Spec k, and the graph of f is a section of that projection, hence itself étale. Tag 0C56 identifies the node condition over k with the one on the base change, and Tag 0C57 identifies the latter with the node condition over k' on X.

theorem isNode_iff_of_finiteSeparable_baseField
    (k k' : Type u) [Field k] [Field k'] [Algebra k k'] [Module.Finite k k']
    [Algebra.IsSeparable k k']
    (X : Scheme.{u}) (f : X ⟶ AlgebraicGeometry.Spec (.of k'))
    [LocallyOfFiniteType f] (hdim : topologicalKrullDim X = 1) (x : X) :
    letI : X.Over (AlgebraicGeometry.Spec (.of k')) := ⟨f⟩
    letI : X.Over (AlgebraicGeometry.Spec (.of k)) :=
      ⟨f ≫ AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k k'))⟩
    (IsNode k' X x ↔ IsNode k X x)

Tag 0C4E, a lemma

Tag 0C4E in the Stacks Project.

Stacks.Curves.hasAtWorstNodalSingularities_iff_lci_and_unramified_relativeSingularIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalLciUnramifiedCriterion.lean, line 319.

Stacks Project, Tag 0C4E.

theorem hasAtWorstNodalSingularities_iff_lci_and_unramified_relativeSingularIdeal
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (hequi : Equidimensional X) (hdim : topologicalKrullDim X = 1) :
    HasAtWorstNodalSingularities k X ↔
      (IsLocalCompleteIntersectionOverField (X ↘ AlgebraicGeometry.Spec (.of k)) ∧
        Unramified ((relativeSingularIdeal
            (X ↘ AlgebraicGeometry.Spec (.of k))).subschemeι ≫
          (X ↘ AlgebraicGeometry.Spec (.of k))))

Stacks.Curves.smoothAt_or_isSeparable_and_depth_eq_one_and_fittingIdeal_eq_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalUnramifiedSingularSubscheme.lean, line 277. The attribute's comment: “the implication (2) ⟹ (1), via condition (5) of Tag 0C4D at every closed point”.

Condition (2) of Tag 0C4E gives condition (5) of Tag 0C4D at every closed point. Let k be a field and X a locally algebraic k-scheme, equidimensional of dimension one. Assume X is a local complete intersection over k and that the closed subscheme cut out by the first Fitting ideal of Ω_{X/k} is unramified over k. Then at a closed point x of X either the structure morphism is smooth, or the residue field extension at x is separable, 𝒪_{X,x} is one-dimensional of depth one, and the first Fitting ideal of Ω_{X/k} generates the maximal ideal of 𝒪_{X,x}.

The hypotheses are condition (2) of Tag 0C4E and the second disjunct is condition (5) of Tag 0C4D together with the dimension of the local ring. Separability is stated over the residue field of the image point of Spec k, the spelling of Tag 02G8.

The remaining step of the implication (2) ⟹ (1) of Tag 0C4E — that condition (5) of Tag 0C4D makes such a point a node — is not delivered here, but it is available in the library: Stacks.Curves.isNode_tfae_of_isClosed (StacksFrontier/AlgebraicGeometry/Curves/NodeFittingIdealClosedPoint.lean) carries a bare @[stacks 0C4D], i.e. the whole six-clause equivalence at a closed point of a one-dimensional scheme locally of finite type over an arbitrary field, and the separability this theorem supplies in its second disjunct is exactly what lets its cycle 1 → 2 → 3 → 4 → 5 → 6 → 1 be run, so (... ).out 5 1 supplies the step. (5) ⟹ (1) over an arbitrary base field is therefore in hand, and the two are composed in Stacks.NodalEtaleLocalStructure.isNode_asFiber_of_mem_relativeSingular (StacksFrontier/AlgebraicGeometry/Curves/NodalEtaleLocalStructureAssembly.lean), which is what Tag 0CBY's existence statement rests on.

The step does not depend on the unproved h₁₄/h₄₅ of Stacks.Curves.isNode_tfae_of_residual_equivalences; that route is only one of several, and Tag 0CBY is an assembly of proved results. Alternatives, if the closed-point hypothesis of isNode_tfae_of_isClosed is inconvenient: Stacks.Curves.isNode_of_isNodalAlgebra_stalk (StacksFrontier/AlgebraicGeometry/Curves/NodeNodalAlgebraAscent.lean, @[stacks 0C4D "clause (2) implies clause (1), over an arbitrary base field"]) and Stacks.Curves.isNode\_iff\_isNodalAlgebra\_stalk (StacksFrontier/AlgebraicGeometry/Curves/NodeResidueFieldSeparable.lean).

theorem smoothAt_or_isSeparable_and_depth_eq_one_and_fittingIdeal_eq_maximalIdeal
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ AlgebraicGeometry.Spec (.of k))
    [LocallyOfFiniteType f] (hequi : Equidimensional X) (hdim : topologicalKrullDim X = 1)
    (hlci : IsLocalCompleteIntersectionOverField f)
    (hZ : Unramified ((relativeSingularIdeal f).subschemeι ≫ f))
    (x : X) (hx : IsClosed ({x} : Set X)) :
    letI : Algebra ((AlgebraicGeometry.Spec (.of k)).residueField (f.base x))
        (X.residueField x) := (f.residueFieldMap x).hom.toAlgebra
    (InfinitesimalLifting.SmoothAt f x ∨
      (Algebra.IsSeparable ((AlgebraicGeometry.Spec (.of k)).residueField (f.base x))
          (X.residueField x) ∧
        ringKrullDim (X.presheaf.stalk x) = 1 ∧
          Module.depth (X.presheaf.stalk x) (maximalIdeal (X.presheaf.stalk x))
              (X.presheaf.stalk x) = 1 ∧
            IdealSheafData.stalk (relativeSingularIdeal f) x =
              maximalIdeal (X.presheaf.stalk x)))

Tag 0E37, a lemma

Tag 0E37 in the Stacks Project.

Stacks.Curves.isGorenstein_of_hasAtWorstNodalSingularities, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalGorensteinReduced.lean, line 297. The attribute's comment: “nodal_curve_gorenstein”.

Stacks Project, Tag 0E37. A locally algebraic scheme over a field, equidimensional of dimension one and with at-worst-nodal singularities, is Gorenstein.

theorem isGorenstein_of_hasAtWorstNodalSingularities (k : Type u) [Field k] (X : Scheme.{u})
    [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (_hequidim : TopologicalSpace.Equidimensional X) (hdim : topologicalKrullDim X = 1)
    (hnodal : HasAtWorstNodalSingularities k X) :
    AlgebraicGeometry.IsGorenstein X

Stacks.Curves.geometricallyReduced_of_hasAtWorstNodalSingularities, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalGorensteinReduced.lean, line 316. The attribute's comment: “nodal_curve_geometrically_reduced”.

Stacks Project, Tag 0E37. A locally algebraic scheme over a field, equidimensional of dimension one and with at-worst-nodal singularities, is geometrically reduced.

theorem geometricallyReduced_of_hasAtWorstNodalSingularities (k : Type u) [Field k]
    (X : Scheme.{u}) [X.Over (AlgebraicGeometry.Spec (.of k))]
    [LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (.of k))]
    (_hequidim : TopologicalSpace.Equidimensional X) (hdim : topologicalKrullDim X = 1)
    (hnodal : HasAtWorstNodalSingularities k X) :
    GeometricallyReduced (X ↘ AlgebraicGeometry.Spec (.of k))

Tag 0E38, a lemma

Tag 0E38 in the Stacks Project.

Stacks.Curves.exists_iso_sigma_spec_intersectionWithComplementaryCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ComplementaryCurve/IntersectionComponentStalks.lean, line 399. The attribute's comment: “intersection_is_disjoint_union_of_spectra_of_finite_separable_extensions”.

Stacks Project, Tag 0E38, clause (2)(a). Let X be a one-dimensional equidimensional curve locally of finite type over a field k with at worst nodal singularities, let Y ⊆ X be a reduced equidimensional closed subscheme of dimension one, and let Z be the scheme-theoretic closure of X ∖ Y. Then the scheme-theoretic intersection Y ∩ Z is, over k, a disjoint union of spectra of finite separable extensions of k.

At each point of Y ∩ Z the stalks of the ideal sheaves of Y and Z are the two minimal primes of the local ring of the node there (Stacks.Curves.exists_stalk_eq_of_mem_support_of_mem_support_complementaryCurveIdeal), and these sum to the maximal ideal, the delta invariant being one (Ring.sup_eq_maximalIdeal_of_deltaInvariant_eq_one). So every local ring of Y ∩ Z is a field: Y ∩ Z is reduced, and its points are closed, so it is discrete. Each Spec κ(w) ⟶ Y ∩ Z is then an open and closed immersion, and together they present Y ∩ Z as the coproduct of the spectra of its residue fields, which are finite (closed points) and separable (nodes) over k.

theorem exists_iso_sigma_spec_intersectionWithComplementaryCurve
    {k : Type u} [Field k] {X : Scheme.{u}} [X.Over (Spec (.of k))]
    [LocallyOfFiniteType (X ↘ Spec (.of k))]
    (hX_equidimensional : Equidimensional X)
    (hX_dimension : topologicalKrullDim X = 1)
    (hX_nodal : HasAtWorstNodalSingularities k X)
    (I : X.IdealSheafData) [IsReduced I.subscheme]
    (hY_equidimensional : Equidimensional I.subscheme)
    (hY_dimension : topologicalKrullDim I.subscheme = 1) :
    ∃ (ι : Type u) (K : ι → Type u) (_ : ∀ i, Field (K i)) (_ : ∀ i, Algebra k (K i)),
      (∀ i, Module.Finite k (K i) ∧ Algebra.IsSeparable k (K i)) ∧
      ∃ e : (∐ fun i => Spec (.of (K i))) ≅ intersectionWithComplementaryCurve I,
        ∀ i, Limits.Sigma.ι (fun i => Spec (.of (K i))) i ≫ e.hom ≫
            (intersectionWithComplementaryCurveIdeal I).subschemeι ≫ (X ↘ Spec (.of k)) =
          Spec.map (CommRingCat.ofHom (algebraMap k (K i)))

Stacks.Curves.isFiniteSeparable_residueField_of_mem_intersection_complementaryCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ComplementaryCurve/IntersectionLocalStructure.lean, line 225. The attribute's comment: “part (2)(a), the residue fields of the intersection are finite separable over k”.

Stacks 0E38, part (2)(a): the residue field at a point where a reduced closed subcurve meets the closure of its complement is a finite separable extension of the base field. Such a point is a node of X by part (2)(b), and the residue field extension at a node is separable (Tag 0C4D) and finite because the point is closed and X is locally of finite type over k.

theorem isFiniteSeparable_residueField_of_mem_intersection_complementaryCurve
    {k : Type u} [Field k] {X : Scheme.{u}} [X.Over (Spec (.of k))]
    [LocallyOfFiniteType (X ↘ Spec (.of k))]
    (hX_equidimensional : Equidimensional X)
    (hX_dimension : topologicalKrullDim X = 1)
    (hX_nodal : HasAtWorstNodalSingularities k X)
    (I : X.IdealSheafData) [IsReduced I.subscheme]
    (hY_equidimensional : Equidimensional I.subscheme)
    (hY_dimension : topologicalKrullDim I.subscheme = 1)
    {x : X} (hxI : x ∈ (I.support : Set X))
    (hxJ : x ∈ ((complementaryCurveIdeal I).support : Set X)) :
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop ≫
        X.presheaf.germ ⊤ x (by simp)).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
    Module.Finite k (X.residueField x) ∧ Algebra.IsSeparableExtension k (X.residueField x)

Stacks.Curves.smoothAt_of_mem_support_complementaryCurveIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ComplementaryCurve/IntersectionLocalStructure.lean, line 303. The attribute's comment: “part (2)(c)”.

Stacks 0E38, part (2)(c): a reduced closed subcurve of a one-dimensional equidimensional at-worst-nodal curve is smooth over the base field at every point where it meets the closure of its complement. At such a point the local ring of X is reduced with delta invariant one and exactly two minimal primes, and the stalk of the ideal sheaf of the subcurve is one of them; the quotient of such a local ring by a minimal prime is a discrete valuation ring, hence a regular local ring, and over a field regularity with separable residue field is smoothness.

theorem smoothAt_of_mem_support_complementaryCurveIdeal
    {k : Type u} [Field k] {X : Scheme.{u}} [X.Over (Spec (.of k))]
    [LocallyOfFiniteType (X ↘ Spec (.of k))]
    (hX_equidimensional : Equidimensional X)
    (hX_dimension : topologicalKrullDim X = 1)
    (hX_nodal : HasAtWorstNodalSingularities k X)
    (I : X.IdealSheafData) [IsReduced I.subscheme]
    (hY_equidimensional : Equidimensional I.subscheme)
    (hY_dimension : topologicalKrullDim I.subscheme = 1)
    (y : I.subscheme)
    (hy : I.subschemeι.base y ∈ ((complementaryCurveIdeal I).support : Set X)) :
    InfinitesimalLifting.SmoothAt (I.subschemeι ≫ (X ↘ Spec (.of k))) y

Stacks.Curves.isDiscrete_and_residueField_intersectionWithComplementaryCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ComplementaryCurve/IntersectionLocalStructure.lean, line 466. The attribute's comment: “part (2)(a)”.

Stacks 0E38, part (2)(a): the scheme-theoretic intersection of a reduced closed subcurve with the closure of its complement is the disjoint union of the spectra of finite separable extensions of the base field. Its underlying space is discrete, so it is the disjoint union of its points; at each point the stalk of the ideal sheaf cutting it out is the maximal ideal of the local ring of X, so the local ring there is the residue field κ(x); and that residue field is a finite separable extension of k.

theorem isDiscrete_and_residueField_intersectionWithComplementaryCurve
    {k : Type u} [Field k] {X : Scheme.{u}} [X.Over (Spec (.of k))]
    [LocallyOfFiniteType (X ↘ Spec (.of k))]
    (hX_equidimensional : Equidimensional X)
    (hX_dimension : topologicalKrullDim X = 1)
    (hX_nodal : HasAtWorstNodalSingularities k X)
    (I : X.IdealSheafData) [IsReduced I.subscheme]
    (hY_equidimensional : Equidimensional I.subscheme)
    (hY_dimension : topologicalKrullDim I.subscheme = 1) :
    DiscreteTopology ((intersectionWithComplementaryCurveIdeal I).subscheme : Type u) ∧
      ∀ w : (intersectionWithComplementaryCurveIdeal I).subscheme,
        let x := (intersectionWithComplementaryCurveIdeal I).subschemeι.base w
        let kToStalk : k →+* X.presheaf.stalk x :=
          ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop ≫
            X.presheaf.germ ⊤ x (by simp)).hom
        letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
        letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
        IdealSheafData.stalk (intersectionWithComplementaryCurveIdeal I) x =
            IsLocalRing.maximalIdeal (X.presheaf.stalk x) ∧
          Module.Finite k (X.residueField x) ∧
            Algebra.IsSeparableExtension k (X.residueField x)

Stacks.Curves.hasAtWorstNodalSingularities_subscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ComplementaryCurve/IntersectionLocalStructure.lean, line 556. The attribute's comment: “part (1)”.

Stacks 0E38, part (1): a reduced closed subscheme, equidimensional of dimension one, of a one-dimensional equidimensional locally algebraic curve with at-worst-nodal singularities again has at-worst-nodal singularities. At a point where the subcurve meets the closure of its complement it is in fact smooth over the base field, by part (2)(c). At any other point the subcurve agrees with the ambient curve on an open neighbourhood, and the dichotomy "smooth over k or a node" transports along the two étale morphisms from that open subscheme.

theorem hasAtWorstNodalSingularities_subscheme
    {k : Type u} [Field k] {X : Scheme.{u}} [X.Over (Spec (.of k))]
    [LocallyOfFiniteType (X ↘ Spec (.of k))]
    (hX_equidimensional : Equidimensional X)
    (hX_dimension : topologicalKrullDim X = 1)
    (hX_nodal : HasAtWorstNodalSingularities k X)
    (I : X.IdealSheafData) [IsReduced I.subscheme]
    (hY_equidimensional : Equidimensional I.subscheme)
    (hY_dimension : topologicalKrullDim I.subscheme = 1) :
    letI : I.subscheme.Over (Spec (.of k)) := ⟨I.subschemeι ≫ (X ↘ Spec (.of k))⟩
    HasAtWorstNodalSingularities k I.subscheme

Stacks.Curves.isNode_of_mem_intersection_complementaryCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ComplementaryCurve/IntersectionNodes.lean, line 231. The attribute's comment: “intersection_points_are_nodes”.

Stacks Project, Tag 0E38. Every point where a reduced equidimensional closed subcurve meets the scheme-theoretic closure of its complement, in a one-dimensional equidimensional curve over a field with at worst nodal singularities, is a node of the ambient curve.

theorem isNode_of_mem_intersection_complementaryCurve
    {k : Type u} [Field k] {X : Scheme.{u}} [X.Over (Spec (.of k))]
    [LocallyOfFiniteType (X ↘ Spec (.of k))]
    (hX_equidimensional : Equidimensional X)
    (hX_dimension : topologicalKrullDim X = 1)
    (hX_nodal : HasAtWorstNodalSingularities k X)
    (I : X.IdealSheafData) [IsReduced I.subscheme]
    (hY_equidimensional : Equidimensional I.subscheme)
    (hY_dimension : topologicalKrullDim I.subscheme = 1) :
    let U : X.Opens := ⟨I.supportᶜ, I.support.isClosed.isOpen_compl⟩
    ∀ y : (I ⊔ U.ι.ker).subscheme, IsNode k X ((I ⊔ U.ι.ker).subschemeι.base y)

Sources

LeanStacks.Curves.IsNode · Stacks.Curves.HasAtWorstNodalSingularities · IsRegularLocalRing.eq_bot_or_eq_maximalIdeal_or_eq_span_singleton_of_quotient_isReduced · IsRegularLocalRing.exists_ne_zero_mem_maximalIdeal_and_eq_span_singleton_of_quotient_depth_eq_one · Stacks.Curves.isNodalAlgebra_tfae · Stacks.Curves.encard_maximalSpectrum_integralClosure_fractionRing_eq_one_or_two · Stacks.Curves.isNodalAlgebra_iff_deltaInvariant_eq_one_and_two_geometricBranches · Stacks.Curves.isSeparableExtension_residueField_integralClosure_fractionRing

Section53.20 Families of nodal curves #

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

Tag 0C59, a lemma

Tag 0C59 in the Stacks Project.

Stacks.Curves.hasAtWorstNodalFibresOfDimensionOne_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalFamilyCriterion.lean, line 348. The attribute's comment: “condition (1) is Stacks.Curves.HasAtWorstNodalFibresOfDimensionOne and condition (2) is AlgebraicGeometry.IsAtWorstNodalOfRelativeDimensionOne”.

Stacks Project, Tag 0C59. A morphism of schemes is flat, locally of finite presentation with every nonempty fibre equidimensional of dimension one and with at-worst-nodal singularities exactly when it is syntomic of relative dimension one and the closed subscheme cut out by the first Fitting ideal of its relative differentials is unramified over the base.

Everything except the nodal condition on the fibres is AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_iff_fibres, which reads that condition as condition (2) of Tag 0C4E; Tag 0C4E (Stacks.Curves.hasAtWorstNodalSingularities_iff_lci_and_unramified_relativeSingularIdeal) applied to a fibre trades the two. Its hypotheses on the fibre are the equidimensionality and the dimension, which both sides of the equivalence provide for a nonempty fibre, and local finite type of the fibre's structure morphism, which follows from local finite presentation of f; over an empty fibre condition (2) holds vacuously.

theorem hasAtWorstNodalFibresOfDimensionOne_iff {X S : Scheme.{u}} (f : X ⟶ S) :
    HasAtWorstNodalFibresOfDimensionOne f ↔ IsAtWorstNodalOfRelativeDimensionOne f

Tag 0C5A, a definition

Tag 0C5A in the Stacks Project.

AlgebraicGeometry.IsAtWorstNodalOfRelativeDimensionOne, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/F6Rank136/AtWorstNodalRelativeDimensionOne.lean, line 48.

A morphism is at-worst-nodal of relative dimension one if it is syntomic of relative dimension one and its relative singular subscheme is unramified over the base.

public abbrev IsAtWorstNodalOfRelativeDimensionOne {X S : Scheme.{u}} (f : X ⟶ S) : Prop

Tag 0CD7, a lemma

Tag 0CD7 in the Stacks Project.

AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_of_smoothOfRelativeDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/F6Rank136/SmoothIsNodal.lean, line 108.

Stacks Project, Tag 0CD7. A morphism of schemes smooth of relative dimension one is at-worst-nodal of relative dimension one: it is syntomic with one-dimensional fibres, and its relative singular subscheme is empty, hence unramified over the base.

public theorem isAtWorstNodalOfRelativeDimensionOne_of_smoothOfRelativeDimension
    {X S : Scheme.{u}} (f : X ⟶ S) [SmoothOfRelativeDimension 1 f] :
    IsAtWorstNodalOfRelativeDimensionOne f

Tag 0C5B, a lemma

Tag 0C5B in the Stacks Project.

AlgebraicGeometry.IsAtWorstNodalOfRelativeDimensionOne.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalFamilyBaseChange.lean, line 74.

Let f : X ⟶ S be at-worst-nodal of relative dimension one. Then so is any base change f' : X' ⟶ S' of f, presented by an arbitrary cartesian square.

public theorem IsAtWorstNodalOfRelativeDimensionOne.of_isPullback {X' X S' S : Scheme.{u}}
    {g' : X' ⟶ X} {f' : X' ⟶ S'} {f : X ⟶ S} {g : S' ⟶ S} (h : IsPullback g' f' f g)
    (hf : IsAtWorstNodalOfRelativeDimensionOne f) :
    IsAtWorstNodalOfRelativeDimensionOne f'

AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalLocality.lean, line 101.

Stacks 0C5B. A base change of a morphism which is at-worst-nodal of relative dimension one is again at-worst-nodal of relative dimension one.

public instance isAtWorstNodalOfRelativeDimensionOne_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (@IsAtWorstNodalOfRelativeDimensionOne.{u} : MorphismProperty Scheme.{u})

Tag 0DSC, a lemma

Tag 0DSC in the Stacks Project.

AlgebraicGeometry.nodalLocus_isGreatest, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalLocus.lean, line 433. The attribute's comment: “the maximal open subscheme”.

Stacks Project, Tag 0DSC. For a morphism of schemes which is flat and locally of finite presentation there is a maximal open subscheme of its source on which it is at-worst-nodal of relative dimension one: the restriction of the morphism to nodalLocus f is at-worst-nodal of relative dimension one, and every open subscheme with that property is contained in nodalLocus f.

theorem nodalLocus_isGreatest {X S : Scheme.{u}} (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] :
    IsGreatest {U : X.Opens | IsAtWorstNodalOfRelativeDimensionOne (U.ι ≫ f)} (nodalLocus f)

AlgebraicGeometry.nodalLocus_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalLocus.lean, line 443. The attribute's comment: “compatibility with base change”.

Stacks Project, Tag 0DSC. Formation of the maximal at-worst-nodal open subscheme commutes with arbitrary base change: in a cartesian square with right edge a flat morphism f locally of finite presentation and base edge g, the nodal locus of the base change f' of f is the inverse image of the nodal locus of f.

theorem nodalLocus_baseChange {X' X S' S : Scheme.{u}} (g' : X' ⟶ X) (f' : X' ⟶ S') (f : X ⟶ S)
    (g : S' ⟶ S) (sq : IsPullback g' f' f g) [Flat f] [LocallyOfFinitePresentation f] :
    nodalLocus f' = g' ⁻¹ᵁ nodalLocus f

Tag 0C5C, a lemma

Tag 0C5C in the Stacks Project.

AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_comp_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalEtaleComposition.lean, line 152.

Stacks Project, Tag 0C5C. Precomposing an at-worst-nodal morphism of relative dimension one with an étale morphism again gives an at-worst-nodal morphism of relative dimension one.

public theorem isAtWorstNodalOfRelativeDimensionOne_comp_etale {X Y S : Scheme.{u}}
    (f : X ⟶ S) (g : Y ⟶ X) [Etale g] (hf : IsAtWorstNodalOfRelativeDimensionOne f) :
    IsAtWorstNodalOfRelativeDimensionOne (g ≫ f)

Tag 0CD8, a lemma

Tag 0CD8 in the Stacks Project.

AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_comp_etale_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalLocality.lean, line 193.

Stacks 0CD8. Composing a morphism which is at-worst-nodal of relative dimension one with an étale morphism of the base again gives a morphism which is at-worst-nodal of relative dimension one.

public theorem isAtWorstNodalOfRelativeDimensionOne_comp_etale_base {X S' S : Scheme.{u}}
    (f : X ⟶ S') (g : S' ⟶ S) [Etale g] (hf : IsAtWorstNodalOfRelativeDimensionOne f) :
    IsAtWorstNodalOfRelativeDimensionOne (f ≫ g)

Tag 0C5D, a lemma

Tag 0C5D in the Stacks Project.

AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_iff_of_etaleCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalEtaleLocalOnSource.lean, line 188.

Stacks Project, Tag 0C5D. Let f : X ⟶ S be a morphism of schemes and let {U i ⟶ X} be an étale covering. The following are equivalent:

f is at-worst-nodal of relative dimension one;

each U i ⟶ S is at-worst-nodal of relative dimension one.

In other words, being at-worst-nodal of relative dimension one is étale local on the source.

public theorem isAtWorstNodalOfRelativeDimensionOne_iff_of_etaleCovering {X S : Scheme.{u}}
    (f : X ⟶ S) {ι : Type*} {U : ι → Scheme.{u}} (g : ∀ i, U i ⟶ X)
    (hg : Presieve.ofArrows U g ∈ Scheme.etalePrecoverage X) :
    IsAtWorstNodalOfRelativeDimensionOne f ↔
      ∀ i, IsAtWorstNodalOfRelativeDimensionOne (g i ≫ f)

AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_isLocalAtSource_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalLocality.lean, line 287.

Stacks 0C5D. Being at-worst-nodal of relative dimension one is étale local on the source: a morphism has the property exactly when all of its restrictions to the members of an étale covering of its source do.

public instance isAtWorstNodalOfRelativeDimensionOne_isLocalAtSource_etale :
    MorphismProperty.IsLocalAtSource
      (@IsAtWorstNodalOfRelativeDimensionOne.{u} : MorphismProperty Scheme.{u})
      Scheme.etalePrecoverage

Tag 0C5E, a lemma

Tag 0C5E in the Stacks Project.

AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalLocality.lean, line 118.

Stacks 0C5E. Being at-worst-nodal of relative dimension one is fpqc local on the target: a morphism has the property exactly when all of its base changes along the members of an fpqc covering of its target do.

public instance isAtWorstNodalOfRelativeDimensionOne_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (@IsAtWorstNodalOfRelativeDimensionOne.{u} : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 0C5F, a lemma

Tag 0C5F in the Stacks Project.

AlgebraicGeometry.exists_isAtWorstNodalOfRelativeDimensionOne_baseChange_of_limitBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/F6Rank136/AtWorstNodalDescentAlongLimit.lean, line 291.

Stacks Project, Tag 0C5F. Let a scheme be the limit of a cofiltered inverse system of schemes with affine transition morphisms, and let f₀ : X₀ ⟶ Y₀ be a morphism locally of finite presentation over a stage, with that stage and both of X₀, Y₀ quasi-compact and quasi-separated. If the base change of f₀ to the limit is at-worst-nodal of relative dimension one, then its base change to some later stage is at-worst-nodal of relative dimension one.

public theorem exists_isAtWorstNodalOfRelativeDimensionOne_baseChange_of_limitBaseChange
    {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D) (i₀ : I)
    (X₀ Y₀ : Over (D.obj i₀)) (f₀ : X₀ ⟶ Y₀) [IsCofiltered I]
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (D.map g)]
    [CompactSpace (D.obj i₀)] [QuasiSeparatedSpace (D.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    (hf₀ : LocallyOfFinitePresentation f₀.left) (hc : IsLimit c)
    (hf : IsAtWorstNodalOfRelativeDimensionOne
      ((Over.pullback (c.π.app i₀)).map f₀).left) :
    ∃ (i : I) (g : i ⟶ i₀), IsAtWorstNodalOfRelativeDimensionOne
      ((Over.pullback (D.map g)).map f₀).left

Tag 0CBX, a lemma

Tag 0CBX in the Stacks Project.

Stacks.Curves.exists_algEquiv_adicCompletion_quotient_mvPowerSeries_of_isSplitNode, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalFamilyCompletedLocalRing.lean, line 2062.

The completion at a split node of a flat, locally finite-type family over a Noetherian local base is a nodal smoothing A⟦x,y⟧/(xy-h) over the completed base ring A.

theorem exists_algEquiv_adicCompletion_quotient_mvPowerSeries_of_isSplitNode
    {T S : Scheme.{u}} (f : T ⟶ S) (t : T)
    (hflat : AlgebraicGeometry.IsFlatAt f.toLRSHom.toShHom t)
    [IsNoetherianRing (S.presheaf.stalk (f t))]
    [LocallyOfFiniteType f]
    (hnode : letI := f.fiberOverSpecResidueField (f t)
      IsSplitNode (S.residueField (f t)) (f.fiber (f t)) (f.asFiber t)) :
    let R := S.presheaf.stalk (f t)
    let Q := T.presheaf.stalk t
    let A := AdicCompletion (maximalIdeal R) R
    let B := AdicCompletion (maximalIdeal Q) Q
    let φ : A →+* B := adicCompletionMap (f.stalkMap t).hom
      (maximalIdeal R) (maximalIdeal Q)
      (map_maximalIdeal_le (f.stalkMap t).hom)
    letI : Algebra A B := φ.toAlgebra
    ∃ h : A, h ∈ maximalIdeal A ∧
      Nonempty ((MvPowerSeries (Fin 2) A ⧸
        Ideal.span {MvPowerSeries.X 0 * MvPowerSeries.X 1 - MvPowerSeries.C h}) ≃ₐ[A] B)

Tag 0GKA, a lemma

Tag 0GKA in the Stacks Project.

Stacks.AlgebraicGeometry.NodalFamilyCohomology.isIso_c_and_isIso_c_of_isPullback_of_isAtWorstNodal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalFamilyStructureSheafCohomology.lean, line 266. The attribute's comment: “(a): f_*𝒪_X = 𝒪_S, as invertibility of f.c, and the same for every base change, stated for every cartesian square over S”.

[Stacks, Tag 0GKA], part (a). Let f : X ⟶ S be proper and at-worst-nodal of relative dimension one, with geometrically connected fibres. Then f_*𝒪_X = 𝒪_S, i.e. the comparison f.c : 𝒪_S ⟶ f_*𝒪_X is invertible, and this holds after any base change: for every cartesian square X' ⟶ X, f' : X' ⟶ S', S' ⟶ S, the comparison f'.c is invertible.

This is [Stacks, Tag 0E0L]: f is flat and locally of finite presentation, being syntomic, and geometrically reduced by geometricallyReduced_of_isAtWorstNodal.

theorem isIso_c_and_isIso_c_of_isPullback_of_isAtWorstNodal (f : X ⟶ S) [IsProper f]
    [GeometricallyConnected f] (hf : IsAtWorstNodalOfRelativeDimensionOne f) :
    IsIso f.c ∧ ∀ {X' S' : Scheme.{u}} {g : S' ⟶ S} {g' : X' ⟶ X} {f' : X' ⟶ S'},
      IsPullback g' f' f g → IsIso f'.c

Stacks.AlgebraicGeometry.NodalFamilyCohomology.isFiniteLocallyFree_rightDerived_one_and_isIso_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalFamilyStructureSheafCohomology.lean, line 319. The attribute's comment: “(b): R¹f_*𝒪_X is finite locally free, and its formation commutes with any base change, read over every quasi-compact quasi-separated open of the base, where the base-change map of Tag 0EX3 is defined”.

[Stacks, Tag 0GKA], part (b). Let f : X ⟶ S be proper and at-worst-nodal of relative dimension one, with geometrically connected fibres. Then R¹f_*𝒪_X is a finite locally free 𝒪_S-module, and its formation commutes with any base change: over every quasi-compact and quasi-separated open V ⊆ S (for instance every affine open, or S itself when S is quasi-compact and quasi-separated), for every cartesian square X'' ⟶ f⁻¹(V), X'' ⟶ Y'', Y'' ⟶ V, the canonical map h^* R¹(f ∣_ V)_*𝒪 ⟶ R¹f''_* (h')^*𝒪 of [Stacks, Tag 0EX3] is an isomorphism.

The base-change map of this library, Stacks.AlgebraicGeometry.TopDegreeBaseChange.topDirectImageBaseChangeMap, is defined over a quasi-compact quasi-separated base; commutation with base change is local on the base, so asking it over every such open of S is the source's assertion.

theorem isFiniteLocallyFree_rightDerived_one_and_isIso_baseChange (f : X ⟶ S) [IsProper f]
    [GeometricallyConnected f] (hf : IsAtWorstNodalOfRelativeDimensionOne f) :
    SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (((Scheme.Modules.pushforward f).rightDerived 1).obj
          (SheafOfModules.unit X.ringCatSheaf)) ∧
      ∀ (V : S.Opens) [CompactSpace V] [QuasiSeparatedSpace V] {X'' Y'' : Scheme.{u}}
        (h' : X'' ⟶ f ⁻¹ᵁ V) (f'' : X'' ⟶ Y'') (h : Y'' ⟶ V)
        (sq : IsPullback h' f'' (f ∣_ V) h),
        IsIso (@Stacks.AlgebraicGeometry.TopDegreeBaseChange.topDirectImageBaseChangeMap _ _
          (topDegreeSituation f hf V) (SheafOfModules.unit (f ⁻¹ᵁ V).toScheme.ringCatSheaf)
          (Stacks.AlgebraicGeometry.AffineQcohPushforward.isQuasicoherent_unit _) h' f'' h
          (Stacks.AlgebraicGeometry.TopDegreeBaseChange.toShHom_comm_of_isPullback
            (S := topDegreeSituation f hf V) h' f'' h sq))

Stacks.AlgebraicGeometry.NodalFamilyCohomology.isZero_rightDerived_of_two_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalFamilyStructureSheafCohomology.lean, line 342. The attribute's comment: “(c): Rᵠf_*𝒪_X = 0 for q ≥ 2”.

[Stacks, Tag 0GKA], part (c). Let f : X ⟶ S be proper and at-worst-nodal of relative dimension one, with geometrically connected fibres. Then Rᵠf_*𝒪_X = 0 for every q ≥ 2.

The fibres have dimension one, so this is [Stacks, Tag 0E7D] at d = 1.

theorem isZero_rightDerived_of_two_le (f : X ⟶ S) [IsProper f] [GeometricallyConnected f]
    (hf : IsAtWorstNodalOfRelativeDimensionOne f) (q : ℕ) (hq : 2 ≤ q) :
    IsZero (((Scheme.Modules.pushforward f).rightDerived q).obj
      (SheafOfModules.unit X.ringCatSheaf))

Sources

LeanStacks.Curves.hasAtWorstNodalFibresOfDimensionOne_iff · AlgebraicGeometry.IsAtWorstNodalOfRelativeDimensionOne · AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_of_smoothOfRelativeDimension · AlgebraicGeometry.IsAtWorstNodalOfRelativeDimensionOne.of_isPullback · AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_isStableUnderBaseChange · AlgebraicGeometry.nodalLocus_isGreatest · AlgebraicGeometry.nodalLocus_baseChange · AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_comp_etale

Section53.21 Étale local structure of nodal families #

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

Tag 0CBY, a lemma

Tag 0CBY in the Stacks Project.

Stacks.NodalEtaleLocalStructure.nonempty_standardNodalDiagram_of_isAtWorstNodal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/NodalEtaleLocalStructureAssembly.lean, line 348. The attribute's comment: “the whole statement. The diagram is the structure Stacks.NodalEtaleLocalStructure.StandardNodalDiagram, whose fields are the tag's four morphisms with the three etaleness assertions, the commutativity of the left and the middle square, the cartesianness of the right-hand square over the standard nodal family Spec Z[u,v,a]/(uv-a) -> Spec Z[a], and the point of U over x. The singular point of the fibre is spelled as the failure of smoothness of the fibre X_s over kappa(s) at x; the equivalent spelling as a point of the relative singular subscheme Sing(f), which is the one the source's own first step carries, is nonempty_standardNodalDiagram_of_mem_relativeSingular, and the two agree by mem_relativeSingular_iff_not_smoothAt_fiber ([Stacks, Tags 0C3I and 0C3K])”.

Stacks Project, Tag 0CBY. Let f : X ⟶ S be at-worst-nodal of relative dimension one and let x be a point of X at which the fibre X_s through it is singular. Then there is a commutative diagram
X ←—— U ——→ W ——→ Spec ℤ[u, v, a]/(uv - a)
↓     ↓     ↓                ↓
S ←———————— V ——————————→ Spec ℤ[a]
in which U ⟶ X, V ⟶ S and U ⟶ W are étale, the right-hand square is cartesian, and some point of U maps to x. The diagram is packaged as Stacks.NodalEtaleLocalStructure.StandardNodalDiagram.

The whole content is nonempty_standardNodalDiagram_of_mem_relativeSingular, which is the same statement with the singular point read on the relative singular subscheme Sing(f); the two spellings agree by mem_relativeSingular_iff_not_smoothAt_fiber, which is [Stacks, Tag 0C3K] on a fibre.

public theorem nonempty_standardNodalDiagram_of_isAtWorstNodal {X S : Scheme.{u}} (f : X ⟶ S)
    (hf : IsAtWorstNodalOfRelativeDimensionOne f) {x : X}
    (hxsing : ¬ InfinitesimalLifting.SmoothAt (f.fiberToSpecResidueField (f x))
      (f.asFiber x)) :
    Nonempty (StandardNodalDiagram f x)

Sources

LeanStacks.NodalEtaleLocalStructure.nonempty_standardNodalDiagram_of_isAtWorstNodal

Section53.22 More vanishing results #

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

Tag 0E3A, a lemma

Tag 0E3A in the Stacks Project.

AlgebraicGeometry.CohenMacaulayCurveSituation.invertibleCurveDegree_le_and_lt_or_nonempty_iso_of_not_isZero_cohomology_idealTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/IdealTwistVanishing.lean, line 441.

Stacks Project, Tag 0E3A. In Situation [Stacks, Tag 0B5D] assume X is integral of genus g. Let ℒ be an invertible 𝒪_X-module and let Z ⊆ X be a closed subscheme of dimension at most zero with ideal sheaf ℐ. If H^1(X, ℐℒ) ≠ 0, then

deg(ℒ) ≤ 2g - 2 + deg(Z),

with strict inequality unless ℐℒ ≅ ω_X. Here ℐℒ is ℒ ⊗ ℐ, deg(Z) = dim_k Γ(Z, 𝒪_Z) and ω_X is the dualizing sheaf of [Stacks, Tag 0BS2].

theorem invertibleCurveDegree_le_and_lt_or_nonempty_iso_of_not_isZero_cohomology_idealTwist
    [IsIntegral S.X] (L : S.X.Modules)
    [SheafOfModules.IsInvertible S.X.presheaf S.X.ringCatSheaf.2 L]
    (Z : S.X.IdealSheafData) (hZ : topologicalKrullDim Z.subscheme ≤ 0)
    (h : ¬ IsZero (cohomologyOverField S.k S.f (S.idealTwist Z L) 1)) :
    invertibleCurveDegree S.k S.f (le_of_eq S.dimension_one) L ≤
        2 * (genus S.f : ℤ) - 2 + (S.subschemeDegree Z : ℤ) ∧
      (invertibleCurveDegree S.k S.f (le_of_eq S.dimension_one) L <
          2 * (genus S.f : ℤ) - 2 + (S.subschemeDegree Z : ℤ) ∨
        Nonempty (S.idealTwist Z L ≅ Stacks.Duality.dualizingSheafOverField S.f))

Tag 0E3B, a lemma

Tag 0E3B in the Stacks Project.

AlgebraicGeometry.CohenMacaulayCurveSituation.isZero_cohomology_one_idealTwist_of_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/IdealTwistSections.lean, line 62. The attribute's comment: “the vanishing of H^1(X, IL)”.

[Stacks, Tag 0E3B], the vanishing. If deg(ℒ) > 2g - 2 + deg(Z) then H¹(X, ℐℒ) = 0: a nonzero H¹(X, ℐℒ) would force deg(ℒ) ≤ 2g - 2 + deg(Z) by [Stacks, Tag 0E3A].

theorem isZero_cohomology_one_idealTwist_of_lt (hZ : topologicalKrullDim Z.subscheme ≤ 0)
    (hdeg : 2 * (genus S.f : ℤ) - 2 + (S.subschemeDegree Z : ℤ) <
      invertibleCurveDegree S.k S.f (le_of_eq S.dimension_one) L) :
    IsZero (cohomologyOverField S.k S.f (S.idealTwist Z L) 1)

AlgebraicGeometry.CohenMacaulayCurveSituation.not_isZero_cohomology_zero_idealTwist_or_of_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/IdealTwistSections.lean, line 73. The attribute's comment: “possibilities (1) and (2)”.

[Stacks, Tag 0E3B], the alternative. If deg(ℒ) > 2g - 2 + deg(Z) then either H⁰(X, ℐℒ) ≠ 0, or g = 0 and deg(ℒ) = deg(Z) - 1. When H⁰(X, ℐℒ) = 0 the Euler characteristic χ(X, ℐℒ) = deg(ℒ) + 1 - g - deg(Z) vanishes, H¹(X, ℐℒ) vanishing as well.

theorem not_isZero_cohomology_zero_idealTwist_or_of_lt (hZ : topologicalKrullDim Z.subscheme ≤ 0)
    (hdeg : 2 * (genus S.f : ℤ) - 2 + (S.subschemeDegree Z : ℤ) <
      invertibleCurveDegree S.k S.f (le_of_eq S.dimension_one) L) :
    ¬ IsZero (cohomologyOverField S.k S.f (S.idealTwist Z L) 0) ∨
      (genus S.f = 0 ∧ invertibleCurveDegree S.k S.f (le_of_eq S.dimension_one) L =
        (S.subschemeDegree Z : ℤ) - 1)

AlgebraicGeometry.CohenMacaulayCurveSituation.exists_isIso_projectiveLine_of_genus_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/IdealTwistSections.lean, line 104. The attribute's comment: “in case (2) with Z empty, X is P^1_k and L corresponds to O(-1)”.

[Stacks, Tag 0E3B], case (2) with Z = ∅. If g = 0 and deg(ℒ) = -1, then X ≅ 𝐏¹_k over k, and under this isomorphism ℒ^{⊗ -1} is the pullback of 𝒪(1), i.e. ℒ corresponds to 𝒪_{𝐏¹}(-1). The invertible module ℒ^{⊗ -1} has degree one, so a basis of its two-dimensional space of global sections defines an isomorphism X ⟶ 𝐏¹_k ([Stacks, Tag 0C6T]) along which 𝒪(1) pulls back to ℒ^{⊗ -1}.

theorem exists_isIso_projectiveLine_of_genus_eq_zero
    (hgenus : genus S.f = 0)
    (hdeg : invertibleCurveDegree S.k S.f (le_of_eq S.dimension_one) L = -1) :
    ∃ p : S.X ⟶ projectiveSpaceOver 1 (Spec (.of S.k)),
      IsIso p ∧
      p ≫ Limits.pullback.fst (Limits.terminal.from (Spec (.of S.k)))
          (Limits.terminal.from (projectiveSpaceAtUniverse.{u} 1)) = S.f ∧
      Nonempty ((Scheme.Modules.pullback
          (p ≫ projectiveSpaceOver.toIntegralAtUniverse 1 (Spec (.of S.k)))).obj
            (Stacks.AmpleProjectiveImmersion.twistingSheafAtUniverse.{u} 1) ≅
          tensorPowerModule L (-1))

Tag 0E3C, a lemma

Tag 0E3C in the Stacks Project.

AlgebraicGeometry.CohenMacaulayCurveSituation.isGeneratedByGlobalSections_of_two_mul_genus_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/GlobalGenerationLargeDegree.lean, line 140.

Stacks Project, Tag 0E3C. In Situation [Stacks, Tag 0B5D] assume X is integral of genus g, and let ℒ be an invertible 𝒪_X-module. If deg(ℒ) ≥ 2g, then ℒ is generated by its global sections.

theorem isGeneratedByGlobalSections_of_two_mul_genus_le [IsIntegral S.X] (L : S.X.Modules)
    [SheafOfModules.IsInvertible S.X.presheaf S.X.ringCatSheaf.2 L]
    (hL : 2 * (genus S.f : ℤ) ≤ invertibleCurveDegree S.k S.f (le_of_eq S.dimension_one) L) :
    SheafOfModules.IsGeneratedByGlobalSections L

Tag 0E3D, a lemma

Tag 0E3D in the Stacks Project.

AlgebraicGeometry.CohenMacaulayCurveSituation.isGeneratedByGlobalSections_and_surjective_subschemeRestrictionπ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/GlobalGenerationLargeDegree.lean, line 306.

Stacks Project, Tag 0E3D. In Situation [Stacks, Tag 0B5D] assume X is integral of genus g, let ℒ be an invertible 𝒪_X-module, and let Z ⊆ X be a nonempty 0-dimensional closed subscheme. If deg(ℒ) ≥ 2g - 1 + deg(Z), then ℒ is generated by its global sections and H⁰(X, ℒ) ⟶ H⁰(X, ℒ|_Z) is surjective.

Here deg(Z) = dim_k Γ(Z, 𝒪_Z) and ℒ|_Z = ℒ ⊗ i_* 𝒪_Z. Global generation is [Stacks, Tag 0E3C], as deg(Z) ≥ 1; the surjectivity follows from H¹(X, ℐ_Z ℒ) = 0, which is [Stacks, Tag 0E3A] since deg(ℒ) > 2g - 2 + deg(Z).

theorem isGeneratedByGlobalSections_and_surjective_subschemeRestrictionπ [IsIntegral S.X]
    (L : S.X.Modules) [SheafOfModules.IsInvertible S.X.presheaf S.X.ringCatSheaf.2 L]
    (Z : S.X.IdealSheafData) (hZ : topologicalKrullDim Z.subscheme ≤ 0)
    (hZne : Nonempty Z.subscheme)
    (hL : 2 * (genus S.f : ℤ) - 1 + (S.subschemeDegree Z : ℤ) ≤
      invertibleCurveDegree S.k S.f (le_of_eq S.dimension_one) L) :
    SheafOfModules.IsGeneratedByGlobalSections L ∧
      Function.Surjective (cohomologyOverFieldMap S.k S.f (S.subschemeRestrictionπ Z L) 0)

Tag 0H2V, a lemma

Tag 0H2V in the Stacks Project.

AlgebraicGeometry.CohenMacaulayCurveSituation.isRelativelyVeryAmple_of_two_mul_genus_add_one_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/VeryAmpleLargeDegree.lean, line 264.

Invertible modules of degree at least 2g + 1 are very ample. In Situation [Stacks, Tag 0B5D] — a proper one-dimensional scheme X over a field k with H⁰(X, 𝒪_X) = k — assume X geometrically integral over k of genus g, and let ℒ be an invertible 𝒪_X-module. If deg(ℒ) ≥ 2g + 1, then ℒ is very ample.

theorem isRelativelyVeryAmple_of_two_mul_genus_add_one_le
    [AlgebraicGeometry.GeometricallyIntegral S.f] (L : S.X.Modules)
    [SheafOfModules.IsInvertible S.X.presheaf S.X.ringCatSheaf.2 L]
    (hL : 2 * (genus S.f : ℤ) + 1 ≤
      invertibleCurveDegree S.k S.f (le_of_eq S.dimension_one) L) :
    Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple S.f L

Tag 0E3E, a lemma

Tag 0E3E in the Stacks Project.

AlgebraicGeometry.exists_subcurve_invertibleCurveDegree_le_of_not_isZero_cohomology_idealTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/SubcurveDegreeBound.lean, line 452.

Stacks Project, Tag 0E3E. Let k be a field and X a proper scheme over k which is reduced and of dimension 1. Let ℒ be an invertible 𝒪_X-module and Z ⊆ X a closed subscheme of dimension at most zero with ideal sheaf ℐ. If H¹(X, ℐℒ) ≠ 0, then there is a reduced connected closed subscheme Y ⊆ X of dimension 1 with

deg(ℒ|_Y) ≤ -2 χ(Y, 𝒪_Y) + deg(Z ∩ Y),

where Z ∩ Y is the scheme-theoretic intersection Z ⊔ Y and deg(Z ∩ Y) = dim_k Γ(Z ∩ Y, 𝒪). Here ℐℒ is ℒ ⊗ ℐ, as in [Stacks, Tag 0E3A]; the source's hypothesis that X is connected is not needed.

A nonzero map ℐℒ ⟶ ω_X from duality ([Stacks, Tag 0BS2]) kills nothing more than the zero module, X being reduced, and AlgebraicGeometry.exists_le_invertibleCurveDegree_le_of_ne_zero applies with T₀ = X.

theorem exists_subcurve_invertibleCurveDegree_le_of_not_isZero_cohomology_idealTwist
    {k : Type u} [Field k] (f : X ⟶ Spec (.of k)) [IsProper f] [IsReduced X]
    (hdim : topologicalKrullDim X = 1) (L : X.Modules)
    [hL : SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
    (Z : X.IdealSheafData) (hZ : topologicalKrullDim Z.subscheme ≤ 0)
    (h : ¬ IsZero (cohomologyOverField k f
      ((((Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u}
            ⟨X.toRingedSpace.presheaf, X.toRingedSpace.IsSheaf⟩).obj L).obj
          (Stacks.ClosedImmersion.idealSheaf Z.subschemeι.toLRSHom.toShHom))) 1)) :
    ∃ (Y : X.IdealSheafData) (_ : IsReduced Y.subscheme) (_ : ConnectedSpace Y.subscheme)
      (hY : topologicalKrullDim Y.subscheme = 1),
      letI := Stacks.AlgebraicGeometry.Tag09NY.isInvertible_modulePullback Y.subschemeι L hL
      letI : Algebra k Γ((Z ⊔ Y).subscheme, ⊤) :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ ((Z ⊔ Y).subschemeι ≫ f).appTop).hom.toAlgebra
      invertibleCurveDegree k (Y.subschemeι ≫ f) hY.le
          ((Scheme.Modules.pullback Y.subschemeι).obj L) ≤
        -2 * (∑ᶠ n : ℕ, (-1 : ℤ) ^ n * (Module.finrank k (cohomologyOverField k
          (Y.subschemeι ≫ f) (SheafOfModules.unit Y.subscheme.ringCatSheaf) n) : ℤ)) +
          (Module.finrank k Γ((Z ⊔ Y).subscheme, ⊤) : ℤ)

Tag 0E3F, a lemma

Tag 0E3F in the Stacks Project.

AlgebraicGeometry.isGeneratedByGlobalSections_of_forall_subcurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/SubcurveFieldExtension.lean, line 557.

Stacks Project, Tag 0E3F. Let k be a field and X a proper scheme over k which is reduced and of dimension 1, and let ℒ be an invertible 𝒪_X-module such that deg(ℒ|_Y) ≥ 2 dim_k H¹(Y, 𝒪_Y) for every reduced connected closed subscheme Y ⊆ X of dimension 1. Then ℒ is globally generated. The source's hypothesis that X is connected is not needed.

As h⁰(Y, 𝒪_Y) ≥ 1, the bound gives -2 χ(Y, 𝒪_Y) < deg(ℒ|_Y) and h¹(Y, 𝒪_Y) < deg(ℒ|_Y) + χ(Y, 𝒪_Y), and AlgebraicGeometry.isGeneratedByGlobalSections_of_forall_subcurve_lt applies.

theorem isGeneratedByGlobalSections_of_forall_subcurve (f : X ⟶ Spec (.of k)) [IsProper f]
    [IsReduced X] (hdim : topologicalKrullDim X = 1) (L : X.Modules)
    [hL : SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
    (h : ∀ (Y : X.IdealSheafData) [IsReduced Y.subscheme] [ConnectedSpace Y.subscheme]
      (hY : topologicalKrullDim Y.subscheme = 1),
      letI := Stacks.AlgebraicGeometry.Tag09NY.isInvertible_modulePullback Y.subschemeι L hL
      2 * (Module.finrank k (cohomologyOverField k (Y.subschemeι ≫ f)
        (SheafOfModules.unit Y.subscheme.ringCatSheaf) 1) : ℤ) ≤
        invertibleCurveDegree k (Y.subschemeι ≫ f) hY.le
          ((Scheme.Modules.pullback Y.subschemeι).obj L)) :
    _root_.SheafOfModules.IsGeneratedByGlobalSections L

Sources

Lean

AlgebraicGeometry.CohenMacaulayCurveSituation.invertibleCurveDegree_le_and_lt_or_nonempty_iso_of_not_isZero_cohomology_idealTwist

· AlgebraicGeometry.CohenMacaulayCurveSituation.isZero_cohomology_one_idealTwist_of_lt · AlgebraicGeometry.CohenMacaulayCurveSituation.not_isZero_cohomology_zero_idealTwist_or_of_lt · AlgebraicGeometry.CohenMacaulayCurveSituation.exists_isIso_projectiveLine_of_genus_eq_zero · AlgebraicGeometry.CohenMacaulayCurveSituation.isGeneratedByGlobalSections_of_two_mul_genus_le · AlgebraicGeometry.CohenMacaulayCurveSituation.isGeneratedByGlobalSections_and_surjective_subschemeRestrictionπ · AlgebraicGeometry.CohenMacaulayCurveSituation.isRelativelyVeryAmple_of_two_mul_genus_add_one_le · AlgebraicGeometry.exists_subcurve_invertibleCurveDegree_le_of_not_isZero_cohomology_idealTwist

Section53.23 Contracting rational tails #

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

Tag 0E3H, an example

Tag 0E3H in the Stacks Project.

Stacks.Curves.isProper_complementaryCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/CanonicalContraction/ContractedCurve.lean, line 86. The attribute's comment: “complementary_curve_is_proper”.

Stacks 0E3H. The scheme-theoretic closure of the complement of a closed subscheme of a proper scheme over a field is again proper over that field. For a rational tail this is the assertion that X' is proper over k; no rational-tail hypothesis is needed for it.

theorem isProper_complementaryCurve
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))] (C : X.IdealSheafData) :
    IsProper (complementaryCurveι C ≫ (X ↘ Spec (.of k)))

Stacks.Curves.topologicalKrullDim_complementaryCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/CanonicalContraction/ContractedCurve.lean, line 104. The attribute's comment: “complementary_curve_has_dimension_one”.

Stacks 0E3H. The scheme-theoretic closure X' of the complement of a rational tail of a proper one-dimensional curve over a field with only constant global functions is again of dimension one.

theorem topologicalKrullDim_complementaryCurve
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (C : X.IdealSheafData) (hC : IsRationalTail k X C) :
    topologicalKrullDim (complementaryCurve C) = 1

Stacks.Curves.isIso_globalSections_complementaryCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/CanonicalContraction/ContractedCurve.lean, line 179. The attribute's comment: “complementary_curve_has_constant_global_functions”.

Stacks 0E3H. The scheme-theoretic closure X' of the complement of a rational tail of a proper one-dimensional nodal curve over a field with only constant global functions again has only constant global functions: H⁰(X', 𝒪_{X'}) = k.

theorem isIso_globalSections_complementaryCurve
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalTail k X C) :
    IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫
      (complementaryCurveι C ≫ (X ↘ Spec (.of k))).appTop)

Stacks.Curves.existsUnique_contractionOfRationalTail, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/CanonicalContraction/Existence.lean, line 195. The attribute's comment: “canonical_contraction”.

Stacks 0E3H. A rational tail of a proper one-dimensional nodal curve over a field with only constant global functions admits exactly one contraction onto the scheme-theoretic closure of its complement.

theorem existsUnique_contractionOfRationalTail
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫
      (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData)
    (hC : IsRationalTail k X C) :
    ∃! c : X ⟶ complementaryCurve C, IsContractionOfRationalTail hC c

Stacks.Curves.isIso_structureSheaf_to_pushforward_canonicalContraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/CanonicalContraction/Existence.lean, line 246. The attribute's comment: “pushforward_structure_sheaf”.

Stacks 0E3H. The canonical contraction c : X ⟶ X' of a rational tail induces an isomorphism 𝒪_{X'} ⟶ c_*𝒪_X of sheaves of rings.

theorem isIso_structureSheaf_to_pushforward_canonicalContraction
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫
      (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData)
    (hC : IsRationalTail k X C) :
    IsIso (canonicalContraction k X hdim hnodal C hC).toRingCatSheafHom

Stacks.Curves.smoothAt_or_isNode_complementaryCurve_of_notMem_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/CanonicalContraction/NodalAwayFromAttaching.lean, line 119. The attribute's comment: “at_worst_nodal_away_from_the_attaching_point”.

Stacks 0E3H, the at-worst-nodal singularities of X' away from the attaching point. Let X be a proper one-dimensional scheme over a field k with at-worst-nodal singularities and only constant global functions, let C ⊆ X be a rational tail and let X' be the scheme-theoretic closure of the complement of C. Every closed point of X' whose image in X lies outside C is smooth over k or is a node of X'.

theorem smoothAt_or_isNode_complementaryCurve_of_notMem_support
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalTail k X C)
    (y : complementaryCurve C) (hyc : IsClosed ({y} : Set (complementaryCurve C)))
    (hy : (complementaryCurveι C).base y ∈ (C.support.compl : X.Opens)) :
    letI : (complementaryCurve C).Over (Spec (.of k)) :=
      ⟨complementaryCurveι C ≫ (X ↘ Spec (.of k))⟩
    InfinitesimalLifting.SmoothAt (complementaryCurveι C ≫ (X ↘ Spec (.of k))) y ∨
      IsNode k (complementaryCurve C) y

Stacks.Curves.nodal_complementaryCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/CanonicalContraction/SmoothAtAttaching.lean, line 499. The attribute's comment: “complementary_curve_has_at_worst_nodal_singularities”.

Stacks 0E3H: the scheme-theoretic closure of the complement of a rational tail of a proper one-dimensional nodal curve with only constant global functions again has at-worst-nodal singularities. Away from the attaching point this is the étale transport of Stacks.Curves.smoothAt_or_isNode_complementaryCurve_of_notMem_support; at the attaching point the closure is in fact smooth over k, by Stacks.Curves.smoothAt_complementaryCurve_attachingPoint.

theorem nodal_complementaryCurve
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalTail k X C) :
    letI : (complementaryCurve C).Over (Spec (.of k)) :=
      ⟨complementaryCurveι C ≫ (X ↘ Spec (.of k))⟩
    HasAtWorstNodalSingularities k (complementaryCurve C)

Stacks.Curves.tail_inf_complementaryCurveIdeal_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ComplementaryCurve/SchemeTheoreticUnion.lean, line 158. The attribute's comment: “scheme_theoretic_union”.

A rational tail C on a proper one-dimensional scheme over a field with at-worst-nodal singularities and with only constant global functions, together with the scheme-theoretic closure of its complement, has scheme-theoretic union the entire curve. Reducedness of the curve comes from the nodality hypothesis.

theorem tail_inf_complementaryCurveIdeal_eq_bot (k : Type u) [Field k] (X : Scheme.{u})
    [X.Over (Spec (.of k))] [IsProper (X ↘ Spec (.of k))]
    (_hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X) (C : X.IdealSheafData)
    (_hC : IsRationalTail k X C) :
    C ⊓ complementaryCurveIdeal C = ⊥

Stacks.Curves.isNode_attachingPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/AttachingPointNode.lean, line 46. The attribute's comment: “attaching_point_is_node”.

Stacks 0E3H. The attaching point of a rational tail — where it meets the closure of its complement — is a node of the ambient curve.

theorem isNode_attachingPoint
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalTail k X C) :
    IsNode k X (C.subschemeι hC.attachingPoint)

Stacks.Curves.isFiniteSeparable_residueField_attachingPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/AttachingPointNode.lean, line 94. The attribute's comment: “finite_separable_residue_field”.

Stacks 0E3H. At the attaching point of a rational tail, the extension of the residue field by the residue field of the node (in the sense of Stacks.Curves.IsNode) is finite and separable.

theorem isFiniteSeparable_residueField_attachingPoint
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalTail k X C) :
    let x := C.subschemeι hC.attachingPoint
    let kToStalk : k →+* X.presheaf.stalk x :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop ≫
        X.presheaf.germ ⊤ x (by simp)).hom
    letI : Algebra k (X.presheaf.stalk x) := kToStalk.toAlgebra
    letI : Algebra k (X.residueField x) := ((X.residue x).hom.comp kToStalk).toAlgebra
    Module.Finite k (X.residueField x) ∧ Algebra.IsSeparableExtension k (X.residueField x)

AlgebraicGeometry.IsContractionOfRationalTail, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/Contraction.lean, line 63. The attribute's comment: “contraction_of_a_rational_tail”.

A morphism contracting a rational tail onto its complementary curve.

def IsContractionOfRationalTail {k : Type u} [Field k] {X : Scheme.{u}}
    [X.Over (Spec (.of k))] {C : X.IdealSheafData} (hC : IsRationalTail k X C)
    (c : X ⟶ complementaryCurve C) : Prop

AlgebraicGeometry.IsRationalTail, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/RationalTail.lean, line 72. The attribute's comment: “rational_tail”.

An integral irreducible component C of a scheme over k is a rational tail when the closure of its complement is nonempty, its intersection with C is one reduced point, the global functions on C map isomorphically to the residue field of that point, and C has genus zero.

def IsRationalTail (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    (C : X.IdealSheafData) : Prop

Stacks.Curves.genus_complementaryCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/DirectImage/RationalTailCohomologyIso.lean, line 254. The attribute's comment: “complementary_curve”.

Contracting a rational tail does not change the genus: for X proper over k of dimension one with at worst nodal singularities and only constant global functions, and C ⊆ X a rational tail, the scheme-theoretic closure X' of the complement of C has the genus of X.

This is the genus clause of [Stacks, Tag 0E3H], with no hypothesis beyond that tag's own. It is Stacks.Curves.contractionCohomologyObjIso at the canonical contraction, restricted further along the structure map of X' — which identifies the two k-module structures by Stacks.Curves.structureMap_appTop_comp_appTop — and then read as an equality of dimensions.

The attribute registers Tag 0E3H with the sub-label "complementary_curve", and not the bare tag: [Stacks, Tag 0E3H] makes several separate assertions about X' and this declaration proves only the one about the genus, so no single declaration states the whole example.

theorem genus_complementaryCurve
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalTail k X C) :
    genus (complementaryCurveι C ≫ (X ↘ Spec (.of k))) = genus (X ↘ Spec (.of k))

Stacks.Curves.isZero_rightDerived_one_pushforward_ambientStructureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/DirectImage/RationalTailHigherDirectImage.lean, line 284. The attribute's comment: “higher_direct_image_vanishing”.

R ¹ c_* 𝒪_X = 0 for a contraction c of a rational tail on a nodal curve.

This is the direct-image vanishing clause of [Stacks, Tag 0E3H], at that tag's standing hypotheses: X is proper and one-dimensional over k with only constant global functions and at worst nodal singularities. Those hypotheses enter only through Stacks.Curves.tail_inf_complementaryCurveIdeal_eq_bot, which says that the tail and the closure of its complement cover X scheme-theoretically, so that the union term of Stacks.Curves.isZero_rightDerived_one_pushforward_schemeTheoreticUnion is the structure sheaf of X itself.

The genus equality that [Stacks, Tag 0E3H] ultimately asserts is downstream of this and is not claimed here; the scoped sub-label registers the direct-image clause alone.

public theorem isZero_rightDerived_one_pushforward_ambientStructureSheaf
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    {hC : IsRationalTail k X C} {c : X ⟶ complementaryCurve C}
    (hc : IsContractionOfRationalTail hC c) :
    Limits.IsZero (((Scheme.Modules.pushforward c).rightDerived 1).obj
      (Scheme.IdealSheafData.ambientStructureSheaf X))

Tag 0E63, a lemma

Tag 0E63 in the Stacks Project.

AlgebraicGeometry.invertibleCurveDegree_pullback_dualizingSheafOverField_neg_of_isRationalTail, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/DualizingSheafDegree.lean, line 317.

Stacks Project, Tag 0E63. Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k and at-worst-nodal singularities, and let C ⊆ X be a rational tail. Then deg(ω_X|_C) < 0.

Here ω_X is invertible (AlgebraicGeometry.isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities). The sequence 0 ⟶ ω_C ⟶ ω_X|_C ⟶ 𝒪_{C ∩ X'} ⟶ 0 of [Stacks, Tag 0E34] gives deg(ω_X|_C) = -[k' : k] with k' = Γ(C, 𝒪_C) (AlgebraicGeometry.invertibleCurveDegree_eq_neg_of_isRationalTail).

theorem invertibleCurveDegree_pullback_dualizingSheafOverField_neg_of_isRationalTail
    [IsProper (X ↘ Spec (.of k))] (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalTail k X C) :
    haveI := connectedSpace_of_isIso_globalSections k (X ↘ Spec (.of k))
    letI hω := isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k X hdim
      hnodal
    letI := Stacks.AlgebraicGeometry.Tag09NY.isInvertible_modulePullback C.subschemeι
      (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k))) hω
    invertibleCurveDegree k (C.subschemeι ≫ (X ↘ Spec (.of k)))
        (Stacks.Curves.topologicalKrullDim_subscheme_eq_one_of_isRationalTail k X hdim C hC).le
        ((Scheme.Modules.pullback C.subschemeι).obj
          (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k)))) < 0

Tag 0E3I, a lemma

Tag 0E3I in the Stacks Project.

AlgebraicGeometry.exists_iso_sigma_isRationalTail_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/BaseChange.lean, line 184.

[Stacks, Tag 0E3I]. Let X be a proper scheme over a field k of dimension one with H⁰(X, 𝒪_X) = k and at-worst-nodal singularities, and let C ⊆ X be a rational tail. For every field extension K/k the base change C_K ⊆ X_K is a finite disjoint union of rational tails of X_K: there are finitely many rational tails Dᵢ of X_K and an isomorphism ∐ᵢ Dᵢ ≅ C_K compatible with the closed immersions into X_K.

theorem exists_iso_sigma_isRationalTail_baseChange
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalTail k X C) :
    let g : Spec (.of K) ⟶ Spec (.of k) :=
      Spec.map (CommRingCat.ofHom (algebraMap k K))
    let Y := (pullback (X ↘ Spec (.of k)) g : Scheme.{u})
    let p : Y ⟶ X := pullback.fst (X ↘ Spec (.of k)) g
    letI : Y.Over (Spec (.of K)) := ⟨pullback.snd (X ↘ Spec (.of k)) g⟩
    ∃ (ι : Type u) (_ : Finite ι) (D : ι → Y.IdealSheafData)
        (_ : ∀ i, IsRationalTail K Y (D i))
        (e : (∐ fun i ↦ (D i).subscheme) ≅ (C.comap p).subscheme),
      e.hom ≫ (C.comap p).subschemeι =
        Sigma.desc (fun i ↦ (D i).subschemeι)

Tag 0E3J, a lemma

Tag 0E3J in the Stacks Project.

AlgebraicGeometry.finrank_cohomologyOverField_one_le_invertibleCurveDegree_of_forall_not_isRationalTail, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/DualizingSheafDegree.lean, line 261.

Stacks Project, Tag 0E3J. Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k and at-worst-nodal singularities. If X has no rational tail, then for every reduced connected closed subscheme Y ⊆ X, Y ≠ X, of dimension one, deg(ω_X|_Y) ≥ dim_k H¹(Y, 𝒪_Y).

Here ω_X is invertible (AlgebraicGeometry.isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities). If the inequality failed, then deg(ω_X|_Y) < 0; for Y irreducible this makes Y a rational tail, and otherwise some one-dimensional component C of Y has deg(ω_X|_C) < 0 ([Stacks, Tag 0AYW]) and is a rational tail by the same analysis.

theorem finrank_cohomologyOverField_one_le_invertibleCurveDegree_of_forall_not_isRationalTail
    [IsProper (X ↘ Spec (.of k))] (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X)
    (htail : ∀ C : X.IdealSheafData, ¬ IsRationalTail k X C)
    (Y : X.IdealSheafData) [IsReduced Y.subscheme] [ConnectedSpace Y.subscheme]
    (hY : topologicalKrullDim Y.subscheme = 1) (hYX : Y ≠ ⊥) :
    haveI := connectedSpace_of_isIso_globalSections k (X ↘ Spec (.of k))
    letI hω := isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k X hdim
      hnodal
    letI := Stacks.AlgebraicGeometry.Tag09NY.isInvertible_modulePullback Y.subschemeι
      (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k))) hω
    (Module.finrank k (cohomologyOverField k (Y.subschemeι ≫ (X ↘ Spec (.of k)))
        (SheafOfModules.unit Y.subscheme.ringCatSheaf) 1) : ℤ) ≤
      invertibleCurveDegree k (Y.subschemeι ≫ (X ↘ Spec (.of k))) hY.le
        ((Scheme.Modules.pullback Y.subschemeι).obj
          (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k))))

Tag 0E3K, a lemma

Tag 0E3K in the Stacks Project.

AlgebraicGeometry.exists_planeCurveData_deg_two_of_forall_not_isRationalTail, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusZeroPositiveDegree/CanonicalNodal.lean, line 94. The attribute's comment: “part (1)”.

Stacks Project, Tag 0E3K, part (1). Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k, with at-worst-nodal singularities and no rational tail. If X has genus 0, then X is isomorphic to an irreducible plane conic and ω_X^{⊗ -1} is very ample.

ω_X is invertible of degree 2g - 2 = -2 ([Stacks, Tag 0E37], [Stacks, Tag 0C19]) and satisfies the subcurve bound of [Stacks, Tag 0E3J], so AlgebraicGeometry.exists_planeCurveData_deg_two_of_subcurve_bound applies.

theorem exists_planeCurveData_deg_two_of_forall_not_isRationalTail
    [IsProper (X ↘ Spec (.of k))] (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (htail : ∀ C : X.IdealSheafData, ¬ IsRationalTail k X C)
    (hgenus : genus (X ↘ Spec (.of k)) = 0) :
    (∃ C : ProjectiveSpectrum.Proj.PlaneCurveData k, C.deg = 2 ∧ IrreducibleSpace C.Z ∧
      ∃ e : X ≅ C.Z, e.hom ≫ C.toSpec = X ↘ Spec (.of k)) ∧
    haveI := connectedSpace_of_isIso_globalSections k (X ↘ Spec (.of k))
    letI := isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k X hdim hnodal
    letI := tensorPower_isInvertible X.presheaf X.ringCatSheaf.2
      (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k))) (-1)
    Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple (X ↘ Spec (.of k))
      (tensorPower X.presheaf X.ringCatSheaf.2
        (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k))) (-1))

AlgebraicGeometry.nonempty_dualizingSheafOverField_iso_unit_of_forall_not_isRationalTail, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusZeroPositiveDegree/CanonicalNodal.lean, line 130. The attribute's comment: “part (2)”.

Stacks Project, Tag 0E3K, part (2). Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k, with at-worst-nodal singularities and no rational tail. If X has genus 1, then ω_X ≅ 𝒪_X.

ω_X is invertible of degree 2g - 2 = 0 with h⁰(ω_X) = g = 1, and satisfies the subcurve bound of [Stacks, Tag 0E3J]; so every component degree is nonnegative, they sum to 0 ([Stacks, Tag 0AYW]), and [Stacks, Tag 0E22] applies (AlgebraicGeometry.isTrivial_of_subcurve_bound).

theorem nonempty_dualizingSheafOverField_iso_unit_of_forall_not_isRationalTail
    [IsProper (X ↘ Spec (.of k))] (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (htail : ∀ C : X.IdealSheafData, ¬ IsRationalTail k X C)
    (hgenus : genus (X ↘ Spec (.of k)) = 1) :
    Nonempty (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k)) ≅
      SheafOfModules.unit X.ringCatSheaf)

AlgebraicGeometry.isGeneratedByGlobalSections_tensorPower_dualizingSheafOverField_of_forall_not_isRationalTail, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusZeroPositiveDegree/CanonicalNodal.lean, line 164. The attribute's comment: “part (3)”.

Stacks Project, Tag 0E3K, part (3). Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k, with at-worst-nodal singularities and no rational tail. If the genus of X is at least 2, then ω_X^{⊗ m} is globally generated for every m ≥ 2.

ω_X is invertible of degree 2g - 2 and satisfies the subcurve bound of [Stacks, Tag 0E3J], which with g ≥ 2 and m ≥ 2 gives the inequalities of [Stacks, Tag 0E3F] (AlgebraicGeometry.isGeneratedByGlobalSections_tensorPower_of_subcurve_bound).

theorem isGeneratedByGlobalSections_tensorPower_dualizingSheafOverField_of_forall_not_isRationalTail
    [IsProper (X ↘ Spec (.of k))] (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (htail : ∀ C : X.IdealSheafData, ¬ IsRationalTail k X C)
    (hgenus : 2 ≤ genus (X ↘ Spec (.of k))) (m : ℕ) (hm : 2 ≤ m) :
    haveI := connectedSpace_of_isIso_globalSections k (X ↘ Spec (.of k))
    letI := isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k X hdim hnodal
    SheafOfModules.IsGeneratedByGlobalSections
      (tensorPower X.presheaf X.ringCatSheaf.2
        (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k))) m)

Tag 0E3L, a lemma

Tag 0E3L in the Stacks Project.

AlgebraicGeometry.IsIteratedContractionOfRationalTails.exists_planeCurveData_deg_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/Terminal.lean, line 60. The attribute's comment: “part (1)”.

Stacks Project, Tag 0E3L, part (1). Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k and at-worst-nodal singularities, and X → X' a chain of contractions of rational tails after which none are left. If X has genus 0, then X' is an irreducible plane conic over k.

theorem exists_planeCurveData_deg_two (hgenus : genus fX = 0) :
    ∃ C : ProjectiveSpectrum.Proj.PlaneCurveData k, C.deg = 2 ∧ IrreducibleSpace C.Z ∧
      ∃ e : Y ≅ C.Z, e.hom ≫ C.toSpec = fY

AlgebraicGeometry.IsIteratedContractionOfRationalTails.nonempty_dualizingSheafOverField_iso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/Terminal.lean, line 76. The attribute's comment: “part (2)”.

Stacks Project, Tag 0E3L, part (2). Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k and at-worst-nodal singularities, and X → X' a chain of contractions of rational tails after which none are left. If X has genus 1, then ω_{X'} ≅ 𝒪_{X'}.

theorem nonempty_dualizingSheafOverField_iso_unit (hgenus : genus fX = 1) :
    haveI : IsProper fY := isProper_target hseq hdim hnodal
    Nonempty (Stacks.Duality.dualizingSheafOverField fY ≅ SheafOfModules.unit Y.ringCatSheaf)

AlgebraicGeometry.IsIteratedContractionOfRationalTails.isGeneratedByGlobalSections_tensorPower_dualizingSheafOverField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/Terminal.lean, line 92. The attribute's comment: “part (3)”.

Stacks Project, Tag 0E3L, part (3). Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k and at-worst-nodal singularities, and X → X' a chain of contractions of rational tails after which none are left. If the genus of X is at least 2, then ω_{X'} is invertible and ω_{X'}^{⊗ m} is globally generated for every m ≥ 2.

theorem isGeneratedByGlobalSections_tensorPower_dualizingSheafOverField
    (hgenus : 2 ≤ genus fX) (m : ℕ) (hm : 2 ≤ m) :
    letI : Y.Over (Spec (.of k)) := ⟨fY⟩
    haveI : IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ fY.appTop) :=
      isIso_globalSections_target hseq hdim hnodal
    haveI := connectedSpace_of_isIso_globalSections k fY
    haveI : IsProper fY := isProper_target hseq hdim hnodal
    letI : SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.2
        (Stacks.Duality.dualizingSheafOverField fY) :=
      @isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k _ Y _ this _
        (topologicalKrullDim_target hseq hdim hnodal)
        (hasAtWorstNodalSingularities_target hseq hdim hnodal)
    SheafOfModules.IsGeneratedByGlobalSections
      (tensorPower Y.presheaf Y.ringCatSheaf.2 (Stacks.Duality.dualizingSheafOverField fY) m)

AlgebraicGeometry.IsIteratedContractionOfRationalTails.existsUnique_iso_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/TerminalBaseChange.lean, line 678. The attribute's comment: “compatibility with base field extensions”.

Stacks Project, Tag 0E3L, compatibility with extension of the ground field. Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k, at-worst-nodal singularities and genus at least one, c : X ⟶ Y a chain of contractions of rational tails after which none are left, and K/k a field extension. For every chain d : X_K ⟶ Z of contractions of rational tails of X_K after which none are left, there is a unique isomorphism e : Y_K ≅ Z with c_K ≫ e = d: the formation of the contraction of all rational tails commutes with the base change to K.

d factors through c_K (AlgebraicGeometry.IsIteratedContractionOfRationalTails.exists_comp_eq_baseChange, using [Stacks, Tag 0E3I]). Conversely Y_K is a nodal curve of positive genus without rational tails (AlgebraicGeometry.forall_not_isRationalTail_baseChange) and 𝒪_{Y_K} = (c_K)_*𝒪_{X_K} by flat base change, so c_K factors through d (IsIteratedContractionOfRationalTails.exists_comp_eq_of_forall_not_isRationalTail). The two factorizations are mutually inverse, c_K and d being dominant onto reduced curves.

theorem IsIteratedContractionOfRationalTails.existsUnique_iso_baseChange (k K : Type u) [Field k]
    [Field K] [Algebra k K] {X Y : Scheme.{u}} {fX : X ⟶ Spec (.of k)} {fY : Y ⟶ Spec (.of k)}
    {c : X ⟶ Y} [IsProper fX] (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ fX.appTop)]
    (hnodal : letI : X.Over (Spec (.of k)) := ⟨fX⟩
      Stacks.Curves.HasAtWorstNodalSingularities k X)
    (hgenus : 1 ≤ genus fX)
    (hseq : IsIteratedContractionOfRationalTails k fX fY c)
    (hterminal : ∀ C : Y.IdealSheafData, ¬ @IsRationalTail k _ Y ⟨fY⟩ C)
    {Z : Scheme.{u}} {fZ : Z ⟶ Spec (.of K)} {d : pullback fX (Spec.map (CommRingCat.ofHom
        (algebraMap k K))) ⟶ Z}
    (hd : IsIteratedContractionOfRationalTails K (pullback.snd fX (Spec.map (CommRingCat.ofHom
        (algebraMap k K)))) fZ d)
    (hdterminal : ∀ C : Z.IdealSheafData, ¬ @IsRationalTail K _ Z ⟨fZ⟩ C) :
    ∃! e : pullback fY (Spec.map (CommRingCat.ofHom (algebraMap k K))) ≅ Z,
      pullback.map fX (Spec.map (CommRingCat.ofHom (algebraMap k K))) fY (Spec.map
          (CommRingCat.ofHom (algebraMap k K))) c (𝟙 _) (𝟙 _)
        (by rw [Category.comp_id, hseq.comp_structureMap]) (by simp) ≫ e.hom = d

AlgebraicGeometry.IsIteratedContractionOfRationalTails.existsUnique_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalTails/Uniqueness.lean, line 402. The attribute's comment: “independence of choices”.

Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k, at-worst-nodal singularities and genus at least one. For two chains c₁ : X ⟶ Y₁ and c₂ : X ⟶ Y₂ of contractions of rational tails after which none are left, there is a unique isomorphism e : Y₁ ≅ Y₂ with c₁ ≫ e = c₂.

theorem existsUnique_iso {X Y₁ Y₂ : Scheme.{u}} {fX : X ⟶ Spec (.of k)}
    {fY₁ : Y₁ ⟶ Spec (.of k)} {fY₂ : Y₂ ⟶ Spec (.of k)} {c₁ : X ⟶ Y₁} {c₂ : X ⟶ Y₂}
    [IsProper fX] (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ fX.appTop)]
    (hnodal : letI : X.Over (Spec (.of k)) := ⟨fX⟩
      Stacks.Curves.HasAtWorstNodalSingularities k X)
    (hgenus : 1 ≤ genus fX)
    (hseq₁ : IsIteratedContractionOfRationalTails k fX fY₁ c₁)
    (hterminal₁ : ∀ C : Y₁.IdealSheafData, ¬ @IsRationalTail k _ Y₁ ⟨fY₁⟩ C)
    (hseq₂ : IsIteratedContractionOfRationalTails k fX fY₂ c₂)
    (hterminal₂ : ∀ C : Y₂.IdealSheafData, ¬ @IsRationalTail k _ Y₂ ⟨fY₂⟩ C) :
    ∃! e : Y₁ ≅ Y₂, c₁ ≫ e.hom = c₂

Sources

LeanStacks.Curves.isProper_complementaryCurve · Stacks.Curves.topologicalKrullDim_complementaryCurve · Stacks.Curves.isIso_globalSections_complementaryCurve · Stacks.Curves.existsUnique_contractionOfRationalTail · Stacks.Curves.isIso_structureSheaf_to_pushforward_canonicalContraction · Stacks.Curves.smoothAt_or_isNode_complementaryCurve_of_notMem_support · Stacks.Curves.nodal_complementaryCurve · Stacks.Curves.tail_inf_complementaryCurveIdeal_eq_bot

Section53.24 Contracting rational bridges #

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

Tag 0E3M, an example

Tag 0E3M in the Stacks Project.

AlgebraicGeometry.IsRationalBridge, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/Basic.lean, line 48. The attribute's comment: “rational_bridge”.

An integral irreducible component is a rational bridge if the closure of its complement is nonempty, the intersection has degree two over its global functions, and its genus is zero.

def IsRationalBridge (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))] (C : X.IdealSheafData) : Prop

Stacks.Curves.exists_isProper_structureMorphism_and_genus_eq_contraction_bridge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/ContractionGenus.lean, line 112. The attribute's comment: “Y is proper over k of dimension one with H⁰(Y, 𝒪_Y) = k and the genus of X”.

The target of a contraction of a rational bridge is a proper scheme over k of dimension one with H⁰(Y, 𝒪_Y) = k and the genus of X. That is, there is a morphism g : Y ⟶ Spec k with c ≫ g the structure morphism of X which has these properties.

theorem exists_isProper_structureMorphism_and_genus_eq_contraction_bridge
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalBridge k X C)
    {Y : Scheme.{u}} (c : X ⟶ Y) (hc : IsContractionOfRationalBridge hC c) :
    ∃ g : Y ⟶ Spec (.of k), c ≫ g = X ↘ Spec (.of k) ∧ IsProper g ∧
      topologicalKrullDim Y = 1 ∧ IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ g.appTop) ∧
      genus g = genus (X ↘ Spec (.of k))

Stacks.Curves.hasAtWorstNodalSingularities_pushoutScheme_bridge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/ContractionNodal.lean, line 382. The attribute's comment: “the singularities of Y are at-worst-nodal”.

The singularities of the contraction Y of a rational bridge, the pushout AlgebraicGeometry.pushoutScheme of Stacks.Curves.bridgePushoutSituation over k by AlgebraicGeometry.pushoutToBase, are at-worst-nodal.

theorem hasAtWorstNodalSingularities_pushoutScheme_bridge
    (hdim : topologicalKrullDim X = 1)
    (hnodal : HasAtWorstNodalSingularities k X)
    {C : X.IdealSheafData} (hC : IsRationalBridge k X C) :
    letI : (pushoutScheme (bridgePushoutSituation hdim hnodal hC)).Over (Spec (.of k)) :=
      ⟨pushoutToBase (bridgePushoutSituation hdim hnodal hC)⟩
    HasAtWorstNodalSingularities k (pushoutScheme (bridgePushoutSituation hdim hnodal hC))

Stacks.Curves.isField_globalSections_bridge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/Intersection.lean, line 76. The attribute's comment: “k' = H⁰(C, 𝒪_C) is a field”.

The ring of global functions on a rational bridge is a field: the bridge is an integral scheme proper over k, so its global functions form a field ([Stacks, Tag 0BUG]).

theorem isField_globalSections_bridge (k : Type u) [Field k] (X : Scheme.{u})
    [X.Over (Spec (.of k))] [IsProper (X ↘ Spec (.of k))]
    (_hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (_hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalBridge k X C) :
    IsField Γ(C.subscheme, ⊤)

Stacks.Curves.isNode_of_mem_intersection_bridge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/Intersection.lean, line 106. The attribute's comment: “the points of C ∩ X' are nodes of X”.

Every point of the intersection of a rational bridge with the closure of its complement is a node of the ambient curve. At least two irreducible components of X pass through each such point, so [Stacks, Tag 0E38] applies.

theorem isNode_of_mem_intersection_bridge (k : Type u) [Field k] (X : Scheme.{u})
    [X.Over (Spec (.of k))] [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalBridge k X C)
    (w : intersectionWithComplementaryCurve C) :
    IsNode k X ((intersectionWithComplementaryCurveIdeal C).subschemeι.base w)

Stacks.Curves.moduleFinite_and_isSeparable_globalSections_bridge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/IntersectionSections.lean, line 414. The attribute's comment: “k'/k is a finite separable extension of fields”.

The field of global functions on a rational bridge is a finite separable extension of the base field. This is the assertion "k'/k is a finite separable extension of fields" of [Stacks, Tag 0E3M], for C ⊆ X a rational bridge of a proper one-dimensional at-worst-nodal curve over k with only constant global functions and k' = Γ(C, 𝒪_C).

Finiteness is clause (1) of [Stacks, Tag 0BUG] (Stacks.AlgebraicGeometry.ProperSectionsGeom.moduleFinite_globalSections_of_isProper): the bridge is a closed subscheme of X, hence proper over k. Separability is the source's appeal to [Stacks, Tag 0C4D] at a point w of C ∩ X', which is nonempty (Stacks.Curves.nonempty_intersection_bridge): that point is a node of X, so the residue field there is separable over k (Stacks.Curves.isSeparableExtension_residueField_intersection_bridge), hence geometrically reduced over k by Tag 030W; the evaluation of global functions of the bridge at w embeds k' in that residue field, k' being a field, so k' is geometrically reduced over k too and therefore separable, which for the finite extension k'/k is separability in the sense of Algebra.IsSeparable.

theorem moduleFinite_and_isSeparable_globalSections_bridge
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalBridge k X C) :
    letI : IsIntegral C.subscheme := hC.isIntegral
    letI : Field Γ(C.subscheme, ⊤) :=
      (isField_of_universallyClosed k (C.subschemeι ≫ (X ↘ Spec (.of k)))).toField
    letI : Algebra k Γ(C.subscheme, ⊤) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫
        (C.subschemeι ≫ (X ↘ Spec (.of k))).appTop).hom.toAlgebra
    Module.Finite k Γ(C.subscheme, ⊤) ∧ Algebra.IsSeparable k Γ(C.subscheme, ⊤)

Stacks.Curves.isField_and_isSeparable_or_algEquiv_prod_intersectionSections_bridge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/IntersectionSections.lean, line 475. The attribute's comment: “k''/k' is either a degree two separable extension of fields or k'' = k' × k'”.

The degree two extension k''/k' of [Stacks, Tag 0E3M] is either a separable field extension or the square of k'. Here C ⊆ X is a rational bridge of a proper one-dimensional at-worst-nodal curve over k with only constant global functions, X' is the scheme-theoretic closure of X \ C, and k' = Γ(C, 𝒪_C), k'' = Γ(C ∩ X', 𝒪).

The intersection is geometrically reduced over k (Stacks.Curves.geometricallyReduced_intersection_bridge), so k'' is a finite etale k-algebra, and the degree of k'' over k' is two by the defining condition of a rational bridge; the dichotomy is then Stacks.Curves.isField_and_isSeparable_or_algEquiv_prod_of_etale_of_finrank_eq_two.

theorem isField_and_isSeparable_or_algEquiv_prod_intersectionSections_bridge
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalBridge k X C) :
    letI : IsIntegral C.subscheme := hC.isIntegral
    letI : Field Γ(C.subscheme, ⊤) :=
      (isField_of_universallyClosed k (C.subschemeι ≫ (X ↘ Spec (.of k)))).toField
    letI : Algebra Γ(C.subscheme, ⊤) Γ(intersectionWithComplementaryCurve C, ⊤) :=
      (Scheme.IdealSheafData.inclusion
        (le_sup_left : C ≤ intersectionWithComplementaryCurveIdeal C)).appTop.hom.toAlgebra
    (IsField Γ(intersectionWithComplementaryCurve C, ⊤) ∧
          Module.finrank Γ(C.subscheme, ⊤) Γ(intersectionWithComplementaryCurve C, ⊤) = 2 ∧
          Algebra.IsSeparable Γ(C.subscheme, ⊤) Γ(intersectionWithComplementaryCurve C, ⊤)) ∨
        Nonempty (Γ(intersectionWithComplementaryCurve C, ⊤) ≃ₐ[Γ(C.subscheme, ⊤)]
          (Γ(C.subscheme, ⊤) × Γ(C.subscheme, ⊤)))

Stacks.Curves.exists_ringEquiv_completedLocalRing_contraction_bridge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/PushoutCompletionShape.lean, line 145. The attribute's comment: “𝒪^∧_{Y,y} ≅ {f ∈ k''[[s]] : f(0) ∈ k'}, and ≅ k'[[s,t]]/(st) when k'' = k' × k'”.

The completed local ring of the contraction of a rational bridge at the image of Spec k'. Let k be a field, X a proper scheme over k of dimension one with H⁰(X, 𝒪_X) = k and at-worst-nodal singularities, and C ⊆ X a rational bridge; let X' be the scheme-theoretic closure of X \ C, k' = Γ(C, 𝒪_C), k'' = Γ(C ∩ X', 𝒪) and Y the pushout of C ∩ X' ⟶ X' along C ∩ X' ⟶ Spec k'. Let y ∈ Y be the image of Spec k', the image of every point of that spectrum. Then
𝒪^∧_{Y, y} ≅ {f ∈ k''⟦s⟧ : f(0) ∈ k'},
and 𝒪^∧_{Y, y} ≅ k'⟦s, t⟧/(st) when C ∩ X' has two points, that is when k'' = k' × k'.

theorem exists_ringEquiv_completedLocalRing_contraction_bridge
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalBridge k X C) :
    letI : IsIntegral C.subscheme := hC.isIntegral
    letI : Field Γ(C.subscheme, ⊤) :=
      (isField_of_universallyClosed k (C.subschemeι ≫ (X ↘ Spec (.of k)))).toField
    letI : Algebra Γ(C.subscheme, ⊤) Γ(intersectionWithComplementaryCurve C, ⊤) :=
      (Scheme.IdealSheafData.inclusion
        (le_sup_left : C ≤ intersectionWithComplementaryCurveIdeal C)).appTop.hom.toAlgebra
    ∃ y : pushoutScheme (bridgePushoutSituation hdim hnodal hC),
      (∀ p : (bridgePushoutSituation hdim hnodal hC).Y,
          pushoutInr (bridgePushoutSituation hdim hnodal hC) p = y) ∧
        Nonempty (Scheme.completedLocalRing
            (pushoutScheme (bridgePushoutSituation hdim hnodal hC)) y ≃+*
          ↥(PowerSeries.constantCoeffInBase (Γ(C.subscheme, ⊤) : Type u)
            (Γ(intersectionWithComplementaryCurve C, ⊤) : Type u))) ∧
        (Nonempty (Γ(intersectionWithComplementaryCurve C, ⊤) ≃ₐ[(Γ(C.subscheme, ⊤) : Type u)]
            ((Γ(C.subscheme, ⊤) : Type u) × (Γ(C.subscheme, ⊤) : Type u))) →
          Nonempty (Scheme.completedLocalRing
              (pushoutScheme (bridgePushoutSituation hdim hnodal hC)) y ≃+*
            (MvPowerSeries (Fin 2) (Γ(C.subscheme, ⊤) : Type u) ⧸
              Ideal.span {(MvPowerSeries.X 0 :
                              MvPowerSeries (Fin 2) (Γ(C.subscheme, ⊤) : Type u)) *
                            MvPowerSeries.X 1})))

Stacks.Curves.exists_pushout_contraction_bridge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/PushoutContraction.lean, line 326. The attribute's comment: “the pushout Y along C ∩ X' ⟶ Spec k' exists and receives the contraction c : X ⟶ Y”.

The pushout of a rational bridge exists and carries a contraction of the bridge. The pushout square
C ∩ X' ⟶ X'
  ↓        ↓ a
Spec k' ⟶  Y
is [Stacks, Tag 0E25] applied to Stacks.Curves.bridgePushoutSituation, and the contraction is the one produced by Stacks.Curves.exists_contraction_pushoutScheme_bridge.

theorem exists_pushout_contraction_bridge
    (hdim : topologicalKrullDim X = 1)
    (hnodal : HasAtWorstNodalSingularities k X)
    {C : X.IdealSheafData} (hC : IsRationalBridge k X C) :
    ∃ (Y : Scheme.{u}) (c : X ⟶ Y), IsContractionOfRationalBridge hC c

Stacks.Curves.smoothAt_bridge_and_complementaryCurve_of_mem_intersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/SmoothIntersection.lean, line 275. The attribute's comment: “the points of C ∩ X' are smooth points of C and of X'”.

The points of C ∩ X' are smooth points on both C and X'. This is the clause of [Stacks, Tag 0E3M] which the source draws from [Stacks, Tag 0E38] after observing that the points of the intersection are nodes of X: a node has two branches, and here they are the bridge and the closure of the complement, each smooth at the point.

theorem smoothAt_bridge_and_complementaryCurve_of_mem_intersection
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalBridge k X C)
    (w : intersectionWithComplementaryCurve C) :
    InfinitesimalLifting.SmoothAt (C.subschemeι ≫ (X ↘ Spec (.of k)))
        ((Scheme.IdealSheafData.inclusion
          (le_sup_left : C ≤ intersectionWithComplementaryCurveIdeal C)).base w) ∧
      InfinitesimalLifting.SmoothAt (complementaryCurveι C ≫ (X ↘ Spec (.of k)))
        ((Scheme.IdealSheafData.inclusion
          (le_sup_right : complementaryCurveIdeal C ≤
            intersectionWithComplementaryCurveIdeal C)).base w)

Stacks.Curves.isIso_structureSheafToPushforward_and_isZero_rightDerived_one_contraction_bridge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/StructurePushforward.lean, line 249. The attribute's comment: “c_𝒪_X = 𝒪_Y and R¹c_𝒪_X = 0”.

The direct images of 𝒪_X along a contraction of a rational bridge: the canonical map 𝒪_Y ⟶ c_* 𝒪_X is an isomorphism and R ¹ c_* 𝒪_X = 0. This is the clause of [Stacks, Tag 0E3M] that reads "we claim that c_* 𝒪_X = 𝒪_Y and R ¹ c_* 𝒪_X = 0".

theorem isIso_structureSheafToPushforward_and_isZero_rightDerived_one_contraction_bridge
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalBridge k X C)
    {Y : Scheme.{u}} (c : X ⟶ Y) (hc : IsContractionOfRationalBridge hC c) :
    IsIso (structureSheafToPushforward c) ∧
      IsZero (((Scheme.Modules.pushforward c).rightDerived 1).obj (structureSheafModule X))

Tag 0E64, a lemma

Tag 0E64 in the Stacks Project.

AlgebraicGeometry.invertibleCurveDegree_pullback_dualizingSheafOverField_eq_zero_of_isRationalBridge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/DualizingSheafDegree.lean, line 39.

Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k and at-worst-nodal singularities, and let C ⊆ X be a rational bridge. Then deg(ω_X|_C) = 0, where ω_X is invertible by isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities.

theorem invertibleCurveDegree_pullback_dualizingSheafOverField_eq_zero_of_isRationalBridge
    [IsProper (X ↘ Spec (.of k))] (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalBridge k X C) :
    haveI := connectedSpace_of_isIso_globalSections k (X ↘ Spec (.of k))
    letI hω := isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k X hdim
      hnodal
    letI := Stacks.AlgebraicGeometry.Tag09NY.isInvertible_modulePullback C.subschemeι
      (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k))) hω
    invertibleCurveDegree k (C.subschemeι ≫ (X ↘ Spec (.of k)))
        (Stacks.Curves.topologicalKrullDim_subscheme_eq_one_of_isRationalBridge k X hdim hC).le
        ((Scheme.Modules.pullback C.subschemeι).obj
          (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k)))) = 0

Tag 0E65, a lemma

Tag 0E65 in the Stacks Project.

AlgebraicGeometry.exists_iso_sigma_isRationalBridge_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/BaseChange.lean, line 614. The attribute's comment: “CONDITIONALLY -- this is not an unconditional proof of 0E65: the binder hgeom, geometric integrality of the bridge over its field of global functions, is not a hypothesis of the tag. It cannot be discharged, because the tag's conclusion as stated -- a DISJOINT union -- is false without it, refuted by Stacks.Curves.DegenerateConic.not_exists_iso_sigma_isRationalBridge_degenerateConic for the rational bridge V(T₀² + T₁²) of V(T₂(T₀² + T₁²)) ⊂ P²_ℝ. The tag at its own hypotheses, with the disjointness dropped from the conclusion, is proved unconditionally as AlgebraicGeometry.exists_finset_isRationalBridge_baseChange in ContractingRationalBridges/BaseChangeUnion.lean”.

The disjoint decomposition of a geometrically integral rational bridge. Let X be a proper one-dimensional scheme over a field k with H⁰(X, 𝒪_X) = k and at-worst-nodal singularities, and let C ⊆ X be a rational bridge that is geometrically integral over its field of global functions. For every field extension K/k the inverse image of C in X_K is a finite disjoint union of rational bridges of X_K, compatibly with their closed immersions into X_K.

Geometric integrality of the bridge is an extra assumption beyond those of [Stacks, Tag 0E65], and the disjointness of the decomposition is false without it: the module docstring above exhibits the plane curve X = V(T₂(T₀² + T₁²)) ⊂ P²_ℝ whose component C = V(T₀² + T₁²) is a rational bridge with C_ℂ connected and reducible, and Stacks.Curves.DegenerateConic.not_exists_iso_sigma_isRationalBridge_degenerateConic proves that the conclusion below fails for it. So the tag itself is registered on AlgebraicGeometry.exists_finset_isRationalBridge_baseChange, which reaches the scheme-theoretic-union form of the conclusion from the tag's own hypotheses.

public theorem exists_iso_sigma_isRationalBridge_baseChange
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData)
    (hC : IsRationalBridge k X C)
    (hgeom :
      letI : IsIntegral C.subscheme := hC.isIntegral
      letI : Field Γ(C.subscheme, ⊤) :=
        (isField_of_universallyClosed k
          (C.subschemeι ≫ (X ↘ Spec (.of k)))).toField
      GeometricallyIntegral C.subscheme.toSpecΓ) :
    let g : Spec (.of K) ⟶ Spec (.of k) :=
      Spec.map (CommRingCat.ofHom (algebraMap k K))
    let Y := (pullback (X ↘ Spec (.of k)) g : Scheme.{u})
    let p : Y ⟶ X := pullback.fst (X ↘ Spec (.of k)) g
    letI : Y.Over (Spec (.of K)) := ⟨pullback.snd (X ↘ Spec (.of k)) g⟩
    letI : IsProper (Y ↘ Spec (.of K)) :=
      inferInstanceAs (IsProper (pullback.snd (X ↘ Spec (.of k)) g))
    ∃ (ι : Type u) (_ : Finite ι) (D : ι → Y.IdealSheafData)
        (_ : ∀ i, IsRationalBridge K Y (D i))
        (e : (∐ fun i ↦ (D i).subscheme) ≅ (C.comap p).subscheme),
      e.hom ≫ (C.comap p).subschemeι =
        Sigma.desc (fun i ↦ (D i).subschemeι)

AlgebraicGeometry.exists_iso_sigma_isRationalBridge_baseChange_of_perfectField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/BaseChange.lean, line 954. The attribute's comment: “CONDITIONALLY -- this is not an unconditional proof of 0E65: the binder hgeom, geometric integrality of the bridge over its field of global functions, is not a hypothesis of the tag, and [PerfectField k] is not either. Both are inherited from AlgebraicGeometry.exists_iso_sigma_isRationalBridge_baseChange, which this specialises; see the disclosure there. The tag at its own hypotheses, with the disjointness dropped from the conclusion, is proved unconditionally as AlgebraicGeometry.exists_finset_isRationalBridge_baseChange in ContractingRationalBridges/BaseChangeUnion.lean”.

The disjoint decomposition over a perfect ground field. Specialisation of AlgebraicGeometry.exists_iso_sigma_isRationalBridge_baseChange to a perfect k.

The general statement no longer carries the two hypotheses this specialisation was introduced to discharge — geometric reducedness of X over k and separability over k of the field of global functions of the bridge are now derived from nodality for an arbitrary ground field, see the implementation notes above — so nothing beyond perfectness of k separates the two, and the proof is an application. It is kept because it is the form in which the perfect-field case is cited elsewhere.

public theorem exists_iso_sigma_isRationalBridge_baseChange_of_perfectField
    (k K : Type u) [Field k] [PerfectField k] [Field K] [Algebra k K]
    (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData)
    (hC : IsRationalBridge k X C)
    (hgeom :
      letI : IsIntegral C.subscheme := hC.isIntegral
      letI : Field Γ(C.subscheme, ⊤) :=
        (isField_of_universallyClosed k
          (C.subschemeι ≫ (X ↘ Spec (.of k)))).toField
      GeometricallyIntegral C.subscheme.toSpecΓ) :
    let g : Spec (.of K) ⟶ Spec (.of k) :=
      Spec.map (CommRingCat.ofHom (algebraMap k K))
    let Y := (pullback (X ↘ Spec (.of k)) g : Scheme.{u})
    let p : Y ⟶ X := pullback.fst (X ↘ Spec (.of k)) g
    letI : Y.Over (Spec (.of K)) := ⟨pullback.snd (X ↘ Spec (.of k)) g⟩
    letI : IsProper (Y ↘ Spec (.of K)) :=
      inferInstanceAs (IsProper (pullback.snd (X ↘ Spec (.of k)) g))
    ∃ (ι : Type u) (_ : Finite ι) (D : ι → Y.IdealSheafData)
        (_ : ∀ i, IsRationalBridge K Y (D i))
        (e : (∐ fun i ↦ (D i).subscheme) ≅ (C.comap p).subscheme),
      e.hom ≫ (C.comap p).subschemeι =
        Sigma.desc (fun i ↦ (D i).subschemeι)

AlgebraicGeometry.exists_finset_isRationalBridge_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/BaseChangeUnion.lean, line 828. The attribute's comment: “base_change_union”.

[Stacks, Tag 0E65] in the union form. Let X be a proper one-dimensional scheme over a field k with H⁰(X, 𝒪_X) = k and at worst nodal singularities, and let C ⊆ X be a rational bridge. For an arbitrary field extension K/k — no normality, separability, algebraicity or finiteness is assumed — the inverse image of C in the base change X_K is the scheme-theoretic union of a finite set of rational bridges of X_K, namely of the reduced structures on the irreducible components of X_K lying over C.

The tag asserts a disjoint union, which is false; that erratum is recorded at AlgebraicGeometry.exists_iso_sigma_isRationalBridge_baseChange, which proves the disjoint form under the extra hypothesis that the bridge is geometrically integral over its field of global functions k' = Γ(C, 𝒪_C). The dichotomy behind the repair is this: a rational bridge is either geometrically integral over k' — exactly the hypothesis that earlier statement carries, and then C_K really is a disjoint union of [k' ⊗_k K : K]-many bridges — or it acquires precisely two geometric components, meeting in one point and carrying one point of C ∩ X' each. In the second case the two components of C_K meet, so no disjoint decomposition exists, while the union form is still correct and is what this statement proves.

What makes each component come out with complementary degree exactly two is a symmetry: over a separably closed extension the components of C_Ω all have the same image in X and are therefore conjugate, so their complementary degrees agree (Stacks.Curves.finrank_sup_complementaryCurveIdeal_eq_of_image_eq). The counting identity Stacks.Curves.sum_finrank_sup_complementaryCurveIdeal_eq alone does not suffice: it only says that the complementary degrees sum to twice the number of components, which a chain of three components with degrees (1, 4, 1) satisfies just as well.

theorem exists_finset_isRationalBridge_baseChange
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) [X.Over (Spec (.of k))] [IsProper (X ↘ Spec (.of k))]
    (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X)
    (C : X.IdealSheafData) (hC : IsRationalBridge k X C) :
    letI : (pullback (C := Scheme.{u}) (X ↘ Spec (.of k))
        (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}).Over (Spec (.of K)) :=
      ⟨pullback.snd _ _⟩
    letI : IsProper ((pullback (C := Scheme.{u}) (X ↘ Spec (.of k))
        (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}) ↘ Spec (.of K)) :=
      inferInstanceAs (IsProper (pullback.snd (X ↘ Spec (.of k))
        (Spec.map (CommRingCat.ofHom (algebraMap k K)))))
    ∃ Λ : Finset (Set (pullback (C := Scheme.{u}) (X ↘ Spec (.of k))
        (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u})),
      (∀ Z ∈ Λ, IsRationalBridge K (pullback (C := Scheme.{u}) (X ↘ Spec (.of k))
          (Spec.map (CommRingCat.ofHom (algebraMap k K))))
          (Scheme.IdealSheafData.vanishingIdeal
            (TopologicalSpace.Closeds.closure Z))) ∧
        C.comap (pullback.fst (X ↘ Spec (.of k))
            (Spec.map (CommRingCat.ofHom (algebraMap k K))))
          = Λ.inf fun Z => Scheme.IdealSheafData.vanishingIdeal
              (TopologicalSpace.Closeds.closure Z)

Tag 0E3N, a lemma

Tag 0E3N in the Stacks Project.

Stacks.Curves.nonempty_pullback_dualizingSheafOverField_iso_contraction_bridge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/DualizingSheafPullback.lean, line 145.

Let k be a field, let X be a proper scheme over k of dimension one with H⁰(X, 𝒪_X) = k and at-worst-nodal singularities, let C ⊆ X be a rational bridge and let c : X ⟶ Y be the contraction of C, with Y over k through g, compatibly with c. Then c^* ω_Y ≅ ω_X.

theorem nonempty_pullback_dualizingSheafOverField_iso_contraction_bridge
    (hdim : topologicalKrullDim X = 1) (hnodal : HasAtWorstNodalSingularities k X)
    {C : X.IdealSheafData} {hC : IsRationalBridge k X C} {Y : Scheme.{u}} {c : X ⟶ Y}
    (hc : IsContractionOfRationalBridge hC c) (g : Y ⟶ Spec (.of k))
    (hcg : c ≫ g = X ↘ Spec (.of k)) :
    haveI := isProper_structureMorphism_of_isContractionOfRationalBridge hdim hnodal hc hcg
    Nonempty ((Scheme.Modules.pullback c).obj (Stacks.Duality.dualizingSheafOverField g) ≅
      Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k)))

Tag 0E3P, a lemma

Tag 0E3P in the Stacks Project.

AlgebraicGeometry.isAmple_dualizingSheafOverField_of_hasAtWorstNodalSingularities, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/DualizingAmple.lean, line 41.

Let k be a field and let X be a proper scheme over k of dimension one with H⁰(X, 𝒪_X) = k. If the singularities of X are at worst nodal, X has no rational tail and no rational bridge, and the genus of X is at least two, then ω_X is an invertible 𝒪_X-module and it is ample.

theorem isAmple_dualizingSheafOverField_of_hasAtWorstNodalSingularities
    (k : Type u) [Field k] (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [IsProper (X ↘ Spec (.of k))] (hdim : topologicalKrullDim X = 1)
    [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X ↘ Spec (.of k)).appTop)]
    (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X)
    (htail : ∀ C : X.IdealSheafData, ¬ IsRationalTail k X C)
    (hbridge : ∀ C : X.IdealSheafData, ¬ IsRationalBridge k X C)
    (hg : 2 ≤ genus (X ↘ Spec (.of k))) :
    ∃ _ : SheafOfModules.IsInvertible X.toRingedSpace.presheaf
        (structureSheafRing X.toRingedSpace).property
        (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k))),
      Scheme.Modules.IsAmple X (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k)))

Tag 0E3Q, a lemma

Tag 0E3Q in the Stacks Project.

AlgebraicGeometry.IsIteratedContractionOfRationalBridges.isStableContraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/Terminal.lean, line 270. The attribute's comment: “ω_{X'} is ample”.

Stacks Project, Tag 0E3Q: ω_{X'} is ample. Let X be a proper scheme over a field k of dimension one with H⁰(X, 𝒪_X) = k, genus g ≥ 2, at-worst-nodal singularities and no rational tails, and let c : X ⟶ X' be the composite of a sequence of contractions of rational bridges (Tag 0E3M) such that X' has no rational bridge. Then ω_{X'} is invertible and ample; more precisely c satisfies the conditions of Tag 0E7Q: X' is proper of dimension one with at-worst-nodal singularities, 𝒪_{X'} = c_* 𝒪_X, R¹ c_* 𝒪_X = 0, and ω_{X'} is ample.

The target has no rational tails (Stacks.Curves.forall_not_isRationalTail_of_pullback_dualizingSheafOverField_iso, from c^* ω_{X'} ≅ ω_X), so Tag 0E3P applies to it.

theorem isStableContraction
    (htail : letI : X.Over (Spec (.of k)) := ⟨fX⟩
      ∀ C : X.IdealSheafData, ¬ IsRationalTail k X C)
    (hg : 2 ≤ genus fX)
    (hterminal : ∀ C : Y.IdealSheafData,
      letI : Y.Over (Spec (.of k)) := ⟨fY⟩
      ∀ _ : IsProper (Y ↘ Spec (.of k)), ¬ IsRationalBridge k Y C) :
    Stacks.Curves.StableModel.IsStableContraction fX fY c

AlgebraicGeometry.IsIteratedContractionOfRationalBridges.existsUnique_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/Terminal.lean, line 309. The attribute's comment: “the morphism X ⟶ X' is independent of choices”.

Stacks Project, Tag 0E3Q: the morphism X ⟶ X' is independent of choices. Under the hypotheses of AlgebraicGeometry.IsIteratedContractionOfRationalBridges.isStableContraction, if c₂ : X ⟶ X'₂ is the composite of a second sequence of contractions of rational bridges such that X'₂ has no rational bridge, then there is a unique isomorphism e : X' ≅ X'₂ with c ≫ e.hom = c₂. Both composites are stable contractions pulling the dualizing sheaves back to ω_X (Tag 0E3N along each chain), so Stacks.Curves.StableModel.existsUnique_iso_of_pullback_dualizingSheafOverField_iso applies.

theorem existsUnique_iso
    (htail : letI : X.Over (Spec (.of k)) := ⟨fX⟩
      ∀ C : X.IdealSheafData, ¬ IsRationalTail k X C)
    (hg : 2 ≤ genus fX)
    (hterminal : ∀ C : Y.IdealSheafData,
      letI : Y.Over (Spec (.of k)) := ⟨fY⟩
      ∀ _ : IsProper (Y ↘ Spec (.of k)), ¬ IsRationalBridge k Y C)
    {Y₂ : Scheme.{u}} {fY₂ : Y₂ ⟶ Spec (.of k)} {c₂ : X ⟶ Y₂}
    (hseq₂ : IsIteratedContractionOfRationalBridges k fX fY₂ c₂)
    (hterminal₂ : ∀ C : Y₂.IdealSheafData,
      letI : Y₂.Over (Spec (.of k)) := ⟨fY₂⟩
      ∀ _ : IsProper (Y₂ ↘ Spec (.of k)), ¬ IsRationalBridge k Y₂ C) :
    ∃! e : Y ≅ Y₂, c ≫ e.hom = c₂

AlgebraicGeometry.IsIteratedContractionOfRationalBridges.existsUnique_iso_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ContractingRationalBridges/TerminalBaseChange.lean, line 239. The attribute's comment: “formation of the morphism X ⟶ X' commutes with base field extensions”.

Formation of the contraction c : X ⟶ Y commutes with base field extensions: under the hypotheses of AlgebraicGeometry.IsIteratedContractionOfRationalBridges.isStableContraction, let K/k be a field extension, X_K = X ×_k K and Y_K = Y ×_k K over K, and c_K : X_K ⟶ Y_K the base change of c. For every sequence d : X_K ⟶ Z of contractions of rational bridges of X_K over K such that Z has no rational bridge, there is a unique isomorphism e : Y_K ≅ Z with c_K ≫ e.hom = d: the morphism the construction produces for X_K is the base change of the one for X.

theorem existsUnique_iso_baseChange
    (htail : letI : X.Over (Spec (.of k)) := ⟨fX⟩
      ∀ C : X.IdealSheafData, ¬ IsRationalTail k X C)
    (hg : 2 ≤ genus fX)
    (hterminal : ∀ C : Y.IdealSheafData,
      letI : Y.Over (Spec (.of k)) := ⟨fY⟩
      ∀ _ : IsProper (Y ↘ Spec (.of k)), ¬ IsRationalBridge k Y C)
    (K : Type u) [Field K] [Algebra k K] {Z : Scheme.{u}} {fZ : Z ⟶ Spec (.of K)}
    {d : pullback fX (Spec.map (CommRingCat.ofHom (algebraMap k K))) ⟶ Z}
    (hd : IsIteratedContractionOfRationalBridges K
      (pullback.snd fX (Spec.map (CommRingCat.ofHom (algebraMap k K)))) fZ d)
    (hdterminal : ∀ C : Z.IdealSheafData,
      letI : Z.Over (Spec (.of K)) := ⟨fZ⟩
      ∀ _ : IsProper (Z ↘ Spec (.of K)), ¬ IsRationalBridge K Z C) :
    ∃! e : pullback fY (Spec.map (CommRingCat.ofHom (algebraMap k K))) ≅ Z,
      pullback.map fX (Spec.map (CommRingCat.ofHom (algebraMap k K))) fY
          (Spec.map (CommRingCat.ofHom (algebraMap k K))) c (𝟙 _) (𝟙 _)
          (by rw [Category.comp_id, hseq.comp_structureMorphism]) (by simp) ≫ e.hom = d

Sources

LeanAlgebraicGeometry.IsRationalBridge · Stacks.Curves.exists_isProper_structureMorphism_and_genus_eq_contraction_bridge · Stacks.Curves.hasAtWorstNodalSingularities_pushoutScheme_bridge · Stacks.Curves.isField_globalSections_bridge · Stacks.Curves.isNode_of_mem_intersection_bridge · Stacks.Curves.moduleFinite_and_isSeparable_globalSections_bridge · Stacks.Curves.isField_and_isSeparable_or_algEquiv_prod_intersectionSections_bridge · Stacks.Curves.exists_ringEquiv_completedLocalRing_contraction_bridge

Section53.25 Contracting to a stable curve #

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

Tag 0E7N, the section

Tag 0E7N in the Stacks Project.

Stacks.Curves.StableModel.exists_isStableContraction_comp_tails_bridges, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/StableContraction/StableModelCharacterization.lean, line 106.

Stacks Project, Tag 0E7N: contracting to a stable curve. Let X be a proper scheme over a field k of dimension one with H⁰(X, 𝒪_X) = k, genus g ≥ 2 and at-worst-nodal singularities. Contract rational tails until none are left, t : X ⟶ X₁ ([Stacks, Tag 0E3L]), and then rational bridges until none are left, d : X₁ ⟶ Y ([Stacks, Tag 0E3Q]). The composite c = t ≫ d is a morphism over k such that Y is proper over k of dimension one with at-worst-nodal singularities, H⁰(Y, 𝒪_Y) = k, Y has genus g, 𝒪_Y = c_*𝒪_X, R¹c_*𝒪_X = 0, and ω_Y is ample. These conditions characterize c ([Stacks, Tag 0E7Q]): any c' : X ⟶ Y' satisfying the conditions of IsStableContraction is related to c by exactly one isomorphism e : Y ≅ Y' with c ≫ e.hom = c'.

theorem exists_isStableContraction_comp_tails_bridges (f : X ⟶ Spec (.of k)) [IsProper f]
    (hdim : topologicalKrullDim X = 1) [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop)]
    (hgenus : 2 ≤ genus f)
    (hnodal : letI : X.Over (Spec (.of k)) := ⟨f⟩
      Stacks.Curves.HasAtWorstNodalSingularities k X) :
    ∃ (X₁ : Scheme.{u}) (f₁ : X₁ ⟶ Spec (.of k)) (t : X ⟶ X₁) (Y : Scheme.{u})
      (gY : Y ⟶ Spec (.of k)) (d : X₁ ⟶ Y),
      IsIteratedContractionOfRationalTails k f f₁ t ∧
      (∀ C : X₁.IdealSheafData, ¬ @IsRationalTail k _ X₁ ⟨f₁⟩ C) ∧
      IsIteratedContractionOfRationalBridges k f₁ gY d ∧
      (∀ C : Y.IdealSheafData,
        letI : Y.Over (Spec (.of k)) := ⟨gY⟩
        ∀ _ : IsProper (Y ↘ Spec (.of k)), ¬ IsRationalBridge k Y C) ∧
      IsStableContraction f gY (t ≫ d) ∧
      IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ gY.appTop) ∧
      genus gY = genus f ∧
      ∀ (Y' : Scheme.{u}) (gY' : Y' ⟶ Spec (.of k)) (c' : X ⟶ Y'),
        IsStableContraction f gY' c' → ∃! e : Y ≅ Y', (t ≫ d) ≫ e.hom = c'

Tag 0E7P, a lemma

Tag 0E7P in the Stacks Project.

Stacks.Curves.DualizingPullback.nonempty_pullback_dualizingSheafOverField_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/StableContraction/DualizingPullbackGorenstein.lean, line 53. The attribute's comment: “Stated for m ≥ 1. For m ≤ 0 the statement fails: let X = V(xy) ⊆ ℙ²_k and let c contract one line C to a point. Then (1)–(3) hold with m = 0 (and with m = -1), but ω_X|_C ≅ 𝒪_C(-1) while (c^*ω_Y)|_C ≅ 𝒪_C.”.

Stacks Project, Tag 0E7P. Let c : X ⟶ Y be a morphism of proper schemes over a field k with 𝒪_Y = c_*𝒪_X and R^1 c_*𝒪_X = 0, where X and Y are reduced, Gorenstein and of dimension one. If H^1(X, ω_X^{⊗ m}) = 0 and ω_X^{⊗ m} is globally generated for some m ≥ 1, then c^*ω_Y ≅ ω_X.

theorem nonempty_pullback_dualizingSheafOverField_iso
    (c : X ⟶ Y) (g : Y ⟶ Spec (.of k)) [IsProper (c ≫ g)] [IsProper g]
    (hO : IsIso (SheafOfModules.unitToPushforwardObjUnit c.toRingCatSheafHom))
    (hR1 : IsZero (((Scheme.Modules.pushforward c).rightDerived 1).obj
      (SheafOfModules.unit X.ringCatSheaf)))
    [IsReduced X] [IsReduced Y] [IsGorenstein X] [IsGorenstein Y]
    (hdimX : topologicalKrullDim X = 1) (hdimY : topologicalKrullDim Y = 1)
    (m : ℕ) (hm : 1 ≤ m)
    (hH1 : IsZero (cohomologyOverField k (c ≫ g)
      (tensorSheafNPow X.toRingedSpace (dualizingSheafOverField (c ≫ g)) m) 1))
    (hgen : SheafOfModules.IsGeneratedByGlobalSections
      (tensorSheafNPow X.toRingedSpace (dualizingSheafOverField (c ≫ g)) m : X.Modules)) :
    Nonempty ((Scheme.Modules.pullback c).obj (dualizingSheafOverField g) ≅
      dualizingSheafOverField (c ≫ g))

Tag 0E7Q, a lemma

Tag 0E7Q in the Stacks Project.

Stacks.Curves.StableModel.existsUnique_isStableContraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/StableContraction/StableModelCharacterization.lean, line 84. The attribute's comment: “Condition (3) includes that ω_Y is invertible, as ampleness is defined for invertible modules. Uniqueness up to unique isomorphism: any two such morphisms are related by exactly one isomorphism of targets under X.”.

Stacks Project, Tag 0E7Q. Let X be a proper scheme over a field k of dimension one with H⁰(X, 𝒪_X) = k, genus g ≥ 2 and at-worst-nodal singularities. There is a morphism c : X ⟶ Y of schemes over k such that 1. Y is proper over k, dim Y = 1, and Y has at-worst-nodal singularities, 2. 𝒪_Y = c_*𝒪_X and R¹c_*𝒪_X = 0, and 3. ω_Y is ample on Y

(IsStableContraction f gY c), and it is unique up to unique isomorphism: any two such c : X ⟶ Y, c' : X ⟶ Y' are related by exactly one isomorphism e : Y ≅ Y' with c ≫ e = c'.

theorem existsUnique_isStableContraction (f : X ⟶ Spec (.of k)) [IsProper f]
    (hdim : topologicalKrullDim X = 1) [IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop)]
    (hgenus : 2 ≤ genus f)
    (hnodal : letI : X.Over (Spec (.of k)) := ⟨f⟩
      Stacks.Curves.HasAtWorstNodalSingularities k X) :
    (∃ (Y : Scheme.{u}) (gY : Y ⟶ Spec (.of k)) (c : X ⟶ Y), IsStableContraction f gY c) ∧
      ∀ (Y Y' : Scheme.{u}) (gY : Y ⟶ Spec (.of k)) (gY' : Y' ⟶ Spec (.of k)) (c : X ⟶ Y)
        (c' : X ⟶ Y'), IsStableContraction f gY c → IsStableContraction f gY' c' →
        ∃! e : Y ≅ Y', c ≫ e.hom = c'

Tag 0E8X, a lemma

Tag 0E8X in the Stacks Project.

AlgebraicGeometry.isRelativelyVeryAmple_tensorPower_three_dualizingSheafOverField_and_isZero_cohomology_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/StableContraction/TricanonicalVeryAmple.lean, line 291.

Stacks Project, Tag 0E8X. Let X be a proper scheme of dimension one over a field k with H⁰(X, 𝒪_X) = k, of genus g ≥ 2, with at-worst-nodal singularities, and assume the dualizing sheaf ω_X is ample. Then ω_X^{⊗ 3} is very ample and H¹(X, ω_X^{⊗ 3}) = 0.

ω_X is invertible since X is Gorenstein ([Stacks, Tag 0E37]). X has no rational tail, so ω_X^{⊗ 3} is globally generated ([Stacks, Tag 0E3K]); its sections define a morphism to projective space, which is a closed immersion once it is one after base change to k̄ ([Stacks, Tag 02L6]). Over k̄ the base change is again nodal of genus g with ample dualizing sheaf the pullback of ω_X ([Stacks, Tag 0E32]), and H¹(ℐ_Z ω^{⊗ 3}) = 0 for every degree-two Z gives the criterion of [Stacks, Tag 0E8T].

theorem isRelativelyVeryAmple_tensorPower_three_dualizingSheafOverField_and_isZero_cohomology_one
    (hdim : topologicalKrullDim X = 1) (hg : 2 ≤ genus (X ↘ Spec (.of k)))
    (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X)
    (hω : haveI := connectedSpace_of_isIso_globalSections k (X ↘ Spec (.of k))
      letI := isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k X hdim hnodal
      Scheme.Modules.IsAmple X (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k)))) :
    haveI := connectedSpace_of_isIso_globalSections k (X ↘ Spec (.of k))
    letI := isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k X hdim hnodal
    Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple (X ↘ Spec (.of k))
        (Stacks.SheafOfModules.Invertible.tensorPower X.presheaf X.ringCatSheaf.2
          (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k))) 3) ∧
      IsZero (cohomologyOverField k (X ↘ Spec (.of k))
        (Stacks.SheafOfModules.Invertible.tensorPower X.presheaf X.ringCatSheaf.2
          (Stacks.Duality.dualizingSheafOverField (X ↘ Spec (.of k))) 3) 1)

Sources

LeanStacks.Curves.StableModel.exists_isStableContraction_comp_tails_bridges · Stacks.Curves.DualizingPullback.nonempty_pullback_dualizingSheafOverField_iso · Stacks.Curves.StableModel.existsUnique_isStableContraction · AlgebraicGeometry.isRelativelyVeryAmple_tensorPower_three_dualizingSheafOverField_and_isZero_cohomology_one

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

53.15 Glueing and squishing to 53.25 Contracting to a stable…

Section53.15 Glueing and squishing#

Tag 0C1I, a lemma

Tag 0C1J, an example

Tag 0C1K, an example

Tag 0C1L, a lemma

Tag 0C1M, a lemma

Tag 0C1N, a lemma

Sources

Section53.16 Multicross and nodal singularities#

Tag 0C1U, an equation

Tag 0C1V, a lemma

Tag 0C1W, a definition

Tag 0C1X, a lemma

Tag 0CDZ, a lemma

Sources

Section53.17 Torsion in the Picard group#

Tag 0C1Z, a lemma

Tag 0CDU, a lemma

Tag 0C20, a proposition

Sources

Section53.18 Genus versus geometric genus#

Tag 0CE0, the section

Tag 0CE1, a lemma

Tag 0CE2, a lemma

Tag 0CE3, a lemma

Tag 0CE4, a lemma

Tag 0CE5, a lemma

Tag 0CE6, a lemma

Sources

Section53.19 Nodal curves#

Tag 0C47, a definition

Tag 0C48, a lemma

Tag 0C49, a lemma

Tag 0C4A, a lemma

Tag 0C4B, a lemma

Tag 0C4C, a lemma

Tag 0C4D, a lemma

Tag 0CBT, a remark

Tag 0CBU, a remark

Tag 0CBV, a definition

Tag 0CBW, a lemma

Tag 0C56, a lemma

Tag 0C57, a lemma

Tag 0CD6, a lemma

Tag 0C4E, a lemma

Tag 0E37, a lemma

Tag 0E38, a lemma

Sources

Section53.20 Families of nodal curves#

Tag 0C59, a lemma

Tag 0C5A, a definition

Tag 0CD7, a lemma

Tag 0C5B, a lemma

Tag 0DSC, a lemma

Tag 0C5C, a lemma

Tag 0CD8, a lemma

Tag 0C5D, a lemma

Tag 0C5E, a lemma

Tag 0C5F, a lemma

Tag 0CBX, a lemma

Tag 0GKA, a lemma

Sources

Section53.21 Étale local structure of nodal families#

Tag 0CBY, a lemma

Sources

Section53.22 More vanishing results#

Tag 0E3A, a lemma

Tag 0E3B, a lemma

Tag 0E3C, a lemma

Tag 0E3D, a lemma

Tag 0H2V, a lemma

Tag 0E3E, a lemma

Tag 0E3F, a lemma

Sources

Section53.23 Contracting rational tails#

Tag 0E3H, an example

Tag 0E63, a lemma

Tag 0E3I, a lemma

Tag 0E3J, a lemma

Section53.15 Glueing and squishing #

Section53.16 Multicross and nodal singularities #

Section53.17 Torsion in the Picard group #

Section53.18 Genus versus geometric genus #

Section53.19 Nodal curves #

Section53.20 Families of nodal curves #

Section53.21 Étale local structure of nodal families #

Section53.22 More vanishing results #

Section53.23 Contracting rational tails #

Section53.24 Contracting rational bridges #

Section53.25 Contracting to a stable curve #