Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/Adapters.lean
Pinned GitHub source · Raw UTF-8 source
Back to Lifting a corner involution to an ambient CAR unitary · Back to Cross-representation state approximation with a protected finite set · Back to Exact vector transport along an almost central unitary path · Back to Approximating another vector state along a unitary path
1import MathlibAnnex.Analysis.CStarAlgebra.Cyclic2import MathlibAnnex.Analysis.CStarAlgebra.Representation.NonUnital3import MathlibAnnex.Analysis.CStarAlgebra.Representation45/-!6# Adapters between the representation interfaces78The project inherited two representation APIs. This file proves their exact9relationship, including the nonzero condition deliberately present in10`Representation.IsIrreducible` and absent from `StarAlgHom.IsIrreducible`.11-/1213set_option autoImplicit false1415namespace MathlibAnnex.Analysis.CStarAlgebra1617universe u v w1819variable {A : Type u} [CStarAlgebra A]20variable {H : Type v} {K : Type w}21variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]22variable [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]2324namespace Representation2526/-- The two inherited unitary-equivalence predicates are definitionally the27same mathematical statement. -/28theorem unitaryEquivalent_iff_starAlgHom29 (pi : Representation A H) (rho : Representation A K) :30 pi.UnitaryEquivalent rho ↔ StarAlgHom.UnitaryEquivalent pi rho :=31 Iff.rfl3233/-- A nonzero represented operator forces the Hilbert space to be nontrivial. -/34theorem nontrivial_of_isNonzero (pi : Representation A H) (hpi : pi.IsNonzero) :35 Nontrivial H := by36 rw [← not_subsingleton_iff_nontrivial]37 intro hsub38 obtain ⟨a, ha⟩ := hpi39 exact ha (Subsingleton.elim (pi a) 0)4041/-- The reducing predicates agree once the separate closedness field is made42explicit. -/43theorem reduces_iff_closed_and_isReducing (pi : Representation A H)44 (L : Submodule ℂ H) :45 pi.Reduces L ↔ IsClosed (L : Set H) ∧ StarAlgHom.IsReducing pi L := by46 constructor47 · intro h48 refine ⟨h.1, fun a ↦ ⟨?_, ?_⟩⟩49 · intro x hx50 exact (h.2 a x hx).151 · intro x hx52 exact (h.2 a x hx).253 · rintro ⟨hclosed, hreduces⟩54 refine ⟨hclosed, ?_⟩55 intro a x hx56 exact ⟨(hreduces a).1 hx, (hreduces a).2 hx⟩5758/-- Nonzero irreducibility implies the closed-reducing-subspace predicate used59by the Schur and cyclic-transport modules. -/60theorem isIrreducible_starAlgHom (pi : Representation A H)61 (hirr : pi.IsIrreducible) : StarAlgHom.IsIrreducible pi := by62 intro L hclosed hreduces63 exact hirr.2 L ((reduces_iff_closed_and_isReducing pi L).2 ⟨hclosed, hreduces⟩)6465/-- On a nontrivial Hilbert space, the closed-reducing-subspace predicate and66the project's explicitly nonzero irreducibility predicate are equivalent. -/67theorem isIrreducible_iff_starAlgHom [Nontrivial H]68 (pi : Representation A H) :69 pi.IsIrreducible ↔ StarAlgHom.IsIrreducible pi := by70 constructor71 · exact isIrreducible_starAlgHom pi72 · intro hirr73 refine ⟨pi.isNonzero_of_nontrivial, ?_⟩74 intro L hreduces75 exact hirr L hreduces.176 ((reduces_iff_closed_and_isReducing pi L).1 hreduces).27778/-- Every nonzero vector has dense represented orbit in the explicitly79nonzero irreducible interface. This is the concrete bridge between the two80inherited cyclic-subspace definitions. -/81theorem denseRange_orbitMap_of_isIrreducible (pi : Representation A H)82 (hirr : pi.IsIrreducible) {xi : H} (hxi : xi ≠ 0) :83 DenseRange (StarAlgHom.orbitMap pi xi) := by84 have htop : StarAlgHom.cyclicSubspace pi xi = ⊤ :=85 StarAlgHom.cyclicSubspace_eq_top pi (isIrreducible_starAlgHom pi hirr) hxi86 have hsets := congrArg (fun L : Submodule ℂ H ↦ (L : Set H)) htop87 rw [denseRange_iff_closure_range]88 simpa [StarAlgHom.cyclicSubspace, StarAlgHom.orbitMap,89 Submodule.topologicalClosure_coe, LinearMap.coe_range] using hsets9091end Representation9293end MathlibAnnex.Analysis.CStarAlgebra