Intersection numbers from Snapper coefficients

Intersection numbers are the top mixed finite differences of the Euler characteristic of line-bundle twists. No cycle group or Chow ring occurs in the construction.

The geometric input remains explicit. TwistContext records coherent representatives and the Snapper.GeometricInduction certificates for every finite family of Picard classes, together with one Picard-level Euler function which they realize. IntersectionContext specializes the base coherent sheaf to the structure sheaf. Thus the missing geometric construction is data in a theorem statement, never a global axiom.

Finite differences on the Picard group

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.picardDifference {X : Scheme} (L : Scheme.Modules.Pic X) (f : Scheme.Modules.Pic X → ℤ) : Scheme.Modules.Pic X → ℤ

One finite difference of an integer-valued function on the Picard group.

Equations

• AlgebraicGeometry.IntersectionTheory.Number.picardDifference L f M = f (M * L) - f M

def AlgebraicGeometry.IntersectionTheory.Number.picardMixedDifference {X : Scheme} : List (Scheme.Modules.Pic X) → (Scheme.Modules.Pic X → ℤ) → Scheme.Modules.Pic X → ℤ

Successive finite differences in a list of Picard classes.

Equations

• One or more equations did not get rendered due to their size.
• AlgebraicGeometry.IntersectionTheory.Number.picardMixedDifference [] x✝ = x✝

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.picardCoefficient {X : Scheme} (classes : List (Scheme.Modules.Pic X)) (f : Scheme.Modules.Pic X → ℤ) : ℤ

A mixed Picard coefficient is evaluated at the trivial line bundle.

Equations

• AlgebraicGeometry.IntersectionTheory.Number.picardCoefficient classes f = AlgebraicGeometry.IntersectionTheory.Number.picardMixedDifference classes f 1

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Number.picardMixedDifference_nil {X : Scheme} (f : Scheme.Modules.Pic X → ℤ) : picardMixedDifference [] f = f

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Number.picardMixedDifference_cons {X : Scheme} (L : Scheme.Modules.Pic X) (classes : List (Scheme.Modules.Pic X)) (f : Scheme.Modules.Pic X → ℤ) : picardMixedDifference (L :: classes) f = picardDifference L (picardMixedDifference classes f)

theorem AlgebraicGeometry.IntersectionTheory.Number.picardDifference_comm {X : Scheme} (L M : Scheme.Modules.Pic X) (f : Scheme.Modules.Pic X → ℤ) : picardDifference L (picardDifference M f) = picardDifference M (picardDifference L f)

theorem AlgebraicGeometry.IntersectionTheory.Number.picardMixedDifference_eq_of_perm {X : Scheme} {classes classes' : List (Scheme.Modules.Pic X)} (h : classes.Perm classes') (f : Scheme.Modules.Pic X → ℤ) : picardMixedDifference classes f = picardMixedDifference classes' f

Picard mixed differences are symmetric in their directions.

theorem AlgebraicGeometry.IntersectionTheory.Number.picardCoefficient_eq_of_perm {X : Scheme} {classes classes' : List (Scheme.Modules.Pic X)} (h : classes.Perm classes') (f : Scheme.Modules.Pic X → ℤ) : picardCoefficient classes f = picardCoefficient classes' f

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Number.picardDifference_one {X : Scheme} (f : Scheme.Modules.Pic X → ℤ) : picardDifference 1 f = 0

theorem AlgebraicGeometry.IntersectionTheory.Number.picardDifference_mul_direction {X : Scheme} (L M : Scheme.Modules.Pic X) (f : Scheme.Modules.Pic X → ℤ) : picardDifference (L * M) f = picardDifference L f + picardDifference M f + picardDifference L (picardDifference M f)

Splitting a tensor-product direction introduces one second-difference correction.

def AlgebraicGeometry.IntersectionTheory.Number.PicardDegreeLE {X : Scheme} (d : ℕ) (f : Scheme.Modules.Pic X → ℤ) : Prop

