Relabelling linear equivalences

i. Overview

This module provides linear equivalences obtained by relabelling the index type of a finite function space d → R or of EuclideanSpace 𝕜 d along an index equivalence e : d ≃ d₂, together with lemmas relating them to Matrix.reindex.

ii. Key results

• LinearEquiv.of_relabel : the R-linear equivalence (d₂ → R) ≃ₗ[R] (d → R) induced by an index equivalence e : d ≃ d₂.
• LinearEquiv.euclidean_of_relabel : the EuclideanSpace analogue of of_relabel.
• Matrix.reindex_toLin' and Matrix.reindex_toEuclideanLin : reindexing a matrix conjugates its associated linear map by these relabelling equivalences.

iii. Table of contents

This can be filled in later.

iv. References

def LinearEquiv.of_relabel {d : Type u_1} {d₂ : Type u_3} (R : Type u_7) [Semiring R] (e : d ≃ d₂) : (d₂ → R) ≃ₗ[R] d → R

The R-linear equivalence (d₂ → R) ≃ₗ[R] (d → R) that relabels the coordinates of a function along an index equivalence e : d ≃ d₂. This is the linear-equivalence packaging of Equiv.piCongrLeft.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.of_relabel_apply {d : Type u_1} {d₂ : Type u_3} (R : Type u_7) [Semiring R] (e : d ≃ d₂) (a✝ : d₂ → R) (b : d) : (of_relabel R e) a✝ b = (Equiv.piCongrLeft (fun (x : d) => R) e.symm).toFun a✝ b

@[simp]

theorem LinearEquiv.of_relabel_symm_apply {d : Type u_1} {d₂ : Type u_3} (R : Type u_7) [Semiring R] (e : d ≃ d₂) (a✝ : d → R) (a : d₂) : (of_relabel R e).symm a✝ a = (Equiv.piCongrLeft (fun (x : d) => R) e.symm).invFun a✝ a

def LinearEquiv.euclidean_of_relabel {d : Type u_1} {d₂ : Type u_3} (𝕜 : Type u_6) [RCLike 𝕜] (e : d ≃ d₂) : EuclideanSpace 𝕜 d₂ ≃ₗ[𝕜] EuclideanSpace 𝕜 d

The 𝕜-linear equivalence EuclideanSpace 𝕜 d₂ ≃ₗ[𝕜] EuclideanSpace 𝕜 d that relabels the coordinates of a vector along an index equivalence e : d ≃ d₂. This is the EuclideanSpace analogue of LinearEquiv.of_relabel, obtained by transporting it across the WithLp identifications.

Equations

• LinearEquiv.euclidean_of_relabel 𝕜 e = (WithLp.linearEquiv 2 𝕜 ((i : d₂) → (fun (x : d₂) => 𝕜) i)).trans ((LinearEquiv.of_relabel 𝕜 e).trans (WithLp.linearEquiv 2 𝕜 (d → 𝕜)).symm)

@[simp]

theorem LinearEquiv.euclidean_of_relabel_symm_apply_ofLp {d : Type u_1} {d₂ : Type u_3} (𝕜 : Type u_6) [RCLike 𝕜] (e : d ≃ d₂) (a✝ : EuclideanSpace 𝕜 d) (i : d₂) : ((euclidean_of_relabel 𝕜 e).symm a✝).ofLp i = a✝.ofLp (e.symm i)

@[simp]

theorem LinearEquiv.euclidean_of_relabel_apply_ofLp {d : Type u_1} {d₂ : Type u_3} (𝕜 : Type u_6) [RCLike 𝕜] (e : d ≃ d₂) (x : WithLp 2 ((i : d₂) → (fun (x : d₂) => 𝕜) i)) (a✝ : d) : ((euclidean_of_relabel 𝕜 e) x).ofLp a✝ = (Equiv.piCongrLeft (fun (x : d) => 𝕜) e.symm) x.ofLp a✝

@[simp]

theorem LinearEquiv.of_relabel_refl {d : Type u_1} {R : Type u_7} [Semiring R] : of_relabel R (Equiv.refl d) = refl R (d → R)

@[simp]

theorem LinearEquiv.euclidean_of_relabel_refl {d : Type u_1} {𝕜 : Type u_6} [RCLike 𝕜] : euclidean_of_relabel 𝕜 (Equiv.refl d) = refl 𝕜 (EuclideanSpace 𝕜 d)

theorem Matrix.reindex_toLin' {d : Type u_1} {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} {R : Type u_7} [CommSemiring R] [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (e : d₁ ≃ d₃) (f : d₂ ≃ d) (M : Matrix d₁ d₂ R) : toLin' ((reindex e f) M) = ↑(LinearEquiv.of_relabel R e.symm) ∘ₗ toLin' M ∘ₗ ↑(LinearEquiv.of_relabel R f)

theorem Matrix.reindex_toEuclideanLin {d : Type u_1} {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} {𝕜 : Type u_6} [RCLike 𝕜] [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (e : d₁ ≃ d₃) (f : d₂ ≃ d) (M : Matrix d₁ d₂ 𝕜) : toEuclideanLin ((reindex e f) M) = ↑(LinearEquiv.euclidean_of_relabel 𝕜 e.symm) ∘ₗ toEuclideanLin M ∘ₗ ↑(LinearEquiv.euclidean_of_relabel 𝕜 f)

theorem Matrix.reindex_right_toLin' {d : Type u_1} {d₂ : Type u_3} {d₃ : Type u_4} {R : Type u_7} [CommSemiring R] [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (e : d ≃ d₂) (M : Matrix d₃ d R) : toLin' ((reindex (Equiv.refl d₃) e) M) = toLin' M ∘ₗ ↑(LinearEquiv.of_relabel R e)

theorem Matrix.reindex_right_toEuclideanLin {d : Type u_1} {d₂ : Type u_3} {d₃ : Type u_4} {𝕜 : Type u_6} [RCLike 𝕜] [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (e : d ≃ d₂) (M : Matrix d₃ d 𝕜) : toEuclideanLin ((reindex (Equiv.refl d₃) e) M) = toEuclideanLin M ∘ₗ ↑(LinearEquiv.euclidean_of_relabel 𝕜 e)

theorem Matrix.reindex_left_toLin' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} {R : Type u_7} [CommSemiring R] [Fintype d₂] [DecidableEq d₂] (e : d₁ ≃ d₃) (M : Matrix d₁ d₂ R) : ⇑(toLin' ((reindex e (Equiv.refl d₂)) M)) = ⇑(LinearEquiv.of_relabel R e.symm) ∘ ⇑(toLin' M)

theorem Matrix.reindex_left_toEuclideanLin {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} {𝕜 : Type u_6} [RCLike 𝕜] [Fintype d₂] [DecidableEq d₂] (e : d₁ ≃ d₃) (M : Matrix d₁ d₂ 𝕜) : ⇑(toEuclideanLin ((reindex e (Equiv.refl d₂)) M)) = ⇑(LinearEquiv.euclidean_of_relabel 𝕜 e.symm) ∘ ⇑(toEuclideanLin M)