Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/NonUnital.lean
Pinned GitHub source · Raw UTF-8 source
Back to Singleton condition tested against all irreducible representations
1import MathlibAnnex.Analysis.CStarAlgebra.Representation.Basic23/-!4Nonunital representation interface and the unitality bridge for nonzero5irreducible representations of unital star algebras.6-/78set_option autoImplicit false910namespace MathlibAnnex.Analysis.CStarAlgebra1112universe u v1314variable {A : Type u} [Semiring A] [Algebra ℂ A] [StarRing A]15variable {H : Type v}16variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]1718/-- A possibly nonunital complex star representation. -/19abbrev NonUnitalRepresentation := A →⋆ₙₐ[ℂ] (H →L[ℂ] H)2021namespace NonUnitalRepresentation2223def IsNonzero (pi : NonUnitalRepresentation (A := A) (H := H)) : Prop :=24 ∃ a : A, pi a ≠ 02526def 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 ∈ K3132def IsIrreducible (pi : NonUnitalRepresentation (A := A) (H := H)) : Prop :=33 pi.IsNonzero ∧ ∀ K : Submodule ℂ H, pi.Reduces K → K = ⊥ ∨ K = ⊤3435theorem one_idempotent (pi : NonUnitalRepresentation (A := A) (H := H)) :36 IsIdempotentElem (pi 1) := by37 rw [IsIdempotentElem, ← map_mul]38 simp3940/-- The range of `pi 1` is a closed reducing subspace, even before unitality41has been established. -/42theorem reduces_range_one (pi : NonUnitalRepresentation (A := A) (H := H)) :43 pi.Reduces (pi 1).range := by44 have hp := one_idempotent pi45 refine ⟨ContinuousLinearMap.IsIdempotentElem.isClosed_range hp, ?_⟩46 intro a x hx47 have hfix : pi 1 x = x :=48 LinearMap.IsIdempotentElem.mem_range_iff49 (ContinuousLinearMap.IsIdempotentElem.toLinearMap hp) |>.mp hx50 have hmap (b : A) : pi b x ∈ (pi 1).range := by51 apply LinearMap.IsIdempotentElem.mem_range_iff52 (ContinuousLinearMap.IsIdempotentElem.toLinearMap hp) |>.mpr53 calc54 pi 1 (pi b x) = (pi 1 * pi b) x := rfl55 _ = pi (1 * b) x := by rw [map_mul]56 _ = pi b x := by simp57 refine ⟨hmap a, ?_⟩58 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star pi]59 exact hmap (star a)6061theorem map_one_ne_zero_of_isNonzero62 (pi : NonUnitalRepresentation (A := A) (H := H)) (hpi : pi.IsNonzero) :63 pi 1 ≠ 0 := by64 obtain ⟨a, ha⟩ := hpi65 intro hzero66 apply ha67 calc68 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]7172/-- A nonzero irreducible representation of a unital algebra sends the unit73to the identity operator. Nontriviality of `H` alone is not substituted for74nonzeroness of the representation. -/75theorem map_one_eq_one_of_isIrreducible76 (pi : NonUnitalRepresentation (A := A) (H := H))77 (hirr : pi.IsIrreducible) : pi 1 = 1 := by78 have hp := one_idempotent pi79 have hrange_ne : (pi 1).range ≠ (⊥ : Submodule ℂ H) := by80 intro hrange81 apply map_one_ne_zero_of_isNonzero pi hirr.182 apply ContinuousLinearMap.ext83 intro x84 have hx : pi 1 x ∈ (pi 1).range := ⟨x, rfl⟩85 rw [hrange, Submodule.mem_bot] at hx86 simpa using hx87 have hrange : (pi 1).range = (⊤ : Submodule ℂ H) :=88 (hirr.2 (pi 1).range (reduces_range_one pi)).resolve_left hrange_ne89 apply ContinuousLinearMap.ext90 intro x91 have hx : x ∈ (pi 1).range := by rw [hrange]; trivial92 have hfix := LinearMap.IsIdempotentElem.mem_range_iff93 (ContinuousLinearMap.IsIdempotentElem.toLinearMap hp) |>.mp hx94 simpa using hfix9596/-- Bundle a nonzero irreducible nonunital representation as a unital star97representation after proving the unit equation. -/98noncomputable def toUnital (pi : NonUnitalRepresentation (A := A) (H := H))99 (hirr : pi.IsIrreducible) : A →⋆ₐ[ℂ] (H →L[ℂ] H) where100 toFun := pi101 map_one' := map_one_eq_one_of_isIrreducible pi hirr102 map_mul' := map_mul pi103 map_zero' := map_zero pi104 map_add' := map_add pi105 commutes' c := by106 calc107 pi (algebraMap ℂ A c) = pi (c • (1 : A)) := by rw [Algebra.smul_def, mul_one]108 _ = c • pi 1 := map_smul pi c 1109 _ = algebraMap ℂ (H →L[ℂ] H) c := by110 rw [map_one_eq_one_of_isIrreducible pi hirr, Algebra.smul_def, mul_one]111 map_star' := map_star pi112113@[simp]114theorem toUnital_apply (pi : NonUnitalRepresentation (A := A) (H := H))115 (hirr : pi.IsIrreducible) (a : A) : pi.toUnital hirr a = pi a :=116 rfl117118/-- Passing a nonzero irreducible possibly nonunital representation through119`toUnital` preserves irreducibility. The represented operators, their120adjoints, and hence all reducing subspaces are definitionally unchanged. -/121theorem isIrreducible_toUnital122 (pi : NonUnitalRepresentation (A := A) (H := H))123 (hirr : pi.IsIrreducible) :124 Representation.IsIrreducible (pi.toUnital hirr) := by125 refine ⟨hirr.1, ?_⟩126 intro K hK127 exact hirr.2 K hK128129end NonUnitalRepresentation130131namespace Representation132133universe w134135/-- Exact capture predicate for the ordinary nonzero, possibly nonunital136target quantifier. Universe `w` is left polymorphic rather than restricting137the target Hilbert dimension. -/138def IsUniqueIrreducibleModelAmongNonUnital139 (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)144145/-- A universal model for unital irreducible representations is already a146universal model for ordinary possibly nonunital nonzero irreducible147representations: irreducibility forces the latter to preserve the unit. -/148theorem IsUniqueIrreducibleModel.isUniqueIrreducibleModelAmongNonUnital149 {pi : Representation A H}150 (hpi : Representation.IsUniqueIrreducibleModel.{u, v, w} pi) :151 Representation.IsUniqueIrreducibleModelAmongNonUnital.{u, v, w} pi := by152 refine ⟨hpi.1, hpi.2.1, ?_⟩153 intro K _ _ _ rho hrho154 exact hpi.2.2 K (rho.toUnital hrho)155 (NonUnitalRepresentation.isIrreducible_toUnital rho hrho)156157end Representation158159end MathlibAnnex.Analysis.CStarAlgebra