72.14 Geometrically integral… to 72.18 Numerical intersections

Section72.14 Geometrically integral algebraic spaces #

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

Tag 0DMW, a definition

Tag 0DMW in the Stacks Project.

AlgebraicGeometry.Space.IsGeometricallyIntegral, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyIntegral.lean, line 102.

Stacks 0DMW. An algebraic space over a field k is geometrically integral when its base change to every field extension of k is an integral algebraic space.

def IsGeometricallyIntegral (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u) : Prop

Tag 0DMX, a lemma

Tag 0DMX in the Stacks Project.

AlgebraicGeometry.Space.isGeometricallyIntegral_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyIntegral.lean, line 169.

Stacks 0DMX. A decent algebraic space over a field k is geometrically integral over k exactly when it is geometrically reduced and geometrically irreducible over k.

theorem isGeometricallyIntegral_iff (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (hdecent : IsDecentSpace B (Spec (.of k)) hk X) :
    IsGeometricallyIntegral B k hk X ↔
      IsGeometricallyReduced k B hk X hX ∧ IsGeometricallyIrreducible B k hk X

Tag 0DMY, a lemma

Tag 0DMY in the Stacks Project.

AlgebraicGeometry.Space.finiteDimensional_globalFunctions_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctions.lean, line 306. The attribute's comment: “part (1), with Stacks 08AS — finiteness over the base ring of the cohomology of a coherent module on a proper algebraic space, in every degree — carried as the hypothesis h08AS”.

Stacks 0DMY, part (1). The global regular functions of a proper algebraic space X over a field k form a finite dimensional k-algebra.

Tag 0DMY gets this from Tag 08AS, which is carried here as the hypothesis h08AS: the cohomology over k of every coherent 𝒪_X-module is a finite k-module in every degree. Properness makes X locally Noetherian over k, so the structure sheaf is a coherent 𝒪_X-module by AlgebraicGeometry.Space.isCoherent_structureModuleLarge, and its degree-zero cohomology over k is the ring of global functions by AlgebraicGeometry.Space.cohomologyZeroStructureModuleLinearEquiv.

theorem finiteDimensional_globalFunctions_of_isProper (hf : IsProper B (Spec (.of k)) hS f)
    (h08AS : ∀ M : Modules.{u, u + 1} B (Spec (.of k)) hS X hX,
      IsCoherent B (Spec (.of k)) hS X hX M → ∀ i : ℕ,
        Module.Finite k (cohomologyOverBase.{u, u} k B hS X hX M i)) :
    Module.Finite k (globalFunctions B (Spec (.of k)) hS X)

AlgebraicGeometry.Space.finite_connectedComponents_points_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctions.lean, line 336. The attribute's comment: “part (2): the product is finite, there being one factor for each of the finitely many connected components of the point space”.

Stacks 0DMY, part (2), the number of factors. The point space of a proper algebraic space over a field has finitely many connected components, so that the product decomposition of its global regular functions is a finite product.

Properness makes X quasi-compact and locally Noetherian through Tags 04ZL and 04ZK, and Tag 04ZF then makes |X| a Noetherian topological space; a Noetherian space has finitely many connected components. Tag 08AS is not used.

theorem finite_connectedComponents_points_of_isProper (hf : IsProper B (Spec (.of k)) hS f) :
    Finite (ConnectedComponents (points B (Spec (.of k)) hS X))

AlgebraicGeometry.Space.nonempty_componentwiseArtinianFactorization_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctions.lean, line 358. The attribute's comment: “part (2), with Stacks 08AS — finiteness over the base ring of the cohomology of a coherent module on a proper algebraic space, in every degree — carried as the hypothesis h08AS”.

Stacks 0DMY, part (2). The global regular functions of a proper algebraic space over a field split as the product, over the connected components of its point space, of the rings of functions on the étale charts lying in each component; each factor is an Artinian local ring, and the splitting is simultaneous restriction to the components. The set of components is finite by AlgebraicGeometry.Space.finite_connectedComponents_points_of_isProper, so the product is finite.

This is AlgebraicGeometry.Space.nonempty_componentwiseArtinianFactorization_of_isQuasiCompactSpace with its remaining hypothesis discharged: artinianness of the whole ring of global functions is AlgebraicGeometry.Space.isArtinianRing_globalFunctions_of_isProper, hence part (1) of Tag 0DMY. Quasi-compactness and local Noetherianity of X come from properness through Tags 04ZL and 04ZK, and Tag 04ZF then makes the point space Noetherian, so that the set of connected components is finite.

theorem nonempty_componentwiseArtinianFactorization_of_isProper
    (hf : IsProper B (Spec (.of k)) hS f)
    (h08AS : ∀ M : Modules.{u, u + 1} B (Spec (.of k)) hS X hX,
      IsCoherent B (Spec (.of k)) hS X hX M → ∀ i : ℕ,
        Module.Finite k (cohomologyOverBase.{u, u} k B hS X hX M i)) :
    Nonempty (ComponentwiseArtinianFactorization k B hS X)

AlgebraicGeometry.Space.isField_componentFunctions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctions.lean, line 408. The attribute's comment: “part (3): the factors of a reduced space are fields”.

Stacks 0DMY, part (3). For a reduced algebraic space, each factor of a componentwise factorization of its global regular functions is a field: the factor is an Artinian local ring by the factorization and reduced by AlgebraicGeometry.Space.isReduced_componentFunctions, and a reduced Artinian local ring is a field.

theorem isField_componentFunctions
    (hred : HasEtaleLocalProperty B (Spec (.of k)) hS X
      (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsReduced T))
    (fac : ComponentwiseArtinianFactorization k B hS X)
    (c : ConnectedComponents (points B (Spec (.of k)) hS X)) :
    IsField (componentFunctions B (Spec (.of k)) hS X c)

AlgebraicGeometry.Space.finiteDimensional_componentFunctions_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctions.lean, line 430. The attribute's comment: “part (3): the factors are finite over the base field, with Stacks 08AS — finiteness over the base ring of the cohomology of a coherent module on a proper algebraic space, in every degree — carried as the hypothesis h08AS”.

Stacks 0DMY, part (3). Each factor of a componentwise factorization of the global regular functions of a proper algebraic space over a field is finite dimensional over that field — so that, X being reduced, each factor is a finite field extension of k by AlgebraicGeometry.Space.isField_componentFunctions.

The global functions are finite dimensional by part (1), the factorization makes the product of the factors k-linearly isomorphic to them, and projection onto a factor is a surjective k-linear map. Reducedness is not used.

theorem finiteDimensional_componentFunctions_of_isProper (hf : IsProper B (Spec (.of k)) hS f)
    (h08AS : ∀ M : Modules.{u, u + 1} B (Spec (.of k)) hS X hX,
      IsCoherent B (Spec (.of k)) hS X hX M → ∀ i : ℕ,
        Module.Finite k (cohomologyOverBase.{u, u} k B hS X hX M i))
    (fac : ComponentwiseArtinianFactorization k B hS X)
    (c : ConnectedComponents (points B (Spec (.of k)) hS X)) :
    @Module.Finite k (componentFunctions B (Spec (.of k)) hS X c) _ _
      (@Algebra.toModule k (componentFunctions B (Spec (.of k)) hS X c) _ _
        (fac.factorAlgebra c))

AlgebraicGeometry.Space.nonempty_componentwiseArtinianFactorization_of_isProper_of_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctionsFinite.lean, line 101. The attribute's comment: “part (2): A is the product, over the connected components of |X|, of Artinian local k-algebras, the splitting being restriction to the components”.

Stacks 0DMY, part (2). The global regular functions A of a proper algebraic space over a field k split as the product, over the connected components of the point space |X|, of the rings of functions on the étale charts lying in each component, each factor an Artinian local k-algebra, the splitting being simultaneous restriction to the components; there are finitely many components (AlgebraicGeometry.Space.finite_connectedComponents_points_of_isProper), so the product is finite.

This is AlgebraicGeometry.Space.nonempty_componentwiseArtinianFactorization_of_isQuasiCompactSpace with its remaining hypothesis, artinianness of A, supplied by part (1): AlgebraicGeometry.Space.isArtinianRing_globalFunctions_of_isProper_of_field. Quasi-compactness and local Noetherianity of X come from properness (Tags 04ZL and 04ZK).

theorem nonempty_componentwiseArtinianFactorization_of_isProper_of_field
    (hf : IsProper B (Spec (.of k)) hS f) :
    Nonempty (ComponentwiseArtinianFactorization k B hS X)

AlgebraicGeometry.Space.moduleFinite_componentFunctions_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctionsFinite.lean, line 118. The attribute's comment: “part (3): the factors are finite over the base field”.

Stacks 0DMY, part (3), finiteness of the factors. Each factor of a componentwise factorization of the global regular functions of a proper algebraic space over a field k is finite dimensional over k — so that, X being reduced, each factor is a field (AlgebraicGeometry.Space.isField_componentFunctions) finite over k.

The global functions are finite dimensional by part (1), the factorization makes the product of the factors k-linearly isomorphic to them, and projection onto a factor is a surjective k-linear map.

theorem moduleFinite_componentFunctions_of_isProper (hf : IsProper B (Spec (.of k)) hS f)
    (fac : ComponentwiseArtinianFactorization k B hS X)
    (c : ConnectedComponents (points B (Spec (.of k)) hS X)) :
    @Module.Finite k (componentFunctions B (Spec (.of k)) hS X c) _ _
      (@Algebra.toModule k (componentFunctions B (Spec (.of k)) hS X c) _ _
        (fac.factorAlgebra c))

AlgebraicGeometry.Space.exists_componentwiseArtinianFactorization_isField_finite_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctionsFinite.lean, line 140. The attribute's comment: “part (3)”.

Stacks 0DMY, part (3). Let X be a reduced proper algebraic space over a field k. Then A = H⁰(X, 𝒪_X) is a product of fields, each a finite extension of k: there is a componentwise factorization of A (part (2)), and each of its factors is a field (AlgebraicGeometry.Space.isField_componentFunctions, the factor being reduced by Tag 0BGS and Artinian local) which is finite dimensional over k (AlgebraicGeometry.Space.moduleFinite_componentFunctions_of_isProper).

theorem exists_componentwiseArtinianFactorization_isField_finite_of_isProper
    (hf : IsProper B (Spec (.of k)) hS f)
    (hred : HasEtaleLocalProperty B (Spec (.of k)) hS X
      (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsReduced T)) :
    ∃ fac : ComponentwiseArtinianFactorization k B hS X,
      ∀ c : ConnectedComponents (points B (Spec (.of k)) hS X),
        IsField (componentFunctions B (Spec (.of k)) hS X c) ∧
          @Module.Finite k (componentFunctions B (Spec (.of k)) hS X c) _ _
            (@Algebra.toModule k (componentFunctions B (Spec (.of k)) hS X c) _ _
              (fac.factorAlgebra c))

AlgebraicGeometry.Space.isSeparable_componentFunctions_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctionsGeometric.lean, line 91. The attribute's comment: “part (4): if X is geometrically reduced, each factor k_i is finite separable over k”.

Stacks 0DMY, part (4). For a proper geometrically reduced algebraic space X over a field k, each factor k_i of the global regular functions A = ∏ k_i is a finite separable field extension of k: for every componentwise factorization of A (part (2)) and every connected component c of |X|, the factor at c is a field, finite over k and separable over k.

theorem isSeparable_componentFunctions_of_isProper (hf : IsProper B (Spec (.of k)) hS f)
    (hgr : IsGeometricallyReduced k B hS X hX)
    (fac : ComponentwiseArtinianFactorization k B hS X)
    (c : ConnectedComponents (points B (Spec (.of k)) hS X)) :
    IsField (componentFunctions B (Spec (.of k)) hS X c) ∧
      @Module.Finite k (componentFunctions B (Spec (.of k)) hS X c) _ _
        (@Algebra.toModule k (componentFunctions B (Spec (.of k)) hS X c) _ _
          (fac.factorAlgebra c)) ∧
      @Algebra.IsSeparable k (componentFunctions B (Spec (.of k)) hS X c) _ _
        (fac.factorAlgebra c)

AlgebraicGeometry.Space.irreducibleSpace_primeSpectrum_globalFunctions_tensorProduct_of_isGeometricallyConnected, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctionsGeometric.lean, line 110. The attribute's comment: “part (5): if X is geometrically connected, A is geometrically irreducible over k”.

Stacks 0DMY, part (5). For a proper geometrically connected algebraic space X over a field k, the ring A = H⁰(X, 𝒪_X) of global regular functions is geometrically irreducible over k: the spectrum of A ⊗_k K is irreducible for every field extension K/k.

theorem irreducibleSpace_primeSpectrum_globalFunctions_tensorProduct_of_isGeometricallyConnected
    (hf : IsProper B (Spec (.of k)) hS f) (hconn : IsGeometricallyConnected B k hS X) :
    ∀ (K : Type v) [Field K] [Algebra k K],
      IrreducibleSpace (PrimeSpectrum (globalFunctions B (Spec (.of k)) hS X ⊗[k] K))

AlgebraicGeometry.Space.irreducibleSpace_primeSpectrum_globalFunctions_tensorProduct_of_isGeometricallyIrreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctionsGeometric.lean, line 127. The attribute's comment: “part (6): if X is geometrically irreducible, A is geometrically irreducible over k”.

Stacks 0DMY, part (6). For a proper geometrically irreducible algebraic space X over a field k, the ring A = H⁰(X, 𝒪_X) of global regular functions is geometrically irreducible over k.

As in the source, this is part (5): every base change of X has an irreducible, hence connected, point space.

theorem irreducibleSpace_primeSpectrum_globalFunctions_tensorProduct_of_isGeometricallyIrreducible
    (hf : IsProper B (Spec (.of k)) hS f) (hirr : IsGeometricallyIrreducible B k hS X) :
    ∀ (K : Type v) [Field K] [Algebra k K],
      IrreducibleSpace (PrimeSpectrum (globalFunctions B (Spec (.of k)) hS X ⊗[k] K))

AlgebraicGeometry.Space.bijective_baseToGlobalFunctions_of_isGeometricallyConnected, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctionsGeometric.lean, line 141. The attribute's comment: “part (7): if X is geometrically reduced and (geometrically) connected, A = k”.

Stacks 0DMY, part (7). For a proper geometrically reduced and geometrically connected algebraic space X over a field k, the canonical homomorphism k ⟶ H⁰(X, 𝒪_X) is bijective: A = k.

theorem bijective_baseToGlobalFunctions_of_isGeometricallyConnected
    (hf : IsProper B (Spec (.of k)) hS f) (hgr : IsGeometricallyReduced k B hS X hX)
    (hconn : IsGeometricallyConnected B k hS X) :
    Function.Bijective (baseToGlobalFunctions k B hS X)

AlgebraicGeometry.Space.bijective_baseToGlobalFunctions_of_isGeometricallyIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctionsGeometric.lean, line 156. The attribute's comment: “part (8): if X is geometrically integral, A = k”.

Stacks 0DMY, part (8). For a proper geometrically integral algebraic space X over a field k, the canonical homomorphism k ⟶ H⁰(X, 𝒪_X) is bijective: A = k.

As in the source, this is part (7): a geometrically integral algebraic space is geometrically reduced and geometrically connected.

theorem bijective_baseToGlobalFunctions_of_isGeometricallyIntegral
    (hf : IsProper B (Spec (.of k)) hS f) (hint : IsGeometricallyIntegral B k hS X) :
    Function.Bijective (baseToGlobalFunctions k B hS X)

Declarations registered for the tag:

AlgebraicGeometry.Space.moduleFinite_globalFunctions_of_isProper, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/ProperGlobalFunctionsFinite.lean, line 53 (StacksFrontier): “part (1): A is finite over the base, here any Noetherian ring”.

Tag 0DMZ, a lemma

Tag 0DMZ in the Stacks Project.

AlgebraicGeometry.Space.isTrivial_of_nontrivial_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvertibleModuleTriviality.lean, line 423. The attribute's comment: “granted that H⁰(F, 𝒪_F) is a field, which Tag 0DMY draws from properness”.

Stacks 0DMZ. Let F be an integral algebraic space whose ring H⁰(F, 𝒪_F) of global regular functions is a field, and let L be an invertible 𝒪_F-module. If H⁰(F, L) and H⁰(F, L^{⊗ -1}) are both nonzero then L ≅ 𝒪_F.

The source states this for a proper integral algebraic space over a field k, and uses properness only through Tag 0DMY, that H⁰(F, 𝒪_F) is then a field. That result is not available in this library, so it is carried here as the hypothesis hfield; the base is correspondingly an arbitrary scheme rather than the spectrum of a field.

theorem isTrivial_of_nontrivial_sections (hint : IsIntegralSpace B S hS F)
    (hfield : IsField (globalFunctions B S hS F))
    (L : SheafOfModules.{u} (modulesRingSheaf B S hS F hF))
    [IsInvertible (structureSheaf B S hS F hF).obj (structureRingPresheaf_isSheaf B S hS F hF) L]
    (hL : Nontrivial L.sections)
    (hLinv : Nontrivial (tensorPower (structureSheaf B S hS F hF).obj
      (structureRingPresheaf_isSheaf B S hS F hF) L (-1)).sections) :
    IsTrivial (structureSheaf B S hS F hF).obj (structureRingPresheaf_isSheaf B S hS F hF) L

AlgebraicGeometry.Space.isTrivial_of_nontrivial_sections_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperIntegralInvertibleTriviality.lean, line 140.

Stacks 0DMZ. Let k be a field, let X be a proper integral algebraic space over k and let L be an invertible 𝒪_X-module. If H⁰(X, L) and H⁰(X, L^{⊗ -1}) are both nonzero then L ≅ 𝒪_X.

This is AlgebraicGeometry.Space.isTrivial_of_nontrivial_sections with its hypothesis that H⁰(X, 𝒪_X) be a field discharged from properness and integrality by AlgebraicGeometry.Space.isField_globalFunctions_of_isProper_of_isIntegralSpace.

theorem isTrivial_of_nontrivial_sections_of_isProper
    (hf : IsProper B (Spec (.of k)) hS f)
    (hint : IsIntegralSpace B (Spec (.of k)) hS X)
    (L : SheafOfModules.{u} (modulesRingSheaf B (Spec (.of k)) hS X hX))
    [IsInvertible (structureSheaf B (Spec (.of k)) hS X hX).obj
      (structureRingPresheaf_isSheaf B (Spec (.of k)) hS X hX) L]
    (hL : Nontrivial L.sections)
    (hLinv : Nontrivial (tensorPower (structureSheaf B (Spec (.of k)) hS X hX).obj
      (structureRingPresheaf_isSheaf B (Spec (.of k)) hS X hX) L (-1)).sections) :
    IsTrivial (structureSheaf B (Spec (.of k)) hS X hX).obj
      (structureRingPresheaf_isSheaf B (Spec (.of k)) hS X hX) L

Sources

Section72.15 Dimension #

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

Tag 0EDB, a lemma

Tag 0EDB in the Stacks Project.

AlgebraicGeometry.Space.dimension_le_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionIntegralMorphism.lean, line 110. The attribute's comment: “dimension inequality”.

An integral morphism of algebraic spaces over S does not increase the dimension.

theorem dimension_le_of_isIntegralHom (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsIntegralHom B S hS f) :
    dimension B S hS X hX ≤ dimension B S hS Y hY

AlgebraicGeometry.Space.dimension_eq_of_isIntegralHom_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionIntegralMorphism.lean, line 120. The attribute's comment: “surjective case”.

A surjective integral morphism of algebraic spaces over S preserves the dimension.

theorem dimension_eq_of_isIntegralHom_of_isSurjective (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsIntegralHom B S hS f)
    (hsurj : IsSurjective B S hS f) :
    dimension B S hS X hX = dimension B S hS Y hY

Tag 0EDC, a lemma

Tag 0EDC in the Stacks Project.

AlgebraicGeometry.Space.dimension_le_dimension_add_transcendenceDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralDominantMorphism.lean, line 166. The attribute's comment: “the dimension inequality”.

Stacks 0EDC, the dimension inequality. Let f : X ⟶ Y be a dominant morphism locally of finite type of integral algebraic spaces over S with Y locally Noetherian, and let x and y be generic points of |X| and |Y|. If the transcendence degree of f at x is r, then dim X ≤ dim Y + r.

theorem dimension_le_dimension_add_transcendenceDegree
    (s : IntegralDominantMorphismSituation B S hS) (r : ℕ∞)
    (hr : HasTranscendenceDegreeAt B S hS s.hom s.sourcePoint r) :
    dimension B S hS s.source s.isAlgebraicSpace_source ≤
      dimension B S hS s.target s.isAlgebraicSpace_target + (r : WithBot ℕ∞)

AlgebraicGeometry.Space.dimension_eq_dimension_add_transcendenceDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralDominantMorphism.lean, line 417. The attribute's comment: “equality for a proper morphism”.

Stacks 0EDC, equality for a proper morphism. Let f : X ⟶ Y be a dominant morphism locally of finite type of integral algebraic spaces over S with Y locally Noetherian, and let x and y be generic points of |X| and |Y|. If f is proper and the transcendence degree of f at x is r, then dim X = dim Y + r.

The inequality ≤ is AlgebraicGeometry.Space.dimension_le_dimension_add_transcendenceDegree. For the reverse inequality both dimensions are read on one commuting pair of surjective étale scheme charts U → X and V → Y (Stacks 0A4H and Stacks 02X1), so that each becomes a topological Krull dimension and a bound on it is a chain of specializations. A chain of length d in V gives one of length at least d in |Y| ending at y, since two points of an étale chart with the same image, one a specialization of the other, are equal (Stacks 03K5); properness makes |f| closed, so that chain lifts to |X| from any point above y (Stacks 0066). Below such a point there are r further nontrivial specializations: the fibre of U → V through the chart point above x has dimension at least the transcendence degree there by the dimension formula of Stacks 02FX, and the resulting chain lies over y. The concatenation is a chain of length d + r in |X|, and it lifts to the chart U by Stacks 03IL.

theorem dimension_eq_dimension_add_transcendenceDegree
    (s : IntegralDominantMorphismSituation B S hS) (hproper : IsProper B S hS s.hom) (r : ℕ∞)
    (hr : HasTranscendenceDegreeAt B S hS s.hom s.sourcePoint r) :
    dimension B S hS s.source s.isAlgebraicSpace_source =
      dimension B S hS s.target s.isAlgebraicSpace_target + (r : WithBot ℕ∞)

Sources

LeanAlgebraicGeometry.Space.dimension_le_of_isIntegralHom · AlgebraicGeometry.Space.dimension_eq_of_isIntegralHom_of_isSurjective · AlgebraicGeometry.Space.dimension_le_dimension_add_transcendenceDegree · AlgebraicGeometry.Space.dimension_eq_dimension_add_transcendenceDegree

Section72.16 Spaces smooth over fields #

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

Tag 06M1, a lemma

Tag 06M1 in the Stacks Project.

AlgebraicGeometry.Space.isRegular_of_isSmooth_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothOverField.lean, line 98.

Stacks 06M1. An algebraic space over S which is smooth over the spectrum of a field is regular.

theorem isRegular_of_isSmooth_over_field (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (k : Type u) [Field k] (T : BigFppfOver B S hS)
    (hT : (BigFppfOver.toScheme B S hS).obj T = Spec (.of k))
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (f : F ⟶ yoneda.obj T) (hf : IsSmooth B S hS f) :
    HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} ↦ IsRegular X)

Tag 07W4, a lemma

Tag 07W4 in the Stacks Project.

AlgebraicGeometry.Space.dense_setOf_class_finiteSeparable_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothOverField.lean, line 132.

Stacks 07W4. Let k be a field and let X be an algebraic space over Spec k which is smooth over Spec k. The points of |X| represented by a morphism Spec k' ⟶ X over Spec k with k' a finite separable extension of k are dense in |X|.

theorem dense_setOf_class_finiteSeparable_of_isSmooth
    {X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (f : X ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hk))))
    (hf : IsSmooth B (Spec (.of k)) hk f) :
    Dense {x : points B (Spec (.of k)) hk X |
      ∃ p : FieldValuedPoint B (Spec (.of k)) hk X,
        p.class B (Spec (.of k)) hk X = x ∧
          ∃ alg : Algebra k p.carrier,
            letI := alg
            Module.Finite k p.carrier ∧ Algebra.IsSeparable k p.carrier ∧
              p.toBase = Spec.map (CommRingCat.ofHom (algebraMap k p.carrier))}

Sources

LeanAlgebraicGeometry.Space.isRegular_of_isSmooth_over_field · AlgebraicGeometry.Space.dense_setOf_class_finiteSeparable_of_isSmooth

Section72.17 Euler characteristics #

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

