Conjugation and maps on complexifications

This file packages a conjugation on a complex vector space as a conjugate-linear involution and bundles the canonical conjugation on the tensor complexification of a real vector space. It also constructs the canonical conjugation on any abstract complexification of an integral module using Mathlib's IsBaseChange interface: it transports coordinatewise conjugation on ℂ ⊗[ℤ] V to an arbitrary complex base-change model and is uniquely characterized by fixing the image of V. The same interface canonically complexifies integral linear maps between abstract complexification models.

Main declarations

• TauCeti.Hodge.Conjugation: a conjugate-linear involution of a complex vector space.
• TauCeti.Hodge.complexificationConjugation: the canonical conjugation on the complexification of a real vector space, bundled as a Hodge conjugation.
• LinearMap.map_eigenspace_baseChange: canonical conjugation carries each eigenspace of a complexified real-linear endomorphism to the eigenspace of the conjugate eigenvalue.
• TauCeti.Hodge.Conjugation.tensorProduct: the tensor product of two conjugations.
• TauCeti.Hodge.Conjugation.tensorProduct_toEquiv_tmul: its action on pure tensors.
• TauCeti.Hodge.Conjugation.internalHom: conjugation on the space of complex-linear maps, acting by conjugating the input and output.
• TauCeti.Hodge.Conjugation.conjFiltration: the conjugate of a complex filtration.
• TauCeti.Hodge.concreteLatticeConj: conjugation on the tensor model ℂ ⊗[ℤ] V.
• TauCeti.Hodge.latticeConj: conjugation on an abstract complex base-change model.
• TauCeti.Hodge.latticeConj_unique: uniqueness among conjugate-linear maps fixing the integral module.
• TauCeti.Hodge.Conjugation.restrict: the conjugation induced on a stable complex subspace.
• TauCeti.Hodge.Conjugation.quotient: the conjugation induced on the quotient by a stable complex subspace.
• TauCeti.Hodge.Conjugation.map_comap_eq_comap_map: a linear map intertwining two conjugations exchanges conjugation with taking preimages of subspaces.
• TauCeti.Hodge.Conjugation.map_prod: a conjugation acting componentwise on a product carries a product subspace to the product of the conjugate subspaces.
• TauCeti.Hodge.Conjugation.dual: the twisted transpose of a conjugation, again a conjugation, on the complex dual space, with its pointwise description TauCeti.Hodge.Conjugation.dual_toEquiv_apply.
• TauCeti.Hodge.Conjugation.map_dualAnnihilator: a conjugation carries dual annihilators to dual annihilators of conjugated subspaces.
• TauCeti.Hodge.latticeConjugation: the abstract map bundled as a Conjugation.
• TauCeti.Hodge.integralMapToComplex: complexification of an integral linear map between abstract complexification models.
• TauCeti.Hodge.tensorLatticeMap and TauCeti.Hodge.isBaseChange_tensorLatticeMap: the tensor product of two complexifications is a complexification of the tensor product of the lattices.
• TauCeti.Hodge.tensorLatticeMap_injective: a flat tensor product lattice embeds in the tensor product of its complexifications.
• TauCeti.Hodge.latticeConjugation_tensorProduct: its lattice conjugation is the tensor product of the two lattice conjugations.
• TauCeti.Hodge.dualLatticeMap and TauCeti.Hodge.isBaseChange_dualLatticeMap: the complex dual of a complexification of a finite free lattice is a complexification of the dual lattice.
• TauCeti.Hodge.latticeConjugation_dual: its lattice conjugation is the twisted transpose of the lattice conjugation, and TauCeti.Hodge.integralMapToComplex_dualMap says that complexifying the transpose of an integral map gives the transpose of its complexification.
• TauCeti.Hodge.homLatticeMap and TauCeti.Hodge.isBaseChange_homLatticeMap: the space of complex-linear maps between two complexifications, the source lattice being finite free, is a complexification of the space of integral linear maps between the lattices.
• TauCeti.Hodge.integralMapToComplex_dualTensorHom and TauCeti.Hodge.integralMapToComplex_dualTensorHomEquiv_symm: contraction and its inverse commute with complexification.
• TauCeti.Hodge.latticeConjugation_internalHom: its lattice conjugation is the internal-hom conjugation, and TauCeti.Hodge.integralMapToComplex_lcomp_comp_llcomp says that complexifying pre- and post-composition by integral maps gives pre- and post-composition by their complexifications.

The base-change design follows the discussion by Johan Commelin, Andrew Yang, Kevin Buzzard, and Joël Riou in the #mathlib4 Zulip thread Complexifications with a view towards Hodge theory. The opposed-filtration formulation that consumes this conjugation is Deligne's, Théorie de Hodge II, §1.2.1.

structure TauCeti.Hodge.Conjugation (W : Type u) [AddCommGroup W] [Module ℂ W] : Type u

A conjugation on a complex vector space: a conjugate-linear involution.

