Snapper polynomiality for line-bundle twists

This file is the geometric bridge from Picard-group tensor powers and Euler characteristics to the dimension-general finite-difference API in NumericalPolynomial.

Mathlib and the present geometric layer do not yet supply the hyperplane-section induction used in the usual proof of Snapper's theorem, nor a general dimension API for schemes. We therefore package exactly that missing input as GeometricInduction: its steps are genuine short exact sequences, with the scalar-linear connecting maps required by Euler additivity, and its terminal families are zero after d + 1 cuts. snapper proves polynomiality from this certificate. A future geometric construction of the certificate will not change the theorem or its downstream coefficient API.

The exponent of a line bundle is an integer. Positive and negative powers are formed in Pic X, so negative twists use the tensor inverse already contained in the Picard group rather than a separate ad hoc construction.

Integer powers in the Picard group

noncomputable def AlgebraicGeometry.IntersectionTheory.Snapper.picardPower {X : Scheme} (L : Scheme.Modules.Pic X) (n : ℤ) : Scheme.Modules.Pic X

The nth tensor power of a line-bundle class, including negative powers.

Equations

• AlgebraicGeometry.IntersectionTheory.Snapper.picardPower L n = L ^ n

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Snapper.picardPower_zero {X : Scheme} (L : Scheme.Modules.Pic X) : picardPower L 0 = 1

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Snapper.picardPower_add {X : Scheme} (L : Scheme.Modules.Pic X) (m n : ℤ) : picardPower L (m + n) = picardPower L m * picardPower L n

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Snapper.picardPower_neg {X : Scheme} (L : Scheme.Modules.Pic X) (n : ℤ) : picardPower L (-n) = (picardPower L n)⁻¹

noncomputable def AlgebraicGeometry.IntersectionTheory.Snapper.linePower {X : Scheme} (L : Scheme.Modules.Pic X) (n : ℤ) : X.Modules

A chosen invertible-sheaf representative of the integer Picard power L ^ n.

Equations

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

instance AlgebraicGeometry.IntersectionTheory.Snapper.linePower_isInvertible {X : Scheme} (L : Scheme.Modules.Pic X) (n : ℤ) : (have this := linePower L n; this).IsInvertible

@[simp]

theorem AlgebraicGeometry.IntersectionTheory.Snapper.linePower_picardClass {X : Scheme} (L : Scheme.Modules.Pic X) (n : ℤ) : Scheme.Modules.PicardClass.mk (linePower L n) = ↑(picardPower L n)

The chosen representative has exactly the requested Picard class.

Multivariable twists

noncomputable def AlgebraicGeometry.IntersectionTheory.Snapper.twistModulesAlong {X : Scheme} {ι : Type v} : List ι → (ι → Scheme.Modules.Pic X) → NumericalPolynomial.Lattice ι → X.Modules → X.Modules

Tensor a module sheaf successively by the integer powers indexed by a list.

Equations

• One or more equations did not get rendered due to their size.
• AlgebraicGeometry.IntersectionTheory.Snapper.twistModulesAlong [] x✝² x✝¹ x✝ = x✝

noncomputable def AlgebraicGeometry.IntersectionTheory.Snapper.twistModules {X : Scheme} {ι : Type v} [Fintype ι] [DecidableEq ι] (L : ι → Scheme.Modules.Pic X) (n : NumericalPolynomial.Lattice ι) (F : X.Modules) : X.Modules

The simultaneous line-bundle twist. The list order is fixed by Finset.univ.toList; the Picard group records that different tensor orders are canonically isomorphic.

Equations

• AlgebraicGeometry.IntersectionTheory.Snapper.twistModules L n F = AlgebraicGeometry.IntersectionTheory.Snapper.twistModulesAlong Finset.univ.toList L n F

noncomputable def AlgebraicGeometry.IntersectionTheory.Snapper.twistModulesAlongMapIso {X : Scheme} {ι : Type v} (indices : List ι) (L : ι → Scheme.Modules.Pic X) (n : NumericalPolynomial.Lattice ι) {F G : X.Modules} (e : F ≅ G) : twistModulesAlong indices L n F ≅ twistModulesAlong indices L n G