Tag 0DN1, a definition

Tag 0DN1 in the Stacks Project.

AlgebraicGeometry.Space.eulerCharacteristic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EulerCharacteristic.lean, line 293.

Stacks 0DN1. The Euler characteristic of a coherent module F on a proper algebraic space X over a field k: the alternating sum ∑ᵢ (-1)ⁱ dim_k Hⁱ(X, F) of the dimensions over k of the cohomology modules of F on the small étale site of X.

def eulerCharacteristic (f : X ⟶ yoneda.obj (baseObject k B hk))
    (_hf : IsProper B (Spec (.of k)) hk f)
    (F : Modules.{u, max (u + 1) w} B (Spec (.of k)) hk X hX)
    [IsCoherent B (Spec (.of k)) hk X hX F] : ℤ

Tag 0DN2, a lemma

Tag 0DN2 in the Stacks Project.

AlgebraicGeometry.Space.eulerCharacteristic_add_of_shortExact_of_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EulerCharacteristic.lean, line 425.

Stacks 0DN2. Let k be a field, X a proper algebraic space over k and 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0 a short exact sequence of coherent 𝒪_X-modules. Then χ(X, F₂) = χ(X, F₁) + χ(X, F₃).

X is quasi-compact and quasi-separated, being proper over Spec k, so by Stacks 072C there is N beyond which the cohomology of every coherent module vanishes; below N the cohomology of F₁ and F₃ is finite-dimensional by Stacks 08AS; and the long exact sequence with rank-nullity is AlgebraicGeometry.Space.finsum_alternating_finrank_cohomologyOverBase_add_of_shortExact_of_outer.

theorem eulerCharacteristic_add_of_shortExact_of_outer
    (f : X ⟶ yoneda.obj (baseObject k B hk)) (hf : IsProper B (Spec (.of k)) hk f)
    {S : ShortComplex (Modules.{u, max (u + 1) w} B (Spec (.of k)) hk X hX)} (hS : S.ShortExact)
    [IsCoherent B (Spec (.of k)) hk X hX S.X₁] [IsCoherent B (Spec (.of k)) hk X hX S.X₂]
    [IsCoherent B (Spec (.of k)) hk X hX S.X₃] :
    eulerCharacteristic.{u, w} k B hk X hX f hf S.X₂ =
      eulerCharacteristic.{u, w} k B hk X hX f hf S.X₁ +
        eulerCharacteristic.{u, w} k B hk X hX f hf S.X₃

AlgebraicGeometry.Space.eulerCharacteristic_add_of_shortExact_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EulerCharacteristicAdditivity.lean, line 65.

Stacks 0DN2. Let k be a field, X a proper algebraic space over k and 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0 a short exact sequence of coherent 𝒪_X-modules. Then χ(X, F₂) = χ(X, F₁) + χ(X, F₃).

This is AlgebraicGeometry.Space.eulerCharacteristic_add_of_shortExact_of_outer: the long exact sequence of cohomology and rank-nullity, with the finiteness of Stacks 08AS and the uniform vanishing of Stacks 072C, for X quasi-compact and quasi-separated, being proper over Spec k.

