MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/CoefficientFamily.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.CoefficientComponents78/-!9# The coefficient-kernel family of one irreducible representation1011The nonzero-vector and unit-vector descriptions agree as actual GSS subsets.12The family lies inside one of the received finite-chain components, and its13kernel intersection is the kernel of the representation. The reverse14component inclusion is deliberately not asserted here: it needs the still15separate inequivalent-pair closedness argument of Paper 5.8.16-/1718set_option autoImplicit false19noncomputable section20open Set21open scoped CStarAlgebra ComplexOrder2223namespace MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation2425universe u v26variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]27variable [PartialOrder A] [StarOrderedRing A]28variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2930private def coefficientFamilyContinuousMap (pi : NonUnitalCStarRepresentation A H) :31    A →L[ℂ] (H →L[ℂ] H) :=32  LinearMap.mkContinuous33    { toFun := pi, map_add' := map_add pi, map_smul' := map_smul pi }34    1 (fun a => by35      change ‖pi a‖ ≤ 1 * ‖a‖36      simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le pi a)3738/-- The actual GSS kernel points represented by one nonzero irreducible representation. -/39def matrixCoefficientKernelFamily (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) :40    Set (NormedSpace.GeometricStructureSpace ℂ A) :=41  {I | ∃ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), matrixCoefficientKernel pi hpi x y hx hy = I}4243/-- Unit vectors give exactly the same family; normalization does not add labels. -/44theorem mem_matrixCoefficientKernelFamily_iff_exists_unit_vectors45    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)46    (I : NormedSpace.GeometricStructureSpace ℂ A) :47    I ∈ matrixCoefficientKernelFamily pi hpi ↔48      ∃ x y : H, ‖x‖ = 1 ∧ ‖y‖ = 1 ∧ ((matrixCoefficient pi x y).ker : Set A) = I.val := by49  constructor50  · rintro ⟨x, y, hx, hy, hI⟩51    obtain ⟨v, w, hv, hw, hker⟩ := exists_unit_vectors_ker_matrixCoefficient_eq pi x y hx hy52    refine ⟨v, w, hv, hw, ?_⟩53    exact (congrArg (fun P : Submodule ℂ A => (P : Set A)) hker).trans54      (congrArg Subtype.val hI)55  · rintro ⟨x, y, hx, hy, hI⟩56    have hx0 : x ≠ 0 := norm_ne_zero_iff.mp (by rw [hx]; exact one_ne_zero)57    have hy0 : y ≠ 0 := norm_ne_zero_iff.mp (by rw [hy]; exact one_ne_zero)58    exact ⟨x, y, hx0, hy0, Subtype.ext hI⟩5960/-- The family is contained in the actual component of any one of its points. -/61theorem matrixCoefficientKernelFamily_subset_component62    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)63    (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) :64    matrixCoefficientKernelFamily pi hpi ⊆65      (NormedSpace.geometricStructureClosure ℂ A).component66        (matrixCoefficientKernel pi hpi x y hx hy) := by67  rintro I ⟨z, w, hz, hw, rfl⟩68  exact related_matrixCoefficientKernel pi hpi x y z w hx hy hz hw6970/-- Intersection of the coefficient-kernel FAMILY is precisely ker(pi).71This does not replace the family by an entire component without proof. -/72theorem setOf_forall_mem_matrixCoefficientKernelFamily_eq_ker73    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) :74    {a : A | ∀ I : NormedSpace.GeometricStructureSpace ℂ A,75      I ∈ matrixCoefficientKernelFamily pi hpi → a ∈ I.val} =76        ((coefficientFamilyContinuousMap pi).ker : Set A) := by77  ext a78  constructor79  · intro ha80    change pi a = 081    ext x82    by_cases hx : x = 083    · simp [hx]84    by_contra hax85    have hx0 : pi a x ≠ 0 := by simpa only [ContinuousLinearMap.zero_apply] using hax86    let I := matrixCoefficientKernel pi hpi x (pi a x) hx hx087    have hIa : a ∈ I.val := ha I ⟨x, pi a x, hx, hx0, rfl⟩88    have hinner : inner ℂ (pi a x) (pi a x) = 0 := hIa89    exact hx0 (inner_self_eq_zero.mp hinner)90  · intro ha91    change pi a = 0 at ha92    rintro I ⟨x, y, hx, hy, rfl⟩93    change inner ℂ y (pi a x) = 094    simp only [ha, ContinuousLinearMap.zero_apply, inner_zero_right]9596end MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation