Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/Basic.lean
Pinned GitHub source · Raw UTF-8 source
Back to An irreducible CAR representation has no nonzero compact image · Back to Lifting a corner involution to an ambient CAR unitary · Back to Realizing a finite Gram matrix in a represented CAR corner · Back to Cross-representation state approximation with a protected finite set · Back to Exact vector transport along an almost central unitary path · Back to Purifying a vector state on a finite CAR stage · Back to Approximating another vector state along a unitary path
1import Mathlib.Analysis.InnerProductSpace.Adjoint23/-!4Ordinary Hilbert-space representations and unitary equivalence. The target5Hilbert space and its universe remain arbitrary. Irreducibility explicitly6includes nonzeroness and quantifies over closed reducing subspaces.7-/89set_option autoImplicit false1011namespace MathlibAnnex.Analysis.CStarAlgebra1213universe u v w z1415variable {A : Type u}16variable [Semiring A] [Algebra ℂ A] [Star A]1718/-- 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)2223section Reducing2425variable {H : Type v}26variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2728/-- A representation is nonzero if some represented element is nonzero. -/29def Representation.IsNonzero (pi : Representation A H) : Prop :=30 ∃ a : A, pi a ≠ 03132/-- A unital representation on a nontrivial Hilbert space is nonzero. -/33theorem Representation.isNonzero_of_nontrivial [Nontrivial H]34 (pi : Representation A H) : pi.IsNonzero := by35 refine ⟨1, ?_⟩36 simpa using (one_ne_zero : (1 : H →L[ℂ] H) ≠ 0)3738/-- 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 ∈ K4344/-- 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 = ⊤4748end Reducing4950section Equivalence5152variable {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]5657/-- 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)6162theorem Representation.unitaryEquivalent_refl (pi : Representation A H) :63 pi.UnitaryEquivalent pi := by64 refine ⟨LinearIsometryEquiv.refl ℂ H, ?_⟩65 simp6667theorem Representation.unitaryEquivalent_symm {pi : Representation A H}68 {rho : Representation A K} (h : pi.UnitaryEquivalent rho) :69 rho.UnitaryEquivalent pi := by70 obtain ⟨U, hU⟩ := h71 refine ⟨U.symm, fun a y ↦ ?_⟩72 have h' := congrArg U.symm (hU a (U.symm y))73 simpa using h'.symm7475theorem 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 := by79 obtain ⟨U, hU⟩ := hpr80 obtain ⟨V, hV⟩ := hrs81 refine ⟨U.trans V, fun a x ↦ ?_⟩82 simp only [LinearIsometryEquiv.trans_apply]83 rw [hU, hV]8485end Equivalence8687section UniqueModel8889variable {H : Type v}90variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]9192/--93A displayed faithful irreducible representation that captures every nonzero94irreducible representation, with no restriction on the target Hilbert space or95its 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 rho101102end UniqueModel103104end MathlibAnnex.Analysis.CStarAlgebra