theorem eulerCharacteristic_add_of_shortExact_of_isProper
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (f : X ⟶ yoneda.obj (baseObject k B hk)) (hf : IsProper B (Spec (.of k)) hk f)
    {S : ShortComplex (Modules.{u, max (u + 1) w} B (Spec (.of k)) hk X hX)} (hS : S.ShortExact)
    [IsCoherent B (Spec (.of k)) hk X hX S.X₁] [IsCoherent B (Spec (.of k)) hk X hX S.X₂]
    [IsCoherent B (Spec (.of k)) hk X hX S.X₃] :
    eulerCharacteristic.{u, w} k B hk X hX f hf S.X₂ =
      eulerCharacteristic.{u, w} k B hk X hX f hf S.X₁ +
        eulerCharacteristic.{u, w} k B hk X hX f hf S.X₃

Tag 0EDD, a lemma

Tag 0EDD in the Stacks Project.

AlgebraicGeometry.Space.eulerCharacteristic_eq_finsum_eulerCharacteristic_higherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EulerCharacteristicHigherDirectImage.lean, line 140.

Let k be a field, f : Y ⟶ X a morphism of algebraic spaces proper over k and 𝓖 a coherent 𝒪_Y-module. Then only finitely many of the higher direct images Rⁱf_*𝓖 are nonzero, each is coherent, and χ(Y, 𝓖) = ∑ᵢ (-1)ⁱ χ(X, Rⁱf_*𝓖).

Here 𝓖 has sections in the universe of the structure sheaf, where Rⁱf_* exists, and both Euler characteristics are taken of universe lifts.

theorem eulerCharacteristic_eq_finsum_eulerCharacteristic_higherDirectImage (f : Y ⟶ X)
    (πX : X.1 ⟶ yoneda.obj (baseObject k B hk)) (hπX : IsProper B (Spec (.of k)) hk πX)
    (πY : Y.1 ⟶ yoneda.obj (baseObject k B hk)) (hπY : IsProper B (Spec (.of k)) hk πY)
    (G : Modules.{u, u} B (Spec (.of k)) hk Y.1 Y.2)
    [hG : IsCoherent B (Spec (.of k)) hk Y.1 Y.2 G] :
    have := hasInjectiveResolutions_modules B (Spec (.of k)) hk Y.1 Y.2
    have := isCoherent_higherDirectImage_of_isProper_toBase k B hk f πX hπX πY hπY G
    {i : ℕ | ¬ IsZero (((modulePushforward B (Spec (.of k)) hk f).rightDerived i).obj G)}.Finite ∧
      eulerCharacteristic.{u, w} k B hk Y.1 Y.2 πY hπY
          (SheafOfModules.uliftForPresentation.{u + 1, u, u, u, max (u + 1) w} G) =
        ∑ᶠ i : ℕ, (-1 : ℤ) ^ i * eulerCharacteristic.{u, w} k B hk X.1 X.2 πX hπX
          (SheafOfModules.uliftForPresentation.{u + 1, u, u, u, max (u + 1) w}
            (((modulePushforward B (Spec (.of k)) hk f).rightDerived i).obj G))

AlgebraicGeometry.Space.exists_eulerCharacteristic_eq_finsum_eulerCharacteristic_higherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EulerCharacteristicHigherDirectImage.lean, line 250. The attribute's comment: “for a coherent module in the universe of the Euler characteristic, the higher direct images being taken of its descent to the universe of the structure sheaf”.

