TopologySeedRank.lean

1 import PaperIRelease.TopologyTransport
2 import Mathlib.SetTheory.Cardinal.Basic
3 
4 /-! # Cardinal-valued topological seed rank and its transport laws -/
5 
6 noncomputable section
7 open Set Function Cardinal
8 
9 namespace PaperIRelease.TopologyTransport
10 
11 universe u v
12 variable {𝕜 : Type u} {X Y : Type v} [Ring 𝕜] [TopologicalSpace 𝕜]
13 variable [AddCommGroup X] [Module 𝕜 X] [TopologicalSpace X]
14 variable [AddCommGroup Y] [Module 𝕜 Y] [TopologicalSpace Y]
15 variable [ContinuousAdd X] [ContinuousSMul 𝕜 X]
16 variable [ContinuousAdd Y] [ContinuousSMul 𝕜 Y]
17 
18 /-- A seed set generates topologically when its algebraic operator hull is dense. -/
19 def TopologicallyGenerates (A : Set (X →L[𝕜] X)) (S : Set X) : Prop :=
20   (operatorHull A S).topologicalClosure = ⊤
21 
22 /-- Minimum cardinality of a densely generating seed set. For an acting
23 unital algebra the infimum is attained, as proved below. -/
24 def topologicalSeedRank (A : Set (X →L[𝕜] X)) : Cardinal.{v} :=
25   ⨅ (S : {S : Set X // TopologicallyGenerates A S}), #S.1
26 
27 theorem generates_univ (A : Set (X →L[𝕜] X))
28     (hA : ContinuousLinearMap.id 𝕜 X ∈ A) : TopologicallyGenerates A univ := by
29   have h : operatorHull A univ = ⊤ := by
30     apply top_unique
31     intro x _
32     exact Submodule.subset_span ⟨ContinuousLinearMap.id 𝕜 X, hA, x, mem_univ x, rfl⟩
33   change (operatorHull A univ).topologicalClosure = ⊤
34   rw [h]
35   exact top_unique (Submodule.le_topologicalClosure ⊤)
36 
37 theorem seedRank_le_card {A : Set (X →L[𝕜] X)} {S : Set X}
38     (hS : TopologicallyGenerates A S) : topologicalSeedRank A ≤ #S :=
39   ciInf_le' (fun T : {T : Set X // TopologicallyGenerates A T} ↦ #T.1) ⟨S, hS⟩
40 
41 /-- The infimum used in the definition is a minimum, including the zero
42 space and infinite generating cardinals. -/
43 theorem exists_generating_set_card_eq_seedRank (A : Set (X →L[𝕜] X))
44     (hA : ContinuousLinearMap.id 𝕜 X ∈ A) :
45     ∃ S : Set X, TopologicallyGenerates A S ∧ #S = topologicalSeedRank A := by
46   have hmem : topologicalSeedRank A ∈
47       Set.range (fun S : {S : Set X // TopologicallyGenerates A S} ↦ #S.1) :=
48     csInf_mem ⟨#(univ : Set X), ⟨⟨univ, generates_univ A hA⟩, rfl⟩⟩
49   obtain ⟨S, hS⟩ := hmem
50   exact ⟨S.1, S.2, hS⟩
51 
52 theorem generates_mono_algebra {A B : Set (X →L[𝕜] X)} {S : Set X}
53     (hAB : A ⊆ B) (hS : TopologicallyGenerates A S) :
54     TopologicallyGenerates B S := by
55   have hHull : operatorHull A S ≤ operatorHull B S := by
56     apply Submodule.span_mono
57     rintro x ⟨T, hT, s, hs, rfl⟩
58     exact ⟨T, hAB hT, s, hs, rfl⟩
59   apply top_unique
60   rw [← hS]
61   exact Submodule.topologicalClosure_mono hHull
62 
63 /-- Enlarging the acting algebra cannot increase topological seed rank. -/
64 theorem seedRank_mono_algebra {A B : Set (X →L[𝕜] X)}
65     (hA : ContinuousLinearMap.id 𝕜 X ∈ A) (hAB : A ⊆ B) :
66     topologicalSeedRank B ≤ topologicalSeedRank A := by
67   obtain ⟨S, hS, hcard⟩ := exists_generating_set_card_eq_seedRank A hA
68   rw [← hcard]
69   exact seedRank_le_card (generates_mono_algebra hAB hS)
70 
71 /-- Surjective continuous intertwiners cannot increase topological seed
72 rank. This includes the closed invariant quotient with its induced action. -/
73 theorem seedRank_le_of_surjective
74     (f : X →L[𝕜] Y) (hf : Surjective f)
75     (φ : (X →L[𝕜] X) → (Y →L[𝕜] Y))
76     (A : Set (X →L[𝕜] X)) (B : Set (Y →L[𝕜] Y))
77     (hA : ContinuousLinearMap.id 𝕜 X ∈ A) (hφ : ∀ T ∈ A, φ T ∈ B)
78     (hintertwine : ∀ T ∈ A, f.comp T = (φ T).comp f) :
79     topologicalSeedRank B ≤ topologicalSeedRank A := by
80   obtain ⟨S, hS, hcard⟩ := exists_generating_set_card_eq_seedRank A hA
81   calc
82     topologicalSeedRank B ≤ #(f '' S) :=
83       seedRank_le_card (dense_operatorHull_image f hf φ A B S hφ hintertwine hS)
84     _ ≤ #S := Cardinal.mk_image_le
85     _ = topologicalSeedRank A := hcard
86 
87 /-- A topological linear isomorphism intertwining both action families
88 preserves the full cardinal-valued topological seed rank. -/
89 theorem seedRank_equiv
90     (e : X ≃L[𝕜] Y)
91     (φ : (X →L[𝕜] X) → (Y →L[𝕜] Y))
92     (ψ : (Y →L[𝕜] Y) → (X →L[𝕜] X))
93     (A : Set (X →L[𝕜] X)) (B : Set (Y →L[𝕜] Y))
94     (hA : ContinuousLinearMap.id 𝕜 X ∈ A) (hB : ContinuousLinearMap.id 𝕜 Y ∈ B)
95     (hφ : ∀ T ∈ A, φ T ∈ B) (hψ : ∀ T ∈ B, ψ T ∈ A)
96     (hforward : ∀ T ∈ A, e.toContinuousLinearMap.comp T = (φ T).comp e.toContinuousLinearMap)
97     (hbackward : ∀ T ∈ B, e.symm.toContinuousLinearMap.comp T = (ψ T).comp e.symm.toContinuousLinearMap) :
98     topologicalSeedRank A = topologicalSeedRank B := by
99   apply le_antisymm
100   · exact seedRank_le_of_surjective e.symm.toContinuousLinearMap e.symm.surjective ψ B A hB hψ hbackward
101   · exact seedRank_le_of_surjective e.toContinuousLinearMap e.surjective φ A B hA hφ hforward
102 
103 end PaperIRelease.TopologyTransport

Back to source controls