The real points of a conjugate-linear involution

A conjugation of a complex vector space V is a conjugate-linear map K : V → V with K ∘ K = id, that is, a starRingEnd ℂ-semilinear self-map that is involutive. Its real points are the vectors it fixes. They form a real subspace TauCeti.realPoints K, and the main theorem of this file is that V is the complexification of that subspace: the canonical map

ℂ ⊗[ℝ] realPoints K → V, c ⊗ₜ w ↦ c • w

is a ℂ-linear isomorphism. Conversely a complexification ℂ ⊗[ℝ] W carries the conjugation c ⊗ₜ w ↦ conj c ⊗ₜ w (TauCeti.tmulConj), whose real points are the image of W. So each of the two constructions produces the other: a conjugation on V presents V as a complexification, and a complexification carries a conjugation. That is what makes conjugations the tool for realizing an object over ℝ.

The canonical TauCeti.realPointsEquiv intertwines TauCeti.tmulConj with the original conjugation K. For a chosen presentation ℂ ⊗[ℝ] W ≃ₗ[ℂ] V, LinearEquiv.conjugationOfComplexification transports the existing tensor conjugation through that equivalence. Its exact fixed locus is the image of the real inclusion. The equivariant application is Representation.IsRealForm.exists_isRealStructure, downstream in TauCeti.RepresentationTheory.RealForm.

Everything is stated for an arbitrary V; no finite-dimensionality is used anywhere.

Main definitions

• TauCeti.realPoints: the real points of a conjugate-linear map, as a Submodule ℝ V.
• TauCeti.conjRealPart and TauCeti.conjImaginaryPart: the two real points a vector decomposes into; TauCeti.conjRealPart_def and TauCeti.conjImaginaryPart_def are their defining formulas.
• TauCeti.realPointsLift: the canonical ℂ-linear map ℂ ⊗[ℝ] realPoints K →ₗ[ℂ] V.
• TauCeti.realPointsEquiv: that map as a ℂ-linear isomorphism, for involutive K.
• TauCeti.tmulConj: the conjugation c ⊗ₜ w ↦ conj c ⊗ₜ w of a complexification ℂ ⊗[ℝ] W.
• TauCeti.realPart and TauCeti.imaginaryPart: the two real coordinates of a vector of a complexification, bundled as TauCeti.complexificationLinearEquivProd; TauCeti.one_tmul_realPart_add_I_tmul_imaginaryPart reassembles it, and TauCeti.complexification_ext says the two coordinates determine the vector.
• LinearEquiv.conjugationOfComplexification: the tensor conjugation transported through a complexification equivalence ℂ ⊗[ℝ] W ≃ₗ[ℂ] V.

Main statements

• TauCeti.conjRealPart_add_I_smul_conjImaginaryPart: the decomposition v = conjRealPart K v + I • conjImaginaryPart K v, which makes TauCeti.realPointsLift surjective.
• TauCeti.realPointsLift_injective, TauCeti.realPointsLift_surjective and TauCeti.realPointsEquiv: a complex vector space is the complexification of the real points of any conjugation on it.
• TauCeti.span_realPoints_eq_top: the real points of an involutive conjugation span V over ℂ, so an identity between ℂ-linear or ℂ-bilinear maps may be checked on real vectors alone.
• TauCeti.finrank_realPoints: the real points have the ℝ-dimension that V has over ℂ.
• TauCeti.finrank_selfAdjoint_submodule: in particular, the self-adjoint elements of a complex star module have the ℝ-dimension that the module has over ℂ.
• TauCeti.exists_one_tmul_add_I_tmul: every element of ℂ ⊗[ℝ] W is 1 ⊗ₜ w₁ + I ⊗ₜ w₂; this is what makes the lift injective.
• LinearMap.liftBaseChange_complex_injective_of_conj: more generally, an injective real-linear map whose values a conjugate-linear map fixes induces an injective map on the complexification, for any real structure compatible with the complex one.
• TauCeti.tmulConj_involutive, TauCeti.tmulConj_tmul and TauCeti.tmulConj_eq_self_iff: the conjugation of a complexification and its real points.
• TauCeti.realPointsEquiv_tmulConj: the canonical real-descent equivalence intertwines tensor conjugation with K.
• TauCeti.tmulConj_baseChange: that conjugation commutes with every base-changed map, which is what makes it equivariant for a base-changed action.
• LinearEquiv.conjugationOfComplexification_apply_tmul: the transported conjugation sends e (c ⊗ₜ w) to e (star c ⊗ₜ w).
• LinearEquiv.conjugationOfComplexification_eq_self_iff, LinearEquiv.conjugationOfComplexification_unique and LinearEquiv.conjugationOfComplexification_natural: the transported conjugation fixes exactly the image of the real inclusion, is the only conjugate-linear map doing so, and commutes with complex-linear maps carrying one real inclusion to another.

