The point, as a consistency witness for Layer A

NumericalVarietyData is an explicit presentation of the graded structure, characteristic data, and Euler characteristic. Its compatibility matters only if the separately stated SatisfiesHRR property has a model.

This file supplies one: a point, in dimension zero. A^•(pt)_ℚ = ℚ concentrated in codimension zero, N(pt) = ℤ, ch(E) = rank E, td(pt) = 1, and Riemann–Roch degenerates to χ(E) = rank E.

It is a witness, not a working example: nothing interesting is true in dimension zero. The K3 presentation is the first positive-dimensional model in which Riemann--Roch has content.

def AlgebraicGeometry.Numerical.Examples.pointPiece : ℕ → Submodule ℚ ℚ

The graded pieces of A^•(pt)_ℚ: everything sits in codimension zero.

Equations

• AlgebraicGeometry.Numerical.Examples.pointPiece i = if i = 0 then ⊤ else ⊥

theorem AlgebraicGeometry.Numerical.Examples.pointPiece_zero : pointPiece 0 = ⊤

theorem AlgebraicGeometry.Numerical.Examples.pointPiece_eq_bot {i : ℕ} (hi : i ≠ 0) : pointPiece i = ⊥

theorem AlgebraicGeometry.Numerical.Examples.pointPiece_isInternal : DirectSum.IsInternal pointPiece

noncomputable def AlgebraicGeometry.Numerical.Examples.pointNumericalRing : NumericalRingData 0 ℚ

A^•(pt)_ℚ = ℚ, in dimension zero.

Equations

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

def AlgebraicGeometry.Numerical.Examples.pointCh (E : ℤ) : ℕ → ℚ

The Chern character on a point: ch₀(E) = rank E, and nothing above.

Equations

• AlgebraicGeometry.Numerical.Examples.pointCh E i = if i = 0 then ↑E else 0

def AlgebraicGeometry.Numerical.Examples.pointTodd : ℕ → ℚ

The Todd class of a point: td₀ = 1, and nothing above.

Equations

• AlgebraicGeometry.Numerical.Examples.pointTodd i = if i = 0 then 1 else 0

theorem AlgebraicGeometry.Numerical.Examples.pointCh_mem (E : ℤ) (i : ℕ) : pointCh E i ∈ pointPiece i

theorem AlgebraicGeometry.Numerical.Examples.pointTodd_mem (i : ℕ) : pointTodd i ∈ pointPiece i

noncomputable def AlgebraicGeometry.Numerical.Examples.pointNumericalVariety : NumericalVarietyData 0 ℚ ℤ

N(pt) = ℤ, with ch = rank and td = 1. Riemann–Roch reads χ(E) = rank E.

Equations

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

theorem AlgebraicGeometry.Numerical.Examples.pointNumericalVariety_satisfiesHRR : pointNumericalVariety.SatisfiesHRR

Riemann--Roch for the explicit point presentation.