Effective Hodge structures of weight one

An effective pure Hodge structure of weight one has only the two Hodge components H^{1,0} and H^{0,1}. Its Weil operator acts on them by i and -i, respectively, and therefore descends to an almost complex structure on the real form fixed by conjugation.

This file identifies the i- and -i-eigenspaces of the Weil operator with H^{1,0} and H^{0,1}. It then transfers those identifications to the scalar extension of the real almost complex structure constructed in TauCeti.Geometry.Hodge.WeilOperator. In weight one without effectivity, the two eigenspaces aggregate all Hodge components according to their first index modulo two, so the identifications with H^{1,0} and H^{0,1} characterize effectivity.

Conversely, an almost complex structure on a real vector space determines an effective pure Hodge structure of weight one on its complexification. Its Hodge components are the i- and -i-eigenspaces of the complex-linear extension, and its Weil operator is that extension.

The two constructions are mutually inverse. An effective weight-one Hodge structure is determined by its Weil operator, and on the complexification ℂ ⊗[ℝ] U of a real vector space the Weil operator of a Hodge structure of odd weight is real, so it is the scalar extension of an almost complex structure on U. Hence the almost complex structures on U are exactly the effective weight-one Hodge structures on ℂ ⊗[ℝ] U.

The real form and its structure map are the generic constructions TauCeti.realPoints and TauCeti.realPointsLift; TauCeti.realPointsEquiv identifies its complexification with the original complex vector space. The almost-complex structure reuses TauCeti.AlmostComplexStructure, rather than introducing a Hodge-specific copy of that notion.

Main declarations

• TauCeti.Hodge.HodgeStructureOn.eigenspace_weilOperator_I and TauCeti.Hodge.HodgeStructureOn.eigenspace_weilOperator_neg_I: for an effective structure, the two eigenspaces of the Weil operator are the two Hodge components.
• TauCeti.Hodge.HodgeStructureOn.eigenspace_weilOperator_I_eq_iSup and TauCeti.Hodge.HodgeStructureOn.eigenspace_weilOperator_neg_I_eq_iSup: in general, the two eigenspaces are spanned by the Hodge components H^{p,1-p} with p odd, respectively even.
• TauCeti.Hodge.HodgeStructureOn.isEffective_iff_eigenspace_weilOperator_I and TauCeti.Hodge.HodgeStructureOn.isEffective_iff_eigenspace_weilOperator_neg_I: either eigenspace comparison holds exactly for effective structures.
• TauCeti.Hodge.HodgeStructureOn.eigenspace_baseChange_realAlmostComplexStructure_I and TauCeti.Hodge.HodgeStructureOn.eigenspace_baseChange_realAlmostComplexStructure_neg_I: the same comparison on the literal complexification of the real form.
• TauCeti.AlmostComplexStructure.hodgeStructure: the effective weight-one Hodge structure associated with an almost complex structure.
• TauCeti.AlmostComplexStructure.hodgeStructure_weilOperator: its Weil operator is the complexification of the original almost complex structure.
• TauCeti.Hodge.HodgeStructureOn.eq_of_weilOperator_eq: an effective weight-one Hodge structure is determined by its Weil operator.
• TauCeti.AlmostComplexStructure.hodgeStructureEquiv: almost complex structures on U are equivalent to effective weight-one Hodge structures on ℂ ⊗[ℝ] U.

The construction and conventions follow Voisin, Hodge Theory and Complex Algebraic Geometry I, §6, and Peters--Steenbrink, Mixed Hodge Structures, §2.

theorem TauCeti.Hodge.HodgeStructureOn.eigenspace_weilOperator_I {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} (hs : HodgeStructureOn W ω 1) (heff : hs.IsEffective) : Module.End.eigenspace hs.weilOperator Complex.I = hs.piece 1

For an effective weight-one Hodge structure, the i-eigenspace of the Weil operator is exactly the Hodge component H^{1,0}.

This and the other effective weight-one eigenspace equalities are intentionally not simp lemmas: isEffective_iff simplifies their IsEffective hypothesis, so simpNF rejects the attributes. Use them as explicit rewrite rules.

theorem TauCeti.Hodge.HodgeStructureOn.eigenspace_weilOperator_neg_I {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} (hs : HodgeStructureOn W ω 1) (heff : hs.IsEffective) : Module.End.eigenspace hs.weilOperator (-Complex.I) = hs.piece 0

For an effective weight-one Hodge structure, the -i-eigenspace of the Weil operator is exactly the conjugate Hodge component H^{0,1}.

theorem TauCeti.Hodge.HodgeStructureOn.eigenspace_weilOperator_I_eq_iSup {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} (hs : HodgeStructureOn W ω 1) : Module.End.eigenspace hs.weilOperator Complex.I = ⨆ (p : ℤ), ⨆ (_ : Odd p), hs.piece p

In weight one, without assuming effectivity, the i-eigenspace of the Weil operator is spanned by the Hodge components H^{p,1-p} with p odd.

theorem TauCeti.Hodge.HodgeStructureOn.eigenspace_weilOperator_neg_I_eq_iSup {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} (hs : HodgeStructureOn W ω 1) : Module.End.eigenspace hs.weilOperator (-Complex.I) = ⨆ (p : ℤ), ⨆ (_ : Even p), hs.piece p

In weight one, without assuming effectivity, the -i-eigenspace of the Weil operator is spanned by the Hodge components H^{p,1-p} with p even.

theorem TauCeti.Hodge.HodgeStructureOn.isEffective_iff_eigenspace_weilOperator_I {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} (hs : HodgeStructureOn W ω 1) : hs.IsEffective ↔ Module.End.eigenspace hs.weilOperator Complex.I = hs.piece 1

The eigenspace comparison characterizes effectivity. A weight-one Hodge structure is effective exactly when the i-eigenspace of its Weil operator is H^{1,0}; otherwise that eigenspace also contains a nonzero component H^{p,1-p} with p ≠ 1 odd.

theorem TauCeti.Hodge.HodgeStructureOn.isEffective_iff_eigenspace_weilOperator_neg_I {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} (hs : HodgeStructureOn W ω 1) : hs.IsEffective ↔ Module.End.eigenspace hs.weilOperator (-Complex.I) = hs.piece 0

A weight-one Hodge structure is effective exactly when the -i-eigenspace of its Weil operator is H^{0,1}; otherwise that eigenspace also contains a nonzero component H^{p,1-p} with p ≠ 0 even.

