noncomputable def sig {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (z : ℝ) : Matrix n n ℂ ≃ₐ[ℂ] Matrix n n ℂ

Equations

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

@[simp]

theorem sig_apply {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (z : ℝ) (a : Matrix n n ℂ) : (sig hφ z) a = ⋯.rpow (-z) * a * ⋯.rpow z

@[simp]

theorem sig_symm_apply {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (z : ℝ) (a : Matrix n n ℂ) : (sig hφ z).symm a = ⋯.rpow z * a * ⋯.rpow (-z)

theorem Module.Dual.IsFaithfulPosMap.sig_trans_sig {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : ℝ) (y : ℝ) : (sig hφ x).trans (sig hφ y) = sig hφ (x + y)

theorem PosDef.smul {n : Type u_1} [Fintype n] {𝕜 : Type u_2} [RCLike 𝕜] {x : Matrix n n 𝕜} (hx : x.PosDef) (α : NNRealˣ) : (↑↑↑α • x).PosDef

theorem posSemidefOne_smul_rpow {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] (α : NNReal) (r : ℝ) : ⋯.rpow r = ↑(↑α ^ r) • 1

theorem posDefOne_smul_rpow {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] (α : NNRealˣ) (r : ℝ) : ⋯.rpow r = ↑(↑↑α ^ r) • 1

theorem Module.Dual.IsFaithfulPosMap.sig_zero {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : sig hφ 0 = 1

theorem AlgEquiv.apply_eq_id {R : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring M] [Algebra R M] {f : M ≃ₐ[R] M} : (∀ (x : M), f x = x) ↔ f = 1

theorem Matrix.PosDef.rpow_neg_eq_inv_rpow {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℝ) : hQ.rpow (-r) = (hQ.rpow r)⁻¹

theorem RCLike.pos_toNNReal_units {𝕜 : Type u_2} [RCLike 𝕜] (r : 𝕜) : 0 < r ↔ ∃ (s : NNRealˣ), r = ↑↑↑s

theorem RCLike.nonneg_toNNReal {𝕜 : Type u_2} [RCLike 𝕜] (r : 𝕜) : 0 ≤ r ↔ ∃ (s : NNReal), r = ↑↑s

theorem Matrix.smulPosDef_isPosDef_iff {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] [H : Nonempty n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : 𝕜) : (r • Q).PosDef ↔ 0 < r

theorem smul_onePosDef_rpow_eq {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {α : 𝕜} (h : (α • 1).PosDef) (r : ℝ) : h.rpow r = ↑(RCLike.re α ^ r) • 1

theorem Matrix.smulPosSemidef_isPosSemidef_iff {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosSemidef) (r : 𝕜) : (r • Q).PosSemidef ↔ 0 ≤ r ∨ Q = 0

theorem smul_onePosSemidef_rpow_eq {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {α : 𝕜} (h : (α • 1).PosSemidef) (r : ℝ) : h.rpow r = ↑(RCLike.re α ^ r) • 1

theorem Matrix.smul_one_inv {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {s : NNRealˣ} : (↑↑↑s • 1)⁻¹ = ↑↑(↑s)⁻¹ • 1

theorem Matrix.PosDef.commutes_iff_rpow_commutes {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℝˣ) : (∀ (x : Matrix n n 𝕜), Commute x (hQ.rpow ↑r)) ↔ ∀ (x : Matrix n n 𝕜), Commute x Q

theorem Module.Dual.IsPosMap.isTracial_iff {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsPosMap) : φ.IsTracial ↔ ∃ (α : ℂ), φ.matrix = α • 1

theorem sig_eq_id_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (k : ℝ) : sig hφ k = 1 ↔ k = 0 ∨ φ.IsTracial

σ_k = 1 iff either k = 0 or φ is tracial

theorem Module.Dual.pi_isTracial_iff {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {φ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} : (Module.Dual.pi φ).IsTracial ↔ ∀ (i : k), (φ i).IsTracial

@[defaultInstance 1000]

noncomputable instance Matrix.isStarAlgebra {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : starAlgebra (Matrix n n ℂ)

Equations

• Matrix.isStarAlgebra = starAlgebra.mk (sig hφ) ⋯ ⋯

noncomputable instance Module.Dual.IsFaithfulPosMap.innerProductAlgebra {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : InnerProductAlgebra (Matrix n n ℂ)

Equations

• Module.Dual.IsFaithfulPosMap.innerProductAlgebra = InnerProductAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance Module.Dual.IsFaithfulPosMap.quantumSet {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : QuantumSet (Matrix n n ℂ)

Equations

• Module.Dual.IsFaithfulPosMap.quantumSet = QuantumSet.mk ⋯ 0 ⋯ ⋯ (n × n) inferInstance inferInstance hφ.orthonormalBasis

noncomputable instance PiMat.isStarAlgebra {k : Type u_2} [Fintype k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [_hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] : starAlgebra (PiMat ℂ k s)

Equations

• PiMat.isStarAlgebra = piStarAlgebra

noncomputable instance Module.Dual.pi.IsFaithfulPosMap.innerProductAlgebra {k : Type u_2} [Fintype k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [∀ (i : k), (ψ i).IsFaithfulPosMap] : InnerProductAlgebra (PiMat ℂ k s)

Equations

• Module.Dual.pi.IsFaithfulPosMap.innerProductAlgebra = piInnerProductAlgebra

noncomputable instance Module.Dual.pi.IsFaithfulPosMap.quantumSet {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] : QuantumSet (PiMat ℂ k s)

Equations

• Module.Dual.pi.IsFaithfulPosMap.quantumSet = QuantumSet.mk ⋯ 0 ⋯ ⋯ ((i : k) × s i × s i) inferInstance inferInstance (Module.Dual.pi.IsFaithfulPosMap.orthonormalBasis hψ)

theorem LinearMap.mul'_comp_mul'_adjoint_of_delta_form {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : LinearMap.mul' ℂ (Matrix n n ℂ) ∘ₗ Coalgebra.comul = φ.matrix⁻¹.trace • 1

theorem LinearMap.pi_mul'_comp_mul'_adjoint_of_delta_form {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] [∀ (i : k), Nontrivial (s i)] {δ : ℂ} {φ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hφ : ∀ (i : k), (φ i).IsFaithfulPosMap] (hφ₂ : ∀ (i : k), (φ i).matrix⁻¹.trace = δ) : LinearMap.mul' ℂ (PiMat ℂ k s) ∘ₗ Coalgebra.comul = δ • 1

theorem Qam.Nontracial.delta_pos {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : 0 < φ.matrix⁻¹.trace

theorem Pi.Qam.Nontracial.delta_ne_zero {k : Type u_2} {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] [Nonempty k] [∀ (i : k), Nontrivial (s i)] {δ : ℂ} {φ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hφ : ∀ (i : k), (φ i).IsFaithfulPosMap] (hφ₂ : ∀ (i : k), (φ i).matrix⁻¹.trace = δ) : 0 < δ

noncomputable instance Matrix.quantumSetDeltaForm {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : QuantumSetDeltaForm (Matrix n n ℂ)

Equations

• Matrix.quantumSetDeltaForm = { delta := φ.matrix⁻¹.trace, delta_pos := ⋯, mul_comp_comul_eq := ⋯ }

noncomputable instance PiMat.quantumSetDeltaForm {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] [Nonempty k] [∀ (i : k), Nontrivial (s i)] {d : ℂ} {φ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hφ : ∀ (i : k), (φ i).IsFaithfulPosMap] [hφ₂ : Fact (∀ (i : k), (φ i).matrix⁻¹.trace = d)] : QuantumSetDeltaForm (PiMat ℂ k s)

Equations

• PiMat.quantumSetDeltaForm = { delta := d, delta_pos := ⋯, mul_comp_comul_eq := ⋯ }