The zero mixed Hodge structure #
This file constructs a zero object in the category of mixed Hodge structures. Its integral,
rational, and complex carriers are the zero modules, presented as functions from Fin 0; its
filtrations are those of the pure zero Hodge structure, viewed as mixed in weight zero.
The zero object is the nullary product and the nullary coproduct of the category, and it is the terminal object from which finite products are assembled out of binary ones. It is therefore one ingredient of the finite limits and colimits that the abelian structure on mixed Hodge structures needs.
Main declarations #
TauCeti.Hodge.MixedHodgeStructureCat.zero: the zero mixed Hodge structure.TauCeti.Hodge.MixedHodgeStructureCat.isZero_of_subsingleton_ratCarrier: a mixed Hodge structure with zero rational carrier is a zero object.TauCeti.Hodge.MixedHodgeStructureCat.isZero_zero: the named object is both initial and terminal.HasZeroObject TauCeti.Hodge.MixedHodgeStructureCat: the resulting categorical instance.
References #
Deligne, Théorie de Hodge II, §2.3; Peters--Steenbrink, Mixed Hodge Structures, Ch. 3.
The categorical API follows the zero-object pattern in
TauCeti.Algebra.Coalgebra.Comodule.Zero.
The zero mixed Hodge structure, with zero integral, rational, and complex carriers.
Instances For
A mixed Hodge structure with subsingleton rational carrier is a zero object.
Morphisms of mixed Hodge structures 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.
The rational carrier of the named zero mixed Hodge structure is subsingleton.
The named zero mixed Hodge structure is both initial and terminal.
The category of mixed Hodge structures has a zero object.