Documentation

LeanPool.Monlib4.LinearAlgebra.InnerAut

Inner Automorphisms #

This file ports the upstream monlib4 unitary inner-automorphism interface. In current Mathlib the general star-algebra automorphism by unitary conjugation is available as Unitary.conjStarAlgAut; the declarations here keep monlib4's names for the matrix-algebra specialization and its trace, spectrum, and Hermitian-preservation lemmas.

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

↑a < 0 ↔ a < 0

@[implicit_reducible]

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) }

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)

@[simp]

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

(f x).trace = x.trace

@[reducible, inline]

abbrev unitary.innerAutStarAlg (K : Type u_1) {R : Type u_2} [Semiring R] [StarMul R] [SMul K R] [IsScalarTower K R R] [SMulCommClass K R R] (a : ↥(unitary R)) :

R ≃⋆ₐ[K] R

The star-algebra automorphism given by conjugation with a unitary element.

Equations

unitary.innerAutStarAlg K a = (Unitary.conjStarAlgAut K R) a

Instances For

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[implicit_reducible]

instance unitary.instCoeTCSubtypeMemSubmonoidLeanPool (R : Type u_1) [Monoid R] [StarMul R] :

CoeTC (↥(unitary R)) R

Equations

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

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)

@[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))

Build a unitary element of a dependent function type from pointwise unitaries.

Equations

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

Instances For

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} :

↑(pi U) i = ↑(U i)

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

↑(a * star a) = 1

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

star ↑U = ↑(star U)

@[reducible, inline]

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

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

The star-algebra automorphism x ↦ U * x * U⁻¹.

Equations

Matrix.innerAutStarAlg a = unitary.innerAutStarAlg 𝕜 a

Instances For

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

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

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

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

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

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

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

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

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

(innerAutStarAlg U).symm = innerAutStarAlg U⁻¹

@[reducible, inline]

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

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

The unitary inner automorphism as a linear map.

Equations

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

Instances For

@[simp]

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

⇑(innerAut U) = ⇑(innerAutStarAlg U)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

toLinAlgEquiv' x = toLin' x

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

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

The spectrum of U * x * U⁻¹ is the spectrum of x.

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

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

innerAut U ∘ₗ innerAut U⁻¹ = 1

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

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

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

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

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

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

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

(innerAut U) 0 = 0

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

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

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

(innerAut U) 1 = 1

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

(innerAutStarAlg U) x = (innerAut U) x

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

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

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

star ((innerAut U) x) = (innerAut U) (star x)

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

innerAut x⁻¹ = innerAut (star x)

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

↑U⁻¹ = (↑U)⁻¹

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

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

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

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

The trace of U * x * U⁻¹ is the trace of x.

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 : ↥(unitaryGroup n 𝕜)), P ((innerAut U) x)) ↔ ∃ (U : ↥(unitaryGroup n 𝕜)), P ((innerAut U⁻¹) x)

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

Function.Injective ⇑(innerAut U)

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

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

A matrix is Hermitian iff its image under a unitary inner automorphism is Hermitian.

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

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

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

(↑U).conjTranspose = ↑U⁻¹

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

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

A unitary inner automorphism preserves positive semidefinite matrices.

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

((innerAut U) a).PosSemidef

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

((Matrix.innerAut U) a).PosSemidef

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

IsUnit ((innerAut U) x) ↔ IsUnit x

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

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

A unitary inner automorphism preserves positive definite matrices.

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

((innerAut U) a).PosDef

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

((Matrix.innerAut U) a).PosDef

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

Every star-algebra equivalence of Mₙ is implemented by a unitary conjugation.

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

↥(Matrix.unitaryGroup n 𝕜)

A unitary matrix implementing a star-algebra equivalence of full matrix algebras.

Equations

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

Instances For

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.ofMatrixUnitary = f

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

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

Spectral theorem in Monlib's inner-automorphism notation.

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

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

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

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

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

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

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

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

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

Matrix.toEuclideanLin 1 = 1

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

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

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

(innerAutStarAlg U).toAlgEquiv.toLinearMap = innerAut U

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(↑U).conj ∈ unitaryGroup n 𝕜

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

↥(unitaryGroup n 𝕜)

Entrywise conjugate of a unitary matrix as a unitary.

Equations

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

Instances For

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

↑(conj U) = (↑U).conj

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

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

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

↑U * star ↑U = 1

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

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

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

↥(unitaryGroup (n × p) 𝕜)

The Kronecker product of two unitary matrices as a unitary matrix.

Equations

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

Instances For

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

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

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

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