Conjugation of Deligne's bigrading

For a mixed Hodge structure, complex conjugation exchanges the Deligne bigrading pieces up to strictly lower bidegrees. This file first proves the coarser weight-filtered form

conj I^{p,q} + W_{p+q-2} = I^{q,p} + W_{p+q-2}.

The two-step weight bound follows directly from the current API. Deligne's closed formula puts a vector of conj I^{p,q} in F^q modulo W_{p+q-2}, while it lies in conj F^p exactly. A representative of the same class in I^{q,p} initially agrees only modulo W_{p+q-1}. On the intervening graded piece, however, their difference lies in the opposed steps F^q and conj F^p of a pure Hodge structure of weight p+q-1, so it vanishes and the difference drops one step further.

The full relation then refines the error term to the sum of the pieces I^{r,s} with r < q and s < p. The Hodge-filtration recovery theorem identifies every intersection F^a ∩ W_b as the sum of the Deligne components satisfying both bounds. It follows that the tail in Deligne's formula, after adjoining its leading filtration step, is precisely saturation by the lower-bidegree components. Induction on total degree gives the same statement for the conjugate tail. The two closed formulas then agree modulo the lower-bidegree sum by the modular law for subspaces.

Main declarations

• TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_le_sup_WC: conjugating I^{p,q} lands in I^{q,p} + W_{p+q-2}.
• TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_sup_WC: the symmetric equality modulo W_{p+q-2}.
• TauCeti.Hodge.MixedHodgeStructure.exists_mem_deligneSplitting_smodEq_latticeConj: the elementwise modular-congruence form.
• TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_sup_below: the full Deligne relation, with the error supported in strictly lower bidegrees.
• TauCeti.Hodge.MixedHodgeStructure.map_deligneSplittingBelow: conjugation exchanges the corresponding lower-bidegree sums.
• TauCeti.Hodge.MixedHodgeStructure.exists_mem_deligneSplitting_smodEq_latticeConj_below: the elementwise form of the full relation.

References

Deligne, Théorie de Hodge II, 1.2.10; Peters--Steenbrink, Mixed Hodge Structures, Lemma-Definition 3.4.

theorem TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_le_sup_WC {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (p q : ℤ) : Submodule.map (latticeConj hℂ) (mhs.deligneSplitting p q) ≤ mhs.deligneSplitting q p ⊔ mhs.WC (p + q - 2)

Conjugating I^{p,q} lands in the swapped Deligne piece modulo W_{p+q-2}.

theorem TauCeti.Hodge.MixedHodgeStructure.deligneSplitting_le_map_latticeConj_sup_WC {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (p q : ℤ) : mhs.deligneSplitting q p ≤ Submodule.map (latticeConj hℂ) (mhs.deligneSplitting p q) ⊔ mhs.WC (p + q - 2)

The swapped Deligne piece lands in the conjugate of I^{p,q} modulo W_{p+q-2}.

This is the reverse containment to TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_le_sup_WC. It follows by applying that containment with the indices exchanged and conjugating once more.

theorem TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_sup_WC {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (p q : ℤ) : Submodule.map (latticeConj hℂ) (mhs.deligneSplitting p q) ⊔ mhs.WC (p + q - 2) = mhs.deligneSplitting q p ⊔ mhs.WC (p + q - 2)

Conjugation exchanges Deligne's bigrading modulo two lower weight steps:

conj I^{p,q} + W_{p+q-2} = I^{q,p} + W_{p+q-2}.

The two containments are symmetric because lattice conjugation is an involution and preserves the weight filtration.

theorem TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_eq_of_WC_eq_bot {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) {p q : ℤ} (hW : mhs.WC (p + q - 2) = ⊥) : Submodule.map (latticeConj hℂ) (mhs.deligneSplitting p q) = mhs.deligneSplitting q p

If the weight filtration already vanishes two steps below p+q, conjugation exchanges the Deligne pieces I^{p,q} and I^{q,p} exactly.

theorem TauCeti.Hodge.MixedHodgeStructure.map_mkQ_map_latticeConj_deligneSplitting_eq {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (p q : ℤ) : Submodule.map (mhs.WC (p + q - 2)).mkQ (Submodule.map (latticeConj hℂ) (mhs.deligneSplitting p q)) = Submodule.map (mhs.WC (p + q - 2)).mkQ (mhs.deligneSplitting q p)

The images of conj I^{p,q} and I^{q,p} in the quotient by W_{p+q-2} agree.

theorem TauCeti.Hodge.MixedHodgeStructure.exists_mem_deligneSplitting_smodEq_latticeConj {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (p q : ℤ) {x : Vℂ} (hx : x ∈ mhs.deligneSplitting p q) : ∃ y ∈ mhs.deligneSplitting q p, (latticeConj hℂ) x ≡ y [SMOD mhs.WC (p + q - 2)]

Elementwise form of conjugation symmetry modulo W_{p+q-2}: every vector in I^{p,q} has a conjugate congruent to a vector in I^{q,p}.

The fine lower-bidegree relation

theorem TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_sup_below {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (p q : ℤ) : Submodule.map (latticeConj hℂ) (mhs.deligneSplitting p q) ⊔ mhs.deligneSplittingBelow q p = mhs.deligneSplitting q p ⊔ mhs.deligneSplittingBelow q p

Deligne's fine conjugation relation. Conjugation exchanges I^{p,q} and I^{q,p} modulo the sum of the components I^{r,s} with r < q and s < p.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.map_deligneSplittingBelow {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (p q : ℤ) : Submodule.map (latticeConj hℂ) (mhs.deligneSplittingBelow p q) = mhs.deligneSplittingBelow q p

Conjugation exchanges the sums of Deligne components below transposed bidegrees.

theorem TauCeti.Hodge.MixedHodgeStructure.exists_mem_deligneSplitting_smodEq_latticeConj_below {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (p q : ℤ) {x : Vℂ} (hx : x ∈ mhs.deligneSplitting p q) : ∃ y ∈ mhs.deligneSplitting q p, (latticeConj hℂ) x ≡ y [SMOD mhs.deligneSplittingBelow q p]

Elementwise form of Deligne's fine conjugation relation.