Linear equivalence conjugation compatibility

Mathlib's LinearEquiv.conjAlgEquiv is the current version of the upstream LinearEquiv.innerConj construction used by the Monlib4 IncludeBlock slice.

noncomputable def OrthonormalBasis.toMatrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {E : Type u_3} [Fintype n] [DecidableEq n] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : OrthonormalBasis n 𝕜 E) : (E →ₗ[𝕜] E) ≃⋆ₐ[𝕜] Matrix n n 𝕜

Star-algebra equivalence from endomorphisms of a finite-dimensional inner-product space to matrices in an orthonormal basis.

Equations

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

theorem OrthonormalBasis.toMatrix_apply {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_1} {E : Type u_2} [Fintype n] [DecidableEq n] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : OrthonormalBasis n 𝕜 E) (x : E →ₗ[𝕜] E) (i j : n) : b.toMatrix x i j = inner 𝕜 (b i) (x (b j))

theorem OrthonormalBasis.toMatrix_symm_apply {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_1} {E : Type u_2} [Fintype n] [DecidableEq n] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : OrthonormalBasis n 𝕜 E) (x : Matrix n n 𝕜) : b.toMatrix.symm x = ∑ i : n, ∑ j : n, x i j • ↑(((InnerProductSpace.rankOne 𝕜) (b i)) (b j))

theorem OrthonormalBasis.toMatrix_symm_apply' {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_1} {E : Type u_2} [Fintype n] [DecidableEq n] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : OrthonormalBasis n 𝕜 E) (x : Matrix n n 𝕜) : b.toMatrix.symm x = ∑ i : n, ∑ j : n, x i j • ↑(((InnerProductSpace.rankOne 𝕜) (b i)) (b j))

theorem orthonormalBasis_toMatrix_eq_basis_toMatrix {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_1} {E : Type u_2} [Fintype n] [DecidableEq n] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : OrthonormalBasis n 𝕜 E) : LinearMap.toMatrixAlgEquiv b.toBasis = b.toMatrix.toAlgEquiv

def EuclideanSpace.orthonormalBasis (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] : OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι)

Alias of EuclideanSpace.basisFun.

---

The basis Pi.basisFun, bundled as an orthonormal basis of EuclideanSpace 𝕜 ι.

Equations

• EuclideanSpace.orthonormalBasis = EuclideanSpace.basisFun

theorem EuclideanSpace.orthonormalBasis.repr_eq_one {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] : (orthonormalBasis n 𝕜).repr = 1

theorem LinearIsometryEquiv.toLinearEquiv_one {R : Type u_1} {E : Type u_2} [Semiring R] [SeminormedAddCommGroup E] [Module R E] : toLinearEquiv 1 = 1

theorem LinearEquiv.one_symm {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] : symm 1 = 1

theorem LinearEquiv.toLinearMap_one {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] : ↑1 = 1

theorem LinearEquiv.refl_conj {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommMonoid E] [Module R E] : (refl R E).conj = 1

theorem LinearEquiv.conj_hMul {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] (f : E ≃ₗ[R] F) (x y : Module.End R E) : f.conj (x * y) = f.conj x * f.conj y

theorem LinearEquiv.conj_apply_one {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] (f : E ≃ₗ[R] F) : f.conj 1 = 1

theorem LinearEquiv.conj_one {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommMonoid E] [Module R E] : conj 1 = 1

theorem LinearEquiv.one_apply {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommMonoid E] [Module R E] (x : E) : 1 x = x

theorem OrthonormalBasis.std_toMatrix {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] [DecidableEq n] : (EuclideanSpace.orthonormalBasis n 𝕜).toMatrix.symm.toLinearEquiv = Matrix.toEuclideanLin

def LinearEquiv.innerConj {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] (e : E ≃ₗ[R] F) : Module.End R E ≃ₐ[R] Module.End R F

Conjugate endomorphism algebras along a linear equivalence.

Equations

• e.innerConj = LinearEquiv.conjAlgEquiv R e

theorem LinearEquiv.innerConj_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] (e : E ≃ₗ[R] F) (f : Module.End R E) : e.innerConj f = ↑e ∘ₗ f ∘ₗ ↑e.symm

theorem Matrix.stdBasis_repr_eq_reshape {R : Type u_1} {I : Type u_2} {J : Type u_3} [Fintype I] [Finite J] [CommSemiring R] : (stdBasis R I J).equivFun = reshape

theorem LinearMap.toMatrix_stdBasis_stdBasis {R : Type u_3} {I : Type u_5} {J : Type u_4} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] {K : Type u_1} {L : Type u_2} [Fintype K] [Finite L] (x : Matrix I J R →ₗ[R] Matrix K L R) : (toMatrix (Matrix.stdBasis R I J) (Matrix.stdBasis R K L)) x = toMatrix' (↑Matrix.reshape ∘ₗ x ∘ₗ ↑Matrix.reshape.symm)

theorem LinearMap.toLin_stdBasis_stdBasis {R : Type u_5} {I : Type u_4} {J : Type u_3} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] {K : Type u_1} {L : Type u_2} [Fintype K] [Finite L] (x : Matrix (K × L) (I × J) R) : (Matrix.toLin (Matrix.stdBasis R I J) (Matrix.stdBasis R K L)) x = ↑Matrix.reshape.symm ∘ₗ Matrix.toLin' x ∘ₗ ↑Matrix.reshape