• toEquiv : W ≃ₗ⋆[ℂ] W

  The conjugate-linear equivalence underlying the conjugation.

• involutive : Function.Involutive ⇑self.toEquiv

  Applying the conjugation twice is the identity.

theorem TauCeti.Hodge.Conjugation.ext {W : Type u} {inst✝ : AddCommGroup W} {inst✝¹ : Module ℂ W} {x y : Conjugation W} (toEquiv : x.toEquiv = y.toEquiv) : x = y

theorem TauCeti.Hodge.Conjugation.ext_iff {W : Type u} {inst✝ : AddCommGroup W} {inst✝¹ : Module ℂ W} {x y : Conjugation W} : x = y ↔ x.toEquiv = y.toEquiv

noncomputable def TauCeti.Hodge.complexificationConjugation (V : Type u) [AddCommGroup V] [Module ℝ V] : Conjugation (TensorProduct ℝ ℂ V)

The canonical conjugation on the complexification of a real vector space, bundled as a conjugate-linear involution.

@[simp]

theorem TauCeti.Hodge.complexificationConjugation_toEquiv_apply (V : Type u) [AddCommGroup V] [Module ℝ V] (x : TensorProduct ℝ ℂ V) : (complexificationConjugation V).toEquiv x = (tmulConj V) x

The bundled canonical conjugation agrees with tensor conjugation on every vector.

theorem TauCeti.Hodge.complexificationConjugation_toEquiv_tmul (V : Type u) [AddCommGroup V] [Module ℝ V] (z : ℂ) (v : V) : (complexificationConjugation V).toEquiv (z ⊗ₜ[ℝ] v) = (starRingEnd ℂ) z ⊗ₜ[ℝ] v

Canonical conjugation on a complexification conjugates the complex coefficient of a pure tensor and fixes its real factor.

@[simp]

theorem LinearMap.map_eigenspace_baseChange {V : Type u} [AddCommGroup V] [Module ℝ V] (f : V →ₗ[ℝ] V) (z : ℂ) : Submodule.map (↑(TauCeti.Hodge.complexificationConjugation V).toEquiv) (Module.End.eigenspace (baseChange ℂ f) z) = Module.End.eigenspace (baseChange ℂ f) ((starRingEnd ℂ) z)

Canonical conjugation carries the z-eigenspace of a complexified real-linear endomorphism to its conjugate-eigenvalue eigenspace.

@[simp]

theorem TauCeti.Hodge.Conjugation.toEquiv_symm {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) : ω.toEquiv.symm = ω.toEquiv

The inverse of a conjugation is the conjugation itself.

@[simp]

