MathlibAnnex/Analysis/Normed/GeometricStructure/Basic.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-/6module78public import MathlibAnnex.Analysis.Normed.GeometricStructure.Face9public import MathlibAnnex.Analysis.Normed.GeometricStructure.Support10public import MathlibAnnex.Topology.ClosureSpace.HullKernel1112/-!13# The geometric structure space from maximal faces1415`S(E)` is a family of sets `I_F`, and not a family of maximal faces: different faces16with the same union of kernels yield the same point. The real structure used for17faces is the canonical restriction of scalars from the given `RCLike` field.18Completeness, finite dimension, and nontriviality are not assumed.1920The representation by extreme-functional kernels is a subsequent bridge theorem,21not the definition. No C*-algebra result is imported here.22-/2324@[expose] public section2526set_option autoImplicit false2728universe u v2930namespace NormedSpace3132variable (𝕜 : Type v) [RCLike 𝕜]33variable (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E]3435/-- The family of unions of supporting kernels, indexed by maximal faces.36The existential is propositional: repeated subsets are not repeated points. -/37def geometricStructureFamily : Set (Set E) :=38  letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E39  {I | ∃ F : Set E, IsMaximalFace F ∧ supportKernelUnion 𝕜 F = I}4041theorem mem_geometricStructureFamily (I : Set E) :42    I ∈ geometricStructureFamily 𝕜 E ↔43      (letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E44       ∃ F : Set E, IsMaximalFace F ∧ supportKernelUnion 𝕜 F = I) := Iff.rfl4546/-- The family meets the exact admissibility condition for the generic hull-kernel space. -/47theorem univ_notMem_geometricStructureFamily :48    Set.univ ∉ geometricStructureFamily 𝕜 E := by49  letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E50  rintro ⟨F, hF, hI⟩51  exact supportKernelUnion_ne_univ 𝕜 hF.nonempty hI5253/-- The points of the geometric structure space are actual subsets of the normed space. -/54def GeometricStructureSpace : Type u := {I : Set E // I ∈ geometricStructureFamily 𝕜 E}5556/-- The hull-kernel closure on `S(E)`. -/57def geometricStructureClosure : ClosureSpace (GeometricStructureSpace 𝕜 E) :=58  ClosureSpace.HullKernel.space (geometricStructureFamily 𝕜 E)59    (univ_notMem_geometricStructureFamily 𝕜 E)6061/-- The closure formula exposes the intersection, including the empty intersection. -/62theorem geometricStructureClosure_closure (S : Set (GeometricStructureSpace 𝕜 E)) :63    (geometricStructureClosure 𝕜 E).closure S =64      {I | (∀ x : E, (∀ J : GeometricStructureSpace 𝕜 E, J ∈ S → x ∈ J.val) →65        x ∈ I.val)} := rfl6667/-- Generic hull-kernel separation gives T0, not yet the stronger T1 theorem. -/68theorem isT0_geometricStructureClosure : (geometricStructureClosure 𝕜 E).IsT0 :=69  ClosureSpace.HullKernel.isT0_space (geometricStructureFamily 𝕜 E)70    (univ_notMem_geometricStructureFamily 𝕜 E)7172/-- The family is empty in the zero-space case. -/73theorem geometricStructureFamily_eq_empty_of_subsingleton [Subsingleton E] :74    geometricStructureFamily 𝕜 E = ∅ := by75  letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E76  apply Set.eq_empty_iff_forall_notMem.277  rintro I ⟨F, hF, _⟩78  exact not_isMaximalFace_of_subsingleton F hF7980/-- No geometric-structure-space point exists in the zero space. -/81theorem isEmpty_geometricStructureSpace_of_subsingleton [Subsingleton E] :82    IsEmpty (GeometricStructureSpace 𝕜 E) := by83  refine ⟨?_⟩84  intro I85  exact (Set.eq_empty_iff_forall_notMem.mp86    (geometricStructureFamily_eq_empty_of_subsingleton 𝕜 E)) I.val I.property8788end NormedSpace