MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/ExtremeKernel.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.FacialStructure.ExtremeMaximalFace7import MathlibAnnex.Analysis.Normed.GeometricStructure.Basic89/-!10# Extreme kernels in the original geometric structure space1112The generic geometric structure family is unchanged: its points are unions13of kernels of ALL supporting functionals of maximal proper faces. The C-star14singleton theorem turns such a union into a single extreme-functional kernel,15and maximality of every extreme slice proves the reverse inclusion.1617Repeated kernels remain a single point. The parametrization by extreme18functionals is surjective, not claimed injective. These statements concern19the complex algebra, not its real self-adjoint part. Nontriviality is explicit:20for the zero algebra the existing generic family is empty, whereas the dual21ball has the extreme point zero.22-/2324set_option autoImplicit false25noncomputable section26open Set Metric27open scoped CStarAlgebra ComplexOrder2829namespace MathlibAnnex.Analysis.CStarAlgebra3031universe u32variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]33variable [PartialOrder A] [StarOrderedRing A]3435/-- The original union of all supporting kernels is exactly the kernel of the36extreme functional. Both inclusions use the proved entire-family singleton. -/37theorem supportKernelUnion_unitBallSupportFace_eq_ker38    {rho : StrongDual ℂ A}39    (hrho : rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :40    NormedSpace.supportKernelUnion ℂ (NormedSpace.unitBallSupportFace ℂ rho) =41      (rho.ker : Set A) := by42  rw [NormedSpace.supportKernelUnion_eq_preimage_zero_of_supportFunctionals_eq_singleton43    ℂ _ rho (supportFunctionals_unitBallSupportFace_eq_singleton hrho)]44  ext a45  rfl4647/-- Exact family identification with the already defined generic S(A).48No C-star-specific replacement of its definition is introduced. -/49theorem geometricStructureFamily_eq_image_ker_extremePoints_dual_closedBall :50    NormedSpace.geometricStructureFamily ℂ A =51      (fun rho : StrongDual ℂ A => (rho.ker : Set A)) ''52        (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ := by53  letI : NormedSpace ℝ A := NormedSpace.restrictScalars ℝ ℂ A54  ext I55  constructor56  · rintro ⟨F, hF, hFI⟩57    obtain ⟨rho, hrho, hFrho⟩ :=58      (isMaximalFace_iff_exists_mem_extremePoints_dual_closedBall F).mp hF59    refine ⟨rho, hrho, ?_⟩60    rw [hFrho, supportKernelUnion_unitBallSupportFace_eq_ker hrho] at hFI61    exact hFI62  · rintro ⟨rho, hrho, rfl⟩63    exact ⟨NormedSpace.unitBallSupportFace ℂ rho,64      isMaximalFace_unitBallSupportFace_of_mem_extremePoints_dual_closedBall hrho,65      supportKernelUnion_unitBallSupportFace_eq_ker hrho⟩6667/-- Membership in the original family is equivalent to being the kernel of68an extreme functional, with equality of the actual subset of A. -/69theorem mem_geometricStructureFamily_iff_exists_mem_extremePoints_dual_closedBall70    (I : Set A) : I ∈ NormedSpace.geometricStructureFamily ℂ A ↔71      ∃ rho : StrongDual ℂ A,72        rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ ∧ (rho.ker : Set A) = I := by73  rw [geometricStructureFamily_eq_image_ker_extremePoints_dual_closedBall]74  rfl7576/-- Send an extreme functional to its kernel as a point of the ORIGINAL77geometric structure space. This does not create a new structure space. -/78def extremeKernel (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :79    NormedSpace.GeometricStructureSpace ℂ A :=80  ⟨(rho.val.ker : Set A),81    (mem_geometricStructureFamily_iff_exists_mem_extremePoints_dual_closedBall _).mpr82      ⟨rho.val, rho.property, rfl⟩⟩8384@[simp]85theorem coe_extremeKernel (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :86    (extremeKernel rho).val = (rho.val.ker : Set A) := rfl8788/-- Every original GSS point is represented by an extreme-functional kernel.89Different functionals may map to the same point. -/90theorem extremeKernel_surjective : Function.Surjective (extremeKernel (A := A)) := by91  intro I92  obtain ⟨rho, hrho, hI⟩ :=93    (mem_geometricStructureFamily_iff_exists_mem_extremePoints_dual_closedBall I.val).mp I.property94  exact ⟨⟨rho, hrho⟩, Subtype.ext hI⟩9596end MathlibAnnex.Analysis.CStarAlgebra