theorem TauCeti.Hodge.HodgeStructureOn.eq_of_weilOperator_eq {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {hs hs' : HodgeStructureOn W ω 1} (h : hs.IsEffective) (h' : hs'.IsEffective) (hC : hs.weilOperator = hs'.weilOperator) : hs = hs'

An effective weight-one Hodge structure is determined by its Weil operator. Its filtration is ⊤ in nonpositive degrees and ⊥ above degree one, while F¹ = H^{1,0} is the i-eigenspace of the Weil operator.

theorem TauCeti.Hodge.HodgeStructureOn.eigenspace_baseChange_realAlmostComplexStructure_I {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} (hs : HodgeStructureOn W ω 1) (heff : hs.IsEffective) : Module.End.eigenspace (LinearMap.baseChange ℂ (hs.realAlmostComplexStructure eigenspace_baseChange_realAlmostComplexStructure_I._proof_1).toLinearMap) Complex.I = Submodule.comap (↑(realPointsEquiv ⋯)) (hs.piece 1)

On the literal complexification ℂ ⊗[ℝ] V_ℝ, the i-eigenspace of the scalar extension of the real almost complex structure corresponds to H^{1,0} under realPointsEquiv.

theorem TauCeti.Hodge.HodgeStructureOn.eigenspace_baseChange_realAlmostComplexStructure_neg_I {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} (hs : HodgeStructureOn W ω 1) (heff : hs.IsEffective) : Module.End.eigenspace (LinearMap.baseChange ℂ (hs.realAlmostComplexStructure eigenspace_baseChange_realAlmostComplexStructure_I._proof_1).toLinearMap) (-Complex.I) = Submodule.comap (↑(realPointsEquiv ⋯)) (hs.piece 0)

On the literal complexification ℂ ⊗[ℝ] V_ℝ, the -i-eigenspace of the scalar extension of the real almost complex structure corresponds to H^{0,1} under realPointsEquiv.

noncomputable def TauCeti.AlmostComplexStructure.hodgeStructure {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : Hodge.HodgeStructureOn (TensorProduct ℝ ℂ V) (Hodge.complexificationConjugation V) 1

The effective pure Hodge structure of weight one associated with a real almost complex structure. Its F¹ is the i-eigenspace of the complexified endomorphism.

@[simp]

theorem TauCeti.AlmostComplexStructure.hodgeStructure_F {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) (p : ℤ) : J.hodgeStructure.F p = if p ≤ 0 then ⊤ else if p = 1 then Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I else ⊥

The filtration of the Hodge structure associated with J is top in nonpositive degrees, the i-eigenspace in degree one, and bottom above degree one.

theorem TauCeti.AlmostComplexStructure.isEffective_hodgeStructure {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.hodgeStructure.IsEffective

The Hodge structure associated with an almost complex structure is effective.

@[simp]

theorem TauCeti.AlmostComplexStructure.hodgeStructure_piece_one {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.hodgeStructure.piece 1 = Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I

The H^{1,0} component associated with J is the i-eigenspace of its complexification.

@[simp]

theorem TauCeti.AlmostComplexStructure.hodgeStructure_piece_zero {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.hodgeStructure.piece 0 = Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I)

The H^{0,1} component associated with J is the -i-eigenspace of its complexification.

theorem TauCeti.AlmostComplexStructure.hodgeStructure_piece_eq_bot {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {p : ℤ} (hpzero : p ≠ 0) (hpone : p ≠ 1) : J.hodgeStructure.piece p = ⊥

Every Hodge component of the structure associated with J other than H^{1,0} and H^{0,1} vanishes.

@[simp]

theorem TauCeti.AlmostComplexStructure.hodgeStructure_proj_one {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.hodgeStructure.proj 1 = J.holomorphicProjection

The degree-one Hodge projection of J is its holomorphic type projection.

@[simp]

theorem TauCeti.AlmostComplexStructure.hodgeStructure_proj_zero {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.hodgeStructure.proj 0 = J.antiholomorphicProjection

The degree-zero Hodge projection of J is its antiholomorphic type projection.

@[simp]

theorem TauCeti.AlmostComplexStructure.hodgeStructure_weilOperator {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) : J.hodgeStructure.weilOperator = LinearMap.baseChange ℂ J.toLinearMap

The Weil operator of the Hodge structure associated with J is the complex-linear scalar extension of J. Thus the construction recovers the original almost complex structure after complexification.

Effective weight-one Hodge structures are almost complex structures

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.hodgeStructure_almostComplexStructure {U : Type u_1} [AddCommGroup U] [Module ℝ U] (hs : HodgeStructureOn (TensorProduct ℝ ℂ U) (complexificationConjugation U) 1) (h : hs.F 0 = ⊤) : (hs.almostComplexStructure ⋯).hodgeStructure = hs

An effective weight-one Hodge structure on ℂ ⊗[ℝ] U is the Hodge structure of its induced almost complex structure.

theorem TauCeti.AlmostComplexStructure.baseChange_injective {U : Type u_1} [AddCommGroup U] [Module ℝ U] : Function.Injective fun (J : AlmostComplexStructure U) => LinearMap.baseChange ℂ J.toLinearMap

An almost complex structure is determined by its complex-linear scalar extension.

@[simp]

theorem TauCeti.AlmostComplexStructure.almostComplexStructure_hodgeStructure {U : Type u_1} [AddCommGroup U] [Module ℝ U] (J : AlmostComplexStructure U) : J.hodgeStructure.almostComplexStructure ⋯ = J

The almost complex structure induced by the weight-one Hodge structure of J is J.

noncomputable def TauCeti.AlmostComplexStructure.hodgeStructureEquiv {U : Type u_1} [AddCommGroup U] [Module ℝ U] : AlmostComplexStructure U ≃ { hs : Hodge.HodgeStructureOn (TensorProduct ℝ ℂ U) (Hodge.complexificationConjugation U) 1 // hs.IsEffective }

Almost complex structures on a real vector space U are the effective weight-one Hodge structures on its complexification. The forward map is TauCeti.AlmostComplexStructure.hodgeStructure, and the inverse restricts the Weil operator to the real vectors.

@[simp]

theorem TauCeti.AlmostComplexStructure.coe_hodgeStructureEquiv_apply {U : Type u_1} [AddCommGroup U] [Module ℝ U] (J : AlmostComplexStructure U) : ↑(hodgeStructureEquiv J) = J.hodgeStructure

The equivalence sends J to its weight-one Hodge structure.

@[simp]

theorem TauCeti.AlmostComplexStructure.hodgeStructureEquiv_symm_apply {U : Type u_1} [AddCommGroup U] [Module ℝ U] (hs : { hs : Hodge.HodgeStructureOn (TensorProduct ℝ ℂ U) (Hodge.complexificationConjugation U) 1 // hs.IsEffective }) : hodgeStructureEquiv.symm hs = (↑hs).almostComplexStructure ⋯

The inverse equivalence sends a Hodge structure to its induced almost complex structure.