Rational subspaces in an abstract complexification

This file develops the ℤ → ℚ → ℂ base-change tower used by pure and mixed Hodge structures. Given abstract models Vℚ and Vℂ of the rational and complex scalar extensions of an integral module Vℤ, TauCeti.Hodge.rationalToComplexLinearEquiv canonically identifies ℂ ⊗[ℚ] Vℚ with Vℂ. Rational subspaces and rational linear maps can therefore be complexified directly inside the chosen ambient complex spaces.

The constructions use Mathlib's IsBaseChange interface rather than requiring the ambient spaces to be definitionally equal to concrete tensor products. This is essential for geometric Hodge structures, whose rational and complex cohomology spaces arrive as abstract base-change models.

Rationality of a subspace is what makes its complexification stable under the lattice-induced conjugation, so that stability is proved here, for an arbitrary rational subspace, rather than imposed later as structure data.

Main declarations

• TauCeti.Hodge.rationalToComplexMap: the canonical structure map from an abstract rationalification to an abstract complexification.
• TauCeti.Hodge.isBaseChange_rationalToComplexMap: the complex space is the base change of the rational space along this structure map.
• TauCeti.Hodge.rationalToComplexLinearEquiv: the canonical tower equivalence between the concrete rational base change and the abstract complexification.
• TauCeti.Hodge.rationalToComplexSubmodule: the complexification of a rational subspace inside the chosen ambient complexification.
• TauCeti.Hodge.rationalToComplexSubmoduleEquiv: the canonical identification of the concrete complexification ℂ ⊗[ℚ] W of a rational subspace with that complexified subspace.
• TauCeti.Hodge.rationalMapToComplex: scalar extension of a rational linear map between two abstract base-change models.
• TauCeti.Hodge.range_rationalMapToComplex and TauCeti.Hodge.ker_rationalMapToComplex: that scalar extension has the complexified range and the complexified kernel as its range and kernel.
• TauCeti.Hodge.isIdempotentElem_rationalMapToComplex: that scalar extension preserves idempotents.
• TauCeti.Hodge.disjoint_rationalToComplexSubmodule and TauCeti.Hodge.rationalToComplexSubmodule_inf: complexification of rational subspaces preserves disjointness and meets.
• TauCeti.Hodge.rationalMapToComplex_commutes_conj: that scalar extension commutes with lattice conjugation, for arbitrary complex models.
• TauCeti.Hodge.latticeConj_rationalToComplexLinearEquiv_one_tmul: lattice conjugation fixes every purely rational vector of the ambient complexification.
• TauCeti.Hodge.rationalToComplexSubmodule_conj: the complexification of a rational subspace is stable under lattice-induced conjugation.
• TauCeti.Hodge.rationalToComplexSubmodule_sup: complexification preserves joins of rational subspaces.
• TauCeti.Hodge.rationalToComplexSubmodule_eq_bot_iff: only the zero subspace has trivial complexification.
• TauCeti.Hodge.rationalToComplexSubmodule_le_iff: an inclusion of rational subspaces can be tested on their complexifications.

The tower is available in two presentations. The structure map rationalToComplexMap and the witness isBaseChange_rationalToComplexMap describe Vℂ as the complex scalar extension of Vℚ; that is what a construction needs when it extends a ℚ-linear datum to a ℂ-linear one and is therefore determined by its values on rational vectors. The equivalence rationalToComplexLinearEquiv is the canonical IsBaseChange.equiv of this witness, used when a construction manipulates the concrete tensor product ℂ ⊗[ℚ] Vℚ as data, as the complexification of a rational subspace does. On purely rational vectors the two agree, by rationalToComplexLinearEquiv_one_tmul.

References

The signatures are adapted from the proposed definitions in HodgeStructures/Suggested.lean, whose definitive mathematical specification is the accompanying Hodge structures roadmap. In particular the statements of latticeConj_rationalToComplexLinearEquiv_one_tmul and rationalToComplexSubmodule_conj are that file's rationalToComplexLinearEquiv_one_tmul_fixed and rationalToComplexSubmodule_conj; the proofs given here are different, being run against the abstract base-change interface rather than the concrete tensor model.

@[simp]

theorem TauCeti.Hodge.latticeConj_ratTensorMap_tmul (U : Type u_1) [AddCommGroup U] [Module ℚ U] (z : ℂ) (u : U) : (latticeConj ⋯) (z ⊗ₜ[ℚ] u) = (starRingEnd ℂ) z ⊗ₜ[ℚ] u

