Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/NonUnital.lean, lines 75–96.
Back to Unitary equivalence without an initial unitality assumption
1import MathlibAnnex.Analysis.CStarAlgebra.Representation.Basic 2 3/-! 4Nonunital representation interface and the unitality bridge for nonzero 5irreducible representations of unital star algebras. 6-/ 7 8set_option autoImplicit false 9 10namespace MathlibAnnex.Analysis.CStarAlgebra 11 12universe u v 13 14variable {A : Type u} [Semiring A] [Algebra ℂ A] [StarRing A] 15variable {H : Type v} 16variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 17 18/-- A possibly nonunital complex star representation. -/ 19abbrev NonUnitalRepresentation := A →⋆ₙₐ[ℂ] (H →L[ℂ] H) 20 21namespace NonUnitalRepresentation 22 23def IsNonzero (pi : NonUnitalRepresentation (A := A) (H := H)) : Prop := 24 ∃ a : A, pi a ≠ 0 25 26def Reduces (pi : NonUnitalRepresentation (A := A) (H := H)) 27 (K : Submodule ℂ H) : Prop := 28 IsClosed (K : Set H) ∧ 29 ∀ (a : A) (x : H), x ∈ K → 30 pi a x ∈ K ∧ ContinuousLinearMap.adjoint (pi a) x ∈ K 31 32def IsIrreducible (pi : NonUnitalRepresentation (A := A) (H := H)) : Prop := 33 pi.IsNonzero ∧ ∀ K : Submodule ℂ H, pi.Reduces K → K = ⊥ ∨ K = ⊤ 34 35theorem one_idempotent (pi : NonUnitalRepresentation (A := A) (H := H)) : 36 IsIdempotentElem (pi 1) := by 37 rw [IsIdempotentElem, ← map_mul] 38 simp 39 40/-- The range of `pi 1` is a closed reducing subspace, even before unitality 41has been established. -/ 42theorem reduces_range_one (pi : NonUnitalRepresentation (A := A) (H := H)) : 43 pi.Reduces (pi 1).range := by 44 have hp := one_idempotent pi 45 refine ⟨ContinuousLinearMap.IsIdempotentElem.isClosed_range hp, ?_⟩ 46 intro a x hx 47 have hfix : pi 1 x = x := 48 LinearMap.IsIdempotentElem.mem_range_iff 49 (ContinuousLinearMap.IsIdempotentElem.toLinearMap hp) |>.mp hx 50 have hmap (b : A) : pi b x ∈ (pi 1).range := by 51 apply LinearMap.IsIdempotentElem.mem_range_iff 52 (ContinuousLinearMap.IsIdempotentElem.toLinearMap hp) |>.mpr 53 calc 54 pi 1 (pi b x) = (pi 1 * pi b) x := rfl 55 _ = pi (1 * b) x := by rw [map_mul] 56 _ = pi b x := by simp 57 refine ⟨hmap a, ?_⟩ 58 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star pi] 59 exact hmap (star a) 60 61theorem map_one_ne_zero_of_isNonzero 62 (pi : NonUnitalRepresentation (A := A) (H := H)) (hpi : pi.IsNonzero) : 63 pi 1 ≠ 0 := by 64 obtain ⟨a, ha⟩ := hpi 65 intro hzero 66 apply ha 67 calc 68 pi a = pi (1 * a) := by rw [one_mul] 69 _ = pi 1 * pi a := by rw [map_mul] 70 _ = 0 := by rw [hzero, zero_mul] 71 72/-- A nonzero irreducible representation of a unital algebra sends the unit 73to the identity operator. Nontriviality of `H` alone is not substituted for 74nonzeroness of the representation. -/ 75theorem map_one_eq_one_of_isIrreducible 76 (pi : NonUnitalRepresentation (A := A) (H := H)) 77 (hirr : pi.IsIrreducible) : pi 1 = 1 := by 78 have hp := one_idempotent pi 79 have hrange_ne : (pi 1).range ≠ (⊥ : Submodule ℂ H) := by 80 intro hrange 81 apply map_one_ne_zero_of_isNonzero pi hirr.1 82 apply ContinuousLinearMap.ext 83 intro x 84 have hx : pi 1 x ∈ (pi 1).range := ⟨x, rfl⟩ 85 rw [hrange, Submodule.mem_bot] at hx 86 simpa using hx 87 have hrange : (pi 1).range = (⊤ : Submodule ℂ H) := 88 (hirr.2 (pi 1).range (reduces_range_one pi)).resolve_left hrange_ne 89 apply ContinuousLinearMap.ext 90 intro x 91 have hx : x ∈ (pi 1).range := by rw [hrange]; trivial 92 have hfix := LinearMap.IsIdempotentElem.mem_range_iff 93 (ContinuousLinearMap.IsIdempotentElem.toLinearMap hp) |>.mp hx 94 simpa using hfix 95 96/-- Bundle a nonzero irreducible nonunital representation as a unital star 97representation after proving the unit equation. -/ 98noncomputable def toUnital (pi : NonUnitalRepresentation (A := A) (H := H)) 99 (hirr : pi.IsIrreducible) : A →⋆ₐ[ℂ] (H →L[ℂ] H) where 100 toFun := pi 101 map_one' := map_one_eq_one_of_isIrreducible pi hirr 102 map_mul' := map_mul pi 103 map_zero' := map_zero pi 104 map_add' := map_add pi 105 commutes' c := by 106 calc 107 pi (algebraMap ℂ A c) = pi (c • (1 : A)) := by rw [Algebra.smul_def, mul_one] 108 _ = c • pi 1 := map_smul pi c 1 109 _ = algebraMap ℂ (H →L[ℂ] H) c := by 110 rw [map_one_eq_one_of_isIrreducible pi hirr, Algebra.smul_def, mul_one] 111 map_star' := map_star pi 112 113@[simp] 114theorem toUnital_apply (pi : NonUnitalRepresentation (A := A) (H := H)) 115 (hirr : pi.IsIrreducible) (a : A) : pi.toUnital hirr a = pi a := 116 rfl 117 118/-- Passing a nonzero irreducible possibly nonunital representation through 119`toUnital` preserves irreducibility. The represented operators, their 120adjoints, and hence all reducing subspaces are definitionally unchanged. -/ 121theorem isIrreducible_toUnital 122 (pi : NonUnitalRepresentation (A := A) (H := H)) 123 (hirr : pi.IsIrreducible) : 124 Representation.IsIrreducible (pi.toUnital hirr) := by 125 refine ⟨hirr.1, ?_⟩ 126 intro K hK 127 exact hirr.2 K hK 128 129end NonUnitalRepresentation 130 131namespace Representation 132 133universe w 134 135/-- Exact capture predicate for the ordinary nonzero, possibly nonunital 136target quantifier. Universe `w` is left polymorphic rather than restricting 137the target Hilbert dimension. -/ 138def IsUniqueIrreducibleModelAmongNonUnital 139 (pi : Representation A H) : Prop := 140 Function.Injective pi ∧ pi.IsIrreducible ∧ 141 ∀ (K : Type w) [NormedAddCommGroup K] [InnerProductSpace ℂ K] 142 [CompleteSpace K] (rho : NonUnitalRepresentation (A := A) (H := K)), 143 ∀ hrho : rho.IsIrreducible, pi.UnitaryEquivalent (rho.toUnital hrho) 144 145/-- A universal model for unital irreducible representations is already a 146universal model for ordinary possibly nonunital nonzero irreducible 147representations: irreducibility forces the latter to preserve the unit. -/ 148theorem IsUniqueIrreducibleModel.isUniqueIrreducibleModelAmongNonUnital 149 {pi : Representation A H} 150 (hpi : Representation.IsUniqueIrreducibleModel.{u, v, w} pi) : 151 Representation.IsUniqueIrreducibleModelAmongNonUnital.{u, v, w} pi := by 152 refine ⟨hpi.1, hpi.2.1, ?_⟩ 153 intro K _ _ _ rho hrho 154 exact hpi.2.2 K (rho.toUnital hrho) 155 (NonUnitalRepresentation.isIrreducible_toUnital rho hrho) 156 157end Representation 158 159end MathlibAnnex.Analysis.CStarAlgebra