Documentation

DerivedAlgGeo.AlgebraicGeometry.Numerical.Mukai.SqrtTodd

The square root of a normalized graded class, and √td(X) #

For a graded class f with f 0 = 1, the square root is the family of components given by the coefficients of √(1 + x):

g 0 = 1,  g 1 = f₁/2,  g 2 = f₂/2 − f₁²/8,  g 3 = f₃/2 − f₁f₂/4 + f₁³/16,
g 4 = f₄/2 − f₁f₃/4 − f₂²/8 + 3f₁²f₂/16 − 5f₁⁴/128

What makes the name honest is sqrtComp_convolution: ∑_{j ≤ i} g_j·g_{i−j} = f_i. Nothing in the repository could write √td(X) before this; git grep sqrt over AlgebraicGeometry/** returned nothing, and Mathlib at the pin has no Chern or Todd theory at all.

The codimension-four ceiling is a limitation, and it is stated #

sqrtComp f i = 0 for i > 4, and sqrtComp_convolution carries an explicit i ≤ 4 hypothesis rather than hiding the bound behind a decide. This is the same ceiling and the same reason as Numerical/Core/CharacteristicClasses.lean, whose toddComponent stops at four: the expressions are written out, not recursed, so they stop where they were written.

Why the proof runs on one scalar #

Every coefficient is a power of 1/2 up to an integer factor — 1/4 = h², 1/8 = h³, 1/16 = h⁴, 3/16 = 3h⁴, 5/128 = 5h⁷ for h = algebraMap ℚ A (1/2). Rewriting them that way leaves one scalar atom, so the convolution becomes a polynomial identity in h and the f's modulo the single relation h + h = 1, and each case closes by linear_combination with an explicit cofactor.

The cofactors are not guesses: G = (2h − 1)·c was verified symbolically for each i before any of this was written. Writing the coefficients as distinct algebraMap values instead leaves ring with five unrelated atoms and no way to relate them, which is why the obvious simp; ring does not work here.

Main results #

The coefficients #

source
noncomputable def AlgebraicGeometry.Numerical.sqrtComp {A : Type u} [CommRing A] [Algebra ℚ A] (f : ℕ → A) :
ℕ → A

The square root of a graded class whose codimension-zero part is 1, component by component. Zero above codimension four; see the module docstring.

Equations
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Numerical.sqrtComp_zero {A : Type u} [CommRing A] [Algebra ℚ A] (f : ℕ → A) :
    sqrtComp f 0 = 1
    source
    theorem AlgebraicGeometry.Numerical.sqrtComp_one {A : Type u} [CommRing A] [Algebra ℚ A] (f : ℕ → A) :
    sqrtComp f 1 = (algebraMap ℚ A) (1 / 2) * f 1
    source
    @[simp]
    theorem AlgebraicGeometry.Numerical.sqrtComp_eq_zero_of_four_lt {A : Type u} [CommRing A] [Algebra ℚ A] (f : ℕ → A) {i : ℕ} (hi : 4 < i) :
    sqrtComp f i = 0

    The scalar relations #

    Each coefficient is a power of h = algebraMap ℚ A (1/2) up to an integer factor, which is what leaves the convolution with a single atom.

    The convolution #

    source
    theorem AlgebraicGeometry.Numerical.sqrtComp_convolution {A : Type u} [CommRing A] [Algebra ℚ A] (f : ℕ → A) (hf : f 0 = 1) {i : ℕ} (hi : i ≤ 4) :
    ∑ j ∈ Finset.range (i + 1), sqrtComp f j * sqrtComp f (i - j) = f i

    The identity that makes the name honest: ∑_{j ≤ i} g_j·g_{i−j} = f_i.

    Carries i ≤ 4 explicitly, because the coefficients stop there.

    The square root respects the grading #

    source
    theorem AlgebraicGeometry.Numerical.sqrtComp_mem {A : Type u} [CommRing A] [Algebra ℚ A] {n : ℕ} (R : NumericalRingData n A) (f : ℕ → A) (hf : ∀ (j : ℕ), f j ∈ R.piece j) (i : ℕ) :
    sqrtComp f i ∈ R.piece i

    If every f j sits in codimension j, so does every sqrtComp f i.

    √td(X) #

    source
    noncomputable def AlgebraicGeometry.Numerical.NumericalVarietyData.sqrtToddComp {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) :
    ℕ → A

    √td(X), component by component.

    Equations
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.Numerical.NumericalVarietyData.sqrtToddComp_zero {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) :
      V.sqrtToddComp 0 = 1
      source
      theorem AlgebraicGeometry.Numerical.NumericalVarietyData.sqrtToddComp_mem {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (i : ℕ) :
      V.sqrtToddComp i ∈ V.ring.piece i

      √td(X) respects the grading, from toddComp_mem.

      source
      theorem AlgebraicGeometry.Numerical.NumericalVarietyData.sqrtToddComp_convolution {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) {i : ℕ} (hi : i ≤ 4) :
      ∑ j ∈ Finset.range (i + 1), V.sqrtToddComp j * V.sqrtToddComp (i - j) = V.toddComp i

      √td(X) squares to td(X), in every codimension up to four.