Lattice conjugation on the complexification ℂ ⊗[ℚ] U of a rational vector space conjugates the scalar factor of a pure tensor. It is the unique conjugate-linear map fixing 1 ⊗ₜ u.

theorem TauCeti.Hodge.integralMapToComplex_ratTensorMap {U : Type u_1} {U' : Type u_2} [AddCommGroup U] [Module ℚ U] [AddCommGroup U'] [Module ℚ U'] (g : U →ₗ[ℚ] U') : integralMapToComplex ⋯ (ratTensorMap ℂ U') (↑ℤ g) = LinearMap.baseChange ℂ g

On the canonical complexification ℂ ⊗[ℚ] U of a rational vector space, the complexification of a ℚ-linear map read as an integral map is its rational base change.

@[instance_reducible]

noncomputable def TauCeti.Hodge.moduleRatOfComplex {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] : Module ℚ Vℂ

The ℚ-module structure on an abstract complexification, obtained by restricting its ℂ-module structure along ℚ → ℂ. It is local to this section, where it is needed to state that the rational-to-complex structure map is ℚ-linear, and has low priority so that ℂ itself keeps its Algebra-derived ℚ-module structure.

theorem TauCeti.Hodge.ratComplexScalarTower {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] : IsScalarTower ℚ ℂ Vℂ

theorem TauCeti.Hodge.instIsScalarTowerIntRatComplex_tauCeti : IsScalarTower ℤ ℚ ℂ

theorem TauCeti.Hodge.instIsScalarTowerIntRat_tauCeti {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] : IsScalarTower ℤ ℚ Vℂ

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

The canonical ℚ-linear structure map from an abstract rationalification to an abstract complexification of the same integral module.

It is the unique map whose composite with the integral structure map ιℚ is ιℂ.

@[simp]

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

The rational-to-complex structure map carries an integral vector to the corresponding vector in the complexification.

@[simp]

theorem TauCeti.Hodge.rationalToComplexMap_restrictScalars_comp {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} (hℚ : IsBaseChange ℚ ιℚ) (ιℂ : Vℤ →ₗ[ℤ] Vℂ) : ↑ℤ (rationalToComplexMap hℚ ιℂ) ∘ₗ ιℚ = ιℂ

Composing the rational-to-complex structure map with rationalification recovers the given integral-to-complex structure map.

theorem TauCeti.Hodge.eq_rationalToComplexMap_of_restrictScalars_comp_eq {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} (hℚ : IsBaseChange ℚ ιℚ) (ιℂ : Vℤ →ₗ[ℤ] Vℂ) (f : Vℚ →ₗ[ℚ] Vℂ) (hf : ↑ℤ f ∘ₗ ιℚ = ιℂ) : f = rationalToComplexMap hℚ ιℂ

The rational-to-complex structure map is the unique ℚ-linear map extending ιℂ along ιℚ.

theorem TauCeti.Hodge.isBaseChange_rationalToComplexMap {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 ℂ ιℂ) : IsBaseChange ℂ (rationalToComplexMap hℚ ιℂ)

The abstract complexification is the base change of the abstract rationalification along the canonical rational-to-complex structure map.

noncomputable def TauCeti.Hodge.rationalToComplexLinearEquiv {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 ℂ ιℂ) : TensorProduct ℚ ℂ Vℚ ≃ₗ[ℂ] Vℂ

The canonical equivalence from the complex base change of an abstract rationalification to the abstract complexification of the same integral module.

theorem TauCeti.Hodge.rationalToComplexLinearEquiv_one_tmul {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 ℂ ιℂ) (x : Vℚ) : (rationalToComplexLinearEquiv hℚ hℂ) (1 ⊗ₜ[ℚ] x) = (rationalToComplexMap hℚ ιℂ) x

On a purely rational vector the tower equivalence agrees with the rational-to-complex structure map.

@[simp]

theorem TauCeti.Hodge.rationalToComplexLinearEquiv_one_tmul_ι {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 ℂ ιℂ) (x : Vℤ) : (rationalToComplexLinearEquiv hℚ hℂ) (1 ⊗ₜ[ℚ] ιℚ x) = ιℂ x

The tower equivalence carries an integral vector through the rationalification to the same integral vector in the complexification.

noncomputable def TauCeti.Hodge.rationalToComplexSubmodule {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 ℂ ιℂ) (W : Submodule ℚ Vℚ) : Submodule ℂ Vℂ

The complexification of a rational subspace, realized inside the chosen ambient complexification.

theorem TauCeti.Hodge.rationalToComplexSubmodule_eq_span {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 ℂ ιℂ) (W : Submodule ℚ Vℚ) : rationalToComplexSubmodule hℚ hℂ W = Submodule.span ℂ ((fun (x : Vℚ) => (rationalToComplexLinearEquiv hℚ hℂ) (1 ⊗ₜ[ℚ] x)) '' ↑W)

The complexification of a rational subspace is the complex span of its rational vectors in the ambient complexification.

theorem TauCeti.Hodge.rationalToComplexLinearEquiv_one_tmul_mem {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 ℂ ιℂ) {W : Submodule ℚ Vℚ} {x : Vℚ} (hx : x ∈ W) : (rationalToComplexLinearEquiv hℚ hℂ) (1 ⊗ₜ[ℚ] x) ∈ rationalToComplexSubmodule hℚ hℂ W

A rational vector belonging to a rational subspace belongs to its complexification.

@[simp]

theorem TauCeti.Hodge.rationalToComplexSubmodule_le_iff {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 ℂ ιℂ) (W₁ W₂ : Submodule ℚ Vℚ) : rationalToComplexSubmodule hℚ hℂ W₁ ≤ rationalToComplexSubmodule hℚ hℂ W₂ ↔ W₁ ≤ W₂

Complexification of rational subspaces reflects inclusions: ℂ is faithfully flat over ℚ, so an inclusion of rational subspaces may be tested on the complexifications.

theorem TauCeti.Hodge.rationalToComplexSubmodule_mono {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 ℂ ιℂ) : Monotone (rationalToComplexSubmodule hℚ hℂ)

Complexification of rational subspaces is monotone.

@[simp]

theorem TauCeti.Hodge.rationalToComplexSubmodule_bot {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 ℂ ιℂ) : rationalToComplexSubmodule hℚ hℂ ⊥ = ⊥

@[simp]

theorem TauCeti.Hodge.rationalToComplexSubmodule_eq_bot_iff {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 ℂ ιℂ) (W : Submodule ℚ Vℚ) : rationalToComplexSubmodule hℚ hℂ W = ⊥ ↔ W = ⊥

A rational subspace is trivial as soon as its complexification is: ℂ is faithfully flat over ℚ.

@[simp]

theorem TauCeti.Hodge.rationalToComplexSubmodule_top {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 ℂ ιℂ) : rationalToComplexSubmodule hℚ hℂ ⊤ = ⊤

@[simp]

theorem TauCeti.Hodge.rationalToComplexSubmodule_sup {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 ℂ ιℂ) (W₁ W₂ : Submodule ℚ Vℚ) : rationalToComplexSubmodule hℚ hℂ (W₁ ⊔ W₂) = rationalToComplexSubmodule hℚ hℂ W₁ ⊔ rationalToComplexSubmodule hℚ hℂ W₂

Complexification of rational subspaces preserves joins.

noncomputable def TauCeti.Hodge.rationalToComplexSubmoduleEquiv {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 ℂ ιℂ) (W : Submodule ℚ Vℚ) : TensorProduct ℚ ℂ ↥W ≃ₗ[ℂ] ↥(rationalToComplexSubmodule hℚ hℂ W)

The canonical equivalence from the concrete complexification ℂ ⊗[ℚ] W of a rational subspace onto the complexification of W inside the ambient complexification.

@[simp]

theorem TauCeti.Hodge.coe_rationalToComplexSubmoduleEquiv {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 ℂ ιℂ) (W : Submodule ℚ Vℚ) (x : TensorProduct ℚ ℂ ↥W) : ↑((rationalToComplexSubmoduleEquiv hℚ hℂ W) x) = (rationalToComplexLinearEquiv hℚ hℂ) ((LinearMap.baseChange ℂ W.subtype) x)

The equivalence onto the complexification of a rational subspace is the tower equivalence applied to the base change of the inclusion of that subspace.

theorem TauCeti.Hodge.latticeConj_rationalToComplexLinearEquiv_one_tmul {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 ℂ ιℂ) (x : Vℚ) : (latticeConj hℂ) ((rationalToComplexLinearEquiv hℚ hℂ) (1 ⊗ₜ[ℚ] x)) = (rationalToComplexLinearEquiv hℚ hℂ) (1 ⊗ₜ[ℚ] x)

Lattice conjugation fixes the image in Vℂ of a purely rational vector 1 ⊗ₜ x.

theorem TauCeti.Hodge.latticeConj_rationalToComplexLinearEquiv_tmul {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 ℂ ιℂ) (z : ℂ) (x : Vℚ) : (latticeConj hℂ) ((rationalToComplexLinearEquiv hℚ hℂ) (z ⊗ₜ[ℚ] x)) = (rationalToComplexLinearEquiv hℚ hℂ) ((starRingEnd ℂ) z ⊗ₜ[ℚ] x)

Lattice conjugation of the image in Vℂ of a pure tensor z ⊗ₜ x with x rational conjugates the scalar.

@[simp]

theorem TauCeti.Hodge.rationalToComplexSubmodule_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 ℂ ιℂ) (W : Submodule ℚ Vℚ) : Submodule.map (latticeConj hℂ) (rationalToComplexSubmodule hℚ hℂ W) = rationalToComplexSubmodule hℚ hℂ W