Implementation notes

A conjugation is carried here as the two unbundled hypotheses K : V →ₛₗ[starRingEnd ℂ] V and Function.Involutive K, rather than as a bundled structure. TauCeti.Hodge.Conjugation already bundles exactly this data, but it lives downstream in TauCeti/Geometry/Hodge/, so bundling here would either duplicate it or invert the dependency between TauCeti.LinearAlgebra and TauCeti.Geometry; a TauCeti.Hodge.Conjugation supplies the hypotheses below from its two fields. For the same reason TauCeti.realPoints asks only for the semilinear map: the subspace makes sense without involutivity, and only the complexification theorem needs it.

Mathlib's realPart/imaginaryPart decomposition of a star module over ℂ is the same mathematics, but it reads the conjugation off the Star instance on V: selfAdjoint.submodule and realPart both ask for [StarAddMonoid V] [StarModule ℂ V], and StarAddMonoid already carries involutivity. Here the conjugation is instead a term K that TauCeti.realPoints and TauCeti.conjRealPart are indexed by, because one V carries many conjugations and TauCeti.realPoints is wanted before K is known to be involutive -- TauCeti.realPointsLift is injective for every conjugate-linear K. So the instance-borne spelling is not available here, and a TauCeti.Hodge.Conjugation, or a Representation.IsRealStructure, hands its conjugation over as a field rather than as an instance.

No definition here exposes its body: TauCeti.mem_realPoints, TauCeti.conjRealPart_def, TauCeti.conjImaginaryPart_def, TauCeti.realPointsLift_tmul, TauCeti.realPointsEquiv_tmul, TauCeti.realPointsEquiv_symm_apply and TauCeti.tmulConj_tmul are the characterizations a consumer works from.

The real scalar structure on V is Mathlib's Module.complexToReal, the one Module ℂ V induces, so r • v and (r : ℂ) • v are definitionally equal and no scalar tower hypothesis is carried. The injectivity argument LinearMap.liftBaseChange_complex_injective_of_conj is the exception: it takes an arbitrary real structure with IsScalarTower ℝ ℂ E, so that it also serves spaces such as Matrix n n ℂ whose real structure is not syntactically Module.complexToReal.

References

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42 (1977), §13.2, where the conjugation attached to an invariant form realizes a representation over ℝ.

The real points of a conjugate-linear map

def TauCeti.realPoints {V : Type u_1} [AddCommGroup V] [Module ℂ V] (K : V →ₗ⋆[ℂ] V) : Submodule ℝ V

The real points of a conjugate-linear map K : V → V: the vectors K fixes. They form a subspace over ℝ but not over ℂ, since K (c • v) = conj c • K v.

@[simp]

theorem TauCeti.mem_realPoints {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} {v : V} : v ∈ realPoints K ↔ K v = v

noncomputable def TauCeti.conjRealPart {V : Type u_1} [AddCommGroup V] [Module ℂ V] (K : V →ₗ⋆[ℂ] V) (v : V) : V

The real part of v relative to a conjugate-linear map: the vector ½ (v + K v), a real point once K is involutive (TauCeti.conjRealPart_mem).

