33.39 The delta invariant to 33.48 Enriques-Severi-Zariski

Section33.39 The delta invariant#

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

Tag 0C3R, a lemma

Tag 0C3R in the Stacks Project.

IsLocalRing.radical_span_eq_maximalIdeal_iff_notMem_minimalPrimes, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Parameters.lean, line 121. The attribute's comment: “parts (1) and (2)”.

An element of the maximal ideal of a one-dimensional Noetherian local ring cuts out the closed point exactly when it is in no minimal prime.

public lemma radical_span_eq_maximalIdeal_iff_notMem_minimalPrimes
    {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (hdim : ringKrullDim A = 1) {f : A} (hf : f ∈ maximalIdeal A) :
    (Ideal.span {f}).radical = maximalIdeal A ↔
      ∀ p ∈ minimalPrimes A, f ∉ p

IsLocalRing.notMem_minimalPrimes_iff_localizationAway_equiv_pi_localizationAtPrime, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Parameters.lean, line 160. The attribute's comment: “parts (2) and (3)”.

Avoiding all minimal primes is equivalent to localization away from the element being the product of the local rings at the minimal primes.

public lemma notMem_minimalPrimes_iff_localizationAway_equiv_pi_localizationAtPrime
    {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (hdim : ringKrullDim A = 1) {f : A} (hf : f ∈ maximalIdeal A) :
    (∀ p ∈ minimalPrimes A, f ∉ p) ↔
      Nonempty (Localization.Away f ≃ₐ[A]
        (∀ p : minimalPrimes A,
          @Localization.AtPrime A _ p.1 p.2.1.1))

IsLocalRing.exists_radical_span_eq_maximalIdeal, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Parameters.lean, line 217. The attribute's comment: “existence”.

A one-dimensional Noetherian local ring has an element of its maximal ideal whose principal ideal has radical equal to the maximal ideal.

public lemma exists_radical_span_eq_maximalIdeal
    {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (hdim : ringKrullDim A = 1) :
    ∃ f ∈ maximalIdeal A, (Ideal.span {f}).radical = maximalIdeal A

IsLocalRing.notMem_minimalPrimes_iff_mem_nonZeroDivisors_of_depth_eq_one, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Parameters.lean, line 226. The attribute's comment: “part (4)”.

At depth one, the elements avoiding all minimal primes are precisely the nonzerodivisors.

public lemma notMem_minimalPrimes_iff_mem_nonZeroDivisors_of_depth_eq_one
    {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (hdim : ringKrullDim A = 1) (hdepth : Module.depth A (maximalIdeal A) A = 1) (f : A) :
    (∀ p ∈ minimalPrimes A, f ∉ p) ↔ f ∈ nonZeroDivisors A

IsLocalRing.notMem_minimalPrimes_iff_localizationAway_equiv_fractionRing_of_depth_eq_one, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Parameters.lean, line 239. The attribute's comment: “part (5)”.

At depth one, avoiding all minimal primes is equivalent to localization away from the element being the total ring of fractions.

public lemma notMem_minimalPrimes_iff_localizationAway_equiv_fractionRing_of_depth_eq_one
    {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (hdim : ringKrullDim A = 1) (hdepth : Module.depth A (maximalIdeal A) A = 1)
    {f : A} (hf : f ∈ maximalIdeal A) :
    (∀ p ∈ minimalPrimes A, f ∉ p) ↔
      Nonempty (Localization.Away f ≃ₐ[A] FractionRing A)

IsLocalRing.depth_eq_one_of_isReduced, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Parameters.lean, line 276. The attribute's comment: “reduced rings have depth one”.

A reduced one-dimensional Noetherian local ring has depth one.

public lemma depth_eq_one_of_isReduced
    {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [IsReduced A]
    (hdim : ringKrullDim A = 1) :
    Module.depth A (maximalIdeal A) A = 1

IsLocalRing.notMem_minimalPrimes_iff_localizationAway_equiv_pi_residueField_of_isReduced, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Parameters.lean, line 292. The attribute's comment: “part (6)”.

In a reduced one-dimensional Noetherian local ring, avoiding all minimal primes is equivalent to localization away from the element being the product of the residue fields at the minimal primes.

public lemma notMem_minimalPrimes_iff_localizationAway_equiv_pi_residueField_of_isReduced
    {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [IsReduced A]
    (hdim : ringKrullDim A = 1) {f : A} (hf : f ∈ maximalIdeal A) :
    (∀ p ∈ minimalPrimes A, f ∉ p) ↔
      Nonempty (Localization.Away f ≃ₐ[A]
        (∀ p : minimalPrimes A, @Ideal.ResidueField A _ p.1 p.2.1.1))
Tag 0C3S, a lemma

Tag 0C3S in the Stacks Project.

isNormalRing_integralClosure_fractionRing, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Normalization.lean, line 149. The attribute's comment: “normality”. References: EGA II (7.4.6), “affine case, 𝒜=R(X)”.

The integral closure of a reduced Noetherian ring in its total ring of fractions is a normal ring.

public lemma isNormalRing_integralClosure_fractionRing
    {A : Type*} [CommRing A] [IsNoetherianRing A] [IsReduced A] :
    IsNormalRing ↥(integralClosure A (FractionRing A))

module_finite_integralClosure_fractionRing, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Normalization.lean, line 178. The attribute's comment: “finiteness”. References: EGA IV (7.6.1), “more general”.

The integral closure of a reduced Nagata ring in its total ring of fractions is finite over the original ring.

public lemma module_finite_integralClosure_fractionRing
    {A : Type*} [CommRing A] [IsReduced A]
    (hA : IsNagataRing A) :
    Module.Finite A ↥(integralClosure A (FractionRing A))

isNagataRing_integralClosure_fractionRing, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Normalization.lean, line 189. The attribute's comment: “Nagata”. References: EGA IV (7.8.3), “(vii)”.

The integral closure of a reduced Nagata ring in its total ring of fractions is Nagata.

public lemma isNagataRing_integralClosure_fractionRing
    {A : Type*} [CommRing A] [IsReduced A]
    (hA : IsNagataRing A) :
    IsNagataRing ↥(integralClosure A (FractionRing A))

isFiniteLength_integralClosure_quotient, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Normalization.lean, line 202. The attribute's comment: “finite length”. References: EGA IV (7.6.1), “finiteness of A' over A”; EGA IV (7.8.3), “(vii), special case”.

For a reduced one-dimensional Nagata local ring, the quotient of its integral closure in the total ring of fractions by the original ring has finite length.

public lemma isFiniteLength_integralClosure_quotient
    {A : Type*} [CommRing A] [IsLocalRing A] [IsReduced A]
    (hA : IsNagataRing A) (hdim : ringKrullDim A = 1) :
    IsFiniteLength A
      (↥(integralClosure A (FractionRing A)) ⧸
        LinearMap.range (Algebra.linearMap A ↥(integralClosure A (FractionRing A))))
Tag 0C3T, a definition

Tag 0C3T in the Stacks Project.

Ring.deltaInvariant, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Defs.lean, line 31. References: SGA 7 X (2.10).

The delta invariant of a commutative ring is the length of the quotient of its integral closure in its total ring of fractions by the image of the ring. For a reduced one-dimensional Nagata local ring, this quotient has finite length.

public noncomputable abbrev Ring.deltaInvariant (A : Type*) [CommRing A] : ℕ∞
Tag 0C3U, a lemma

Tag 0C3U in the Stacks Project.

Ring.deltaInvariant_eq_zero_iff_isDiscreteValuationRing, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Vanishing.lean, line 66.

A reduced one-dimensional Nagata local ring has delta invariant zero if and only if it is a discrete valuation ring.

public lemma deltaInvariant_eq_zero_iff_isDiscreteValuationRing
    {A : Type*} [CommRing A] [IsLocalRing A] [IsReduced A]
    (hA : IsNagataRing A) (hdim : ringKrullDim A = 1) :
    deltaInvariant A = 0 ↔ ∃ _ : IsDomain A, IsDiscreteValuationRing A
Tag 0C3V, a lemma

Tag 0C3V in the Stacks Project.

IsLocalRing.isReduced_adicCompletion_maximalIdeal_of_isNagataRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Completion.lean, line 55. The attribute's comment: “completion_properties”. References: EGA IV (7.6.1), “more general”.

The maximal-ideal-adic completion of a reduced Nagata local ring is reduced.

public theorem isReduced_adicCompletion_maximalIdeal_of_isNagataRing
    {A : Type*} [CommRing A] [IsLocalRing A] [IsReduced A]
    (hA : IsNagataRing A) : IsReduced (AdicCompletion (maximalIdeal A) A)

IsLocalRing.isNagataRing_adicCompletion_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Completion.lean, line 63. The attribute's comment: “completion_properties”.

The maximal-ideal-adic completion of a Noetherian local ring is a Nagata ring.

public theorem isNagataRing_adicCompletion_maximalIdeal
    {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] :
    IsNagataRing (AdicCompletion (maximalIdeal A) A)

IsLocalRing.ringKrullDim_adicCompletion_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Completion.lean, line 70. The attribute's comment: “completion_properties”. References: EGA IV (7.3.19), “dim(Â) = 1”.

Completion of a Noetherian local ring at its maximal ideal preserves Krull dimension.

public theorem ringKrullDim_adicCompletion_maximalIdeal
    {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] :
    ringKrullDim (AdicCompletion (maximalIdeal A) A) = ringKrullDim A

IsLocalRing.IsHenselization.isReduced, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Henselization.lean, line 376. The attribute's comment: “henselization_properties”. References: EGA IV (18.6.9), “(i), special case”.

The henselization of a reduced local ring is reduced.

public lemma isReduced [IsReduced A] : IsReduced Ah

IsLocalRing.IsHenselization.isNagataRing, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Henselization.lean, line 383. The attribute's comment: “henselization_properties”. References: EGA IV (18.7.3), “Forward implication”.

The henselization of a Nagata local ring is Nagata.

public lemma isNagataRing (hNagata : IsNagataRing A) : IsNagataRing Ah

IsLocalRing.IsHenselization.ringKrullDim_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Henselization.lean, line 399. The attribute's comment: “henselization_properties”.

Henselization preserves the Krull dimension of a local ring.

public lemma ringKrullDim_eq : ringKrullDim Ah = ringKrullDim A

IsLocalRing.strictHenselization_isReduced, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Henselization.lean, line 413. The attribute's comment: “strict_henselization_properties”. References: EGA IV (18.8.12), “(i)”.

A strict henselization of a reduced local ring is reduced.

public lemma strictHenselization_isReduced
    (ksep : Type v) [Field ksep] [Algebra (IsLocalRing.ResidueField A) ksep]
    [IsSepClosure (IsLocalRing.ResidueField A) ksep]
    [IsLocalRing.IsHenselization A ksep Ash] [IsReduced A] : IsReduced Ash

IsLocalRing.strictHenselization_isNagataRing, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Henselization.lean, line 433. The attribute's comment: “strict_henselization_properties”.

A strict henselization of a Nagata local ring is Nagata.

public lemma strictHenselization_isNagataRing
    (ksep : Type v) [Field ksep] [Algebra (IsLocalRing.ResidueField A) ksep]
    [IsSepClosure (IsLocalRing.ResidueField A) ksep]
    [IsLocalRing.IsHenselization A ksep Ash]
    (hA : IsNagataRing A) : IsNagataRing Ash

IsLocalRing.strictHenselization_ringKrullDim, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Henselization.lean, line 458. The attribute's comment: “strict_henselization_properties”. References: SGA 5 I (3.1.3), “more general”.

A local ring and a strict henselization of it have the same Krull dimension.

public lemma strictHenselization_ringKrullDim
    (ksep : Type v) [Field ksep] [Algebra (IsLocalRing.ResidueField A) ksep]
    [IsSepClosure (IsLocalRing.ResidueField A) ksep]
    [IsLocalRing.IsHenselization A ksep Ash] : ringKrullDim Ash = ringKrullDim A

IsLocalRing.exists_fractionRing_map_and_tensorProduct_range_eq_integralClosure_completion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/IntegralClosureCompletion.lean, line 89. The attribute's comment: “completion_integral_closure”.

The base change to the completion of the integral closure of a reduced one-dimensional Nagata local ring in its total ring of fractions is the integral closure of the completion in its total ring of fractions.

public lemma exists_fractionRing_map_and_tensorProduct_range_eq_integralClosure_completion
    {A : Type u} [CommRing A] [IsLocalRing A] [IsReduced A]
    (hA : IsNagataRing A) (hdim : ringKrullDim A = 1) :
    let B := AdicCompletion (maximalIdeal A) A
    ∃ q : FractionRing A →ₐ[A] FractionRing B,
      ∃ g : (integralClosure A (FractionRing A) ⊗[A] B) →ₐ[A] FractionRing B,
        Function.Injective g ∧
          g.range = (integralClosure B (FractionRing B)).restrictScalars A ∧
          g.comp
              (Algebra.TensorProduct.includeLeft :
                integralClosure A (FractionRing A) →ₐ[A]
                  (integralClosure A (FractionRing A) ⊗[A] B)) =
            q.comp (integralClosure A (FractionRing A)).val ∧
          g.comp
              (Algebra.TensorProduct.includeRight :
                B →ₐ[A] (integralClosure A (FractionRing A) ⊗[A] B)) =
            IsScalarTower.toAlgHom A B (FractionRing B)

IsLocalRing.tensorProduct_integralClosure_isIntegralClosure_strictHenselization, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/IntegralClosureHenselization.lean, line 190. The attribute's comment: “strict_henselization_integral_closure”.

Stacks Project, Tag 0C3V. After strict henselization, the base change of the integral closure in the total ring of fractions is the integral closure in the new total ring of fractions.

public lemma tensorProduct_integralClosure_isIntegralClosure_strictHenselization
    {A Ash : Type u} [CommRing A] [IsLocalRing A] [IsReduced A]
    [CommRing Ash] [IsLocalRing Ash] [Algebra A Ash]
    (K : Type v) [Field K] [Algebra (ResidueField A) K]
    [IsSepClosure (ResidueField A) K] [IsHenselization A K Ash]
    (hA : IsNagataRing A) (hdim : ringKrullDim A = 1) :
    ∃ q : FractionRing A →ₐ[A] FractionRing Ash,
      ∃ g : (integralClosure A (FractionRing A) ⊗[A] Ash) →ₐ[A] FractionRing Ash,
        Function.Injective g ∧
          g.range = (integralClosure Ash (FractionRing Ash)).restrictScalars A ∧
          g.comp (Algebra.TensorProduct.includeLeft :
            integralClosure A (FractionRing A) →ₐ[A]
              (integralClosure A (FractionRing A) ⊗[A] Ash)) =
              q.comp (integralClosure A (FractionRing A)).val ∧
          g.comp (Algebra.TensorProduct.includeRight :
            Ash →ₐ[A] (integralClosure A (FractionRing A) ⊗[A] Ash)) =
              IsScalarTower.toAlgHom A Ash (FractionRing Ash)

IsLocalRing.exists_integralClosure_henselization_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/IntegralClosureHenselization.lean, line 266. The attribute's comment: “henselization_integral_closure”.

Stacks Project, Tag 0C3V. The base change to a henselization of the integral closure in the total ring of fractions is the integral closure of the henselization in its total ring of fractions.

public theorem exists_integralClosure_henselization_map
    (hA : IsNagataRing A) (hdim : ringKrullDim A = 1) :
    ∃ q : FractionRing A →ₐ[A] FractionRing Ah,
      ∃ g : (integralClosure A (FractionRing A) ⊗[A] Ah) →ₐ[A] FractionRing Ah,
        Function.Injective g ∧
          g.range = (integralClosure Ah (FractionRing Ah)).restrictScalars A ∧
          g.comp (Algebra.TensorProduct.includeLeft :
            integralClosure A (FractionRing A) →ₐ[A]
              (integralClosure A (FractionRing A) ⊗[A] Ah)) =
              q.comp (integralClosure A (FractionRing A)).val ∧
          g.comp (Algebra.TensorProduct.includeRight :
            Ah →ₐ[A] (integralClosure A (FractionRing A) ⊗[A] Ah)) =
              IsScalarTower.toAlgHom A Ah (FractionRing Ah)

Declarations registered for the tag:

Tag 0C3W, a lemma

Tag 0C3W in the Stacks Project.

Stacks.Curves.deltaInvariant_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/BaseChangeDelta.lean, line 206. The attribute's comment: “henselization”.

Henselization preserves the delta invariant of a reduced one-dimensional Nagata local ring.

public theorem deltaInvariant_henselization
    (A Ah : Type u) [CommRing A] [IsLocalRing A] [IsReduced A]
    [CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
    [IsLocalRing.IsHenselization A (ResidueField A) Ah]
    (hA : IsNagataRing A) (hdim : ringKrullDim A = 1) :
    Ring.deltaInvariant Ah = Ring.deltaInvariant A

Stacks.Curves.deltaInvariant_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/BaseChangeDelta.lean, line 224. The attribute's comment: “strict henselization”.

Strict henselization preserves the delta invariant of a reduced one-dimensional Nagata local ring.

public theorem deltaInvariant_strictHenselization
    (A Ash : Type u) [CommRing A] [IsLocalRing A] [IsReduced A]
    [CommRing Ash] [IsLocalRing Ash] [Algebra A Ash]
    (ksep : Type v) [Field ksep] [Algebra (ResidueField A) ksep]
    [IsSepClosure (ResidueField A) ksep] [IsLocalRing.IsHenselization A ksep Ash]
    (hA : IsNagataRing A) (hdim : ringKrullDim A = 1) :
    Ring.deltaInvariant Ash = Ring.deltaInvariant A

Stacks.Curves.deltaInvariant_adicCompletion_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/BaseChangeDelta.lean, line 244. The attribute's comment: “completion”. References: SGA 7 X (2.26), “partial”.

Completion at the maximal ideal preserves the delta invariant of a reduced one-dimensional Nagata local ring.

public theorem deltaInvariant_adicCompletion_maximalIdeal
    (A : Type u) [CommRing A] [IsLocalRing A] [IsReduced A]
    (hA : IsNagataRing A) (hdim : ringKrullDim A = 1) :
    Ring.deltaInvariant (AdicCompletion (maximalIdeal A) A) = Ring.deltaInvariant A
Tag 0C1T, a definition

Tag 0C1T in the Stacks Project.

Ring.deltaInvariant, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaInvariant/Defs.lean, line 31. The attribute's comment: “the invariant of a scheme at a point, as the invariant of the local ring there”. References: SGA 7 X (2.10).

The delta invariant of a commutative ring is the length of the quotient of its integral closure in its total ring of fractions by the image of the ring. For a reduced one-dimensional Nagata local ring, this quotient has finite length.

public noncomputable abbrev Ring.deltaInvariant (A : Type*) [CommRing A] : ℕ∞
Tag 0C3X, a lemma

Tag 0C3X in the Stacks Project.

AlgebraicGeometry.deltaInvariant_mul_length_quotient_le_of_flat_local_hom, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/DeltaInvariantFieldChange.lean, line 226. The attribute's comment: “sharpened by the length of the closed fibre: the source states the inequality without that factor”.

The delta invariant under a flat local homomorphism, with the length of the closed fibre as a factor. For a flat local homomorphism f : A → B of local rings, the delta invariant of A times the length of B / 𝔪_A B is at most the delta invariant of B.

The base change B ⊗[A] (A'/A) injects into B'/B, so its length bounds δ(B); the length of a base change along a flat local homomorphism is the length of the module times the length of the closed fibre (length_baseChange_eq_length_mul_length_quotient, Tag 02M1), which is the left-hand side. Dropping the factor — it is at least one — gives Tag 0C3X itself, AlgebraicGeometry.deltaInvariant_le_of_flat_local_hom.

public lemma deltaInvariant_mul_length_quotient_le_of_flat_local_hom
    (A B : Type u) [CommRing A] [IsLocalRing A] [CommRing B] [IsLocalRing B]
    (f : A →+* B) (hlocal : IsLocalHom f) (hflat : f.Flat) :
    Ring.deltaInvariant A *
        Module.length B (B ⧸ Ideal.map f (IsLocalRing.maximalIdeal A)) ≤
      Ring.deltaInvariant B

AlgebraicGeometry.deltaInvariant_stalk_le_baseChange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/DeltaInvariantFieldChange.lean, line 274.

Stacks Project, Tag 0C3X. The delta invariant of a scheme locally of finite type over a field at a point cannot decrease under an extension of the ground field.

public lemma deltaInvariant_stalk_le_baseChange
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    (x : X)
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}))
    (hy : pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K))) y = x) :
    Ring.deltaInvariant (X.presheaf.stalk x) ≤
      Ring.deltaInvariant
        ((pullback f
          (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}).presheaf.stalk y)

AlgebraicGeometry.deltaInvariant_mul_length_specialFibre_stalk_le_baseChange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/DeltaInvariantFieldChange.lean, line 303. The attribute's comment: “sharpened by the length of the special fibre of the map on local rings: the source states the inequality without that factor”.

The delta invariant of a stalk under extension of the ground field, with the length of the special fibre as a factor. The delta invariant at x times the length of the quotient of the local ring at a point y above x by the extension of the maximal ideal at x is at most the delta invariant at y.

Dropping the factor — it is at least one — gives Stacks Tag 0C3X itself, AlgebraicGeometry.deltaInvariant_stalk_le_baseChange. Keeping it turns a delta invariant that does not grow into a bound on the special fibre: when both delta invariants equal one the quotient has length one, so the maximal ideal at x already generates the maximal ideal at y.

public lemma deltaInvariant_mul_length_specialFibre_stalk_le_baseChange
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u})) :
    Ring.deltaInvariant
        (X.presheaf.stalk
          ((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y)) *
        Module.length
          ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) :
            Scheme.{u}).presheaf.stalk y)
          ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) :
              Scheme.{u}).presheaf.stalk y ⧸
            Ideal.map
              ((pullback.fst f
                (Spec.map (CommRingCat.ofHom (algebraMap k K)))).stalkMap y).hom
              (IsLocalRing.maximalIdeal
                (X.presheaf.stalk
                  ((pullback.fst f
                    (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y)))) ≤
      Ring.deltaInvariant
        ((pullback f
          (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}).presheaf.stalk y)
Tag 0C3Y, a lemma

Tag 0C3Y in the Stacks Project.

AlgebraicGeometry.deltaInvariant_stalk_baseChange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/DeltaInvariantSeparableFieldChange.lean, line 701.

The delta invariant of a reduced one-dimensional point whose normalization has separable residue fields is unchanged at any one-dimensional point above it after extending the field.

public lemma deltaInvariant_stalk_baseChange
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    (x : X)
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}))
    (hy : pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K))) y = x)
    (hred : _root_.IsReduced (X.presheaf.stalk x))
    (hdimX : ringKrullDim (X.presheaf.stalk x) = 1)
    (hsep :
      let Xnorm := normalizationSchemeOverField k f
      let ν := normalizationOverField k f
      ∀ x' : Xnorm, ν x' = x →
        letI : Algebra k (Xnorm.residueField x') :=
          ((Scheme.ΓSpecIso (.of k)).inv ≫ (ν ≫ f).appTop ≫ Xnorm.Γevaluation x').hom.toAlgebra
        Algebra.IsSeparableExtension k (Xnorm.residueField x'))
    (hdimY : ringKrullDim
      ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}).presheaf.stalk y)
        = 1) :
    Ring.deltaInvariant (X.presheaf.stalk x) =
      Ring.deltaInvariant
        ((pullback f
          (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}).presheaf.stalk y)
Sources
LeanIsLocalRing.radical_span_eq_maximalIdeal_iff_notMem_minimalPrimes · IsLocalRing.notMem_minimalPrimes_iff_localizationAway_equiv_pi_localizationAtPrime · IsLocalRing.exists_radical_span_eq_maximalIdeal · IsLocalRing.notMem_minimalPrimes_iff_mem_nonZeroDivisors_of_depth_eq_one · IsLocalRing.notMem_minimalPrimes_iff_localizationAway_equiv_fractionRing_of_depth_eq_one · IsLocalRing.depth_eq_one_of_isReduced · IsLocalRing.notMem_minimalPrimes_iff_localizationAway_equiv_pi_residueField_of_isReduced · isNormalRing_integralClosure_fractionRing

Section33.40 The number of branches#

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

Tag 0C1S, a lemma

Tag 0C1S in the Stacks Project.

AlgebraicGeometry.numberOfBranches_eq_encard_normalizationFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/NormalizationBranches.lean, line 77. The attribute's comment: “branches”.

The number of branches at a point equals the number of points of the normalization above it.

public theorem numberOfBranches_eq_encard_normalizationFiber
    (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (x : X) :
    AlgebraicGeometry.numberOfBranches X x =
      Set.encard {y : Scheme.normalizationScheme X hX |
        Scheme.normalization X hX y = x}

AlgebraicGeometry.numberOfGeometricBranches_eq_card_sigma_sepDegree_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/NormalizationBranches.lean, line 112. The attribute's comment: “geometric_branches”.

The number of geometric branches at a point is the sum, over the points of the normalization above it, of the separable degrees of the corresponding residue-field extensions, interpreted as the extended cardinality of the sigma type of these multiplicities.

public theorem numberOfGeometricBranches_eq_card_sigma_sepDegree_normalization
    (X : Scheme.{u})
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (x : X) :
    AlgebraicGeometry.numberOfGeometricBranches X x =
      ENat.card (Σ y : {y : Scheme.normalizationScheme X hX //
          Scheme.normalization X hX y = x},
        letI := (((X.residueFieldCongr y.property).inv ≫
          (Scheme.normalization X hX).residueFieldMap y).hom).toAlgebra
        (Field.sepDegree (X.residueField x)
          ((Scheme.normalizationScheme X hX).residueField y)).ord.ToType)
Tag 0C40, a lemma

Tag 0C40 in the Stacks Project.

AlgebraicGeometry.numberOfGeometricBranches_baseChange_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/GeometricBranchesFieldChange.lean, line 1030.

The number of geometric branches at a point of a scheme locally of finite type over a field is unchanged after extending the ground field and choosing a point above it.

public theorem numberOfGeometricBranches_baseChange_fieldExtension
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    (x : X)
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}))
    (hy : (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y = x) :
    AlgebraicGeometry.numberOfGeometricBranches X x =
      AlgebraicGeometry.numberOfGeometricBranches
        (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}) y
Tag 0C55, a lemma

Tag 0C55 in the Stacks Project.

AlgebraicGeometry.isGeometricallyUnibranchAt_iff_of_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/GeometricBranchesFieldChange.lean, line 1125. References: EGA IV (6.15.7), “loc. finite type, at x”.

Stacks Project, Tag 0C55. Geometric unibranchness at a point is invariant under extension of the ground field for a scheme locally of finite type over that field.

public theorem isGeometricallyUnibranchAt_iff_of_fieldExtension
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f]
    (x : X)
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}))
    (hy : (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y = x) :
    IsGeometricallyUnibranchAt X x ↔
      IsGeometricallyUnibranchAt
        (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}) y
Tag 0C41, a definition

Tag 0C41 in the Stacks Project.

IsLocalRing.IsWedge, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Branches/Wedge.lean, line 65.

A local ring A is a wedge of the nonempty finite family B if their residue fields can be identified and A is isomorphic to the subring of the product consisting of tuples with a common residue.

public def IsWedge (A : Type u) {n : ℕ} (B : Fin (n + 1) → Type v)
    [CommRing A] [IsLocalRing A] [∀ i, CommRing (B i)] [∀ i, IsLocalRing (B i)] : Prop
Tag 0C42, a lemma

Tag 0C42 in the Stacks Project.

Ring.deltaInvariant_ge_numberOfGeometricBranches_sub_one_of_strictlyHenselian, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/DeltaBranchBound.lean, line 78. The attribute's comment: “delta_ge_branches_sub_one”.

The delta invariant of a strictly henselian reduced Nagata local ring is at least the number of its geometric branches minus one.

public lemma deltaInvariant_ge_numberOfGeometricBranches_sub_one_of_strictlyHenselian
    (A : Type u) [CommRing A] [IsReduced A]
    [StrictlyHenselianLocalRing A]
    (hA : IsNagataRing A) :
    Ring.deltaInvariant A ≥
      numberOfGeometricBranchesOfLocalRing A - 1

Ring.exists_isWedge_of_deltaInvariant_eq_numberOfGeometricBranches_sub_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/DeltaBranchBound.lean, line 350. The attribute's comment: “equality_implies_wedge”.

A strictly henselian, reduced, one-dimensional Nagata local ring attaining the lower bound for its delta invariant is a wedge of a nonempty finite family of strictly henselian discrete valuation rings.

