Much like Matrix.reindex and Matrix.submatrix, we can reindex a Hermitian matrix to get another Hermitian matrix; however, this only makes sense when both permutations are the same, accordingly, HermitianMat.reindex only takes one Equiv argument (as opposed to Matrix.reindex's two).

This file then gives relevant lemmas for simplifying this.

def HermitianMat.reindex {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_5} [RCLike 𝕜] (A : HermitianMat d 𝕜) (e : d ≃ d₂) : HermitianMat d₂ 𝕜

Equations

• A.reindex e = ⟨(Matrix.reindex e e) ↑A, ⋯⟩

@[simp]

theorem HermitianMat.reindex_coe {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_5} [RCLike 𝕜] (A : HermitianMat d 𝕜) (e : d ≃ d₂) : ↑(A.reindex e) = (Matrix.reindex e e) ↑A

Our simp-normal form for expressions involving HermitianMat.reindex is that we try to push the reindexing as far out as possible, so that it can be absorbed by HermitianMat.trace, or cancelled our in a HermitianMat.inner. In places where it commutes (like HermitianMat.inner) we push it to the right side.

@[simp]

theorem HermitianMat.reindex_refl {d : Type u_1} (A : HermitianMat d ℂ) : A.reindex (Equiv.refl d) = A

@[simp]

theorem HermitianMat.reindex_reindex {d : Type u_1} {d₂ : Type u_2} {d₃ : Type u_3} (A : HermitianMat d ℂ) (e : d ≃ d₂) (f : d₂ ≃ d₃) : (A.reindex e).reindex f = A.reindex (e.trans f)

@[simp]

theorem HermitianMat.reindex_add {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_5} [RCLike 𝕜] (A B : HermitianMat d 𝕜) (e : d ≃ d₂) : A.reindex e + B.reindex e = (A + B).reindex e

@[simp]

theorem HermitianMat.reindex_sub {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_5} [RCLike 𝕜] (A B : HermitianMat d 𝕜) (e : d ≃ d₂) : A.reindex e - B.reindex e = (A - B).reindex e

@[simp]

theorem HermitianMat.reindex_conj {d : Type u_1} {d₂ : Type u_2} {d₃ : Type u_3} {𝕜 : Type u_5} [RCLike 𝕜] (A : HermitianMat d 𝕜) (e : d ≃ d₂) [Fintype d₂] [Fintype d] (B : Matrix d₃ d₂ 𝕜) : (conj B) (A.reindex e) = (conj (B.submatrix id ⇑e)) A

@[simp]

theorem HermitianMat.conj_submatrix {d : Type u_1} {d₂ : Type u_2} {d₃ : Type u_3} {d₄ : Type u_4} [Fintype d] (A : HermitianMat d ℂ) (B : Matrix d₂ d₄ ℂ) (e : d₃ ≃ d₂) (f : d → d₄) : (conj (B.submatrix (⇑e) f)) A = ((conj (B.submatrix id f)) A).reindex e.symm

theorem HermitianMat.ker_reindex {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_5} [RCLike 𝕜] (A : HermitianMat d 𝕜) (e : d ≃ d₂) [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] : (A.reindex e).ker = Submodule.comap (LinearEquiv.euclidean_of_relabel 𝕜 e) A.ker

@[simp]

theorem HermitianMat.ker_reindex_le_iff {d : Type u_1} {d₂ : Type u_2} {𝕜 : Type u_5} [RCLike 𝕜] (A B : HermitianMat d 𝕜) (e : d ≃ d₂) [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] : (A.reindex e).ker ≤ (B.reindex e).ker ↔ A.ker ≤ B.ker