theorem TauCeti.Hodge.Conjugation.apply_apply {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (x : W) : ω.toEquiv (ω.toEquiv x) = x

Applying a conjugation twice returns the original vector.

def TauCeti.Hodge.Conjugation.tensorProduct {W₁ : Type u} {W₂ : Type v} [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] (ω₁ : Conjugation W₁) (ω₂ : Conjugation W₂) : Conjugation (TensorProduct ℂ W₁ W₂)

The tensor product of two conjugate-linear involutions.

@[simp]

theorem TauCeti.Hodge.Conjugation.tensorProduct_toEquiv_tmul {W₁ : Type u} {W₂ : Type v} [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] (ω₁ : Conjugation W₁) (ω₂ : Conjugation W₂) (x : W₁) (y : W₂) : (ω₁.tensorProduct ω₂).toEquiv (x ⊗ₜ[ℂ] y) = ω₁.toEquiv x ⊗ₜ[ℂ] ω₂.toEquiv y

Tensor-product conjugation acts componentwise on pure tensors.

def TauCeti.Hodge.Conjugation.internalHom {W₁ : Type u} {W₂ : Type v} [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] (ω₁ : Conjugation W₁) (ω₂ : Conjugation W₂) : Conjugation (W₁ →ₗ[ℂ] W₂)

The conjugation on the internal hom of two complex vector spaces with conjugation. It sends f : W₁ →ₗ[ℂ] W₂ to x ↦ ω₂ (f (ω₁ x)).

@[simp]

theorem TauCeti.Hodge.Conjugation.internalHom_toEquiv_apply_apply {W₁ : Type u} {W₂ : Type v} [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] (ω₁ : Conjugation W₁) (ω₂ : Conjugation W₂) (f : W₁ →ₗ[ℂ] W₂) (x : W₁) : ((ω₁.internalHom ω₂).toEquiv f) x = ω₂.toEquiv (f (ω₁.toEquiv x))

Conjugation on an internal hom conjugates the input and output.

theorem TauCeti.Hodge.Conjugation.internalHom_toEquiv_eq_self_iff {W₁ : Type u} {W₂ : Type v} [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] (ω₁ : Conjugation W₁) (ω₂ : Conjugation W₂) (f : W₁ →ₗ[ℂ] W₂) : (ω₁.internalHom ω₂).toEquiv f = f ↔ ∀ (x : W₁), f (ω₁.toEquiv x) = ω₂.toEquiv (f x)

A complex-linear map is fixed by the internal-hom conjugation exactly when it intertwines the two conjugations.

@[simp]

theorem TauCeti.Hodge.Conjugation.map_map_eq_self {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (U : Submodule ℂ W) : Submodule.map (↑ω.toEquiv) (Submodule.map (↑ω.toEquiv) U) = U

Mapping a complex subspace twice by a conjugation returns the original subspace.

def TauCeti.Hodge.Conjugation.conjFiltration {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (F : ℤ → Submodule ℂ W) (p : ℤ) : Submodule ℂ W

The conjugate filtration obtained by mapping each step through a conjugation.

theorem TauCeti.Hodge.Conjugation.conjFiltration_def {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (F : ℤ → Submodule ℂ W) (p : ℤ) : ω.conjFiltration F p = Submodule.map (↑ω.toEquiv) (F p)

A conjugate filtration step is the image of the original step under conjugation.

theorem TauCeti.Hodge.Conjugation.conjFiltration_antitone {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) {F : ℤ → Submodule ℂ W} (hF : Antitone F) : Antitone (ω.conjFiltration F)

Conjugating an antitone filtration produces an antitone filtration.

@[simp]

theorem TauCeti.Hodge.Conjugation.mem_conjFiltration_iff {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (F : ℤ → Submodule ℂ W) (p : ℤ) (x : W) : x ∈ ω.conjFiltration F p ↔ ω.toEquiv x ∈ F p

Membership in a conjugate filtration step is detected by applying the conjugation.

@[simp]

theorem TauCeti.Hodge.Conjugation.conjFiltration_conjFiltration {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (F : ℤ → Submodule ℂ W) (p : ℤ) : Submodule.map (↑ω.toEquiv) (ω.conjFiltration F p) = F p

Applying conjugation to a conjugate filtration step recovers the original step.

theorem TauCeti.Hodge.Conjugation.map_conjFiltration_le {W : Type u} [AddCommGroup W] [Module ℂ W] {W' : Type v} [AddCommGroup W'] [Module ℂ W'] (ω : Conjugation W) (ω' : Conjugation W') (F : ℤ → Submodule ℂ W) (F' : ℤ → Submodule ℂ W') (f : W →ₗ[ℂ] W') (hcomm : ∀ (x : W), f (ω.toEquiv x) = ω'.toEquiv (f x)) {p : ℤ} (hF : Submodule.map f (F p) ≤ F' p) : Submodule.map f (ω.conjFiltration F p) ≤ ω'.conjFiltration F' p

A linear map commuting with two conjugations carries the conjugate of a preserved filtration step into the corresponding conjugate filtration step.

def TauCeti.Hodge.Conjugation.restrict {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) {U : Submodule ℂ W} (hU : ∀ x ∈ U, ω.toEquiv x ∈ U) : Conjugation ↥U

The conjugation induced on a complex subspace stable under a given conjugation.

@[simp]

theorem TauCeti.Hodge.Conjugation.restrict_toEquiv_apply {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) {U : Submodule ℂ W} (hU : ∀ x ∈ U, ω.toEquiv x ∈ U) (x : ↥U) : ↑((ω.restrict hU).toEquiv x) = ω.toEquiv ↑x

A restricted conjugation acts as the ambient one.

@[simp]

theorem TauCeti.Hodge.Conjugation.map_restrict_comap_subtype {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) {U : Submodule ℂ W} (hU : ∀ x ∈ U, ω.toEquiv x ∈ U) (A : Submodule ℂ W) : Submodule.map (↑(ω.restrict hU).toEquiv) (Submodule.comap U.subtype A) = Submodule.comap U.subtype (Submodule.map (↑ω.toEquiv) A)

Conjugating inside a stable subspace is conjugating in the ambient space: the image of an intersection with the subspace under the restricted conjugation is the intersection with the conjugate subspace.

theorem TauCeti.Hodge.Conjugation.map_comap_eq_comap_map {W : Type u} [AddCommGroup W] [Module ℂ W] {W' : Type v} [AddCommGroup W'] [Module ℂ W'] (ω : Conjugation W) (ω' : Conjugation W') (f : W →ₗ[ℂ] W') (hf : ∀ (x : W), f (ω.toEquiv x) = ω'.toEquiv (f x)) (A : Submodule ℂ W') : Submodule.map (↑ω.toEquiv) (Submodule.comap f A) = Submodule.comap f (Submodule.map (↑ω'.toEquiv) A)

A linear map intertwining two conjugations exchanges conjugating a preimage with taking the preimage of the conjugate.

def TauCeti.Hodge.Conjugation.quotient {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) {U : Submodule ℂ W} (hU : ∀ x ∈ U, ω.toEquiv x ∈ U) : Conjugation (W ⧸ U)

The conjugation induced on the quotient of a complex vector space by a stable subspace.

@[simp]

theorem TauCeti.Hodge.Conjugation.quotient_toEquiv_mk {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) {U : Submodule ℂ W} (hU : ∀ x ∈ U, ω.toEquiv x ∈ U) (x : W) : (ω.quotient hU).toEquiv (Submodule.Quotient.mk x) = Submodule.Quotient.mk (ω.toEquiv x)

The induced conjugation on a quotient acts on classes through the ambient conjugation.

def TauCeti.Hodge.Conjugation.dual {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) : Conjugation (Module.Dual ℂ W)

The twisted transpose of a conjugation ω: a functional φ acts by conjugating the values of φ along ω. It is again an involution, so it packages as a conjugation on the dual space; see TauCeti.Hodge.Conjugation.dual_toEquiv_apply for its pointwise description.

@[simp]

theorem TauCeti.Hodge.Conjugation.dual_toEquiv_apply {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (φ : Module.Dual ℂ W) (v : W) : (ω.dual.toEquiv φ) v = star (φ (ω.toEquiv v))

Pointwise description of the dual conjugation.

@[simp]

theorem TauCeti.Hodge.Conjugation.map_dualAnnihilator {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (U : Submodule ℂ W) : Submodule.map (↑ω.dual.toEquiv) U.dualAnnihilator = (Submodule.map (↑ω.toEquiv) U).dualAnnihilator

A conjugation carries dual annihilators to dual annihilators of conjugated subspaces.

@[reducible, inline]

abbrev TauCeti.Hodge.Complexification (V : Type u) [AddCommGroup V] : Type u

The canonical complexification ℂ ⊗[ℤ] V of an integral module.

def TauCeti.Hodge.complexificationMap {V : Type u} [AddCommGroup V] : V →ₗ[ℤ] Complexification V

The canonical map from an integral module to its tensor-product complexification.

theorem TauCeti.Hodge.isBaseChange_complexificationMap {V : Type u} [AddCommGroup V] : IsBaseChange ℂ complexificationMap

The tensor-product complexification satisfies the abstract base-change interface.

noncomputable def TauCeti.Hodge.concreteLatticeConj {V : Type u} [AddCommGroup V] : Complexification V →ₗ⋆[ℂ] Complexification V

Lattice-induced conjugation on the tensor model ℂ ⊗[ℤ] V, acting by complex conjugation on the scalar tensor factor and by the identity on the integral module.

@[simp]

theorem TauCeti.Hodge.concreteLatticeConj_tmul {V : Type u} [AddCommGroup V] (z : ℂ) (v : V) : concreteLatticeConj (z ⊗ₜ[ℤ] v) = (starRingEnd ℂ) z ⊗ₜ[ℤ] v

Conjugation on the tensor model conjugates the scalar in a pure tensor.

@[simp]

theorem TauCeti.Hodge.concreteLatticeConj_complexificationMap {V : Type u} [AddCommGroup V] (v : V) : concreteLatticeConj (complexificationMap v) = complexificationMap v

Conjugation on the tensor model fixes the image of the integral module.

theorem TauCeti.Hodge.concreteLatticeConj_involutive {V : Type u} [AddCommGroup V] : Function.Involutive ⇑concreteLatticeConj

Conjugation on the tensor model is involutive.

@[simp]

theorem TauCeti.Hodge.concreteLatticeConj_apply_apply {V : Type u} [AddCommGroup V] (x : Complexification V) : concreteLatticeConj (concreteLatticeConj x) = x

Applying conjugation on the tensor model twice returns the original vector.

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

Lattice-induced conjugation on an abstract complex base-change model.

@[simp]

theorem TauCeti.Hodge.latticeConj_ι {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (v : V) : (latticeConj hℂ) (ιℂ v) = ιℂ v

Abstract lattice-induced conjugation fixes the image of the integral module.

theorem TauCeti.Hodge.latticeConj_involutive {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) : Function.Involutive ⇑(latticeConj hℂ)

Abstract lattice-induced conjugation is involutive.

@[simp]

theorem TauCeti.Hodge.latticeConj_apply_apply {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (x : Vℂ) : (latticeConj hℂ) ((latticeConj hℂ) x) = x

Applying abstract lattice-induced conjugation twice returns the original vector.

theorem TauCeti.Hodge.latticeConj_unique {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (c : Vℂ →ₗ⋆[ℂ] Vℂ) (hc : ∀ (v : V), c (ιℂ v) = ιℂ v) : c = latticeConj hℂ

Lattice-induced conjugation is the unique conjugate-linear map on an abstract complexification that fixes every integral vector.

theorem TauCeti.Hodge.latticeConj_complexificationMap {V : Type u} [AddCommGroup V] : latticeConj ⋯ = concreteLatticeConj

On the canonical tensor-product model, abstract lattice-induced conjugation is the concrete tensor map.

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

Lattice-induced conjugation on an abstract complexification, bundled as a conjugation.

@[simp]

theorem TauCeti.Hodge.latticeConjugation_toEquiv_apply {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (x : Vℂ) : (latticeConjugation hℂ).toEquiv x = (latticeConj hℂ) x

The equivalence underlying bundled lattice conjugation applies as latticeConj.

theorem TauCeti.Hodge.latticeConjugation_toLinearMap {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) : ↑(latticeConjugation hℂ).toEquiv = latticeConj hℂ

The linear map underlying bundled lattice conjugation is latticeConj, bridging the bundled spelling used by HodgeStructureOn and the bare spelling used by the base-change API. This is not a simp lemma: rewriting with it discards the equivalence, and with it simp's ability to see that conjugating a subspace preserves ⊤.

theorem TauCeti.Hodge.latticeConjugation_toEquiv_ι {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (v : V) : (latticeConjugation hℂ).toEquiv (ιℂ v) = ιℂ v

Bundled lattice conjugation fixes the image of the integral module.

noncomputable def TauCeti.Hodge.integralMapToComplex {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} (h₁ : IsBaseChange ℂ ι₁) (ι₂ : V₂ →ₗ[ℤ] W₂) (f : V₁ →ₗ[ℤ] V₂) : W₁ →ₗ[ℂ] W₂

The complexification of an integral linear map between abstract complexification models.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_apply_ι {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} (h₁ : IsBaseChange ℂ ι₁) (ι₂ : V₂ →ₗ[ℤ] W₂) (f : V₁ →ₗ[ℤ] V₂) (x : V₁) : (integralMapToComplex h₁ ι₂ f) (ι₁ x) = ι₂ (f x)

Complexification agrees with the target lattice map on integral vectors.

noncomputable def TauCeti.Hodge.homLatticeMap {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} (h₁ : IsBaseChange ℂ ι₁) (ι₂ : V₂ →ₗ[ℤ] W₂) : (V₁ →ₗ[ℤ] V₂) →ₗ[ℤ] W₁ →ₗ[ℂ] W₂

The integral structure map φ ↦ integralMapToComplex h₁ ι₂ φ of the space of complex-linear maps between two complexifications: an integral linear map between the lattices extends complex-linearly to the complexifications (TauCeti.Hodge.homLatticeMap_apply).

It is Mathlib's IsBaseChange.linearMapLeftRightHom, restated through AddMonoidHom.toIntLinearMap so that both spaces of linear maps carry their canonical ℤ-module structures: a space of linear maps also carries the ℤ-module structure of LinearMap.module, which is equal but not reducibly defeq to the canonical one that the lattice API of this file is stated for.

@[simp]

theorem TauCeti.Hodge.homLatticeMap_apply {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} (h₁ : IsBaseChange ℂ ι₁) (ι₂ : V₂ →ₗ[ℤ] W₂) (f : V₁ →ₗ[ℤ] V₂) : (homLatticeMap h₁ ι₂) f = integralMapToComplex h₁ ι₂ f

The structure map of a space of linear maps between complexifications sends an integral linear map to its complexification.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_id {V₁ : Type u₁} {W₁ : Type v₁} [AddCommGroup V₁] [AddCommGroup W₁] [Module ℂ W₁] {ι₁ : V₁ →ₗ[ℤ] W₁} (h₁ : IsBaseChange ℂ ι₁) : integralMapToComplex h₁ ι₁ LinearMap.id = LinearMap.id

Complexification sends the identity integral map to the identity complex map.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_zero {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} (h₁ : IsBaseChange ℂ ι₁) (ι₂ : V₂ →ₗ[ℤ] W₂) : integralMapToComplex h₁ ι₂ 0 = 0

Complexification sends the zero integral map to the zero complex map.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_add {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} (h₁ : IsBaseChange ℂ ι₁) (ι₂ : V₂ →ₗ[ℤ] W₂) (f g : V₁ →ₗ[ℤ] V₂) : integralMapToComplex h₁ ι₂ (f + g) = integralMapToComplex h₁ ι₂ f + integralMapToComplex h₁ ι₂ g

Complexification preserves addition of integral linear maps.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_neg {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} (h₁ : IsBaseChange ℂ ι₁) (ι₂ : V₂ →ₗ[ℤ] W₂) (f : V₁ →ₗ[ℤ] V₂) : integralMapToComplex h₁ ι₂ (-f) = -integralMapToComplex h₁ ι₂ f

Complexification preserves negation of integral linear maps.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_sub {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} (h₁ : IsBaseChange ℂ ι₁) (ι₂ : V₂ →ₗ[ℤ] W₂) (f g : V₁ →ₗ[ℤ] V₂) : integralMapToComplex h₁ ι₂ (f - g) = integralMapToComplex h₁ ι₂ f - integralMapToComplex h₁ ι₂ g

Complexification preserves subtraction of integral linear maps.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_nsmul {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} (h₁ : IsBaseChange ℂ ι₁) (ι₂ : V₂ →ₗ[ℤ] W₂) (k : ℕ) (f : V₁ →ₗ[ℤ] V₂) : integralMapToComplex h₁ ι₂ (k • f) = k • integralMapToComplex h₁ ι₂ f

Complexification preserves natural-number multiples of integral linear maps.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_zsmul {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} (h₁ : IsBaseChange ℂ ι₁) (ι₂ : V₂ →ₗ[ℤ] W₂) (k : ℤ) (f : V₁ →ₗ[ℤ] V₂) : integralMapToComplex h₁ ι₂ (k • f) = k • integralMapToComplex h₁ ι₂ f

Complexification preserves integer multiples of integral linear maps.

theorem TauCeti.Hodge.integralMapToComplex_comp {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃} {W₁ : Type v₁} {W₂ : Type v₂} {W₃ : Type v₃} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] [AddCommGroup W₃] [Module ℂ W₃] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} (h₁ : IsBaseChange ℂ ι₁) (h₂ : IsBaseChange ℂ ι₂) (ι₃ : V₃ →ₗ[ℤ] W₃) (f : V₁ →ₗ[ℤ] V₂) (g : V₂ →ₗ[ℤ] V₃) : integralMapToComplex h₁ ι₃ (g ∘ₗ f) = integralMapToComplex h₂ ι₃ g ∘ₗ integralMapToComplex h₁ ι₂ f

Complexification preserves composition of integral linear maps.

theorem TauCeti.Hodge.integralMapToComplex_injective {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} (h₁ : IsBaseChange ℂ ι₁) (h₂ : IsBaseChange ℂ ι₂) {f : V₁ →ₗ[ℤ] V₂} (hf : Function.Injective ⇑f) : Function.Injective ⇑(integralMapToComplex h₁ ι₂ f)

Complexification preserves injectivity of integral linear maps, because ℂ is flat over ℤ.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_commutes_conj {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} (h₁ : IsBaseChange ℂ ι₁) (h₂ : IsBaseChange ℂ ι₂) (f : V₁ →ₗ[ℤ] V₂) (x : W₁) : (integralMapToComplex h₁ ι₂ f) ((latticeConj h₁) x) = (latticeConj h₂) ((integralMapToComplex h₁ ι₂ f) x)

The complexification of an integral map commutes with lattice-induced conjugation.

theorem TauCeti.Hodge.Conjugation.map_prod {W : Type u_3} {W' : Type u_4} [AddCommGroup W] [Module ℂ W] [AddCommGroup W'] [Module ℂ W'] {ω : Conjugation W} {ω' : Conjugation W'} {Ω : Conjugation (W × W')} (hΩ : ∀ (x : W × W'), Ω.toEquiv x = (ω.toEquiv x.1, ω'.toEquiv x.2)) (U : Submodule ℂ W) (U' : Submodule ℂ W') : Submodule.map (↑Ω.toEquiv) (U.prod U') = (Submodule.map (↑ω.toEquiv) U).prod (Submodule.map (↑ω'.toEquiv) U')

A conjugation acting componentwise on a product carries a product subspace to the product of the conjugate subspaces.

The hypothesis is what TauCeti.Hodge.latticeConjugation_prodMap_toEquiv_apply supplies for the canonical conjugation of a product of complexifications.

@[simp]

theorem TauCeti.Hodge.latticeConj_prodMap {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℂ : V' →ₗ[ℤ] V'ℂ} (hℂ : IsBaseChange ℂ ιℂ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (x : Vℂ × V'ℂ) : (latticeConj ⋯) x = ((latticeConj hℂ) x.1, (latticeConj h'ℂ) x.2)

Lattice conjugation acts componentwise on a product of complexifications.

theorem TauCeti.Hodge.latticeConjugation_prodMap_toEquiv_apply {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℂ : V' →ₗ[ℤ] V'ℂ} (hℂ : IsBaseChange ℂ ιℂ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (x : Vℂ × V'ℂ) : (latticeConjugation ⋯).toEquiv x = ((latticeConjugation hℂ).toEquiv x.1, (latticeConjugation h'ℂ).toEquiv x.2)

The bundled lattice conjugation of a product of complexifications acts componentwise.

@[simp]

theorem TauCeti.Hodge.map_latticeConj_prod {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℂ : V' →ₗ[ℤ] V'ℂ} (hℂ : IsBaseChange ℂ ιℂ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (U : Submodule ℂ Vℂ) (U' : Submodule ℂ V'ℂ) : Submodule.map (latticeConj ⋯) (U.prod U') = (Submodule.map (latticeConj hℂ) U).prod (Submodule.map (latticeConj h'ℂ) U')

Conjugation of a product subspace is the product of the conjugate subspaces.

noncomputable def TauCeti.Hodge.tensorLatticeMap {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] (ιℂ : V →ₗ[ℤ] Vℂ) {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] (ι'ℂ : V' →ₗ[ℤ] V'ℂ) : TensorProduct ℤ V V' →ₗ[ℤ] TensorProduct ℂ Vℂ V'ℂ

The integral structure map v ⊗ v' ↦ ιℂ v ⊗ ι'ℂ v' of a tensor product of two complexifications.

It is the map of IsBaseChange.tensorProduct, restated through AddMonoidHom.toIntLinearMap so that both sides carry their canonical ℤ-module structures: a tensor product also carries the ℤ-module structure induced from a factor, which is equal but not reducibly defeq to the canonical one that the lattice API of this file is stated for.

@[simp]

theorem TauCeti.Hodge.tensorLatticeMap_tmul {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℂ : V' →ₗ[ℤ] V'ℂ} (v : V) (v' : V') : (tensorLatticeMap ιℂ ι'ℂ) (v ⊗ₜ[ℤ] v') = ιℂ v ⊗ₜ[ℂ] ι'ℂ v'

The structure map of a tensor product of complexifications on a pure tensor.

theorem TauCeti.Hodge.isBaseChange_tensorLatticeMap {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℂ : V' →ₗ[ℤ] V'ℂ} (hℂ : IsBaseChange ℂ ιℂ) (h'ℂ : IsBaseChange ℂ ι'ℂ) : IsBaseChange ℂ (tensorLatticeMap ιℂ ι'ℂ)

The tensor product of two complexifications is a complexification of the tensor product of the two lattices.

theorem TauCeti.Hodge.tensorLatticeMap_injective {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℂ : V' →ₗ[ℤ] V'ℂ} [Module.Flat ℤ (TensorProduct ℤ V V')] (hℂ : IsBaseChange ℂ ιℂ) (h'ℂ : IsBaseChange ℂ ι'ℂ) : Function.Injective ⇑(tensorLatticeMap ιℂ ι'ℂ)

A flat tensor product lattice embeds in the tensor product of its complexifications.

@[simp]

theorem TauCeti.Hodge.latticeConj_tensorLatticeMap_tmul {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℂ : V' →ₗ[ℤ] V'ℂ} (hℂ : IsBaseChange ℂ ιℂ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (x : Vℂ) (y : V'ℂ) : (latticeConj ⋯) (x ⊗ₜ[ℂ] y) = (latticeConj hℂ) x ⊗ₜ[ℂ] (latticeConj h'ℂ) y

Lattice conjugation of a tensor product of complexifications conjugates both factors of a pure tensor.

theorem TauCeti.Hodge.latticeConjugation_tensorProduct {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℂ : V' →ₗ[ℤ] V'ℂ} (hℂ : IsBaseChange ℂ ιℂ) (h'ℂ : IsBaseChange ℂ ι'ℂ) : latticeConjugation ⋯ = (latticeConjugation hℂ).tensorProduct (latticeConjugation h'ℂ)

The lattice conjugation of a tensor product of complexifications is the tensor product of the two lattice conjugations.

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

The integral structure map f ↦ (ιℂ v ↦ f v) of the complex dual of a complexification: an integral functional on the lattice extends complex-linearly to the complexification.

It is Mathlib's IsBaseChange.toDual, restated through AddMonoidHom.toIntLinearMap so that the dual space carries its canonical ℤ-module structure: the space of complex functionals also carries the ℤ-module structure of LinearMap.module, which is equal but not reducibly defeq to the canonical one that the lattice API of this file is stated for.

@[simp]

theorem TauCeti.Hodge.dualLatticeMap_apply_ι {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (f : Module.Dual ℤ V) (v : V) : ((dualLatticeMap hℂ) f) (ιℂ v) = ↑(f v)

The extension of an integral functional takes the given integer values on integral vectors.

theorem TauCeti.Hodge.dual_latticeConjugation_toEquiv_dualLatticeMap {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (f : Module.Dual ℤ V) : (latticeConjugation hℂ).dual.toEquiv ((dualLatticeMap hℂ) f) = (dualLatticeMap hℂ) f

The twisted transpose of the lattice conjugation fixes the extension of every integral functional.

theorem TauCeti.Hodge.isBaseChange_dualLatticeMap {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} [Module.Free ℤ V] [Module.Finite ℤ V] (hℂ : IsBaseChange ℂ ιℂ) : IsBaseChange ℂ (dualLatticeMap hℂ)

The complex dual of a complexification of a finite free lattice is a complexification of the dual lattice.

@[simp]

theorem TauCeti.Hodge.latticeConj_dualLatticeMap_apply {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} [Module.Free ℤ V] [Module.Finite ℤ V] (hℂ : IsBaseChange ℂ ιℂ) (φ : Module.Dual ℂ Vℂ) (x : Vℂ) : ((latticeConj ⋯) φ) x = star (φ ((latticeConj hℂ) x))

Lattice conjugation on the complex dual of a complexification is the twisted transpose of the lattice conjugation: it conjugates the value of a functional at the conjugate vector.

theorem TauCeti.Hodge.latticeConjugation_dual {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} [Module.Free ℤ V] [Module.Finite ℤ V] (hℂ : IsBaseChange ℂ ιℂ) : latticeConjugation ⋯ = (latticeConjugation hℂ).dual

The lattice conjugation of the complex dual of a complexification is the twisted transpose of the lattice conjugation.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_dualMap {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} [Module.Free ℤ V] [Module.Finite ℤ V] {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℂ : V' →ₗ[ℤ] V'ℂ} (h'ℂ : IsBaseChange ℂ ι'ℂ) (hℂ : IsBaseChange ℂ ιℂ) (f : V' →ₗ[ℤ] V) : integralMapToComplex ⋯ (dualLatticeMap h'ℂ) f.dualMap = (integralMapToComplex h'ℂ ιℂ f).dualMap

Complexifying the transpose of an integral linear map gives the transpose of its complexification.

theorem TauCeti.Hodge.isBaseChange_homLatticeMap {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} [Module.Free ℤ V₁] [Module.Finite ℤ V₁] (h₁ : IsBaseChange ℂ ι₁) (h₂ : IsBaseChange ℂ ι₂) : IsBaseChange ℂ (homLatticeMap h₁ ι₂)

The space of complex-linear maps between two complexifications is a complexification of the space of integral linear maps between the lattices, when the source lattice is finite free.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_dualTensorHom {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} [Module.Free ℤ V₁] [Module.Finite ℤ V₁] (h₁ : IsBaseChange ℂ ι₁) (h₂ : IsBaseChange ℂ ι₂) : integralMapToComplex ⋯ (homLatticeMap h₁ ι₂) (dualTensorHom ℤ V₁ V₂).toAddMonoidHom.toIntLinearMap = dualTensorHom ℂ W₁ W₂

Complexifying the integral contraction V* ⊗ W → Hom(V, W) gives the complex contraction between the complexifications.

@[simp]

theorem TauCeti.Hodge.integralMapToComplex_dualTensorHomEquiv_symm {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} [Module.Free ℤ V₁] [Module.Finite ℤ V₁] [Module.Finite ℂ W₁] (h₁ : IsBaseChange ℂ ι₁) (h₂ : IsBaseChange ℂ ι₂) : integralMapToComplex ⋯ (tensorLatticeMap (dualLatticeMap h₁) ι₂) (↑(dualTensorHomEquiv ℤ V₁ V₂).symm).toAddMonoidHom.toIntLinearMap = ↑(dualTensorHomEquiv ℂ W₁ W₂).symm

Complexifying the inverse integral contraction gives the inverse complex contraction.

theorem TauCeti.Hodge.latticeConj_homLatticeMap_apply {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} [Module.Free ℤ V₁] [Module.Finite ℤ V₁] (h₁ : IsBaseChange ℂ ι₁) (h₂ : IsBaseChange ℂ ι₂) (φ : W₁ →ₗ[ℂ] W₂) (x : W₁) : ((latticeConj ⋯) φ) x = (latticeConj h₂) (φ ((latticeConj h₁) x))

Lattice conjugation on the space of complex-linear maps between two complexifications conjugates the input and the output of a map.

theorem TauCeti.Hodge.latticeConjugation_internalHom {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} [Module.Free ℤ V₁] [Module.Finite ℤ V₁] (h₁ : IsBaseChange ℂ ι₁) (h₂ : IsBaseChange ℂ ι₂) : latticeConjugation ⋯ = (latticeConjugation h₁).internalHom (latticeConjugation h₂)

The lattice conjugation of the space of complex-linear maps between two complexifications is the internal-hom conjugation of the two lattice conjugations.

theorem TauCeti.Hodge.integralMapToComplex_lcomp_comp_llcomp {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} [Module.Free ℤ V₁] [Module.Finite ℤ V₁] {V₃ : Type u₃} {V₄ : Type u₄} {W₃ : Type v₃} {W₄ : Type v₄} [AddCommGroup V₃] [AddCommGroup V₄] [AddCommGroup W₃] [Module ℂ W₃] [AddCommGroup W₄] [Module ℂ W₄] {ι₃ : V₃ →ₗ[ℤ] W₃} (h₁ : IsBaseChange ℂ ι₁) (h₂ : IsBaseChange ℂ ι₂) (h₃ : IsBaseChange ℂ ι₃) (ι₄ : V₄ →ₗ[ℤ] W₄) (f : V₃ →ₗ[ℤ] V₁) (g : V₂ →ₗ[ℤ] V₄) : integralMapToComplex ⋯ (homLatticeMap h₃ ι₄) (LinearMap.lcomp ℤ V₄ f ∘ₗ (LinearMap.llcomp ℤ V₁ V₂ V₄) g) = LinearMap.lcomp ℂ W₄ (integralMapToComplex h₃ ι₁ f) ∘ₗ (LinearMap.llcomp ℂ W₁ W₂ W₄) (integralMapToComplex h₂ ι₄ g)

Complexifying the map φ ↦ g ∘ φ ∘ f of pre- and post-composition by integral linear maps gives pre- and post-composition by their complexifications.