public theorem exists_isWedge_of_deltaInvariant_eq_numberOfGeometricBranches_sub_one
    (A : Type u) [CommRing A] [IsReduced A]
    [StrictlyHenselianLocalRing A]
    (hA : IsNagataRing A) (hdim : ringKrullDim A = 1)
    (hdelta : Ring.deltaInvariant A =
      numberOfGeometricBranchesOfLocalRing A - 1) :
    ∃ (n : ℕ) (B : Fin (n + 1) → Type u)
      (_ : ∀ i, CommRing (B i)) (_ : ∀ i, IsDomain (B i))
      (_ : ∀ i, IsLocalRing (B i)) (_ : ∀ i, IsDiscreteValuationRing (B i))
      (_ : ∀ i, StrictlyHenselianLocalRing (B i)),
      IsLocalRing.IsWedge A B
Tag 0C43, a lemma

Tag 0C43 in the Stacks Project.

Ring.deltaInvariant_ge_numberOfGeometricBranches_sub_one, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/DeltaBranches/LowerBound.lean, line 65.

The delta invariant of a reduced one-dimensional Nagata local ring is at least the number of its geometric branches minus one.

public lemma deltaInvariant_ge_numberOfGeometricBranches_sub_one
    (A : Type*) [CommRing A] [IsLocalRing A] [IsReduced A]
    (hA : IsNagataRing A) (hdim : ringKrullDim A = 1) :
    Ring.deltaInvariant A ≥
      numberOfGeometricBranchesOfLocalRing A - 1
Sources
LeanAlgebraicGeometry.numberOfBranches_eq_encard_normalizationFiber · AlgebraicGeometry.numberOfGeometricBranches_eq_card_sigma_sepDegree_normalization · AlgebraicGeometry.numberOfGeometricBranches_baseChange_fieldExtension · AlgebraicGeometry.isGeometricallyUnibranchAt_iff_of_fieldExtension · IsLocalRing.IsWedge · Ring.deltaInvariant_ge_numberOfGeometricBranches_sub_one_of_strictlyHenselian · Ring.exists_isWedge_of_deltaInvariant_eq_numberOfGeometricBranches_sub_one · Ring.deltaInvariant_ge_numberOfGeometricBranches_sub_one

Section33.41 Normalization of one dimensional schemes#

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

Tag 0C45, a lemma

Tag 0C45 in the Stacks Project.

AlgebraicGeometry.normalization_of_isLocallyNoetherian_dimension_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/NormalizationNoetherianDimensionOne.lean, line 140. References: EGA IV (18.9.7.8), “more general”.

Stacks Project, Tag 0C45. Let X be a locally Noetherian scheme of dimension 1 and let ν : X^ν → X be its normalization. Then

  1. ν is integral, surjective, and induces a bijection on irreducible components,
  2. there is a factorization X^ν → X_red → X and the morphism X^ν → X_red is the normalization of X_red,
  3. X^ν → X_red is birational,
  4. for every closed point x ∈ X the stalk (ν_* 𝒪_{X^ν})_x is the integral closure of 𝒪_{X,x} in the total ring of fractions of (𝒪_{X,x})_red = 𝒪_{X_red,x},
  5. the fibres of ν are finite and the residue field extensions are finite,
  6. X^ν is a disjoint union of integral normal locally Noetherian schemes and each affine open is the spectrum of a finite product of Dedekind domains.
theorem normalization_of_isLocallyNoetherian_dimension_one (X : Scheme.{u})
    [IsLocallyNoetherian X] (hdim : topologicalKrullDim X = 1) :
    -- (1)
    (IsIntegralHom X.normalizationOfIsLocallyNoetherian ∧
        Surjective X.normalizationOfIsLocallyNoetherian ∧
        Set.BijOn (fun C ↦ closure (X.normalizationOfIsLocallyNoetherian.base '' C))
          (irreducibleComponents X.normalizationSchemeOfIsLocallyNoetherian)
          (irreducibleComponents X)) ∧
      -- (2) and (3)
      (∃ g : X.normalizationSchemeOfIsLocallyNoetherian ⟶ X.nilradical.subscheme,
        g ≫ X.nilradical.subschemeι = X.normalizationOfIsLocallyNoetherian ∧
          IsBirational g ∧
          ∃ e : X.normalizationSchemeOfIsLocallyNoetherian ≅
            X.nilradical.subscheme.normalizationScheme
              (X.finite_irreducibleComponents_reduction
                (finite_irreducibleComponents_of_isCompact X)),
            e.hom ≫ X.nilradical.subscheme.normalization
              (X.finite_irreducibleComponents_reduction
                (finite_irreducibleComponents_of_isCompact X)) = g) ∧
      -- (4)
      (∀ x : X, IsClosed ({x} : Set X) →
        letI := normalizationPushforwardStalkAlgebra X
          (finite_irreducibleComponents_of_isCompact X) x
        letI : Algebra (X.presheaf.stalk x)
            (FractionRing (X.presheaf.stalk x ⧸ nilradical (X.presheaf.stalk x))) :=
          (reductionFractionRingHom (X.presheaf.stalk x)).toAlgebra
        Nonempty (normalizationPushforwardStalk X
              (finite_irreducibleComponents_of_isCompact X) x ≃ₐ[X.presheaf.stalk x]
            integralClosure (X.presheaf.stalk x)
              (FractionRing (X.presheaf.stalk x ⧸ nilradical (X.presheaf.stalk x)))) ∧
          ∀ z : X.nilradical.subscheme, X.nilradical.subschemeι z = x →
            Nonempty ((X.presheaf.stalk x ⧸ nilradical (X.presheaf.stalk x)) ≃+*
              X.nilradical.subscheme.presheaf.stalk z)) ∧
      -- (5)
      ((∀ x : X, (X.normalizationOfIsLocallyNoetherian.base ⁻¹' {x}).Finite) ∧
        ∀ y : X.normalizationSchemeOfIsLocallyNoetherian,
          (X.normalizationOfIsLocallyNoetherian.residueFieldMap y).hom.Finite) ∧
      -- (6)
      ((∃ (ι : Type u) (Y : ι → Scheme.{u}) (_ : ∀ i, IsIntegral (Y i))
          (_ : ∀ i, IsNormal (Y i)) (_ : ∀ i, IsLocallyNoetherian (Y i)),
          Nonempty (X.normalizationSchemeOfIsLocallyNoetherian ≅ ∐ Y)) ∧
        ∀ W : X.normalizationSchemeOfIsLocallyNoetherian.Opens, IsAffineOpen W →
          Stacks.IsFiniteProductOfDedekindDomains
            Γ(X.normalizationSchemeOfIsLocallyNoetherian, W))
Tag 0C1R, a lemma

Tag 0C1R in the Stacks Project.

AlgebraicGeometry.Scheme.isBirational_normalization_morphismRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Birational/RestrictOpen.lean, line 104. The attribute's comment: “finite_normalization”.

Stacks Project, Tag 0C1R. Over every open of a reduced scheme, the normalization morphism is birational.

public theorem isBirational_normalization_morphismRestrict (X : Scheme.{u}) [IsReduced X]
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (V : X.Opens) : IsBirational (X.normalization hX ∣_ V)

Stacks.AlgebraicGeometry.NormalizationQuotient.existsUnique_linearEquiv_quotient_adicCompletion_normalizationPushforwardStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationQuotient/Completion.lean, line 138. The attribute's comment: “quotient_completion”.

Stacks Project, Tag 0C1R. Let X be a reduced scheme of dimension one with normalization ν, let x ∈ X, write A = 𝒪_{X,x} and A' = (ν_* 𝒪_{X^ν})_x, and complete at the maximal ideal of A. There is exactly one A-linear isomorphism A'/A ≅ A'^∧/A^∧ compatible with the canonical maps to the completions.

The closedness of the point assumed in the source is not used; the dimension hypothesis is.

public theorem existsUnique_linearEquiv_quotient_adicCompletion_normalizationPushforwardStalk
    (X : Scheme.{u}) [IsReduced X] (hNagata : IsNagataScheme X)
    (hdim : topologicalKrullDim X = 1)
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) (x : X) :
    letI : Algebra (X.presheaf.stalk x) (normalizationPushforwardStalk X hX x) :=
      normalizationPushforwardStalkAlgebra X hX x
    ∃! e :
        (normalizationPushforwardStalk X hX x ⧸
            LinearMap.range (Algebra.linearMap (X.presheaf.stalk x)
              (normalizationPushforwardStalk X hX x))) ≃ₗ[X.presheaf.stalk x]
          (AdicCompletion (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
              (normalizationPushforwardStalk X hX x) ⧸
            LinearMap.range (AdicCompletion.map
              (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
              (Algebra.linearMap (X.presheaf.stalk x)
                (normalizationPushforwardStalk X hX x)))),
      ∀ a : normalizationPushforwardStalk X hX x,
        e (Submodule.mkQ _ a) = Submodule.mkQ _
          (AdicCompletion.of (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
            (normalizationPushforwardStalk X hX x) a)

Stacks.AlgebraicGeometry.NormalizationQuotient.normalizationQuotient_iso_coproduct_skyscraperModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationQuotient/DirectSum.lean, line 60. The attribute's comment: “quotient_sheaf”.

Stacks Project, Tag 0C1R(2). For a reduced Nagata scheme of dimension one the quotient ν_* 𝒪_{X^ν} / 𝒪_X is the direct sum of the skyscraper sheaves of its stalks at the singular points: the quotient's stalk vanishes at every regular point, and the singular locus is closed and discrete.

public theorem normalizationQuotient_iso_coproduct_skyscraperModule (X : Scheme.{u})
    [IsReduced X] (hX : IsNagataScheme X) (hdim : topologicalKrullDim X = 1) :
    Nonempty
      (normalizationQuotient X (finite_irreducibleComponents_of_isNagataScheme X hX) ≅
        ∐ fun z : singularLocus X =>
          skyscraperModule X z.1
            (normalizationQuotientStalk X
              (finite_irreducibleComponents_of_isNagataScheme X hX) z.1))

Stacks.AlgebraicGeometry.NormalizationQuotient.normalizationQuotientStalk_linearEquiv_quotient_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationQuotient/StalkLength.lean, line 441. The attribute's comment: “delta_length”.

Stacks Project, Tag 0C1R. The stalk of the normalization quotient ν_* 𝒪_{X^ν} / 𝒪_X at a point of a reduced scheme is the normalization stalk modulo the image of the local ring.

Neither the Nagata hypothesis, nor the dimension of X, nor closedness of the point is needed.

public theorem normalizationQuotientStalk_linearEquiv_quotient_range
    (X : Scheme.{u}) [IsReduced X]
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) (x : X) :
    letI : Algebra (X.presheaf.stalk x) (normalizationPushforwardStalk X hX x) :=
      normalizationPushforwardStalkAlgebra X hX x
    Nonempty (normalizationQuotientStalk X hX x ≃ₗ[X.presheaf.stalk x]
      (normalizationPushforwardStalk X hX x ⧸
        LinearMap.range (Algebra.linearMap (X.presheaf.stalk x)
          (normalizationPushforwardStalk X hX x))))

Stacks.AlgebraicGeometry.NormalizationQuotient.length_normalizationQuotientStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationQuotient/StalkLength.lean, line 582. The attribute's comment: “delta_length”.

Stacks Project, Tag 0C1R. The length of the stalk of the normalization quotient is the delta invariant of the local ring.

Neither the Nagata hypothesis, nor the dimension of X, nor closedness of the point is needed; without them both sides may be infinite.

public theorem length_normalizationQuotientStalk (X : Scheme.{u}) [IsReduced X]
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) (x : X) :
    Module.length (X.presheaf.stalk x) (normalizationQuotientStalk X hX x) =
      Ring.deltaInvariant (X.presheaf.stalk x)

Stacks.AlgebraicGeometry.NormalizationQuotient.isFiniteLength_normalizationQuotientStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationQuotient/StalkLength.lean, line 625. The attribute's comment: “delta_length”.

Stacks Project, Tag 0C1R. On a reduced Nagata scheme of dimension one the stalk of the normalization quotient has finite length.

Closedness of the point is not needed, and the dimension hypothesis is used only through the dimension of the local ring at x.

public theorem isFiniteLength_normalizationQuotientStalk (X : Scheme.{u}) [IsReduced X]
    (hNagata : IsNagataScheme X) (hdim : topologicalKrullDim X = 1)
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) (x : X) :
    IsFiniteLength (X.presheaf.stalk x) (normalizationQuotientStalk X hX x)

Stacks.AlgebraicGeometry.NormalizationQuotientDirectSum.normalizationQuotientIsoCoproductSkyscraper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationQuotientDirectSum/Basic.lean, line 41. The attribute's comment: “quotient_sheaf”.

For a reduced Nagata scheme X of dimension one, the normalization quotient of X is isomorphic to the direct sum, over the singular points x of X, of the skyscraper modules at x of its stalks.

public theorem normalizationQuotientIsoCoproductSkyscraper (X : Scheme.{u}) [IsReduced X]
    (hX : IsNagataScheme X) (hdim : topologicalKrullDim X = 1) :
    Nonempty
      (normalizationQuotient X
          (Stacks.AlgebraicGeometry.Normalization.finite_irreducibleComponents_of_isNagataScheme
            X hX) ≅
        ∐ fun x : singularLocus X =>
          skyscraperModule X x.1
            (normalizationQuotientStalk X
              (Stacks.AlgebraicGeometry.Normalization.finite_irreducibleComponents_of_isNagataScheme
                X hX) x.1))

AlgebraicGeometry.existsUnique_algHom_normalizationPushforwardStalk_fractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormalizationStalkAmbient/UniqueEmbedding.lean, line 108. The attribute's comment: “normalization_stalk”.

Stacks Project, Tag 0C1R. At a point of a reduced scheme the stalk of the pushforward of the structure sheaf of the normalization carries exactly one injective algebra map into the total ring of fractions of the local ring whose image is the integral closure: the canonical embedding of the normalization stalk.

Neither the dimension-one hypothesis nor the closedness of the point is used, and the Nagata hypothesis of the source enters only through the finiteness of irreducible components needed to form the normalization.

public theorem existsUnique_algHom_normalizationPushforwardStalk_fractionRing
    (X : Scheme.{u}) [IsReduced X]
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) (x : X) :
    letI : Algebra (X.presheaf.stalk x) (normalizationPushforwardStalk X hX x) :=
      normalizationPushforwardStalkAlgebra X hX x
    ∃! f : normalizationPushforwardStalk X hX x →ₐ[X.presheaf.stalk x]
        FractionRing (X.presheaf.stalk x),
      Function.Injective f ∧
        f.range = integralClosure (X.presheaf.stalk x) (FractionRing (X.presheaf.stalk x))

AlgebraicGeometry.exists_pi_isDiscreteValuationRing_adicCompletion_normalizationStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/NormalizationStalkCompletion.lean, line 417. The attribute's comment: “complete_dvr_product”.

Stacks Project, Tag 0C1R. At a point of a reduced Nagata scheme whose local ring has dimension one, the completion of the stalk of the pushforward of the structure sheaf of the normalization, along the ideal generated by the maximal ideal of the local ring, is a nonempty finite product of complete discrete valuation rings.

Neither the dimension of X nor the closedness of the point is needed: the dimension hypothesis of the source enters only through the dimension of the local ring at x.

public theorem exists_pi_isDiscreteValuationRing_adicCompletion_normalizationStalk
    (X : Scheme.{u}) [IsReduced X] (hNagata : IsNagataScheme X)
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) (x : X)
    (hxdim : ringKrullDim (X.presheaf.stalk x) = 1) :
    letI : Algebra (X.presheaf.stalk x) (normalizationPushforwardStalk X hX x) :=
      normalizationPushforwardStalkAlgebra X hX x
    ∃ (n : ℕ) (D : Fin n → Type u) (_ : ∀ i, CommRing (D i)) (_ : ∀ i, IsDomain (D i))
        (_ : ∀ i, IsDiscreteValuationRing (D i)),
      0 < n ∧ (∀ i, IsAdicComplete (maximalIdeal (D i)) (D i)) ∧
        Nonempty (AdicCompletion
          ((maximalIdeal (X.presheaf.stalk x)).map
            (algebraMap (X.presheaf.stalk x) (normalizationPushforwardStalk X hX x)))
          (normalizationPushforwardStalk X hX x) ≃+* ∀ i, D i)

AlgebraicGeometry.exists_injective_range_eq_integralClosure_adicCompletion_normalizationStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/NormalizationStalkCompletion.lean, line 471. The attribute's comment: “normalization_after_completion”. References: EGA IV (7.6.1), “special case”.

Stacks Project, Tag 0C1R. Completing the stalk of the pushforward of the structure sheaf of the normalization of a reduced one-dimensional Nagata scheme, along the ideal generated by the maximal ideal of the local ring at the point, gives the integral closure of the completed local ring in its own total ring of fractions.

The two compatibility equations say that the resulting embedding extends the structure map of the completed local ring and the given embedding f₀ of the normalization stalk; the embedding f₀ exists and is unique by existsUnique_algHom_normalizationPushforwardStalk_fractionRing.

Closedness of the point is not needed. The points whose local ring is zero-dimensional are covered: there the local ring is a field and both completions are trivial.

public theorem exists_injective_range_eq_integralClosure_adicCompletion_normalizationStalk
    (X : Scheme.{u}) [IsReduced X] (hNagata : IsNagataScheme X)
    (hdim : topologicalKrullDim X = 1)
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) (x : X) :
    letI : Algebra (X.presheaf.stalk x) (normalizationPushforwardStalk X hX x) :=
      normalizationPushforwardStalkAlgebra X hX x
    let A := X.presheaf.stalk x
    let A' := normalizationPushforwardStalk X hX x
    let Ac := AdicCompletion (maximalIdeal A) A
    let J := (maximalIdeal A).map (algebraMap A A')
    let C := AdicCompletion J A'
    let k : Ac →+* C := adicCompletionMap (algebraMap A A') (maximalIdeal A) J le_rfl
    ∀ f₀ : A' →ₐ[A] FractionRing A, Function.Injective f₀ →
      f₀.range = integralClosure A (FractionRing A) →
      ∃ q : FractionRing A →+* FractionRing Ac,
        (∀ a : A, q (algebraMap A (FractionRing A) a) =
          algebraMap Ac (FractionRing Ac) (algebraMap A Ac a)) ∧
        ∃ g : C →+* FractionRing Ac,
          Function.Injective g ∧
          g.range = (integralClosure Ac (FractionRing Ac)).toSubring ∧
          (∀ y : Ac, g (k y) = algebraMap Ac (FractionRing Ac) y) ∧
          (∀ a' : A', g (algebraMap A' C a') = q (f₀ a'))

AlgebraicGeometry.Scheme.isFinite_surjective_isBirational_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/PrepareDeltaInvariant.lean, line 85. The attribute's comment: “part (1): ν is finite, surjective and birational”. References: EGA II (6.3.8), “special case”.

Stacks Project, Tag 0C1R, part (1). The normalization ν : X^ν ⟶ X of a reduced Nagata scheme is finite, surjective and birational.

The dimension of X is not used.

public theorem isFinite_surjective_isBirational_normalization (X : Scheme.{u}) [IsReduced X]
    (hX : IsNagataScheme X) :
    IsFinite (X.normalization (finite_irreducibleComponents_of_isNagataScheme X hX)) ∧
      Surjective (X.normalization (finite_irreducibleComponents_of_isNagataScheme X hX)) ∧
      IsBirational (X.normalization (finite_irreducibleComponents_of_isNagataScheme X hX))

AlgebraicGeometry.normalizationQuotient_mono_iso_coproduct_skyscraperModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/PrepareDeltaInvariant.lean, line 120. The attribute's comment: “part (2): O_X ⊂ ν_*O, the quotient a sum of skyscrapers Q_x at singular points”.

Stacks Project, Tag 0C1R, part (2). For a reduced Nagata scheme X of dimension one, 𝒪_X ⊂ ν_* 𝒪_{X^ν} — the map is a monomorphism both of sheaves of rings and of 𝒪_X-modules — and the quotient ν_* 𝒪_{X^ν} / 𝒪_X is the direct sum, over the singular points x of X, of the skyscraper sheaves at x with value 𝒬_x, the stalk of the quotient at x; that stalk is nonzero exactly at the singular points.

public theorem normalizationQuotient_mono_iso_coproduct_skyscraperModule (X : Scheme.{u})
    [IsReduced X] (hX : IsNagataScheme X) (hdim : topologicalKrullDim X = 1) :
    Mono (Scheme.Hom.toRingCatSheafHom
        (X.normalization (finite_irreducibleComponents_of_isNagataScheme X hX))) ∧
      Mono (normalizationModuleMap X (finite_irreducibleComponents_of_isNagataScheme X hX)) ∧
      Nonempty
        (normalizationQuotient X (finite_irreducibleComponents_of_isNagataScheme X hX) ≅
          ∐ fun z : singularLocus X =>
            skyscraperModule X z.1
              (normalizationQuotientStalk X
                (finite_irreducibleComponents_of_isNagataScheme X hX) z.1)) ∧
      ∀ x : X, ¬ IsZero (normalizationQuotientStalk X
          (finite_irreducibleComponents_of_isNagataScheme X hX) x) ↔ x ∈ singularLocus X

AlgebraicGeometry.normalizationQuotientStalk_finiteLength_eq_deltaInvariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/PrepareDeltaInvariant.lean, line 144. The attribute's comment: “part (4): Q_x = A'/A has finite length equal to the δ-invariant”.

Stacks Project, Tag 0C1R, part (4). On a reduced Nagata scheme of dimension one, the stalk 𝒬_x of ν_* 𝒪_{X^ν} / 𝒪_X at x is A' / A, where A = 𝒪_{X,x} and A' = (ν_* 𝒪_{X^ν})_x; it has finite length over A, and that length is the δ-invariant of X at x.

public theorem normalizationQuotientStalk_finiteLength_eq_deltaInvariant (X : Scheme.{u})
    [IsReduced X] (hX : IsNagataScheme X) (hdim : topologicalKrullDim X = 1) (x : X) :
    letI : Algebra (X.presheaf.stalk x)
        (normalizationPushforwardStalk X (finite_irreducibleComponents_of_isNagataScheme X hX) x) :=
      normalizationPushforwardStalkAlgebra X _ x
    Nonempty (normalizationQuotientStalk X (finite_irreducibleComponents_of_isNagataScheme X hX) x
        ≃ₗ[X.presheaf.stalk x]
        (normalizationPushforwardStalk X (finite_irreducibleComponents_of_isNagataScheme X hX) x ⧸
          LinearMap.range (Algebra.linearMap (X.presheaf.stalk x)
            (normalizationPushforwardStalk X
              (finite_irreducibleComponents_of_isNagataScheme X hX) x)))) ∧
      IsFiniteLength (X.presheaf.stalk x)
        (normalizationQuotientStalk X (finite_irreducibleComponents_of_isNagataScheme X hX) x) ∧
      Module.length (X.presheaf.stalk x)
          (normalizationQuotientStalk X (finite_irreducibleComponents_of_isNagataScheme X hX) x) =
        Ring.deltaInvariant (X.presheaf.stalk x)

AlgebraicGeometry.normalizationPushforwardStalk_semilocal_finiteProductOfDedekindDomains, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/PrepareDeltaInvariant.lean, line 170. The attribute's comment: “part (5): A' is semi-local and a finite product of Dedekind domains”.

Stacks Project, Tag 0C1R, part (5). On a Nagata scheme of dimension one, the stalk A' = (ν_* 𝒪_{X^ν})_x is a semi-local ring — it has finitely many maximal ideals — which is a finite product of Dedekind domains.

Reducedness of X is not used.

public theorem normalizationPushforwardStalk_semilocal_finiteProductOfDedekindDomains
    (X : Scheme.{u}) (hX : IsNagataScheme X) (hdim : topologicalKrullDim X = 1) (x : X) :
    Finite (MaximalSpectrum
        (normalizationPushforwardStalk X (finite_irreducibleComponents_of_isNagataScheme X hX) x)) ∧
      IsDiscreteValuationRing.IsFiniteProductOfDedekindDomains
        (normalizationPushforwardStalk X (finite_irreducibleComponents_of_isNagataScheme X hX) x)

AlgebraicGeometry.adicCompletion_stalk_reduced_noetherian_complete_local_dim_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/PrepareDeltaInvariant.lean, line 188. The attribute's comment: “part (6): A^ is reduced Noetherian complete local of dimension 1 (dim A = 1)”. References: EGA IV (7.3.19), “dim(Â)=1”.

Stacks Project, Tag 0C1R, part (6), at a point whose local ring has dimension one. For a reduced Nagata scheme X and a point x with dim 𝒪_{X,x} = 1, the completion A^∧ of A = 𝒪_{X,x} at its maximal ideal is a reduced Noetherian complete local ring of dimension one.

The hypothesis on dim 𝒪_{X,x} corrects the source: at a closed point of a one-dimensional scheme whose local ring is a field (an isolated point), A^∧ = A has dimension zero. Everything except the dimension holds without it.

public theorem adicCompletion_stalk_reduced_noetherian_complete_local_dim_one (X : Scheme.{u})
    [IsReduced X] (hX : IsNagataScheme X) (x : X)
    (hxdim : ringKrullDim (X.presheaf.stalk x) = 1) :
    _root_.IsReduced (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) ∧
      IsNoetherianRing (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) ∧
      ∃ _ : IsLocalRing
          (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)),
        IsAdicComplete
            (maximalIdeal
              (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)))
            (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) ∧
          ringKrullDim
              (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) = 1

AlgebraicGeometry.adicCompletion_stalk_reduced_noetherian_complete_local_ringKrullDim_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/PrepareDeltaInvariant.lean, line 218. The attribute's comment: “part (6) at every point: A^ reduced Noetherian complete local, dim A^ = dim A ≤ 1”. References: EGA IV (7.3.19), “dim(Â)=1”.

Stacks Project, Tag 0C1R, part (6), at every point. Let X be a reduced Nagata scheme of dimension one, x ∈ X and A = 𝒪_{X,x}. The completion A^∧ of A at its maximal ideal is a reduced Noetherian complete local ring with dim A^∧ = dim A; moreover dim A ≤ 1, with dim A = 1 exactly when A is not a field. So the source's "of dimension 1" is precisely the case dim A = 1, the one adicCompletion_stalk_reduced_noetherian_complete_local_dim_one states.

Part (6) as printed fails when A is a field, which happens at an isolated point: the scheme X = Spec (k × k[t]) is reduced, Nagata and of dimension one, its point Spec k is closed, and there A = A^∧ = k has dimension zero. Neither closedness of x nor any hypothesis on dim A is used.

public theorem adicCompletion_stalk_reduced_noetherian_complete_local_ringKrullDim_eq
    (X : Scheme.{u}) [IsReduced X] (hX : IsNagataScheme X) (hdim : topologicalKrullDim X = 1)
    (x : X) :
    _root_.IsReduced (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) ∧
      IsNoetherianRing (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) ∧
      (∃ _ : IsLocalRing
          (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)),
        IsAdicComplete
            (maximalIdeal
              (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)))
            (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) ∧
          ringKrullDim
              (AdicCompletion (maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) =
            ringKrullDim (X.presheaf.stalk x)) ∧
      ringKrullDim (X.presheaf.stalk x) ≤ 1 ∧
      (ringKrullDim (X.presheaf.stalk x) = 1 ↔ ¬ IsField (X.presheaf.stalk x))

AlgebraicGeometry.exists_injective_range_eq_integralClosure_adicCompletion_normalizationStalk_of_isNagataScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/PrepareDeltaInvariant.lean, line 266. The attribute's comment: “part (7): (A')^ is the integral closure of A^ in its total ring of fractions”.