For a coherent module 𝓖' with sections in the universe of the Euler characteristic: 𝓖' is the universe lift of a coherent module 𝓖 with sections in the universe of the structure sheaf, only finitely many Rⁱf_*𝓖 are nonzero, and χ(Y, 𝓖') = ∑ᵢ (-1)ⁱ χ(X, Rⁱf_*𝓖).

theorem exists_eulerCharacteristic_eq_finsum_eulerCharacteristic_higherDirectImage (f : Y ⟶ X)
    (πX : X.1 ⟶ yoneda.obj (baseObject k B hk)) (hπX : IsProper B (Spec (.of k)) hk πX)
    (πY : Y.1 ⟶ yoneda.obj (baseObject k B hk)) (hπY : IsProper B (Spec (.of k)) hk πY)
    (G' : Modules.{u, max (u + 1) w} B (Spec (.of k)) hk Y.1 Y.2)
    [IsCoherent B (Spec (.of k)) hk Y.1 Y.2 G'] :
    ∃ (G : Modules.{u, u} B (Spec (.of k)) hk Y.1 Y.2)
      (_ : IsCoherent B (Spec (.of k)) hk Y.1 Y.2 G)
      (_ : SheafOfModules.uliftForPresentation.{u + 1, u, u, u, max (u + 1) w} G ≅ G'),
      have := hasInjectiveResolutions_modules B (Spec (.of k)) hk Y.1 Y.2
      have := isCoherent_higherDirectImage_of_isProper_toBase k B hk f πX hπX πY hπY G
      {i : ℕ | ¬ IsZero (((modulePushforward B (Spec (.of k)) hk f).rightDerived i).obj G)}.Finite ∧
        eulerCharacteristic.{u, w} k B hk Y.1 Y.2 πY hπY G' =
          ∑ᶠ i : ℕ, (-1 : ℤ) ^ i * eulerCharacteristic.{u, w} k B hk X.1 X.2 πX hπX
            (SheafOfModules.uliftForPresentation.{u + 1, u, u, u, max (u + 1) w}
              (((modulePushforward B (Spec (.of k)) hk f).rightDerived i).obj G))

Sources

LeanAlgebraicGeometry.Space.eulerCharacteristic · AlgebraicGeometry.Space.eulerCharacteristic_add_of_shortExact_of_outer · AlgebraicGeometry.Space.eulerCharacteristic_add_of_shortExact_of_isProper · AlgebraicGeometry.Space.eulerCharacteristic_eq_finsum_eulerCharacteristic_higherDirectImage · AlgebraicGeometry.Space.exists_eulerCharacteristic_eq_finsum_eulerCharacteristic_higherDirectImage

Section72.18 Numerical intersections #

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

Tag 0DN4, a lemma

Tag 0DN4 in the Stacks Project.

AlgebraicGeometry.Space.isTwistedEulerNumericalPolynomial_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedEulerNumericalPolynomialProper.lean, line 76. The attribute's comment: “for every closed subspace Z with F = i_*G, G coherent; the scheme-theoretic support is the smallest such Z (Stacks 07U0), and the bound at it is hasTwistedEulerPolynomialOfDegreeLE_coherentSchemeTheoreticSupport”. References: SGA 6 X (2.3.1), “more general”.

Stacks 0DN4. Let k be a field, X a proper algebraic space over k, F a coherent 𝒪_X-module and L₁, …, L_r invertible 𝒪_X-modules. For every closed subspace i : Z ⟶ X with F ≅ i_*𝒢 for a coherent 𝒪_Z-module 𝒢, the twisted Euler characteristics χ(X, F ⊗ L₁^{⊗ n₁} ⊗ ⋯ ⊗ L_r^{⊗ n_r}) are the values at the integral tuples of a rational polynomial which is zero or of total degree at most dim Z. Taking Z to be the scheme-theoretic support of F is AlgebraicGeometry.Space.hasTwistedEulerPolynomialOfDegreeLE_coherentSchemeTheoreticSupport.

theorem isTwistedEulerNumericalPolynomial_of_isCoherent
    (F : Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    (hF : IsCoherent B (Spec (.of k)) hk X.1 X.2 F)
    (L : Fin r → Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O)).property (L j)] :
    @IsTwistedEulerNumericalPolynomial.{u, w} k _ B hk X r f hf F L _
      (isCoherent_twistedModuleUlift_of_isProper.{u, w} k B hk X f hf L F hF)

AlgebraicGeometry.Space.hasTwistedEulerPolynomialOfDegreeLE_coherentSchemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedEulerNumericalPolynomialProper.lean, line 101.

Stacks 0DN4. Let k be a field, X a proper algebraic space over k, F a coherent 𝒪_X-module and L₁, …, L_r invertible 𝒪_X-modules. The map (n₁, …, n_r) ↦ χ(X, F ⊗ L₁^{⊗ n₁} ⊗ ⋯ ⊗ L_r^{⊗ n_r}) is the restriction to the integral tuples of a rational polynomial which is zero or of total degree at most the dimension of the scheme-theoretic support of F. It is numerical, its values being integers (AlgebraicGeometry.Space.exists_intCast_eq_eval_of_representsTwistedEuler), and unique (AlgebraicGeometry.Space.eq_of_representsTwistedEuler); when the support is empty it is 0.

F is the direct image of a coherent module on its scheme-theoretic support (Stacks 07U0 and 07UG), and AlgebraicGeometry.Space.isTwistedEulerNumericalPolynomial_of_isCoherent applies.

theorem hasTwistedEulerPolynomialOfDegreeLE_coherentSchemeTheoreticSupport
    (F : Modules.{u, u} B (Spec (.of k)) hk X.1 X.2) [hF : IsCoherent B (Spec (.of k)) hk X.1 X.2 F]
    (L : Fin r → Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O)).property (L j)] :
    @HasTwistedEulerPolynomialOfDegreeLE.{u, w} k _ B hk X r f hf F L _
      (isCoherent_twistedModuleUlift_of_isProper.{u, w} k B hk X f hf L F hF)
      (dimension B (Spec (.of k)) hk
        (closedSubspaceToSpace B (Spec (.of k)) hk X
          (coherentSchemeTheoreticSupport B (Spec (.of k)) hk X F)).1
        (closedSubspaceToSpace B (Spec (.of k)) hk X
          (coherentSchemeTheoreticSupport B (Spec (.of k)) hk X F)).2)

AlgebraicGeometry.Space.hasTwistedEulerPolynomialOfDegreeLE_fin_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedEulerPolynomial.lean, line 374. The attribute's comment: “the case r = 0 of no invertible modules: the constant function χ(X, F) is represented by a constant polynomial, of total degree 0, which is at most the dimension of the closed subspace carrying F whenever that subspace has a point. The empty-support case, and every case with invertible modules present, is not proved”.

Stacks 0DN4 in the case r = 0. With no invertible modules to twist by, the function on ℤ ^ 0 is the constant χ(X, F), so it is represented by a constant polynomial, whose total degree is 0; and 0 is at most the dimension of the closed subspace Z carrying F as soon as Z has a point, by AlgebraicGeometry.Space.zero_le_dimension. Taking Z to be the scheme theoretic support of F gives the source's statement for r = 0.

The point of Z is the one hypothesis beyond the source's, and it is the empty-support case that it excludes: a space with no points has dimension ⊥, the bound then forces the representing polynomial to be 0, hence χ(X, F) = 0, and that needs an empty scheme theoretic support to force F ≅ 0, which this library does not provide. The closed immersion i, the module G and the isomorphism F ≅ i_*G are the source's hypotheses, carried so that the statement is the one of the tag; the constant polynomial does not use them.

theorem hasTwistedEulerPolynomialOfDegreeLE_fin_zero
    (Z : AlgebraicSpaces B (Spec (.of k)) hk) (i : Z ⟶ X)
    (_hi : IsClosedImmersion B (Spec (.of k)) hk i.hom)
    (G : Modules.{u, u} B (Spec (.of k)) hk Z.1 Z.2)
    (_hG : IsCoherent B (Spec (.of k)) hk Z.1 Z.2 G)
    (_hF : F ≅ (modulePushforward B (Spec (.of k)) hk i).obj G)
    (z : points B (Spec (.of k)) hk Z.1) :
    HasTwistedEulerPolynomialOfDegreeLE.{u, w} k B hk X f hf F L
      (dimension B (Spec (.of k)) hk Z.1 Z.2)

Tag 0EDE, a lemma

Tag 0EDE in the Stacks Project.

AlgebraicGeometry.Space.exists_twistedEuler_sub_finsum_mul_twistedEuler_topDimensionalComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedEulerTopDimensionalComponents.lean, line 210.

Stacks 0EDE. Let X be proper over a field k, F a coherent 𝒪_X-module and L₁, …, L_r invertible 𝒪_X-modules. Let Z_C be the reduced closed subspace on an irreducible component C of Supp(F) of dimension d = dim Supp(F), x̄_C a geometric generic point of C and m_C = length_{𝒪_{X, x̄_C}}(F_{x̄_C}). Then χ(X, F ⊗ L₁^{⊗ n₁} ⊗ ⋯ ⊗ L_r^{⊗ n_r}) - ∑_C m_C χ(Z_C, (L₁^{⊗ n₁} ⊗ ⋯ ⊗ L_r^{⊗ n_r})|_{Z_C}) is given by a rational polynomial in n₁, …, n_r which is zero or of total degree < d.

theorem exists_twistedEuler_sub_finsum_mul_twistedEuler_topDimensionalComponent
    (F : Modules.{u, u} B (Spec (.of k)) hk X.1 X.2) (hF : IsCoherent B (Spec (.of k)) hk X.1 X.2 F)
    (x : irreducibleComponents (moduleSupportSet B (Spec (.of k)) hk X F) → GeometricPoint B (Spec
        (.of k)) hk X.1)
    (hx : ∀ C, IsGenericPoint (x C).image (Subtype.val '' (C : Set (moduleSupportSet B (Spec
        (.of k)) hk X F)))) :
    have hT : IsClosed (moduleSupportSet B (Spec (.of k)) hk X F) := isClosed_moduleSupportSet B
        (Spec (.of k)) hk X F hF
    have hW : ∀ C : irreducibleComponents (moduleSupportSet B (Spec (.of k)) hk X F),
        IsClosedSubspace B (Spec (.of k)) hk (reducedClosedSubspace B (Spec (.of k)) hk X.1 X.2 _
          (closedSetComponentPoints B (Spec (.of k)) hk (moduleSupportSet B (Spec
              (.of k)) hk X F) hT C).isClosed) := fun C =>
      isClosedSubspace_reducedClosedSubspace B (Spec (.of k)) hk X.1 X.2 _
        (closedSetComponentPoints B (Spec (.of k)) hk (moduleSupportSet B (Spec
            (.of k)) hk X F) hT C).isClosed
    have hfZ : ∀ C : irreducibleComponents (moduleSupportSet B (Spec (.of k)) hk X F),
        IsProper B (Spec (.of k)) hk ((closedSubfunctorι B (Spec (.of k)) hk (hW C)).hom ≫ f) :=
      fun C => isProper_comp B (Spec (.of k)) hk (hW C).1 X.2
        (isAlgebraicSpace_yoneda B (Spec (.of k)) hk (baseObject k B hk)) _ f
        (isProper_of_isClosedImmersion B (Spec (.of k)) hk (hW C).1 X.2 _ (hW C).2) hf
    ∃ P : MvPolynomial (Fin r) ℚ,
      (P = 0 ∨ (P.totalDegree : WithBot ℕ∞) < topologicalKrullDim (moduleSupportSet B (Spec
          (.of k)) hk X F)) ∧
      ∀ n : Fin r → ℤ, MvPolynomial.eval (fun j => (n j : ℚ)) P =
        (@eulerCharacteristic.{u, w} k _ B hk X.1 X.2 f hf
          (twistedModuleUlift.{u, w} B (Spec (.of k)) hk X.1 X.2 F L n)
          (isCoherent_twistedModuleUlift_of_isProper.{u, w} k B hk X f hf L F hF n) : ℚ) -
        ∑ᶠ C ∈ {C : irreducibleComponents (moduleSupportSet B (Spec (.of k)) hk X F) |
            topologicalKrullDim (Subtype.val '' (C : Set (moduleSupportSet B (Spec
                (.of k)) hk X F))) = topologicalKrullDim (moduleSupportSet B (Spec
                    (.of k)) hk X F)},
          haveI := fun j => stacksIsInvertible_modulePullback_obj B (Spec (.of k)) hk
            (closedSubfunctorι B (Spec (.of k)) hk (hW C)) (L j)
          ((geometricLength B (Spec (.of k)) hk X (x C) F).toNat : ℚ) *
            (@eulerCharacteristic.{u, w} k _ B hk (closedSubfunctorSpace B (Spec (.of k)) hk
                (hW C)).1
              (closedSubfunctorSpace B (Spec (.of k)) hk (hW C)).2
              ((closedSubfunctorι B (Spec (.of k)) hk (hW C)).hom ≫ f) (hfZ C)
              (twistedModuleUlift.{u, w} B (Spec (.of k)) hk
                (closedSubfunctorSpace B (Spec (.of k)) hk (hW C)).1
                (closedSubfunctorSpace B (Spec (.of k)) hk (hW C)).2
                (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf
                  (smallEtaleRingedSite B (Spec (.of k)) hk
                    (closedSubfunctorSpace B (Spec (.of k)) hk (hW C)).1
                    (closedSubfunctorSpace B (Spec (.of k)) hk (hW C)).2).O))
                (fun j => (modulePullback B (Spec (.of k)) hk
                  (closedSubfunctorι B (Spec (.of k)) hk (hW C))).obj (L j)) n)
              (isCoherent_twistedModuleUlift_of_isProper.{u, w} k B hk
                (closedSubfunctorSpace B (Spec (.of k)) hk (hW C))
                ((closedSubfunctorι B (Spec (.of k)) hk (hW C)).hom ≫ f) (hfZ C) _ _
                (isCoherent_unit_of_isClosedImmersion k B hk X
                  (closedSubfunctorSpace B (Spec (.of k)) hk (hW C)) f hf
                  (closedSubfunctorι B (Spec (.of k)) hk (hW C)) (hW C).2) n) : ℚ)

Tag 0EDF, a definition

Tag 0EDF in the Stacks Project.

AlgebraicGeometry.Space.intersectionNumber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NumericalIntersection.lean, line 776. References: SGA 6 X (4.4), “defn, algebraic spaces”.

Stacks 0EDF. The intersection number (L₁ ⋯ L_d · Z) of d invertible 𝒪_X-modules against a closed subspace i : Z ⟶ X of dimension d of a proper algebraic space X over a field k: the coefficient of n₁ ⋯ n_d in the numerical polynomial χ(X, i_*𝒪_Z ⊗ L₁^{⊗ n₁} ⊗ ⋯ ⊗ L_d^{⊗ n_d}), computed as the d-fold mixed finite difference

∑_{T ⊆ {1, …, d}} (-1)^{d - |T|} χ(X, i_*𝒪_Z ⊗ ⨂_{j ∈ T} L_j)

of that function. This is an honest integer: only finitely many values of the function are used, so neither polynomiality nor a choice of representing polynomial enters.

def intersectionNumber (d : ℕ) (f : X.1 ⟶ yoneda.obj (baseObject k B hk))
    (hf : IsProper B (Spec (.of k)) hk f) (i : Z ⟶ X)
    (hi : IsClosedImmersion B (Spec (.of k)) hk i.hom)
    (_hd : dimension B (Spec (.of k)) hk Z.1 Z.2 = d)
    (L : Fin d → Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L j)] :
    ℤ

AlgebraicGeometry.Space.intersectionNumber_eq_coeff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NumericalIntersection.lean, line 820. The attribute's comment: “the coefficient of n_1 ⋯ n_d”. References: SGA 6 X (4.4), “defn, algebraic spaces”.

