Exact source: MathlibAnnex/Analysis/CStarAlgebra/NonUnital/CompactModel.lean
Pinned GitHub source · Raw UTF-8 source
Back to A singleton model is faithful and exactly compact-valued
1import MathlibAnnex.Analysis.CStarAlgebra.CompactPreimage2import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.CompactExclusion3import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.CompactRange4import MathlibAnnex.Analysis.CStarAlgebra.State.Ideal56/-!7# Compact-operator models for genuinely non-unital C-star algebras89This file assembles the non-unital Rosenberg conclusion. No unit is assumed10on the source algebra. `NonUnital.CompactExclusion` proves directly that11every represented operator is compact, while `NonUnital.CompactRange` proves12the reverse range inclusion. The older simplicity-based closure is retained13below as an independent conditional route.14-/1516set_option autoImplicit false1718namespace MathlibAnnex.Analysis.CStarAlgebra1920universe u v2122variable {A : Type u} [NonUnitalCStarAlgebra A]23 [PartialOrder A] [StarOrderedRing A]24variable {H : Type v}25variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2627namespace NonUnitalCStarRepresentation2829/-- A separable singleton irreducible representation of a nonzero possibly30non-unital complex C-star algebra is an exact model of the compact operators.31Neither simplicity nor faithfulness is assumed. -/32theorem isCompactOperatorModel_of_singleton [Nontrivial A]33 [TopologicalSpace.SeparableSpace H]34 (pi : NonUnitalCStarRepresentation A H)35 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :36 IsCompactOperatorModel pi := by37 exact ⟨injective_of_singleton pi hsingle,38 isCompactOperator_map_of_singleton pi hsingle,39 exists_preimage_of_compact_singleton pi hsingle⟩4041/-- Faithfulness and equality of the represented range with all compact42operators for a genuinely non-unital singleton model. -/43theorem faithful_and_compactOperatorModel_of_singleton [Nontrivial A]44 [TopologicalSpace.SeparableSpace H]45 (pi : NonUnitalCStarRepresentation A H)46 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :47 Function.Injective pi ∧ IsCompactOperatorModel pi :=48 ⟨injective_of_singleton pi hsingle,49 isCompactOperatorModel_of_singleton pi hsingle⟩5051/-- Closed-ideal simplicity turns the one nonzero compact image supplied by52the singleton argument into compactness of the entire represented image. -/53theorem isCompactOperator_map_of_singleton_of_isSimple [Nontrivial A]54 [TopologicalSpace.SeparableSpace H]55 (pi : NonUnitalCStarRepresentation A H)56 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)57 (hsimple : IsSimpleCStarAlgebra A) :58 ∀ a : A, IsCompactOperator (pi a) := by59 obtain ⟨p, _hp, hpne, _hrankOne, hpcompact⟩ :=60 exists_nonzero_projection_rankOne_map pi hsingle61 let I : TwoSidedIdeal A :=62 MathlibAnnex.CStarAlgebra.compactPreimageIdeal pi63 have hpI : p ∈ I :=64 (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal pi p).2 hpcompact65 have hIne : I ≠ ⊥ := by66 intro hbot67 have hpzero : p = 0 := by68 rw [hbot] at hpI69 simpa using hpI70 exact hpne hpzero71 have hItop : I = ⊤ :=72 (hsimple.2 I73 (MathlibAnnex.CStarAlgebra.isClosed_compactPreimageIdeal pi)).resolve_left hIne74 intro a75 have haI : a ∈ I := by76 rw [hItop]77 trivial78 exact (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal pi a).1 haI7980/-- Conditional closure of the genuinely non-unital compact-operator model:81the only extra input is norm-closed two-sided simplicity of `A`. -/82theorem isCompactOperatorModel_of_singleton_of_isSimple [Nontrivial A]83 [TopologicalSpace.SeparableSpace H]84 (pi : NonUnitalCStarRepresentation A H)85 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)86 (hsimple : IsSimpleCStarAlgebra A) :87 IsCompactOperatorModel pi := by88 refine ⟨injective_of_singleton pi hsingle,89 isCompactOperator_map_of_singleton_of_isSimple pi hsingle hsimple, ?_⟩90 exact exists_preimage_of_compact_singleton pi hsingle9192/-- Faithfulness and exact compact range, conditionally on the generic93non-unital simplicity bridge. -/94theorem faithful_and_compactOperatorModel_of_singleton_of_isSimple95 [Nontrivial A] [TopologicalSpace.SeparableSpace H]96 (pi : NonUnitalCStarRepresentation A H)97 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)98 (hsimple : IsSimpleCStarAlgebra A) :99 Function.Injective pi ∧ IsCompactOperatorModel pi :=100 ⟨injective_of_singleton pi hsingle,101 isCompactOperatorModel_of_singleton_of_isSimple pi hsingle hsimple⟩102103end NonUnitalCStarRepresentation104105end MathlibAnnex.Analysis.CStarAlgebra