Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.Analysis.CStarAlgebra.Representation.denseRange_orbitMap_of_isIrreducible
MathlibAnnex/Analysis/CStarAlgebra/Representation/Adapters.lean · lines 81–89
1import MathlibAnnex.Analysis.CStarAlgebra.Cyclic 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.NonUnital 3import MathlibAnnex.Analysis.CStarAlgebra.Representation 4 5/-! 6# Adapters between the representation interfaces 7 8The project inherited two representation APIs. This file proves their exact 9relationship, including the nonzero condition deliberately present in 10`Representation.IsIrreducible` and absent from `StarAlgHom.IsIrreducible`. 11-/ 12 13set_option autoImplicit false 14 15namespace MathlibAnnex.Analysis.CStarAlgebra 16 17universe u v w 18 19variable {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] 23 24namespace Representation 25 26/-- The two inherited unitary-equivalence predicates are definitionally the 27same mathematical statement. -/ 28theorem unitaryEquivalent_iff_starAlgHom 29 (pi : Representation A H) (rho : Representation A K) : 30 pi.UnitaryEquivalent rho ↔ StarAlgHom.UnitaryEquivalent pi rho := 31 Iff.rfl 32 33/-- 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 := by 36 rw [← not_subsingleton_iff_nontrivial] 37 intro hsub 38 obtain ⟨a, ha⟩ := hpi 39 exact ha (Subsingleton.elim (pi a) 0) 40 41/-- The reducing predicates agree once the separate closedness field is made 42explicit. -/ 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 := by 46 constructor 47 · intro h 48 refine ⟨h.1, fun a ↦ ⟨?_, ?_⟩⟩ 49 · intro x hx 50 exact (h.2 a x hx).1 51 · intro x hx 52 exact (h.2 a x hx).2 53 · rintro ⟨hclosed, hreduces⟩ 54 refine ⟨hclosed, ?_⟩ 55 intro a x hx 56 exact ⟨(hreduces a).1 hx, (hreduces a).2 hx⟩ 57 58/-- Nonzero irreducibility implies the closed-reducing-subspace predicate used 59by the Schur and cyclic-transport modules. -/ 60theorem isIrreducible_starAlgHom (pi : Representation A H) 61 (hirr : pi.IsIrreducible) : StarAlgHom.IsIrreducible pi := by 62 intro L hclosed hreduces 63 exact hirr.2 L ((reduces_iff_closed_and_isReducing pi L).2 ⟨hclosed, hreduces⟩) 64 65/-- On a nontrivial Hilbert space, the closed-reducing-subspace predicate and 66the 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 := by 70 constructor 71 · exact isIrreducible_starAlgHom pi 72 · intro hirr 73 refine ⟨pi.isNonzero_of_nontrivial, ?_⟩ 74 intro L hreduces 75 exact hirr L hreduces.1 76 ((reduces_iff_closed_and_isReducing pi L).1 hreduces).2 77 78/-- Every nonzero vector has dense represented orbit in the explicitly 79nonzero irreducible interface. This is the concrete bridge between the two 80inherited 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) := by 84 have htop : StarAlgHom.cyclicSubspace pi xi = ⊤ := 85 StarAlgHom.cyclicSubspace_eq_top pi (isIrreducible_starAlgHom pi hirr) hxi 86 have hsets := congrArg (fun L : Submodule ℂ H ↦ (L : Set H)) htop 87 rw [denseRange_iff_closure_range] 88 simpa [StarAlgHom.cyclicSubspace, StarAlgHom.orbitMap, 89 Submodule.topologicalClosure_coe, LinearMap.coe_range] using hsets 90 91end Representation 92 93end MathlibAnnex.Analysis.CStarAlgebra