Stacks Project, Tag 0C1R, part (7). Let X be a reduced Nagata scheme of dimension one, A = 𝒪_{X,x} and A' = (ν_* 𝒪_{X^ν})_x. The completion (A')^∧ of A' along 𝔪_A A' is the integral closure of A^∧ in its total ring of fractions: there is an injective ring map (A')^∧ → Frac(A^∧) extending the structure map of A^∧, whose image is the integral closure of A^∧ in Frac(A^∧).

Closedness of the point is not needed.

public theorem
    exists_injective_range_eq_integralClosure_adicCompletion_normalizationStalk_of_isNagataScheme
    (X : Scheme.{u}) [IsReduced X] (hX : IsNagataScheme X) (hdim : topologicalKrullDim X = 1)
    (x : X) :
    letI : Algebra (X.presheaf.stalk x)
        (normalizationPushforwardStalk X (finite_irreducibleComponents_of_isNagataScheme X hX) x) :=
      normalizationPushforwardStalkAlgebra X _ x
    let A := X.presheaf.stalk x
    let A' :=
      normalizationPushforwardStalk X (finite_irreducibleComponents_of_isNagataScheme X hX) x
    let Ac := AdicCompletion (maximalIdeal A) A
    let J := (maximalIdeal A).map (algebraMap A A')
    let C := AdicCompletion J A'
    let k : Ac →+* C := adicCompletionMap (algebraMap A A') (maximalIdeal A) J le_rfl
    ∃ g : C →+* FractionRing Ac,
      Function.Injective g ∧
        g.range = (integralClosure Ac (FractionRing Ac)).toSubring ∧
        ∀ y : Ac, g (k y) = algebraMap Ac (FractionRing Ac) y

AlgebraicGeometry.finite_maximalSpectrum_normalizationPushforwardStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/SemilocalDedekind.lean, line 151. The attribute's comment: “semilocal_dedekind”.

Stacks Project, Tag 0C1R. The stalk of the pushforward of the structure sheaf of the normalization of a Nagata scheme is semilocal: it has finitely many maximal ideals.

The point is not assumed closed, and the dimension hypothesis of the source is not used.

public theorem finite_maximalSpectrum_normalizationPushforwardStalk
    (X : Scheme.{u}) (hNagata : IsNagataScheme X)
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) (x : X) :
    letI : Algebra (X.presheaf.stalk x) (normalizationPushforwardStalk X hX x) :=
      normalizationPushforwardStalkAlgebra X hX x
    Finite (MaximalSpectrum (normalizationPushforwardStalk X hX x))

AlgebraicGeometry.isFiniteProductOfDedekindDomains_normalizationPushforwardStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/SemilocalDedekind.lean, line 174. The attribute's comment: “semilocal_dedekind”.

Stacks Project, Tag 0C1R. On a Nagata scheme of dimension one, the stalk of the pushforward of the structure sheaf of the normalization is a finite product of Dedekind domains.

The point is not assumed closed.

public theorem isFiniteProductOfDedekindDomains_normalizationPushforwardStalk
    (X : Scheme.{u}) (hNagata : IsNagataScheme X) (hdim : topologicalKrullDim X = 1)
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) (x : X) :
    IsDiscreteValuationRing.IsFiniteProductOfDedekindDomains
      (normalizationPushforwardStalk X hX x)

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.normalization_of_isLocallyNoetherian_dimension_one · AlgebraicGeometry.Scheme.isBirational_normalization_morphismRestrict · Stacks.AlgebraicGeometry.NormalizationQuotient.existsUnique_linearEquiv_quotient_adicCompletion_normalizationPushforwardStalk · Stacks.AlgebraicGeometry.NormalizationQuotient.normalizationQuotient_iso_coproduct_skyscraperModule · Stacks.AlgebraicGeometry.NormalizationQuotient.normalizationQuotientStalk_linearEquiv_quotient_range · Stacks.AlgebraicGeometry.NormalizationQuotient.length_normalizationQuotientStalk · Stacks.AlgebraicGeometry.NormalizationQuotient.isFiniteLength_normalizationQuotientStalk · Stacks.AlgebraicGeometry.NormalizationQuotientDirectSum.normalizationQuotientIsoCoproductSkyscraper

Section33.42 Finding affine opens#

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

Tag 09NG, a lemma

Tag 09NG in the Stacks Project.

AlgebraicGeometry.isOpenImmersion_of_openCover_source_of_separated_of_genericPoints_injOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/FindingAffineOpens/OpenImmersionCriterion.lean, line 189.

Stacks Project, Tag 09NG. A separated morphism that is locally an open immersion on the source and injective on generic points of irreducible components is an open immersion.

public theorem isOpenImmersion_of_openCover_source_of_separated_of_genericPoints_injOn
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsSeparated f] (𝒰 : X.OpenCover)
    (h𝒰 : ∀ i, IsOpenImmersion (𝒰.f i ≫ f))
    (hinj : Set.InjOn f (genericPoints X)) :
    IsOpenImmersion f
Tag 09NH, a lemma

Tag 09NH in the Stacks Project.

AlgebraicGeometry.exists_isOpenImmersion_res_of_isIso_stalkMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/FindingAffineOpens/LocalIsomorphism.lean, line 81.

Stacks Project, Tag 09NH. If the local-ring map of a locally finite-type morphism is an isomorphism at x, and the target is reduced with finitely many irreducible components, then the morphism is an open immersion near x.

public theorem exists_isOpenImmersion_res_of_isIso_stalkMap
    {X S : Scheme.{u}} (f : X ⟶ S) (x : X)
    [IsReduced S] [LocallyOfFiniteType f]
    (hcomponents : (irreducibleComponents S).Finite)
    (hstalk : IsIso (f.stalkMap x)) :
    ∃ U : X.Opens, x ∈ U ∧ IsOpenImmersion (U.ι ≫ f)
Tag 09NI, a lemma

Tag 09NI in the Stacks Project.

AlgebraicGeometry.exists_isAffineOpen_containing_image_of_genericPoints_injOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/FindingAffineOpens/CommonAffineOpenOfStalks.lean, line 420.

[Stacks, Tag 09NI]. Let f : T ⟶ X be a morphism of schemes with T affine and X quasi-separated with finitely many generic points. If f carries the generic points of the irreducible components of T into those of X and does so injectively, and if the canonical map of local rings at each member of a finite family of points of T is an isomorphism, then the images of that family lie in a common affine open of X.

public theorem exists_isAffineOpen_containing_image_of_genericPoints_injOn
    {T X : Scheme.{u}} (f : T ⟶ X) [IsAffine T] [QuasiSeparatedSpace X]
    (hX : (genericPoints X).Finite)
    (hgeneric : Set.MapsTo f (genericPoints T) (genericPoints X))
    (hinj : Set.InjOn f (genericPoints T))
    {ι : Type v} [Finite ι] (t : ι → T)
    (hstalk : ∀ i, IsIso (f.stalkMap (t i))) :
    ∃ U : X.Opens, IsAffineOpen U ∧ ∀ i, f (t i) ∈ U
Tag 09NJ, a lemma

Tag 09NJ in the Stacks Project.

AlgebraicGeometry.exists_isAffineOpen_containing_of_stalk_krullDimLE_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/FindingAffineOpens/CommonAffineOpenOfDimensionOnePoints.lean, line 179.

[Stacks, Tag 09NJ] A finite family of points on an integral separated scheme, whose local rings are Noetherian of Krull dimension at most one, lies in a common affine open.

theorem exists_isAffineOpen_containing_of_stalk_krullDimLE_one
    (X : Scheme.{u}) [IsIntegral X] [X.IsSeparated]
    {ι : Type v} [Finite ι] (x : ι → X)
    (h_noetherian : ∀ i, IsNoetherianRing (X.presheaf.stalk (x i)))
    (h_dimension : ∀ i, Ring.KrullDimLE 1 (X.presheaf.stalk (x i))) :
    ∃ U : X.Opens, IsAffineOpen U ∧ ∀ i, x i ∈ U
Tag 09NK, a lemma

Tag 09NK in the Stacks Project.

Ideal.exists_lift_avoiding_primes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/AvoidingPrimes.lean, line 33.

If an ideal is contained in none of a finite family of prime ideals, every class modulo that ideal has a representative outside all of the primes.

public theorem exists_lift_avoiding_primes
    {A : Type u} [CommRing A] (I : Ideal A) {r : ℕ} (p : Fin r → Ideal A)
    (hp : ∀ i, (p i).IsPrime) (hI : ∀ i, ¬ I ≤ p i) (fbar : A ⧸ I) :
    ∃ f : A, (∀ i, f ∉ p i) ∧ Ideal.Quotient.mk I f = fbar
Tag 09NM, a lemma

Tag 09NM in the Stacks Project.

AlgebraicGeometry.exists_isAffineOpen_containing_of_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/FindingAffineOpens/CommonAffineOpenOfComponents.lean, line 471.

[Stacks, Tag 09NM]. Let X be a scheme with finitely many irreducible components and T ⊆ X a finite set of points. If for every irreducible component Z the set T ∩ Z is contained in an affine open of the reduced induced closed subscheme on Z, then T is contained in an affine open subscheme of X.

public theorem exists_isAffineOpen_containing_of_components
    (X : Scheme.{u}) {T : Set X} (hT : T.Finite)
    (hcomponents : (irreducibleComponents X).Finite)
    (hlocal : ∀ Z : Closeds X, (Z : Set X) ∈ irreducibleComponents X →
      ∃ U : (Scheme.IdealSheafData.vanishingIdeal Z).subscheme.Opens,
        IsAffineOpen U ∧
          T ∩ (Z : Set X) ⊆
            Set.range (U.ι ≫ (Scheme.IdealSheafData.vanishingIdeal Z).subschemeι)) :
    ∃ U : X.Opens, IsAffineOpen U ∧ T ⊆ U
Tag 09NN, a proposition

Tag 09NN in the Stacks Project.

AlgebraicGeometry.exists_isAffineOpen_containing_of_stalk_krullDimLE_one_of_finite_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/FindingAffineOpens/CommonAffineOpenOfDimensionOnePointsFiniteComponents.lean, line 80.

[Stacks, Tag 09NN] Let X be a separated scheme such that every quasi-compact open of X has finitely many irreducible components. A finite family of points of X whose local rings are Noetherian of Krull dimension at most one is contained in an affine open subscheme of X.

theorem exists_isAffineOpen_containing_of_stalk_krullDimLE_one_of_finite_components
    (X : Scheme.{u}) [X.IsSeparated]
    (hX : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    {ι : Type v} [Finite ι] (x : ι → X)
    (h_noetherian : ∀ i, IsNoetherianRing (X.presheaf.stalk (x i)))
    (h_dimension : ∀ i, Ring.KrullDimLE 1 (X.presheaf.stalk (x i))) :
    ∃ U : X.Opens, IsAffineOpen U ∧ ∀ i, x i ∈ U
Sources
LeanAlgebraicGeometry.isOpenImmersion_of_openCover_source_of_separated_of_genericPoints_injOn · AlgebraicGeometry.exists_isOpenImmersion_res_of_isIso_stalkMap · AlgebraicGeometry.exists_isAffineOpen_containing_image_of_genericPoints_injOn · AlgebraicGeometry.exists_isAffineOpen_containing_of_stalk_krullDimLE_one · Ideal.exists_lift_avoiding_primes · AlgebraicGeometry.exists_isAffineOpen_containing_of_components · AlgebraicGeometry.exists_isAffineOpen_containing_of_stalk_krullDimLE_one_of_finite_components

Section33.43 Curves#

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

Tag 0A23, a definition

Tag 0A23 in the Stacks Project.

AlgebraicGeometry.IsCurve, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/Defs.lean, line 46. References: EGA II (7.4.2), “special case”.

Stacks Project, Tag 0A23. A curve over a field is a variety of Krull dimension one.

public class IsCurve (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) : Prop
    extends IsVariety k f
Tag 0A24, a lemma

Tag 0A24 in the Stacks Project.

AlgebraicGeometry.not_isProper_compl_singleton, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/Proper.lean, line 44.

Stacks 0A24. Removing a closed point from an irreducible scheme of positive dimension gives an open subscheme which is not proper over any base over which the scheme is separated.

public lemma not_isProper_compl_singleton
    {X S : Scheme.{u}} (f : X ⟶ S)
    [IsSeparated f] [IrreducibleSpace X] (x : X) (hx : IsClosed ({x} : Set X))
    (hdim : 0 < topologicalKrullDim X) :
    let U : X.Opens := ⟨{x}ᶜ, hx.isOpen_compl⟩
    ¬ IsProper (U.ι ≫ f)
Tag 0A25, a lemma

Tag 0A25 in the Stacks Project.

Stacks.HQuasiProjectiveDimensionOne.isHQuasiProjective_of_topologicalKrullDim_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HQuasiProjectiveDimensionOne/Basic.lean, line 159. The attribute's comment: “for a scheme of topological Krull dimension zero, where reducedness is not needed because such a scheme is affine and the structure sheaf of an affine scheme is ample”.

A separated scheme of finite type over a field k of topological Krull dimension zero is H-quasi-projective over k.

theorem isHQuasiProjective_of_topologicalKrullDim_eq_zero {k : Type u} [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of k)) [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    (hdim : topologicalKrullDim (X : Type u) = 0) :
    AlgebraicGeometry.IsHQuasiProjective f

Stacks.HQuasiProjectiveDimensionOne.isHQuasiProjective_of_dimension_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HQuasiProjectiveDimensionOne/Basic.lean, line 180.

A separated scheme of finite type over a field k whose topological Krull dimension is at most one is H-quasi-projective over k.

theorem isHQuasiProjective_of_dimension_le_one
    {k : Type u} [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of k)) [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    (hdim : topologicalKrullDim (X : Type u) ≤ 1) :
    AlgebraicGeometry.IsHQuasiProjective f
Tag 0A26, a lemma

Tag 0A26 in the Stacks Project.

Stacks.HQuasiProjectiveDimensionOne.isProjectiveMorphism_of_isProper_of_topologicalKrullDim_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HQuasiProjectiveDimensionOne/Basic.lean, line 203.

A proper scheme over a field k whose topological Krull dimension is at most one is H-projective over k.

theorem isProjectiveMorphism_of_isProper_of_topologicalKrullDim_le_one
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f]
    (hdim : topologicalKrullDim (X : Type u) ≤ 1) :
    IsProjectiveMorphism f
Tag 0BXV, a lemma

Tag 0BXV in the Stacks Project.

Stacks.CurveProjectiveCompletion.exists_projective_completion_of_dimension_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/ProjectiveCompletion.lean, line 286. The attribute's comment: “the whole tag: all three clauses, for every separated scheme of finite type over k of dimension at most one”.

Let X be a separated scheme of finite type over a field k with dim(X) ≤ 1. Then there is an open immersion j : X ⟶ X̄ such that

  1. X̄ is H-projective over k, a closed subscheme of ℙᵈ_k for some d;
  2. j(X) is dense and scheme-theoretically dense in X̄;
  3. X̄ \ j(X) is a finite set of closed points of X̄.
theorem exists_projective_completion_of_dimension_le_one
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of k))
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    (hdim : topologicalKrullDim (X : Type u) ≤ 1) :
    ∃ (Y : Scheme.{u}) (q : Y ⟶ Spec (CommRingCat.of k)) (j : X ⟶ Y) (hj : IsOpenImmersion j),
      letI : IsOpenImmersion j := hj
      j ≫ q = f ∧ IsProjectiveMorphism q ∧ IsDominant j ∧
        Scheme.Opens.IsSchemeTheoreticallyDense j.opensRange ∧
        ((Set.range j.base)ᶜ).Finite ∧
        ∀ y : Y, y ∉ Set.range j.base → IsClosed ({y} : Set Y)
Tag 0BXW, a lemma

Tag 0BXW in the Stacks Project.

Stacks.CurveProjectiveCompletion.exists_projective_completion_discreteValuation_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/ProjectiveCompletionDiscreteValuation.lean, line 304.

[Stacks, Tag 0BXW]. Let X be a reduced separated scheme of finite type over a field k with dim(X) ≤ 1. Then there is an open immersion j : X ⟶ X' such that X' is H-projective over k, the image of j is dense and scheme-theoretically dense in X', the complement X' ∖ j(X) is a finite set of closed points, and the local ring of X' at each of those points is a discrete valuation ring.

The first step of the proof, [Stacks, Tag 0A25], is used in its reduced case Stacks.CurveProjectiveCompletion.isHQuasiProjective_of_isReduced.

theorem exists_projective_completion_discreteValuation_of_isReduced
    (k : Type u) [Field k] {X : Scheme.{u}} (p : X ⟶ Spec (CommRingCat.of k))
    [IsSeparated p] [LocallyOfFiniteType p] [QuasiCompact p] [AlgebraicGeometry.IsReduced X]
    (hdim : topologicalKrullDim (X : Type u) ≤ 1) :
    ∃ (Y : Scheme.{u}) (q : Y ⟶ Spec (CommRingCat.of k)) (j : X ⟶ Y) (hj : IsOpenImmersion j),
      letI : IsOpenImmersion j := hj
      j ≫ q = p ∧ IsProjectiveMorphism q ∧ IsDominant j ∧
        Scheme.Opens.IsSchemeTheoreticallyDense j.opensRange ∧
        ((Set.range j.base)ᶜ).Finite ∧
        ∀ y : Y, y ∉ Set.range j.base →
          IsClosed ({y} : Set Y) ∧
            ∃ _ : IsDomain (Y.presheaf.stalk y),
              IsDiscreteValuationRing (Y.presheaf.stalk y)
Tag 0GK5, a lemma

Tag 0GK5 in the Stacks Project.

AlgebraicGeometry.exists_isPurelyInseparable_smooth_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/SmoothNormalizationPurelyInseparable.lean, line 132. The attribute's comment: “clauses (1) and (2), with ν smooth over k'; clauses (3), (4), (5) not established”. References: SGA 4 XIV (1.11).