Stacks 0EDF, the coefficient of n₁ ⋯ n_d. If a rational polynomial P in d variables of total degree at most d takes the Euler characteristics χ(X, i_*𝒪_Z ⊗ L₁^{⊗ n₁} ⊗ ⋯ ⊗ L_d^{⊗ n_d}) as its values at the integral tuples, then the intersection number (L₁ ⋯ L_d · Z) is the coefficient of n₁ ⋯ n_d in P.

This is the source's own description of the intersection number. The existence of such a P, which is Stacks 0DN4, 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.

theorem intersectionNumber_eq_coeff (d : ℕ) (f : X.1 ⟶ yoneda.obj (baseObject k B hk))
    (hf : IsProper B (Spec (.of k)) hk f) (i : Z ⟶ X)
    (hi : IsClosedImmersion B (Spec (.of k)) hk i.hom)
    (hd : dimension B (Spec (.of k)) hk Z.1 Z.2 = d)
    (L : Fin d → Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L j)]
    (P : MvPolynomial (Fin d) ℚ)
    (hP : ∀ n : Fin d → ℤ, MvPolynomial.eval (fun j => (n j : ℚ)) P =
      ((@eulerCharacteristic.{u, w} k _ B hk X.1 X.2 f hf
        (twistedModuleUlift.{u, w} B (Spec (.of k)) hk X.1 X.2
          (structureSheafPushforward B (Spec (.of k)) hk i) L n)
          (isCoherent_twistedModuleUlift_structureSheafPushforward.{u, w}
            k B hk X Z f hf i hi L n) : ℤ) : ℚ))
    (hdeg : P.totalDegree ≤ d) :
    ((intersectionNumber.{u, w} k B hk X Z d f hf i hi hd L : ℤ) : ℚ) =
      P.coeff (Finsupp.equivFunOnFinite.symm fun _ => 1)

AlgebraicGeometry.Space.selfIntersectionNumber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NumericalIntersection.lean, line 891. The attribute's comment: “the self-intersection notation (L^d · Z)”.

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

def selfIntersectionNumber (d : ℕ) (f : X.1 ⟶ yoneda.obj (baseObject k B hk))
    (hf : IsProper B (Spec (.of k)) hk f) (i : Z ⟶ X)
    (hi : IsClosedImmersion B (Spec (.of k)) hk i.hom)
    (hd : dimension B (Spec (.of k)) hk Z.1 Z.2 = d)
    (L : Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property L] :
    ℤ

Tag 0EDG, a lemma

Tag 0EDG in the Stacks Project.

AlgebraicGeometry.Space.exists_eval_eq_eulerCharacteristic_and_exists_intCast_eq_coeff_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntersectionNumberAdditivity.lean, line 128. References: SGA 6 X (2.3.1), “special case”.

Stacks 0EDG. In the situation of Definition 0EDF — X a proper algebraic space over a field k, i : Z ⟶ X a closed subspace of dimension d and L₁, …, L_d invertible 𝒪_X-modules — the intersection number (L₁ ⋯ L_d · Z) is an integer: the function n ↦ χ(X, i_*𝒪_Z ⊗ L₁^{⊗ n₁} ⊗ ⋯ ⊗ L_d^{⊗ n_d}) is the restriction to the integral tuples of a rational polynomial of total degree at most d, and the coefficient of n₁ ⋯ n_d in any rational polynomial with these values is the cast of an integer.

The first conjunct is Stacks 0DN4, AlgebraicGeometry.Space.exists_representsTwistedEuler_structureSheafPushforward, and it is what makes the second one say something about the numerical polynomial of the source: a rational polynomial is determined by its values at the integral tuples (MvPolynomial.eq_of_eval_intCast_eq), so every polynomial with these values is that one, and AlgebraicGeometry.Space.exists_intCast_eq_coeff_one applies to it, the integer being AlgebraicGeometry.Space.intersectionNumber.

theorem exists_eval_eq_eulerCharacteristic_and_exists_intCast_eq_coeff_one (d : ℕ)
    (f : X.1 ⟶ yoneda.obj (baseObject k B hk)) (hf : IsProper B (Spec (.of k)) hk f)
    (i : Z ⟶ X) (hi : IsClosedImmersion B (Spec (.of k)) hk i.hom)
    (hd : dimension B (Spec (.of k)) hk Z.1 Z.2 = d)
    (L : Fin d → Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L j)] :
    (∃ P : MvPolynomial (Fin d) ℚ, (∀ n : Fin d → ℤ, MvPolynomial.eval (fun j => (n j : ℚ)) P =
      ((@eulerCharacteristic.{u, w} k _ B hk X.1 X.2 f hf
        (twistedModuleUlift.{u, w} B (Spec (.of k)) hk X.1 X.2
          (structureSheafPushforward B (Spec (.of k)) hk i) L n)
          (isCoherent_twistedModuleUlift_structureSheafPushforward.{u, w}
            k B hk X Z f hf i hi L n) : ℤ) : ℚ)) ∧ P.totalDegree ≤ d) ∧
    ∀ P : MvPolynomial (Fin d) ℚ, (∀ n : Fin d → ℤ, MvPolynomial.eval (fun j => (n j : ℚ)) P =
      ((@eulerCharacteristic.{u, w} k _ B hk X.1 X.2 f hf
        (twistedModuleUlift.{u, w} B (Spec (.of k)) hk X.1 X.2
          (structureSheafPushforward B (Spec (.of k)) hk i) L n)
          (isCoherent_twistedModuleUlift_structureSheafPushforward.{u, w}
            k B hk X Z f hf i hi L n) : ℤ) : ℚ)) →
      ∃ m : ℤ, P.coeff (Finsupp.equivFunOnFinite.symm fun _ => 1) = (m : ℚ)

AlgebraicGeometry.Space.exists_intCast_eq_coeff_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NumericalIntersection.lean, line 868. The attribute's comment: “granted a representing numerical polynomial, whose existence is Tag 0DN4”.

Stacks 0EDG. The intersection number (L₁ ⋯ L_d · Z) is an integer: the coefficient of n₁ ⋯ n_d in a rational polynomial of total degree at most d taking the Euler characteristics χ(X, i_*𝒪_Z ⊗ L₁^{⊗ n₁} ⊗ ⋯ ⊗ L_d^{⊗ n_d}) as its values at the integral tuples is the cast of an integer, namely of AlgebraicGeometry.Space.intersectionNumber.

That coefficient is a priori only rational, and integrality is special to it: a numerical polynomial such as n (n - 1) / 2 has coefficients which are not integers, and it is the degree bound that makes the coefficient of the squarefree monomial a mixed finite difference of finitely many integer values.

theorem exists_intCast_eq_coeff_one (d : ℕ) (f : X.1 ⟶ yoneda.obj (baseObject k B hk))
    (hf : IsProper B (Spec (.of k)) hk f) (i : Z ⟶ X)
    (hi : IsClosedImmersion B (Spec (.of k)) hk i.hom)
    (hd : dimension B (Spec (.of k)) hk Z.1 Z.2 = d)
    (L : Fin d → Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L j)]
    (P : MvPolynomial (Fin d) ℚ)
    (hP : ∀ n : Fin d → ℤ, MvPolynomial.eval (fun j => (n j : ℚ)) P =
      ((@eulerCharacteristic.{u, w} k _ B hk X.1 X.2 f hf
        (twistedModuleUlift.{u, w} B (Spec (.of k)) hk X.1 X.2
          (structureSheafPushforward B (Spec (.of k)) hk i) L n)
          (isCoherent_twistedModuleUlift_structureSheafPushforward.{u, w}
            k B hk X Z f hf i hi L n) : ℤ) : ℚ))
    (hdeg : P.totalDegree ≤ d) :
    ∃ m : ℤ, P.coeff (Finsupp.equivFunOnFinite.symm fun _ => 1) = (m : ℚ)

Tag 0EDH, a lemma

Tag 0EDH in the Stacks Project.

AlgebraicGeometry.Space.intersectionNumber_eq_add_intersectionNumber_of_iso_tensorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntersectionNumberAdditivity.lean, line 169.

Stacks 0EDH. In the situation of Definition 0EDF, the intersection number is additive in each of its invertible modules: if L_{i₀} ≅ L_{i₀}' ⊗ L_{i₀}'', and L' and L'' agree with L away from i₀, then

(L₁ ⋯ L_{i₀} ⋯ L_d · Z) = (L₁ ⋯ L_{i₀}' ⋯ L_d · Z) + (L₁ ⋯ L_{i₀}'' ⋯ L_d · Z).

The proof is the source's: by Stacks 0DN4 (AlgebraicGeometry.Space.exists_representsTwistedEuler_structureSheafPushforward) the twisted Euler characteristics of i_*𝒪_Z by the d + 1 invertible modules L_{i₀}'', L_1', …, L_d' are the values of a numerical polynomial of total degree at most d in d + 1 variables, and AlgebraicGeometry.Space.intersectionNumber_eq_add_of_iso_tensorSheaf_of_totalDegree_le reads the three intersection numbers off it.

theorem intersectionNumber_eq_add_intersectionNumber_of_iso_tensorSheaf (d : ℕ)
    (f : X.1 ⟶ yoneda.obj (baseObject k B hk)) (hf : IsProper B (Spec (.of k)) hk f)
    (i : Z ⟶ X) (hi : IsClosedImmersion B (Spec (.of k)) hk i.hom)
    (hd : dimension B (Spec (.of k)) hk Z.1 Z.2 = d) (i₀ : Fin d)
    (L L' L'' : Fin d → Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L j)]
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L' j)]
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L'' j)]
    (hL' : ∀ j, j ≠ i₀ → L' j = L j) (hL'' : ∀ j, j ≠ i₀ → L'' j = L j)
    (hL : L i₀ ≅ (((Stacks.SheafOfModules.Tensor.sheafTensor
      (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).obj (L' i₀)).obj (L'' i₀) :
        Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)) :
    intersectionNumber.{u, w} k B hk X Z d f hf i hi hd L =
      intersectionNumber.{u, w} k B hk X Z d f hf i hi hd L' +
        intersectionNumber.{u, w} k B hk X Z d f hf i hi hd L''

AlgebraicGeometry.Space.intersectionNumber_eq_add_of_iso_tensorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NumericalIntersection.lean, line 925. The attribute's comment: “with the numerical polynomial of Stacks 0DN4 for the split family of d + 1 invertible modules carried as a hypothesis”.

Stacks 0EDH. Additivity of the intersection number in each of its invertible modules. Let k be a field, let X be a proper algebraic space over k, let i : Z ⟶ X be a closed subspace of dimension d and let L₁, …, L_d be invertible 𝒪_X-modules. Let L' and L'' be two families agreeing with L away from one index i₀ and satisfying L_{i₀} ≅ L_{i₀}' ⊗ L_{i₀}''. Then

(L₁ ⋯ L_{i₀} ⋯ L_d · Z) = (L₁ ⋯ L_{i₀}' ⋯ L_d · Z) + (L₁ ⋯ L_{i₀}'' ⋯ L_d · Z).

The mechanism is the source's. The Euler characteristics of the twists of i_*𝒪_Z by the d + 1 invertible modules L_{i₀}'', L_1', …, L_d' are the values of a rational polynomial Q of total degree at most d in d + 1 variables, which is Stacks 0DN4 and is the one thing carried, as the hypotheses Q, hQ and hQdeg; the three intersection numbers are then the three mixed finite differences of Q obtained by tying the two new variables together, by setting the second to zero, and by setting the first to zero. Their alternating combination is the (d + 1)-fold mixed finite difference of Q, which vanishes because the squarefree monomial in d + 1 variables has degree d + 1; this is MvPolynomial.sum_neg_one_pow_mul_sub_eval_cons_eq_zero.

The three comparisons of the twists by the split family with the twists by L, L' and L'' are proved: at the indicator tuples only the exponents 0 and 1 occur, where the constraints of the sheaf tensor product suffice and no multiplication of tensor powers is needed. See the implementation notes.

theorem intersectionNumber_eq_add_of_iso_tensorSheaf (d : ℕ)
    (f : X.1 ⟶ yoneda.obj (baseObject k B hk)) (hf : IsProper B (Spec (.of k)) hk f)
    (i : Z ⟶ X) (hi : IsClosedImmersion B (Spec (.of k)) hk i.hom)
    (hd : dimension B (Spec (.of k)) hk Z.1 Z.2 = d) (i₀ : Fin d)
    (L L' L'' : Fin d → Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L j)]
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L' j)]
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L'' j)]
    [∀ n : Fin d → ℤ, IsCoherent B (Spec (.of k)) hk X.1 X.2
      (twistedModuleUlift.{u, w} B (Spec (.of k)) hk X.1 X.2
        (structureSheafPushforward B (Spec (.of k)) hk i) L n)]
    [∀ n : Fin d → ℤ, IsCoherent B (Spec (.of k)) hk X.1 X.2
      (twistedModuleUlift.{u, w} B (Spec (.of k)) hk X.1 X.2
        (structureSheafPushforward B (Spec (.of k)) hk i) L' n)]
    [∀ n : Fin d → ℤ, IsCoherent B (Spec (.of k)) hk X.1 X.2
      (twistedModuleUlift.{u, w} B (Spec (.of k)) hk X.1 X.2
        (structureSheafPushforward B (Spec (.of k)) hk i) L'' n)]
    [∀ m : Fin (d + 1) → ℤ, IsCoherent B (Spec (.of k)) hk X.1 X.2
      (twistedModuleUlift.{u, w} B (Spec (.of k)) hk X.1 X.2
        (structureSheafPushforward B (Spec (.of k)) hk i) (Fin.cons (L'' i₀) L') m)]
    (hL' : ∀ j, j ≠ i₀ → L' j = L j) (hL'' : ∀ j, j ≠ i₀ → L'' j = L j)
    (hL : L i₀ ≅ (((Stacks.SheafOfModules.Tensor.sheafTensor
      (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).obj (L' i₀)).obj (L'' i₀) :
        Modules.{u, u} B (Spec (.of k)) hk X.1 X.2))
    (Q : MvPolynomial (Fin (d + 1)) ℚ) (hQdeg : Q.totalDegree ≤ d)
    (hQ : ∀ m : Fin (d + 1) → ℤ, MvPolynomial.eval (fun p => (m p : ℚ)) Q =
      ((eulerCharacteristic.{u, w} k B hk X.1 X.2 f hf
        (twistedModuleUlift.{u, w} B (Spec (.of k)) hk X.1 X.2
          (structureSheafPushforward B (Spec (.of k)) hk i) (Fin.cons (L'' i₀) L') m) : ℤ) : ℚ)) :
    intersectionNumber.{u, w} k B hk X Z d f hf i hi hd L =
      intersectionNumber.{u, w} k B hk X Z d f hf i hi hd L' +
        intersectionNumber.{u, w} k B hk X Z d f hf i hi hd L''

Tag 0EDI, a lemma

Tag 0EDI in the Stacks Project.

AlgebraicGeometry.Space.intersectionNumber_eq_finsum_mul_intersectionNumber_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntersectionNumberComponents.lean, line 308. References: SGA 6 X (4.4), “partial”.

Stacks 0EDI. Let k be a field, X a proper algebraic space over k, i : Z ⟶ X a closed subspace of dimension d and L₁, …, L_d invertible 𝒪_X-modules. Let Z_C ⊆ Z be the irreducible components of Z of dimension d — the components C of the closed set |Z| ⊆ |X| of Krull dimension d, each with its reduced induced structure (Stacks 03IQ) — let x̄_C be a geometric generic point of Z_C and let m_C = length_{𝒪_{X, x̄_C}}(𝒪_{Z, x̄_C}), the length of the stalk of i_*𝒪_Z at x̄_C. Then

(L₁ ⋯ L_d · Z) = ∑_C m_C (L₁ ⋯ L_d · Z_C).

As in the source this is immediate from Stacks 0EDE, in the form AlgebraicGeometry.Space.exists_twistedEuler_sub_finsum_mul_componentStructureSheaf applied to F = i_*𝒪_Z, whose support is |Z| (AlgebraicGeometry.Space.moduleSupportSet_structureSheafPushforward_of_isClosedImmersion): the difference of the Euler characteristics is a polynomial of total degree < d, so its coefficient of n₁ ⋯ n_d vanishes, and comparing that coefficient is Space.intersectionNumber_eq_finsum_mul_of_eval_eq_sub_finsum_irreducibleComponents. The length m_C is a natural number by Stacks 0EE4.

theorem intersectionNumber_eq_finsum_mul_intersectionNumber_irreducibleComponents (d : ℕ)
    (f : X.1 ⟶ yoneda.obj (baseObject k B hk)) (hf : IsProper B (Spec (.of k)) hk f)
    (i : Z ⟶ X) (hi : IsClosedImmersion B (Spec (.of k)) hk i.hom)
    (hd : dimension B (Spec (.of k)) hk Z.1 Z.2 = d)
    (L : Fin d → Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L j)]
    (x : irreducibleComponents (Set.range (pointsMap B (Spec (.of k)) hk Z.1 i.hom)) →
      GeometricPoint B (Spec (.of k)) hk X.1)
    (hx : ∀ C, IsGenericPoint (x C).image
      (Subtype.val '' (C : Set (Set.range (pointsMap B (Spec (.of k)) hk Z.1 i.hom))))) :
    intersectionNumber.{u, w} k B hk X Z d f hf i hi hd L =
      ∑ᶠ (C : {C : irreducibleComponents (Set.range (pointsMap B (Spec (.of k)) hk Z.1 i.hom)) //
          topologicalKrullDim (Subtype.val ''
            (C : Set (Set.range (pointsMap B (Spec (.of k)) hk Z.1 i.hom)))) = d}),
        ((geometricLength B (Spec (.of k)) hk X (x C.1)
            (structureSheafPushforward B (Spec (.of k)) hk i)).toNat : ℤ) *
          intersectionNumber.{u, w} k B hk X
            (closedSubfunctorSpace B (Spec (.of k)) hk
              (isClosedSubspace_reducedClosedSubspace B (Spec (.of k)) hk X.1 X.2 _
                (closedSetComponentPoints B (Spec (.of k)) hk _
                  (isClosed_range_pointsMap_of_isClosedImmersion B (Spec (.of k)) hk X.2 i.hom hi)
                  C.1).isClosed)) d f hf
            (closedSubfunctorι B (Spec (.of k)) hk
              (isClosedSubspace_reducedClosedSubspace B (Spec (.of k)) hk X.1 X.2 _
                (closedSetComponentPoints B (Spec (.of k)) hk _
                  (isClosed_range_pointsMap_of_isClosedImmersion B (Spec (.of k)) hk X.2 i.hom hi)
                  C.1).isClosed))
            (isClosedSubspace_reducedClosedSubspace B (Spec (.of k)) hk X.1 X.2 _
              (closedSetComponentPoints B (Spec (.of k)) hk _
                (isClosed_range_pointsMap_of_isClosedImmersion B (Spec (.of k)) hk X.2 i.hom hi)
                C.1).isClosed).2
            ((dimension_reducedClosedSubspace B (Spec (.of k)) hk X.1 X.2
              (isDecentSpace_of_isProper_baseObject k B hk X.1 X.2 f hf) _ _).trans C.2) L

Tag 0EDJ, a lemma

Tag 0EDJ in the Stacks Project.

AlgebraicGeometry.Space.intersectionNumber_modulePullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntersectionNumberProperImage.lean, line 668.

Stacks 0EDJ. Let k be a field, let f : Y ⟶ X be a morphism of algebraic spaces proper over k, let Z ⊂ Y be an integral closed subspace of dimension d and let L₁, …, L_d be invertible 𝒪_X-modules. Let f(Z) ⊂ X be the image of Z: the integral closed subspace on the closure of f(|Z|), which is the scheme-theoretic image of Z ⟶ X, and has dimension at most d. Then

(f^*L₁ ⋯ f^*L_d · Z) = deg(Z/f(Z)) · (L₁ ⋯ L_d · f(Z))

where deg(Z/f(Z)) is the degree of Stacks 0AD6 if dim f(Z) = d, and the right hand side is 0 if dim f(Z) < d.

The three conjuncts are: f(Z) is the scheme-theoretic image of Z ⟶ X (AlgebraicGeometry.Space.IntegralClosedSubspace.closureImage_subspace_eq_schemeTheoreticImage, Stacks 0830); dim f(Z) ≤ d (AlgebraicGeometry.Space.IntegralClosedSubspace.dimension_closureImage_le, Stacks 0EDC); and the formula, which is AlgebraicGeometry.Space.intersectionNumber_modulePullback_eq_degree_mul when dim f(Z) = d and AlgebraicGeometry.Space.intersectionNumber_modulePullback_eq_zero_of_dimension_lt otherwise.

theorem intersectionNumber_modulePullback_eq (f : Y ⟶ X)
    (Z : IntegralClosedSubspace B (Spec (.of k)) hk Y.1) {d : ℕ}
    (hZd : dimension B (Spec (.of k)) hk Z.subspace.toFunctor Z.isClosedSubspace.1 = d)
    (L : Fin d → Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [hL : ∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O).property (L j)] :
    let W := IntegralClosedSubspace.closureImage B (Spec (.of k)) hk X.2
      (isDecentSpace_of_isProper_baseObject k B hk X.1 X.2 pX hpX) f.hom Z
    W.subspace = schemeTheoreticImageSubfunctor B (Spec (.of k)) hk (Z.subspace.ι ≫ f.hom) ∧
      dimension B (Spec (.of k)) hk W.subspace.toFunctor W.isClosedSubspace.1 ≤ d ∧
      @intersectionNumber.{u, w} k _ B hk Y
          (closedSubspaceToSpace B (Spec (.of k)) hk Y ⟨Z.subspace, Z.isClosedSubspace⟩) d pY hpY
          (closedSubspaceInclusion B (Spec (.of k)) hk Y ⟨Z.subspace, Z.isClosedSubspace⟩)
          Z.isClosedSubspace.2 hZd
          (fun j => (modulePullback B (Spec (.of k)) hk f).obj (L j))
          (fun j => stacksIsInvertible_modulePullback_obj B (Spec (.of k)) hk f (L j)
            (hM := hL j)) =
        if hW : dimension B (Spec (.of k)) hk W.subspace.toFunctor W.isClosedSubspace.1 = d then
          (degree B (Spec (.of k)) hk Z.isClosedSubspace.1 W.isClosedSubspace.1 Z.isIntegralSpace
              W.isIntegralSpace
              (IntegralClosedSubspace.toClosureImage B (Spec (.of k)) hk X.2
                (isDecentSpace_of_isProper_baseObject k B hk X.1 X.2 pX hpX) f.hom Z) : ℤ) *
            intersectionNumber.{u, w} k B hk X
              (closedSubspaceToSpace B (Spec (.of k)) hk X ⟨W.subspace, W.isClosedSubspace⟩) d pX
              hpX (closedSubspaceInclusion B (Spec (.of k)) hk X ⟨W.subspace, W.isClosedSubspace⟩)
              W.isClosedSubspace.2 hW L
        else 0

Tag 0EDK, a lemma

Tag 0EDK in the Stacks Project.

AlgebraicGeometry.Space.intersectionNumber_eq_sum_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntersectionNumberCartierDivisor.lean, line 168. The attribute's comment: “the right-hand side as the defining sum of Definition 0EDF for D, of dimension at most d; it is intersectionNumber D when dim D = d and 0 when dim D < d”.

Stacks 0EDK. Let k be a field, let X be a proper algebraic space over k, let i : Z ⟶ X be a closed subspace of dimension d + 1 and let L₁, …, L_{d+1} be invertible 𝒪_X-modules. Let D ⊆ Z be an effective Cartier divisor with L₁|_Z ≅ 𝒪_Z(D), and let j : D ⟶ X be its inclusion into X. Then

(L₁ ⋯ L_{d+1} · Z) = (L₂ ⋯ L_{d+1} · D).

The right-hand side is written as the defining expression of Definition 0EDF, ∑_{T ⊆ {2, …, d + 1}} (-1)^{d - |T|} χ(X, j_*𝒪_D ⊗ ⨂_{l ∈ T} L_l):

(i) this is the intersection number of Definition 0EDF read for the closed subspace D, which has dimension at most d (AlgebraicGeometry.Space.dimension_le_of_isEffectiveCartierDivisor) but not necessarily exactly d;

(ii) it is AlgebraicGeometry.Space.intersectionNumber of D by AlgebraicGeometry.Space.intersectionNumber_eq_sum whenever dim D = d, which is intersectionNumber_eq_intersectionNumber_of_isEffectiveCartierDivisor_of_dimension_eq;

(iii) it is 0 when dim D < d, by Stacks 0DN4, which is AlgebraicGeometry.Space.sum_eulerCharacteristic_eq_zero_of_dimension_lt.

No hypothesis beyond the source's is taken.

theorem intersectionNumber_eq_sum_of_isEffectiveCartierDivisor (d : ℕ)
    (f : X.1 ⟶ yoneda.obj (baseObject k B hk)) (hf : IsProper B (Spec (.of k)) hk f) (i : Z ⟶ X)
    (hi : IsClosedImmersion B (Spec (.of k)) hk i.hom)
    (hd : dimension B (Spec (.of k)) hk Z.1 Z.2 = d + 1)
    (Dv : ClosedSubspaces B (Spec (.of k)) hk Z.1)
    (hDv : IsEffectiveCartierDivisor B (Spec (.of k)) hk Z Dv)
    (L : Fin (d + 1) → Modules.{u, u} B (Spec (.of k)) hk X.1 X.2)
    [∀ j, Stacks.SheafOfModules.IsInvertible (structurePresheaf B (Spec (.of k)) hk X.1)
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B (Spec (.of k)) hk X.1 X.2).O)).property (L j)]
    (hL : (modulePullback B (Spec (.of k)) hk i).obj (L 0) ≅
      associatedInvertibleSheaf B (Spec (.of k)) hk Z Dv hDv) :
    intersectionNumber.{u, w} k B hk X Z (d + 1) f hf i hi hd L =
      ∑ T : Finset (Fin d), (-1 : ℤ) ^ (d - T.card) *
        @eulerCharacteristic.{u, w} k _ B hk X.1 X.2 f hf
          (twistedModuleUlift.{u, w} B (Spec (.of k)) hk X.1 X.2
            (structureSheafPushforward B (Spec (.of k)) hk
              ((ObjectProperty.homMk Dv.1.ι :
                (⟨Dv.1.toFunctor, Dv.2.1⟩ : AlgebraicSpaces B (Spec (.of k)) hk) ⟶ Z) ≫ i))
            (fun j => L j.succ) fun j => if j ∈ T then 1 else 0)
          (isCoherent_twistedModuleUlift_structureSheafPushforward.{u, w} k B hk X
            ⟨Dv.1.toFunctor, Dv.2.1⟩ f hf _
            (isClosedImmersion_comp B (Spec (.of k)) hk Dv.1.ι i.hom Dv.2.2 hi) _ _)

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

72.14 Geometrically integral… to 72.18 Numerical intersections

Section72.14 Geometrically integral algebraic spaces#

Tag 0DMW, a definition

Tag 0DMX, a lemma

Tag 0DMY, a lemma

Tag 0DMZ, a lemma

Sources

Section72.15 Dimension#

Tag 0EDB, a lemma

Tag 0EDC, a lemma

Sources

Section72.16 Spaces smooth over fields#

Tag 06M1, a lemma

Tag 07W4, a lemma

Sources

Section72.17 Euler characteristics#

Tag 0DN1, a definition

Tag 0DN2, a lemma

Tag 0EDD, a lemma

Sources

Section72.18 Numerical intersections#

Tag 0DN4, a lemma

Tag 0EDE, a lemma

Tag 0EDF, a definition

Tag 0EDG, a lemma

Tag 0EDH, a lemma

Tag 0EDI, a lemma

Tag 0EDJ, a lemma

Tag 0EDK, a lemma

Sources

Section72.14 Geometrically integral algebraic spaces #

Section72.15 Dimension #

Section72.16 Spaces smooth over fields #

Section72.17 Euler characteristics #

Section72.18 Numerical intersections #