The complexification of a rational subspace is stable under lattice-induced conjugation.

noncomputable def TauCeti.Hodge.rationalMapToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) : Vℂ →ₗ[ℂ] V'ℂ

The complexification of a rational linear map between abstract rational and complex base-change models.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_rationalToComplexLinearEquiv_tmul {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) (z : ℂ) (x : Vℚ) : (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f) ((rationalToComplexLinearEquiv hℚ hℂ) (z ⊗ₜ[ℚ] x)) = (rationalToComplexLinearEquiv h'ℚ h'ℂ) (z ⊗ₜ[ℚ] f x)

Complexification of a rational map sends the image of the pure tensor z ⊗ₜ x to the image of z ⊗ₜ f x.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_rationalToComplexMap {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) (x : Vℚ) : (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f) ((rationalToComplexMap hℚ ιℂ) x) = (rationalToComplexMap h'ℚ ι'ℂ) (f x)

Complexification of a rational map is natural for the rational-to-complex structure maps: it carries the image of a rational vector to the image of its value under the map.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_id {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 ℂ ιℂ) : rationalMapToComplex hℚ hℂ hℚ hℂ LinearMap.id = LinearMap.id

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

noncomputable def TauCeti.Hodge.rationalMapToComplexHom {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) : (Vℚ →ₗ[ℚ] V'ℚ) →ₗ[ℚ] Vℂ →ₗ[ℂ] V'ℂ

Complexification of rational linear maps, bundled as a rational linear map.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplexHom_rationalToComplexMap {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (f : Vℚ →ₗ[ℚ] V'ℚ) (x : Vℚ) : ((rationalMapToComplexHom hℚ hℂ h'ℚ) f) ((rationalToComplexMap hℚ ιℂ) x) = (rationalToComplexMap h'ℚ ι'ℂ) (f x)

The bundled complexification sends a rational vector to the image of that vector.

theorem TauCeti.Hodge.rationalMapToComplexHom_apply {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) : (rationalMapToComplexHom hℚ hℂ h'ℚ) f = rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f

The generic base-change hom agrees with the Hodge-facing complexification map.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_zero {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) : rationalMapToComplex hℚ hℂ h'ℚ h'ℂ 0 = 0

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

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_add {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f g : Vℚ →ₗ[ℚ] V'ℚ) : rationalMapToComplex hℚ hℂ h'ℚ h'ℂ (f + g) = rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f + rationalMapToComplex hℚ hℂ h'ℚ h'ℂ g

Complexification preserves addition of rational linear maps.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_neg {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) : rationalMapToComplex hℚ hℂ h'ℚ h'ℂ (-f) = -rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f

Complexification preserves negation of rational linear maps.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_sub {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f g : Vℚ →ₗ[ℚ] V'ℚ) : rationalMapToComplex hℚ hℂ h'ℚ h'ℂ (f - g) = rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f - rationalMapToComplex hℚ hℂ h'ℚ h'ℂ g

Complexification preserves subtraction of rational linear maps.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_nsmul {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (k : ℕ) (f : Vℚ →ₗ[ℚ] V'ℚ) : rationalMapToComplex hℚ hℂ h'ℚ h'ℂ (k • f) = k • rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f

Complexification preserves natural-number multiples of rational linear maps.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_zsmul {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (k : ℤ) (f : Vℚ →ₗ[ℚ] V'ℚ) : rationalMapToComplex hℚ hℂ h'ℚ h'ℂ (k • f) = k • rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f

Complexification preserves integer multiples of rational linear maps.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_smul {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (q : ℚ) (f : Vℚ →ₗ[ℚ] V'ℚ) : rationalMapToComplex hℚ hℂ h'ℚ h'ℂ (q • f) = ↑q • rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f

Complexification preserves rational multiples of rational linear maps, the rational scalar acting on the complexification through ℚ → ℂ.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_commutes_conj {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) (x : Vℂ) : (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f) ((latticeConj hℂ) x) = (latticeConj h'ℂ) ((rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f) x)

The complexification of a rational map commutes with lattice conjugation. The abstract base-change interface makes this a statement about arbitrary complex models, not only about the concrete tensor product.

theorem TauCeti.Hodge.rationalMapToComplex_comp_latticeConj {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) : rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f ∘ₛₗ latticeConj hℂ = latticeConj h'ℂ ∘ₛₗ rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f

The complexification of a rational map commutes with lattice conjugation, as an identity of conjugate-linear maps.

theorem TauCeti.Hodge.rationalMapToComplex_comp {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {V'ℤ : Type u'} {V'ℚ : Type v'} {V'ℂ : Type w'} [AddCommGroup V'ℤ] [AddCommGroup V'ℚ] [Module ℚ V'ℚ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℚ : V'ℤ →ₗ[ℤ] V'ℚ} {ι'ℂ : V'ℤ →ₗ[ℤ] V'ℂ} {V''ℤ : Type u_1} {V''ℚ : Type u_2} {V''ℂ : Type u_3} [AddCommGroup V''ℤ] [AddCommGroup V''ℚ] [Module ℚ V''ℚ] [AddCommGroup V''ℂ] [Module ℂ V''ℂ] {ι''ℚ : V''ℤ →ₗ[ℤ] V''ℚ} {ι''ℂ : V''ℤ →ₗ[ℤ] V''ℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (h''ℚ : IsBaseChange ℚ ι''ℚ) (h''ℂ : IsBaseChange ℂ ι''ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) (g : V'ℚ →ₗ[ℚ] V''ℚ) : rationalMapToComplex hℚ hℂ h''ℚ h''ℂ (g ∘ₗ f) = rationalMapToComplex h'ℚ h'ℂ h''ℚ h''ℂ g ∘ₗ rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f

Complexification preserves composition of rational linear maps.

theorem TauCeti.Hodge.isIdempotentElem_rationalMapToComplex {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 ℂ ιℂ) {e : Vℚ →ₗ[ℚ] Vℚ} (he : IsIdempotentElem e) : IsIdempotentElem (rationalMapToComplex hℚ hℂ hℚ hℂ e)

Extension of scalars along ℚ → ℂ preserves idempotents: the complexification of an idempotent rational endomorphism is idempotent.

theorem TauCeti.Hodge.map_rationalToComplexSubmodule {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) (W : Submodule ℚ Vℚ) : Submodule.map (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f) (rationalToComplexSubmodule hℚ hℂ W) = rationalToComplexSubmodule h'ℚ h'ℂ (Submodule.map f W)

Complexifying the image of a rational subspace is the image of its complexification.

theorem TauCeti.Hodge.map_rationalToComplexSubmodule_le {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) {W : Submodule ℚ Vℚ} {W' : Submodule ℚ V'ℚ} (hW : Submodule.map f W ≤ W') : Submodule.map (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f) (rationalToComplexSubmodule hℚ hℂ W) ≤ rationalToComplexSubmodule h'ℚ h'ℂ W'

A rational map carrying one rational subspace into another carries their complexifications into one another.

@[simp]

theorem TauCeti.Hodge.range_rationalMapToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) : (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f).range = rationalToComplexSubmodule h'ℚ h'ℂ f.range

The scalar extension of a rational linear map has the complexification of its range as its range.

@[simp]

theorem TauCeti.Hodge.ker_rationalMapToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {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 ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (f : Vℚ →ₗ[ℚ] V'ℚ) : (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f).ker = rationalToComplexSubmodule hℚ hℂ f.ker

The scalar extension of a rational linear map has the complexification of its kernel as its kernel: extension of scalars along ℚ → ℂ is exact.

theorem TauCeti.Hodge.disjoint_rationalToComplexSubmodule {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 ℂ ιℂ) {W₁ W₂ : Submodule ℚ Vℚ} (h : Disjoint W₁ W₂) : Disjoint (rationalToComplexSubmodule hℚ hℂ W₁) (rationalToComplexSubmodule hℚ hℂ W₂)

Complexification of rational subspaces preserves disjointness.

@[simp]

theorem TauCeti.Hodge.rationalToComplexSubmodule_inf {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 ℂ ιℂ) (W₁ W₂ : Submodule ℚ Vℚ) : rationalToComplexSubmodule hℚ hℂ (W₁ ⊓ W₂) = rationalToComplexSubmodule hℚ hℂ W₁ ⊓ rationalToComplexSubmodule hℚ hℂ W₂

Complexification of rational subspaces preserves meets.

theorem TauCeti.Hodge.instIsScalarTowerRatComplex_tauCeti {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] : IsScalarTower ℚ ℂ Vℂ

theorem TauCeti.Hodge.instIsScalarTowerRatComplex_tauCeti_1 {V'ℂ : Type u_3} [AddCommGroup V'ℂ] [Module ℂ V'ℂ] : IsScalarTower ℚ ℂ V'ℂ

@[simp]

theorem TauCeti.Hodge.rationalToComplexMap_prodMap {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {V'ℤ : Type u_1} {V'ℚ : Type u_2} {V'ℂ : Type u_3} [AddCommGroup V'ℤ] [AddCommGroup V'ℚ] [Module ℚ V'ℚ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℚ : V'ℤ →ₗ[ℤ] V'ℚ} {ι'ℂ : V'ℤ →ₗ[ℤ] V'ℂ} (hℚ : IsBaseChange ℚ ιℚ) (h'ℚ : IsBaseChange ℚ ι'ℚ) : rationalToComplexMap ⋯ (ιℂ.prodMap ι'ℂ) = (rationalToComplexMap hℚ ιℂ).prodMap (rationalToComplexMap h'ℚ ι'ℂ)

Rational-to-complex structure maps commute with products of base-change models.

@[simp]

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

Complexification commutes with products of rational subspaces.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_fst {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {V'ℤ : Type u_1} {V'ℚ : Type u_2} {V'ℂ : Type u_3} [AddCommGroup V'ℤ] [AddCommGroup V'ℚ] [Module ℚ V'ℚ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℚ : V'ℤ →ₗ[ℤ] V'ℚ} {ι'ℂ : V'ℤ →ₗ[ℤ] V'ℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) : rationalMapToComplex ⋯ ⋯ hℚ hℂ (LinearMap.fst ℚ Vℚ V'ℚ) = LinearMap.fst ℂ Vℂ V'ℂ

Complexification sends the first rational projection to the first complex projection.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_snd {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {V'ℤ : Type u_1} {V'ℚ : Type u_2} {V'ℂ : Type u_3} [AddCommGroup V'ℤ] [AddCommGroup V'ℚ] [Module ℚ V'ℚ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℚ : V'ℤ →ₗ[ℤ] V'ℚ} {ι'ℂ : V'ℤ →ₗ[ℤ] V'ℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) : rationalMapToComplex ⋯ ⋯ h'ℚ h'ℂ (LinearMap.snd ℚ Vℚ V'ℚ) = LinearMap.snd ℂ Vℂ V'ℂ

Complexification sends the second rational projection to the second complex projection.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_inl {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {V'ℤ : Type u_1} {V'ℚ : Type u_2} {V'ℂ : Type u_3} [AddCommGroup V'ℤ] [AddCommGroup V'ℚ] [Module ℚ V'ℚ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℚ : V'ℤ →ₗ[ℤ] V'ℚ} {ι'ℂ : V'ℤ →ₗ[ℤ] V'ℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) : rationalMapToComplex hℚ hℂ ⋯ ⋯ (LinearMap.inl ℚ Vℚ V'ℚ) = LinearMap.inl ℂ Vℂ V'ℂ

Complexification sends the first rational inclusion to the first complex inclusion.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_inr {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {V'ℤ : Type u_1} {V'ℚ : Type u_2} {V'ℂ : Type u_3} [AddCommGroup V'ℤ] [AddCommGroup V'ℚ] [Module ℚ V'ℚ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℚ : V'ℤ →ₗ[ℤ] V'ℚ} {ι'ℂ : V'ℤ →ₗ[ℤ] V'ℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) : rationalMapToComplex h'ℚ h'ℂ ⋯ ⋯ (LinearMap.inr ℚ Vℚ V'ℚ) = LinearMap.inr ℂ Vℂ V'ℂ

Complexification sends the second rational inclusion to the second complex inclusion.