Twisting carries an isomorphism of the underlying module sheaves through every tensor factor.

Equations

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

noncomputable def AlgebraicGeometry.IntersectionTheory.Snapper.twistModulesMapIso {X : Scheme} {ι : Type v} [Fintype ι] [DecidableEq ι] (L : ι → Scheme.Modules.Pic X) (n : NumericalPolynomial.Lattice ι) {F G : X.Modules} (e : F ≅ G) : twistModules L n F ≅ twistModules L n G

Simultaneous twisting is functorial on isomorphisms.

Equations

• AlgebraicGeometry.IntersectionTheory.Snapper.twistModulesMapIso L n e = AlgebraicGeometry.IntersectionTheory.Snapper.twistModulesAlongMapIso Finset.univ.toList L n e

structure AlgebraicGeometry.IntersectionTheory.Snapper.CoherentTwistFamily {X : Scheme} {ι : Type v} [Fintype ι] [DecidableEq ι] (F : Coh X) (L : ι → Scheme.Modules.Pic X) : Prop

Coherence of every integer twist. This field isolates the current missing closure theorem for tensoring a finitely presented module sheaf by an invertible sheaf.

• coherent (n : NumericalPolynomial.Lattice ι) : Scheme.Modules.IsCoherent X (twistModules L n F.obj)

noncomputable def AlgebraicGeometry.IntersectionTheory.Snapper.CoherentTwistFamily.obj {X : Scheme} {ι : Type v} [Fintype ι] [DecidableEq ι] {F : Coh X} {L : ι → Scheme.Modules.Pic X} (T : CoherentTwistFamily F L) (n : NumericalPolynomial.Lattice ι) : Coh X

The coherent sheaf represented by the twist at exponent n.

Equations

• T.obj n = { obj := AlgebraicGeometry.IntersectionTheory.Snapper.twistModules L n F.obj, property := ⋯ }

