Exact source: MathlibAnnex/Analysis/CStarAlgebra/NonUnital/RankOneProjection.lean
Pinned GitHub source · Raw UTF-8 source
Back to A projection represented by a rank-one operator · Back to Every rank-one operator has an algebra preimage
1import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.MinimalProjection2import MathlibAnnex.Analysis.CStarAlgebra.Representation.RankOneProjection34/-!5# Rank-one images of non-unital minimal projections6-/78set_option autoImplicit false910namespace MathlibAnnex.Analysis.CStarAlgebra1112universe u v1314variable {A : Type u} [NonUnitalCStarAlgebra A]15variable {H : Type v}16variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]1718namespace NonUnitalCStarRepresentation1920/-- A scalar corner in a non-unital algebra remains a scalar corner after21passing to the minimal unitization. -/22theorem scalar_corner_unitization {p : A} (hp : IsStarProjection p)23 (hcorner : ∀ a : A, ∃ c : ℂ, p * a * p = c • p) :24 ∀ z : Unitization ℂ A, ∃ c : ℂ,25 (p : Unitization ℂ A) * z * (p : Unitization ℂ A) =26 c • (p : Unitization ℂ A) := by27 intro z28 induction z using Unitization.ind with29 | inl_add_inr c a =>30 obtain ⟨d, hd⟩ := hcorner a31 refine ⟨c + d, ?_⟩32 calc33 (p : Unitization ℂ A) *34 (Unitization.inl c + (a : Unitization ℂ A)) *35 (p : Unitization ℂ A) =36 (((c • p) * p : A) : Unitization ℂ A) +37 ((p * a * p : A) : Unitization ℂ A) := by38 rw [mul_add, add_mul, Unitization.inr_mul_inl]39 simp only [← Unitization.inr_mul]40 _ = ((c • p + d • p : A) : Unitization ℂ A) := by41 rw [smul_mul_assoc, hp.isIdempotentElem.eq, hd]42 exact (Unitization.inr_add ℂ (c • p) (d • p)).symm43 _ = (((c + d) • p : A) : Unitization ℂ A) := by rw [add_smul]44 _ = (c + d) • (p : Unitization ℂ A) := Unitization.inr_smul ℂ (c + d) p4546/-- A nonzero scalar corner is represented by a rank-one projection in an47irreducible non-unital representation. -/48theorem exists_unitVector_map_eq_rankOne_of_scalar_corner49 (pi : NonUnitalCStarRepresentation A H) (hirr : pi.IsIrreducible)50 {p : A} (hp : IsStarProjection p) (hpmap : pi p ≠ 0)51 (hcorner : ∀ a : A, ∃ c : ℂ, p * a * p = c • p) :52 ∃ e : H, ‖e‖ = 1 ∧53 pi p = InnerProductSpace.rankOne ℂ e e := by54 have hirrU := isIrreducible_unitization pi hirr55 have hpU : IsStarProjection (p : Unitization ℂ A) := hp.inr56 have hpmapU : pi.unitization (p : Unitization ℂ A) ≠ 0 := by57 simpa using hpmap58 obtain ⟨e, he, hmap⟩ :=59 Representation.exists_unitVector_map_eq_rankOne_of_scalar_corner60 pi.unitization hirrU hpU hpmapU61 (scalar_corner_unitization hp hcorner)62 exact ⟨e, he, by simpa using hmap⟩6364/-- A nonzero scalar corner has compact image in an irreducible non-unital65representation. -/66theorem isCompactOperator_map_of_scalar_corner67 (pi : NonUnitalCStarRepresentation A H) (hirr : pi.IsIrreducible)68 {p : A} (hp : IsStarProjection p) (hpmap : pi p ≠ 0)69 (hcorner : ∀ a : A, ∃ c : ℂ, p * a * p = c • p) :70 IsCompactOperator (pi p) := by71 obtain ⟨e, _he, hmap⟩ :=72 exists_unitVector_map_eq_rankOne_of_scalar_corner pi hirr hp hpmap hcorner73 rw [hmap]74 exact isCompactOperator_rankOne e e7576/-- A separable singleton model contains a nonzero minimal projection whose77represented image is rank one and compact. -/78theorem exists_nonzero_projection_rankOne_map [Nontrivial A]79 [PartialOrder A] [StarOrderedRing A]80 [TopologicalSpace.SeparableSpace H]81 (pi : NonUnitalCStarRepresentation A H)82 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :83 ∃ p : A, IsStarProjection p ∧ p ≠ 0 ∧84 (∃ e : H, ‖e‖ = 1 ∧ pi p = InnerProductSpace.rankOne ℂ e e) ∧85 IsCompactOperator (pi p) := by86 obtain ⟨p, hp, hpne, hcorner⟩ :=87 exists_nonzero_projection_scalar_corner pi hsingle88 have hpinj := injective_of_singleton pi hsingle89 have hpmap : pi p ≠ 0 := by90 intro hzero91 apply hpne92 apply hpinj93 simpa using hzero94 obtain ⟨e, he, hmap⟩ :=95 exists_unitVector_map_eq_rankOne_of_scalar_corner96 pi hsingle.1 hp hpmap hcorner97 refine ⟨p, hp, hpne, ⟨e, he, hmap⟩, ?_⟩98 rw [hmap]99 exact isCompactOperator_rankOne e e100101end NonUnitalCStarRepresentation102103end MathlibAnnex.Analysis.CStarAlgebra