[Stacks, Tag 0GK5], clauses (1) and (2), with the normalization smooth over k'. Let k be a field and let X be a scheme of finite type over k with dim X ≤ 1. There is a finite purely inseparable extension k'/k such that the normalization of X_{k'} is smooth over k'.

Clauses (3), (4) and (5) of the source — the compactification j with dense image, the finite separable extensions k'_i/k' and the smooth projective geometrically irreducible pieces over them — are not established here; see the module docstring.

public theorem exists_isPurelyInseparable_smooth_normalization (k : Type u) [Field k]
    {X : Scheme.{u}} (p : X ⟶ Spec (.of k)) [LocallyOfFiniteType p] [QuasiCompact p]
    (hdim : topologicalKrullDim X ≤ 1) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k') (_ : Module.Finite k k')
      (_ : IsPurelyInseparable k k'),
      Smooth (normalizationOverField k' (pullback.fst (spectrumMap k k') p) ≫
        pullback.fst (spectrumMap k k') p)

AlgebraicGeometry.exists_isPurelyInseparable_dense_openImmersion_smooth_projective_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/SmoothProjectiveCompactificationCurve.lean, line 117. The attribute's comment: “clauses (3), (4) and (5) -- the whole diagram -- for a REDUCED X. The source's first move is to replace X by its reduction; everything after that move is proved here. The normalization of X_{k'} is exhibited as a DENSE OPEN SUBSCHEME of the disjoint union of the compactifications Ybar_i (clause 3), each of which is SMOOTH, PROJECTIVE and GEOMETRICALLY IRREDUCIBLE of dimension at most one over a finite SEPARABLE extension k'_i/k' (clauses 4 and 5), and the diagram commutes over Spec k'. What is NOT covered: the reduction step, i.e. the case of an X that is not reduced.”. References: EGA IV (17.15.14), “special case”; SGA 4 XIV (1.11), “special case”.

[Stacks, Tag 0GK5] for a reduced X. Let k be a field and let X be a reduced separated scheme of finite type over k with dim(X) ≤ 1. There is a finite purely inseparable extension k'/k, a finite family of schemes Ȳᵢ over Spec k', and a dense open immersion j from the normalization of X_{k'} into their disjoint union over Spec k', such that each Ȳᵢ is smooth, H-projective and geometrically irreducible of dimension at most one over a finite separable extension k'ᵢ/k'.

public theorem exists_isPurelyInseparable_dense_openImmersion_smooth_projective_of_isReduced
    (k : Type u) [Field k] {X : Scheme.{u}} (p : X ⟶ Spec (.of k))
    [IsSeparated p] [LocallyOfFiniteType p] [QuasiCompact p] [AlgebraicGeometry.IsReduced X]
    (hdim : topologicalKrullDim (X : Type u) ≤ 1) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k') (_ : Module.Finite k k')
      (_ : IsPurelyInseparable k k') (ι : Type u) (_ : Finite ι) (Ybar : ι → Scheme.{u})
      (sbar : (∐ Ybar) ⟶ Spec (.of k'))
      (K : ι → Type u) (_ : ∀ i, Field (K i)) (_ : ∀ i, Algebra k' (K i))
      (_ : ∀ i, Module.Finite k' (K i)) (_ : ∀ i, Algebra.IsSeparable k' (K i))
      (rbar : ∀ i, Ybar i ⟶ Spec (.of (K i)))
      (j : normalizationSchemeOverField k' (pullback.fst (spectrumMap k k') p) ⟶ ∐ Ybar)
      (_ : IsOpenImmersion j),
      Dense (Set.range j.base) ∧
        j ≫ sbar = normalizationOverField k' (pullback.fst (spectrumMap k k') p) ≫
            pullback.fst (spectrumMap k k') p ∧
          (∀ i, rbar i ≫ Spec.map (CommRingCat.ofHom (algebraMap k' (K i)))
              = Sigma.ι Ybar i ≫ sbar) ∧
            ∀ i, Smooth (rbar i) ∧ IsProjectiveMorphism (rbar i) ∧
              GeometricallyIrreducible (rbar i) ∧ topologicalKrullDim (Ybar i : Type u) ≤ 1

AlgebraicGeometry.exists_isPurelyInseparable_dense_openImmersion_smooth_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/SmoothProjectiveCompactificationCurve.lean, line 252. References: EGA IV (17.15.14), “special case”; SGA 4 XIV (1.11), “special case”.

[Stacks, Tag 0GK5]. Let k be a field and let X be a separated scheme of finite type over k with dim(X) ≤ 1. There is a finite purely inseparable extension k'/k (clause 1) such that the normalization of X_{k'} (clause 2) is a dense open subscheme (clause 3) of a finite disjoint union of schemes Ȳᵢ, each smooth, H-projective and geometrically irreducible of dimension at most one (clause 5) over a finite separable extension k'ᵢ/k' (clause 4), the whole diagram commuting over Spec k'.

public theorem exists_isPurelyInseparable_dense_openImmersion_smooth_projective
    (k : Type u) [Field k] {X : Scheme.{u}} (p : X ⟶ Spec (.of k))
    [IsSeparated p] [LocallyOfFiniteType p] [QuasiCompact p]
    (hdim : topologicalKrullDim (X : Type u) ≤ 1) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k') (_ : Module.Finite k k')
      (_ : IsPurelyInseparable k k') (ι : Type u) (_ : Finite ι) (Ybar : ι → Scheme.{u})
      (sbar : (∐ Ybar) ⟶ Spec (.of k'))
      (K : ι → Type u) (_ : ∀ i, Field (K i)) (_ : ∀ i, Algebra k' (K i))
      (_ : ∀ i, Module.Finite k' (K i)) (_ : ∀ i, Algebra.IsSeparable k' (K i))
      (rbar : ∀ i, Ybar i ⟶ Spec (.of (K i)))
      (j : normalizationSchemeOverField k' (pullback.fst (spectrumMap k k') p) ⟶ ∐ Ybar)
      (_ : IsOpenImmersion j),
      Dense (Set.range j.base) ∧
        j ≫ sbar = normalizationOverField k' (pullback.fst (spectrumMap k k') p) ≫
            pullback.fst (spectrumMap k k') p ∧
          (∀ i, rbar i ≫ Spec.map (CommRingCat.ofHom (algebraMap k' (K i)))
              = Sigma.ι Ybar i ≫ sbar) ∧
            ∀ i, Smooth (rbar i) ∧ IsProjectiveMorphism (rbar i) ∧
              GeometricallyIrreducible (rbar i) ∧ topologicalKrullDim (Ybar i : Type u) ≤ 1

AlgebraicGeometry.exists_isPurelyInseparable_normalization_coproduct_smooth_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/SmoothProjectiveNormalizationProper.lean, line 88. The attribute's comment: “clauses (3), (4) and (5) for a PROPER X, where the open immersion j of clause (3) is an isomorphism and the compactifications Ybar_i are the components Y_i of the normalization themselves. Clauses (1) and (2) -- the finite purely inseparable k'/k and the normalization of X_{k'} -- are reproved here as part of the diagram. What the general separated case still needs is the compactification of Stacks 0BXW applied to X before k' is chosen, together with the identification of the normalization of X_{k'} with the open part of the normalization of that compactification.”. References: EGA IV (17.15.14), “Proper case of 17.15.14”; SGA 4 XIV (1.11), “special case”.

[Stacks, Tag 0GK5] for a proper X. Let k be a field and let X be proper over k with dim(X) ≤ 1. There is a finite purely inseparable extension k'/k such that the normalization of X_{k'} is a finite coproduct of schemes Yᵢ, each smooth, H-projective and geometrically irreducible of dimension at most one over a finite separable extension k'ᵢ/k', compatibly with the structure morphisms.

public theorem exists_isPurelyInseparable_normalization_coproduct_smooth_projective
    (k : Type u) [Field k] {X : Scheme.{u}} (p : X ⟶ Spec (.of k)) [IsProper p]
    (hdim : topologicalKrullDim (X : Type u) ≤ 1) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k') (_ : Module.Finite k k')
      (_ : IsPurelyInseparable k k') (ι : Type u) (_ : Finite ι) (Y : ι → Scheme.{u})
      (e : normalizationSchemeOverField k' (pullback.fst (spectrumMap k k') p) ≅ ∐ Y)
      (K : ι → Type u) (_ : ∀ i, Field (K i)) (_ : ∀ i, Algebra k' (K i))
      (_ : ∀ i, Module.Finite k' (K i)) (_ : ∀ i, Algebra.IsSeparable k' (K i))
      (r : ∀ i, Y i ⟶ Spec (.of (K i))),
      (∀ i, r i ≫ Spec.map (CommRingCat.ofHom (algebraMap k' (K i))) =
          Sigma.ι Y i ≫ e.inv ≫
            normalizationOverField k' (pullback.fst (spectrumMap k k') p) ≫
              pullback.fst (spectrumMap k k') p) ∧
        ∀ i, Smooth (r i) ∧ IsProjectiveMorphism (r i) ∧ GeometricallyIrreducible (r i) ∧
          topologicalKrullDim (Y i : Type u) ≤ 1

AlgebraicGeometry.exists_isSeparable_smooth_isProjectiveMorphism_geometricallyIrreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/SmoothProperConnectedComponent.lean, line 98. The attribute's comment: “clauses (4) and (5), at one component: for a CONNECTED scheme Z smooth and proper over a field k with dim Z <= 1 -- that is, for one of the compactified pieces Ybar_i of the diagram -- the field k'_i = Gamma(Z, O_Z) of clause (4) is a finite SEPARABLE extension of k, and Z is SMOOTH, PROJECTIVE and GEOMETRICALLY IRREDUCIBLE of dimension at most one over it, which is clause (5). The assembly of the diagram -- decomposing the normalization into its components and transporting along the open immersion j of clause (3) -- is not done here; clauses (1) and (2) are carried by AlgebraicGeometry.exists_isPurelyInseparable_smooth_normalization.”.

[Stacks, Tag 0GK5], clauses (4) and (5) at one component. Let Z be a connected scheme, smooth and proper over a field k, of dimension at most one. Then there is a finite separable extension K/k and a morphism r : Z ⟶ Spec K over k which is smooth, H-projective and geometrically irreducible, with dim(Z) ≤ 1.

The field is K = Γ(Z, 𝒪_Z) and the morphism is the canonical Z ⟶ Spec Γ(Z, 𝒪_Z), exactly as in the source.

public theorem exists_isSeparable_smooth_isProjectiveMorphism_geometricallyIrreducible
    (k : Type u) [Field k] {Z : Scheme.{u}} (q : Z ⟶ Spec (.of k))
    [IsProper q] [Smooth q] [ConnectedSpace Z]
    (hdim : topologicalKrullDim (Z : Type u) ≤ 1) :
    ∃ (K : Type u) (_ : Field K) (_ : Algebra k K) (_ : Module.Finite k K)
      (_ : Algebra.IsSeparable k K) (r : Z ⟶ Spec (.of K)),
      r ≫ Spec.map (CommRingCat.ofHom (algebraMap k K)) = q ∧
        Smooth r ∧ IsProjectiveMorphism r ∧ GeometricallyIrreducible r ∧
        topologicalKrullDim (Z : Type u) ≤ 1
Tag 0B8Y, a lemma

Tag 0B8Y in the Stacks Project.

AlgebraicGeometry.isDiscreteValuationRing_stalk_tfae_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CurveLocalRing/Basic.lean, line 144. The attribute's comment: “(1), (2) and (3)”. References: EGA II (7.4.5); EGA II (7.1.6), “curve stalk case”; EGA IV (6.7.5), “partial”; SGA 7 IX (3.2.1), “special case”.

Items (1), (2) and (3) of [Stacks, Tag 0B8Y]. At a closed point x of a curve over a field the local ring 𝒪_{X,x} is regular if and only if it is normal if and only if it is a discrete valuation ring.

public theorem isDiscreteValuationRing_stalk_tfae_of_isCurve [IsCurve k f] {x : X}
    (hx : IsClosed ({x} : Set X)) :
    List.TFAE [IsRegularLocalRing (X.presheaf.stalk x), IsNormalRing (X.presheaf.stalk x),
      IsDiscreteValuationRing (X.presheaf.stalk x)]

AlgebraicGeometry.isEffectiveCartierDivisor_closedPoint_tfae_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CurveLocalRing/EffectiveCartier.lean, line 130. The attribute's comment: “(1), (2), (3), (4) and (5)”. References: EGA II (7.4.5); EGA II (7.1.6), “curve stalk case”; EGA IV (6.7.5), “partial”.

At a closed point x of a curve over a field the following are equivalent: 𝒪_{X,x} is regular; 𝒪_{X,x} is normal; 𝒪_{X,x} is a discrete valuation ring; and the sheaf of ideals of the reduced closed subscheme {x} is an invertible 𝒪_X-module, which is to say that x is an effective Cartier divisor on X.

public theorem isEffectiveCartierDivisor_closedPoint_tfae_of_isCurve [IsCurve k f] {x : X}
    (hx : IsClosed ({x} : Set X)) :
    List.TFAE [IsRegularLocalRing (X.presheaf.stalk x), IsNormalRing (X.presheaf.stalk x),
      IsDiscreteValuationRing (X.presheaf.stalk x),
      Stacks.Divisors.IsEffectiveCartierDivisor
        (Scheme.IdealSheafData.vanishingIdeal (⟨{x}, hx⟩ : Closeds X))]

AlgebraicGeometry.smoothAt_closedPoint_tfae_of_isCurve_of_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CurveLocalRing/Smooth.lean, line 49. The attribute's comment: “(1), (2), (3), (4), (5) and (6), for κ(x) separable over k”. References: EGA IV (17.15.1), “the smoothness item”; SGA 1 II (5.4), “κ(x)/k separable”.

Smoothness at a closed point of a curve, for a separable residue field. Let k be a field, let X be a curve over k and let x be a closed point of X whose residue field is separable over k. Then the following are equivalent: 𝒪_{X,x} is regular; 𝒪_{X,x} is normal; 𝒪_{X,x} is a discrete valuation ring; the sheaf of ideals of the reduced closed subscheme {x} is an invertible 𝒪_X-module, which is to say that x is an effective Cartier divisor on X; and X → Spec k is smooth at x.

public theorem smoothAt_closedPoint_tfae_of_isCurve_of_isSeparable [IsCurve k f] {x : X}
    (hx : IsClosed ({x} : Set X))
    (hsep : letI : Algebra k (X.residueField x) :=
        ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
      Algebra.IsSeparableExtension k (X.residueField x)) :
    List.TFAE [IsRegularLocalRing (X.presheaf.stalk x), IsNormalRing (X.presheaf.stalk x),
      IsDiscreteValuationRing (X.presheaf.stalk x),
      Stacks.Divisors.IsEffectiveCartierDivisor
        (Scheme.IdealSheafData.vanishingIdeal (⟨{x}, hx⟩ : Closeds X)),
      InfinitesimalLifting.SmoothAt f x]

AlgebraicGeometry.smoothAt_closedPoint_tfae_of_isCurve_of_perfectField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CurveLocalRing/Smooth.lean, line 73. The attribute's comment: “(1), (2), (3), (4), (5) and (6), for k perfect”. References: EGA IV (17.15.2), “the smoothness item”; EGA IV (6.7.5), “special case”; SGA 1 II (5.4), “k perfect”.

Smoothness at a closed point of a curve, over a perfect field. Let k be a perfect field, let X be a curve over k and let x be a closed point of X. Then the following are equivalent: 𝒪_{X,x} is regular; 𝒪_{X,x} is normal; 𝒪_{X,x} is a discrete valuation ring; the sheaf of ideals of the reduced closed subscheme {x} is an invertible 𝒪_X-module, which is to say that x is an effective Cartier divisor on X; and X → Spec k is smooth at x.

public theorem smoothAt_closedPoint_tfae_of_isCurve_of_perfectField [PerfectField k] [IsCurve k f]
    {x : X} (hx : IsClosed ({x} : Set X)) :
    List.TFAE [IsRegularLocalRing (X.presheaf.stalk x), IsNormalRing (X.presheaf.stalk x),
      IsDiscreteValuationRing (X.presheaf.stalk x),
      Stacks.Divisors.IsEffectiveCartierDivisor
        (Scheme.IdealSheafData.vanishingIdeal (⟨{x}, hx⟩ : Closeds X)),
      InfinitesimalLifting.SmoothAt f x]
Tag 0H1F, a remark

Tag 0H1F in the Stacks Project.

AlgebraicGeometry.exists_isRegular_isProjectiveMorphism_compactification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/RegularCompactification.lean, line 141. The attribute's comment: “the regular projective compactification”.

Let k be a field and let X be a regular curve over k. Then there is a nonsingular projective curve X̄ over k and an open immersion j : X ⟶ X̄ over k whose complement is a finite set of closed points of X̄.

public theorem exists_isRegular_isProjectiveMorphism_compactification
    (k : Type u) [Field k] {X : Scheme.{u}} (p : X ⟶ Spec (.of k)) [IsCurve k p]
    (hX : IsRegular X) :
    ∃ (Y : Scheme.{u}) (q : Y ⟶ Spec (.of k)) (j : X ⟶ Y) (hj : IsOpenImmersion j),
      letI : IsOpenImmersion j := hj
      j ≫ q = p ∧ IsCurve k q ∧ IsProjectiveMorphism q ∧ IsRegular Y ∧
        ((Set.range j.base)ᶜ).Finite ∧
        ∀ y : Y, y ∉ Set.range j.base → IsClosed ({y} : Set Y)

AlgebraicGeometry.exists_smooth_isProjectiveMorphism_compactification_of_perfectField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/RegularCompactification.lean, line 181. The attribute's comment: “the smooth projective compactification over a perfect field”.

Let k be a perfect field and let X be a regular curve over k. Then X is smooth over k, and there is a nonsingular projective curve X̄ over k, smooth over k, with an open immersion j : X ⟶ X̄ over k whose complement is a finite set of closed points of X̄.

public theorem exists_smooth_isProjectiveMorphism_compactification_of_perfectField
    (k : Type u) [Field k] [PerfectField k] {X : Scheme.{u}} (p : X ⟶ Spec (.of k))
    [IsCurve k p] (hX : IsRegular X) :
    Smooth p ∧ ∃ (Y : Scheme.{u}) (q : Y ⟶ Spec (.of k)) (j : X ⟶ Y) (hj : IsOpenImmersion j),
      letI : IsOpenImmersion j := hj
      j ≫ q = p ∧ IsCurve k q ∧ IsProjectiveMorphism q ∧ IsRegular Y ∧ Smooth q ∧
        ((Set.range j.base)ᶜ).Finite ∧
        ∀ y : Y, y ∉ Set.range j.base → IsClosed ({y} : Set Y)
Tag 0A27, a lemma

Tag 0A27 in the Stacks Project.

AlgebraicGeometry.isAffine_or_isProjectiveMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/AffineOrProjective.lean, line 209.

Let k be a field and let X be a curve over k. Then X is an affine scheme or X is H-projective over k.

theorem isAffine_or_isProjectiveMorphism
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsCurve k f] :
    IsAffine X ∨ IsProjectiveMorphism f
Tag 0A28, a lemma

Tag 0A28 in the Stacks Project.

AlgebraicGeometry.isAffine_of_topologicalKrullDim_le_one_of_forall_component_not_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/OneDimensional/AffineOfNoProperComponent.lean, line 205.

[Stacks, Tag 0A28]. Let k be a field and let X be a separated scheme of finite type over k with dim(X) ≤ 1. If no irreducible component of X, taken with its reduced induced closed subscheme structure, is proper over k of dimension one, then X is an affine scheme.

Each component is integral, and separated and of finite type over k of dimension at most one. A one-dimensional component is therefore a curve over k, so [Stacks, Tag 0A27] makes it affine or H-projective over k, and the latter would make it proper over k, which hcomponent forbids; a zero-dimensional component is affine by [Stacks, Tag 06LH]. The components are finitely many, their coproduct is affine, and the induced morphism to X is finite and surjective, so [Stacks, Tag 01YQ] makes X affine.

theorem isAffine_of_topologicalKrullDim_le_one_of_forall_component_not_isProper
    (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    (hdim : topologicalKrullDim X ≤ 1)
    (hcomponent : ∀ Z : irreducibleComponents X,
      topologicalKrullDim (Scheme.IdealSheafData.vanishingIdeal
          (⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.2⟩ : Closeds X)).subscheme = 1 →
        ¬ IsProper ((Scheme.IdealSheafData.vanishingIdeal
          (⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.2⟩ : Closeds X)).subschemeι ≫ f)) :
    IsAffine X
Sources
LeanAlgebraicGeometry.IsCurve · AlgebraicGeometry.not_isProper_compl_singleton · Stacks.HQuasiProjectiveDimensionOne.isHQuasiProjective_of_topologicalKrullDim_eq_zero · Stacks.HQuasiProjectiveDimensionOne.isHQuasiProjective_of_dimension_le_one · Stacks.HQuasiProjectiveDimensionOne.isProjectiveMorphism_of_isProper_of_topologicalKrullDim_le_one · Stacks.CurveProjectiveCompletion.exists_projective_completion_of_dimension_le_one · Stacks.CurveProjectiveCompletion.exists_projective_completion_discreteValuation_of_isReduced · AlgebraicGeometry.exists_isPurelyInseparable_smooth_normalization

Section33.44 Degrees on curves#

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

Tag 0AYR, a definition

Tag 0AYR in the Stacks Project.

AlgebraicGeometry.curveDegree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/Degree.lean, line 82. The attribute's comment: “finite locally free case”.

The degree of a finite locally free sheaf of constant rank on a proper scheme of dimension at most one over a field.

public noncomputable def curveDegree (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f]
    (_hdim : topologicalKrullDim X ≤ 1) (E : X.Modules) (rank : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E rank] : ℤ

AlgebraicGeometry.invertibleCurveDegree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/Degree.lean, line 106. The attribute's comment: “invertible case”.

The degree of an invertible sheaf on a proper scheme of dimension at most one over a field: its Euler characteristic minus the Euler characteristic of the structure sheaf.

public noncomputable def invertibleCurveDegree (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f]
    (_hdim : topologicalKrullDim X ≤ 1) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L] : ℤ
Tag 0B59, a lemma

Tag 0B59 in the Stacks Project.

AlgebraicGeometry.curveDegree_baseChange_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/DegreeFieldExtension.lean, line 68.

Stacks Project, Tag 0B59. Let k'/k be an extension of fields, let X be a proper scheme of dimension at most one over k and let ℰ be a finite locally free 𝒪_X-module of constant rank. Then the degree of ℰ over k equals the degree of its inverse image on the base change X_{k'} over k'.

theorem curveDegree_baseChange_field (k k' : Type u) [Field k] [Field k'] [Algebra k k']
    {X' X : Scheme.{u}} (g' : X' ⟶ X) (f' : X' ⟶ Spec (.of k')) (f : X ⟶ Spec (.of k))
    (h : IsPullback g' f' f (Spec.map (CommRingCat.ofHom (algebraMap k k')))) [IsProper f]
    (hdim : topologicalKrullDim X ≤ 1) (E : X.Modules) (rank : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E rank] :
    @curveDegree k' _ X' f' (MorphismProperty.of_isPullback (P := @IsProper) h inferInstance)
        ((topologicalKrullDim_baseChange k k' g' f' f h).trans_le hdim)
        ((Scheme.Modules.pullback g').obj E) rank
        (isFiniteLocallyFreeOfRank_pullback g' E rank) =
      curveDegree k f hdim E rank
Tag 0AYS, a lemma

Tag 0AYS in the Stacks Project.

AlgebraicGeometry.curveDegree_add_of_shortExact_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/DegreeAdditivityUnconditional.lean, line 49. The attribute's comment: “deg(ℰ₂) = deg(ℰ₁) + deg(ℰ₃) for a short exact sequence of locally free modules of finite constant rank on a proper scheme of dimension at most one over a field”.

Let k be a field and let X be a scheme proper over k of dimension at most one. For a short exact sequence 0 ⟶ ℰ₁ ⟶ ℰ₂ ⟶ ℰ₃ ⟶ 0 of locally free 𝒪_X-modules of finite constant ranks r₁, r₂, r₃, deg(ℰ₂) = deg(ℰ₁) + deg(ℰ₃).

public theorem curveDegree_add_of_shortExact_of_isProper (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] (hdim : topologicalKrullDim X ≤ 1)
    (S : ShortComplex X.Modules) (hS : S.ShortExact) (r₁ r₂ r₃ : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₁ r₁]
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₂ r₂]
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₃ r₃] :
    curveDegree k f hdim S.X₂ r₂ =
      curveDegree k f hdim S.X₁ r₁ + curveDegree k f hdim S.X₃ r₃

AlgebraicGeometry.curveDegree_add_of_shortExact_of_cohomologyFiniteDimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/EulerChar/CoherentFiniteness.lean, line 252. The attribute's comment: “deg(ℰ₂) = deg(ℰ₁) + deg(ℰ₃); hfin is [Stacks, Tag 02O6] for X”.

Additivity of the degree along a short exact sequence. For a short exact sequence 0 ⟶ ℰ₁ ⟶ ℰ₂ ⟶ ℰ₃ ⟶ 0 of finite locally free 𝒪_X-modules of constant ranks r₁, r₂, r₃ on a scheme X proper over a field k and of dimension at most one, deg(ℰ₂) = deg(ℰ₁) + deg(ℰ₃).

The single hypothesis hfin is [Stacks, Tag 02O6] for X; everything else the source uses — additivity of the Euler characteristic, additivity of the constant rank, and the empty scheme — is discharged. hfin is now itself a theorem, so the tag is additionally registered on the form that takes no finiteness hypothesis at all, AlgebraicGeometry.curveDegree_add_of_shortExact_of_isProper of StacksFrontier/AlgebraicGeometry/Variety/Curve/DegreeAdditivityUnconditional.lean, which applies this theorem to AlgebraicGeometry.forall_finiteDimensional_cohomologyOverField_of_isProper.

public theorem curveDegree_add_of_shortExact_of_cohomologyFiniteDimensional (k : Type u)
    [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f]
    (hfin : CohomologyFiniteDimensionalOverFieldOn k f) (hdim : topologicalKrullDim X ≤ 1)
    (S : ShortComplex X.Modules) (hS : S.ShortExact) (r₁ r₂ r₃ : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₁ r₁]
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₂ r₂]
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₃ r₃] :
    curveDegree k f hdim S.X₂ r₂ =
      curveDegree k f hdim S.X₁ r₁ + curveDegree k f hdim S.X₃ r₃
Tag 0AYU, a lemma

Tag 0AYU in the Stacks Project.

AlgebraicGeometry.curveDegree_pullback_eq_of_bijOn_genericPointsOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CurveDegreeInvariance/Morphism.lean, line 497. References: SGA 6 X (4.4), “special case”.

[Stacks, Tag 0AYU], the "more generally" statement. Let k be a field and let g : X' ⟶ X be a morphism over k between schemes proper over k and of dimension at most one which induces a bijection between the generic points of the one-dimensional irreducible components of X' and those of X, and isomorphisms of local rings at the points of X' involved. Let ℰ be finite locally free of constant rank n on X. Then

deg(g^*ℰ) = deg(ℰ).

hbij and hstalk are the tag's own hypotheses — the bijection on the generic points of the one-dimensional components and the isomorphisms of local rings at the corresponding points — and the source's "more generally" clause implies its first, birational, sentence, which is not separately derived here. The finiteness input [Stacks, Tag 02O6] over a field is not assumed: it is AlgebraicGeometry.cohomologyFiniteDimensionalOverField_of_isProper. The projection formula [Stacks, Tag 01E8] at g, the source's displayed equation g_*g^*ℰ ≅ ℰ ⊗_{𝒪_X} g_*𝒪_{X'}, is proved rather than assumed, by projectionFormula_iso_of_isFiniteLocallyFreeOfRank above.

The proof is the source's. The bijection on generic points makes g finite, so the cohomology of X' is read on X through g_*; the isomorphisms of local rings make the kernel and the cokernel of 𝒪_X ⟶ g_*𝒪_{X'} vanish at the generic points of the one-dimensional components, hence give them zero-dimensional support, so clause (5) of [Stacks, Tag 0AYT] applies at both; and the computation of CurveDegreeInvariance/Basic.lean collapses the difference of the two degrees to zero.

theorem curveDegree_pullback_eq_of_bijOn_genericPointsOne (k : Type u) [Field k]
    {X' X : Scheme.{u}} (p' : X' ⟶ Spec (.of k)) (p : X ⟶ Spec (.of k))
    [IsProper p'] [IsProper p]
    (hdimX' : topologicalKrullDim (X' : Type u) ≤ 1)
    (hdimX : topologicalKrullDim (X : Type u) ≤ 1)
    (g : X' ⟶ X) (hgOver : g ≫ p = p')
    (hbij : Set.BijOn g (genericPointsOne X') (genericPointsOne X))
    (E : X.Modules) (n : ℕ) [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E n]
    (hstalk : ∀ z ∈ genericPointsOne X', IsIso (g.stalkMap z)) :
    @curveDegree k _ X' p' _ hdimX' ((Scheme.Modules.pullback g).obj E) n
        (isFiniteLocallyFreeOfRank_pullback g E n) =
      curveDegree k p hdimX E n

AlgebraicGeometry.curveDegree_pullback_eq_of_bijOn_genericPointsOne_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CurveDegreeInvariance/Unconditional.lean, line 66. The attribute's comment: “the 'more generally' statement, with no hypothesis beyond the tag's own”. References: SGA 6 X (4.4), “special case”.

[Stacks, Tag 0AYU], the "more generally" statement, with no hypothesis beyond the tag's own. Let k be a field and let g : X' ⟶ X be a morphism over k between schemes proper over k and of dimension at most one which induces a bijection between the generic points of the one-dimensional irreducible components of X' and those of X, and isomorphisms of the local rings at the points of X' involved. Let ℰ be finite locally free of constant rank n on X. Then

deg(g^*ℰ) = deg(ℰ).

hbij and hstalk are the tag's own hypotheses, and they are all that curveDegree_pullback_eq_of_bijOn_genericPointsOne takes: [Stacks, Tag 02O6] over a field and the projection formula at g are proved there rather than carried.

theorem curveDegree_pullback_eq_of_bijOn_genericPointsOne_of_isProper (k : Type u) [Field k]
    {X' X : Scheme.{u}} (p' : X' ⟶ Spec (.of k)) (p : X ⟶ Spec (.of k))
    [IsProper p'] [IsProper p]
    (hdimX' : topologicalKrullDim (X' : Type u) ≤ 1)
    (hdimX : topologicalKrullDim (X : Type u) ≤ 1)
    (g : X' ⟶ X) (hgOver : g ≫ p = p')
    (hbij : Set.BijOn g (genericPointsOne X') (genericPointsOne X))
    (E : X.Modules) (n : ℕ) [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E n]
    (hstalk : ∀ z ∈ genericPointsOne X', IsIso (g.stalkMap z)) :
    @curveDegree k _ X' p' _ hdimX' ((Scheme.Modules.pullback g).obj E) n
        (isFiniteLocallyFreeOfRank_pullback g E n) =
      curveDegree k p hdimX E n
Tag 0AYV, a lemma

Tag 0AYV in the Stacks Project.

AlgebraicGeometry.exists_eulerCharacteristic_tensorSheaf_eq_fiberRank_mul_curveDegree_add_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CurveTensorEulerUnit/Unconditional.lean, line 65.

[Stacks, Tag 0AYV], with no hypothesis. Let k be a field, let X be a proper curve over k with generic point ξ, let ℰ be finite locally free of rank n and let ℱ be coherent. Then

χ(X, ℰ ⊗ ℱ) = r·deg(ℰ) + n·χ(X, ℱ),

where r = dim_{κ(ξ)} ℱ_ξ is the rank of ℱ at the generic point.

public theorem exists_eulerCharacteristic_tensorSheaf_eq_fiberRank_mul_curveDegree_add_of_isCurve
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsCurve k f] [IsProper f] (E : X.Modules) (n : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E n]
    (F : X.Modules) [SheafOfModules.IsCoherent F] :
    ∃ h : ((((Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨((X.toRingedSpace)).presheaf, ((X.toRingedSpace)).IsSheaf⟩).obj (E)).obj (F))).IsCoherent,
      @eulerCharacteristic k _ X f _
          ((((Stacks.SheafOfModules.Tensor.sheafTensor
            ⟨((X.toRingedSpace)).presheaf, ((X.toRingedSpace)).IsSheaf⟩).obj (E)).obj (F))) h =
        (Scheme.Modules.fiberRank F (genericPoint X) : ℤ) *
            curveDegree k f (le_of_eq (IsCurve.topologicalKrullDim_eq_one (f := f))) E n +
          (n : ℤ) * eulerCharacteristic k f F

AlgebraicGeometry.eulerCharacteristic_tensorSheaf_eq_fiberRank_mul_curveDegree_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CurveTensorEulerUnit/Unconditional.lean, line 92.

[Stacks, Tag 0AYV], with the coherence h of ℰ ⊗ ℱ taken as an argument instead of produced existentially: for ℰ finite locally free of rank n and ℱ coherent on a proper curve X over a field k, χ(X, ℰ ⊗ ℱ) = r·deg(ℰ) + n·χ(X, ℱ), where r = dim_{κ(ξ)} ℱ_ξ is the rank of ℱ at the generic point ξ.

public theorem eulerCharacteristic_tensorSheaf_eq_fiberRank_mul_curveDegree_add
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [IsCurve k f] [IsProper f] (E : X.Modules) (n : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E n]
    (F : X.Modules) [SheafOfModules.IsCoherent F]
    (h : ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X.toRingedSpace)).presheaf,
        ((X.toRingedSpace)).IsSheaf⟩).obj (E)).obj (F))).IsCoherent) :
    @eulerCharacteristic k _ X f _
        ((((Stacks.SheafOfModules.Tensor.sheafTensor
          ⟨((X.toRingedSpace)).presheaf, ((X.toRingedSpace)).IsSheaf⟩).obj (E)).obj (F))) h =
      (Scheme.Modules.fiberRank F (genericPoint X) : ℤ) *
          curveDegree k f (le_of_eq (IsCurve.topologicalKrullDim_eq_one (f := f))) E n +
        (n : ℤ) * eulerCharacteristic k f F
Tag 0AYW, a lemma

Tag 0AYW in the Stacks Project.

Stacks.AlgebraicGeometry.ComponentDegreeDevissage.curveDegree_eq_finsum_componentDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ComponentDegreeDevissage/Basic.lean, line 407.

The degree of a finite locally free module of constant rank on a scheme proper over a field and of dimension at most one is the multiplicity-weighted sum of its degrees on the reduced one-dimensional components:

deg(ℰ) = ∑ᶠ ξ, m(ξ) · deg(ℰ|_{C(ξ)}).

theorem curveDegree_eq_finsum_componentDegree [IsProper f]
    (hX : topologicalKrullDim X ≤ 1) (E : X.Modules) (rank : ℕ)
    [_root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E rank] :
    curveDegree k f hX E rank =
      ∑ᶠ ξ : genericPointsOne X,
        (componentMultiplicity X ξ : ℤ) * componentDegree k f hX E rank ξ

Stacks.AlgebraicGeometry.ComponentDegreeDevissage.exists_curveDegree_eq_finsum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ComponentDegreeDevissage/Basic.lean, line 431.

The component formula for the degree in existential form: each reduced one-dimensional component is proper over the base, has dimension at most one and carries a restriction of ℰ that is again finite locally free of the same rank, and the component formula holds with respect to those three proofs.

theorem exists_curveDegree_eq_finsum [IsProper f]
    (hX : topologicalKrullDim X ≤ 1) (E : X.Modules) (rank : ℕ)
    [_root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E rank] :
    ∃ (hproper : ∀ ξ : genericPointsOne X, IsProper (reducedComponentι X ξ ≫ f))
      (hdimC : ∀ ξ : genericPointsOne X, topologicalKrullDim (reducedComponent X ξ) ≤ 1)
      (hrank : ∀ ξ : genericPointsOne X,
        _root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
          ((Scheme.Modules.pullback (reducedComponentι X ξ)).obj E) rank),
      curveDegree k f hX E rank =
        ∑ᶠ ξ : genericPointsOne X,
          (componentMultiplicity X ξ : ℤ) *
            @curveDegree k _ (reducedComponent X ξ) (reducedComponentι X ξ ≫ f)
              (hproper ξ) (hdimC ξ)
              ((Scheme.Modules.pullback (reducedComponentι X ξ)).obj E) rank (hrank ξ)

Stacks.AlgebraicGeometry.ComponentDegrees.curveDegree_eq_finsum_componentDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ComponentMultiplicity/Devissage.lean, line 198. The attribute's comment: “the component formula, from the two steps of the source argument”.

Stacks 0AYW. The degree of a finite locally free module of constant rank on a proper scheme of dimension at most one over a field is the multiplicity-weighted sum of its degrees on the reduced one-dimensional components.

theorem curveDegree_eq_finsum_componentDegree
    (hreduce : curveDegree k f hX E rank =
      ∑ᶠ ξ : genericPointsOne X, @curveDegree k _ (Y ξ) (i ξ ≫ f) (hproper ξ) (hdimY ξ)
        ((Scheme.Modules.pullback (i ξ)).obj E) rank
        (_root_.AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback (i ξ) E rank))
    (hirreducible : ∀ ξ : genericPointsOne X,
      @curveDegree k _ (Y ξ) (i ξ ≫ f) (hproper ξ) (hdimY ξ)
          ((Scheme.Modules.pullback (i ξ)).obj E) rank
          (_root_.AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback (i ξ) E rank) =
        (componentMultiplicity X ξ : ℤ) * componentDegree k f hX E rank ξ) :
    curveDegree k f hX E rank =
      ∑ᶠ ξ : genericPointsOne X,
        (componentMultiplicity X ξ : ℤ) * componentDegree k f hX E rank ξ

Stacks.AlgebraicGeometry.ComponentDegrees.exists_curveDegree_eq_finsum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ComponentMultiplicity/Devissage.lean, line 219. The attribute's comment: “the existential form the source states”.

Stacks 0AYW, in the existential form the source states: each reduced one-dimensional component is proper over the base, has dimension at most one and carries a restriction of ℰ that is again finite locally free of the same rank, and the component formula holds with respect to those three proofs.

theorem exists_curveDegree_eq_finsum
    (hreduce : curveDegree k f hX E rank =
      ∑ᶠ ξ : genericPointsOne X, @curveDegree k _ (Y ξ) (i ξ ≫ f) (hproper ξ) (hdimY ξ)
        ((Scheme.Modules.pullback (i ξ)).obj E) rank
        (_root_.AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback (i ξ) E rank))
    (hirreducible : ∀ ξ : genericPointsOne X,
      @curveDegree k _ (Y ξ) (i ξ ≫ f) (hproper ξ) (hdimY ξ)
          ((Scheme.Modules.pullback (i ξ)).obj E) rank
          (_root_.AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback (i ξ) E rank) =
        (componentMultiplicity X ξ : ℤ) * componentDegree k f hX E rank ξ) :
    ∃ (hproperC : ∀ ξ : genericPointsOne X, IsProper (reducedComponentι X ξ ≫ f))
      (hdimC : ∀ ξ : genericPointsOne X, topologicalKrullDim (reducedComponent X ξ) ≤ 1)
      (hrank : ∀ ξ : genericPointsOne X,
        _root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
          ((Scheme.Modules.pullback (reducedComponentι X ξ)).obj E) rank),
      curveDegree k f hX E rank =
        ∑ᶠ ξ : genericPointsOne X,
          (componentMultiplicity X ξ : ℤ) *
            @curveDegree k _ (reducedComponent X ξ) (reducedComponentι X ξ ≫ f)
              (hproperC ξ) (hdimC ξ)
              ((Scheme.Modules.pullback (reducedComponentι X ξ)).obj E) rank (hrank ξ)

Stacks.AlgebraicGeometry.ComponentDegrees.curveDegree_eq_sum_componentDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ComponentMultiplicity/Devissage.lean, line 246. The attribute's comment: “the component formula as a finite sum”.

Stacks 0AYW with the locally finite sum read as a finite sum over the components. This is the shape in which a consumer that already has the components as a Fintype uses the formula.

theorem curveDegree_eq_sum_componentDegree [Fintype (genericPointsOne X)]
    (hreduce : curveDegree k f hX E rank =
      ∑ᶠ ξ : genericPointsOne X, @curveDegree k _ (Y ξ) (i ξ ≫ f) (hproper ξ) (hdimY ξ)
        ((Scheme.Modules.pullback (i ξ)).obj E) rank
        (_root_.AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback (i ξ) E rank))
    (hirreducible : ∀ ξ : genericPointsOne X,
      @curveDegree k _ (Y ξ) (i ξ ≫ f) (hproper ξ) (hdimY ξ)
          ((Scheme.Modules.pullback (i ξ)).obj E) rank
          (_root_.AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback (i ξ) E rank) =
        (componentMultiplicity X ξ : ℤ) * componentDegree k f hX E rank ξ) :
    curveDegree k f hX E rank =
      ∑ ξ : genericPointsOne X,
        (componentMultiplicity X ξ : ℤ) * componentDegree k f hX E rank ξ

Stacks.AlgebraicGeometry.ComponentDegrees.curveDegree_eq_finsum_componentDegree_of_stalk_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ComponentMultiplicity/Devissage.lean, line 273. The attribute's comment: “the component formula, from the reduction to the irreducible case”.

Stacks 0AYW, with the first paragraph of the source proof discharged from the reduction to a finite family of closed subschemes.

The family Zs is the source's Xᵢ, the scheme-theoretic closures of the complements of the other components, enumerated by 0, …, N - 1; σ picks out the member attached to a given one-dimensional component, and hzero says the remaining members — the zero-dimensional components — contribute nothing.

theorem curveDegree_eq_finsum_componentDegree_of_stalk_bijective
    {Zs : ℕ → Scheme.{u}} (ι : ∀ j, Zs j ⟶ X) [∀ j, IsClosedImmersion (ι j)] (N : ℕ)
    (σ : genericPointsOne X → Fin N) (hσ : Function.Injective σ)
    (Z : Set X) (hZfin : Z.Finite) (hZcl : ∀ x ∈ Z, IsClosed ({x} : Set X))
    (hbij : ∀ x ∉ Z, Function.Bijective (ConcreteCategory.hom
      ((_root_.AlgebraicGeometry.SheafOfModules.stalkAddCommGroupFunctor X.ringCatSheaf x).map
        (Scheme.Modules.pushforwardUnitSeriesMap ι N))))
    (hirreducible : ∀ ξ : genericPointsOne X,
      @curveDegree k _ (Zs (σ ξ)) (ι (σ ξ) ≫ f) _
          (le_trans (IsClosedImmersion.isClosedEmbedding
            (ι (σ ξ))).isInducing.topologicalKrullDim_le hX)
          ((Scheme.Modules.pullback (ι (σ ξ))).obj E) rank
          (_root_.AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback (ι (σ ξ)) E rank) =
        (componentMultiplicity X ξ : ℤ) * componentDegree k f hX E rank ξ)
    (hzero : ∀ j : Fin N, (∀ ξ : genericPointsOne X, σ ξ ≠ j) →
      @curveDegree k _ (Zs j) (ι j ≫ f) _
        (le_trans (IsClosedImmersion.isClosedEmbedding
          (ι j)).isInducing.topologicalKrullDim_le hX)
        ((Scheme.Modules.pullback (ι j)).obj E) rank
        (_root_.AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback (ι j) E rank) = 0) :
    curveDegree k f hX E rank =
      ∑ᶠ ξ : genericPointsOne X,
        (componentMultiplicity X ξ : ℤ) * componentDegree k f hX E rank ξ

Stacks.AlgebraicGeometry.ComponentDegrees.curveDegree_eq_finsum_componentDegree_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ComponentMultiplicity/Unconditional.lean, line 455.

[Stacks, Tag 0AYW]. The degree of a finite locally free module of constant rank on a proper scheme of dimension at most one over a field is the multiplicity-weighted sum of its degrees on the reduced one-dimensional components.

The four steps are: the degree is the quantity D(𝒫) = χ(𝒫 ⊗ ℰ) − n·χ(𝒫) of [Stacks, Tag 0AYU] at 𝒫 = 𝒪_X; D is additive along the dévissage of [Stacks, Tag 01YF] applied to 𝒪_X; at each layer D is the weighted sum of the component degrees, the weights being the lengths of the layer at the generic points; and those lengths add up to the multiplicities.

theorem curveDegree_eq_finsum_componentDegree_of_isProper (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] (hX : topologicalKrullDim X ≤ 1)
    (E : X.Modules) (rank : ℕ)
    [_root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E rank] :
    _root_.AlgebraicGeometry.curveDegree k f hX E rank =
      ∑ᶠ ξ : genericPointsOne X,
        (componentMultiplicity X ξ : ℤ) * componentDegree k f hX E rank ξ

Stacks.AlgebraicGeometry.ComponentDegrees.exists_curveDegree_eq_finsum_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ComponentMultiplicity/Unconditional.lean, line 526. The attribute's comment: “the existential form the source states, with no hypothesis”.

[Stacks, Tag 0AYW], in the existential form the source states: each reduced one-dimensional component is proper over the base, has dimension at most one and carries a restriction of ℰ that is again finite locally free of the same rank, and the component formula holds with respect to those three proofs.

theorem exists_curveDegree_eq_finsum_of_isProper (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] (hX : topologicalKrullDim X ≤ 1)
    (E : X.Modules) (rank : ℕ)
    [_root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E rank] :
    ∃ (hproperC : ∀ ξ : genericPointsOne X, IsProper (reducedComponentι X ξ ≫ f))
      (hdimC : ∀ ξ : genericPointsOne X, topologicalKrullDim (reducedComponent X ξ) ≤ 1)
      (hrank : ∀ ξ : genericPointsOne X,
        _root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
          ((Scheme.Modules.pullback (reducedComponentι X ξ)).obj E) rank),
      _root_.AlgebraicGeometry.curveDegree k f hX E rank =
        ∑ᶠ ξ : genericPointsOne X,
          (componentMultiplicity X ξ : ℤ) *
            @curveDegree k _ (reducedComponent X ξ) (reducedComponentι X ξ ≫ f)
              (hproperC ξ) (hdimC ξ)
              ((Scheme.Modules.pullback (reducedComponentι X ξ)).obj E) rank (hrank ξ)
Tag 0AYX, a lemma

Tag 0AYX in the Stacks Project.

AlgebraicGeometry.curveDegree_tensorSheaf_eq_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CurveDegreeTensor/Cohomological.lean, line 185. The attribute's comment: “on a proper curve; the whole tag, on a proper scheme of dimension at most one, is AlgebraicGeometry.curveDegree_tensorSheaf_eq_add_of_topologicalKrullDim_le_one”.

[Stacks, Tag 0AYX] on a proper curve. For ℰ and 𝒱 finite locally free of constant ranks n and m on a proper curve over a field,

deg(ℰ ⊗ 𝒱) = m · deg(ℰ) + n · deg(𝒱).

No hypothesis beyond the source's own, apart from the curve hypothesis discussed in the module docstring. The rank of the tensor product is AlgebraicGeometry.SheafOfModules.isFiniteLocallyFreeOfRank_tensorSheaf, and the two instances of [Stacks, Tag 02O6] over a field that [Stacks, Tag 0AYV] needs are supplied by AlgebraicGeometry.forall_finiteDimensional_cohomologyOverField_of_isProper.

The proof is the arithmetic of [Stacks, Tag 0AYX]: the Euler characteristic of ℰ ⊗ 𝒱 is m · deg(ℰ) + n · χ(𝒱) by [Stacks, Tag 0AYV], whose rank input is the fibre rank of 𝒱 at the generic point and hence m; every degree is then unfolded into Euler characteristics by AlgebraicGeometry.curveDegree_eq_eulerCharacteristic_sub, where the identity is linear arithmetic.

public theorem curveDegree_tensorSheaf_eq_add
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsCurve k f] [IsProper f]
    (hdim : topologicalKrullDim X ≤ 1) (E V : X.Modules) (n m : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E n]
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} V m] :
    @curveDegree k _ X f _ hdim
        ((((Stacks.SheafOfModules.Tensor.sheafTensor
          ⟨((X.toRingedSpace)).presheaf, ((X.toRingedSpace)).IsSheaf⟩).obj (E)).obj (V))) (n * m)
        (SheafOfModules.isFiniteLocallyFreeOfRank_tensorSheaf X E V n m) =
      (m : ℤ) * curveDegree k f hdim E n + (n : ℤ) * curveDegree k f hdim V m

AlgebraicGeometry.curveDegree_tensorSheaf_eq_add_of_topologicalKrullDim_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CurveDegreeTensor/Devissage.lean, line 599.

For ℰ and 𝒱 finite locally free of constant ranks n and m on a scheme X proper of dimension at most one over a field k,

deg(ℰ ⊗ 𝒱) = m · deg(ℰ) + n · deg(𝒱).

theorem curveDegree_tensorSheaf_eq_add_of_topologicalKrullDim_le_one (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f]
    (hdim : topologicalKrullDim X ≤ 1) (E V : X.Modules) (n m : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E n]
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} V m] :
    @curveDegree k _ X f _ hdim
        ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X.toRingedSpace)).presheaf,
            ((X.toRingedSpace)).IsSheaf⟩).obj (E)).obj (V))) (n * m)
        (SheafOfModules.isFiniteLocallyFreeOfRank_tensorSheaf X E V n m) =
      (m : ℤ) * curveDegree k f hdim E n + (n : ℤ) * curveDegree k f hdim V m
Tag 0DJ5, a lemma

Tag 0DJ5 in the Stacks Project.

AlgebraicGeometry.curveDegree_eq_curveDegree_exteriorPower_eq_invertibleCurveDegree_determinant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/DegreeExteriorDeterminant.lean, line 147.

[Stacks, Tag 0DJ5]. Let k be a field, X a proper scheme of dimension at most one over k and ℰ a finite locally free 𝒪_X-module of constant rank n. Then

deg(ℰ) = deg(⋀ⁿ ℰ) = deg(det(ℰ)).

Both equalities are asserted, under exactly the source's hypotheses. det(ℰ) is the determinant of [Stacks, Tag 0FJN], AlgebraicGeometry.Scheme.Modules.determinant, and its invertibility — which AlgebraicGeometry.invertibleCurveDegree needs and the source does not assume — is derived from the rank of ℰ by AlgebraicGeometry.Scheme.Modules.isInvertible_determinant.

The first equality is AlgebraicGeometry.curveDegree_eq_curveDegree_exteriorPower_of_isProper: the source's dévissage on a proper curve, passed to X through the one-dimensional components ([Stacks, Tag 0AYW]). The second is the identification ⋀ⁿ ℰ ≅ det(ℰ) of [Stacks, Tag 0B37] together with the agreement of the invertible degree with the rank-one degree.

theorem curveDegree_eq_curveDegree_exteriorPower_eq_invertibleCurveDegree_determinant
    (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f]
    (hdim : topologicalKrullDim X ≤ 1) (E : X.Modules) (n : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E n] :
    curveDegree k f hdim E n =
        @curveDegree k _ X f _ hdim (Scheme.Modules.exteriorPower E (n : ℤ)) 1
          (Scheme.Modules.isFiniteLocallyFreeOfRank_exteriorPower_self E n) ∧
      @curveDegree k _ X f _ hdim (Scheme.Modules.exteriorPower E (n : ℤ)) 1
          (Scheme.Modules.isFiniteLocallyFreeOfRank_exteriorPower_self E n) =
        @invertibleCurveDegree k _ X f _ hdim (Scheme.Modules.determinant E)
          (Scheme.Modules.isInvertible_determinant E n)
Tag 0AYY, a lemma

Tag 0AYY in the Stacks Project.

AlgebraicGeometry.isFinite_and_curveDegree_tensorSheaf_invertibleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/DivisorTwistDegree.lean, line 270.

[Stacks, Tag 0AYY]. Let k be a field, let X be a proper scheme of dimension at most one over k and let D be an effective Cartier divisor on X. Then D is finite over Spec(k), of degree

deg(D) = dim_k Γ(D, 𝒪_D),

and for a finite locally free ℰ of rank n,

deg(ℰ(D)) = n · deg(D) + deg(ℰ), where ℰ(D) = ℰ ⊗_{𝒪_X} 𝒪_X(D).

The three assertions are about one and the same number dim_k Γ(D, 𝒪_D): it is the rank of the finite locally free morphism D ⟶ Spec(k) — which is what "finite of degree deg(D)" asserts — and it is the coefficient of n in the twist formula.

Finiteness and the degree are AlgebraicGeometry.isFinite_divisorSubscheme and AlgebraicGeometry.isFiniteLocallyFreeOfRank_divisorSubscheme. The twist formula is [Stacks, Tag 0AYX], i.e. AlgebraicGeometry.curveDegree_tensorSheaf_eq_add_of_topologicalKrullDim_le_one, at ℰ and 𝒪_X(D), whose deg(𝒪_X(D)) term is AlgebraicGeometry.curveDegree_invertibleSheaf_eq_finrank_globalSections.

theorem isFinite_and_curveDegree_tensorSheaf_invertibleSheaf (E : X.Modules) (n : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E n] :
    letI : Algebra k Γ(D.subscheme, ⊤) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ (D.subschemeι ≫ f).appTop).hom.toAlgebra
    IsFinite (D.subschemeι ≫ f) ∧
      Stacks.Morphisms.IsFiniteLocallyFreeOfRank (D.subschemeι ≫ f)
          (Module.finrank k Γ(D.subscheme, ⊤)) ∧
        @curveDegree k _ X f _ hdim
            ((((Stacks.SheafOfModules.Tensor.sheafTensor
              ⟨((X.toRingedSpace)).presheaf, ((X.toRingedSpace)).IsSheaf⟩).obj (E)).obj
              ((Stacks.Divisors.invertibleSheaf' D)))) n
            (isFiniteLocallyFreeOfRank_tensorSheaf_invertibleSheaf D E n) =
          (n : ℤ) * (Module.finrank k Γ(D.subscheme, ⊤) : ℤ) + curveDegree k f hdim E n
Tag 0C6P, a lemma

Tag 0C6P in the Stacks Project.

AlgebraicGeometry.isField_and_finite_globalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/DegreeDivisibility.lean, line 103. The attribute's comment: “the global sections are a finite field extension”.

For a proper scheme over a field which is reduced and connected, the ring of global sections is a finite field extension of the base field.

theorem isField_and_finite_globalSections (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] [IsReduced X] [ConnectedSpace X] :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    IsField Γ(X, ⊤) ∧ Module.Finite k Γ(X, ⊤)

AlgebraicGeometry.finrank_globalSections_dvd_curveDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/DegreeDivisibility.lean, line 156. The attribute's comment: “w divides the degree of a finite locally free sheaf”.

For a proper scheme over a field which is reduced and connected and of dimension at most one, the degree of the extension Γ(X, 𝒪_X)/k divides the degree of every finite locally free sheaf of constant rank on X.

theorem finrank_globalSections_dvd_curveDegree (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] [IsReduced X] [ConnectedSpace X]
    (hdim : topologicalKrullDim X ≤ 1) (E : X.Modules) (rank : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E rank] :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    (Module.finrank k Γ(X, ⊤) : ℤ) ∣ curveDegree k f hdim E rank

AlgebraicGeometry.finrank_globalSections_dvd_finrank_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/DegreeDivisibility.lean, line 173. The attribute's comment: “w divides the degree of a residue field”.

For a proper scheme over a field which is reduced and connected, the degree of the extension Γ(X, 𝒪_X)/k divides the degree over k of the residue field at every point.

theorem finrank_globalSections_dvd_finrank_residueField (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] [IsReduced X] [ConnectedSpace X] (x : X) :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    letI : Algebra k (X.residueField x) :=
      ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop ≫ X.Γevaluation x).hom.toAlgebra
    Module.finrank k Γ(X, ⊤) ∣ Module.finrank k (X.residueField x)

AlgebraicGeometry.finrank_globalSections_dvd_finrank_globalSections_of_dimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/DegreeDivisibility.lean, line 186. The attribute's comment: “w divides the degree of a zero-dimensional closed subscheme”.

Let X be a proper scheme over a field which is reduced and connected and let D ⊆ X be a closed subscheme of dimension zero. Then D is finite locally free over k of rank dim_k Γ(D, 𝒪_D), and the degree of the extension Γ(X, 𝒪_X)/k divides it.

theorem finrank_globalSections_dvd_finrank_globalSections_of_dimension_zero (k : Type u)
    [Field k] {X D : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] [IsReduced X]
    [ConnectedSpace X] (i : D ⟶ X) [IsClosedImmersion i] (hdimD : topologicalKrullDim D = 0) :
    letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appTop).hom.toAlgebra
    letI : Algebra k Γ(D, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ (i ≫ f).appTop).hom.toAlgebra
    Stacks.Morphisms.IsFiniteLocallyFreeOfRank (i ≫ f) (Module.finrank k Γ(D, ⊤)) ∧
      Module.finrank k Γ(X, ⊤) ∣ Module.finrank k Γ(D, ⊤)
Tag 0AYZ, a lemma

Tag 0AYZ in the Stacks Project.

AlgebraicGeometry.curveDegree_pullback_eq_degreeOver_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/PullbackDegree.lean, line 332.

Let k be a field, let f : X ⟶ Y be a nonconstant morphism of proper curves over k and let ℰ be a finite locally free 𝒪_Y-module of constant rank n. Then

deg(f^*ℰ) = deg(X/Y)·deg(ℰ),

where deg(X/Y) = [R(X) : R(Y)] is AlgebraicGeometry.degreeOver ([Stacks, Tag 02NY]) and deg is AlgebraicGeometry.curveDegree ([Stacks, Tag 0AYR]).

theorem curveDegree_pullback_eq_degreeOver_mul (k : Type u) [Field k] {X Y : Scheme.{u}}
    (πX : X ⟶ Spec (.of k)) (πY : Y ⟶ Spec (.of k))
    [IsCurve k πX] [IsCurve k πY] [IsProper πX] [IsProper πY]
    (f : X ⟶ Y) (hf : f ≫ πY = πX) (hnc : ¬ ∃ y : Y, ∀ x : X, f.base x = y)
    (E : Y.Modules) (n : ℕ) [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E n] :
    @curveDegree k _ X πX _ (le_of_eq (IsCurve.topologicalKrullDim_eq_one (f := πX)))
        ((Scheme.Modules.pullback f).obj E) n (isFiniteLocallyFreeOfRank_pullback f E n) =
      (@degreeOver X Y f _ _ (locallyOfFiniteType_of_isCurve_comp k πX πY f hf)
          (isDominant_of_not_constant k πX πY f hnc) : ℤ) *
        curveDegree k πY (le_of_eq (IsCurve.topologicalKrullDim_eq_one (f := πY))) E n

AlgebraicGeometry.curveDegree_pullback_eq_degreeOver_mul_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/PullbackDegree.lean, line 422. References: SGA 6 X (4.4), “(4.4.3), special case”.

Let k be a field, let f : X ⟶ Y be a nonconstant morphism of proper curves over k and let ℰ be a finite locally free 𝒪_Y-module. Then

deg(f^*ℰ) = deg(X/Y)·deg(ℰ),

where deg(X/Y) = [R(X) : R(Y)] is AlgebraicGeometry.degreeOver ([Stacks, Tag 02NY]) and deg is AlgebraicGeometry.curveDegree ([Stacks, Tag 0AYR]), both degrees taken at the fibre rank of ℰ at the generic point of Y.

theorem curveDegree_pullback_eq_degreeOver_mul_of_isFiniteLocallyFree (k : Type u) [Field k]
    {X Y : Scheme.{u}} (πX : X ⟶ Spec (.of k)) (πY : Y ⟶ Spec (.of k))
    [IsCurve k πX] [IsCurve k πY] [IsProper πX] [IsProper πY]
    (f : X ⟶ Y) (hf : f ≫ πY = πX) (hnc : ¬ ∃ y : Y, ∀ x : X, f.base x = y)
    (E : Y.Modules)
    [SheafOfModules.IsFiniteLocallyFree.{u, u, u} (R := Y.ringCatSheaf) E] :
    letI _hrank : SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E
        (Scheme.Modules.fiberRank E (genericPoint (Y : Type u))) :=
      Scheme.Modules.isFiniteLocallyFreeOfRank_of_fiberRank_eq E
        (Scheme.Modules.fiberRank E (genericPoint (Y : Type u)))
        (genericPoint (Y : Type u)) rfl
    @curveDegree k _ X πX _ (le_of_eq (IsCurve.topologicalKrullDim_eq_one (f := πX)))
        ((Scheme.Modules.pullback f).obj E)
        (Scheme.Modules.fiberRank E (genericPoint (Y : Type u)))
        (isFiniteLocallyFreeOfRank_pullback f E
          (Scheme.Modules.fiberRank E (genericPoint (Y : Type u)))) =
      (@degreeOver X Y f _ _ (locallyOfFiniteType_of_isCurve_comp k πX πY f hf)
          (isDominant_of_not_constant k πX πY f hnc) : ℤ) *
        curveDegree k πY (le_of_eq (IsCurve.topologicalKrullDim_eq_one (f := πY))) E
          (Scheme.Modules.fiberRank E (genericPoint (Y : Type u)))
Tag 0B40, a lemma

Tag 0B40 in the Stacks Project.

AlgebraicGeometry.invertibleCurveDegree_nonneg_of_eval_top_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/SectionDegree.lean, line 272. The attribute's comment: “part (1)”.

The degree of an invertible module with a nonzero global section is nonnegative, on a proper integral scheme of dimension at most one over a field.

theorem invertibleCurveDegree_nonneg_of_eval_top_ne_zero [IsProper f] [IsIntegral X]
    (hdim : topologicalKrullDim X ≤ 1) (L : X.Modules)
    [hL : SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] (s : L.sections)
    (hs : s.eval (op ⊤) ≠ 0) :
    0 ≤ @invertibleCurveDegree k _ X f _ hdim L hL

AlgebraicGeometry.invertibleCurveDegree_pos_of_eval_top_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/SectionDegree.lean, line 377. The attribute's comment: “part (2)”.

A nonzero section with a zero forces positive degree. On a proper integral scheme of dimension at most one over a field, a nonzero global section of an invertible module which vanishes at some point forces the degree of that module to be positive.

theorem invertibleCurveDegree_pos_of_eval_top_ne_zero [IsProper f] [IsIntegral X]
    (hdim : topologicalKrullDim X ≤ 1) (L : X.Modules)
    [hL : SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] (s : L.sections)
    (hs : s.eval (op ⊤) ≠ 0)
    (hzero : ∃ y : X, y ∉ nonvanishingLocus (X := X.toRingedSpace) L s) :
    0 < @invertibleCurveDegree k _ X f _ hdim L hL

AlgebraicGeometry.isIso_unitHomEquiv_symm_of_invertibleCurveDegree_nonpos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/SectionDegree.lean, line 432. The attribute's comment: “part (4), in the stronger form the source's proof supports and the text does not state: the multiplication map O_X -> L of the given section is itself an isomorphism, not merely L isomorphic to O_X abstractly. The weaker reading is the corollary isTrivial_of_invertibleCurveDegree_nonpos beside it”.

A nonzero section of a module of nonpositive degree trivializes it. On a proper integral scheme of dimension at most one over a field, let ℒ be an invertible module with deg(ℒ) ≤ 0 and a nonzero global section s. Then multiplication by s is an isomorphism 𝒪_X ⟶ ℒ.

theorem isIso_unitHomEquiv_symm_of_invertibleCurveDegree_nonpos [IsProper f] [IsIntegral X]
    (hdim : topologicalKrullDim X ≤ 1) (L : X.Modules)
    [hL : SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] (s : L.sections)
    (hs : s.eval (op ⊤) ≠ 0) (hdeg : @invertibleCurveDegree k _ X f _ hdim L hL ≤ 0) :
    IsIso (L.unitHomEquiv.symm s)

AlgebraicGeometry.isTrivial_of_invertibleCurveDegree_nonpos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/SectionDegree.lean, line 447. The attribute's comment: “part (4) as stated -- L is isomorphic to O_X”.

An invertible module of nonpositive degree with a nonzero global section is trivial, on a proper integral scheme of dimension at most one over a field.

theorem isTrivial_of_invertibleCurveDegree_nonpos [IsProper f] [IsIntegral X]
    (hdim : topologicalKrullDim X ≤ 1) (L : X.Modules)
    [hL : SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] (s : L.sections)
    (hs : s.eval (op ⊤) ≠ 0) (hdeg : @invertibleCurveDegree k _ X f _ hdim L hL ≤ 0) :
    SheafOfModules.IsTrivial X.presheaf X.ringCatSheaf.property L

AlgebraicGeometry.isTrivial_of_eval_top_ne_zero_of_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/SectionDegree.lean, line 537. The attribute's comment: “part (3)”.

An invertible module whose inverse also has a nonzero section is trivial. If an invertible module ℒ on an integral scheme universally closed over a field and its inverse ℒ^{⊗ -1} both have nonzero global sections, then ℒ ≅ 𝒪_X.

theorem isTrivial_of_eval_top_ne_zero_of_inverse [IsIntegral X] [UniversallyClosed f]
    (L : X.Modules) [hL : SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.property L]
    (s : L.sections) (hs : s.eval (op ⊤) ≠ 0)
    (t : (tensorPowerModule L (-1)).sections) (ht : t.eval (op ⊤) ≠ 0) :
    SheafOfModules.IsTrivial X.presheaf X.ringCatSheaf.property L

AlgebraicGeometry.invertibleCurveDegree_le_of_hom_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/SectionDegree.lean, line 706. The attribute's comment: “part (5), the inequality deg(N) <= deg(L)”.

A nonzero morphism of invertible modules does not decrease the degree. On a proper curve over a field, a nonzero morphism 𝒩 ⟶ ℒ of invertible modules forces deg(𝒩) ≤ deg(ℒ).

theorem invertibleCurveDegree_le_of_hom_ne_zero [IsCurve k f] [IsProper f]
    (hdim : topologicalKrullDim X ≤ 1) (N L : X.Modules)
    [hN : SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.property N]
    [hL : SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.property L]
    (φ : N ⟶ L) (hφ : φ ≠ 0) :
    invertibleCurveDegree k f hdim N ≤ invertibleCurveDegree k f hdim L

AlgebraicGeometry.isIso_of_invertibleCurveDegree_eq_of_hom_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/SectionDegree.lean, line 724. The attribute's comment: “part (5), the equality case: the morphism is an isomorphism”.

A nonzero morphism of invertible modules of equal degree is an isomorphism, on a proper curve over a field.

theorem isIso_of_invertibleCurveDegree_eq_of_hom_ne_zero [IsCurve k f] [IsProper f]
    (hdim : topologicalKrullDim X ≤ 1) (N L : X.Modules)
    [hN : SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.property N]
    [hL : SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.property L]
    (φ : N ⟶ L) (hφ : φ ≠ 0)
    (heq : invertibleCurveDegree k f hdim N = invertibleCurveDegree k f hdim L) : IsIso φ

AlgebraicGeometry.invertibleCurveDegree_eq_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/SectionDegree.lean, line 750. The attribute's comment: “part (5), the converse of the equality case: an isomorphism has equal degrees, so the equality holds exactly when the morphism is an isomorphism”.

An isomorphism of invertible modules preserves the degree, on a proper scheme of dimension at most one over a field.

theorem invertibleCurveDegree_eq_of_isIso [IsProper f] (hdim : topologicalKrullDim X ≤ 1)
    (N L : X.Modules)
    [hN : SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.property N]
    [hL : SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.property L]
    (φ : N ⟶ L) [IsIso φ] :
    invertibleCurveDegree k f hdim N = invertibleCurveDegree k f hdim L
Tag 0E22, a lemma

Tag 0E22 in the Stacks Project.

AlgebraicGeometry.subsingleton_globalSections_or_isTrivial_of_invertibleCurveDegree_nonpos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/NonpositiveDegreeSection.lean, line 238.

Let k be a field and X a proper scheme over k which is reduced, connected and equidimensional of dimension one, and let ℒ be an invertible 𝒪_X-module whose restriction to every irreducible component of X has degree ≤ 0. Then either H⁰(X, ℒ) = 0 or ℒ ≅ 𝒪_X.

theorem subsingleton_globalSections_or_isTrivial_of_invertibleCurveDegree_nonpos [IsReduced X]
    [ConnectedSpace X] (_hequi : TopologicalSpace.Equidimensional (X : Type u))
    (hdim : topologicalKrullDim (X : Type u) = 1) (L : X.Modules)
    [hL : SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
    (hdeg : ∀ (C : Set X) (hC : C ∈ irreducibleComponents (X : Type u)),
      haveI : SheafOfModules.IsInvertible
          (Scheme.IdealSheafData.vanishingIdeal
            ⟨C, isClosed_of_mem_irreducibleComponents C hC⟩).subscheme.presheaf
          (Scheme.IdealSheafData.vanishingIdeal
            ⟨C, isClosed_of_mem_irreducibleComponents C hC⟩).subscheme.ringCatSheaf.2
          ((RingedSpaceModuleAdjunction.modulePullback
            (Scheme.IdealSheafData.vanishingIdeal
              ⟨C, isClosed_of_mem_irreducibleComponents C hC⟩).subschemeι.toLRSHom.toShHom).obj
            L) :=
        RingedSpaceModuleAdjunction.modulePullback_isInvertible_scheme _ L
      invertibleCurveDegree k
          ((Scheme.IdealSheafData.vanishingIdeal
            ⟨C, isClosed_of_mem_irreducibleComponents C hC⟩).subschemeι ≫ f)
          ((StacksTag09NX.topologicalKrullDim_le_of_isClosedImmersion
            (Scheme.IdealSheafData.vanishingIdeal
              ⟨C, isClosed_of_mem_irreducibleComponents C hC⟩).subschemeι).trans hdim.le)
          ((RingedSpaceModuleAdjunction.modulePullback
            (Scheme.IdealSheafData.vanishingIdeal
              ⟨C, isClosed_of_mem_irreducibleComponents C hC⟩).subschemeι.toLRSHom.toShHom).obj
            L) ≤ 0) :
    Subsingleton Γ(L, ⊤) ∨ SheafOfModules.IsTrivial X.presheaf X.ringCatSheaf.2 L
Tag 0B5X, a lemma

Tag 0B5X in the Stacks Project.

AlgebraicGeometry.isAmple_iff_invertibleCurveDegree_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleDegreeCriterion/CurveAmple.lean, line 154. The attribute's comment: “both directions, for a proper curve over a field”.

[Stacks, Tag 0B5X]. Let k be a field, X a proper curve over k and 𝓛 an invertible 𝒪_X-module. Then 𝓛 is ample if and only if deg(𝓛) > 0.

The forward direction is AlgebraicGeometry.invertibleCurveDegree_pos_of_isAmple_of_isCurve of ./CurveInputs.lean. The converse composes the source's second paragraph, AlgebraicGeometry.hasAffinePowerOfDegreePos_of_isCurve of ./CurveSection.lean, with its third, which enters through AlgebraicGeometry.isAmple_of_exists_tensorPower_section_of_isCurve above.

hdim is an explicit argument because AlgebraicGeometry.invertibleCurveDegree takes the dimension bound as one; on a curve it is le_of_eq (IsCurve.topologicalKrullDim_eq_one f), and it is an unused argument of that definition, so any two proofs of it give the same degree.

public theorem isAmple_iff_invertibleCurveDegree_pos [IsCurve k f] [IsProper f]
    (hdim : topologicalKrullDim X ≤ 1) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L] :
    Scheme.Modules.IsAmple X L ↔ 0 < invertibleCurveDegree k f hdim L

AlgebraicGeometry.invertibleCurveDegree_pos_of_isAmple_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleDegreeCriterion/CurveInputs.lean, line 241. The attribute's comment: “the implication: L ample ⟹ deg(L) > 0, with no hypothesis beyond the tag's own; both directions are registered on isAmple_iff_invertibleCurveDegree_pos”.

The forward direction of [Stacks, Tag 0B5X], at the source's hypotheses. On a proper curve over a field an ample invertible module has positive degree.

This is AlgebraicGeometry.invertibleCurveDegree_pos_of_isAmple_of_devissage with each of its four inputs supplied by the theorems above.

The converse implication is AlgebraicGeometry.isAmple_iff_invertibleCurveDegree_pos of CurveAmple.lean, which states both directions.

public theorem invertibleCurveDegree_pos_of_isAmple_of_isCurve [IsCurve k f] [IsProper f]
    (hdim : topologicalKrullDim X ≤ 1) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
    (hL : Scheme.Modules.IsAmple X L) :
    0 < invertibleCurveDegree k f hdim L
Tag 0B5Y, a lemma

Tag 0B5Y in the Stacks Project.

AlgebraicGeometry.isAmple_iff_forall_invertibleCurveDegree_reducedComponent_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleDegreeCriterion/ComponentCriterion.lean, line 302. The attribute's comment: “both directions, at the tag's own indexing by the one-dimensional irreducible components with their reduced induced closed subscheme structure”.

[Stacks, Tag 0B5Y], both directions. Let k be a field, let X be a scheme proper of dimension at most one over k and let 𝓛 be an invertible 𝒪_X-module. Then 𝓛 is ample if and only if the degree of the restriction of 𝓛 to every one-dimensional irreducible component of X, taken with its reduced induced closed subscheme structure, is positive.

The components of dimension one are the tag's C₁, …, C_t: they are indexed by their generic points, Stacks.AlgebraicGeometry.ComponentDegrees.genericPointsOne X, the reduced induced subscheme is Stacks.AlgebraicGeometry.ComponentDegrees.reducedComponent, and that it is a proper curve over k is proved with no hypothesis.

The implication (1) ⟹ (2) is AlgebraicGeometry.invertibleCurveDegree_reducedComponent_pos_of_isAmple of ./ComponentPositivity.lean, which has no hypothesis beyond the tag's own.

For the implication (2) ⟹ (1) the covering family of the source is formed: all the irreducible components, which are finitely many because a scheme proper over a field is Noetherian. Each has dimension zero or one. On a zero-dimensional one the restriction of 𝓛 is ample outright, and on a one-dimensional one positivity of the degree makes it ample by the converse direction of [Stacks, Tag 0B5X]; ampleness then descends to X along the finite surjection from the disjoint union, by [Stacks, Tag 0B5V] together with AlgebraicGeometry.isAmple_sigma_of_forall_isAmple_pullback_sigmaι.

No hypothesis beyond the tag's own.

public theorem isAmple_iff_forall_invertibleCurveDegree_reducedComponent_pos
    (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f]
    (hdim : topologicalKrullDim X ≤ 1) (L : X.Modules)
    [SheafOfModules.IsInvertible X.toRingedSpace.presheaf
      (structureSheafRing X.toRingedSpace).property L] :
    Scheme.Modules.IsAmple X L ↔
      ∀ ζ : genericPointsOne X,
        0 < @invertibleCurveDegree k _ (reducedComponent X ζ) (reducedComponentι X ζ ≫ f)
          (isProper_reducedComponentι_comp k f ζ)
          (topologicalKrullDim_reducedComponent_le X hdim ζ)
          ((Scheme.Modules.pullback (reducedComponentι X ζ)).obj L)
          (SheafOfModules.isInvertible_pullback (reducedComponentι X ζ) L)

AlgebraicGeometry.invertibleCurveDegree_reducedComponent_pos_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleDegreeCriterion/ComponentPositivity.lean, line 246. The attribute's comment: “the implication (1) ⟹ (2), at the tag's own indexing by the one-dimensional irreducible components with their reduced induced structure, with no hypothesis beyond the tag's own; the full equivalence is registered on isAmple_iff_forall_invertibleCurveDegree_reducedComponent_pos”.

The implication (1) ⟹ (2) of [Stacks, Tag 0B5Y]. Let k be a field, let X be proper of dimension at most one over k and let 𝓛 be an ample invertible 𝒪_X-module. Then the degree of the restriction of 𝓛 to every one-dimensional irreducible component of X, taken with its reduced induced closed subscheme structure, is positive.

The components of dimension one are indexed by their generic points, Stacks.AlgebraicGeometry.ComponentDegrees.genericPointsOne X, and the reduced induced subscheme is Stacks.AlgebraicGeometry.ComponentDegrees.reducedComponent; that it is a proper curve over k — integral, separated, of finite type and of dimension exactly one — is Stacks.AlgebraicGeometry.ComponentDegrees.isCurve_reducedComponentι_comp together with Stacks.AlgebraicGeometry.ComponentDegrees.isProper_reducedComponentι_comp, both proved with no hypothesis. So this is the tag's own family C₁, …, C_t and its own conclusion.

No hypothesis beyond the tag's own. The reverse implication is AlgebraicGeometry.isAmple_iff_forall_invertibleCurveDegree_reducedComponent_pos of ComponentCriterion.lean, which states the full equivalence.

public theorem invertibleCurveDegree_reducedComponent_pos_of_isAmple [IsProper f]
    (hdim : topologicalKrullDim X ≤ 1) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
    (hL : Scheme.Modules.IsAmple X L) (ξ : genericPointsOne X) :
    0 < @invertibleCurveDegree k _ (reducedComponent X ξ) (reducedComponentι X ξ ≫ f)
      (isProper_reducedComponentι_comp k f ξ)
      (topologicalKrullDim_reducedComponent_le X hdim ξ)
      ((Scheme.Modules.pullback (reducedComponentι X ξ)).obj L)
      (SheafOfModules.isInvertible_pullback (reducedComponentι X ξ) L)
Tag 0B8Z, a lemma

Tag 0B8Z in the Stacks Project.

AlgebraicGeometry.exists_invertible_finrank_cohomologyOverField_zero_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PrescribedLowCohomology.lean, line 237. The attribute's comment: “assertion (1)”.

[Stacks, Tag 0B8Z], assertion (1). On a proper curve over an algebraically closed field there is an invertible module ℒ with dim_k H⁰(X, ℒ) = 1 and H¹(X, ℒ) = 0.

Starting from an invertible module with vanishing H¹ and a nonzero global section (AlgebraicGeometry.exists_invertible_isZero_cohomologyOverField_one_and_zero_lt_finrank) and twisting down dim_k H⁰(X, ℒ₀) - 1 times by AlgebraicGeometry.exists_pointTwistDown, each step lowering dim_k H⁰ by one and preserving the vanishing of H¹.

public theorem exists_invertible_finrank_cohomologyOverField_zero_eq_one [IsAlgClosed k]
    [IsProper f] [IsCurve k f] :
    ∃ L : X.Modules, SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L ∧
      Module.finrank k (cohomologyOverField k f L 0) = 1 ∧
        IsZero (cohomologyOverField k f L 1)

AlgebraicGeometry.exists_invertible_isZero_cohomologyOverField_zero_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/PrescribedLowCohomology.lean, line 256. The attribute's comment: “assertion (2), the vanishing of both H⁰ and H¹”.

[Stacks, Tag 0B8Z], assertion (2). On a proper curve over an algebraically closed field there is an invertible module 𝒩 with H⁰(X, 𝒩) = 0 and H¹(X, 𝒩) = 0.

The same descent as for assertion (1), run one step further, down to dim_k H⁰ = 0; the vanishing of H⁰ — rather than only its dimension — comes from the finite dimensionality carried along the induction.

public theorem exists_invertible_isZero_cohomologyOverField_zero_one [IsAlgClosed k] [IsProper f]
    [IsCurve k f] :
    ∃ N : X.Modules, SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property N ∧
      IsZero (cohomologyOverField k f N 0) ∧ IsZero (cohomologyOverField k f N 1)
Tag 0B90, a lemma

Tag 0B90 in the Stacks Project.

AlgebraicGeometry.isZero_cohomologyOverField_one_of_two_mul_genus_sub_one_le_invertibleCurveDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/LargeDegreeVanishing.lean, line 641. The attribute's comment: “the whole statement: H¹(X, L) = 0 for every invertible O_X-module L with deg(L) ≥ 2g - 1 on a proper curve X over an algebraically closed field, with g the genus”.

[Stacks, Tag 0B90]. Let k be an algebraically closed field, let X be a proper curve over k and let g = dim_k H¹(X, 𝒪_X). Then H¹(X, ℒ) = 0 for every invertible 𝒪_X-module ℒ with deg(ℒ) ≥ 2g - 1.

Let 𝒩 be the invertible module of [Stacks, Tag 0B8Z] (2), of degree g - dim_k H⁰(X, 𝒪_X). Then ℒ ⊗ 𝒩^{⊗ -1} has degree deg(ℒ) - g + dim_k H⁰(X, 𝒪_X), so

dim_k H⁰(ℒ ⊗ 𝒩^{⊗ -1}) - dim_k H¹(ℒ ⊗ 𝒩^{⊗ -1}) = deg(ℒ) - 2g + 2 dim_k H⁰(X, 𝒪_X) ≥ 1

because dim_k H⁰(X, 𝒪_X) ≥ 1 on a proper integral scheme; hence ℒ ⊗ 𝒩^{⊗ -1} has a nonzero global section and isZero_cohomologyOverField_one_of_tensorInverse_section applies.

public theorem isZero_cohomologyOverField_one_of_two_mul_genus_sub_one_le_invertibleCurveDegree
    [IsAlgClosed k] [IsProper f] [IsCurve k f] (L : X.Modules)
    (hL : SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L)
    (hdeg : 2 * (genus f : ℤ) - 1 ≤ @invertibleCurveDegree k _ X f _
      (IsCurve.topologicalKrullDim_eq_one (k := k) (f := f)).le L hL) :
    IsZero (cohomologyOverField k f L 1)
Sources
LeanAlgebraicGeometry.curveDegree · AlgebraicGeometry.invertibleCurveDegree · AlgebraicGeometry.curveDegree_baseChange_field · AlgebraicGeometry.curveDegree_add_of_shortExact_of_isProper · AlgebraicGeometry.curveDegree_add_of_shortExact_of_cohomologyFiniteDimensional · AlgebraicGeometry.curveDegree_pullback_eq_of_bijOn_genericPointsOne · AlgebraicGeometry.curveDegree_pullback_eq_of_bijOn_genericPointsOne_of_isProper · AlgebraicGeometry.exists_eulerCharacteristic_tensorSheaf_eq_fiberRank_mul_curveDegree_add_of_isCurve

Section33.45 Numerical intersections#

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

Tag 0BEM, a lemma

Tag 0BEM in the Stacks Project.

AlgebraicGeometry.exists_eulerPolynomial_twistedSheaf_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistedSheaf/EulerPolynomialProper.lean, line 38.

Let k be a field, let X be a scheme proper over k, let 𝓛_1, …, 𝓛_r be invertible 𝒪_X-modules and let ℱ be a coherent 𝒪_X-module. Then the Euler characteristics of the twists ℱ ⊗ 𝓛_1^{⊗ n_1} ⊗ ⋯ ⊗ 𝓛_r^{⊗ n_r} are the values of a polynomial in ℚ[n_1, …, n_r] which is zero or of total degree at most dim Supp ℱ.

theorem exists_eulerPolynomial_twistedSheaf_of_isProper (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) {r : ℕ} (L : Fin r → X.Modules)
    [∀ i, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L i)] [IsProper f]
    (F : X.Modules) (hF : _root_.SheafOfModules.IsCoherent F) :
    ∃ P : MvPolynomial (Fin r) ℚ,
      (P = 0 ∨ (P.totalDegree : WithBot ℕ∞) ≤
        topologicalKrullDim (_root_.SheafOfModules.supp F)) ∧
      ∀ n : Fin r → ℤ, MvPolynomial.eval (fun j => (n j : ℚ)) P
        = (@eulerCharacteristic k _ X f _ (twistedSheaf F L n)
            (@twistedSheaf_isCoherent X r F L _ hF n) : ℚ)
Tag 0BEN, a lemma

Tag 0BEN in the Stacks Project.

AlgebraicGeometry.exists_eulerPolynomial_sub_topDimComponents_totalDegree_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersectionLeadingTerm.lean, line 981. The attribute's comment: “the Euler characteristic minus the length-weighted Euler characteristics of the top-dimensional components of the support is a numerical polynomial of lower total degree”.

[Stacks, Tag 0BEN]. For X proper over a field k, a coherent 𝒪_X-module ℱ and invertible 𝒪_X-modules 𝓛_1, …, 𝓛_r, the difference between χ(X, ℱ ⊗ 𝓛_1^{⊗ n_1} ⊗ ⋯ ⊗ 𝓛_r^{⊗ n_r}) and the sum over the top-dimensional integral components Z of Supp ℱ, weighted by the length of ℱ at the generic point of Z, of χ(Z, 𝒪_Z ⊗ 𝓛_1^{⊗ n_1} ⊗ ⋯ ⊗ 𝓛_r^{⊗ n_r}) is a numerical polynomial in n_1, …, n_r of total degree strictly less than dim Supp ℱ.

theorem exists_eulerPolynomial_sub_topDimComponents_totalDegree_lt (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] {r : ℕ} (L : Fin r → X.Modules)
    [∀ i, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L i)]
    (F : X.Modules) [F.IsCoherent] :
    ∃ P : MvPolynomial (Fin r) ℚ,
      (P = 0 ∨ ((P.totalDegree : ℕ) : WithBot ℕ∞) <
        topologicalKrullDim (_root_.SheafOfModules.supp F)) ∧
      ∀ n : Fin r → ℤ, MvPolynomial.eval (fun j ↦ (n j : ℚ)) P =
        (eulerCharacteristic k f (twistedSheaf F L n) : ℚ) -
          ∑ᶠ Z : TopDimIntegralSubscheme F,
            (Stacks.Chow.sheafMultiplicity F Z.genericPt : ℚ) *
              (componentTwistEulerCharacteristic k f L Z n : ℚ)
Tag 0BEP, a definition

Tag 0BEP in the Stacks Project.

AlgebraicGeometry.intersectionNumber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersection.lean, line 192. References: SGA 6 XIII (2.1); SGA 6 X (4.4), “defn of (L_1..L_d;F)”.

Stacks 0BEP. The intersection number (𝓛_1 ⋯ 𝓛_d · Z) of d invertible 𝒪_X-modules against a closed subscheme i : Z ⟶ X of dimension at most d of a proper scheme X over a field k: the coefficient of n_1 ⋯ n_d in the numerical polynomial χ(Z, 𝓛_1^{⊗ n_1} ⊗ ⋯ ⊗ 𝓛_d^{⊗ n_d}|_Z), computed as the d-fold mixed finite difference

∑_{T ⊆ {1, …, d}} (-1)^{d - |T|} χ(Z, ⨂_{j ∈ T} 𝓛_j|_Z)

of that function. This is an honest integer, which is Stacks 0BEQ: only finitely many values of the function are used, so neither polynomiality nor a choice of representing polynomial enters. The Euler characteristic is written out as the alternating sum of the dimensions of the cohomology groups, so that no coherence hypothesis is needed to state the definition; AlgebraicGeometry.intersectionNumber_eq_sum_eulerCharacteristic is the comparison with AlgebraicGeometry.eulerCharacteristic.

public noncomputable def intersectionNumber (k : Type u) [Field k] {X Z : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i]
    (d : ℕ) (_hd : topologicalKrullDim Z ≤ d) (L : Fin d → X.Modules)
    [∀ j, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L j)] : ℤ

AlgebraicGeometry.intersectionNumber_eq_coeff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersection.lean, line 260. The attribute's comment: “the coefficient of n_1 ⋯ n_d”. References: SGA 6 XIII (2.1), “coeff of n_1⋯n_s”; SGA 6 X (4.4), “defn of (L_1..L_d;F)”.

Stacks 0BEP, the coefficient of n_1 ⋯ n_d. If a rational polynomial P in d variables of total degree at most d takes the Euler characteristics χ(Z, 𝓛_1^{⊗ n_1} ⊗ ⋯ ⊗ 𝓛_d^{⊗ n_d}|_Z) as its values at the integral tuples, then the intersection number (𝓛_1 ⋯ 𝓛_d · Z) is the coefficient of n_1 ⋯ n_d in P.

This is the source's own description of the intersection number. The existence of such a P, which is Stacks 0BEM, is not assumed: the statement is unconditional in P, and the proof is the monomial computation MvPolynomial.sum_neg_one_pow_mul_eval_indicator_eq_coeff_one.

public theorem intersectionNumber_eq_coeff (k : Type u) [Field k] {X Z : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i]
    (d : ℕ) (hd : topologicalKrullDim Z ≤ d) (L : Fin d → X.Modules)
    [∀ j, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L j)]
    (P : MvPolynomial (Fin d) ℚ)
    (hP : ∀ n : Fin d → ℤ, MvPolynomial.eval (fun j => (n j : ℚ)) P =
      ((@eulerCharacteristic k _ Z (i ≫ f) inferInstance
        (twistedSheaf (SheafOfModules.unit Z.ringCatSheaf)
          (fun j => (Scheme.Modules.pullback i).obj (L j)) n)
        (isCoherent_twistedSheafUnitPullback k f i L n) : ℤ) : ℚ))
    (hdeg : P.totalDegree ≤ d) :
    ((intersectionNumber k f i d hd L : ℤ) : ℚ) =
      P.coeff (Finsupp.equivFunOnFinite.symm fun _ => 1)

AlgebraicGeometry.selfIntersectionNumber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersection.lean, line 311. The attribute's comment: “the self-intersection notation (L^d · Z)”. References: SGA 6 XIII (2.1), “all L_i equal”.

Stacks 0BEP, the self-intersection notation (𝓛^d · Z). The intersection number of a single invertible 𝒪_X-module 𝓛 repeated d times against a closed subscheme i : Z ⟶ X of dimension at most d.

public noncomputable def selfIntersectionNumber (k : Type u) [Field k] {X Z : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i]
    (d : ℕ) (hd : topologicalKrullDim Z ≤ d) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L] : ℤ
Tag 0BEQ, a lemma

Tag 0BEQ in the Stacks Project.

AlgebraicGeometry.intersectionNumber_isInteger, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersectionIntegrality.lean, line 164.

Stacks 0BEQ. In the situation of Stacks 0BEP — k a field, X a scheme proper over k, i : Z ⟶ X a closed subscheme of dimension at most d, and 𝓛_1, …, 𝓛_d invertible 𝒪_X-modules — the intersection number (𝓛_1 ⋯ 𝓛_d · Z) is an integer.

The intersection number is the coefficient of the squarefree monomial n_1 ⋯ n_d in the numerical polynomial χ(Z, 𝓛_1^{⊗ n_1} ⊗ ⋯ ⊗ 𝓛_d^{⊗ n_d}|_Z) of Stacks 0BEM, whose coefficients are a priori only rational; the assertion is that this one is integral. The polynomial is not assumed: Stacks 0BEM, available unconditionally as AlgebraicGeometry.exists_eulerPolynomial_twistedSheaf_of_isProper, produces it, and its total degree is at most dim Supp 𝒪_Z ≤ dim Z ≤ d. The integer produced is AlgebraicGeometry.intersectionNumber k f i d hd L, by AlgebraicGeometry.intersectionNumber_eq_coeff.

The integrality itself is AlgebraicGeometry.exists_int_coeff_one_of_eval_eq_eulerCharacteristic, which holds for every polynomial of total degree at most d representing those Euler characteristics.

public theorem intersectionNumber_isInteger (k : Type u) [Field k] {X Z : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i]
    (d : ℕ) (hd : topologicalKrullDim Z ≤ d) (L : Fin d → X.Modules)
    [∀ j, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L j)] :
    ∃ P : MvPolynomial (Fin d) ℚ,
      (∀ n : Fin d → ℤ, MvPolynomial.eval (fun j => (n j : ℚ)) P =
        ((@eulerCharacteristic k _ Z (i ≫ f) inferInstance
          (twistedSheaf (SheafOfModules.unit Z.ringCatSheaf)
            (fun j => (Scheme.Modules.pullback i).obj (L j)) n)
          (isCoherent_twistedSheafUnitPullback k f i L n) : ℤ) : ℚ)) ∧
        P.totalDegree ≤ d ∧
        ∃ m : ℤ, P.coeff (Finsupp.equivFunOnFinite.symm fun _ => 1) = (m : ℚ)
Tag 0BER, a lemma

Tag 0BER in the Stacks Project.

AlgebraicGeometry.intersectionNumber_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/Additivity.lean, line 499. The attribute's comment: “additivity of the intersection number in each invertible module”.

[Stacks, Tag 0BER]. The intersection number is additive in each slot: if 𝓛_j is the tensor product of 𝓛_j' and 𝓛_j'', and the three families of invertible modules agree away from j, then

(𝓛_1 ⋯ 𝓛_j ⋯ 𝓛_d · Z) = (𝓛_1 ⋯ 𝓛_j' ⋯ 𝓛_d · Z) + (𝓛_1 ⋯ 𝓛_j'' ⋯ 𝓛_d · Z).

public theorem intersectionNumber_tensor (k : Type u) [Field k] {X Z : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i]
    (d : ℕ) (hd : topologicalKrullDim Z ≤ d) (j : Fin d) (L L' L'' : Fin d → X.Modules)
    [∀ q, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L q)]
    [∀ q, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L' q)]
    [∀ q, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L'' q)]
    (hL' : ∀ q, q ≠ j → L' q = L q) (hL'' : ∀ q, q ≠ j → L'' q = L q)
    (hj : L j ≅ (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨X.presheaf,
        Presheaf.isSheaf_of_isSheaf_comp _ (X.presheaf) (forget₂ CommRingCat RingCat)
        (X.ringCatSheaf.2)⟩).obj ((L' j))).obj ((L'' j)))) :
    intersectionNumber k f i d hd L =
      intersectionNumber k f i d hd L' + intersectionNumber k f i d hd L''

AlgebraicGeometry.intersectionNumber_update_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/Additivity.lean, line 638. The attribute's comment: “additivity in the j-th slot, written with Function.update”.

[Stacks, Tag 0BER], the Function.update form. If 𝓛_j ≅ 𝓜 ⊗ 𝓝 then

(𝓛_1 ⋯ 𝓛_j ⋯ 𝓛_d · Z) = (𝓛_1 ⋯ 𝓜 ⋯ 𝓛_d · Z) + (𝓛_1 ⋯ 𝓝 ⋯ 𝓛_d · Z),

the two families on the right being the given one with its j-th member replaced.

public theorem intersectionNumber_update_tensor (k : Type u) [Field k] {X Z : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i]
    (d : ℕ) (hd : topologicalKrullDim Z ≤ d) (j : Fin d) (L : Fin d → X.Modules)
    [∀ q, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L q)] (M N : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 M]
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 N]
    (hj : L j ≅ (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨X.presheaf,
        Presheaf.isSheaf_of_isSheaf_comp _ (X.presheaf) (forget₂ CommRingCat RingCat)
        (X.ringCatSheaf.2)⟩).obj (M)).obj (N))) :
    intersectionNumber k f i d hd L =
      intersectionNumber k f i d hd (Function.update L j M) +
        intersectionNumber k f i d hd (Function.update L j N)
Tag 0BES, a lemma

Tag 0BES in the Stacks Project.

AlgebraicGeometry.intersectionNumber_eq_sum_topDimComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/Components.lean, line 118. The attribute's comment: “the intersection number is the length-weighted sum of the intersection numbers of the top-dimensional irreducible components”.

[Stacks, Tag 0BES]. Let k be a field, let X be proper over k, let i : Z ⟶ X be a closed subscheme of dimension d and let 𝓛_1, …, 𝓛_d be invertible 𝒪_X-modules. Writing Z_1, …, Z_t for the irreducible components of Z of dimension d, with generic points ξ_i and multiplicities m_i = length_{𝒪_{X, ξ_i}} 𝒪_{Z, ξ_i}, the intersection number of Z is the weighted sum of those of its components:

(𝓛_1 ⋯ 𝓛_d · Z) = ∑_i m_i (𝓛_1 ⋯ 𝓛_d · Z_i).

public theorem intersectionNumber_eq_sum_topDimComponents (k : Type u) [Field k]
    {X Z : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i]
    (d : ℕ) (hd : topologicalKrullDim Z = (d : WithBot ℕ∞)) (L : Fin d → X.Modules)
    [∀ j, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L j)] :
    intersectionNumber k f i d hd.le L =
      ∑ᶠ W : TopDimIntegralSubscheme
          ((Scheme.Modules.pushforward i).obj (Stacks.Ample.unitModule Z)),
        Stacks.Chow.sheafMultiplicity
            ((Scheme.Modules.pushforward i).obj (Stacks.Ample.unitModule Z)) W.genericPt *
          intersectionNumber k f W.1.subschemeι d
            (topologicalKrullDim_subscheme_le_of_topDimIntegralSubscheme i hd W) L

AlgebraicGeometry.intersectionNumber_eq_sum_dimComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/ComponentsVanishing.lean, line 199.

[Stacks, Tag 0BES]. Let k be a field, let X be proper over k, let i : Z ⟶ X be a closed subscheme of dimension at most d and let 𝓛_1, …, 𝓛_d be invertible 𝒪_X-modules. Writing Z_1, …, Z_t for the irreducible components of Z of dimension d, with generic points ξ_i and multiplicities m_i = length_{𝒪_{X, ξ_i}} 𝒪_{Z, ξ_i}, the intersection number of Z is the weighted sum of those of its d-dimensional components:

(𝓛_1 ⋯ 𝓛_d · Z) = ∑_i m_i (𝓛_1 ⋯ 𝓛_d · Z_i).

For dim Z = d this is AlgebraicGeometry.intersectionNumber_eq_sum_topDimComponents, the components of dimension d being then the top-dimensional ones; for dim Z < d both sides are zero, the sum being empty.

public theorem intersectionNumber_eq_sum_dimComponents (k : Type u) [Field k]
    {X Z : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i]
    (d : ℕ) (hd : topologicalKrullDim Z ≤ (d : WithBot ℕ∞)) (L : Fin d → X.Modules)
    [∀ j, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L j)] :
    intersectionNumber k f i d hd L =
      ∑ᶠ W : DimIntegralSubscheme
          ((Scheme.Modules.pushforward i).obj (Stacks.Ample.unitModule Z)) d,
        Stacks.Chow.sheafMultiplicity
            ((Scheme.Modules.pushforward i).obj (Stacks.Ample.unitModule Z)) W.genericPt *
          intersectionNumber k f W.1.subschemeι d W.topologicalKrullDim_le L
Tag 0BET, a lemma

Tag 0BET in the Stacks Project.

AlgebraicGeometry.intersectionNumber_pullback_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/Pullback.lean, line 662. The attribute's comment: “the right-hand side is zero when the scheme-theoretic image has dimension less than d”.

[Stacks, Tag 0BET], the case of a scheme-theoretic image of smaller dimension. Let k be a field, let f : Y ⟶ X be a morphism of schemes proper over k, let i : Z ⟶ Y be an integral closed subscheme of dimension at most d and let 𝓛_1, …, 𝓛_d be invertible 𝒪_X-modules. If the scheme-theoretic image f(Z) has dimension less than d, then

(f^*𝓛_1 ⋯ f^*𝓛_d · Z) = 0.

public theorem intersectionNumber_pullback_eq_zero (k : Type u) [Field k] {Y X Z : Scheme.{u}}
    (pY : Y ⟶ Spec (.of k)) (pX : X ⟶ Spec (.of k)) [IsProper pY] [IsProper pX]
    (f : Y ⟶ X) (hf : f ≫ pX = pY) (i : Z ⟶ Y) [IsClosedImmersion i] [IsIntegral Z]
    (d : ℕ) (hd : topologicalKrullDim Z ≤ (d : WithBot ℕ∞)) (L : Fin d → X.Modules)
    [∀ j, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L j)]
    (hIm : topologicalKrullDim (i ≫ f).image < (d : WithBot ℕ∞)) :
    intersectionNumber k pY i d hd (fun j => (Scheme.Modules.pullback f).obj (L j)) = 0

AlgebraicGeometry.intersectionNumber_pullback_eq_degreeOver_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/Pullback.lean, line 698. The attribute's comment: “the degree formula when the scheme-theoretic image has the same dimension”.

[Stacks, Tag 0BET], the equal-dimensional case. Let k be a field, let f : Y ⟶ X be a morphism of schemes proper over k, let i : Z ⟶ Y be an integral closed subscheme of dimension d and let 𝓛_1, …, 𝓛_d be invertible 𝒪_X-modules. If the scheme-theoretic image f(Z) again has dimension d, then

(f^*𝓛_1 ⋯ f^*𝓛_d · Z) = deg(f|_Z : Z → f(Z)) (𝓛_1 ⋯ 𝓛_d · f(Z)),

the degree being the one of [Stacks, Morphisms, Definition 02NY].

public theorem intersectionNumber_pullback_eq_degreeOver_mul (k : Type u) [Field k]
    {Y X Z : Scheme.{u}} (pY : Y ⟶ Spec (.of k)) (pX : X ⟶ Spec (.of k))
    [IsProper pY] [IsProper pX] (f : Y ⟶ X) (hf : f ≫ pX = pY) (i : Z ⟶ Y)
    [IsClosedImmersion i] [IsIntegral Z] (d : ℕ)
    (hZ : topologicalKrullDim Z = (d : WithBot ℕ∞)) (L : Fin d → X.Modules)
    [∀ j, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L j)]
    (hIm : topologicalKrullDim (i ≫ f).image = (d : WithBot ℕ∞)) :
    haveI : IsProper (i ≫ f) := isProper_comp_of_structureMap k pY pX f hf i
    haveI : IsIntegral (i ≫ f).image := Stacks.Chow.isIntegral_image (i ≫ f)
    haveI : IsProper (i ≫ f).toImage := Stacks.Chow.isProper_toImage (i ≫ f)
    intersectionNumber k pY i d hZ.le (fun j => (Scheme.Modules.pullback f).obj (L j)) =
      degreeOver (i ≫ f).toImage *
        intersectionNumber k pX (i ≫ f).imageι d hIm.le L
Tag 0BEU, a lemma

Tag 0BEU in the Stacks Project.

AlgebraicGeometry.intersectionNumber_eq_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/DivisorIntersectionProper.lean, line 92. The attribute's comment: “taking the divisor's dimension bound as an argument”.

[Stacks, Tag 0BEU]. Let k be a field, let X be a scheme proper over k, let i : Z ⟶ X be a closed subscheme of dimension at most d + 1 and let 𝓛_1, …, 𝓛_{d+1} be invertible 𝒪_X-modules. Let D ⊆ Z be an effective Cartier divisor of dimension at most d with 𝓛_1|_Z ≅ 𝒪_Z(D). Then

(𝓛_1 ⋯ 𝓛_{d+1} · Z) = (𝓛_2 ⋯ 𝓛_{d+1} · D),

the intersection number of the divisor being taken along the composite closed immersion D ⟶ Z ⟶ X.

This is AlgebraicGeometry.intersectionNumber_eq_intersectionNumber_of_isEffectiveCartierDivisor with its hypothesis hfin discharged by AlgebraicGeometry.forall_finiteDimensional_cohomologyOverField_of_isProper, which is [Stacks, Tag 02O6].

The bound hdD on the dimension of the divisor is still an argument here; it is not part of Tag 0BEU's data, being a consequence of hd, and it is discharged in AlgebraicGeometry.intersectionNumber_eq_of_isEffectiveCartierDivisor', which therefore carries the tag with no bound to supply. This form keeps its own registration.

public theorem intersectionNumber_eq_of_isEffectiveCartierDivisor
    (k : Type u) [Field k] {X Z : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f]
    (i : Z ⟶ X) [IsClosedImmersion i] (d : ℕ)
    (hd : topologicalKrullDim Z ≤ (d + 1 : ℕ)) (L : Fin (d + 1) → X.Modules)
    [∀ t, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L t)]
    (Dv : Z.IdealSheafData) [hDv : IsEffectiveCartierDivisor Dv]
    (hdD : topologicalKrullDim Dv.subscheme ≤ d)
    (hL : (Scheme.Modules.pullback i).obj (L 0) ≅ (invertibleSheaf Dv : Z.Modules)) :
    intersectionNumber k f i (d + 1) hd L =
      intersectionNumber k f (Dv.subschemeι ≫ i) d hdD fun t : Fin d => L t.succ

AlgebraicGeometry.intersectionNumber_eq_of_isEffectiveCartierDivisor', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/DivisorIntersectionProper.lean, line 142. The attribute's comment: “the intersection number of a closed subscheme against invertible modules equals that of an effective Cartier divisor cutting out the first module's restriction”.

[Stacks, Tag 0BEU]. Let k be a field, let X be a scheme proper over k, let i : Z ⟶ X be a closed subscheme of dimension at most d + 1 and let 𝓛_1, …, 𝓛_{d+1} be invertible 𝒪_X-modules. Let D ⊆ Z be an effective Cartier divisor with 𝓛_1|_Z ≅ 𝒪_Z(D). Then

(𝓛_1 ⋯ 𝓛_{d+1} · Z) = (𝓛_2 ⋯ 𝓛_{d+1} · D),

the intersection number of the divisor being taken along the composite closed immersion D ⟶ Z ⟶ X.

This is the tag with nothing assumed. Beyond hd, hL and the effective Cartier divisor instance — which are the tag's own data — it has no hypothesis: the dimension bound dim D ≤ d that the right-hand intersection number needs is supplied by AlgebraicGeometry.topologicalKrullDim_subscheme_le_of_isEffectiveCartierDivisor_of_isProper, since an effective Cartier divisor is nowhere dense and so loses a dimension.

public theorem intersectionNumber_eq_of_isEffectiveCartierDivisor'
    (k : Type u) [Field k] {X Z : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f]
    (i : Z ⟶ X) [IsClosedImmersion i] (d : ℕ)
    (hd : topologicalKrullDim Z ≤ (d + 1 : ℕ)) (L : Fin (d + 1) → X.Modules)
    [∀ t, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L t)]
    (Dv : Z.IdealSheafData) [hDv : IsEffectiveCartierDivisor Dv]
    (hL : (Scheme.Modules.pullback i).obj (L 0) ≅ (invertibleSheaf Dv : Z.Modules)) :
    intersectionNumber k f i (d + 1) hd L =
      intersectionNumber k f (Dv.subschemeι ≫ i) d
        (topologicalKrullDim_subscheme_le_of_isEffectiveCartierDivisor_of_isProper k f i d hd Dv)
        fun t : Fin d => L t.succ
Tag 0BEV, a lemma

Tag 0BEV in the Stacks Project.

AlgebraicGeometry.intersectionNumber_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/Positivity.lean, line 275.

[Stacks, Tag 0BEV]. Let k be a field, let X be a scheme proper over k, let i : Z ⟶ X be a closed subscheme of dimension d and let 𝓛_1, …, 𝓛_d be ample invertible 𝒪_X-modules. Then the intersection number (𝓛_1 ⋯ 𝓛_d · Z) is positive.

public theorem intersectionNumber_pos (k : Type u) [Field k] {X Z : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i] (d : ℕ)
    (hdim : topologicalKrullDim Z = (d : WithBot ℕ∞)) (L : Fin d → X.Modules)
    [∀ j, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L j)]
    (hL : ∀ j, Scheme.Modules.IsAmple X (L j)) :
    0 < intersectionNumber k f i d hdim.le L

AlgebraicGeometry.selfIntersectionNumber_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/Positivity.lean, line 286. The attribute's comment: “the self-intersection number of a single ample module”.

[Stacks, Tag 0BEV] for the self-intersection number (𝓛^d · Z) of a single ample invertible module.

public theorem selfIntersectionNumber_pos (k : Type u) [Field k] {X Z : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i] (d : ℕ)
    (hdim : topologicalKrullDim Z = (d : WithBot ℕ∞)) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
    (hL : Scheme.Modules.IsAmple X L) :
    0 < selfIntersectionNumber k f i d hdim.le L

AlgebraicGeometry.degreeWithRespectTo_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/Positivity.lean, line 297. The attribute's comment: “the degree deg_L(Z) of Tag 0BEW is positive”.

[Stacks, Tag 0BEV] for the degree deg_𝓛(Z) of [Stacks, Tag 0BEW]: the degree of a closed subscheme with respect to an ample invertible module is positive.

public theorem degreeWithRespectTo_pos (k : Type u) [Field k] {X Z : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i] (d : ℕ)
    (hdim : topologicalKrullDim Z = (d : WithBot ℕ∞)) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
    (hL : Scheme.Modules.IsAmple X L) :
    0 < degreeWithRespectTo k f i d hdim L hL
Tag 0BEW, a definition

Tag 0BEW in the Stacks Project.

AlgebraicGeometry.degreeWithRespectTo, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersection.lean, line 338.

Stacks 0BEW. The degree deg_𝓛(Z) of a closed subscheme i : Z ⟶ X of a proper scheme X over a field k with respect to an ample invertible 𝒪_X-module 𝓛: the intersection number (𝓛^d · Z) for d the dimension of Z.

The dimension is passed as a natural number d together with the hypothesis topologicalKrullDim Z = d, which is what makes d the source's dim(Z); d is therefore determined by the data and the degree does not depend on which d is supplied. An empty Z has dimension ⊥ and an infinite-dimensional Z has dimension ⊤, neither of which is (d : WithBot ℕ∞) for a natural number d, so no value is assigned to them — see the implementation notes. Ampleness is not used in the body: the source requires it so that deg_𝓛 deserves the name of a degree, and it is carried for that reason.

public noncomputable def degreeWithRespectTo (k : Type u) [Field k] {X Z : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i]
    (d : ℕ) (hd : topologicalKrullDim Z = d) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
    (_hample : Scheme.Modules.IsAmple X L) : ℤ
Tag 0BEX, a lemma

Tag 0BEX in the Stacks Project.

AlgebraicGeometry.selfIntersectionNumber_pullback_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/FiniteDominant.lean, line 227. The attribute's comment: “for an arbitrary invertible module, with no ampleness”.

[Stacks, Tag 0BEX]. Let k be a field, let f : Y ⟶ X be a finite dominant morphism of proper varieties over k of dimension d and let 𝓛 be an invertible 𝒪_X-module. Then

(f^*𝓛^d · Y) = deg(f) (𝓛^d · X),

the degree deg(f) = [R(Y) : R(X)] being AlgebraicGeometry.degreeOver of [Stacks, Morphisms, Definition 02NY]. For 𝓛 ample both sides are the degrees deg_{f^*𝓛}(Y) and deg_𝓛(X) of [Stacks, Tag 0BEW], which is the source's statement; see AlgebraicGeometry.degreeWithRespectTo_pullback_of_isFinite.

Ampleness is not assumed: it is not used by the source's proof and neither side needs it to be formed.

public theorem selfIntersectionNumber_pullback_of_isFinite (k : Type u) [Field k]
    {Y X : Scheme.{u}} (p : X ⟶ Spec (.of k)) [IsVariety k p] [IsProper p] (f : Y ⟶ X)
    [IsFinite f] [IsDominant f] [IsVariety k (f ≫ p)] (d : ℕ)
    (hd : topologicalKrullDim X = (d : WithBot ℕ∞)) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L] :
    selfIntersectionNumber k (f ≫ p) (𝟙 Y) d
          (((topologicalKrullDim_eq_of_isFinite_of_isDominant f).trans hd).le)
          ((Scheme.Modules.pullback f).obj L) =
      (degreeOver f : ℤ) * selfIntersectionNumber k p (𝟙 X) d hd.le L

AlgebraicGeometry.degreeWithRespectTo_pullback_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/FiniteDominant.lean, line 298.

[Stacks, Tag 0BEX]. Let k be a field, let f : Y ⟶ X be a finite dominant morphism of proper varieties over k and let 𝓛 be an ample invertible 𝒪_X-module. Then

deg_{f^*𝓛}(Y) = deg(f) deg_𝓛(X),

the degrees being those of [Stacks, Tag 0BEW] and deg(f) = [R(Y) : R(X)] that of [Stacks, Morphisms, Definition 02NY].

The dimension of X is passed as a natural number d together with topologicalKrullDim X = d, as AlgebraicGeometry.degreeWithRespectTo asks; the dimension of Y is then d too and is not a hypothesis. Neither is the ampleness of f^*𝓛 that the left-hand side needs: it is AlgebraicGeometry.isAmple_pullback_of_isFinite.

The content is AlgebraicGeometry.selfIntersectionNumber_pullback_of_isFinite, which does not mention ampleness; AlgebraicGeometry.degreeWithRespectTo is by definition the self-intersection number, so this is that statement read at the source's notation.

public theorem degreeWithRespectTo_pullback_of_isFinite (k : Type u) [Field k]
    {Y X : Scheme.{u}} (p : X ⟶ Spec (.of k)) [IsVariety k p] [IsProper p] (f : Y ⟶ X)
    [IsFinite f] [IsDominant f] [IsVariety k (f ≫ p)] (d : ℕ)
    (hd : topologicalKrullDim X = (d : WithBot ℕ∞)) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
    (hL : Scheme.Modules.IsAmple X L) :
    degreeWithRespectTo k (f ≫ p) (𝟙 Y) d
          ((topologicalKrullDim_eq_of_isFinite_of_isDominant f).trans hd)
          ((Scheme.Modules.pullback f).obj L) (isAmple_pullback_of_isFinite f L hL) =
      (degreeOver f : ℤ) * degreeWithRespectTo k p (𝟙 X) d hd L hL
Tag 0BEY, a lemma

Tag 0BEY in the Stacks Project.

AlgebraicGeometry.intersectionNumber_one_eq_invertibleCurveDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersection.lean, line 369.

Stacks 0BEY. For a closed subscheme Z ⊂ X of dimension at most one of a proper scheme X over a field k and an invertible 𝒪_X-module 𝓛, the intersection number (𝓛 · Z) is the degree deg(𝓛|_Z) of Stacks 0AYR.

The source's proof is that n ↦ χ(Z, 𝓛|_Z^{⊗ n}) has degree one, so its leading coefficient is the difference of consecutive values. With the finite difference as the definition that difference is the intersection number: the sum over Finset (Fin 1) has the two terms -χ(Z, 𝒪_Z) and χ(Z, 𝓛|_Z), the first twist being the trivial one (AlgebraicGeometry.twistedSheafZeroIso) and the second 𝓛|_Z itself (Stacks.SheafOfModules.Invertible.tensorPowerOneIso and the left unitor), and AlgebraicGeometry.invertibleCurveDegree is by definition their difference. Neither polynomiality nor a degree computation is needed, so the statement keeps the source's ≤ 1; it is in fact true for every Z.

public theorem intersectionNumber_one_eq_invertibleCurveDegree (k : Type u) [Field k]
    {X Z : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i]
    (hdim : topologicalKrullDim Z ≤ 1) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L] :
    intersectionNumber k f i 1 hdim (fun _ => L) =
      invertibleCurveDegree k (i ≫ f) hdim ((Scheme.Modules.pullback i).obj L)

AlgebraicGeometry.degreeWithRespectTo_eq_invertibleCurveDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersection.lean, line 425. The attribute's comment: “the ample case”.

Stacks 0BEY, the ample case. For a closed subscheme Z ⊂ X of dimension one of a proper scheme X over a field k and an ample invertible 𝒪_X-module 𝓛, the degree deg_𝓛(Z) of Stacks 0BEW is the degree deg(𝓛|_Z) of Stacks 0AYR.

The source states this for Z of dimension at most one, but at dimension zero the two numbers differ: deg_𝓛(Z) is then (𝓛^0 · Z) = χ(Z, 𝒪_Z) (AlgebraicGeometry.intersectionNumber_zero) while deg(𝓛|_Z) is χ(Z, 𝓛|_Z) - χ(Z, 𝒪_Z), and for a nonempty zero-dimensional Z the first is the positive integer dim_k Γ(Z, 𝒪_Z) and the second is 0. The hypothesis is therefore topologicalKrullDim Z = 1, which is where deg_𝓛(Z) is the intersection number (𝓛 · Z); the conclusion is then AlgebraicGeometry.intersectionNumber_one_eq_invertibleCurveDegree, which does keep the source's ≤ 1.

public theorem degreeWithRespectTo_eq_invertibleCurveDegree (k : Type u) [Field k]
    {X Z : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i]
    (hd : topologicalKrullDim Z = 1) (L : X.Modules)
    [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
    (hample : Scheme.Modules.IsAmple X L) :
    degreeWithRespectTo k f i 1 hd L hample =
      invertibleCurveDegree k (i ≫ f) hd.le ((Scheme.Modules.pullback i).obj L)
Tag 0BJ8, a proposition

Tag 0BJ8 in the Stacks Project.

AlgebraicGeometry.degreeWithRespectTo_div_factorial_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/AsymptoticRiemannRoch.lean, line 276. The attribute's comment: “the leading coefficient deg_L(X)/d! is a positive constant”.

[Stacks, Tag 0BJ8], the leading coefficient. For X proper over k of dimension d and 𝓛 ample, the constant deg_𝓛(X)/d! is positive. The degree deg_𝓛(X) is positive by [Stacks, Tag 0BEV] and d! is positive.

public theorem degreeWithRespectTo_div_factorial_pos :
    0 < (degreeWithRespectTo k f (𝟙 X) d hdim L hL : ℚ) / (d.factorial : ℚ)

AlgebraicGeometry.exists_degree_lt_eventually_finrank_globalSections_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/AsymptoticRiemannRoch.lean, line 382. The attribute's comment: “the asymptotic formula for dim_k Γ(X, L^n)”.

[Stacks, Tag 0BJ8], the asymptotic formula. For X proper over k of dimension d and 𝓛 ample, for all sufficiently large n

dim_k Γ(X, 𝓛^{⊗ n}) = deg_𝓛(X)/d! ⬝ n^d + P(n)

with P a rational polynomial of degree strictly less than d.

public theorem exists_degree_lt_eventually_finrank_globalSections_eq :
    ∃ P : Polynomial ℚ, P.degree < (d : WithBot ℕ) ∧
      ∀ᶠ n : ℕ in atTop,
        (Module.finrank k (globalSectionsOverField k f
            (tensorPower X.presheaf X.ringCatSheaf.2 L (n : ℤ))) : ℚ) =
          (degreeWithRespectTo k f (𝟙 X) d hdim L hL : ℚ) / (d.factorial : ℚ) * (n : ℚ) ^ d +
            P.eval (n : ℚ)

AlgebraicGeometry.asymptotic_riemann_roch, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/AsymptoticRiemannRoch.lean, line 466.

[Stacks, Tag 0BJ8] (Asymptotic Riemann–Roch). Let k be a field, let X be a scheme proper over k of dimension d and let 𝓛 be an ample invertible 𝒪_X-module. Then

dim_k Γ(X, 𝓛^{⊗ n}) = deg_𝓛(X)/d! ⬝ n^d + lower order terms

for all sufficiently large n, and the leading constant deg_𝓛(X)/d! is positive.

public theorem asymptotic_riemann_roch :
    0 < (degreeWithRespectTo k f (𝟙 X) d hdim L hL : ℚ) / (d.factorial : ℚ) ∧
      ∃ P : Polynomial ℚ, P.degree < (d : WithBot ℕ) ∧
        ∀ᶠ n : ℕ in atTop,
          (Module.finrank k (globalSectionsOverField k f
              (tensorPower X.presheaf X.ringCatSheaf.2 L (n : ℤ))) : ℚ) =
            (degreeWithRespectTo k f (𝟙 X) d hdim L hL : ℚ) / (d.factorial : ℚ) * (n : ℚ) ^ d +
              P.eval (n : ℚ)
Sources
LeanAlgebraicGeometry.exists_eulerPolynomial_twistedSheaf_of_isProper · AlgebraicGeometry.exists_eulerPolynomial_sub_topDimComponents_totalDegree_lt · AlgebraicGeometry.intersectionNumber · AlgebraicGeometry.intersectionNumber_eq_coeff · AlgebraicGeometry.selfIntersectionNumber · AlgebraicGeometry.intersectionNumber_isInteger · AlgebraicGeometry.intersectionNumber_tensor · AlgebraicGeometry.intersectionNumber_update_tensor

Section33.46 Embedding dimension#

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

Tag 0C1Q, a definition

Tag 0C1Q in the Stacks Project.

AlgebraicGeometry.Scheme.embeddingDimension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/EmbeddingDimension.lean, line 49.

The dimension of the cotangent space of the local ring of X at x, over its residue field.

abbrev Scheme.embeddingDimension (X : Scheme.{u}) (x : X) [FiniteDimensional
    (ResidueField (X.presheaf.stalk x)) (CotangentSpace (X.presheaf.stalk x))] : ℕ
Tag 0C2H, a definition

Tag 0C2H in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.embeddingDimension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Tangent/EmbeddingDimension.lean, line 55.

The dimension over κ(x) of the tangent space of X over k at x.

abbrev Scheme.Hom.embeddingDimension (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] (x : X) : ℕ
Sources
LeanAlgebraicGeometry.Scheme.embeddingDimension · AlgebraicGeometry.Scheme.Hom.embeddingDimension

Section33.47 Bertini theorems#

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

Tag 0FD5, a lemma

Tag 0FD5 in the Stacks Project.

Stacks.SectionsVanishingOnSubscheme.exists_bound_generatesOffSupport_and_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/VanishingSystemImmersion/Basic.lean, line 790.

[Stacks, Tag 0FD5]. Let k be a field, let X be a proper scheme over k, let ℒ be an ample invertible 𝒪_X-module and let Z ⊂ X be the closed subscheme cut out by a quasi-coherent sheaf of ideals I. Then there is an integer n₀ such that for every n ≥ n₀ the kernel V_n of Γ(X, ℒ ^⊗ n) ⟶ Γ(Z, ℒ ^⊗ n|_Z) generates ℒ ^⊗ n on X ∖ Z and the canonical morphism

X ∖ Z ⟶ 𝐏(V_n)

of [Stacks, Tag 0FCY] is an immersion of schemes over k.

The generation is the hypothesis h the existential carries: GeneratesOffSupport k f I L n says that the germs of the members of V_n span the stalk of ℒ ^⊗ n at every point of X ∖ Z, and it is what makes the canonical morphism exist. That morphism is AlgebraicGeometry.toProjectiveSpaceOfModule, the morphism of [Stacks, Tag 0FCY], applied to the linear system V_n restricted to X ∖ Z: that is what Stacks.SectionsVanishingOnSubscheme.toProjectiveSpaceOfVanishingSections_eq proves the morphism named below to be. The source speaks of the canonical morphism, which is basis free, and the conclusion is asserted for the morphism built in every basis of V_n — the presentation of 𝐏(V_n) as ℙᴺ_k that [Stacks, Tag 0FCY] is stated with needs one.

theorem exists_bound_generatesOffSupport_and_isImmersion [IsProper f]
    (hL : IsAmple X L) :
    ∃ n₀ : ℤ, ∀ n : ℤ, n₀ ≤ n → ∃ h : GeneratesOffSupport k f I L n,
      ∀ (N : ℕ) (b : Module.Basis (Fin (N + 1)) k (vanishingSections k f I L n)),
        IsImmersion (toProjectiveSpaceOfVanishingSections k f b h) ∧
        toProjectiveSpaceOfVanishingSections k f b h ≫
            projectiveSpaceOfModuleToSpec k (vanishingSections k f I L n) =
          (openComplement I).ι ≫ f
Tag 0G47, a situation

Tag 0G47 in the Stacks Project.

Stacks.Bertini.FamilyDivisors.divisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniCommonZeroSet.lean, line 89. The attribute's comment: “the divisor of a vector of the linear system”.

The divisor H_w = Z(ψ(w)) cut out on X by a vector of the linear system, as a quasi-coherent ideal sheaf.

def divisor (w : D.V) : D.X.IdealSheafData

Stacks.Bertini.FamilyDivisors, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniFamilyDivisors.lean, line 94. The attribute's comment: “the standing situation”.

Stacks Project, Tag 0G47. The standing situation of the Bertini theorems: a field k, a scheme X over k, an invertible 𝒪_X-module L, a finite dimensional k-vector space V with a chosen basis v₁, …, v_r, and a k-linear map ψ : V → Γ(X, L).

structure FamilyDivisors

Stacks.Bertini.FamilyDivisors.universalSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniFamilyDivisors.lean, line 172. The attribute's comment: “the universal section”.

The universal section s_univ = Σᵢ xᵢ ψ(vᵢ) of pr₂^* L on 𝔸^r_k ×_k X, where x₁, …, x_r are the coordinates of the parameter affine space.

def universalSection :
    Γ((Scheme.Modules.pullback D.parameterProjection).obj D.L, ⊤)

Stacks.Bertini.FamilyDivisors.universalDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniFamilyDivisors.lean, line 181. The attribute's comment: “the universal divisor”.

The universal divisor H_univ = Z(s_univ) ⊂ 𝔸^r_k ×_k X, the zero scheme of the universal section.

def universalDivisor : D.parameterSpace.IdealSheafData

Stacks.Bertini.FamilyDivisors.specializedSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniFamilyDivisors.lean, line 206. The attribute's comment: “the section attached to a vector over an extension field”.

The section ψ(v) = Σᵢ aᵢ ψ(vᵢ) of L|_{X_{k'}} attached to the vector v = Σᵢ aᵢ vᵢ of V ⊗_k k' with coordinate tuple a over a field extension k'/k.

def specializedSection (a : Fin (Module.finrank D.k D.V) → K) :
    Γ((Scheme.Modules.pullback (D.baseChangeToX K)).obj D.L, ⊤)

Stacks.Bertini.FamilyDivisors.specializedDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniFamilyDivisors.lean, line 215. The attribute's comment: “the divisor attached to a vector over an extension field”.

The divisor H_v = Z(ψ(v)) on X_{k'} attached to the vector of V ⊗_k k' with coordinate tuple a, as the zero scheme of the section it determines.

def specializedDivisor (a : Fin (Module.finrank D.k D.V) → K) :
    (D.baseChange K).IdealSheafData

Stacks.Bertini.FamilyDivisors.specializedDivisor_eq_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniFamilyDivisors.lean, line 248. The attribute's comment: “the fibre of the universal divisor”.

H_v = H_{univ, v}. The divisor attached to a vector of V ⊗_k k' is the fibre of the universal divisor over the corresponding k'-point of 𝔸^r_k, as quasi-coherent sheaves of ideals on X_{k'}.

theorem specializedDivisor_eq_comap (a : Fin (Module.finrank D.k D.V) → K) :
    D.specializedDivisor K a = D.universalDivisor.comap (D.fibreParameterMap K a)

Stacks.Bertini.FamilyDivisors.ForGeneral, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniFamilyDivisors.lean, line 268. The attribute's comment: “holding for general vectors”.

A property of vectors holds for general v when there is one nonempty open U ⊂ 𝔸^r_k such that P holds at every vector of V ⊗_k k' whose coordinate tuple gives a k'-point of U, for every field extension k'/k.

def ForGeneral
    (P : ∀ (K : Type u) [Field K] [Algebra D.k K], TensorProduct D.k D.V K → Prop) : Prop
Tag 0FD6, a lemma

Tag 0FD6 in the Stacks Project.

Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_basis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniFieldBaseChangeDescent.lean, line 300. The attribute's comment: “the conclusion from hypotheses (1), (2) and (3) over an ARBITRARY base field -- the algebraically closed case is no longer assumed, the reduction of Tag 02FY to it being carried out by forGeneral_smooth_specializedDivisor_of_forGeneral_baseChangeAlgebraicClosure. No proof obligation and no dimension datum is assumed, and quasi-compactness of X is derived from hypothesis (3) rather than assumed. Carrying a basis of the linear system is NOT a deviation: Situation 0G47 itself says 'Say dim(V) = r and we have a basis v_1, ..., v_r of V', so the basis is the source's own datum, and by isImmersive_congr_basis' the hypothesis does not depend on which basis it is read at. ONE deviation survives, and it is only this: the index type Fin (m + 1) forces dim V >= 1, where the source allows the degenerate r = 0 (there H_univ = X and the conclusion holds trivially by hypothesis (1)). Separately, (3) is spelled through the morphism built from that basis rather than through the source's canonical phi_(L, psi) characterised by theta : phi^*O(1) = L -- the same input Tag 01ND is registered without”.

[Stacks, Tag 0FD6]. In the standing situation of [Stacks, Tag 0G47] with X smooth over a field k, if the image of ψ generates L and the morphism φ_{L,ψ} : X → 𝐏(V) it determines is an immersion, then the divisor H_v is smooth over k' for general v ∈ V ⊗_k k'.

This is the statement with no hypothesis that k be algebraically closed: that case is Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_generates_pointwise_of_ basis', and the reduction of [Stacks, Tag 02FY] to it is Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_baseChange AlgebraicClosure followed by Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_forGeneral_ baseChangeAlgebraicClosure.

The registration stays qualified for one reason only: hypothesis (3) is spelled as the immersiveness of φ read at a basis of V indexed by Fin (m + 1) rather than on the intrinsic morphism φ_{L,ψ}. Carrying a basis so indexed is an input the source does not make — it forces dim_k V = m + 1, in particular V ≠ 0 — and the two readings of (3) agree only up to an identity the repository cannot yet prove. Everything else is the source's: (1) is the instance [Smooth D.toBase], (2) is hgen, quasi-compactness of X is derived rather than assumed, and no dimension datum or proof obligation is taken.

theorem forGeneral_smooth_specializedDivisor_of_basis [Smooth D.toBase] (hgen : D.Generates)
    {m : ℕ} (b : Module.Basis (Fin (m + 1)) D.k D.V)
    (himm : D.IsImmersive b (D.generatesBy_basis hgen b)) :
    D.ForGeneral (fun K _ _ w =>
      ∀ a : Fin (Module.finrank D.k D.V) → K,
        w = ∑ i, TensorProduct.tmul D.k (D.basis i) (a i) →
          Smooth ((D.specializedDivisor K a).subschemeι ≫ D.baseChangeToSpec K))

Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniFieldBaseChangeDescent.lean, line 376.

[Stacks, Tag 0FD6]. In the standing situation of [Stacks, Tag 0G47] with X smooth over a field k, if the image of ψ generates L and the morphism φ_{L,ψ} : X → 𝐏(V) it determines is an immersion, then the divisor H_v is smooth over k' for general v ∈ V ⊗_k k'.

This takes the data of [Stacks, Tag 0G47] — the field k, the scheme X over it, the invertible module L, the finite dimensional linear system V with its basis, and ψ — and the source's three hypotheses, and nothing else: (1) is the instance [Smooth D.toBase], (2) is hgen, and (3) is himm. There is no hypothesis that k be algebraically closed, no quasi-compactness assumption, no dimension datum, no proof obligation, and no condition on dim V: the degenerate case dim V = 0 that the source allows is Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_finrank_eq_zero, and dim V ≥ 1 is Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_basis, the basis of the standing situation reindexed along dim V = m + 1.

Hypothesis (3) is read at every basis of V indexed by some Fin (m + 1) rather than at one: that is not a strengthening, because by Stacks.Bertini.FamilyDivisors.isImmersive_congr_basis' the hypothesis holds at one such basis exactly when it holds at all of them, and when dim V = 0 there are none and himm says nothing — which is what lets the degenerate case be covered at all.

One caveat on hypothesis (3). It is spelled through the morphism built from a basis rather than through the source's canonical φ_{L,ψ} characterised by θ : φ^*𝒪(1) ≅ L; that is the same input [Stacks, Tag 01ND] is itself registered without, and Stacks.Bertini.FamilyDivisors.isImmersive_congr_basis' shows the hypothesis does not depend on which basis it is read at.

theorem forGeneral_smooth_specializedDivisor [Smooth D.toBase] (hgen : D.Generates)
    (himm : ∀ (m : ℕ) (b : Module.Basis (Fin (m + 1)) D.k D.V),
      D.IsImmersive b (D.generatesBy_basis hgen b)) :
    D.ForGeneral (fun K _ _ w =>
      ∀ a : Fin (Module.finrank D.k D.V) → K,
        w = ∑ i, TensorProduct.tmul D.k (D.basis i) (a i) →
          Smooth ((D.specializedDivisor K a).subschemeι ≫ D.baseChangeToSpec K))

Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_baseChangeAlgebraicClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniFieldBaseChangeImmersion.lean, line 134. The attribute's comment: “the conclusion of the tag for the standing situation base changed to an algebraic closure of the base field, with hypotheses (1), (2) and (3) assumed only for the original situation over k -- hypothesis (3) transfers by isImmersive_baseChangeFamily. This is NOT the tag for an arbitrary base field: the descent of the conclusion from kbar back to k (the reduction of Tag 02FY) needs a nonempty open of A^r_k whose points lift into the given nonempty open of A^r_kbar, which is not proved. Hypothesis (3) is also still spelled at a basis of the linear system rather than on the intrinsic morphism phi_(L, psi)”.

[Stacks, Tag 0FD6] for the situation base changed to an algebraic closure of the base field, from the source's three hypotheses for the original situation. X smooth over k, the image of ψ generating L, and φ_{L,ψ} an immersion: then over k̄ the divisor H_v is smooth for general v.

All three hypotheses transfer to D.baseChangeAlgebraicClosure (Stacks.Bertini.FamilyDivisors.smooth_baseChangeFamily, Stacks.Bertini.FamilyDivisors.generates_baseChangeFamily and Stacks.Bertini.FamilyDivisors.isImmersive_baseChangeFamily), and k̄ is algebraically closed, so the carrier of the tag applies to the base-changed situation.

The registration is qualified: the conclusion drawn is the tag's conclusion for D.baseChangeAlgebraicClosure, not for D, and the passage between the two is what [Stacks, Tag 02FY] still owes — a nonempty open of 𝔸^r_k whose points lift into the given nonempty open of 𝔸^r_{k̄}, together with the identification of H_v on X_{k'} with its own base change.

theorem forGeneral_smooth_specializedDivisor_baseChangeAlgebraicClosure [Smooth D.toBase]
    (hgen : D.Generates) {m : ℕ} (b : Module.Basis (Fin (m + 1)) D.k D.V)
    (himm : D.IsImmersive b (D.generatesBy_basis hgen b)) :
    D.baseChangeAlgebraicClosure.ForGeneral (fun K' _ _ w =>
      ∀ a : Fin (Module.finrank D.baseChangeAlgebraicClosure.k
          D.baseChangeAlgebraicClosure.V) → K',
        w = ∑ i, TensorProduct.tmul D.baseChangeAlgebraicClosure.k
            (D.baseChangeAlgebraicClosure.basis i) (a i) →
          Smooth ((D.baseChangeAlgebraicClosure.specializedDivisor K' a).subschemeι ≫
            D.baseChangeAlgebraicClosure.baseChangeToSpec K'))

Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_generates_pointwise_of_basis', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniImmersionQuasiCompact.lean, line 147. The attribute's comment: “the conclusion from hypotheses (2) and (3) with no proof obligation and no dimension data assumed, with (3) at an arbitrary basis of the linear system, and with quasi-compactness of X no longer assumed -- it is derived from hypothesis (3), P(V) having a Noetherian space. ONE hypothesis here is not the source's: that k is algebraically closed, the case Tag 02FY reduces to. (3) is also still spelled at a basis rather than on the intrinsic morphism phi_(L, psi), but that is now only a spelling: they agree by Stacks.Bertini.FamilyDivisors.isImmersive_congr_basis, so the hypothesis is independent of the basis it is read at; what is still unproved is its agreement with the source's canonical phi_(L, psi) as characterised by theta : phi^*O(1) = L, the same input Tag 01ND is registered without”.

[Stacks, Tag 0FD6]. In the standing situation of [Stacks, Tag 0G47] with X smooth over an algebraically closed field k, if the image of ψ generates L and the morphism φ_{L,ψ} : X → 𝐏(V) it determines is an immersion, then the divisor H_v is smooth over k' for general v ∈ V ⊗_k k'.

This is Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_generates_pointwise_of_ basis with [QuasiCompact D.toBase] removed. That binder was not a hypothesis of the source: [Stacks, Tag 0G47] assumes of X only that it is a scheme over k, and [Stacks, Tag 0FD6] adds only smoothness, generation and the immersion — and smoothness gives X locally of finite presentation, hence locally of finite type, but not quasi-compact. It is discharged rather than dropped, from the immersion hypothesis itself: see Stacks.Bertini.FamilyDivisors.quasiCompact_of_isImmersive.

[IsAlgClosed D.k] is then the only hypothesis of this statement that the source does not make. It is the case the source reduces to by [Stacks, Tag 02FY]; that reduction is a development of its own rather than a loose end. Its first half is done: the base change of the whole standing situation along k → k̄ is Stacks.Bertini.FamilyDivisors.baseChangeAlgebraicClosure, all three hypotheses transfer to it — the third by Stacks.Bertini.FamilyDivisors.isImmersive_baseChangeFamily — and Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_baseChangeAlgebraicClosure draws the conclusion of this statement over k̄ from the source's three hypotheses over k. What is still owed is the descent of that conclusion: a nonempty open of 𝔸^r_k whose points lift into the nonempty open of 𝔸^r_{k̄} the conclusion over k̄ provides, and the identification of H_v on X_{k'} with its own base change along an extension of k'. Hypothesis (3) is also still spelled at a basis of V rather than on the intrinsic morphism φ_{L,ψ} — but that is now only a spelling, the two agreeing by Stacks.Bertini.FamilyDivisors.isImmersive_congr_basis, so hypothesis (3) does not depend on which basis it is read at. What is not yet proved is its agreement with the source's canonical φ_{L,ψ} as characterised by an isomorphism θ : φ^*𝒪(1) ≅ ℒ through which ψ factors — the same input [Stacks, Tag 01ND] is registered without.

theorem forGeneral_smooth_specializedDivisor_of_generates_pointwise_of_basis' [IsAlgClosed D.k]
    [Smooth D.toBase] (hgen : D.Generates) {m : ℕ}
    (b : Module.Basis (Fin (m + 1)) D.k D.V)
    (himm : D.IsImmersive b (D.generatesBy_basis hgen b)) :
    D.ForGeneral (fun K _ _ w =>
      ∀ a : Fin (Module.finrank D.k D.V) → K,
        w = ∑ i, TensorProduct.tmul D.k (D.basis i) (a i) →
          Smooth ((D.specializedDivisor K a).subschemeι ≫ D.baseChangeToSpec K))

Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_generates_pointwise, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniJacobianDivisor.lean, line 613. The attribute's comment: “the conclusion from hypotheses (2) and (3) with no proof obligation assumed and no dimension data assumed -- the whole of the source's proof is discharged, the count being run at each closed point with the local dimension of X there -- but over an algebraically closed field, and with (3) taken at the standing basis; the source assumes neither of those two”.

[Stacks, Tag 0FD6]. In the standing situation of [Stacks, Tag 0G47] with X smooth and of finite type over an algebraically closed field k, if the image of ψ generates L and the morphism φ_{L,ψ} : X → 𝐏(V) it determines is an immersion, then the divisor H_v is smooth over k' for general v ∈ V ⊗_k k'.

This is Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_generates with its three non-source numerical and finiteness hypotheses removed. Hypothesis (1) of the tag is [Smooth D.toBase] together with [QuasiCompact D.toBase], which is X of finite type over k in the shape clause (1) of Stacks.Bertini.FamilyDivisors.Hypotheses uses; hypothesis (2) is Stacks.Bertini.FamilyDivisors.Generates and hypothesis (3) is Stacks.Bertini.FamilyDivisors.IsImmersive. The whole of the source's proof is proved, as for that theorem, and in addition:

  • the Noetherianness of H_univ, which is derived from X being of finite type over k (Stacks.Bertini.FamilyDivisors.noetherianSpace_universalDivisorScheme) rather than assumed;
  • the dimension data. The count is run at each closed point x of X with the local dimension n_x of X at x in place of one global n: n_x exists because the local ring of a smooth scheme at a closed point is regular (Stacks.Bertini.FamilyDivisors.exists_natCast_eq_topologicalKrullDimAt_of_isClosed), the inequality n_x + 1 ≤ dim V is read off the surjectivity of ev_x (Stacks.Bertini.FamilyDivisors.succ_le_of_smooth) as it is in the source, and the fibre bound dim V - (n_x + 1) is combined with n_x itself rather than with a global bound, by AlgebraicGeometry.topologicalKrullDim_le_of_isClosed_singleton_fiber_add_target. So no equidimensionality, no bound on dim X, and no numerical hypothesis n + 1 ≤ dim V remain.

What remains in the signature and is not a hypothesis of the source: [IsAlgClosed D.k], the case the source reduces to by [Stacks, Tag 02FY], a reduction not formalized here; and that hypothesis (3) is taken at the standing basis of the linear system read through Fin (m + 1) rather than at an arbitrary basis.

theorem forGeneral_smooth_specializedDivisor_of_generates_pointwise [IsAlgClosed D.k]
    [Smooth D.toBase] [QuasiCompact D.toBase] (hgen : D.Generates) {m : ℕ}
    (hm : Module.finrank D.k D.V = m + 1)
    (himm : D.IsImmersive (D.basis.reindex (finCongr hm))
      (D.generatesBy_basis hgen (D.basis.reindex (finCongr hm)))) :
    D.ForGeneral (fun K _ _ w =>
      ∀ a : Fin (Module.finrank D.k D.V) → K,
        w = ∑ i, TensorProduct.tmul D.k (D.basis i) (a i) →
          Smooth ((D.specializedDivisor K a).subschemeι ≫ D.baseChangeToSpec K))

Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_generates_pointwise_of_basis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniJacobianDivisor.lean, line 681. The attribute's comment: “the conclusion from hypotheses (2) and (3) with no proof obligation and no dimension data assumed, and with (3) at an arbitrary basis of the linear system -- the whole of the source's proof is discharged, the count being run at each closed point with the local dimension of X there. TWO hypotheses here are not the source's: that k is algebraically closed, the case Tag 02FY reduces to, and [QuasiCompact D.toBase]. Situation 0G47 assumes only that X is a scheme over k and Tag 0FD6 adds only smoothness, so quasi-compactness is an addition; it is NOT clause (1) of this project's Hypotheses bundle, which is Tag 0G4F's hypothesis, not 0G47's standing situation. (3) is also still spelled at a basis rather than on the intrinsic morphism phi_(L, psi), but that is now only a spelling: the two agree by Stacks.Bertini.FamilyDivisors.isImmersive_congr_basis, so the hypothesis does not depend on which basis it is read at”.

[Stacks, Tag 0FD6]. In the standing situation of [Stacks, Tag 0G47] with X smooth and of finite type over an algebraically closed field k, if the image of ψ generates L and the morphism φ_{L,ψ} : X → 𝐏(V) it determines is an immersion, then the divisor H_v is smooth over k' for general v ∈ V ⊗_k k'.

This is Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_generates_pointwise with hypothesis (3) taken at an arbitrary basis of the linear system rather than at the standing basis: the basis b is any basis of V, and the generation hypothesis at it is hypothesis (2) of the tag, which is basis free (Stacks.Bertini.FamilyDivisors.generates_iff_generatesBy_basis). No relation between b and the standing basis D.basis is assumed, and no bound on dim V is needed: b itself exhibits one.

The basis enters the proof in two roles, which this statement separates. Hypothesis (3) feeds only the surjectivity of the evaluation ev_x, a property of the basis-free map Stacks.Bertini.FamilyDivisors.evalVector and so of no basis at all (Stacks.Bertini.FamilyDivisors.surjective_evalCoord_sectionOf_iff); the Jacobian criterion Stacks.Bertini.FamilyDivisors.JacobianAtDivisor, on the other hand, can only be stated against the standing basis, since the coordinates of the parameter space are coefficients against it. The chain Stacks.Bertini.FamilyDivisors.exists_evalMatrix_of_basis → …smooth_specializedDivisor_forGeneral_of_jacobianAtDivisor_pointwise_of_basis carries the two as separate parameters, and this statement instantiates the second at D.basis.reindex (finCongr …), which is where Stacks.Bertini.FamilyDivisors.jacobianAtDivisor applies.

What remains in the signature and is not a hypothesis of the source: [IsAlgClosed D.k] and [QuasiCompact D.toBase]. [Smooth D.toBase] is hypothesis (1); it gives X locally of finite presentation, hence locally of finite type, but not quasi-compact, so [QuasiCompact D.toBase] is an addition — [Stacks, Tag 0G47] assumes of X only that it is a scheme over k, and clause (1) of Stacks.Bertini.FamilyDivisors.Hypotheses, which does assume finite type, is [Stacks, Tag 0G4F]'s hypothesis rather than 0G47's standing situation. It is however not needed: hypothesis (3) implies it, since 𝐏(V) has a Noetherian underlying space and an immersion embeds X in it. The sibling Stacks.Bertini.FamilyDivisors.forGeneral_smooth_specializedDivisor_of_generates_pointwise_of_ basis' is this statement with the binder discharged that way; see Stacks.Bertini.FamilyDivisors.quasiCompact_of_isImmersive. Every proof obligation of the source's argument is discharged, and so is all the dimension data: no equidimensionality of X, no bound on dim X, no inequality n + 1 ≤ dim V, and no Noetherianness of H_univ is assumed, the count being run at each closed point of X with the local dimension of X there. [IsAlgClosed D.k] is the case the source reduces to by [Stacks, Tag 02FY]; that reduction is not formalized here, and it is not a loose end but a development of its own — it needs the base change of the standing situation along k → k̄, which nothing in the library constructs, and above all the transfer of hypothesis (3) itself, for which the base-change compatibility of AlgebraicGeometry.toProjectiveSpaceOfModule is missing.

theorem forGeneral_smooth_specializedDivisor_of_generates_pointwise_of_basis [IsAlgClosed D.k]
    [Smooth D.toBase] [QuasiCompact D.toBase] (hgen : D.Generates) {m : ℕ}
    (b : Module.Basis (Fin (m + 1)) D.k D.V)
    (himm : D.IsImmersive b (D.generatesBy_basis hgen b)) :
    D.ForGeneral (fun K _ _ w =>
      ∀ a : Fin (Module.finrank D.k D.V) → K,
        w = ∑ i, TensorProduct.tmul D.k (D.basis i) (a i) →
          Smooth ((D.specializedDivisor K a).subschemeι ≫ D.baseChangeToSpec K))

Stacks.Bertini.FamilyDivisors.smooth_specializedDivisor_forGeneral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/BertiniSmooth.lean, line 147. The attribute's comment: “carrying the Tag 0B2L dimension bound on the singular locus of q”.

In the standing situation of Stacks.Bertini.FamilyDivisors with X smooth over k, the divisor H_v is smooth over k' for general v ∈ V ⊗_k k'.

It takes as hypothesis hsing: there is a nonempty open U of 𝔸^r_k whose preimage under q : H_univ → 𝔸^r_k lies in the smooth locus of q. It also takes the instance argument LocallyOfFinitePresentation q, which locallyOfFinitePresentation_universalFamilyMap supplies from the smoothness of X over k.

public theorem smooth_specializedDivisor_forGeneral [Smooth D.toBase]
    [LocallyOfFinitePresentation D.universalFamilyMap]
    (U : D.parameterBase.Opens) (hU : (U : Set D.parameterBase).Nonempty)
    (hsing : ((D.universalFamilyMap ⁻¹ᵁ U : D.universalDivisor.subscheme.Opens) :
        Set D.universalDivisor.subscheme) ⊆
      (D.universalFamilyMap.smoothLocus : Set D.universalDivisor.subscheme)) :
    D.ForGeneral (fun K _ _ w =>
      ∀ a : Fin (Module.finrank D.k D.V) → K,
        w = ∑ i, TensorProduct.tmul D.k (D.basis i) (a i) →
          Smooth ((D.specializedDivisor K a).subschemeι ≫ D.baseChangeToSpec K))
Sources
LeanStacks.SectionsVanishingOnSubscheme.exists_bound_generatesOffSupport_and_isImmersion · Stacks.Bertini.FamilyDivisors.divisor · Stacks.Bertini.FamilyDivisors · Stacks.Bertini.FamilyDivisors.universalSection · Stacks.Bertini.FamilyDivisors.universalDivisor · Stacks.Bertini.FamilyDivisors.specializedSection · Stacks.Bertini.FamilyDivisors.specializedDivisor · Stacks.Bertini.FamilyDivisors.specializedDivisor_eq_comap

Section33.48 Enriques-Severi-Zariski#

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

Tag 0FD7, a lemma

Tag 0FD7 in the Stacks Project.

Stacks.EnriquesSeveriZariski.forall_le_eq_zero_sections_twist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EnriquesSeveriZariski/Basic.lean, line 407. The attribute's comment: “the vanishing stated on the global sections themselves”.

[Stacks, Tag 0FD7], on global sections. Let k be a field, let X be a proper scheme over k, let ℒ be an ample invertible 𝒪_X-module and let ℱ be a coherent 𝒪_X-module. If Ass(ℱ) contains no closed points then Γ(X, ℱ ⊗ ℒ^{⊗ n}) = 0 for all n ≪ 0.

theorem forall_le_eq_zero_sections_twist (k : Type u) [Field k] (f : X ⟶ Spec (.of k))
    [IsProper f] (hL : Stacks.Ample.IsAmple X L) (F : X.Modules) [F.IsCoherent]
    (hAss : ∀ x : X, IsClosed ({x} : Set X) → x ∉ Stacks.Divisors.associatedPoints F) :
    ∃ n₀ : ℤ, ∀ n : ℤ, n ≤ n₀ → ∀ t : Γ(twist L F n, ⊤), t = 0

Stacks.EnriquesSeveriZariski.exists_forall_le_isZero_globalSectionsOverField_twist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EnriquesSeveriZariski/Basic.lean, line 432.

[Stacks, Tag 0FD7]. Let k be a field, let X be a proper scheme over k, let ℒ be an ample invertible 𝒪_X-module and let ℱ be a coherent 𝒪_X-module. If Ass(ℱ) contains no closed points then

Γ(X, ℱ ⊗_{𝒪_X} ℒ^{⊗ n}) = 0

for all n ≪ 0, as an assertion about the k-vector space of global sections.

theorem exists_forall_le_isZero_globalSectionsOverField_twist (k : Type u) [Field k]
    (f : X ⟶ Spec (.of k)) [IsProper f] (hL : Stacks.Ample.IsAmple X L) (F : X.Modules)
    [F.IsCoherent]
    (hAss : ∀ x : X, IsClosed ({x} : Set X) → x ∉ Stacks.Divisors.associatedPoints F) :
    ∃ n₀ : ℤ, ∀ n : ℤ, n ≤ n₀ → IsZero (globalSectionsOverField k f (twist L F n))

Stacks.EnriquesSeveriZariski.exists_forall_le_isZero_cohomologyOverField_zero_twist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EnriquesSeveriZariski/Basic.lean, line 447. The attribute's comment: “the vanishing stated on degree-zero cohomology”.

[Stacks, Tag 0FD7], in degree-zero cohomology. The same vanishing read through the derived functor computing H⁰, which is the form the twisted-cohomology consumers of 0FD7 ask for.

theorem exists_forall_le_isZero_cohomologyOverField_zero_twist (k : Type u) [Field k]
    (f : X ⟶ Spec (.of k)) [IsProper f] (hL : Stacks.Ample.IsAmple X L) (F : X.Modules)
    [F.IsCoherent]
    (hAss : ∀ x : X, IsClosed ({x} : Set X) → x ∉ Stacks.Divisors.associatedPoints F) :
    ∃ n₀ : ℤ, ∀ n : ℤ, n ≤ n₀ → IsZero (cohomologyOverField k f (twist L F n) 0)

Stacks.EnriquesSeveriZariski.exists_forall_le_isZero_globalSectionsOverField_twistedGradedModuleTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EnriquesSeveriZariski/Basic.lean, line 477. The attribute's comment: “the vanishing at the twisted-graded-module spelling of the twist”.

[Stacks, Tag 0FD7] at the twisted-graded-module spelling of the twist, which is the spelling the graded twisted-cohomology machinery is typed against.

theorem exists_forall_le_isZero_globalSectionsOverField_twistedGradedModuleTwist (k : Type u)
    [Field k] (f : X ⟶ Spec (.of k)) [IsProper f] (hL : Stacks.Ample.IsAmple X L)
    (F : X.Modules) [F.IsCoherent]
    (hAss : ∀ x : X, IsClosed ({x} : Set X) → x ∉ Stacks.Divisors.associatedPoints F) :
    ∃ n₀ : ℤ, ∀ n : ℤ, n ≤ n₀ →
      IsZero (globalSectionsOverField k f
        (Stacks.Cohomology.TwistedGradedModule.twist X L F n))

Stacks.EnriquesSeveriZariski.exists_forall_le_isZero_cohomologyOverField_zero_twistedGradedModuleTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EnriquesSeveriZariski/Basic.lean, line 490. The attribute's comment: “the vanishing at the twisted-graded-module spelling, in degree-zero cohomology”.

[Stacks, Tag 0FD7] at the twisted-graded-module spelling, in degree-zero cohomology.

theorem exists_forall_le_isZero_cohomologyOverField_zero_twistedGradedModuleTwist (k : Type u)
    [Field k] (f : X ⟶ Spec (.of k)) [IsProper f] (hL : Stacks.Ample.IsAmple X L)
    (F : X.Modules) [F.IsCoherent]
    (hAss : ∀ x : X, IsClosed ({x} : Set X) → x ∉ Stacks.Divisors.associatedPoints F) :
    ∃ n₀ : ℤ, ∀ n : ℤ, n ≤ n₀ →
      IsZero (cohomologyOverField k f
        (Stacks.Cohomology.TwistedGradedModule.twist X L F n) 0)
Tag 0FD8, a lemma

Tag 0FD8 in the Stacks Project.

Stacks.EnriquesSeveriZariski.exists_forall_le_isZero_cohomologyOverField_one_twistedGradedModuleTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EnriquesSeveriZariski/H1Vanishing.lean, line 194.

[Stacks, Tag 0FD8]. Let k be a field, let X be a scheme proper over k, let ℒ be an ample invertible 𝒪_X-module and let ℱ be a coherent 𝒪_X-module. If the stalk of ℱ has depth at least two at every closed point of X, then

H¹(X, ℱ ⊗_{𝒪_X} ℒ^{⊗ m}) = 0

for all m ≪ 0.

theorem exists_forall_le_isZero_cohomologyOverField_one_twistedGradedModuleTwist (k : Type u)
    [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] (L : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L] (hL : Stacks.Ample.IsAmple X L) (F : X.Modules)
    [F.IsCoherent]
    (hdepth : ∀ x : X, IsClosed ({x} : Set X) → (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
      (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
      (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x)) :
    ∃ m₀ : ℤ, ∀ m : ℤ, m ≤ m₀ →
      IsZero (AlgebraicGeometry.cohomologyOverField k f
        (Stacks.Cohomology.TwistedGradedModule.twist X L F m) 1)
Tag 0FD9, a lemma

Tag 0FD9 in the Stacks Project.

Stacks.AmpleSectionConnected.connectedSpace_zeroScheme_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleSectionConnected/Connected.lean, line 88.

[Stacks, Tag 0FD9]. Let k be a field, let X be a proper scheme over k, let ℒ be an ample invertible 𝒪_X-module and let s ∈ Γ(X, ℒ). If s is a regular section ([Stacks, Tag 01WY]), if depth(𝒪_{X,x}) ≥ 2 for every closed point x ∈ X, and if X is connected, then the zero scheme Z(s) is connected.

theorem connectedSpace_zeroScheme_of_isAmple (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f]
    (L : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
    [inst : AlgebraicGeometry.SheafOfModules.IsInvertible X.toRingedSpace.presheaf
      (structureSheafRing X.toRingedSpace).property L]
    (hL : AlgebraicGeometry.Scheme.Modules.IsAmple X L) (s : L.sections)
    (hs : Mono (L.unitHomEquiv.symm s))
    (hdepth : ∀ x : X, IsClosed ({x} : Set X) → (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
      (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x))
    [ConnectedSpace X] :
    ConnectedSpace (zeroScheme X L (s.eval (op ⊤))).subscheme
Sources
LeanStacks.EnriquesSeveriZariski.forall_le_eq_zero_sections_twist · Stacks.EnriquesSeveriZariski.exists_forall_le_isZero_globalSectionsOverField_twist · Stacks.EnriquesSeveriZariski.exists_forall_le_isZero_cohomologyOverField_zero_twist · Stacks.EnriquesSeveriZariski.exists_forall_le_isZero_globalSectionsOverField_twistedGradedModuleTwist · Stacks.EnriquesSeveriZariski.exists_forall_le_isZero_cohomologyOverField_zero_twistedGradedModuleTwist · Stacks.EnriquesSeveriZariski.exists_forall_le_isZero_cohomologyOverField_one_twistedGradedModuleTwist · Stacks.AmpleSectionConnected.connectedSpace_zeroScheme_of_isAmple

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.