Mixed Hodge structures #
A mixed Hodge structure on an integral module is an increasing rational weight filtration W
together with a decreasing complex Hodge filtration F inducing a pure Hodge structure of weight
k on every rational graded piece grᵂ_k = W_k / W_{k-1}. The graded objects the purity
condition is stated against are built in TauCeti/Geometry/Hodge/Graded.lean.
Purity is recorded as the existence of a TauCeti.Hodge.HodgeStructure whose filtration is the
induced one, rather than as a restatement of the pure axioms or as the bare existence of some
Hodge structure on the graded piece: the former would duplicate the pure object, the latter would
lose the link with F. As a consequence every result about pure Hodge structures — Hodge
components, the Hodge decomposition, the Weil operator — applies to the graded pieces of a mixed
Hodge structure through TauCeti.Hodge.MixedHodgeStructure.gradedHodgeStructure.
A pure Hodge structure of weight n is a mixed Hodge structure whose weight filtration is
concentrated in degree n; this is TauCeti.Hodge.MixedHodgeStructure.ofPure, and it makes the
Tate structure ℤ(m) an explicit rank-one inhabitant.
Main declarations #
TauCeti.Hodge.MixedHodgeStructure: the mixed Hodge structure itself.TauCeti.Hodge.MixedHodgeStructure.WC: the complexified weight filtration.TauCeti.Hodge.MixedHodgeStructure.conjF: the conjugate Hodge filtration.TauCeti.Hodge.MixedHodgeStructure.gradedHodgeStructure: the pure Hodge structure of weightkcarried by thek-th graded piece.TauCeti.Hodge.MixedHodgeStructure.ofPure: a pure Hodge structure viewed as a mixed one.TauCeti.Hodge.tateMixed: the Tate structure as a mixed Hodge structure.
References #
Deligne, Théorie de Hodge II, 1.2.10 and 2.3.5; Peters–Steenbrink, Mixed Hodge Structures,
Ch. 3. The signature of MixedHodgeStructure is adapted from the proposed definitions in
HodgeStructures/Suggested.lean,
whose definitive mathematical specification is the accompanying Hodge structures roadmap.
A mixed Hodge structure on an integral module Vℤ with rational and complex base-change
models Vℚ and Vℂ.
The weight filtration WQ is increasing, recorded rationally, and finite in both directions; the
Hodge filtration F is decreasing and bounded on the complex model. Purity is imposed on the
rational graded pieces: for every k, the filtration TauCeti.Hodge.gradedF induced by F on
the complexification of grᵂ_k = W_k / W_{k-1} is the Hodge filtration of a pure Hodge structure
of weight k.
The increasing rational weight filtration.
The weight filtration is increasing.
The weight filtration is exhaustive:
W_kis everything forklarge.The weight filtration is separated:
W_kis zero forksmall.The decreasing Hodge filtration on the complex model.
The Hodge filtration is decreasing.
The Hodge filtration is exhaustive:
F^pis everything forpsmall.The Hodge filtration is separated:
F^pis zero forplarge.The
k-th rational graded piece, complexified, is a pure Hodge structure of weightkfor the induced filtration.
Instances For
The complexified weight filtration of a mixed Hodge structure.
It is an abbrev because it is a name for the complexification of WQ rather than a new
construction: the graded pieces of WC have to be definitionally those of the complexified
rational filtration for the pure structure on a graded piece to transport onto them.
Instances For
The complex weight filtration is obtained by complexifying the rational weight filtration.
The complexified weight filtration is stable under lattice-induced conjugation.
The complexified weight filtration is increasing.
The complexified weight filtration is exhaustive.
The complexified weight filtration is separated.
The conjugate Hodge filtration #
The conjugate conj F^p of the p-th step of the Hodge filtration of a mixed Hodge
structure, taken for lattice-induced conjugation.
Instances For
The conjugate Hodge filtration step is the image of the Hodge filtration step under lattice-induced conjugation.
The conjugate Hodge filtration is decreasing.
Membership in a conjugate Hodge filtration step is detected by conjugating.
Conjugating a Hodge filtration step twice recovers it.
The conjugate Hodge filtration is exhaustive wherever the Hodge filtration is.
The conjugate Hodge filtration is separated wherever the Hodge filtration is.
The conjugate Hodge filtration is exhaustive.
The conjugate Hodge filtration is separated.
The pure Hodge structure of weight k carried by the complexification of the k-th rational
graded piece. Its filtration is the induced one on the nose, so the whole pure theory applies to
the graded pieces of a mixed Hodge structure.
Instances For
The Hodge decomposition of each graded piece of a mixed Hodge structure.
The weight filtration concentrated in a single degree n: everything from degree n on,
zero below. It is the weight filtration of a pure Hodge structure of weight n.
Instances For
Away from its single jump, the concentrated weight filtration is constant.
A pure Hodge structure is a mixed Hodge structure. Its weight filtration is concentrated
in the single degree n, so the only nonzero graded piece is grᵂ_n, which is the whole space
with the given filtration. This exhibits the mixed axioms as satisfiable.
Instances For
The conjugate Hodge filtration of a pure Hodge structure viewed as a mixed one is its conjugate Hodge filtration.
The weight filtration of a pure Hodge structure of weight n, viewed as a mixed one, is the
whole space from degree n on.
The weight filtration of a pure Hodge structure of weight n, viewed as a mixed one, vanishes
below degree n.
The Tate structure ℤ(m) as a mixed Hodge structure: a rank-one example whose weight
filtration jumps in degree -2m.