Rational substructures of pure Hodge structures #
A rational Hodge substructure is a rational subspace whose complexification is spanned by its
intersections with the Hodge components. This file packages that condition and equips the
complexified subspace with the pure Hodge structure it inherits from the ambient one, so that the
whole HodgeStructureOn API applies to it — in particular the Hodge decomposition of the
complexified subspace into its own components is HodgeStructureOn.isInternal_piece, not a second
copy of that argument.
Conjugation stability of the complexification is not a field of the structure: it holds for every
rational subspace, by rationalToComplexSubmodule_conj. Together with the spanning condition this
exhibits the complexification as a sub-Hodge structure in the sense of
TauCeti.Hodge.HodgeStructureOn.IsSubstructure, and the induced conjugation, filtration and
components are read off from that general construction.
The definition and its base-change interface are those specified in Layer L1 of
TauCetiRoadmap/HodgeStructures/README.md, following Voisin, Hodge Theory and Complex Algebraic
Geometry I, §7.1.2. The induced structure is what makes a rational Hodge substructure a subobject
of a Hodge structure, as the semisimplicity milestone of that layer requires.
The signatures of RationalHodgeSubstructure and RationalHodgeSubstructure.WC are adapted from
the roadmap's formal companion
HodgeStructures/Suggested.lean.
Main declarations #
TauCeti.Hodge.RationalHodgeSubstructure: a rational subspace split by the Hodge components.TauCeti.Hodge.RationalHodgeSubstructure.isSubstructure: its complexification is a sub-Hodge structure of the ambient pure Hodge structure, soTauCeti.Hodge.HodgeStructureOn.IsSubstructure.hodgeStructureequips it with the induced pure Hodge structure, whose Hodge components are the intersections with the ambient ones.TauCeti.Hodge.RationalHodgeSubstructure.ofIsSubstructure: conversely, a rational subspace whose complexification is a sub-Hodge structure is a rational Hodge substructure.TauCeti.Hodge.RationalHodgeSubstructure.ofRationalMorphismRangeand…ofRationalMorphismKer: the image and kernel of a rational linear map whose complexification is a morphism of pure Hodge structures, as rational Hodge substructures.- The
Lattice,BoundedOrderandIsModularLatticeinstances: rational Hodge substructures form a modular lattice under inclusion. TauCeti.Hodge.RationalHodgeSubstructure.exists_isAtom_le: over a finite-dimensional rational space that lattice is atomic, its atoms being the simple substructures.
structure
TauCeti.Hodge.RationalHodgeSubstructure
{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 ℂ ιℂ}
{n : ℤ}
(hℚ : IsBaseChange ℚ ιℚ)
(hs : HodgeStructure hℂ n)
:
Type v
A rational Hodge substructure of a pure Hodge structure.
Its rational subspace WQ complexifies to the sum of its intersections with the Hodge
components. Stability under conjugation is not a field: it follows from rationality via
rationalToComplexSubmodule_conj.
The underlying rational subspace.
- hodge_spanning : rationalToComplexSubmodule hℚ hℂ self.WQ = ⨆ (p : ℤ), rationalToComplexSubmodule hℚ hℂ self.WQ ⊓ HodgeStructureOn.piece hs p
The complexification is spanned by its intersections with the Hodge components.
Instances For
theorem
TauCeti.Hodge.RationalHodgeSubstructure.ext
{Vℤ : Type u}
{Vℚ : Type v}
{Vℂ : Type w}
{inst✝ : AddCommGroup Vℤ}
{inst✝¹ : AddCommGroup Vℚ}
{inst✝² : Module ℚ Vℚ}
{inst✝³ : AddCommGroup Vℂ}
{inst✝⁴ : Module ℂ Vℂ}
{ιℚ : Vℤ →ₗ[ℤ] Vℚ}
{ιℂ : Vℤ →ₗ[ℤ] Vℂ}
{hℂ : IsBaseChange ℂ ιℂ}
{n : ℤ}
{hℚ : IsBaseChange ℚ ιℚ}
{hs : HodgeStructure hℂ n}
{x y : RationalHodgeSubstructure hℚ hs}
(WQ : x.WQ = y.WQ)
:
theorem
TauCeti.Hodge.RationalHodgeSubstructure.ext_iff
{Vℤ : Type u}
{Vℚ : Type v}
{Vℂ : Type w}
{inst✝ : AddCommGroup Vℤ}
{inst✝¹ : AddCommGroup Vℚ}
{inst✝² : Module ℚ Vℚ}
{inst✝³ : AddCommGroup Vℂ}
{inst✝⁴ : Module ℂ Vℂ}
{ιℚ : Vℤ →ₗ[ℤ] Vℚ}
{ιℂ : Vℤ →ₗ[ℤ] Vℂ}
{hℂ : IsBaseChange ℂ ιℂ}
{n : ℤ}
{hℚ : IsBaseChange ℚ ιℚ}
{hs : HodgeStructure hℂ n}
{x y : RationalHodgeSubstructure hℚ hs}
:
noncomputable def
TauCeti.Hodge.RationalHodgeSubstructure.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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(W : RationalHodgeSubstructure hℚ hs)
:
The complexification of a rational Hodge substructure inside the ambient complexification.
Instances For
theorem
TauCeti.Hodge.RationalHodgeSubstructure.WC_def
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(W : RationalHodgeSubstructure hℚ hs)
:
The complexification of a rational Hodge substructure is the complexification of its rational subspace.
theorem
TauCeti.Hodge.RationalHodgeSubstructure.WC_eq_iSup_inf_piece
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(W : RationalHodgeSubstructure hℚ hs)
:
The complexification is the supremum of its intersections with the ambient Hodge components.
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.map_WC_conj
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(W : RationalHodgeSubstructure hℚ hs)
:
The complexification of a rational Hodge substructure is stable under conjugation.
theorem
TauCeti.Hodge.RationalHodgeSubstructure.conj_mem_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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(W : RationalHodgeSubstructure hℚ hs)
{x : Vℂ}
(hx : x ∈ W.WC)
:
Conjugation carries every vector of a rational Hodge substructure back into its complexification.
theorem
TauCeti.Hodge.RationalHodgeSubstructure.isSubstructure
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(W : RationalHodgeSubstructure hℚ hs)
:
The complexification of a rational Hodge substructure is a sub-Hodge structure of the ambient
pure Hodge structure: it is conjugation stable because it is rational, and spanned by its
intersections with the Hodge components by definition. The induced pure Hodge structure is
TauCeti.Hodge.HodgeStructureOn.IsSubstructure.hodgeStructure.
def
TauCeti.Hodge.RationalHodgeSubstructure.ofIsSubstructure
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(A : Submodule ℚ Vℚ)
(h : HodgeStructureOn.IsSubstructure hs (rationalToComplexSubmodule hℚ hℂ A))
:
A rational subspace whose complexification is a sub-Hodge structure is a rational Hodge
substructure. This is the converse of TauCeti.Hodge.RationalHodgeSubstructure.isSubstructure.
Instances For
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.ofIsSubstructure_WQ
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(A : Submodule ℚ Vℚ)
(h : HodgeStructureOn.IsSubstructure hs (rationalToComplexSubmodule hℚ hℂ A))
:
Subobjects cut out by rational morphisms #
def
TauCeti.Hodge.RationalHodgeSubstructure.ofRationalMorphismRange
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
{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 ℂ ι'ℂ}
{hs' : HodgeStructure h'ℂ n}
{f : Vℚ →ₗ[ℚ] V'ℚ}
(hf : HodgeStructureOn.IsMorphism hs hs' (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f))
:
RationalHodgeSubstructure h'ℚ hs'
The image of a rational Hodge morphism, as a rational Hodge substructure of the target: its complexification is the image of the complexified map, which is a sub-Hodge structure.
Instances For
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.ofRationalMorphismRange_WQ
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
{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 ℂ ι'ℂ}
{hs' : HodgeStructure h'ℂ n}
{f : Vℚ →ₗ[ℚ] V'ℚ}
(hf : HodgeStructureOn.IsMorphism hs hs' (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f))
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.ofRationalMorphismRange_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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
{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 ℂ ι'ℂ}
{hs' : HodgeStructure h'ℂ n}
{f : Vℚ →ₗ[ℚ] V'ℚ}
(hf : HodgeStructureOn.IsMorphism hs hs' (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f))
:
The complexification of the image of a rational Hodge morphism is the image of the complexified map.
def
TauCeti.Hodge.RationalHodgeSubstructure.ofRationalMorphismKer
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
{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 ℂ ι'ℂ}
{hs' : HodgeStructure h'ℂ n}
{f : Vℚ →ₗ[ℚ] V'ℚ}
(hf : HodgeStructureOn.IsMorphism hs hs' (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f))
:
The kernel of a rational Hodge morphism, as a rational Hodge substructure of the source: its complexification is the kernel of the complexified map, which is a sub-Hodge structure.
Instances For
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.ofRationalMorphismKer_WQ
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
{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 ℂ ι'ℂ}
{hs' : HodgeStructure h'ℂ n}
{f : Vℚ →ₗ[ℚ] V'ℚ}
(hf : HodgeStructureOn.IsMorphism hs hs' (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f))
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.ofRationalMorphismKer_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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
{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 ℂ ι'ℂ}
{hs' : HodgeStructure h'ℂ n}
{f : Vℚ →ₗ[ℚ] V'ℚ}
(hf : HodgeStructureOn.IsMorphism hs hs' (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f))
:
The complexification of the kernel of a rational Hodge morphism is the kernel of the complexified map.
The lattice of rational Hodge substructures #
Rational Hodge substructures are ordered by inclusion of their rational subspaces, and the intersection and the sum of two of them are again rational Hodge substructures. The resulting lattice is modular, being a sublattice of the lattice of rational subspaces, and it satisfies the descending chain condition as soon as the ambient rational space is finite-dimensional; so every nonzero rational Hodge substructure contains a simple one, an atom of this lattice.
@[instance_reducible]
instance
TauCeti.Hodge.RationalHodgeSubstructure.instLE
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
LE (RationalHodgeSubstructure hℚ hs)
@[instance_reducible]
instance
TauCeti.Hodge.RationalHodgeSubstructure.instLT
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
LT (RationalHodgeSubstructure hℚ hs)
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.le_def
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
{W₁ W₂ : RationalHodgeSubstructure hℚ hs}
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.lt_def
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
{W₁ W₂ : RationalHodgeSubstructure hℚ hs}
:
@[instance_reducible]
instance
TauCeti.Hodge.RationalHodgeSubstructure.instMax
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
Max (RationalHodgeSubstructure hℚ hs)
@[instance_reducible]
instance
TauCeti.Hodge.RationalHodgeSubstructure.instMin
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
Min (RationalHodgeSubstructure hℚ hs)
@[instance_reducible]
instance
TauCeti.Hodge.RationalHodgeSubstructure.instBot
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
Bot (RationalHodgeSubstructure hℚ hs)
@[instance_reducible]
instance
TauCeti.Hodge.RationalHodgeSubstructure.instTop
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
Top (RationalHodgeSubstructure hℚ hs)
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.sup_WQ
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(W₁ W₂ : RationalHodgeSubstructure hℚ hs)
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.inf_WQ
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(W₁ W₂ : RationalHodgeSubstructure hℚ hs)
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.bot_WQ
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.top_WQ
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
@[instance_reducible]
instance
TauCeti.Hodge.RationalHodgeSubstructure.instLattice
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
Lattice (RationalHodgeSubstructure hℚ hs)
@[instance_reducible]
instance
TauCeti.Hodge.RationalHodgeSubstructure.instBoundedOrder
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(W₁ W₂ : RationalHodgeSubstructure hℚ hs)
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.inf_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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(W₁ W₂ : RationalHodgeSubstructure hℚ hs)
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.bot_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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.top_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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.isCompl_iff_WQ
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
{W₁ W₂ : RationalHodgeSubstructure hℚ hs}
:
Two rational Hodge substructures are complementary exactly when their rational subspaces are.
instance
TauCeti.Hodge.RationalHodgeSubstructure.instIsModularLattice
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
@[simp]
theorem
TauCeti.Hodge.RationalHodgeSubstructure.finsetSup_WQ
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
(s : Finset (RationalHodgeSubstructure hℚ hs))
:
The rational subspace of a finite supremum of rational Hodge substructures.
theorem
TauCeti.Hodge.RationalHodgeSubstructure.WQ_strictMono
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
:
Passing to the underlying rational subspace is strictly monotone.
instance
TauCeti.Hodge.RationalHodgeSubstructure.instWellFoundedLTOfFiniteRat
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
[Module.Finite ℚ Vℚ]
:
theorem
TauCeti.Hodge.RationalHodgeSubstructure.exists_isAtom_le
{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 ℂ ιℂ}
{n : ℤ}
{hs : HodgeStructure hℂ n}
[Module.Finite ℚ Vℚ]
{W : RationalHodgeSubstructure hℚ hs}
(hW : W ≠ ⊥)
:
∃ (U : RationalHodgeSubstructure hℚ hs), IsAtom U ∧ U ≤ W
Every nonzero rational Hodge substructure contains a simple one. The simple substructures are the atoms of the lattice of rational Hodge substructures, and over a finite-dimensional rational space that lattice is atomic.