Picard-group degree at most d, in the coefficient form needed for intersections.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.IntersectionTheory.Number.picardCoefficient_cons_mul {X : Scheme} (classes : List (Scheme.Modules.Pic X)) (L M : Scheme.Modules.Pic X) (f : Scheme.Modules.Pic X → ℤ) (hf : PicardDegreeLE (classes.length + 1) f) : picardCoefficient (L * M :: classes) f = picardCoefficient (L :: classes) f + picardCoefficient (M :: classes) f

Additivity of a top Picard coefficient in its first class.

theorem AlgebraicGeometry.IntersectionTheory.Number.picardCoefficient_middle_mul {X : Scheme} (before after : List (Scheme.Modules.Pic X)) (L M : Scheme.Modules.Pic X) (f : Scheme.Modules.Pic X → ℤ) (hf : PicardDegreeLE (before.length + after.length + 1) f) : picardCoefficient (before ++ L * M :: after) f = picardCoefficient (before ++ L :: after) f + picardCoefficient (before ++ M :: after) f

Additivity of a top Picard coefficient in any class slot.

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.picardCoefficientAddHom {X : Scheme} (before after : List (Scheme.Modules.Pic X)) (f : Scheme.Modules.Pic X → ℤ) (hf : PicardDegreeLE (before.length + after.length + 1) f) : Additive (Scheme.Modules.Pic X) →+ ℤ

With every other class fixed, a top Picard coefficient is an additive homomorphism from the Picard group written additively.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Number.picardCoefficientAddHom_apply {X : Scheme} (before after : List (Scheme.Modules.Pic X)) (f : Scheme.Modules.Pic X → ℤ) (hf : PicardDegreeLE (before.length + after.length + 1) f) (L : Additive (Scheme.Modules.Pic X)) : (picardCoefficientAddHom before after f hf) L = picardCoefficient (before ++ Additive.toMul L :: after) f

theorem AlgebraicGeometry.IntersectionTheory.Number.picardCoefficient_middle_zpow {X : Scheme} (before after : List (Scheme.Modules.Pic X)) (L : Scheme.Modules.Pic X) (m : ℤ) (f : Scheme.Modules.Pic X → ℤ) (hf : PicardDegreeLE (before.length + after.length + 1) f) : picardCoefficient (before ++ L ^ m :: after) f = m * picardCoefficient (before ++ L :: after) f

Integer homogeneity of a top Picard coefficient in every slot.

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.picardMonomial {X : Scheme} {ι : Type u_1} [Fintype ι] (L : ι → Scheme.Modules.Pic X) (n : NumericalPolynomial.Lattice ι) : Scheme.Modules.Pic X

The Picard class represented by an integer vector in a finite family.

Equations

• AlgebraicGeometry.IntersectionTheory.Number.picardMonomial L n = ∏ i : ι, L i ^ n i

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.picardPolynomial {X : Scheme} {ι : Type u_1} [Fintype ι] (f : Scheme.Modules.Pic X → ℤ) (L : ι → Scheme.Modules.Pic X) : NumericalPolynomial.NumericalFunction ι

Restrict a Picard-level function to the exponent lattice generated by L.

Equations

• AlgebraicGeometry.IntersectionTheory.Number.picardPolynomial f L n = f (AlgebraicGeometry.IntersectionTheory.Number.picardMonomial L n)

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Number.picardMonomial_zero {X : Scheme} {ι : Type u_1} [Fintype ι] (L : ι → Scheme.Modules.Pic X) : picardMonomial L 0 = 1

theorem AlgebraicGeometry.IntersectionTheory.Number.picardMonomial_add {X : Scheme} {ι : Type u_1} [Fintype ι] (L : ι → Scheme.Modules.Pic X) (m n : NumericalPolynomial.Lattice ι) : picardMonomial L (m + n) = picardMonomial L m * picardMonomial L n

theorem AlgebraicGeometry.IntersectionTheory.Number.mixedDifference_picardPolynomial {X : Scheme} {ι : Type u_1} [Fintype ι] (f : Scheme.Modules.Pic X → ℤ) (L : ι → Scheme.Modules.Pic X) (directions : List (NumericalPolynomial.Lattice ι)) (n : NumericalPolynomial.Lattice ι) : NumericalPolynomial.mixedDifference directions (picardPolynomial f L) n = picardMixedDifference (List.map (picardMonomial L) directions) f (picardMonomial L n)

