Realizing a geometric variety numerically #
Variety.NumericalData is the first explicit bridge from the geometric half of DerivedAlgGeo to
the numerical half. Its source is a genuine a variety over k and coherent sheaves on its underlying
scheme. Its target is a numerical intersection ring A, a numerical Grothendieck group N,
and ultimately a NumericalVarietyData n A N.
The important direction of construction is encoded in the fields:
- coherent sheaves map to numerical classes, invariant under isomorphism and additive in short exact sequences;
- Chern classes are primary data;
chCompis computed from those Chern classes by the universal formulas inAlgebraicGeometry/Numerical/Core/CharacteristicClasses.lean;toddCompis computed from the Chern classes of the tangent bundle;- geometric Chern classes and Euler characteristics agree with their numerical descendants.
The remaining hard mathematics is visible rather than hidden. A realization must still prove gradedness, additivity of the computed Chern character, and Hirzebruch--Riemann--Roch. Those proofs will be supplied by the future geometric Chern-class and Riemann--Roch developments.
The current characteristic-class API is complete through codimension four, so this first
constructor records n ≤ 4. Extending the universal power-series implementation removes that
bound without changing the realization structure conceptually.
Certified data exhibiting how a geometric variety descends to a numerical variety.
NumericalRingData n A is an input because constructing the numerical intersection ring is a
separate geometric task. This structure then derives the numerical Chern character and Todd
components from Chern-class data and packages all compatibility obligations needed for
NumericalVarietyData.
- ring : Numerical.NumericalRingData n A
The selected numerical intersection-ring presentation.
The component formulas currently supplied cover every codimension of
X.The numerical class, as a hom out of the Grothendieck group of
Coh X.This was a function together with
classOf_isoandclassOf_shortExact. Those two laws say exactly that the function factors throughK₀Ab, so they are not data: they areK₀Ab.of_isoandK₀Ab.of_shortExactcomposed with this hom, and they survive as theorems of the same names and argument shapes below.Rank on the numerical Grothendieck group.
- chernClasses : N → Numerical.ChernClassData A
Chern classes of a numerical class.
The rank stored with the Chern classes agrees with numerical rank.
- coherentChernClasses : Coh X → Numerical.ChernClassData A
Chern classes constructed geometrically for coherent sheaves.
- coherentChernClasses_classOf (F : Coh X) : self.chernClasses (self.classOfHom (CategoryTheory.K₀Ab.of F)) = self.coherentChernClasses F
Geometric Chern classes descend through the numerical class map.
- chernCharacter_mem (E : N) (i : ℕ) : (self.chernClasses E).chernCharacterComponent i ∈ self.ring.piece i
The universally computed Chern-character components have the expected grading.
- chernCharacter_add (E F : N) (i : ℕ) : (self.chernClasses (E + F)).chernCharacterComponent i = (self.chernClasses E).chernCharacterComponent i + (self.chernClasses F).chernCharacterComponent i
The universally computed Chern character is additive on numerical classes.
- tangentChernClasses : Numerical.ChernClassData A
Chern classes of the tangent bundle, used to compute the Todd class.
The universally computed Todd components have the expected grading.
Euler characteristic on numerical classes.
- finiteCohomology : Cohomology.FiniteCohomology k X
Finite-dimensional derived cohomology from which the geometric Euler characteristic is constructed.
- coherentEulerCharacteristic_classOf (F : Coh X) : self.chi (self.classOfHom (CategoryTheory.K₀Ab.of F)) = self.finiteCohomology.eulerCharacteristic F
The cohomological Euler characteristic descends through the numerical class map.
Instances For
Hirzebruch--Riemann--Roch as a property of geometric numerical data, kept separate from the selected realization.
- eq (E : N) : ↑(D.chi E) = D.ring.degree ((∑ i ∈ Finset.range (n + 1), (D.chernClasses E).chernCharacterComponent i) * ∑ j ∈ Finset.range (n + 1), D.tangentChernClasses.toddComponent j)
Instances For
The geometric Euler characteristic used by a numerical realization, constructed from its finite-dimensional derived cohomology.
Equations
Instances For
Construct the numerical variety certified by geometric NumericalData.
Unlike the original direct model definitions, the Chern-character and Todd components are not independent fields here: they are definitionally the universal expressions in the supplied Chern classes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A geometric HRR proof induces the proposition-valued numerical HRR witness.
The second Chern-character component produced by a realization.
The third Chern-character component produced by a realization.
The fourth Chern-character component produced by a realization.
The second Todd component produced from the tangent Chern classes.
The third Todd component produced from the tangent Chern classes.
The fourth Todd component produced from the tangent Chern classes.
The numerical class of a coherent sheaf.
Equations
- D.classOf F = D.classOfHom (CategoryTheory.K₀Ab.of F)
Instances For
The two formal laws, now theorems #
classOf_iso and classOf_shortExact were fields. They are K₀Ab.of_iso and
K₀Ab.of_shortExact composed with classOfHom, so they are proved here and the
names and argument shapes are unchanged.
The numerical Chern character of a coherent sheaf is computed from its geometric Chern classes.
Numerical and geometric Euler characteristics agree on coherent sheaves.
Geometric Chern-character components are invariant under isomorphism of coherent sheaves.
Geometric Chern-character components are additive in short exact sequences. This is the characteristic-class form of descent through the numerical Grothendieck group.
Geometric Euler characteristic is invariant under isomorphism of coherent sheaves.
Geometric Euler characteristic is additive in short exact sequences.