Universal characteristic-class formulas

The Chern character and Todd class do not have separate definitions for surfaces, threefolds, and fourfolds. They are universal power-series expressions; dimension only says where the series truncates in a particular numerical ring.

This module records the components through codimension four, the range currently used by the project. ChernClassData A is deliberately just algebraic input. The geometric construction of these classes for coherent sheaves and tangent bundles, and the proof that the resulting formulas agree with NumericalVarietyData.chComp and toddComp, belong to the future geometric-to-numerical realization layer.

structure AlgebraicGeometry.Numerical.ChernClassData (A : Type u) : Type u

Rank and Chern-class components in a commutative coefficient ring.

No dimension is stored here: a NumericalRingData n A determines which components vanish after these universal formulas have been evaluated.

• rank : ℤ

  The virtual rank.

• c : ℕ → A

  The Chern classes, with positive indices carrying the mathematical content.

noncomputable def AlgebraicGeometry.Numerical.ChernClassData.chernCharacterZero {A : Type u} [CommRing A] [Algebra ℚ A] (C : ChernClassData A) : A

ch₀ = rank.

Equations

• C.chernCharacterZero = (algebraMap ℚ A) ↑C.rank

def AlgebraicGeometry.Numerical.ChernClassData.chernCharacterOne {A : Type u} (C : ChernClassData A) : A

ch₁ = c₁.

Equations

• C.chernCharacterOne = C.c 1

noncomputable def AlgebraicGeometry.Numerical.ChernClassData.chernCharacterTwo {A : Type u} [CommRing A] [Algebra ℚ A] (C : ChernClassData A) : A

ch₂ = (c₁² - 2c₂) / 2.

Equations

• C.chernCharacterTwo = (algebraMap ℚ A) (1 / 2) * (C.c 1 ^ 2 - 2 * C.c 2)

noncomputable def AlgebraicGeometry.Numerical.ChernClassData.chernCharacterThree {A : Type u} [CommRing A] [Algebra ℚ A] (C : ChernClassData A) : A

ch₃ = (c₁³ - 3c₁c₂ + 3c₃) / 6.

Equations

• C.chernCharacterThree = (algebraMap ℚ A) (1 / 6) * (C.c 1 ^ 3 - 3 * C.c 1 * C.c 2 + 3 * C.c 3)

noncomputable def AlgebraicGeometry.Numerical.ChernClassData.chernCharacterFour {A : Type u} [CommRing A] [Algebra ℚ A] (C : ChernClassData A) : A

ch₄ = (c₁⁴ - 4c₁²c₂ + 2c₂² + 4c₁c₃ - 4c₄) / 24.

Equations

• C.chernCharacterFour = (algebraMap ℚ A) (1 / 24) * (C.c 1 ^ 4 - 4 * C.c 1 ^ 2 * C.c 2 + 2 * C.c 2 ^ 2 + 4 * C.c 1 * C.c 3 - 4 * C.c 4)

noncomputable def AlgebraicGeometry.Numerical.ChernClassData.chernCharacterComponent {A : Type u} [CommRing A] [Algebra ℚ A] (C : ChernClassData A) : ℕ → A

The Chern-character component selected from the universal formulas through codimension four. Components above four are zero because this is the bounded realization API currently supported by DerivedAlgGeo; Variety.NumericalData records the corresponding hypothesis n ≤ 4.

Equations

• C.chernCharacterComponent 0 = C.chernCharacterZero
• C.chernCharacterComponent 1 = C.chernCharacterOne
• C.chernCharacterComponent 2 = C.chernCharacterTwo
• C.chernCharacterComponent 3 = C.chernCharacterThree
• C.chernCharacterComponent 4 = C.chernCharacterFour
• C.chernCharacterComponent x✝ = 0

@[simp]

theorem AlgebraicGeometry.Numerical.ChernClassData.chernCharacterComponent_zero {A : Type u} [CommRing A] [Algebra ℚ A] (C : ChernClassData A) : C.chernCharacterComponent 0 = (algebraMap ℚ A) ↑C.rank

@[simp]

theorem AlgebraicGeometry.Numerical.ChernClassData.chernCharacterComponent_one {A : Type u} [CommRing A] [Algebra ℚ A] (C : ChernClassData A) : C.chernCharacterComponent 1 = C.c 1

@[simp]

