Documentation

TauCeti.LinearAlgebra.TotallyReal.Complex

Totally real subspaces of complex modules #

This file gives an elementary example of a totally real real subspace of a complex module and develops the complex-linear algebra of maximal totally real subspaces. A real basis of such a subspace is a complex basis of the ambient space. Complex-linear automorphisms act transitively on these subspaces, and an endomorphism preserving one has real determinant.

Main declarations #

source
theorem TauCeti.isTotallyReal_range_pi_smulRight {ι : Type u_1} {v : ι → ℂ} :
IsTotallyReal (↑ℝ ((LinearMap.lsmul ℂ (ι → ℂ)) Complex.I)) (LinearMap.pi fun (i : ι) => (LinearMap.proj i).smulRight (v i)).range

The real span of vectors, one in each coordinate, is totally real. The image of the real-linear map τ ↦ (τ i • v i)ᵢ from ι → ℝ to ι → ℂ meets its image under multiplication by i only in 0.

source
theorem TauCeti.IsTotallyReal.linearIndependent_complex {E : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] {L : Submodule ℝ E} (hL : IsTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) {ι : Type u_3} {v : ι → E} (hv : LinearIndependent ℝ v) (hvL : ∀ (i : ι), v i ∈ L) :
LinearIndependent ℂ v

Vectors of a totally real subspace of a complex module that are linearly independent over ℝ are linearly independent over ℂ.

source
theorem TauCeti.IsMaximalTotallyReal.span_complex_eq_top {E : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] {L : Submodule ℝ E} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) {ι : Type u_3} {v : ι → E} (hv : Submodule.span ℝ (Set.range v) = L) :
Submodule.span ℂ (Set.range v) = ⊤

Vectors spanning a maximal totally real subspace over ℝ span the ambient complex module over ℂ.

source
noncomputable def TauCeti.IsMaximalTotallyReal.complexBasis {E : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] {L : Submodule ℝ E} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) {ι : Type u_3} (b : Module.Basis ι ℝ ↥L) :
Module.Basis ι ℂ E

A real basis of a maximal totally real subspace L of a complex module E is a complex basis of E: L is a real form of E.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.IsMaximalTotallyReal.complexBasis_apply {E : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] {L : Submodule ℝ E} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) {ι : Type u_3} (b : Module.Basis ι ℝ ↥L) (i : ι) :
    (hL.complexBasis b) i = ↑(b i)
    source
    @[simp]
    theorem TauCeti.IsMaximalTotallyReal.complexBasis_repr_coe {E : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] {L : Submodule ℝ E} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) {ι : Type u_3} (b : Module.Basis ι ℝ ↥L) (x : ↥L) (i : ι) :
    ((hL.complexBasis b).repr ↑x) i = ↑((b.repr x) i)

    The complex coordinates of a vector of L in complexBasis b are its real coordinates in b.

    source
    theorem TauCeti.IsMaximalTotallyReal.map_linearEquiv {E : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] {L : Submodule ℝ E} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) (A : E ≃ₗ[ℂ] E) :
    IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) (Submodule.map (↑ℝ ↑A) L)

    A complex-linear automorphism maps maximal totally real subspaces to maximal totally real subspaces.

    source
    theorem TauCeti.IsMaximalTotallyReal.finrank_eq_finrank_complex {E : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] {L : Submodule ℝ E} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) [FiniteDimensional ℂ E] :
    Module.finrank ℝ ↥L = Module.finrank ℂ E

    A maximal totally real subspace has real dimension equal to the complex dimension of the ambient module.

    source
    theorem TauCeti.IsMaximalTotallyReal.det_eq_det_restrict {E : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] {L : Submodule ℝ E} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) [FiniteDimensional ℂ E] (f : E →ₗ[ℂ] E) (hf : ∀ x ∈ L, f x ∈ L) :
    LinearMap.det f = ↑(LinearMap.det ((↑ℝ f).restrict hf))

    A complex-linear endomorphism f preserving a maximal totally real subspace L is the complexification of its restriction to L, so its determinant is the (real) determinant of that restriction.

    source
    theorem TauCeti.IsMaximalTotallyReal.exists_linearEquiv_map_eq {E : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] {L : Submodule ℝ E} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) [FiniteDimensional ℂ E] {L' : Submodule ℝ E} (hL' : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L') :
    ∃ (A : E ≃ₗ[ℂ] E), Submodule.map (↑ℝ ↑A) L = L'

    The complex-linear automorphisms act transitively on the maximal totally real subspaces of a finite-dimensional complex module.

    source
    theorem TauCeti.IsMaximalTotallyReal.isMaximalTotallyReal_prod {E : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] {L : Submodule ℝ E} {E' : Type u_3} [AddCommGroup E'] [Module ℝ E'] [Module ℂ E'] [IsScalarTower ℝ ℂ E'] {M : Submodule ℝ E'} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) (hM : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E') Complex.I)) M) :
    IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ (E × E')) Complex.I)) (L.prod M)

    A direct sum of maximal totally real subspaces is maximal totally real. The coordinate submodule L.prod M of a product of complex modules is maximal totally real for multiplication by i whenever the two summands are.