Weight-one Hodge structures from complex structures on integral modules

Let V be an integral module and let J be an almost complex structure on its realification Vℝ = ℝ ⊗[ℤ] V. Extending J to ℂ and transporting it to any chosen abstract complexification Vℂ of V gives complementary i- and -i-eigenspaces. They define an effective Hodge structure of weight one on V.

This file carries the construction on a real vector space through the base-change comparison from TauCeti.Geometry.Hodge.Realification. In particular the resulting filtration, Hodge pieces, and Weil operator are described directly in the chosen ambient complexification, so geometric models need no transport isomorphism in their public statements.

Conversely, the Weil operator of an effective Hodge structure of weight one on V is real and squares to -1, so it restricts to a complex structure on Vℝ. The two constructions are mutually inverse. Effective weight-one examples, such as the first cohomology of a complex torus, can therefore be given either by a Hodge filtration or by a complex structure on the real lattice span, and the two descriptions agree.

Main declarations

• TauCeti.AlmostComplexStructure.latticeComplexification: the complex-linear extension of J acting on the chosen abstract complexification; on the real points coming from the realification it acts by J (latticeComplexification_realificationComplexEquiv_one_tmul).
• TauCeti.AlmostComplexStructure.latticeHodgeStructure: the associated effective integral Hodge structure of weight one.
• TauCeti.AlmostComplexStructure.latticeHodgeStructure_piece_one and TauCeti.AlmostComplexStructure.latticeHodgeStructure_piece_zero: its degree-one and degree-zero pieces.
• TauCeti.AlmostComplexStructure.latticeHodgeStructure_weilOperator: the Weil operator recovers the transported complex structure.
• TauCeti.AlmostComplexStructure.two_mul_latticeHodgeStructure_hodgeNumber: on a finite free lattice, h^{1,0} = h^{0,1} is half the rank and all other Hodge numbers vanish.
• TauCeti.Hodge.HodgeStructureOn.latticeAlmostComplexStructure: conversely, the complex structure on Vℝ induced by an integral Hodge structure of odd weight on V, which complexifies to its Weil operator (latticeComplexification_latticeAlmostComplexStructure).
• TauCeti.AlmostComplexStructure.latticeHodgeStructureEquiv: the two constructions are mutually inverse, so complex structures on Vℝ are exactly the effective integral Hodge structures of weight one on V.

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

noncomputable def TauCeti.AlmostComplexStructure.latticeComplexification {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) : Vℂ →ₗ[ℂ] Vℂ

The complex-linear extension of an almost complex structure on the realification of an integral module, transported to a chosen abstract complexification of that module.

@[simp]

theorem TauCeti.AlmostComplexStructure.realificationComplexEquiv_baseChange_apply {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) (x : TensorProduct ℝ ℂ (Hodge.Realification V)) : (Hodge.realificationComplexEquiv hℂ) ((LinearMap.baseChange ℂ J.toLinearMap) x) = (J.latticeComplexification hℂ) ((Hodge.realificationComplexEquiv hℂ) x)

The realification comparison intertwines the scalar extension of J with its transported action on the abstract complexification.

@[simp]

theorem TauCeti.AlmostComplexStructure.latticeComplexification_realificationComplexEquiv_one_tmul {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) (x : Hodge.Realification V) : (J.latticeComplexification hℂ) ((Hodge.realificationComplexEquiv hℂ) (1 ⊗ₜ[ℝ] x)) = (Hodge.realificationComplexEquiv hℂ) (1 ⊗ₜ[ℝ] J.toLinearMap x)

The transported complex structure acts on the image of a real vector by the original almost complex structure.

theorem TauCeti.AlmostComplexStructure.latticeComplexification_comp_self {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) : J.latticeComplexification hℂ ∘ₗ J.latticeComplexification hℂ = -LinearMap.id

The transported complex structure still squares to minus the identity.

theorem TauCeti.AlmostComplexStructure.eigenspace_latticeComplexification {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) (z : ℂ) : Module.End.eigenspace (J.latticeComplexification hℂ) z = Submodule.map (↑(Hodge.realificationComplexEquiv hℂ)) (Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) z)

The eigenspaces of the transported endomorphism are the transports of the eigenspaces of the literal scalar extension.

noncomputable def TauCeti.AlmostComplexStructure.latticeHodgeStructure {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) : Hodge.HodgeStructure hℂ 1

The effective weight-one Hodge structure determined by a complex structure on the realification of an integral module.

@[simp]

theorem TauCeti.AlmostComplexStructure.latticeHodgeStructure_F {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) (p : ℤ) : (J.latticeHodgeStructure hℂ).F p = if p ≤ 0 then ⊤ else if p = 1 then Module.End.eigenspace (J.latticeComplexification hℂ) Complex.I else ⊥

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

theorem TauCeti.AlmostComplexStructure.isEffective_latticeHodgeStructure {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) : Hodge.HodgeStructureOn.IsEffective (J.latticeHodgeStructure hℂ)