noncomputable def AlgebraicGeometry.IntersectionTheory.Snapper.eulerFunction {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {ι : Type v} [Fintype ι] [DecidableEq ι] (D : Cohomology.FiniteCohomology k X) {F : Coh X} {L : ι → Scheme.Modules.Pic X} (T : CoherentTwistFamily F L) : NumericalPolynomial.NumericalFunction ι

Euler characteristic as a function on the full integer exponent lattice.

Equations

• AlgebraicGeometry.IntersectionTheory.Snapper.eulerFunction D T n = D.eulerCharacteristic (T.obj n)

Geometric induction certificate

structure AlgebraicGeometry.IntersectionTheory.Snapper.GeometricInduction {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {ι : Type v} [Fintype ι] [DecidableEq ι] (D : Cohomology.FiniteCohomology k X) {F : Coh X} {L : ι → Scheme.Modules.Pic X} (T : CoherentTwistFamily F L) (d : ℕ) : Type (max (u + 1) v)

The exact-sequence induction input in the classical proof of Snapper's theorem.

descended directions n is the sheaf obtained after the cuts in directions. A new cut v is exhibited by a short exact sequence

0 ⟶ descended directions n ⟶ descended directions (n + v) ⟶ descended (v :: directions) n ⟶ 0.

After d + 1 cuts the descended sheaf is zero.

• descended : List (NumericalPolynomial.Lattice ι) → NumericalPolynomial.Lattice ι → Coh X
• baseIso (n : NumericalPolynomial.Lattice ι) : self.descended [] n ≅ T.obj n
• step (_directions : List (NumericalPolynomial.Lattice ι)) (_v _n : NumericalPolynomial.Lattice ι) : CategoryTheory.ShortComplex (Coh X)
• stepShortExact (directions : List (NumericalPolynomial.Lattice ι)) (v n : NumericalPolynomial.Lattice ι) : (self.step directions v n).ShortExact
• stepX₁ (directions : List (NumericalPolynomial.Lattice ι)) (v n : NumericalPolynomial.Lattice ι) : (self.step directions v n).X₁ ≅ self.descended directions n
• stepX₂ (directions : List (NumericalPolynomial.Lattice ι)) (v n : NumericalPolynomial.Lattice ι) : (self.step directions v n).X₂ ≅ self.descended directions (n + v)
• stepX₃ (directions : List (NumericalPolynomial.Lattice ι)) (v n : NumericalPolynomial.Lattice ι) : (self.step directions v n).X₃ ≅ self.descended (v :: directions) n
• stepConnecting (directions : List (NumericalPolynomial.Lattice ι)) (v n : NumericalPolynomial.Lattice ι) : D.LinearConnectingMaps (self.step directions v n) ⋯
• terminalIsZero (directions : List (NumericalPolynomial.Lattice ι)) : directions.length = d + 1 → ∀ (n : NumericalPolynomial.Lattice ι), CategoryTheory.Limits.IsZero (self.descended directions n)

noncomputable def AlgebraicGeometry.IntersectionTheory.Snapper.GeometricInduction.descendedEuler {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {ι : Type v} [Fintype ι] [DecidableEq ι] {D : Cohomology.FiniteCohomology k X} {F : Coh X} {L : ι → Scheme.Modules.Pic X} {T : CoherentTwistFamily F L} {d : ℕ} (I : GeometricInduction D T d) (directions : List (NumericalPolynomial.Lattice ι)) : NumericalPolynomial.NumericalFunction ι

Euler characteristic of the family after a list of geometric cuts.

Equations

• I.descendedEuler directions n = D.eulerCharacteristic (I.descended directions n)

theorem AlgebraicGeometry.IntersectionTheory.Snapper.GeometricInduction.difference_descendedEuler {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {ι : Type v} [Fintype ι] [DecidableEq ι] {D : Cohomology.FiniteCohomology k X} {F : Coh X} {L : ι → Scheme.Modules.Pic X} {T : CoherentTwistFamily F L} {d : ℕ} (I : GeometricInduction D T d) (directions : List (NumericalPolynomial.Lattice ι)) (v : NumericalPolynomial.Lattice ι) : NumericalPolynomial.difference v (I.descendedEuler directions) = I.descendedEuler (v :: directions)

Euler additivity identifies one geometric cut with one forward difference.

theorem AlgebraicGeometry.IntersectionTheory.Snapper.GeometricInduction.mixedDifference_eulerFunction {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {ι : Type v} [Fintype ι] [DecidableEq ι] {D : Cohomology.FiniteCohomology k X} {F : Coh X} {L : ι → Scheme.Modules.Pic X} {T : CoherentTwistFamily F L} {d : ℕ} (I : GeometricInduction D T d) (directions : List (NumericalPolynomial.Lattice ι)) : NumericalPolynomial.mixedDifference directions (eulerFunction D T) = I.descendedEuler directions

Every mixed difference is the Euler characteristic of the corresponding descended family.

Snapper's theorem and its exposed difference coefficients

theorem AlgebraicGeometry.IntersectionTheory.Snapper.eulerCharacteristic_isZero {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : Cohomology.FiniteCohomology k X) (C : D.LinearConnectingSystem) {F : Coh X} (hF : CategoryTheory.Limits.IsZero F) : D.eulerCharacteristic F = 0

The zero coherent sheaf has Euler characteristic zero, using the same global choice of linear connecting maps required for all Euler-additivity arguments.

theorem AlgebraicGeometry.IntersectionTheory.Snapper.snapper {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {ι : Type v} [Fintype ι] [DecidableEq ι] (D : Cohomology.FiniteCohomology k X) (C : D.LinearConnectingSystem) {F : Coh X} {L : ι → Scheme.Modules.Pic X} (T : CoherentTwistFamily F L) (d : ℕ) (I : GeometricInduction D T d) : NumericalPolynomial.DegreeLE d (eulerFunction D T)

Snapper polynomiality. Euler characteristics of simultaneous integer line-bundle twists have total finite-difference degree at most d.

theorem AlgebraicGeometry.IntersectionTheory.Snapper.mixedDifference_eq_euler_descended {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {ι : Type v} [Fintype ι] [DecidableEq ι] {D : Cohomology.FiniteCohomology k X} {F : Coh X} {L : ι → Scheme.Modules.Pic X} {T : CoherentTwistFamily F L} {d : ℕ} (I : GeometricInduction D T d) (directions : List (NumericalPolynomial.Lattice ι)) (n : NumericalPolynomial.Lattice ι) : NumericalPolynomial.mixedDifference directions (eulerFunction D T) n = D.eulerCharacteristic (I.descended directions n)

The mixed-difference form needed by later intersection-theoretic constructions.

theorem AlgebraicGeometry.IntersectionTheory.Snapper.coefficient_eq_euler_descended {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {ι : Type v} [Fintype ι] [DecidableEq ι] {D : Cohomology.FiniteCohomology k X} {F : Coh X} {L : ι → Scheme.Modules.Pic X} {T : CoherentTwistFamily F L} {d : ℕ} (I : GeometricInduction D T d) (directions : List (NumericalPolynomial.Lattice ι)) : NumericalPolynomial.coefficient directions (eulerFunction D T) = D.eulerCharacteristic (I.descended directions 0)

A Newton coefficient is the Euler characteristic of the descended sheaf at the origin.

Invariance and one-variable specialization

theorem AlgebraicGeometry.IntersectionTheory.Snapper.eulerFunction_eq_of_coherentSheafIso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {ι : Type v} [Fintype ι] [DecidableEq ι] (D : Cohomology.FiniteCohomology k X) {F G : Coh X} (e : F ≅ G) {L : ι → Scheme.Modules.Pic X} (TF : CoherentTwistFamily F L) (TG : CoherentTwistFamily G L) : eulerFunction D TF = eulerFunction D TG

Euler-twist functions are invariant under isomorphism of the coherent base sheaf.

theorem AlgebraicGeometry.IntersectionTheory.Snapper.eulerFunction_eq_of_lineBundleIso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {ι : Type v} [Fintype ι] [DecidableEq ι] (D : Cohomology.FiniteCohomology k X) {F : Coh X} {L M : ι → Scheme.Modules.Pic X} (h : ∀ (i : ι), L i = M i) (TL : CoherentTwistFamily F L) (TM : CoherentTwistFamily F M) : eulerFunction D TL = eulerFunction D TM

Equality in Pic X is precisely line-bundle isomorphism class equality, so pointwise equal Picard classes give the same Euler-twist function.

noncomputable def AlgebraicGeometry.IntersectionTheory.Snapper.oneVariableEulerFunction {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : Cohomology.FiniteCohomology k X) {F : Coh X} (L : Scheme.Modules.Pic X) (T : CoherentTwistFamily F fun (x : Fin 1) => L) : ℤ → ℤ

The ordinary one-variable Euler function attached to powers of one Picard class.

Equations

• AlgebraicGeometry.IntersectionTheory.Snapper.oneVariableEulerFunction D L T n = AlgebraicGeometry.IntersectionTheory.Snapper.eulerFunction D T (NumericalPolynomial.oneVariablePoint n)

theorem AlgebraicGeometry.IntersectionTheory.Snapper.oneVariable_eulerFunction {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : Cohomology.FiniteCohomology k X) {F : Coh X} (L : Scheme.Modules.Pic X) (T : CoherentTwistFamily F fun (x : Fin 1) => L) : NumericalPolynomial.oneVariable (oneVariableEulerFunction D L T) = eulerFunction D T

theorem AlgebraicGeometry.IntersectionTheory.Snapper.oneVariable_fwdDiff_euler_vanishes {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (D : Cohomology.FiniteCohomology k X) (C : D.LinearConnectingSystem) {F : Coh X} (L : Scheme.Modules.Pic X) (T : CoherentTwistFamily F fun (x : Fin 1) => L) (d : ℕ) (I : GeometricInduction D T d) : (fwdDiff 1)^[d + 1] (oneVariableEulerFunction D L T) = 0

One-variable specialization: the (d + 1)st ordinary forward difference vanishes.