Numerical Chern-character reconstruction from twist polynomials #
This file is the bounded, no-Chow reconstruction layer between Snapper polynomials and the
components consumed by NumericalVarietyData. There are two deliberately separate steps.
First, homogeneousPicardCoefficient extracts the ordinary rational homogeneous coefficient of
a Picard Euler polynomial. Raw finite differences below top degree are not sufficient: they
mix the desired term with higher-degree terms. We remove that mixing by interpolating the
scaled mixed coefficient and taking its lowest possible ordinary coefficient.
Second, PairingContext and ReconstructionData state exactly when those divisor-tested
functionals are represented by elements of a chosen NumericalRingData. Representability gives
existence; divisorPairing_ext gives uniqueness. Neither is inferred from the intersection
numbers. In particular, on a higher-dimensional variety products of divisors need not separate
all middle-codimension numerical classes.
The represented Todd-weighted components are denoted tauComponent. The structure-sheaf
components supply the reconstructed Todd class, and Chern-character components are recovered by
the triangular identities
tau_i(F) = sum_{a+b=i} ch_a(F) * td_b(X).
The formulas are implemented through codimension four, the current bound of
AlgebraicGeometry/Numerical/Core/CharacteristicClasses.lean. Isomorphism and
exact-sequence results use explicit
rank and Euler-polynomial comparisons. The line-bundle theorem uses an explicit coefficient
comparison rather than silently assuming a perfect intersection pairing or Riemann--Roch.
Rational homogeneous coefficients #
noncomputable def
AlgebraicGeometry.IntersectionTheory.ChernCharacter.scaledPicardCoefficient
{X : Scheme}
(classes : List (Scheme.Modules.Pic X))
(f : Scheme.Modules.Pic X → ℤ)
(z : ℤ)
:
Scale every Picard direction by the same integer and take the resulting mixed coefficient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
AlgebraicGeometry.IntersectionTheory.ChernCharacter.interpolatingPolynomial
(d : ℕ)
(q : ℤ → ℤ)
:
The degree-d rational interpolation of an integer-valued function, using the nodes
0, ..., d.
Equations
- AlgebraicGeometry.IntersectionTheory.ChernCharacter.interpolatingPolynomial d q = (Lagrange.interpolate (Finset.range (d + 1)) fun (j : ℕ) => ↑j) fun (j : ℕ) => ↑(q ↑j)
Instances For
noncomputable def
AlgebraicGeometry.IntersectionTheory.ChernCharacter.homogeneousPicardCoefficient
{X : Scheme}
(d : ℕ)
(classes : List (Scheme.Modules.Pic X))
(f : Scheme.Modules.Pic X → ℤ)
:
The ordinary homogeneous coefficient polarized in classes.
For r = classes.length, this is the coefficient of z^r in the degree-d interpolation of
z ↦ Δ_{L₁^z}⋯Δ_{Lᵣ^z} f(1). In top degree it agrees with the usual top mixed
coefficient; below top degree it removes the higher-degree contamination present in a raw
finite difference.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.picardMixedDifference_add
{X : Scheme}
(classes : List (Scheme.Modules.Pic X))
(f g : Scheme.Modules.Pic X → ℤ)
:
Number.picardMixedDifference classes (f + g) = Number.picardMixedDifference classes f + Number.picardMixedDifference classes g
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.picardCoefficient_add
{X : Scheme}
(classes : List (Scheme.Modules.Pic X))
(f g : Scheme.Modules.Pic X → ℤ)
:
Number.picardCoefficient classes (f + g) = Number.picardCoefficient classes f + Number.picardCoefficient classes g
@[simp]
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.scaledPicardCoefficient_add
{X : Scheme}
(classes : List (Scheme.Modules.Pic X))
(f g : Scheme.Modules.Pic X → ℤ)
:
scaledPicardCoefficient classes (f + g) = scaledPicardCoefficient classes f + scaledPicardCoefficient classes g
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.interpolatingPolynomial_add
(d : ℕ)
(q r : ℤ → ℤ)
:
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.homogeneousPicardCoefficient_add
{X : Scheme}
(d : ℕ)
(classes : List (Scheme.Modules.Pic X))
(f g : Scheme.Modules.Pic X → ℤ)
:
homogeneousPicardCoefficient d classes (f + g) = homogeneousPicardCoefficient d classes f + homogeneousPicardCoefficient d classes g
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.scaledPicardCoefficient_eq_of_perm
{X : Scheme}
{classes classes' : List (Scheme.Modules.Pic X)}
(h : classes.Perm classes')
(f : Scheme.Modules.Pic X → ℤ)
:
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.homogeneousPicardCoefficient_eq_of_perm
{X : Scheme}
{classes classes' : List (Scheme.Modules.Pic X)}
(h : classes.Perm classes')
(d : ℕ)
(f : Scheme.Modules.Pic X → ℤ)
:
Homogeneous coefficients are symmetric in their Picard directions.
Explicit realization in a numerical ring #
noncomputable def
AlgebraicGeometry.IntersectionTheory.ChernCharacter.divisorProduct
{X : Scheme}
{A : Type v}
[CommRing A]
(divisorClass : Additive (Scheme.Modules.Pic X) →+ A)
(classes : List (Scheme.Modules.Pic X))
:
A
The product of the degree-one realizations of a list of Picard classes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.divisorProduct_nil
{X : Scheme}
{A : Type v}
[CommRing A]
(divisorClass : Additive (Scheme.Modules.Pic X) →+ A)
:
structure
AlgebraicGeometry.IntersectionTheory.ChernCharacter.PairingContext
{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 : ℕ)
(A : Type v)
[CommRing A]
[Algebra ℚ A]
:
Type (max (u + 1) v)
A chosen numerical ring realization of the divisor intersection theory.
divisorPairing_ext is the required nondegeneracy statement: divisor products separate the
chosen graded pieces. It is intentionally a field rather than an instance or theorem.
- ring : Numerical.NumericalRingData d A
The selected numerical-ring presentation.
- intersection : Number.IntersectionContext D C d
- degree_divisorProduct (L : Fin d → Scheme.Modules.Pic X) : self.ring.degree (divisorProduct self.divisorClass (List.ofFn L)) = ↑(self.intersection.picardIntersectionNumber L)
- divisorPairing_ext (i : ℕ) : i ≤ d → ∀ {x y : A}, x ∈ self.ring.piece i → y ∈ self.ring.piece i → (∀ (classes : List (Scheme.Modules.Pic X)), classes.length = d - i → self.ring.degree (x * divisorProduct self.divisorClass classes) = self.ring.degree (y * divisorProduct self.divisorClass classes)) → x = y
Instances For
noncomputable def
AlgebraicGeometry.IntersectionTheory.ChernCharacter.PairingContext.twistPairing
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsVariety k X]
{D : Cohomology.FiniteCohomology k X}
{d : ℕ}
{F : Coh X}
(T : Number.TwistContext D F d)
(_i : ℕ)
(classes : List (Scheme.Modules.Pic X))
:
The divisor-tested rational functional extracted from a coherent sheaf's twist polynomial.
Equations
Instances For
structure
AlgebraicGeometry.IntersectionTheory.ChernCharacter.PairingContext.ReconstructionData
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
(P : PairingContext D C d A)
(F : Coh X)
:
Type (u + 1)
Existence data for representatives of all Todd-weighted components of one coherent sheaf.
This is separate from PairingContext.divisorPairing_ext: existence and uniqueness are distinct
hypotheses.
- twists : Number.TwistContext D F d
- rank : ℤ
- representable (i : ℕ) : i ≤ d → ∃ x ∈ P.ring.piece i, ∀ (classes : List (Scheme.Modules.Pic X)), classes.length = d - i → P.ring.degree (x * divisorProduct P.divisorClass classes) = twistPairing self.twists i classes
Instances For
noncomputable def
AlgebraicGeometry.IntersectionTheory.ChernCharacter.PairingContext.ReconstructionData.tauComponent
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{F : Coh X}
(R : P.ReconstructionData F)
(i : ℕ)
:
A
The unique chosen representative of the Todd-weighted component tau_i(F) when i ≤ d,
and zero above the dimension.
Equations
- R.tauComponent i = if hi : i ≤ d then Classical.choose ⋯ else 0
Instances For
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.PairingContext.ReconstructionData.tauComponent_mem
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{F : Coh X}
(R : P.ReconstructionData F)
(i : ℕ)
:
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.PairingContext.ReconstructionData.degree_tauComponent_mul_divisorProduct
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{F : Coh X}
(R : P.ReconstructionData F)
(i : ℕ)
(hi : i ≤ d)
(classes : List (Scheme.Modules.Pic X))
(hlength : classes.length = d - i)
:
P.ring.degree (R.tauComponent i * divisorProduct P.divisorClass classes) = twistPairing R.twists i classes
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.PairingContext.ReconstructionData.tauComponent_eq_of_twistPairing_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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{F G : Coh X}
(R : P.ReconstructionData F)
(S : P.ReconstructionData G)
(i : ℕ)
(hpair :
∀ (classes : List (Scheme.Modules.Pic X)),
classes.length = d - i → twistPairing R.twists i classes = twistPairing S.twists i classes)
:
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.PairingContext.ReconstructionData.tauComponent_eq_of_eulerPic_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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{F G : Coh X}
(R : P.ReconstructionData F)
(S : P.ReconstructionData G)
(h : R.twists.eulerPic = S.twists.eulerPic)
(i : ℕ)
:
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.PairingContext.ReconstructionData.tauComponent_add
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{F G H : Coh X}
(R : P.ReconstructionData F)
(S : P.ReconstructionData G)
(Q : P.ReconstructionData H)
(heuler : Q.twists.eulerPic = R.twists.eulerPic + S.twists.eulerPic)
(i : ℕ)
:
Todd normalization and Chern-character components through degree four #
noncomputable def
AlgebraicGeometry.IntersectionTheory.ChernCharacter.toddComponent
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(i : ℕ)
:
A
The reconstructed Todd component is the Todd-weighted component of the structure sheaf.
Equations
Instances For
@[irreducible]
noncomputable def
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
:
ℕ → A
Chern-character components recovered from tau(F) = ch(F) * td(X), through degree four.
Equations
- One or more equations did not get rendered due to their size.
- AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent RO R 0 = (algebraMap ℚ A) ↑R.rank
- AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent RO R x✝ = 0
Instances For
@[simp]
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_zero
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
:
@[simp]
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
:
@[simp]
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_two
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
:
chernCharacterComponent RO R 2 = R.tauComponent 2 - chernCharacterComponent RO R 1 * toddComponent RO 1 - (algebraMap ℚ A) ↑R.rank * toddComponent RO 2
@[simp]
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_three
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
:
chernCharacterComponent RO R 3 = R.tauComponent 3 - chernCharacterComponent RO R 2 * toddComponent RO 1 - chernCharacterComponent RO R 1 * toddComponent RO 2 - (algebraMap ℚ A) ↑R.rank * toddComponent RO 3
@[simp]
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_four
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
:
chernCharacterComponent RO R 4 = R.tauComponent 4 - chernCharacterComponent RO R 3 * toddComponent RO 1 - chernCharacterComponent RO R 2 * toddComponent RO 2 - chernCharacterComponent RO R 1 * toddComponent RO 3 - (algebraMap ℚ A) ↑R.rank * toddComponent RO 4
@[simp]
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_of_five_le
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
{i : ℕ}
(hi : 5 ≤ i)
:
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_mem
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
(i : ℕ)
:
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_eq_zero_of_dimension_lt
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
{i : ℕ}
(hi : d < i)
:
The triangular extraction principle #
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.tauComponent_one_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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
:
R.tauComponent 1 = chernCharacterComponent RO R 1 + chernCharacterComponent RO R 0 * toddComponent RO 1
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.tauComponent_two_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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
:
R.tauComponent 2 = chernCharacterComponent RO R 2 + chernCharacterComponent RO R 1 * toddComponent RO 1 + chernCharacterComponent RO R 0 * toddComponent RO 2
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.tauComponent_three_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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
:
R.tauComponent 3 = chernCharacterComponent RO R 3 + chernCharacterComponent RO R 2 * toddComponent RO 1 + chernCharacterComponent RO R 1 * toddComponent RO 2 + chernCharacterComponent RO R 0 * toddComponent RO 3
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.tauComponent_four_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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
:
R.tauComponent 4 = chernCharacterComponent RO R 4 + chernCharacterComponent RO R 3 * toddComponent RO 1 + chernCharacterComponent RO R 2 * toddComponent RO 2 + chernCharacterComponent RO R 1 * toddComponent RO 3 + chernCharacterComponent RO R 0 * toddComponent RO 4
Invariance and exact-sequence additivity #
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_eq_of_eulerPic_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}
{d : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F G : Coh X}
(R : P.ReconstructionData F)
(S : P.ReconstructionData G)
(hrank : R.rank = S.rank)
(heuler : R.twists.eulerPic = S.twists.eulerPic)
(i : ℕ)
:
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_iso
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F G : Coh X}
(R : P.ReconstructionData F)
(S : P.ReconstructionData G)
(_e : F ≅ G)
(hrank : R.rank = S.rank)
(heuler : R.twists.eulerPic = S.twists.eulerPic)
(i : ℕ)
:
Isomorphism invariance once the chosen rank and twist-polynomial realizations have been
compared. The comparison hypotheses stay explicit because a bare coherent-sheaf isomorphism
does not choose compatible ReconstructionData.
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_add
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F G H : Coh X}
(R : P.ReconstructionData F)
(S : P.ReconstructionData G)
(Q : P.ReconstructionData H)
(hrank : Q.rank = R.rank + S.rank)
(heuler : Q.twists.eulerPic = R.twists.eulerPic + S.twists.eulerPic)
(i : ℕ)
:
Explicit line-bundle comparison #
noncomputable def
AlgebraicGeometry.IntersectionTheory.ChernCharacter.expComponent
{A : Type v}
[CommRing A]
[Algebra ℚ A]
(x : A)
(i : ℕ)
:
A
The degree-i exponential term D^i / i!.
Equations
- AlgebraicGeometry.IntersectionTheory.ChernCharacter.expComponent x i = (algebraMap ℚ A) (↑i.factorial)⁻¹ * x ^ i
Instances For
noncomputable def
AlgebraicGeometry.IntersectionTheory.ChernCharacter.lineTauCandidate
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
(x : A)
(i : ℕ)
:
A
The expected Todd-weighted component of a line bundle with first Chern class x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
AlgebraicGeometry.IntersectionTheory.ChernCharacter.LineBundleComparison
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
(L : Scheme.Modules.Pic X)
:
Coefficient-level comparison identifying one reconstruction with a line bundle.
This is the precise missing translation/representability input. It is stated on the extracted twist coefficients, not as the desired Chern-character equality.
- candidate_mem (i : ℕ) : i ≤ d → i ≤ 4 → lineTauCandidate RO (P.divisorClass (Additive.ofMul L)) i ∈ P.ring.piece i
- coefficient_formula (i : ℕ) : i ≤ d → i ≤ 4 → ∀ (classes : List (Scheme.Modules.Pic X)), classes.length = d - i → PairingContext.twistPairing R.twists i classes = P.ring.degree (lineTauCandidate RO (P.divisorClass (Additive.ofMul L)) i * divisorProduct P.divisorClass classes)
Instances For
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.tauComponent_eq_lineTauCandidate
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
(L : Scheme.Modules.Pic X)
(Q : LineBundleComparison RO R L)
(i : ℕ)
(hi : i ≤ d)
(hi4 : i ≤ 4)
:
The line-bundle coefficient comparison determines the represented Todd-weighted component.
The conclusion uses both the stated representability and the explicit divisor-pairing
nondegeneracy from PairingContext.
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.chernCharacterComponent_lineBundle
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
(L : Scheme.Modules.Pic X)
(Q : LineBundleComparison RO R L)
(htoddZero : toddComponent RO 0 = 1)
(i : ℕ)
(hi : i ≤ d)
(hi4 : i ≤ 4)
:
Under the visible normalization td₀ = 1, the reconstructed Chern character of a line
bundle is exp(c₁) through the supported degree four.
Compatibility with the degree-level surface construction #
theorem
AlgebraicGeometry.IntersectionTheory.ChernCharacter.degree_chernCharacterComponent_two_eq_surface
{k : Type u}
[Field k]
{X : Scheme}
[X.Over (Spec (CommRingCat.of k))]
[IsVariety k X]
{D : Cohomology.FiniteCohomology k X}
{C : D.LinearConnectingSystem}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
(P : PairingContext D C 2 A)
{O F : Coh X}
(RO : P.ReconstructionData O)
(R : P.ReconstructionData F)
(Qdet : F.TwoTermPerfectDeterminantData)
(hrank : R.rank = ChernCharacterSurface.virtualRank Qdet)
(htauTop : P.ring.degree (R.tauComponent 2) = ↑(D.eulerCharacteristic F))
(hfirst : chernCharacterComponent RO R 1 = P.divisorClass (ChernCharacterSurface.picardFirstChernClass Qdet))
(htoddOne :
P.ring.degree (P.divisorClass (ChernCharacterSurface.picardFirstChernClass Qdet) * toddComponent RO 1) = (ChernCharacterSurface.toddOnePairing P.intersection) (ChernCharacterSurface.picardFirstChernClass Qdet))
(htoddTop : P.ring.degree (toddComponent RO 2) = ChernCharacterSurface.toddTwoDegree P.intersection)
:
P.ring.degree (chernCharacterComponent RO R 2) = ChernCharacterSurface.chernCharacterTwoDegree P.intersection Qdet
The reconstructed ring-valued ch₂ has the degree constructed in issue #37 once the
chosen rank, determinant class, and Todd-weighted representatives are explicitly compared.
This does not turn the degree-level surface class into an unconditional element of A.
Compatibility with the universal A7 formulas #
noncomputable def
AlgebraicGeometry.IntersectionTheory.ChernCharacter.toChernClassData
{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 : ℕ}
{A : Type v}
[CommRing A]
[Algebra ℚ A]
{P : PairingContext D C d A}
{O : Coh X}
(RO : P.ReconstructionData O)
{F : Coh X}
(R : P.ReconstructionData F)
:
Recover Chern classes whose universal formulas give the reconstructed character through codimension four.
Equations
- One or more equations did not get rendered due to their size.