Inner automorphisms #

This file defines the inner automorphism of a unitary matrix U as U x U⁻¹ and proves that any star-algebraic automorphism on Mₙ(ℂ) is an inner automorphism.

source

theorem RCLike.pos_ofReal {𝕜 : Type u_1} [RCLike 𝕜] {x : ℝ} :

0 ≤ ↑x ↔ 0 ≤ x

Alias of RCLike.zero_le_real.

source

theorem RCLike.neg_ofReal {𝕜 : Type u_1} [RCLike 𝕜] (a : ℝ) :

↑a < 0 ↔ a < 0

source

@[simp]

theorem StarAlgEquiv.trace_preserving {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (f : Matrix n n 𝕜 ≃⋆ₐ[𝕜] Matrix n n 𝕜) (x : Matrix n n 𝕜) :

(f x).trace = x.trace

source

def unitary.innerAutStarAlg (K : Type u_1) {R : Type u_2} [CommSemiring K] [Semiring R] [StarMul R] [Algebra K R] (a : ↥(unitary R)) :

R ≃⋆ₐ[K] R

Equations

unitary.innerAutStarAlg K a = StarAlgEquiv.ofAlgEquiv (Algebra.autInner ↑a) ⋯

Instances For

source

theorem unitary.innerAutStarAlg_apply {K : Type u_1} {R : Type u_2} [CommSemiring K] [Semiring R] [StarMul R] [Algebra K R] (U : ↥(unitary R)) (x : R) :

(unitary.innerAutStarAlg K U) x = ↑U * x * ↑(star U)

source

@[simp]

theorem unitary.innerAutStarAlg_apply' {K : Type u_1} {R : Type u_2} [CommSemiring K] [Semiring R] [StarMul R] [Algebra K R] (U : ↥(unitary R)) (x : R) :

(unitary.innerAutStarAlg K U) x = ↑U * x * ↑U⁻¹

source

theorem unitary.innerAutStarAlg_apply'' {K : Type u_1} {R : Type u_2} [CommSemiring K] [Semiring R] [StarMul R] [Algebra K R] (U : ↥(unitary R)) (x : R) :

(unitary.innerAutStarAlg K U) x = ↑U * x * star ↑U

source

theorem unitary.innerAutStarAlg_symm_apply {K : Type u_1} {R : Type u_2} [CommSemiring K] [Semiring R] [StarMul R] [Algebra K R] (U : ↥(unitary R)) (x : R) :

(unitary.innerAutStarAlg K U).symm x = ↑(star U) * x * ↑U

source

@[simp]

theorem unitary.innerAutStarAlg_symm_apply' {K : Type u_1} {R : Type u_2} [CommSemiring K] [Semiring R] [StarMul R] [Algebra K R] (U : ↥(unitary R)) (x : R) :

(unitary.innerAutStarAlg K U).symm x = ↑U⁻¹ * x * ↑U

source

theorem unitary.innerAutStarAlg_symm_apply'' {K : Type u_1} {R : Type u_2} [CommSemiring K] [Semiring R] [StarMul R] [Algebra K R] (U : ↥(unitary R)) (x : R) :

(unitary.innerAutStarAlg K U).symm x = star ↑U * x * ↑U

source

theorem unitary.innerAutStarAlg_symm {K : Type u_1} {R : Type u_2} [CommSemiring K] [Semiring R] [StarMul R] [Algebra K R] (U : ↥(unitary R)) :

(unitary.innerAutStarAlg K U).symm = unitary.innerAutStarAlg K U⁻¹

source

theorem unitary.innerAutStarAlg_symm' {K : Type u_1} {R : Type u_2} [CommSemiring K] [Semiring R] [StarMul R] [Algebra K R] (U : ↥(unitary R)) :

(unitary.innerAutStarAlg K U).symm = unitary.innerAutStarAlg K (star U)

source

instance Pi.coe {k : Type u_1} {s : k → Type u_2} {r : k → Type u_3} [(i : k) → CoeTC (s i) (r i)] :

CoeTC ((i : k) → s i) ((i : k) → r i)

Equations

Pi.coe = { coe := fun (U : (i : k) → s i) (i : k) => CoeTC.coe (U i) }

source

theorem Pi.coe_eq {k : Type u_1} {s : k → Type u_2} {r : k → Type u_3} [(i : k) → CoeTC (s i) (r i)] (U : (i : k) → s i) :

(fun (i : k) => CoeTC.coe (U i)) = fun (i : k) => CoeTC.coe (U i)

source

instance instCoeTCSubtypeMemSubmonoidUnitary_monlib (R : Type u_1) [Monoid R] [StarMul R] :

CoeTC (↥(unitary R)) R

Equations

instCoeTCSubtypeMemSubmonoidUnitary_monlib R = { coe := fun (x : ↥(unitary R)) => ↑x }

source

theorem unitary.pi_mem {k : Type u_1} {s : k → Type u_2} [(i : k) → Semiring (s i)] [(i : k) → StarMul (s i)] (U : (i : k) → ↥(unitary (s i))) :

(fun (i : k) => ↑(U i)) ∈ unitary ((i : k) → s i)

source

@[reducible, inline]

abbrev unitary.pi {k : Type u_1} {s : k → Type u_2} [(i : k) → Semiring (s i)] [(i : k) → StarMul (s i)] (U : (i : k) → ↥(unitary (s i))) :

↥(unitary ((i : k) → s i))

Equations

unitary.pi U = ⟨fun (i : k) => ↑(U i), ⋯⟩

Instances For

source

theorem unitary.pi_apply {k : Type u_1} {s : k → Type u_2} [(i : k) → Semiring (s i)] [(i : k) → StarMul (s i)] (U : (i : k) → ↥(unitary (s i))) {i : k} :

↑(unitary.pi U) i = ↑(U i)

source

@[simp]

theorem Matrix.unitaryGroup.coe_hMul_star_self {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (a : ↥(Matrix.unitaryGroup n 𝕜)) :

↑(a * star a) = 1

source

@[simp]

theorem Matrix.unitaryGroup.star_coe_eq_coe_star {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

star ↑U = ↑(star U)

source

@[reducible, inline]

abbrev Matrix.innerAutStarAlg {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (a : ↥(Matrix.unitaryGroup n 𝕜)) :

Matrix n n 𝕜 ≃⋆ₐ[𝕜] Matrix n n 𝕜

given a unitary $U$, we have the inner algebraic automorphism, given by $x \mapsto UxU^*$ with its inverse given by $x \mapsto U^* x U$

Equations

Matrix.innerAutStarAlg a = unitary.innerAutStarAlg 𝕜 a

Instances For

source

theorem Matrix.innerAutStarAlg_apply {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAutStarAlg U) x = ↑U * x * ↑(star U)

source

theorem Matrix.innerAutStarAlg_apply' {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAutStarAlg U) x = ↑U * x * ↑U⁻¹

source

theorem Matrix.innerAutStarAlg_symm_apply {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAutStarAlg U).symm x = ↑(star U) * x * ↑U

source

theorem Matrix.innerAutStarAlg_symm_apply' {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAutStarAlg U).symm x = ↑U⁻¹ * x * ↑U

source

@[simp]

theorem Matrix.innerAutStarAlg_symm {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

(Matrix.innerAutStarAlg U).symm = Matrix.innerAutStarAlg U⁻¹

source

@[reducible, inline]

abbrev Matrix.innerAut {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

Matrix n n 𝕜 →ₗ[𝕜] Matrix n n 𝕜

inner automorphism (matrix.innerAut_star_alg), but as a linear map

Equations

Matrix.innerAut U = (Matrix.innerAutStarAlg U).toLinearMap

Instances For

source

@[simp]

theorem Matrix.innerAut_coe {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

⇑(Matrix.innerAut U) = ⇑(Matrix.innerAutStarAlg U)

source

@[simp]

theorem Matrix.innerAut_inv_coe {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

⇑(Matrix.innerAut U⁻¹) = ⇑(Matrix.innerAutStarAlg U).symm

source

theorem Matrix.innerAut_apply {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAut U) x = ↑U * x * ↑U⁻¹

source

theorem Matrix.innerAut_apply' {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAut U) x = ↑U * x * ↑(star U)

source

theorem Matrix.innerAut_inv_apply {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAut U⁻¹) x = ↑U⁻¹ * x * ↑U

source

theorem Matrix.innerAut_star_apply {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAut (star U)) x = ↑(star U) * x * ↑U

source

theorem Matrix.innerAut_conjTranspose {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

((Matrix.innerAut U) x).conjTranspose = (Matrix.innerAut U) x.conjTranspose

source

theorem Matrix.innerAut_comp_innerAut {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U₁ : ↥(Matrix.unitaryGroup n 𝕜)) (U₂ : ↥(Matrix.unitaryGroup n 𝕜)) :

Matrix.innerAut U₁ ∘ₗ Matrix.innerAut U₂ = Matrix.innerAut (U₁ * U₂)

source

theorem Matrix.innerAut_apply_innerAut {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U₁ : ↥(Matrix.unitaryGroup n 𝕜)) (U₂ : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAut U₁) ((Matrix.innerAut U₂) x) = (Matrix.innerAut (U₁ * U₂)) x

source

theorem Matrix.innerAut_eq_iff {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) (y : Matrix n n 𝕜) :

(Matrix.innerAut U) x = y ↔ x = (Matrix.innerAut U⁻¹) y

source

theorem Matrix.unitaryGroup.toLinearEquiv_apply {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : n → 𝕜) :

(Matrix.UnitaryGroup.toLinearEquiv U) x = (↑U).mulVec x

source

theorem Matrix.unitaryGroup.toLinearEquiv_eq {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : n → 𝕜) :

(Matrix.UnitaryGroup.toLinearEquiv U) x = (Matrix.UnitaryGroup.toLin' U) x

source

theorem Matrix.unitaryGroup.toLin'_apply {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : n → 𝕜) :

(Matrix.UnitaryGroup.toLin' U) x = (↑U).mulVec x

source

theorem Matrix.unitaryGroup.toLin'_eq {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : n → 𝕜) :

(Matrix.UnitaryGroup.toLin' U) x = (Matrix.toLin' ↑U) x

source

theorem Matrix.toLinAlgEquiv'_apply' {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [DecidableEq n] (x : Matrix n n 𝕜) :

Matrix.toLinAlgEquiv' x = Matrix.toLin' x

source

theorem Matrix.innerAut.spectrum_eq {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

spectrum 𝕜 (Matrix.toLin' ((Matrix.innerAut U) x)) = spectrum 𝕜 (Matrix.toLin' x)

the spectrum of $U x U^*$ for any unitary $U$ is equal to the spectrum of $x$

source

theorem Matrix.innerAut_one {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] :

Matrix.innerAut 1 = 1

source

theorem Matrix.innerAut_comp_innerAut_inv {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

Matrix.innerAut U ∘ₗ Matrix.innerAut U⁻¹ = 1

source

theorem Matrix.innerAut_apply_innerAut_inv {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U₁ : ↥(Matrix.unitaryGroup n 𝕜)) (U₂ : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAut U₁) ((Matrix.innerAut U₂⁻¹) x) = (Matrix.innerAut (U₁ * U₂⁻¹)) x

source

theorem Matrix.innerAut_apply_innerAut_inv_self {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAut U) ((Matrix.innerAut U⁻¹) x) = x

source

theorem Matrix.innerAut_inv_apply_innerAut_self {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAut U⁻¹) ((Matrix.innerAut U) x) = x

source

theorem Matrix.innerAut_apply_zero {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

(Matrix.innerAut U) 0 = 0

source

theorem Matrix.innerAut_conj_spectrum_eq {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜 →ₗ[𝕜] Matrix n n 𝕜) :

spectrum 𝕜 (Matrix.innerAut U⁻¹ ∘ₗ x ∘ₗ Matrix.innerAut U) = spectrum 𝕜 x

the spectrum of a linear map $x$ equals the spectrum of $f_U^{-1} x f_U$ for some unitary $U$ and $f_U$ is the inner automorphism (matrix.innerAut)

source

theorem Matrix.innerAut_apply_one {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

(Matrix.innerAut U) 1 = 1

the inner automorphism is unital

source

theorem Matrix.innerAutStarAlg_apply_eq_innerAut_apply {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

(Matrix.innerAutStarAlg U) x = (Matrix.innerAut U) x

source

theorem Matrix.innerAut.map_mul {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) (y : Matrix n n 𝕜) :

(Matrix.innerAut U) (x * y) = (Matrix.innerAut U) x * (Matrix.innerAut U) y

source

theorem Matrix.innerAut.map_star {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

star ((Matrix.innerAut U) x) = (Matrix.innerAut U) (star x)

source

theorem Matrix.innerAut_inv_eq_star {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] {x : ↥(Matrix.unitaryGroup n 𝕜)} :

Matrix.innerAut x⁻¹ = Matrix.innerAut (star x)

source

theorem Matrix.unitaryGroup.coe_inv {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

↑U⁻¹ = (↑U)⁻¹

source

theorem Matrix.innerAut.map_inv {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

((Matrix.innerAut U) x)⁻¹ = (Matrix.innerAut U) x⁻¹

source

theorem Matrix.innerAut_apply_trace_eq {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

((Matrix.innerAut U) x).trace = x.trace

the trace of $f_U(x)$ is equal to the trace of $x$

source

theorem Matrix.exists_innerAut_iff_exists_innerAut_inv {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] {P : Matrix n n 𝕜 → Prop} (x : Matrix n n 𝕜) :

(∃ (U : ↥(Matrix.unitaryGroup n 𝕜)), P ((Matrix.innerAut U) x)) ↔ ∃ (U : ↥(Matrix.unitaryGroup n 𝕜)), P ((Matrix.innerAut U⁻¹) x)

source

theorem Matrix.innerAut.is_injective {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

Function.Injective ⇑(Matrix.innerAut U)

source

theorem Matrix.innerAut_isHermitian_iff {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

x.IsHermitian ↔ ((Matrix.innerAut U) x).IsHermitian

$x$ is Hermitian if and only if $f_U(x)$ is Hermitian

source

theorem Matrix.innerAut_posSemidef_iff {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) {a : Matrix n n 𝕜} :

((Matrix.innerAut U) a).PosSemidef ↔ a.PosSemidef

source

theorem Matrix.PosSemidef.innerAut {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] [DecidableEq n] {a : Matrix n n 𝕜} (ha : a.PosSemidef) (U : ↥(Matrix.unitaryGroup n 𝕜)) :

((Matrix.innerAut U) a).PosSemidef

source

theorem Matrix.unitaryGroup_conjTranspose {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

(↑U).conjTranspose = ↑U⁻¹

source

theorem Matrix.innerAut_posDef_iff {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) {x : Matrix n n 𝕜} :

((Matrix.innerAut U) x).PosDef ↔ x.PosDef

$f_U(x)$ is positive definite if and only if $x$ is positive definite

source

theorem Matrix.PosDef.innerAut {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] [DecidableEq n] {a : Matrix n n 𝕜} (ha : a.PosDef) (U : ↥(Matrix.unitaryGroup n 𝕜)) :

((Matrix.innerAut U) a).PosDef

source

theorem Matrix.IsAlmostHermitian.schur_decomp {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_1} [RCLike 𝕜] [DecidableEq 𝕜] {A : Matrix n n 𝕜} (hA : A.IsAlmostHermitian) :

∃ (D : n → 𝕜) (U : ↥(Matrix.unitaryGroup n 𝕜)), (Matrix.innerAut U) (Matrix.diagonal D) = A

Schur decomposition, but only for almost Hermitian matrices: given an almost Hermitian matrix $A$, there exists a diagonal matrix $D$ and a unitary matrix $U$ such that $UDU^*=A$

source

theorem toEuclideanLin_one {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] [DecidableEq n] :

Matrix.toEuclideanLin 1 = 1

source

theorem StarAlgEquiv.of_matrix_is_inner {n : Type u_2} {𝕜 : Type u_1} [Fintype n] [RCLike 𝕜] [DecidableEq n] (f : Matrix n n 𝕜 ≃⋆ₐ[𝕜] Matrix n n 𝕜) :

∃ (U : ↥(Matrix.unitaryGroup n 𝕜)), Matrix.innerAutStarAlg U = f

any $^*$-isomorphism on $M_n$ is an inner automorphism

source

noncomputable def StarAlgEquiv.of_matrix_unitary {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] [DecidableEq n] (f : Matrix n n 𝕜 ≃⋆ₐ[𝕜] Matrix n n 𝕜) :

↥(Matrix.unitaryGroup n 𝕜)

Equations

f.of_matrix_unitary = (fun (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix.innerAutStarAlg U = f) => U) (Classical.choose ⋯) ⋯

Instances For

source

theorem StarAlgEquiv.eq_innerAut {n : Type u_2} {𝕜 : Type u_1} [Fintype n] [RCLike 𝕜] [DecidableEq n] (f : Matrix n n 𝕜 ≃⋆ₐ[𝕜] Matrix n n 𝕜) :

Matrix.innerAutStarAlg f.of_matrix_unitary = f

source

theorem Matrix.IsHermitian.spectral_theorem'' {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_1} [RCLike 𝕜] {x : Matrix n n 𝕜} (hx : x.IsHermitian) :

x = (Matrix.innerAut hx.eigenvectorUnitary) (Matrix.diagonal (RCLike.ofReal ∘ hx.eigenvalues))

source

theorem Matrix.coe_diagonal_eq_diagonal_coe {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [DecidableEq n] (x : n → ℝ) :

Matrix.diagonal (RCLike.ofReal ∘ x) = CoeTC.coe ∘ Matrix.diagonal x

source

theorem Matrix.diagonal.spectrum {𝕜 : Type u_1} {n : Type u_2} [Field 𝕜] [Fintype n] [DecidableEq n] (A : n → 𝕜) :

spectrum 𝕜 (Matrix.toLin' (Matrix.diagonal A)) = {x : 𝕜 | ∃ (i : n), A i = x}

source

theorem Matrix.IsHermitian.spectrum {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.IsHermitian) :

spectrum 𝕜 (Matrix.toLin' x) = {x_1 : 𝕜 | ∃ (i : n), ↑(hx.eigenvalues i) = x_1}

source

theorem Matrix.IsHermitian.hasEigenvalue_iff {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_1} [RCLike 𝕜] [DecidableEq 𝕜] {x : Matrix n n 𝕜} (hx : x.IsHermitian) (α : 𝕜) :

Module.End.HasEigenvalue (Matrix.toLin' x) α ↔ ∃ (i : n), ↑(hx.eigenvalues i) = α

source

theorem Matrix.innerAut_commutes_with_map_lid_symm {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

TensorProduct.map 1 (Matrix.innerAut U) ∘ₗ ↑(TensorProduct.lid 𝕜 (Matrix n n 𝕜)).symm = ↑(TensorProduct.lid 𝕜 (Matrix n n 𝕜)).symm ∘ₗ Matrix.innerAut U

source

theorem Matrix.innerAut_commutes_with_lid_comm {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

↑(TensorProduct.lid 𝕜 (Matrix n n 𝕜)) ∘ₗ ↑(TensorProduct.comm 𝕜 (Matrix n n 𝕜) 𝕜) ∘ₗ TensorProduct.map (Matrix.innerAut U) 1 = Matrix.innerAut U ∘ₗ ↑(TensorProduct.lid 𝕜 (Matrix n n 𝕜)) ∘ₗ ↑(TensorProduct.comm 𝕜 (Matrix n n 𝕜) 𝕜)

source

theorem Matrix.unitaryGroup.conj_mem {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

(↑U).conj ∈ Matrix.unitaryGroup n 𝕜

source

def Matrix.unitaryGroup.conj {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

↥(Matrix.unitaryGroup n 𝕜)

Equations

Matrix.unitaryGroup.conj U = ⟨(↑U).conj, ⋯⟩

Instances For

source

theorem Matrix.unitaryGroup.conj_coe {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

↑(Matrix.unitaryGroup.conj U) = (↑U).conj

source

theorem Matrix.innerAut.conj {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) :

((Matrix.innerAut U) x).conj = (Matrix.innerAut (Matrix.unitaryGroup.conj U)) x.conj

source

theorem Matrix.UnitaryGroup.mul_star_self {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

↑U * star ↑U = 1

source

theorem Matrix.kronecker_mem_unitaryGroup {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] [DecidableEq n] {p : Type u_1} [Fintype p] [DecidableEq p] (U₁ : ↥(Matrix.unitaryGroup n 𝕜)) (U₂ : ↥(Matrix.unitaryGroup p 𝕜)) :

Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) ↑U₁ ↑U₂ ∈ Matrix.unitaryGroup (n × p) 𝕜

source

def Matrix.unitaryGroup.kronecker {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] [DecidableEq n] {p : Type u_3} [Fintype p] [DecidableEq p] (U₁ : ↥(Matrix.unitaryGroup n 𝕜)) (U₂ : ↥(Matrix.unitaryGroup p 𝕜)) :

↥(Matrix.unitaryGroup (n × p) 𝕜)

Equations

Matrix.unitaryGroup.kronecker U₁ U₂ = ⟨Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) ↑U₁ ↑U₂, ⋯⟩

Instances For

source

theorem Matrix.unitaryGroup.kronecker_coe {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] [DecidableEq n] {p : Type u_1} [Fintype p] [DecidableEq p] (U₁ : ↥(Matrix.unitaryGroup n 𝕜)) (U₂ : ↥(Matrix.unitaryGroup p 𝕜)) :

↑(Matrix.unitaryGroup.kronecker U₁ U₂) = Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) ↑U₁ ↑U₂

source

theorem Matrix.innerAut_kronecker {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] [DecidableEq n] {p : Type u_1} [Fintype p] [DecidableEq p] (U₁ : ↥(Matrix.unitaryGroup n 𝕜)) (U₂ : ↥(Matrix.unitaryGroup p 𝕜)) (x : Matrix n n 𝕜) (y : Matrix p p 𝕜) :

Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) ((Matrix.innerAut U₁) x) ((Matrix.innerAut U₂) y) = (Matrix.innerAut (Matrix.unitaryGroup.kronecker U₁ U₂)) (Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) x y)

source

theorem Matrix.PosSemidef.kronecker {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_1} {p : Type u_2} [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p] {x : Matrix n n 𝕜} {y : Matrix p p 𝕜} (hx : x.PosSemidef) (hy : y.PosSemidef) :

(Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) x y).PosSemidef

source

theorem Matrix.PosDef.kronecker {𝕜 : Type u_1} {n : Type u_2} {p : Type u_3} [RCLike 𝕜] [DecidableEq 𝕜] [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p] {x : Matrix n n 𝕜} {y : Matrix p p 𝕜} (hx : x.PosDef) (hy : y.PosDef) :

(Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) x y).PosDef

source

theorem Matrix.unitaryGroup.injective_hMul {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] (U : ↥(Matrix.unitaryGroup n 𝕜)) (x : Matrix n n 𝕜) (y : Matrix n n 𝕜) :

x = y ↔ x * ↑U = y * ↑U

source

theorem Matrix.innerAutStarAlg_equiv_toLinearMap {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] [DecidableEq 𝕜] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

(Matrix.innerAutStarAlg U).toLinearMap = Matrix.innerAut U

source

theorem Matrix.innerAutStarAlg_equiv_symm_toLinearMap {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] (U : ↥(Matrix.unitaryGroup n 𝕜)) :

(Matrix.innerAutStarAlg U).symm.toLinearMap = Matrix.innerAut U⁻¹

source

theorem Matrix.innerAut.comp_inj {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] (U : ↥(Matrix.unitaryGroup n 𝕜)) (S : Matrix n n 𝕜 →ₗ[𝕜] Matrix n n 𝕜) (T : Matrix n n 𝕜 →ₗ[𝕜] Matrix n n 𝕜) :

S = T ↔ Matrix.innerAut U ∘ₗ S = Matrix.innerAut U ∘ₗ T

source

theorem Matrix.innerAut.inj_comp {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] (U : ↥(Matrix.unitaryGroup n 𝕜)) (S : Matrix n n 𝕜 →ₗ[𝕜] Matrix n n 𝕜) (T : Matrix n n 𝕜 →ₗ[𝕜] Matrix n n 𝕜) :

S = T ↔ S ∘ₗ Matrix.innerAut U = T ∘ₗ Matrix.innerAut U

Documentation

Monlib.LinearAlgebra.InnerAut

Inner automorphisms #