theorem AlgebraicGeometry.Numerical.ChernClassData.chernCharacterComponent_two {A : Type u} [CommRing A] [Algebra ℚ A] (C : ChernClassData A) : C.chernCharacterComponent 2 = C.chernCharacterTwo

@[simp]

theorem AlgebraicGeometry.Numerical.ChernClassData.chernCharacterComponent_three {A : Type u} [CommRing A] [Algebra ℚ A] (C : ChernClassData A) : C.chernCharacterComponent 3 = C.chernCharacterThree

@[simp]

theorem AlgebraicGeometry.Numerical.ChernClassData.chernCharacterComponent_four {A : Type u} [CommRing A] [Algebra ℚ A] (C : ChernClassData A) : C.chernCharacterComponent 4 = C.chernCharacterFour

def AlgebraicGeometry.Numerical.ChernClassData.toddZero {A : Type u} [CommRing A] : A

td₀ = 1.

Equations

• AlgebraicGeometry.Numerical.ChernClassData.toddZero = 1

noncomputable def AlgebraicGeometry.Numerical.ChernClassData.toddOne {A : Type u} [CommRing A] [Algebra ℚ A] (T : ChernClassData A) : A

td₁ = c₁ / 2.

Equations

• T.toddOne = (algebraMap ℚ A) (1 / 2) * T.c 1

noncomputable def AlgebraicGeometry.Numerical.ChernClassData.toddTwo {A : Type u} [CommRing A] [Algebra ℚ A] (T : ChernClassData A) : A

td₂ = (c₁² + c₂) / 12.

Equations

• T.toddTwo = (algebraMap ℚ A) (1 / 12) * (T.c 1 ^ 2 + T.c 2)

noncomputable def AlgebraicGeometry.Numerical.ChernClassData.toddThree {A : Type u} [CommRing A] [Algebra ℚ A] (T : ChernClassData A) : A

td₃ = c₁c₂ / 24.

Equations

• T.toddThree = (algebraMap ℚ A) (1 / 24) * (T.c 1 * T.c 2)

noncomputable def AlgebraicGeometry.Numerical.ChernClassData.toddFour {A : Type u} [CommRing A] [Algebra ℚ A] (T : ChernClassData A) : A

td₄ = (-c₁⁴ + 4c₁²c₂ + 3c₂² + c₁c₃ - c₄) / 720.

Equations

• T.toddFour = (algebraMap ℚ A) (1 / 720) * (-T.c 1 ^ 4 + 4 * T.c 1 ^ 2 * T.c 2 + 3 * T.c 2 ^ 2 + T.c 1 * T.c 3 - T.c 4)

noncomputable def AlgebraicGeometry.Numerical.ChernClassData.toddComponent {A : Type u} [CommRing A] [Algebra ℚ A] (T : ChernClassData A) : ℕ → A

The Todd component selected from the universal formulas through codimension four.

Equations

• T.toddComponent 0 = AlgebraicGeometry.Numerical.ChernClassData.toddZero
• T.toddComponent 1 = T.toddOne
• T.toddComponent 2 = T.toddTwo
• T.toddComponent 3 = T.toddThree
• T.toddComponent 4 = T.toddFour
• T.toddComponent x✝ = 0

@[simp]

theorem AlgebraicGeometry.Numerical.ChernClassData.toddComponent_zero {A : Type u} [CommRing A] [Algebra ℚ A] (T : ChernClassData A) : T.toddComponent 0 = 1

@[simp]

theorem AlgebraicGeometry.Numerical.ChernClassData.toddComponent_one {A : Type u} [CommRing A] [Algebra ℚ A] (T : ChernClassData A) : T.toddComponent 1 = T.toddOne

@[simp]

theorem AlgebraicGeometry.Numerical.ChernClassData.toddComponent_two {A : Type u} [CommRing A] [Algebra ℚ A] (T : ChernClassData A) : T.toddComponent 2 = T.toddTwo

@[simp]

theorem AlgebraicGeometry.Numerical.ChernClassData.toddComponent_three {A : Type u} [CommRing A] [Algebra ℚ A] (T : ChernClassData A) : T.toddComponent 3 = T.toddThree

@[simp]

theorem AlgebraicGeometry.Numerical.ChernClassData.toddComponent_four {A : Type u} [CommRing A] [Algebra ℚ A] (T : ChernClassData A) : T.toddComponent 4 = T.toddFour