The weight-one Hodge structure associated with the complex structure is effective.

@[simp]

theorem TauCeti.AlmostComplexStructure.latticeHodgeStructure_piece_one {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) : Hodge.HodgeStructureOn.piece (J.latticeHodgeStructure hℂ) 1 = Module.End.eigenspace (J.latticeComplexification hℂ) Complex.I

The H^{1,0} component associated with the complex structure is its i-eigenspace.

@[simp]

theorem TauCeti.AlmostComplexStructure.latticeHodgeStructure_piece_zero {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) : Hodge.HodgeStructureOn.piece (J.latticeHodgeStructure hℂ) 0 = Module.End.eigenspace (J.latticeComplexification hℂ) (-Complex.I)

The H^{0,1} component associated with the complex structure is its -i-eigenspace.

theorem TauCeti.AlmostComplexStructure.latticeHodgeStructure_piece_eq_bot {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) {p : ℤ} (hpzero : p ≠ 0) (hpone : p ≠ 1) : Hodge.HodgeStructureOn.piece (J.latticeHodgeStructure hℂ) p = ⊥

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

@[simp]

theorem TauCeti.AlmostComplexStructure.latticeHodgeStructure_weilOperator {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) : Hodge.HodgeStructureOn.weilOperator (J.latticeHodgeStructure hℂ) = J.latticeComplexification hℂ

The Weil operator of the Hodge structure associated with the complex structure is the transported complex-linear extension of that structure.

theorem TauCeti.AlmostComplexStructure.two_mul_latticeHodgeStructure_hodgeNumber {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} [Module.Free ℤ V] [Module.Finite ℤ V] (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) (p : ℤ) : 2 * Hodge.HodgeStructureOn.hodgeNumber (J.latticeHodgeStructure hℂ) p = if p = 0 ∨ p = 1 then Module.finrank ℤ V else 0

The Hodge numbers of the structure associated with a complex structure: h^{1,0} and h^{0,1} are both half the rank of V, and all other Hodge numbers vanish.

Effective weight-one Hodge structures on a lattice are complex structures

noncomputable def TauCeti.Hodge.HodgeStructureOn.latticeAlmostComplexStructure {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} (hs : HodgeStructure hℂ n) (hn : Odd n) : AlmostComplexStructure (Realification V)

The almost complex structure on the realification ℝ ⊗[ℤ] V determined by an integral Hodge structure of odd weight on V: its Weil operator, which is real, restricted to the real points of the complexification.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.latticeComplexification_latticeAlmostComplexStructure {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} (hs : HodgeStructure hℂ n) (hn : Odd n) : (latticeAlmostComplexStructure hs hn).latticeComplexification hℂ = weilOperator hs

The induced complex structure complexifies to the Weil operator on the chosen abstract complexification.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.latticeHodgeStructure_latticeAlmostComplexStructure {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} (hs : HodgeStructure hℂ 1) (h : hs.F 0 = ⊤) : (latticeAlmostComplexStructure hs ⋯).latticeHodgeStructure hℂ = hs

An effective integral Hodge structure of weight one is the Hodge structure of its induced complex structure on the realification.

theorem TauCeti.AlmostComplexStructure.latticeComplexification_injective {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) : Function.Injective fun (J : AlmostComplexStructure (Hodge.Realification V)) => J.latticeComplexification hℂ

A complex structure on the realification is determined by its transport to a chosen abstract complexification.

@[simp]

theorem TauCeti.AlmostComplexStructure.latticeAlmostComplexStructure_latticeHodgeStructure {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) : Hodge.HodgeStructureOn.latticeAlmostComplexStructure (J.latticeHodgeStructure hℂ) ⋯ = J

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

noncomputable def TauCeti.AlmostComplexStructure.latticeHodgeStructureEquiv {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) : AlmostComplexStructure (Hodge.Realification V) ≃ { hs : Hodge.HodgeStructure hℂ 1 // Hodge.HodgeStructureOn.IsEffective hs }

Complex structures on the realification of V are the effective integral Hodge structures of weight one on V, for any chosen abstract complexification of V. The forward map is TauCeti.AlmostComplexStructure.latticeHodgeStructure, and the inverse restricts the Weil operator to the real points.

@[simp]

theorem TauCeti.AlmostComplexStructure.coe_latticeHodgeStructureEquiv_apply {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (J : AlmostComplexStructure (Hodge.Realification V)) : ↑((latticeHodgeStructureEquiv hℂ) J) = J.latticeHodgeStructure hℂ

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

@[simp]

theorem TauCeti.AlmostComplexStructure.latticeHodgeStructureEquiv_symm_apply {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (hs : { hs : Hodge.HodgeStructure hℂ 1 // Hodge.HodgeStructureOn.IsEffective hs }) : (latticeHodgeStructureEquiv hℂ).symm hs = Hodge.HodgeStructureOn.latticeAlmostComplexStructure ↑hs ⋯

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