noncomputable def TauCeti.conjImaginaryPart {V : Type u_1} [AddCommGroup V] [Module ℂ V] (K : V →ₗ⋆[ℂ] V) (v : V) : V

The imaginary part of v relative to a conjugate-linear map: the vector ½ I • (K v - v), the coefficient of I in TauCeti.conjRealPart_add_I_smul_conjImaginaryPart.

theorem TauCeti.conjRealPart_def {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (v : V) : conjRealPart K v = 2⁻¹ • (v + K v)

The defining formula for the real part, the body of TauCeti.conjRealPart not being exposed.

theorem TauCeti.conjImaginaryPart_def {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (v : V) : conjImaginaryPart K v = 2⁻¹ • Complex.I • (K v - v)

The defining formula for the imaginary part, the body of TauCeti.conjImaginaryPart not being exposed.

theorem TauCeti.conjRealPart_mem {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (hK : Function.Involutive ⇑K) (v : V) : conjRealPart K v ∈ realPoints K

theorem TauCeti.conjImaginaryPart_mem {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (hK : Function.Involutive ⇑K) (v : V) : conjImaginaryPart K v ∈ realPoints K

@[simp]

theorem TauCeti.conjRealPart_of_mem {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} {v : V} (hv : v ∈ realPoints K) : conjRealPart K v = v

A real point is its own real part.

@[simp]

theorem TauCeti.conjImaginaryPart_of_mem {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} {v : V} (hv : v ∈ realPoints K) : conjImaginaryPart K v = 0

A real point has vanishing imaginary part.

theorem TauCeti.conjRealPart_add_I_smul_conjImaginaryPart {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (v : V) : conjRealPart K v + Complex.I • conjImaginaryPart K v = v

The decomposition into real points: every vector is its real part plus I times its imaginary part. Once K is involutive both summands lie in TauCeti.realPoints K, so this is what exhibits V as the complexification of that subspace.

theorem TauCeti.span_realPoints_eq_top {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (hK : Function.Involutive ⇑K) : Submodule.span ℂ ↑(realPoints K) = ⊤

The real points of a conjugation span the whole space over ℂ. Every vector is a complex combination of the two real points it decomposes into, so an identity between ℂ-linear or ℂ-bilinear maps may be checked on real vectors alone.

A complexification splits along 1 and I

theorem TauCeti.exists_one_tmul_add_I_tmul {W : Type u_2} [AddCommGroup W] [Module ℝ W] (u : TensorProduct ℝ ℂ W) : ∃ (w₁ : W) (w₂ : W), u = 1 ⊗ₜ[ℝ] w₁ + Complex.I ⊗ₜ[ℝ] w₂

Every element of ℂ ⊗[ℝ] W is 1 ⊗ₜ w₁ + I ⊗ₜ w₂: writing a complex scalar as x + y * I with x, y : ℝ moves its two real coordinates into the second factor. This is the splitting ℂ ⊗[ℝ] W ≅ W ⊕ I · W in the form the injectivity argument below uses it.

Real-linear maps into the real points

theorem LinearMap.liftBaseChange_complex_injective_of_conj {E : Type u_2} {W : Type u_3} [AddCommGroup E] [Module ℂ E] [Module ℝ E] [IsScalarTower ℝ ℂ E] [AddCommGroup W] [Module ℝ W] (f : W →ₗ[ℝ] E) {K : E →ₗ⋆[ℂ] E} (hf : Function.Injective ⇑f) (hK : ∀ (w : W), K (f w) = f w) : Function.Injective ⇑(liftBaseChange ℂ f)

Vectors fixed by a conjugate-linear map complexify injectively. If a conjugate-linear K fixes every value of an injective real-linear map f : W → E, then the induced map ℂ ⊗[ℝ] W → E, c ⊗ₜ w ↦ c • f w, is injective: applying K to a relation f w₁ + I • f w₂ = 0 flips the sign of its I-component, so adding the two relations kills f w₂ and leaves 2 • f w₁ = 0.

The real structure on E is an arbitrary one compatible with the complex structure (IsScalarTower ℝ ℂ E), so this also applies to spaces such as Matrix n n ℂ whose real structure is not syntactically Module.complexToReal.

The complexification of the real points

noncomputable def TauCeti.realPointsLift {V : Type u_1} [AddCommGroup V] [Module ℂ V] (K : V →ₗ⋆[ℂ] V) : TensorProduct ℝ ℂ ↥(realPoints K) →ₗ[ℂ] V

The canonical ℂ-linear map from the complexification of the real points, c ⊗ₜ w ↦ c • w. It is LinearMap.liftBaseChange applied to the inclusion of the real points. TauCeti.realPointsEquiv upgrades it to an isomorphism when K is involutive.

@[simp]

theorem TauCeti.realPointsLift_tmul {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (c : ℂ) (w : ↥(realPoints K)) : (realPointsLift K) (c ⊗ₜ[ℝ] w) = c • ↑w

theorem TauCeti.realPointsLift_surjective {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (hK : Function.Involutive ⇑K) : Function.Surjective ⇑(realPointsLift K)

The lift is surjective once K is involutive: its image is the complex span of the real points, which is all of V (TauCeti.span_realPoints_eq_top).

theorem TauCeti.realPointsLift_injective {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} : Function.Injective ⇑(realPointsLift K)

The lift is injective for any conjugate-linear K: only its surjectivity uses that K is involutive. This is LinearMap.liftBaseChange_complex_injective_of_conj for the inclusion of the real points.

noncomputable def TauCeti.realPointsEquiv {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (hK : Function.Involutive ⇑K) : TensorProduct ℝ ℂ ↥(realPoints K) ≃ₗ[ℂ] V

A complex vector space is the complexification of the real points of any conjugation on it. The isomorphism is c ⊗ₜ w ↦ c • w; surjectivity is the decomposition TauCeti.conjRealPart_add_I_smul_conjImaginaryPart, and injectivity is that a relation w₁ + I • w₂ = 0 between real points is killed by adding and subtracting its conjugate.

@[simp]

theorem TauCeti.realPointsEquiv_tmul {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (hK : Function.Involutive ⇑K) (c : ℂ) (w : ↥(realPoints K)) : (realPointsEquiv hK) (c ⊗ₜ[ℝ] w) = c • ↑w

The isomorphism sends c ⊗ₜ w to c • w.

@[simp]

theorem TauCeti.realPointsEquiv_symm_apply {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (hK : Function.Involutive ⇑K) (v : V) : (realPointsEquiv hK).symm v = 1 ⊗ₜ[ℝ] ⟨conjRealPart K v, ⋯⟩ + Complex.I ⊗ₜ[ℝ] ⟨conjImaginaryPart K v, ⋯⟩

The inverse of the isomorphism is the decomposition into real and imaginary parts: v ↦ 1 ⊗ₜ conjRealPart K v + I ⊗ₜ conjImaginaryPart K v.

theorem TauCeti.finrank_realPoints {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (hK : Function.Involutive ⇑K) : Module.finrank ℝ ↥(realPoints K) = Module.finrank ℂ V

The real points of a conjugation halve the dimension: their ℝ-dimension is the ℂ-dimension of V, because V is their complexification and base change does not change the dimension. No finiteness is assumed: in the infinite-dimensional case both sides are the junk value 0.

theorem TauCeti.finrank_selfAdjoint_submodule {A : Type u_2} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : Module.finrank ℝ ↥(selfAdjoint.submodule ℝ A) = Module.finrank ℂ A

The self-adjoint elements of a complex star module have the ℝ-dimension that the module has over ℂ: they are the real points of the conjugation star.

The conjugation of a complexification

noncomputable def TauCeti.tmulConj (W : Type u_2) [AddCommGroup W] [Module ℝ W] : TensorProduct ℝ ℂ W →ₗ⋆[ℂ] TensorProduct ℝ ℂ W

The conjugation of a complexification: c ⊗ₜ w ↦ conj c ⊗ₜ w, conjugate-linear because conjugation is ℝ-linear and multiplicative on ℂ. The underlying ℝ-linear map is LinearMap.rTensor W Complex.conjAe.toLinearMap. This is the construction converse to TauCeti.realPointsEquiv: it turns a presentation of a space as a complexification into a conjugation on it.

@[simp]

theorem TauCeti.tmulConj_tmul (W : Type u_2) [AddCommGroup W] [Module ℝ W] (c : ℂ) (w : W) : (tmulConj W) (c ⊗ₜ[ℝ] w) = (starRingEnd ℂ) c ⊗ₜ[ℝ] w

The conjugation of a complexification conjugates the scalar and leaves the vector alone.

@[simp]

theorem TauCeti.tmulConj_tmulConj (W : Type u_2) [AddCommGroup W] [Module ℝ W] (u : TensorProduct ℝ ℂ W) : (tmulConj W) ((tmulConj W) u) = u

Conjugating twice is the identity, in the applied form simp can use. The proof is an induction on the tensor, run off the characterization TauCeti.tmulConj_tmul rather than the unexposed body.

theorem TauCeti.tmulConj_involutive (W : Type u_2) [AddCommGroup W] [Module ℝ W] : Function.Involutive ⇑(tmulConj W)

The conjugation of a complexification is involutive, so it is a conjugation in the sense of this file.

@[simp]

theorem TauCeti.tmulConj_eq_self_iff (W : Type u_2) [AddCommGroup W] [Module ℝ W] (u : TensorProduct ℝ ℂ W) : (tmulConj W) u = u ↔ ∃ (w : W), u = 1 ⊗ₜ[ℝ] w

The vectors the conjugation of a complexification fixes are exactly the image of W, that is, the elements 1 ⊗ₜ w. Stated on tmulConj W u = u rather than on u ∈ realPoints (tmulConj W) because TauCeti.mem_realPoints is the simp normal form of the latter.

noncomputable def TauCeti.realPart (W : Type u_3) [AddCommGroup W] [Module ℝ W] : TensorProduct ℝ ℂ W →ₗ[ℝ] W

The real-linear retraction c ⊗ₜ w ↦ (re c) • w of w ↦ 1 ⊗ₜ w.

@[simp]

theorem TauCeti.realPart_tmul (W : Type u_2) [AddCommGroup W] [Module ℝ W] (c : ℂ) (w : W) : (realPart W) (c ⊗ₜ[ℝ] w) = c.re • w

The real part of a pure tensor is its real scalar part acting on the vector.

theorem TauCeti.realPart_one_tmul (W : Type u_2) [AddCommGroup W] [Module ℝ W] (w : W) : (realPart W) (1 ⊗ₜ[ℝ] w) = w

The real part of a real vector embedded in its complexification is that vector.

noncomputable def TauCeti.imaginaryPart (W : Type u_3) [AddCommGroup W] [Module ℝ W] : TensorProduct ℝ ℂ W →ₗ[ℝ] W

The real-linear map c ⊗ₜ w ↦ (im c) • w, reading off the coefficient of I in the splitting ℂ ⊗[ℝ] W ≅ W ⊕ I · W.

@[simp]

theorem TauCeti.imaginaryPart_tmul (W : Type u_2) [AddCommGroup W] [Module ℝ W] (c : ℂ) (w : W) : (imaginaryPart W) (c ⊗ₜ[ℝ] w) = c.im • w

The imaginary part of a pure tensor is its imaginary scalar part acting on the vector.

@[simp]

theorem TauCeti.one_tmul_realPart_add_I_tmul_imaginaryPart (W : Type u_2) [AddCommGroup W] [Module ℝ W] (u : TensorProduct ℝ ℂ W) : 1 ⊗ₜ[ℝ] (realPart W) u + Complex.I ⊗ₜ[ℝ] (imaginaryPart W) u = u

Every element of ℂ ⊗[ℝ] W is 1 ⊗ₜ realPart W u + I ⊗ₜ imaginaryPart W u.

theorem TauCeti.complexification_ext {W : Type u_2} [AddCommGroup W] [Module ℝ W] {u v : TensorProduct ℝ ℂ W} (hre : (realPart W) u = (realPart W) v) (him : (imaginaryPart W) u = (imaginaryPart W) v) : u = v

Extensionality in a complexification: a vector of ℂ ⊗[ℝ] W is determined by its real and imaginary parts.

theorem TauCeti.complexification_ext_iff {W : Type u_2} [AddCommGroup W] [Module ℝ W] {u v : TensorProduct ℝ ℂ W} : u = v ↔ (realPart W) u = (realPart W) v ∧ (imaginaryPart W) u = (imaginaryPart W) v

Two vectors of ℂ ⊗[ℝ] W are equal exactly when their real and imaginary parts are.

@[simp]

theorem TauCeti.one_tmul_add_I_tmul_inj (W : Type u_2) [AddCommGroup W] [Module ℝ W] {w₁ w₂ w₁' w₂' : W} : 1 ⊗ₜ[ℝ] w₁ + Complex.I ⊗ₜ[ℝ] w₂ = 1 ⊗ₜ[ℝ] w₁' + Complex.I ⊗ₜ[ℝ] w₂' ↔ w₁ = w₁' ∧ w₂ = w₂'

The two real coordinates of 1 ⊗ₜ w₁ + I ⊗ₜ w₂ are w₁ and w₂.

theorem TauCeti.smul_one_tmul_add_I_tmul (W : Type u_2) [AddCommGroup W] [Module ℝ W] (c : ℂ) (v w : W) : c • (1 ⊗ₜ[ℝ] v + Complex.I ⊗ₜ[ℝ] w) = 1 ⊗ₜ[ℝ] (c.re • v - c.im • w) + Complex.I ⊗ₜ[ℝ] (c.re • w + c.im • v)

Multiplication by a complex scalar c in the real coordinates of a complexification: c • (1 ⊗ₜ v + I ⊗ₜ w) = 1 ⊗ₜ (re c • v - im c • w) + I ⊗ₜ (re c • w + im c • v).

theorem TauCeti.I_smul_one_tmul_add_I_tmul (W : Type u_2) [AddCommGroup W] [Module ℝ W] (v w : W) : Complex.I • (1 ⊗ₜ[ℝ] v + Complex.I ⊗ₜ[ℝ] w) = 1 ⊗ₜ[ℝ] (-w) + Complex.I ⊗ₜ[ℝ] v

I • (1 ⊗ₜ v + I ⊗ₜ w) = 1 ⊗ₜ (-w) + I ⊗ₜ v in a complexification.

@[simp]

theorem TauCeti.realPart_smul (W : Type u_2) [AddCommGroup W] [Module ℝ W] (c : ℂ) (u : TensorProduct ℝ ℂ W) : (realPart W) (c • u) = c.re • (realPart W) u - c.im • (imaginaryPart W) u

The real part of c • u is re c • realPart W u - im c • imaginaryPart W u.

@[simp]

theorem TauCeti.imaginaryPart_smul (W : Type u_2) [AddCommGroup W] [Module ℝ W] (c : ℂ) (u : TensorProduct ℝ ℂ W) : (imaginaryPart W) (c • u) = c.re • (imaginaryPart W) u + c.im • (realPart W) u

The imaginary part of c • u is re c • imaginaryPart W u + im c • realPart W u.

noncomputable def TauCeti.complexificationLinearEquivProd (W : Type u_2) [AddCommGroup W] [Module ℝ W] : TensorProduct ℝ ℂ W ≃ₗ[ℝ] W × W

Real-linear isomorphism ℂ ⊗[ℝ] W ≃ₗ[ℝ] W × W given by (realPart, imaginaryPart).

@[simp]

theorem TauCeti.complexificationLinearEquivProd_apply {W : Type u_2} [AddCommGroup W] [Module ℝ W] (u : TensorProduct ℝ ℂ W) : (complexificationLinearEquivProd W) u = ((realPart W) u, (imaginaryPart W) u)

@[simp]

theorem TauCeti.complexificationLinearEquivProd_symm_apply {W : Type u_2} [AddCommGroup W] [Module ℝ W] (p : W × W) : (complexificationLinearEquivProd W).symm p = 1 ⊗ₜ[ℝ] p.1 + Complex.I ⊗ₜ[ℝ] p.2

@[simp]

theorem TauCeti.realPart_tmulConj {W : Type u_2} [AddCommGroup W] [Module ℝ W] (u : TensorProduct ℝ ℂ W) : (realPart W) ((tmulConj W) u) = (realPart W) u

Complex conjugation preserves the real part of u : ℂ ⊗[ℝ] W.

@[simp]

theorem TauCeti.imaginaryPart_tmulConj {W : Type u_2} [AddCommGroup W] [Module ℝ W] (u : TensorProduct ℝ ℂ W) : (imaginaryPart W) ((tmulConj W) u) = -(imaginaryPart W) u

Complex conjugation negates the imaginary part of u : ℂ ⊗[ℝ] W.

theorem TauCeti.tmulConj_eq_one_tmul_sub_I_tmul {W : Type u_2} [AddCommGroup W] [Module ℝ W] (u : TensorProduct ℝ ℂ W) : (tmulConj W) u = 1 ⊗ₜ[ℝ] (realPart W) u - Complex.I ⊗ₜ[ℝ] (imaginaryPart W) u

Coordinate decomposition of tmulConj W u into 1 ⊗ₜ realPart W u - I ⊗ₜ imaginaryPart W u.

@[simp]

theorem TauCeti.realPointsEquiv_tmulConj {V : Type u_1} [AddCommGroup V] [Module ℂ V] {K : V →ₗ⋆[ℂ] V} (hK : Function.Involutive ⇑K) (x : TensorProduct ℝ ℂ ↥(realPoints K)) : (realPointsEquiv hK) ((tmulConj ↥(realPoints K)) x) = K ((realPointsEquiv hK) x)

Real descent intertwines tensor conjugation with the original conjugation.

theorem TauCeti.tmulConj_baseChange {W : Type u_2} {W' : Type u_3} [AddCommGroup W] [Module ℝ W] [AddCommGroup W'] [Module ℝ W'] (f : W →ₗ[ℝ] W') (u : TensorProduct ℝ ℂ W) : (tmulConj W') ((LinearMap.baseChange ℂ f) u) = (LinearMap.baseChange ℂ f) ((tmulConj W) u)

The conjugation of a complexification commutes with every base-changed map, because LinearMap.baseChange leaves the conjugated factor alone.

@[simp]

theorem TauCeti.realPart_baseChange {W : Type u_2} {W' : Type u_3} [AddCommGroup W] [Module ℝ W] [AddCommGroup W'] [Module ℝ W'] (f : W →ₗ[ℝ] W') (u : TensorProduct ℝ ℂ W) : (realPart W') ((LinearMap.baseChange ℂ f) u) = f ((realPart W) u)

Base change commutes with realPart.

@[simp]

theorem TauCeti.imaginaryPart_baseChange {W : Type u_2} {W' : Type u_3} [AddCommGroup W] [Module ℝ W] [AddCommGroup W'] [Module ℝ W'] (f : W →ₗ[ℝ] W') (u : TensorProduct ℝ ℂ W) : (imaginaryPart W') ((LinearMap.baseChange ℂ f) u) = f ((imaginaryPart W) u)

Base change commutes with imaginaryPart.

noncomputable def LinearEquiv.conjugationOfComplexification {V : Type u_1} [AddCommGroup V] [Module ℂ V] {W : Type u_2} [AddCommGroup W] [Module ℝ W] (e : TensorProduct ℝ ℂ W ≃ₗ[ℂ] V) : V →ₗ⋆[ℂ] V

Transport the existing tensor conjugation through a complexification equivalence. The result uses the native semilinear-map carrier.

theorem LinearEquiv.conjugationOfComplexification_apply {V : Type u_1} [AddCommGroup V] [Module ℂ V] {W : Type u_2} [AddCommGroup W] [Module ℝ W] (e : TensorProduct ℝ ℂ W ≃ₗ[ℂ] V) (v : V) : e.conjugationOfComplexification v = e ((TauCeti.tmulConj W) (e.symm v))

The defining transport formula for tensor conjugation.

@[simp]

theorem LinearEquiv.conjugationOfComplexification_apply_tmul {V : Type u_1} [AddCommGroup V] [Module ℂ V] {W : Type u_2} [AddCommGroup W] [Module ℝ W] (e : TensorProduct ℝ ℂ W ≃ₗ[ℂ] V) (c : ℂ) (w : W) : e.conjugationOfComplexification (e (c ⊗ₜ[ℝ] w)) = e (star c ⊗ₜ[ℝ] w)

The transported conjugation conjugates the scalar of the image of a pure tensor.

@[simp]

theorem LinearEquiv.conjugationOfComplexification_conjugationOfComplexification {V : Type u_1} [AddCommGroup V] [Module ℂ V] {W : Type u_2} [AddCommGroup W] [Module ℝ W] (e : TensorProduct ℝ ℂ W ≃ₗ[ℂ] V) (v : V) : e.conjugationOfComplexification (e.conjugationOfComplexification v) = v

Applying the transported tensor conjugation twice gives back the input.

theorem LinearEquiv.conjugationOfComplexification_involutive {V : Type u_1} [AddCommGroup V] [Module ℂ V] {W : Type u_2} [AddCommGroup W] [Module ℝ W] (e : TensorProduct ℝ ℂ W ≃ₗ[ℂ] V) : Function.Involutive ⇑e.conjugationOfComplexification

Transported tensor conjugation is involutive.

@[simp]

theorem LinearEquiv.conjugationOfComplexification_eq_self_iff {V : Type u_1} [AddCommGroup V] [Module ℂ V] {W : Type u_2} [AddCommGroup W] [Module ℝ W] (e : TensorProduct ℝ ℂ W ≃ₗ[ℂ] V) (v : V) : e.conjugationOfComplexification v = v ↔ ∃ (w : W), e (1 ⊗ₜ[ℝ] w) = v

The exact fixed locus is the image of the real inclusion w ↦ e (1 ⊗ w).

theorem LinearEquiv.conjugationOfComplexification_unique {V : Type u_1} [AddCommGroup V] [Module ℂ V] {W : Type u_2} [AddCommGroup W] [Module ℝ W] (e : TensorProduct ℝ ℂ W ≃ₗ[ℂ] V) (K : V →ₗ⋆[ℂ] V) (hfix : ∀ (w : W), K (e (1 ⊗ₜ[ℝ] w)) = e (1 ⊗ₜ[ℝ] w)) : K = e.conjugationOfComplexification

A conjugate-linear map fixing the real inclusion is uniquely the transported conjugation. No involutivity assumption on the competing map is necessary.

theorem LinearEquiv.conjugationOfComplexification_natural {V : Type u_1} [AddCommGroup V] [Module ℂ V] {W : Type u_2} {W' : Type u_3} {V' : Type u_4} [AddCommGroup W] [Module ℝ W] [AddCommGroup W'] [Module ℝ W'] [AddCommGroup V'] [Module ℂ V'] (e : TensorProduct ℝ ℂ W ≃ₗ[ℂ] V) (e' : TensorProduct ℝ ℂ W' ≃ₗ[ℂ] V') (A : V →ₗ[ℂ] V') (b : W →ₗ[ℝ] W') (hreal : ∀ (w : W), A (e (1 ⊗ₜ[ℝ] w)) = e' (1 ⊗ₜ[ℝ] b w)) (v : V) : e'.conjugationOfComplexification (A v) = A (e.conjugationOfComplexification v)

Transported conjugation is natural under complex-linear maps carrying the real inclusions to each other. The map between the real carriers need not be invertible.