TopologySemilinearRank.lean

1 import PaperIRelease.TopologySeedRank
2 
3 /-!
4 # Topological seed rank for arbitrary ring-changing module maps
5 
6 The rank here is defined directly from the actual module span. The theorem
7 allows an arbitrary ring homomorphism, including non-surjective ones, and a
8 continuous additive semilinear surjection. No faithful-action hypothesis or
9 choice of a map between concrete endomorphism algebras is needed.
10 -/
11 
12 noncomputable section
13 open Set Function Cardinal
14 
15 namespace PaperIRelease.TopologySemilinearRank
16 
17 universe u v w
18 variable {A : Type u} {B : Type w} {M N : Type v}
19 variable [Ring A] [Ring B] [AddCommGroup M] [Module A M]
20 variable [AddCommGroup N] [Module B N]
21 variable [TopologicalSpace M] [TopologicalSpace N]
22 
23 /-- Dense generation by the actual acting-ring module span. -/
24 def Generates (A : Type*) {M : Type v} [Ring A] [AddCommGroup M] [Module A M]
25     [TopologicalSpace M] (S : Set M) : Prop := Dense (Submodule.span A S : Set M)
26 
27 /-- The full cardinal-valued topological module seed rank. -/
28 def moduleSeedRank (A : Type*) (M : Type v) [Ring A] [AddCommGroup M] [Module A M]
29     [TopologicalSpace M] : Cardinal.{v} :=
30   ⨅ S : {S : Set M // Generates A S}, #S.1
31 
32 theorem generates_univ : Generates A (univ : Set M) := by
33   simp [Generates]
34 
35 theorem rank_le_card {S : Set M} (hS : Generates A S) : moduleSeedRank A M ≤ #S :=
36   ciInf_le' (fun T : {T : Set M // Generates A T} ↦ #T.1) ⟨S, hS⟩
37 
38 theorem rank_attained : ∃ S : Set M, Generates A S ∧ #S = moduleSeedRank A M := by
39   have hm : moduleSeedRank A M ∈ range (fun S : {S : Set M // Generates A S} ↦ #S.1) :=
40     csInf_mem ⟨#(univ : Set M), ⟨⟨univ, generates_univ⟩, rfl⟩⟩
41   obtain ⟨S, hS⟩ := hm
42   exact ⟨S.1, S.2, hS⟩
43 
44 omit [TopologicalSpace M] [TopologicalSpace N] in
45 /-- Semilinearity carries the source module span into the target module
46 span even when the ring homomorphism is not surjective. -/
47 theorem map_mem_span {φ : A →+* B} (f : M →ₛₗ[φ] N) (S : Set M)
48     {x : M} (hx : x ∈ Submodule.span A S) : f x ∈ Submodule.span B (f '' S) := by
49   induction hx using Submodule.span_induction with
50   | mem x hx => exact Submodule.subset_span ⟨x, hx, rfl⟩
51   | zero => simp
52   | add x y hx hy ihx ihy => simpa using Submodule.add_mem _ ihx ihy
53   | smul a x hx ih => simpa using Submodule.smul_mem (Submodule.span B (f '' S)) (φ a) ih
54 
55 /-- Exact topological semilinear surjection theorem for generated sets. -/
56 theorem generates_image {φ : A →+* B} (f : M →ₛₗ[φ] N)
57     (hf : Surjective f) (hcont : Continuous f) {S : Set M} (hS : Generates A S) :
58     Generates B (f '' S) := by
59   apply (hf.denseRange.dense_image hcont hS).mono
60   rintro y ⟨x, hx, rfl⟩
61   exact map_mem_span f S hx
62 
63 /-- PSC-I-T-QUOTIENT-MONOTONICITY, topological clause, with the literal
64 arbitrary ring-homomorphism and additive semilinear hypotheses. -/
65 theorem rank_le_of_continuous_semilinear_surjective
66     {φ : A →+* B} (f : M →ₛₗ[φ] N) (hf : Surjective f) (hcont : Continuous f) :
67     moduleSeedRank B N ≤ moduleSeedRank A M := by
68   obtain ⟨S, hS, hcard⟩ := rank_attained (A := A) (M := M)
69   calc
70     moduleSeedRank B N ≤ #(f '' S) := rank_le_card (generates_image f hf hcont hS)
71     _ ≤ #S := Cardinal.mk_image_le
72     _ = moduleSeedRank A M := hcard
73 
74 /-- The same statement starting with the printed additive map and its
75 explicit scalar compatibility, rather than a prebundled semilinear map. -/
76 theorem rank_le_of_continuous_additive_surjective
77     (φ : A →+* B) (f : M →+ N) (hf : Surjective f) (hcont : Continuous f)
78     (hsmul : ∀ a x, f (a • x) = φ a • f x) :
79     moduleSeedRank B N ≤ moduleSeedRank A M := by
80   let F : M →ₛₗ[φ] N := { f with map_smul' := hsmul }
81   exact rank_le_of_continuous_semilinear_surjective F hf hcont
82 
83 /-- Topological ring-changing module isomorphisms preserve the same
84 cardinal-valued rank, using the actual inverse semilinear map. -/
85 theorem rank_eq_of_continuous_semilinear_equiv
86     {φ : A →+* B} {ψ : B →+* A} [RingHomInvPair φ ψ] [RingHomInvPair ψ φ]
87     (e : M ≃ₛₗ[φ] N) (hc : Continuous e) (hci : Continuous e.symm) :
88     moduleSeedRank A M = moduleSeedRank B N := by
89   apply le_antisymm
90   · exact rank_le_of_continuous_semilinear_surjective e.symm.toLinearMap e.symm.surjective hci
91   · exact rank_le_of_continuous_semilinear_surjective e.toLinearMap e.surjective hc
92 
93 section OperatorBridge
94 
95 variable [IsTopologicalAddGroup M] [ContinuousConstSMul A M]
96 
97 /-- Every continuous action of an arbitrary ring element is a continuous
98 integer-linear endomorphism of the additive module. -/
99 def actingOperator (a : A) : M →L[ℤ] M :=
100   { (smulAddHom A M a).toIntLinearMap with cont := continuous_const_smul a }
101 
102 /-- The concrete acting operator family, allowing a nonfaithful action. -/
103 def actingOperators : Set (M →L[ℤ] M) := range (actingOperator (A := A) (M := M))
104 
105 omit [IsTopologicalAddGroup M] in
106 /-- The integer-linear orbit hull is exactly the actual `A`-module span.
107 This proves the connection between the operator-family rank and the
108 arbitrary acting-ring module rank, rather than asserting it as an input. -/
109 theorem operatorHull_eq_moduleSpan (S : Set M) :
110     (TopologyTransport.operatorHull (actingOperators (A := A) (M := M)) S : Set M) =
111       (Submodule.span A S : Set M) := by
112   ext x
113   constructor
114   · intro hx
115     induction hx using Submodule.span_induction with
116     | mem x hx =>
117       rcases hx with ⟨T, ⟨a, rfl⟩, s, hs, rfl⟩
118       exact Submodule.smul_mem _ a (Submodule.subset_span hs)
119     | zero => exact Submodule.zero_mem _
120     | add x y hx hy ihx ihy => exact Submodule.add_mem _ ihx ihy
121     | smul z x hx ih => exact (Submodule.span A S).toAddSubgroup.zsmul_mem ih z
122   · intro hx
123     have hstable (a : A) {x : M}
124         (hx : x ∈ TopologyTransport.operatorHull (actingOperators (A := A) (M := M)) S) :
125         a • x ∈ TopologyTransport.operatorHull (actingOperators (A := A) (M := M)) S := by
126       induction hx using Submodule.span_induction with
127       | mem x hx =>
128         rcases hx with ⟨T, ⟨b, rfl⟩, s, hs, rfl⟩
129         exact Submodule.subset_span ⟨actingOperator (a * b), ⟨a * b, rfl⟩, s, hs,
130           mul_smul a b s⟩
131       | zero => simp
132       | add x y hx hy ihx ihy => simpa only [smul_add] using Submodule.add_mem _ ihx ihy
133       | smul z x hx ih =>
134         have h := Submodule.smul_mem
135           (TopologyTransport.operatorHull (actingOperators (A := A) (M := M)) S) z ih
136         simpa only [smul_comm a z] using h
137     induction hx using Submodule.span_induction with
138     | mem x hx =>
139       exact Submodule.subset_span ⟨actingOperator (1 : A), ⟨1, rfl⟩, x, hx, one_smul A x⟩
140     | zero => exact Submodule.zero_mem _
141     | add x y hx hy ihx ihy => exact Submodule.add_mem _ ihx ihy
142     | smul a x hx ih => exact hstable a ih
143 
144 theorem generates_iff_operator_generates (S : Set M) :
145     Generates A S ↔ TopologyTransport.TopologicallyGenerates (actingOperators (A := A) (M := M)) S := by
146   rw [TopologyTransport.TopologicallyGenerates, ← Submodule.dense_iff_topologicalClosure_eq_top]
147   rw [operatorHull_eq_moduleSpan]
148   rfl
149 
150 /-- The two cardinal rank definitions agree exactly. -/
151 theorem moduleSeedRank_eq_operatorSeedRank :
152     moduleSeedRank A M =
153       TopologyTransport.topologicalSeedRank (actingOperators (A := A) (M := M)) := by
154   have hp : Generates (M := M) A =
155       TopologyTransport.TopologicallyGenerates (actingOperators (A := A) (M := M)) := by
156     funext S
157     exact propext (generates_iff_operator_generates S)
158   unfold moduleSeedRank TopologyTransport.topologicalSeedRank
159   rw [hp]
160 
161 end OperatorBridge
162 
163 end PaperIRelease.TopologySemilinearRank

Back to source controls