MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_rankOne_map

Raw UTF-8 source

theorem exists_nonzero_projection_rankOne_map [Nontrivial A]
    [PartialOrder A] [StarOrderedRing A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    ∃ p : A, IsStarProjection p ∧ p ≠ 0 ∧
      (∃ e : H, ‖e‖ = 1 ∧ pi p = InnerProductSpace.rankOne ℂ e e) ∧
      IsCompactOperator (pi p)

1 import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.MinimalProjection
2 import MathlibAnnex.Analysis.CStarAlgebra.Representation.RankOneProjection
3 
4 /-!
5 # Rank-one images of non-unital minimal projections
6 -/
7 
8 set_option autoImplicit false
9 
10 namespace MathlibAnnex.Analysis.CStarAlgebra
11 
12 universe u v
13 
14 variable {A : Type u} [NonUnitalCStarAlgebra A]
15 variable {H : Type v}
16 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
17 
18 namespace NonUnitalCStarRepresentation
19 
20 /-- A scalar corner in a non-unital algebra remains a scalar corner after
21 passing to the minimal unitization. -/
22 theorem 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) := by
27   intro z
28   induction z using Unitization.ind with
29   | inl_add_inr c a =>
30       obtain ⟨d, hd⟩ := hcorner a
31       refine ⟨c + d, ?_⟩
32       calc
33         (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) := by
38           rw [mul_add, add_mul, Unitization.inr_mul_inl]
39           simp only [← Unitization.inr_mul]
40         _ = ((c • p + d • p : A) : Unitization ℂ A) := by
41           rw [smul_mul_assoc, hp.isIdempotentElem.eq, hd]
42           exact (Unitization.inr_add ℂ (c • p) (d • p)).symm
43         _ = (((c + d) • p : A) : Unitization ℂ A) := by rw [add_smul]
44         _ = (c + d) • (p : Unitization ℂ A) := Unitization.inr_smul ℂ (c + d) p
45 
46 /-- A nonzero scalar corner is represented by a rank-one projection in an
47 irreducible non-unital representation. -/
48 theorem exists_unitVector_map_eq_rankOne_of_scalar_corner
49     (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 := by
54   have hirrU := isIrreducible_unitization pi hirr
55   have hpU : IsStarProjection (p : Unitization ℂ A) := hp.inr
56   have hpmapU : pi.unitization (p : Unitization ℂ A) ≠ 0 := by
57     simpa using hpmap
58   obtain ⟨e, he, hmap⟩ :=
59     Representation.exists_unitVector_map_eq_rankOne_of_scalar_corner
60       pi.unitization hirrU hpU hpmapU
61         (scalar_corner_unitization hp hcorner)
62   exact ⟨e, he, by simpa using hmap⟩
63 
64 /-- A nonzero scalar corner has compact image in an irreducible non-unital
65 representation. -/
66 theorem isCompactOperator_map_of_scalar_corner
67     (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) := by
71   obtain ⟨e, _he, hmap⟩ :=
72     exists_unitVector_map_eq_rankOne_of_scalar_corner pi hirr hp hpmap hcorner
73   rw [hmap]
74   exact isCompactOperator_rankOne e e
75 
76 /-- A separable singleton model contains a nonzero minimal projection whose
77 represented image is rank one and compact. -/
78 theorem 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) := by
86   obtain ⟨p, hp, hpne, hcorner⟩ :=
87     exists_nonzero_projection_scalar_corner pi hsingle
88   have hpinj := injective_of_singleton pi hsingle
89   have hpmap : pi p ≠ 0 := by
90     intro hzero
91     apply hpne
92     apply hpinj
93     simpa using hzero
94   obtain ⟨e, he, hmap⟩ :=
95     exists_unitVector_map_eq_rankOne_of_scalar_corner
96       pi hsingle.1 hp hpmap hcorner
97   refine ⟨p, hp, hpne, ⟨e, he, hmap⟩, ?_⟩
98   rw [hmap]
99   exact isCompactOperator_rankOne e e
100 
101 end NonUnitalCStarRepresentation
102 
103 end MathlibAnnex.Analysis.CStarAlgebra