Hodge structures (pure, mixed, and polarized)
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
TheoremCategorical semisimplicity of polarizable rational Hodge structures#
Every object is isomorphic to a finite biproduct of simple objects induced by rational Hodge substructures.
TauCeti.Hodge.PolarizableHodgeStructureCat.exists_iso_biproduct_simple.{u'} {n : ℤ}
(X : TauCeti.Hodge.PolarizableHodgeStructureCat n) :
∃ s,
(∀ U ∈ s, CategoryTheory.Simple (X.ofSubstructure U)) ∧
Nonempty ((⨁ fun U => X.ofSubstructure ↑U) ≅ X)
Lean
Formalized in Tau Ceti as TauCeti.Hodge.PolarizableHodgeStructureCat.exists_iso_biproduct_simple.
Sources
TheoremSemisimplicity of polarizable rational Hodge structures#
Every rational Hodge substructure
of a polarizable pure Hodge structure has a complement, both over ℚ and after complexification,
orthogonal to it for some polarization.
TauCeti.Hodge.exists_isCompl_of_isPolarizable.{u, v, w} {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w}
[AddCommGroup Vℤ] [AddCommGroup Vℚ] [_root_.Module ℚ Vℚ] [AddCommGroup Vℂ] [_root_.Module ℂ Vℂ]
{ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ}
{hs : TauCeti.Hodge.HodgeStructure hℂ n} [Module.Finite ℚ Vℚ]
(h : TauCeti.Hodge.IsPolarizable hℂ hs) (W : TauCeti.Hodge.RationalHodgeSubstructure hℚ hs) :
∃ P W', IsCompl W.WQ W'.WQ ∧ IsCompl W.WC W'.WC ∧ ∀ v ∈ W.WC, ∀ w ∈ W'.WC, (P.Q v) w = 0
Uses 5
TheoremThe Hodge decomposition#
The Hodge components H^{p,n-p} form an internal direct sum of
the ambient complex vector space.
TauCeti.Hodge.HodgeStructureOn.isInternal_piece.{u} {W : Type u} [AddCommGroup W]
[_root_.Module ℂ W] {ω : TauCeti.Hodge.Conjugation W} {n : ℤ}
(hs : TauCeti.Hodge.HodgeStructureOn W ω n) : DirectSum.IsInternal hs.piece
Lean
Formalized in Tau Ceti as TauCeti.Hodge.HodgeStructureOn.isInternal_piece.
Other forms
The Hodge decomposition of a complex graded piece. Formalized in Tau Ceti as TauCeti.Hodge.MixedHodgeStructure.isInternal_complexGradedHodgeStructure_piece.
TauCeti.Hodge.MixedHodgeStructure.isInternal_complexGradedHodgeStructure_piece.{u, v, w}
{Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [_root_.Module ℚ Vℚ]
[AddCommGroup Vℂ] [_root_.Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ}
{hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : TauCeti.Hodge.MixedHodgeStructure hℚ hℂ)
(k : ℤ) : DirectSum.IsInternal (mhs.complexGradedHodgeStructure k).piece
Sources
Uses 1 · Used by 8
J is a Riemann form for J, with no flatness assumption · Polarizable pure Hodge structures are closed under internal homs · Self-duality is invertible up to a nonzero integer · Semisimplicity of polarizable rational Hodge structures · The dual of a polarizable pure Hodge structure is polarizable · The Hodge numbers partition the dimension · When V is flat over ℤ, the Riemann forms for J are exactly the forms polarizing its weight-one Hodge structureTheoremThe Hodge numbers partition the dimension#
the Hodge numbers of a weight-n Hodge
structure on a finite-dimensional complex vector space sum to its dimension.
TauCeti.Hodge.HodgeStructureOn.finsum_hodgeNumber_eq_finrank.{u} {W : Type u} [AddCommGroup W]
[_root_.Module ℂ W] {ω : TauCeti.Hodge.Conjugation W} {n : ℤ}
(hs : TauCeti.Hodge.HodgeStructureOn W ω n) [FiniteDimensional ℂ W] :
∑ᶠ (p : ℤ), hs.hodgeNumber p = Module.finrank ℂ W
Lean
Formalized in Tau Ceti as TauCeti.Hodge.HodgeStructureOn.finsum_hodgeNumber_eq_finrank.
Sources
Uses 2
TheoremDeligne's theorem (TauCeti.Hodge.MixedHodgeStructure.isInternal_deligneSplittingFamily)#
The pieces I^{p,q} of Deligne's bigrading form an internal direct sum
of the complex vector space underlying a mixed Hodge structure.
TauCeti.Hodge.MixedHodgeStructure.isInternal_deligneSplittingFamily.{u, v, w} {Vℤ : Type u}
{Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [_root_.Module ℚ Vℚ]
[AddCommGroup Vℂ] [_root_.Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ}
{hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ}
(mhs : TauCeti.Hodge.MixedHodgeStructure hℚ hℂ) : DirectSum.IsInternal mhs.deligneSplittingFamily
Lean
Formalized in Tau Ceti as TauCeti.Hodge.MixedHodgeStructure.isInternal_deligneSplittingFamily.
Sources
Uses 1
TheoremStrictness of a morphism of mixed Hodge structures for the Hodge filtration#
A complex
vector lying both in the image of f and in the target's Hodge step F^p is the image of a
vector of the source's F^p.
The two filtration steps are the sums of the bigrading pieces of first index at least p, and f
respects the bigrading, so a preimage may be truncated to its components of first index at least
p without changing its image.
TauCeti.Hodge.MixedHodgeStructure.Hom.range_inf_F_eq_map_F.{u, v, w, u', v', w'} {Vℤ : Type u}
{Vℚ : Type v} {Vℂ : Type w} {V'ℤ : Type u'} {V'ℚ : Type v'} {V'ℂ : Type w'} [AddCommGroup Vℤ]
[AddCommGroup Vℚ] [_root_.Module ℚ Vℚ] [AddCommGroup Vℂ] [_root_.Module ℂ Vℂ] [AddCommGroup V'ℤ]
[AddCommGroup V'ℚ] [_root_.Module ℚ V'ℚ] [AddCommGroup V'ℂ] [_root_.Module ℂ V'ℂ]
{ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {ι'ℚ : V'ℤ →ₗ[ℤ] V'ℚ} {ι'ℂ : V'ℤ →ₗ[ℤ] V'ℂ}
{hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℚ : IsBaseChange ℚ ι'ℚ}
{h'ℂ : IsBaseChange ℂ ι'ℂ} {source : TauCeti.Hodge.MixedHodgeStructure hℚ hℂ}
{target : TauCeti.Hodge.MixedHodgeStructure h'ℚ h'ℂ} (f : source.Hom target) (p : ℤ) :
f.toLinearMap.range ⊓ target.F p = Submodule.map f.toLinearMap (source.F p)
Lean
Formalized in Tau Ceti as TauCeti.Hodge.MixedHodgeStructure.Hom.range_inf_F_eq_map_F.
Sources
Uses 1 · Used by 2
InstanceTauCeti.Hodge.MixedHodgeStructureCat.abelian#
Mixed Hodge structures, with rational Hodge morphisms, form an abelian category.
TauCeti.Hodge.MixedHodgeStructureCat.abelian.{u} :
CategoryTheory.Abelian TauCeti.Hodge.MixedHodgeStructureCat
Uses 2
TheoremDeligne'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.
TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_sup_below.{u, v, w} {Vℤ : Type u}
{Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [_root_.Module ℚ Vℚ]
[AddCommGroup Vℂ] [_root_.Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ}
{hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : TauCeti.Hodge.MixedHodgeStructure hℚ hℂ)
(p q : ℤ) :
Submodule.map (TauCeti.Hodge.latticeConj hℂ) (mhs.deligneSplitting p q) ⊔
mhs.deligneSplittingBelow q p =
mhs.deligneSplitting q p ⊔ mhs.deligneSplittingBelow q p
Lean
Formalized in Tau Ceti as TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_sup_below.
Sources
- Tau Ceti documentation:
TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_sup_below - Source of
TauCeti.Hodge.MixedHodgeStructure.map_latticeConj_deligneSplitting_sup_belowin TauCeti/Geometry/Hodge/Mixed/Conjugation.lean - Tau Ceti roadmap status: Hodge structures (pure, mixed, and polarized)
Uses 1
TheoremWhen V is flat over ℤ, the Riemann forms for J are exactly the forms polarizing its weight-one Hodge structure#
Flatness is used only in the forward direction, for nondegeneracy.
TauCeti.AlmostComplexStructure.isRiemannForm_iff_isPolarization.{u, v} {V : Type u} {Vℂ : Type v}
[AddCommGroup V] [AddCommGroup Vℂ] [_root_.Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} [Module.Flat ℤ V]
(J : TauCeti.AlmostComplexStructure (TauCeti.Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ)
(E : LinearMap.BilinForm ℤ V) :
J.IsRiemannForm E ↔ TauCeti.Hodge.IsPolarization hℂ (J.latticeHodgeStructure hℂ) E
Lean
Formalized in Tau Ceti as TauCeti.AlmostComplexStructure.isRiemannForm_iff_isPolarization.
Sources
TheoremEvery form polarizing the weight-one Hodge structure of J is a Riemann form for J, with no flatness assumption#
J-invariance of E_ℝ says that the Weil operator is an isometry of the
polarization, and positivity of E_ℝ (J x) x is positivity of the Hodge form on real vectors.
TauCeti.AlmostComplexStructure.isRiemannForm_of_isPolarization.{u, v} {V : Type u} {Vℂ : Type v}
[AddCommGroup V] [AddCommGroup Vℂ] [_root_.Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ}
{J : TauCeti.AlmostComplexStructure (TauCeti.Hodge.Realification V)} {hℂ : IsBaseChange ℂ ιℂ}
{E : LinearMap.BilinForm ℤ V}
(h : TauCeti.Hodge.IsPolarization hℂ (J.latticeHodgeStructure hℂ) E) : J.IsRiemannForm E
Lean
Formalized in Tau Ceti as TauCeti.AlmostComplexStructure.isRiemannForm_of_isPolarization.
Sources
Uses 5 · Used by 1
TheoremSelf-duality is invertible up to a nonzero integer#
For a polarization of V, there is a
Hodge morphism g : V^*(-n) → V such that composing it with self-duality, in either order, is
multiplication by a nonzero natural number c. Over ℚ, c⁻¹ • g is the inverse of
self-duality.
TauCeti.Hodge.Polarization.exists_comp_toDualHom_eq_nsmul_id.{u, v} {V : Type u} {Vℂ : Type v}
[AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [_root_.Module ℂ Vℂ]
{ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : TauCeti.Hodge.HodgeStructure hℂ n}
(P : TauCeti.Hodge.Polarization hℂ hs) :
∃ c,
c ≠ 0 ∧
∃ g,
P.toDualHom.comp g = c • TauCeti.Hodge.HodgeStructure.Hom.id hs.dualTateTwist ∧
g.comp P.toDualHom = c • TauCeti.Hodge.HodgeStructure.Hom.id hs
Lean
Formalized in Tau Ceti as TauCeti.Hodge.Polarization.exists_comp_toDualHom_eq_nsmul_id.
Sources
Uses 5 · Used by 1
TheoremThe dual of a polarizable pure Hodge structure is polarizable#
TauCeti.Hodge.IsPolarizable.dual.{u, v} {V : Type u} {Vℂ : Type v} [AddCommGroup V]
[Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [_root_.Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ}
{hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : TauCeti.Hodge.HodgeStructure hℂ n}
(h : TauCeti.Hodge.IsPolarizable hℂ hs) : TauCeti.Hodge.IsPolarizable ⋯ hs.dual
Uses 6 · Used by 1
TheoremPolarizable pure Hodge structures are closed under internal homs#
The internal hom of
weights n₁ and n₂ is polarizable of weight n₂ - n₁.
TauCeti.Hodge.IsPolarizable.internalHom.{u₁, u₂, v₁, v₂} {V₁ : Type u₁} {V₂ : Type u₂}
{W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [Module.Free ℤ V₁] [Module.Finite ℤ V₁]
[AddCommGroup V₂] [AddCommGroup W₁] [_root_.Module ℂ W₁] [AddCommGroup W₂] [_root_.Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} {h₁ : IsBaseChange ℂ ι₁} {h₂ : IsBaseChange ℂ ι₂}
{n₁ n₂ : ℤ} {hs₁ : TauCeti.Hodge.HodgeStructure h₁ n₁} {hs₂ : TauCeti.Hodge.HodgeStructure h₂ n₂}
(h : TauCeti.Hodge.IsPolarizable h₁ hs₁) (h' : TauCeti.Hodge.IsPolarizable h₂ hs₂) :
TauCeti.Hodge.IsPolarizable ⋯ (hs₁.internalHom hs₂)
StructureTauCeti.Hodge.HodgeStructureOn#
A pure Hodge structure of weight n on a complex vector space with conjugation ω.
The decreasing filtration F is bounded and n-opposed to its conjugate: for every p,
F p is complementary to the conjugate of F (n + 1 - p).
TauCeti.Hodge.HodgeStructureOn.{u} (W : Type u) [AddCommGroup W] [_root_.Module ℂ W]
(ω : TauCeti.Hodge.Conjugation W) (n : ℤ) : Type u
Used by 16
TauCeti.Hodge.MixedHodgeStructure.isInternal_deligneSplittingFamily) · Every form polarizing the weight-one Hodge structure of J is a Riemann form for J, with no flatness assumption · Polarizable pure Hodge structures are closed under internal homs · Self-duality is invertible up to a nonzero integer · Semisimplicity of polarizable rational Hodge structures · Strictness of a morphism of mixed Hodge structures for the Hodge filtration · TauCeti.Hodge.IsPolarization · TauCeti.Hodge.MixedHodgeStructureCat.abelian · TauCeti.Hodge.PolarizableHodgeStructureCat · TauCeti.Hodge.Polarization.Q · The dual of a polarizable pure Hodge structure is polarizable · The Hodge decomposition · The Hodge numbers partition the dimension · When V is flat over ℤ, the Riemann forms for J are exactly the forms polarizing its weight-one Hodge structureStructureTauCeti.Hodge.IsPolarization#
The Hodge–Riemann bilinear relations for a fixed integral bilinear form Q on the lattice
of a weight-n Hodge structure.
The form is (-1)^n-symmetric and nondegenerate; its complexification annihilates
F p × F (n + 1 - p); and i^(p-q) Q x (conj x) is a positive real number for every nonzero x
in the Hodge component H^{p,q}, where q = n - p.
TauCeti.Hodge.IsPolarization.{u, v} {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ]
[_root_.Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) {n : ℤ}
(hs : TauCeti.Hodge.HodgeStructure hℂ n) (Q : LinearMap.BilinForm ℤ V) : Prop
Uses 2 · Used by 9
J is a Riemann form for J, with no flatness assumption · Polarizable pure Hodge structures are closed under internal homs · Self-duality is invertible up to a nonzero integer · Semisimplicity of polarizable rational Hodge structures · TauCeti.Hodge.PolarizableHodgeStructureCat · TauCeti.Hodge.Polarization.Q · The dual of a polarizable pure Hodge structure is polarizable · When V is flat over ℤ, the Riemann forms for J are exactly the forms polarizing its weight-one Hodge structureDefinitionTauCeti.Hodge.Polarization.Q#
The complex bilinear form of a polarization, derived by complexifying the integral form.
TauCeti.Hodge.Polarization.Q.{u, v} {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ]
[_root_.Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ}
{hs : TauCeti.Hodge.HodgeStructure hℂ n} (P : TauCeti.Hodge.Polarization hℂ hs) :
LinearMap.BilinForm ℂ Vℂ
Uses 3 · Used by 6
J is a Riemann form for J, with no flatness assumption · Polarizable pure Hodge structures are closed under internal homs · Self-duality is invertible up to a nonzero integer · Semisimplicity of polarizable rational Hodge structures · The dual of a polarizable pure Hodge structure is polarizableDefinitionIsBaseChange.bilinForm#
Extend a bilinear form to an abstract base change, transporting Mathlib's tensor-product base change along the canonical equivalence.
IsBaseChange.bilinForm.{u_1, u_2, u_3, u_4} {R : Type u_1} {A : Type u_2} {M : Type u_3}
{N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M]
[_root_.Module R M] [AddCommMonoid N] [_root_.Module R N] [_root_.Module A N]
[IsScalarTower R A N] {f : M →ₗ[R] N} (h : IsBaseChange A f) (B : LinearMap.BilinForm R M) :
LinearMap.BilinForm A N
Used by 9
J is a Riemann form for J, with no flatness assumption · Polarizable pure Hodge structures are closed under internal homs · Self-duality is invertible up to a nonzero integer · Semisimplicity of polarizable rational Hodge structures · TauCeti.Hodge.IsPolarization · TauCeti.Hodge.Polarization.Q · The dual of a polarizable pure Hodge structure is polarizable · When V is flat over ℤ, the Riemann forms for J are exactly the forms polarizing its weight-one Hodge structureStructureTauCeti.Hodge.PolarizableHodgeStructureCat#
The category of finite-dimensional polarizable rational Hodge structures of weight n, with
integral, rational, and complex models in Type u.
The integral model is a finitely generated free lattice and determines the conjugation on the complexification. The rational model is the carrier on which morphisms are defined. Polarizability is retained only as a property, so no particular polarizing form is part of an object.
TauCeti.Hodge.PolarizableHodgeStructureCat.{u} (n : ℤ) : Type (u + 1)
Uses 2 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.