Deligne's bigrading is an internal direct sum #
TauCeti/Geometry/Hodge/Mixed/DeligneSplitting.lean builds the bigrading I^{p,q} of a mixed
Hodge structure from Deligne's closed formula and proves what follows from the formula alone. This
file proves Deligne's theorem about it: the pieces I^{p,q} form an internal direct sum of the
complex vector space, and the complexified weight step W_k is exactly the supremum of the pieces
of total degree at most k,
W_k = ⨆_{p + q ≤ k} I^{p,q}.
Everything runs through the comparison of I^{p,q} with the pure Hodge structure carried by the
graded piece gr^W_{p+q}, built in TauCeti/Geometry/Hodge/Mixed/Graded.lean. Three facts drive
it.
I^{p,q}meetsW_{p+q-1}trivially. A vector ofI^{p,q} ∩ W_mwithm < p + qlies inF^p, and lies inconj F^{m+1-p}moduloW_{m-1}; its class ingr^W_mtherefore lies in two complementary steps of a pure Hodge structure of weightmand so vanishes, pushing the vector down toW_{m-1}. Iterating exhausts the weight filtration downwards.I^{p,q}covers the Hodge componentH^{p,q}ofgr^W_{p+q}, granted thatW_{p+q-1}is already spanned by bigrading pieces. A representative of a class inH^{p,q}lies inF^pand is congruent moduloW_{p+q-1}to a vector ofconj F^q; splitting the error term into the bigrading pieces whose first index is at leastp— which lie inF^p— and those whose first index is smaller — which lie in the second factor of Deligne's formula — corrects the representative intoI^{p,q}without changing its class. Running this against the Hodge decomposition ofgr^W_kand inducting upwards onkfrom a weight step where the filtration vanishes gives the recovery ofW, and with it that the bigrading spans.- A weight step meets the supremum of the pieces of larger total degree trivially. This is a
descending induction on the weight which peels off one total degree at a time, and independence
follows: a vector of
I^{p,q}lying in the sum of all the other pieces first loses its part of larger total degree, and what is left has a class ingr^W_{p+q}lying both inH^{p,q}and in the complementaryconj F^{q+1} ⊔ F^{p+1}, hence vanishing.
The Hodge filtration is recovered from the bigrading by the same upward induction on the weight:
a vector of F^p ∩ W_k has its class in gr^W_k in the p-th step of the induced Hodge
filtration, so — the graded piece being pure — that class is a sum of Hodge components of first
index at least p, each the image of a bigrading piece; correcting the vector by a representative
of that sum drops it into F^p ∩ W_{k-1}.
The simultaneous recovery formula also supplies the lower-bidegree sums used to state and prove
the conjugation symmetry developed in TauCeti.Geometry.Hodge.Mixed.Conjugation.
Main declarations #
TauCeti.Hodge.MixedHodgeStructure.deligneSplitting_disjoint_WC:I^{p,q}meetsW_{p+q-1}trivially.TauCeti.Hodge.MixedHodgeStructure.WC_eq_iSup_deligneSplitting: the recoveryW_k = ⨆_{p+q ≤ k} I^{p,q}of the weight filtration.TauCeti.Hodge.MixedHodgeStructure.map_deligneSplitting_eq_piece: the image ofI^{p,q}ingr^W_{p+q}is the Hodge componentH^{p,q}.TauCeti.Hodge.MixedHodgeStructure.iSup_deligneSplittingFamily_eq_top: the bigrading spans.TauCeti.Hodge.MixedHodgeStructure.iSupIndep_deligneSplittingFamily: the pieces are independent.TauCeti.Hodge.MixedHodgeStructure.isInternal_deligneSplittingFamily: Deligne's theorem, the bigrading is an internal direct sum.TauCeti.Hodge.MixedHodgeStructure.F_eq_iSup_deligneSplitting: the recoveryF^p = ⨆_{p' ≥ p} ⨆_{q'} I^{p',q'}of the Hodge filtration.TauCeti.Hodge.MixedHodgeStructure.F_inf_WC_eq_iSup_deligneSplitting: simultaneous truncation by a Hodge step and a weight step.TauCeti.Hodge.MixedHodgeStructure.deligneSplittingBelow: the sum of the bigrading pieces strictly below a given bidegree.
References #
Deligne, Théorie de Hodge II, 1.2.8 and 1.2.10; Peters–Steenbrink, Mixed Hodge Structures, Lemma-Definition 3.4.
A bigrading piece meets the lower weight steps trivially #
A bigrading piece meets the weight step below its total degree trivially.
Where the Hodge filtration vanishes in the second index the bigrading vanishes: I^{p,q}
then lies in W_{p+q-1}, which it meets trivially. The bound on the first index is
TauCeti.Hodge.MixedHodgeStructure.deligneSplitting_eq_bot_of_F_eq_bot_left.
Above a weight index at which the weight filtration is everything the bigrading vanishes.
The bigrading covers the Hodge components of the graded pieces #
The recovery of the weight filtration #
Deligne's bigrading recovers the weight filtration: the complexified weight step W_k is
the supremum of the bigrading pieces of total degree at most k.
One inclusion is the containment I^{p,q} ≤ W_{p+q}. The other is an induction upwards on k
starting from a step where the weight filtration vanishes: the pieces of total degree exactly k
cover the Hodge components of gr^W_k, hence all of gr^W_k, so together with W_{k-1} they
span W_k.
The image of the Deligne bigrading piece I^{p,q} in gr^W_{p+q} is exactly the pure Hodge
component H^{p,q} of that graded piece.
Deligne's bigrading spans: the supremum of all the pieces I^{p,q} is the whole complex
vector space.
Independence of the bigrading pieces #
A weight step meets the supremum of the bigrading pieces of larger total degree trivially.
Descending induction on the weight peels off one total degree at a time, using that the supremum
of the pieces of total degree k meets W_{k-1} trivially.
The pieces of Deligne's bigrading are independent.
A vector of I^{p,q} lying in the sum of the other pieces first loses its part of larger total
degree, which the previous theorem kills; what is left lies in W_{p+q} and splits into
W_{p+q-1} and pieces of the same total degree but different first index, which together lie in
the two filtration steps complementary to the Hodge component H^{p,q}. The vector therefore
vanishes.
Deligne's theorem. The pieces I^{p,q} of Deligne's bigrading form an internal direct sum
of the complex vector space underlying a mixed Hodge structure.
The recovery of the Hodge filtration #
Deligne's bigrading recovers the Hodge filtration: the Hodge step F^p is the supremum of
the bigrading pieces whose first index is at least p.
One inclusion is I^{p',q'} ≤ F^{p'} ≤ F^p. The other is an induction upwards on the weight
filtration, starting from a step where it vanishes: the class in gr^W_k of a vector of
F^p ∩ W_k is a sum of Hodge components of first index at least p, each the image of a
bigrading piece, so correcting the vector by a representative of that sum drops it into
F^p ∩ W_{k-1}.
Intersecting a Hodge-filtration step with a weight-filtration step selects exactly the Deligne components satisfying both index bounds.
Lower-bidegree sums #
The sum of the Deligne components strictly below (p,q) in both bidegrees.
Instances For
A Deligne component strictly below both bounds belongs to the lower Deligne sum.
The lower Deligne sum is contained in a submodule exactly when every component strictly below both bounds is.
The lower-bidegree error below (p,q) lies at least two steps below total weight p+q.
Enlarging either bound enlarges the sum of lower Deligne components.