Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/FiniteDimension.lean
Pinned GitHub source · Raw UTF-8 source
Back to Finite-dimensional algebra in the unital singleton case
1import MathlibAnnex.Analysis.CStarAlgebra.CompactPreimage2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Faithful3import MathlibAnnex.Analysis.CStarAlgebra.Representation.RankOneProjection45/-!6# Finite dimension forced by a separable singleton irreducible model7-/89set_option autoImplicit false1011open Set12open scoped ComplexOrder1314namespace MathlibAnnex.Analysis.CStarAlgebra1516universe u v1718variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]19variable {H : Type v}20variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2122namespace Representation2324/-- The Hilbert space of a separable singleton irreducible model of a25nonzero unital C-star algebra is finite-dimensional. -/26theorem finiteDimensional_space_of_singleton [Nontrivial A]27 [TopologicalSpace.SeparableSpace H]28 (pi : Representation A H)29 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :30 FiniteDimensional ℂ H := by31 have hinj : Function.Injective pi := injective_of_singleton pi hsingle32 have hsimple : IsSimpleCStarAlgebra A :=33 isSimpleCStarAlgebra_of_singleton_of_injective pi hsingle hinj34 obtain ⟨p, hp, hpne, hcorner⟩ :=35 exists_nonzero_projection_scalar_corner pi hsingle36 have hpmap : pi p ≠ 0 := by37 intro hzero38 apply hpne39 apply hinj40 simpa using hzero41 have hpcompact : IsCompactOperator (pi p) :=42 isCompactOperator_map_of_scalar_corner pi hsingle.1 hp hpmap hcorner43 let piNU : A →⋆ₙₐ H →L[ℂ] H := pi.toNonUnitalStarAlgHom44 let I : TwoSidedIdeal A := MathlibAnnex.CStarAlgebra.compactPreimageIdeal piNU45 have hpI : p ∈ I :=46 (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal piNU p).2 hpcompact47 have hIne : I ≠ ⊥ := by48 intro hbot49 have hpzero : p = 0 := by50 rw [hbot] at hpI51 simpa using hpI52 exact hpne hpzero53 have hItop : I = ⊤ :=54 (hsimple.2 I55 (MathlibAnnex.CStarAlgebra.isClosed_compactPreimageIdeal piNU)).resolve_left hIne56 have honeI : (1 : A) ∈ I := by57 rw [hItop]58 trivial59 have honeCompact : IsCompactOperator (pi (1 : A)) :=60 (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal piNU 1).1 honeI61 have hcompactOne :62 IsCompactOperator ((1 : H →L[ℂ] H) : H → H) := by63 simpa only [map_one, one_apply_eq_self] using honeCompact64 apply FiniteDimensional.of_isCompactOperator_id65 change IsCompactOperator (fun x : H => x)66 exact hcompactOne6768/-- The algebra itself is finite-dimensional once its singleton model is69faithful and its separable representation space is finite-dimensional. -/70theorem finiteDimensional_algebra_of_singleton [Nontrivial A]71 [TopologicalSpace.SeparableSpace H]72 (pi : Representation A H)73 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :74 FiniteDimensional ℂ A := by75 letI : FiniteDimensional ℂ H :=76 finiteDimensional_space_of_singleton pi hsingle77 letI : FiniteDimensional ℂ (H →L[ℂ] H) :=78 ContinuousLinearMap.finiteDimensional79 exact FiniteDimensional.of_injective80 (LinearMapClass.linearMap pi) (injective_of_singleton pi hsingle)8182end Representation8384end MathlibAnnex.Analysis.CStarAlgebra