Lattice mixed differences are Picard mixed differences in the represented classes.

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Number.picardMonomial_coordinateDirection {X : Scheme} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : ι → Scheme.Modules.Pic X) (i : ι) : picardMonomial L (NumericalPolynomial.coordinateDirection i) = L i

theorem AlgebraicGeometry.IntersectionTheory.Number.topCoefficient_picardPolynomial {X : Scheme} {d : ℕ} (f : Scheme.Modules.Pic X → ℤ) (L : Fin d → Scheme.Modules.Pic X) : NumericalPolynomial.topCoefficient (fun (i : Fin d) => NumericalPolynomial.coordinateDirection i) (picardPolynomial f L) = picardCoefficient (List.ofFn L) f

The standard-coordinate top coefficient is the intrinsic Picard mixed coefficient.

Explicit geometric contexts

structure AlgebraicGeometry.IntersectionTheory.Number.TwistContext {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : Cohomology.FiniteCohomology k X) (F : Coh X) (d : ℕ) : Type (u + 1)

Uniform Snapper data for twists of one coherent sheaf by every finite family of line bundles. The single eulerPic field makes coefficients independent of the chosen finite presentation; realization identifies it with the actual geometric Euler characteristic.

• eulerPic : Scheme.Modules.Pic X → ℤ
• twistFamily (r : ℕ) (L : Fin r → Scheme.Modules.Pic X) : Snapper.CoherentTwistFamily F L
• geometricInduction (r : ℕ) (L : Fin r → Scheme.Modules.Pic X) : Snapper.GeometricInduction D ⋯ d
• realization (r : ℕ) (L : Fin r → Scheme.Modules.Pic X) (n : NumericalPolynomial.Lattice (Fin r)) : self.eulerPic (picardMonomial L n) = Snapper.eulerFunction D ⋯ n

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.structureSheafObject {X : Scheme} (h : Scheme.Modules.IsCoherent X (SheafOfModules.unit X.ringCatSheaf)) : Coh X

The structure sheaf as a coherent object, from the explicitly supplied coherence proof.

Equations

• AlgebraicGeometry.IntersectionTheory.Number.structureSheafObject h = { obj := SheafOfModules.unit X.ringCatSheaf, property := h }

structure AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : Cohomology.FiniteCohomology k X) (C : D.LinearConnectingSystem) (d : ℕ) : Type (u + 1)

Snapper input specialized to twists of the structure sheaf.

• structureSheafCoherent : Scheme.Modules.IsCoherent X (SheafOfModules.unit X.ringCatSheaf)
• twists : TwistContext D (structureSheafObject ⋯) d

