Documentation

TauCeti.Geometry.Hodge.Zero

The zero polarizable Hodge structure #

The zero lattice carries a unique Hodge structure of any weight, and the zero bilinear form polarizes it: the Hodge–Riemann positivity is a condition on nonzero vectors of the Hodge components, of which there are none. So the zero object exists in the category of polarizable rational Hodge structures of a fixed weight, which is what makes the empty direct sum available alongside the binary ones.

Main declarations #

References #

Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1.2; Peters--Steenbrink, Mixed Hodge Structures, §2.

The zero-carrier and zero-object constructions follow TauCeti.Geometry.Hodge.Mixed.Zero.

source
noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.zero (n : ℤ) :
PolarizableHodgeStructureCat n

The zero polarizable Hodge structure of weight n, on the zero lattice.

Instances For
    source
    theorem TauCeti.Hodge.PolarizableHodgeStructureCat.isZero_of_subsingleton_ratCarrier {n : ℤ} (X : PolarizableHodgeStructureCat n) [Subsingleton X.ratCarrier] :
    CategoryTheory.Limits.IsZero X

    A polarizable Hodge structure with subsingleton rational carrier is a zero object.

    Morphisms are determined by their rational linear maps, so the rational carrier alone detects the zero object; no separate hypothesis on the complex carrier is needed.

    source
    theorem TauCeti.Hodge.PolarizableHodgeStructureCat.subsingleton_zero_ratCarrier (n : ℤ) :
    Subsingleton (zero n).ratCarrier

    The rational carrier of the named zero object is subsingleton.

    source
    theorem TauCeti.Hodge.PolarizableHodgeStructureCat.isZero_zero (n : ℤ) :
    CategoryTheory.Limits.IsZero (zero n)

    The named zero object is both initial and terminal.

    source
    instance TauCeti.Hodge.PolarizableHodgeStructureCat.hasZeroObject {n : ℤ} :
    CategoryTheory.Limits.HasZeroObject (PolarizableHodgeStructureCat n)

    The category of polarizable Hodge structures of weight n has a zero object.