def LinearMap.toMatrixOfAlgEquiv {R : Type u_1} {I : Type u_2} {J : Type u_3} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] : (Matrix I J R →ₗ[R] Matrix I J R) ≃ₐ[R] Matrix (I × J) (I × J) R

Identify endomorphisms of a matrix space with matrices on the reshaped index type.

Equations

• LinearMap.toMatrixOfAlgEquiv = Matrix.reshape.innerConj.trans LinearMap.toMatrixAlgEquiv'

theorem LinearMap.toMatrixOfAlgEquiv_apply {R : Type u_1} {I : Type u_3} {J : Type u_2} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix I J R →ₗ[R] Matrix I J R) : toMatrixOfAlgEquiv x = toMatrixAlgEquiv' (↑Matrix.reshape ∘ₗ x ∘ₗ ↑Matrix.reshape.symm)

theorem LinearMap.toMatrixOfAlgEquiv_symm_apply {R : Type u_3} {I : Type u_2} {J : Type u_1} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix (I × J) (I × J) R) : toMatrixOfAlgEquiv.symm x = ↑Matrix.reshape.symm ∘ₗ toMatrixAlgEquiv'.symm x ∘ₗ ↑Matrix.reshape

theorem LinearMap.toMatrixOfAlgEquiv_apply' {R : Type u_1} {I : Type u_3} {J : Type u_2} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix I J R →ₗ[R] Matrix I J R) (ij kl : I × J) : toMatrixOfAlgEquiv x ij kl = x (Matrix.single kl.1 kl.2 1) ij.1 ij.2

def Matrix.toLinOfAlgEquiv {R : Type u_1} {I : Type u_2} {J : Type u_3} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] : Matrix (I × J) (I × J) R ≃ₐ[R] Matrix I J R →ₗ[R] Matrix I J R

The inverse algebra equivalence turning a matrix on I × J into an endomorphism of Matrix I J R.

Equations

• Matrix.toLinOfAlgEquiv = LinearMap.toMatrixOfAlgEquiv.symm

theorem Matrix.toLinOfAlgEquiv_apply {R : Type u_3} {I : Type u_2} {J : Type u_1} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix (I × J) (I × J) R) (y : Matrix I J R) : (toLinOfAlgEquiv x) y = reshape.symm ((toLinAlgEquiv' x) (reshape y))

def Matrix.rankOneStdBasis {R : Type u_1} [CommSemiring R] {I : Type u_2} {J : Type u_3} [DecidableEq I] [DecidableEq J] (ij kl : I × J) (r : R) : Matrix I J R →ₗ[R] Matrix I J R

Rank-one endomorphism on the standard basis of a matrix space.

Equations

• Matrix.rankOneStdBasis ij kl r = { toFun := fun (x : Matrix I J R) => Matrix.single ij.1 ij.2 (r • r • x kl.1 kl.2), map_add' := ⋯, map_smul' := ⋯ }

theorem Matrix.rankOneStdBasis_apply {R : Type u_3} [CommSemiring R] {I : Type u_1} {J : Type u_2} [DecidableEq I] [DecidableEq J] (ij kl : I × J) (r : R) (x : Matrix I J R) : (rankOneStdBasis ij kl r) x = single ij.1 ij.2 (r • r • x kl.1 kl.2)

theorem Matrix.toLinOfAlgEquiv_eq {R : Type u_3} {I : Type u_2} {J : Type u_1} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix (I × J) (I × J) R) : toLinOfAlgEquiv x = ∑ ij : I × J, ∑ kl : I × J, x ij kl • rankOneStdBasis ij kl 1

theorem Matrix.toLinOfAlgEquiv_toMatrixOfAlgEquiv {R : Type u_3} {I : Type u_2} {J : Type u_1} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix (I × J) (I × J) R) : LinearMap.toMatrixOfAlgEquiv (toLinOfAlgEquiv x) = x

theorem LinearMap.toMatrixOfAlgEquiv_toLinOfAlgEquiv {R : Type u_1} {I : Type u_3} {J : Type u_2} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix I J R →ₗ[R] Matrix I J R) : Matrix.toLinOfAlgEquiv (toMatrixOfAlgEquiv x) = x

theorem innerAut_toMatrix {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] (U : ↥(Matrix.unitaryGroup n 𝕜)) : LinearMap.toMatrixOfAlgEquiv (Matrix.innerAut U) = Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) (↑U) (↑U).conj

theorem innerAut_coord {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] (U : ↥(Matrix.unitaryGroup n 𝕜)) (ij kl : n × n) : LinearMap.toMatrixOfAlgEquiv (Matrix.innerAut U) ij kl = ↑U ij.1 kl.1 * star (↑U ij.2 kl.2)

theorem innerAut_inv_coord {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n ℂ)) (ij kl : n × n) : LinearMap.toMatrixOfAlgEquiv (Matrix.innerAut U⁻¹) ij kl = ↑U kl.2 ij.2 * star (↑U kl.1 ij.1)