Internal homs of pure Hodge structures #
For pure Hodge structures V and W, the complex vector space Hom_ℂ(V, W) carries a pure
Hodge structure of weight weight W - weight V. Its conjugation sends a map f to
x ↦ conj (f (conj x)), and its degree-r component consists of the maps carrying the degree-p
component of V into the degree-p+r component of W.
Those degree-shifting subspaces are the construction: since a Hodge decomposition has only
finitely many nonzero components, every linear map is the finite sum of the compositions
proj_W^q ∘ f ∘ proj_V^p, so the degree-shifting subspaces decompose Hom_ℂ(V, W). Conjugation
exchanges them in complementary degrees, and they vanish in low degrees, so they form a Hodge
decomposition in the sense of TauCeti.Hodge.IsHodgeDecomposition. No finiteness hypothesis on
V or W is needed.
When V is finite-dimensional the construction agrees with the transport of the tensor product of
the dual Hodge structure on V^* and the Hodge structure on W along Mathlib's contraction
equivalence V^* ⊗ W ≃ₗ[ℂ] Hom_ℂ(V, W); that comparison is
TauCeti.Hodge.HodgeStructureOn.internalHom_piece_eq_comap.
The Weil operator of the internal hom conjugates a map by the two Weil operators,
C(f) = C_W ∘ f ∘ C_V⁻¹, and the internal hom is functorial in morphisms: contravariantly in V
and covariantly in W.
For integral structures on lattices V_ℤ and W_ℤ, with V_ℤ finite free, the internal hom is
an integral pure Hodge structure on the lattice Hom_ℤ(V_ℤ, W_ℤ): the complex-linear maps between
the complexifications are a complexification of the integral linear maps, whose lattice
conjugation is the internal-hom conjugation (TauCeti.Hodge.latticeConjugation_internalHom).
When V and W have the same weight, the internal hom has weight 0, and its real vectors of
type (0,0) — equivalently, its real vectors in F^0 — are exactly the morphisms of pure Hodge
structures V → W. For integral structures this reads Hom_HS(V, W) = Hom_ℤ(V, W) ∩ F^0: an
integral linear map is a Hodge morphism exactly when its complexification lies in F^0 of the
internal hom, the conjugation condition being automatic for complexified integral maps.
Main declarations #
TauCeti.Hodge.HodgeStructureOn.internalHom: the internal hom Hodge structure, of weightn₂ - n₁, withTauCeti.Hodge.HodgeStructureOn.internalHom_pieceits components.TauCeti.Hodge.HodgeStructureOn.map_mem_piece_of_mem_internalHom_piece: a degree-rmap sends the degree-pcomponent into the degree-p+rcomponent, andTauCeti.Hodge.HodgeStructureOn.mem_internalHom_piece_iffsays this characterizes the components.TauCeti.Hodge.HodgeStructureOn.map_mem_F_of_mem_internalHom_F: a map in filtration degree at leastrsendsF^p VintoF^{p+r} W, andTauCeti.Hodge.HodgeStructureOn.mem_internalHom_F_iffsays this characterizes the filtration.TauCeti.Hodge.HodgeStructureOn.id_mem_internalHom_pieceandTauCeti.Hodge.HodgeStructureOn.comp_mem_internalHom_piece: the identity has internal-hom degree0, and composing maps adds internal-hom degrees.TauCeti.Hodge.HodgeStructureOn.internalHom_piece_eq_comapandTauCeti.Hodge.HodgeStructureOn.internalHom_F_eq_comap: over a finite-dimensional source, the internal-hom components and filtration are the pullbacks of those ofV^* ⊗ Walong the contraction equivalence.TauCeti.Hodge.HodgeStructureOn.weilOperator_internalHom: the Weil operator of the internal hom is conjugation by the Weil operators, so thatTauCeti.Hodge.HodgeStructureOn.weilOperator_internalHom_apply_weilOperatorgivesC(f) (C_V x) = C_W (f x).TauCeti.Hodge.HodgeStructureOn.IsMorphism.internalHomMap: pre- and post-composition by morphisms is a morphism between internal homs.TauCeti.Hodge.HodgeStructureOn.isMorphism_iff_mem_internalHom_pieceandTauCeti.Hodge.HodgeStructureOn.isMorphism_iff_mem_internalHom_F: the morphisms of pure Hodge structures of the same weight are the real vectors of type(0,0)of the internal hom, or equivalently its real vectors inF^0.TauCeti.Hodge.HodgeStructure.Hom.ofMemInternalHomFandTauCeti.Hodge.HodgeStructure.Hom.exists_toIntLinearMap_eq_iff: an integral linear map is a morphism of integral pure Hodge structures exactly when its complexification lies inF^0of the internal hom.TauCeti.Hodge.HodgeStructure.internalHom: the internal hom of integral pure Hodge structures, on the lattice of integral linear maps, withTauCeti.Hodge.HodgeStructure.internalHom_F,…internalHom_pieceand…internalHom_weilOperatoridentifying its filtration, components and Weil operator with those of the complex internal hom.TauCeti.Hodge.HodgeStructure.Hom.internalHomMap: the morphismφ ↦ g ∘ φ ∘ fbetween integral internal homs induced by morphismsfandg, withTauCeti.Hodge.HodgeStructure.Hom.internalHomMap_idand…internalHomMap_compits functoriality.
This is the internal-hom companion to duals and tensor products for pure Hodge structures; the convention follows Peters--Steenbrink, Mixed Hodge Structures, §2.1.
The contraction V^* ⊗ W → Hom_ℂ(V, W) intertwines tensor-product conjugation with the
intrinsic conjugation on the space of linear maps.
The inverse of the finite-dimensional contraction equivalence intertwines internal-hom conjugation with tensor-product conjugation.
The internal hom of a pure Hodge structure of weight n₁ and one of weight n₂, as a
pure Hodge structure of weight n₂ - n₁ on the space of complex-linear maps.
Its components are the maps shifting Hodge degree by a fixed amount.
Instances For
The degree-r component of the internal hom is the space of maps shifting Hodge degree
by r.
The internal-hom filtration is the sum of the components shifting Hodge degree by at
least p.
The conjugate internal-hom filtration is the sum of the components shifting Hodge degree by less than the complementary index.
A map of internal-hom Hodge degree p carries the source component of degree a into the
target component of degree a + p.
A map lies in the degree-p internal-hom component exactly when it carries every source
component of degree a into the target component of degree a + p.
The identity map has internal-hom degree 0.
Composing a map of internal-hom degree p with one of internal-hom degree q gives a map of
internal-hom degree p + q.
A rank-one map made from a dual vector of degree p and a target vector of degree q has
internal-hom degree p + q.
The degree-r internal-hom component of a map, evaluated at a vector of Hodge degree a,
is the degree-a + r component of the value.
A map in the p-th step of the internal-hom filtration sends the q-th step of the source
filtration into the (p+q)-th step of the target filtration.
A map lies in the p-th step of the internal-hom filtration exactly when it sends every
step F^q of the source filtration into the step F^{p+q} of the target filtration.
The tensor presentation of the internal hom. Over a finite-dimensional source, the
degree-p internal-hom component is the pullback of the degree-p component of the tensor
product V^* ⊗ W along Mathlib's contraction equivalence.
In the tensor presentation, the internal-hom filtration is the pullback of the tensor-product
filtration on V^* ⊗ W.
The Weil operator of the internal hom #
The Weil operator of the internal hom is conjugation by the Weil operators: it sends a
map f to C_W ∘ f ∘ C_V⁻¹.
The Weil operators intertwine evaluation: C(f) (C_V x) = C_W (f x).
Morphisms as Hodge classes of the internal hom #
Morphisms are the real vectors of F^0 of the internal hom. A complex-linear map between
pure Hodge structures of the same weight is a morphism exactly when it lies in F^0 of the
internal hom and is fixed by the internal-hom conjugation.
Morphisms are the real Hodge classes of type (0,0) of the internal hom. A complex-linear
map between pure Hodge structures of the same weight is a morphism exactly when it lies in the
Hodge component H^{0,0} of the internal hom, which has weight 0, and is fixed by the
internal-hom conjugation.
A morphism of pure Hodge structures of the same weight lies in the Hodge component H^{0,0}
of the internal hom.
Functoriality of the internal hom. Pre-composition by a morphism into the source and
post-composition by a morphism out of the target, φ ↦ g ∘ φ ∘ f, is a morphism between the
internal homs.
The complex action of a morphism of integral pure Hodge structures lies in the Hodge
component H^{0,0} of the internal hom.
The complex action of a morphism of integral pure Hodge structures lies in F^0 of the
internal hom.
An integral linear map whose complexification lies in F^0 of the internal hom is a morphism
of integral pure Hodge structures.
Instances For
The integral map underlying TauCeti.Hodge.HodgeStructure.Hom.ofMemInternalHomF is the given
one.
Integral Hodge morphisms are the integral maps in F^0 of the internal hom. An integral
linear map underlies a morphism of integral pure Hodge structures exactly when its
complexification lies in F^0 of the internal hom: Hom_HS(V, W) = Hom_ℤ(V, W) ∩ F^0.
The internal hom of two integral Hodge structures #
The internal hom of two integral pure Hodge structures, of weight n₂ - n₁. It is carried
by the lattice of integral linear maps Hom_ℤ(V₁, V₂), and its Hodge filtration is that of the
internal hom of the complex Hodge structures (HodgeStructure.internalHom_F).
Instances For
The Hodge filtration of the internal hom of two integral Hodge structures is that of the internal hom of the complex Hodge structures.
The Hodge components of the internal hom of two integral Hodge structures are those of the internal hom of the complex Hodge structures.
The Weil operator of the integral internal hom is conjugation by the Weil operators.
The morphism φ ↦ g ∘ φ ∘ f between integral internal homs induced by a morphism f into the
source and a morphism g out of the target.
Instances For
The integral map underlying TauCeti.Hodge.HodgeStructure.Hom.internalHomMap is pre- and
post-composition by the integral maps.
The morphism between integral internal homs acts on a complex-linear map by pre- and post-composition.
The internal hom of identity morphisms is the identity.
The internal hom is functorial: contravariant in the source and covariant in the target.