theorem AlgebraicGeometry.IntersectionTheory.Number.TwistContext.eulerFunction_eq_picardPolynomial {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {F : Coh X} {d : ℕ} (P : TwistContext D F d) (r : ℕ) (L : Fin r → Scheme.Modules.Pic X) : Snapper.eulerFunction D ⋯ = picardPolynomial P.eulerPic L

The geometric Euler function of any chosen finite presentation is the restriction of the intrinsic Picard-level Euler function.

theorem AlgebraicGeometry.IntersectionTheory.Number.TwistContext.picardDegreeLE {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {F : Coh X} {d : ℕ} (P : TwistContext D F d) (C : D.LinearConnectingSystem) : PicardDegreeLE d P.eulerPic

Snapper polynomiality for every finite presentation implies intrinsic Picard coefficient vanishing in degree d + 1.

def AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.eulerPic {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) : Scheme.Modules.Pic X → ℤ

The intrinsic Euler characteristic of a Picard class.

Equations

• P.eulerPic = P.twists.eulerPic

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardDegreeLE {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) : PicardDegreeLE d P.eulerPic

The Picard Euler function has finite-difference degree at most the geometric dimension.

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardIntersectionNumber {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (L : Fin d → Scheme.Modules.Pic X) : ℤ

The dimension-d intersection number of d Picard classes, defined as the top mixed Snapper coefficient of the corresponding structure-sheaf twists.

Equations

• P.picardIntersectionNumber L = NumericalPolynomial.topCoefficient (fun (i : Fin d) => NumericalPolynomial.coordinateDirection i) (AlgebraicGeometry.IntersectionTheory.Snapper.eulerFunction D ⋯)

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardIntersectionNumber_eq_coefficient {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (L : Fin d → Scheme.Modules.Pic X) : P.picardIntersectionNumber L = picardCoefficient (List.ofFn L) P.eulerPic

Intrinsic formulation: the intersection number is the iterated Picard difference of eulerPic, evaluated at the trivial bundle.

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardIntersectionList {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (classes : List (Scheme.Modules.Pic X)) : ℤ

List form of the intersection coefficient. The separate list API is convenient for multilinearity proofs and for downstream Chern-character formulas.

Equations

• P.picardIntersectionList classes = AlgebraicGeometry.IntersectionTheory.Number.picardCoefficient classes P.eulerPic

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardIntersectionList_ofFn {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (L : Fin d → Scheme.Modules.Pic X) : P.picardIntersectionList (List.ofFn L) = P.picardIntersectionNumber L

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardIntersectionNumber_congr {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) {L M : Fin d → Scheme.Modules.Pic X} (h : ∀ (i : Fin d), L i = M i) : P.picardIntersectionNumber L = P.picardIntersectionNumber M

Intersection numbers are invariant under line-bundle isomorphism. Equality in Pic X is exactly equality of isomorphism classes.

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardIntersectionNumber_comp_perm {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (L : Fin d → Scheme.Modules.Pic X) (σ : Equiv.Perm (Fin d)) : P.picardIntersectionNumber (L ∘ ⇑σ) = P.picardIntersectionNumber L

Symmetry in all divisor arguments.

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardIntersectionList_eq_of_perm {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) {classes classes' : List (Scheme.Modules.Pic X)} (h : classes.Perm classes') : P.picardIntersectionList classes = P.picardIntersectionList classes'

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardIntersectionList_middle_mul {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (before after : List (Scheme.Modules.Pic X)) (L M : Scheme.Modules.Pic X) (hlength : before.length + after.length + 1 = d) : P.picardIntersectionList (before ++ L * M :: after) = P.picardIntersectionList (before ++ L :: after) + P.picardIntersectionList (before ++ M :: after)

Multilinearity, in list form: tensor product in any one slot becomes addition of intersection numbers.

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardIntersectionList_middle_zpow {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (before after : List (Scheme.Modules.Pic X)) (L : Scheme.Modules.Pic X) (m : ℤ) (hlength : before.length + after.length + 1 = d) : P.picardIntersectionList (before ++ L ^ m :: after) = m * P.picardIntersectionList (before ++ L :: after)

Integer homogeneity, in list form.

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardIntersectionList_middle_one {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (before after : List (Scheme.Modules.Pic X)) : P.picardIntersectionList (before ++ 1 :: after) = 0

A trivial line-bundle argument makes every positive-arity intersection vanish.

Cartier divisors and divisor classes

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.cartierClassIntersectionNumber {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (classes : Fin d → Scheme.CartierDivisor.ClassGroup X) : ℤ

Intersection numbers of Cartier divisor classes, through the additive class-to-Picard map.

Equations

• P.cartierClassIntersectionNumber classes = P.picardIntersectionNumber fun (i : Fin d) => Additive.toMul (AlgebraicGeometry.Scheme.CartierDivisor.classToPicAdd (classes i))

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.cartierDivisorIntersectionNumber {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (divisors : Fin d → ↥X.CartierDivisor) : ℤ

Intersection numbers of actual Cartier divisors depend only on their divisor classes.

Equations

• P.cartierDivisorIntersectionNumber divisors = P.cartierClassIntersectionNumber fun (i : Fin d) => (AlgebraicGeometry.Scheme.CartierDivisor.toClass X) (divisors i)

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.cartierDivisorIntersectionNumber_eq_picard {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (divisors : Fin d → ↥X.CartierDivisor) : P.cartierDivisorIntersectionNumber divisors = P.picardIntersectionNumber fun (i : Fin d) => Scheme.CartierDivisor.toPic (divisors i)

The divisor and Picard formulations agree under D ↦ O_X(D).

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.cartierDivisorIntersectionNumber_eq_of_principalEquivalent {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) {divisors divisors' : Fin d → ↥X.CartierDivisor} (h : ∀ (i : Fin d), (Scheme.CartierDivisor.toClass X) (divisors i) = (Scheme.CartierDivisor.toClass X) (divisors' i)) : P.cartierDivisorIntersectionNumber divisors = P.cartierDivisorIntersectionNumber divisors'

Principal equivalence does not change intersection numbers.

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.cartierDivisorIntersectionNumber_add_principal {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (divisors : Fin d → ↥X.CartierDivisor) (f : Fin d → Additive (↑X.functionField)ˣ) : (P.cartierDivisorIntersectionNumber fun (i : Fin d) => divisors i + (Scheme.CartierDivisor.principal X) (f i)) = P.cartierDivisorIntersectionNumber divisors

Adding a principal divisor in every slot leaves the intersection number unchanged.

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.cartierDivisorIntersectionNumber_comp_perm {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} (P : IntersectionContext D C d) (divisors : Fin d → ↥X.CartierDivisor) (σ : Equiv.Perm (Fin d)) : P.cartierDivisorIntersectionNumber (divisors ∘ ⇑σ) = P.cartierDivisorIntersectionNumber divisors

Symmetry also holds in the Cartier-divisor formulation.

Dimension-zero, curve, and surface specializations

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.point_normalization {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} (P : IntersectionContext D C 0) (L : Fin 0 → Scheme.Modules.Pic X) : P.picardIntersectionNumber L = P.eulerPic 1

In dimension zero the empty intersection is honestly the empty coefficient: χ(O_X).

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.curve_intersection_eq {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} (P : IntersectionContext D C 1) (L : Scheme.Modules.Pic X) : (P.picardIntersectionNumber fun (x : Fin 1) => L) = P.eulerPic L - P.eulerPic 1

On a curve the divisor number is the first difference χ(L) - χ(O_X).

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.surfaceIntersectionNumber {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} (P : IntersectionContext D C 2) (L M : Scheme.Modules.Pic X) : ℤ

The binary surface intersection coefficient.

Equations

• P.surfaceIntersectionNumber L M = AlgebraicGeometry.IntersectionTheory.Number.picardCoefficient [L, M] P.eulerPic

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.picardIntersectionNumber_fin2 {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} (P : IntersectionContext D C 2) (L M : Scheme.Modules.Pic X) : P.picardIntersectionNumber ![L, M] = P.surfaceIntersectionNumber L M

The binary name is exactly the Fin 2 top Snapper coefficient.

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.surfaceIntersectionNumber_eq {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} (P : IntersectionContext D C 2) (L M : Scheme.Modules.Pic X) : P.surfaceIntersectionNumber L M = P.eulerPic (L * M) - P.eulerPic L - P.eulerPic M + P.eulerPic 1

The surface coefficient is the expected inclusion-exclusion expression.

noncomputable def AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.surfaceIntersectionPairing {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} (P : IntersectionContext D C 2) : Additive (Scheme.Modules.Pic X) →ₗ[ℤ] Additive (Scheme.Modules.Pic X) →ₗ[ℤ] ℤ

The surface specialization as a symmetric bilinear form on the additive Picard group.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.surfaceIntersectionPairing_apply {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} (P : IntersectionContext D C 2) (L M : Scheme.Modules.Pic X) : (P.surfaceIntersectionPairing (Additive.ofMul L)) (Additive.ofMul M) = P.surfaceIntersectionNumber L M

theorem AlgebraicGeometry.IntersectionTheory.Number.IntersectionContext.surfaceIntersectionPairing_symm {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} (P : IntersectionContext D C 2) (L M : Scheme.Modules.Pic X) : (P.surfaceIntersectionPairing (Additive.ofMul L)) (Additive.ofMul M) = (P.surfaceIntersectionPairing (Additive.ofMul M)) (Additive.ofMul L)