Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/Basic.lean, lines 19–47.
Back to Purifying a vector state on a finite CAR stage · Back to Lifting a corner involution to an ambient CAR unitary · Back to Exact vector transport along an almost central unitary path · Back to Approximating another vector state along a unitary path · Back to Cross-representation state approximation with a protected finite set · Back to Realizing a finite Gram matrix in a represented CAR corner · Back to An irreducible CAR representation has no nonzero compact image
1import Mathlib.Analysis.InnerProductSpace.Adjoint 2 3/-! 4Ordinary Hilbert-space representations and unitary equivalence. The target 5Hilbert space and its universe remain arbitrary. Irreducibility explicitly 6includes nonzeroness and quantifies over closed reducing subspaces. 7-/ 8 9set_option autoImplicit false 10 11namespace MathlibAnnex.Analysis.CStarAlgebra 12 13universe u v w z 14 15variable {A : Type u} 16variable [Semiring A] [Algebra ℂ A] [Star A] 17 18/-- A unital complex star representation on a Hilbert space. -/ 19abbrev Representation (A : Type u) [Semiring A] [Algebra ℂ A] [Star A] 20 (H : Type v) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] := 21 A →⋆ₐ[ℂ] (H →L[ℂ] H) 22 23section Reducing 24 25variable {H : Type v} 26variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 27 28/-- A representation is nonzero if some represented element is nonzero. -/ 29def Representation.IsNonzero (pi : Representation A H) : Prop := 30 ∃ a : A, pi a ≠ 0 31 32/-- A unital representation on a nontrivial Hilbert space is nonzero. -/ 33theorem Representation.isNonzero_of_nontrivial [Nontrivial H] 34 (pi : Representation A H) : pi.IsNonzero := by 35 refine ⟨1, ?_⟩ 36 simpa using (one_ne_zero : (1 : H →L[ℂ] H) ≠ 0) 37 38/-- A closed subspace invariant under the representation and all adjoints. -/ 39def Representation.Reduces (pi : Representation A H) (K : Submodule ℂ H) : Prop := 40 IsClosed (K : Set H) ∧ 41 ∀ (a : A) (x : H), x ∈ K → 42 pi a x ∈ K ∧ ContinuousLinearMap.adjoint (pi a) x ∈ K 43 44/-- Irreducibility in the closed-reducing-subspace sense, with nonzero action. -/ 45def Representation.IsIrreducible (pi : Representation A H) : Prop := 46 pi.IsNonzero ∧ ∀ K : Submodule ℂ H, pi.Reduces K → K = ⊥ ∨ K = ⊤ 47 48end Reducing 49 50section Equivalence 51 52variable {H : Type v} {K : Type w} {L : Type z} 53variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 54variable [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 55variable [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L] 56 57/-- Unitary equivalence of representations, including the full intertwining law. -/ 58def Representation.UnitaryEquivalent (pi : Representation A H) 59 (rho : Representation A K) : Prop := 60 ∃ U : H ≃ₗᵢ[ℂ] K, ∀ (a : A) (x : H), U (pi a x) = rho a (U x) 61 62theorem Representation.unitaryEquivalent_refl (pi : Representation A H) : 63 pi.UnitaryEquivalent pi := by 64 refine ⟨LinearIsometryEquiv.refl ℂ H, ?_⟩ 65 simp 66 67theorem Representation.unitaryEquivalent_symm {pi : Representation A H} 68 {rho : Representation A K} (h : pi.UnitaryEquivalent rho) : 69 rho.UnitaryEquivalent pi := by 70 obtain ⟨U, hU⟩ := h 71 refine ⟨U.symm, fun a y ↦ ?_⟩ 72 have h' := congrArg U.symm (hU a (U.symm y)) 73 simpa using h'.symm 74 75theorem Representation.unitaryEquivalent_trans {pi : Representation A H} 76 {rho : Representation A K} {sigma : Representation A L} 77 (hpr : pi.UnitaryEquivalent rho) (hrs : rho.UnitaryEquivalent sigma) : 78 pi.UnitaryEquivalent sigma := by 79 obtain ⟨U, hU⟩ := hpr 80 obtain ⟨V, hV⟩ := hrs 81 refine ⟨U.trans V, fun a x ↦ ?_⟩ 82 simp only [LinearIsometryEquiv.trans_apply] 83 rw [hU, hV] 84 85end Equivalence 86 87section UniqueModel 88 89variable {H : Type v} 90variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 91 92/-- 93A displayed faithful irreducible representation that captures every nonzero 94irreducible representation, with no restriction on the target Hilbert space or 95its universe. 96-/ 97def Representation.IsUniqueIrreducibleModel (pi : Representation A H) : Prop := 98 Function.Injective pi ∧ pi.IsIrreducible ∧ 99 ∀ (K : Type w) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 100 (rho : Representation A K), rho.IsIrreducible → pi.UnitaryEquivalent rho 101 102end UniqueModel 103 104end MathlibAnnex.Analysis.CStarAlgebra