TopologyTransport.lean

1 import KomorebiVerification.TopologicalCompletion
2 import Mathlib.Topology.Algebra.Module.Basic
3 import Mathlib.LinearAlgebra.Isomorphisms
4 
5 /-!
6 # Paper I: topological transport at the stated generality
7 
8 The dense-realization result below uses topological modules, without a norm
9 or a metrizability assumption. Fibre aggregation is represented by actual
10 finite sums of the source projectors. The quotient equivalence uses an
11 explicit quotient-map hypothesis.
12 -/
13 
14 noncomputable section
15 open scoped BigOperators
16 open Set Function Topology
17 
18 namespace PaperIRelease.TopologyTransport
19 
20 section General
21 
22 variable {𝕜 X Y : Type*} [Ring 𝕜] [TopologicalSpace 𝕜]
23 variable [AddCommGroup X] [Module 𝕜 X] [TopologicalSpace X]
24 variable [AddCommGroup Y] [Module 𝕜 Y] [TopologicalSpace Y]
25 variable [ContinuousAdd X] [ContinuousSMul 𝕜 X]
26 variable [ContinuousAdd Y] [ContinuousSMul 𝕜 Y]
27 
28 /-- The algebraic operator hull in a general topological module. -/
29 def operatorHull (A : Set (X →L[𝕜] X)) (S : Set X) : Submodule 𝕜 X :=
30   Submodule.span 𝕜 {x | ∃ T ∈ A, ∃ s ∈ S, T s = x}
31 
32 omit [TopologicalSpace 𝕜] [ContinuousAdd X] [ContinuousSMul 𝕜 X]
33   [ContinuousAdd Y] [ContinuousSMul 𝕜 Y] in
34 /-- Intertwining transports the actual operator hull. -/
35 theorem map_operatorHull_le
36     (f : X →L[𝕜] Y) (φ : (X →L[𝕜] X) → (Y →L[𝕜] Y))
37     (A : Set (X →L[𝕜] X)) (B : Set (Y →L[𝕜] Y))
38     (S : Set X) (hφ : ∀ T ∈ A, φ T ∈ B)
39     (hintertwine : ∀ T ∈ A, f.comp T = (φ T).comp f) :
40     (operatorHull A S).map f.toLinearMap ≤ operatorHull B (f '' S) := by
41   rw [Submodule.map_le_iff_le_comap]
42   apply Submodule.span_le.2
43   rintro x ⟨T, hTA, s, hs, rfl⟩
44   change f (T s) ∈ operatorHull B (f '' S)
45   have hpoint : f (T s) = φ T (f s) := by
46     simpa using congrArg (fun L : X →L[𝕜] Y ↦ L s) (hintertwine T hTA)
47   rw [hpoint]
48   exact Submodule.subset_span ⟨φ T, hφ T hTA, f s, ⟨s, hs, rfl⟩, rfl⟩
49 
50 /-- Dense realization for arbitrary topological modules. In particular,
51 this covers Hausdorff topological vector spaces as printed in Paper I. -/
52 theorem dense_operatorHull_image
53     (f : X →L[𝕜] Y) (hf : Surjective f)
54     (φ : (X →L[𝕜] X) → (Y →L[𝕜] Y))
55     (A : Set (X →L[𝕜] X)) (B : Set (Y →L[𝕜] Y))
56     (S : Set X) (hφ : ∀ T ∈ A, φ T ∈ B)
57     (hintertwine : ∀ T ∈ A, f.comp T = (φ T).comp f)
58     (hgenerate : (operatorHull A S).topologicalClosure = ⊤) :
59     (operatorHull B (f '' S)).topologicalClosure = ⊤ := by
60   have himage : ((operatorHull A S).map f.toLinearMap).topologicalClosure = ⊤ :=
61     hf.denseRange.topologicalClosure_map_submodule hgenerate
62   apply top_unique
63   rw [← himage]
64   exact Submodule.topologicalClosure_mono
65     (map_operatorHull_le f φ A B S hφ hintertwine)
66 
67 omit [TopologicalSpace 𝕜] [ContinuousAdd X] [ContinuousSMul 𝕜 X]
68   [ContinuousAdd Y] [ContinuousSMul 𝕜 Y] in
69 /-- A continuous surjective intertwiner maps the source range onto the
70 target range, with no norm assumption. -/
71 theorem map_packetRange_eq
72     (f : X →L[𝕜] Y) (hf : Surjective f)
73     (P : X →L[𝕜] X) (Q : Y →L[𝕜] Y)
74     (hintertwine : f.comp P = Q.comp f) :
75     P.range.map f.toLinearMap = Q.range := by
76   have hi : ∀ a, f (P a) = Q (f a) := by
77     intro a
78     simpa using congrArg (fun L : X →L[𝕜] Y ↦ L a) hintertwine
79   ext y
80   constructor
81   · rintro ⟨x, ⟨a, rfl⟩, rfl⟩
82     exact ⟨f a, (hi a).symm⟩
83   · rintro ⟨b, rfl⟩
84     rcases hf b with ⟨a, rfl⟩
85     exact ⟨P a, ⟨a, rfl⟩, hi a⟩
86 
87 omit [TopologicalSpace 𝕜] [ContinuousSMul 𝕜 X] [ContinuousAdd Y] [ContinuousSMul 𝕜 Y] in
88 /-- The arbitrary fibre-aggregation clause of dense realization. Empty
89 fibres are included because their projector is the empty sum. -/
90 theorem map_aggregated_packetRange_eq
91     {ι κ : Type*} [Fintype ι] [DecidableEq κ]
92     (f : X →L[𝕜] Y) (hf : Surjective f) (σ : ι → κ)
93     (P : ι → X →L[𝕜] X) (Q : κ → Y →L[𝕜] Y)
94     (hintertwine : ∀ j, f.comp (∑ i with σ i = j, P i) = (Q j).comp f)
95     (j : κ) :
96     (∑ i with σ i = j, P i).range.map f.toLinearMap = (Q j).range :=
97   map_packetRange_eq f hf _ _ (hintertwine j)
98 
99 end General
100 
101 section Quotient
102 
103 variable {𝕜 X Y : Type*} [Ring 𝕜]
104 variable [AddCommGroup X] [Module 𝕜 X] [TopologicalSpace X]
105 variable [AddCommGroup Y] [Module 𝕜 Y] [TopologicalSpace Y]
106 
107 /-- The algebraic first-isomorphism equivalence is a topological linear
108 equivalence precisely under the declared quotient-map hypothesis. -/
109 def quotientEquiv (f : X →L[𝕜] Y) (hf : IsQuotientMap f) :
110     (X ⧸ f.ker) ≃L[𝕜] Y := by
111   let e := f.toLinearMap.quotKerEquivOfSurjective hf.surjective
112   have hcomp : (e : X ⧸ f.ker → Y) ∘ f.ker.mkQ = f := by
113     funext x
114     exact LinearMap.quotKerEquivOfSurjective_apply_mk _ _ x
115   have he : IsQuotientMap e := by
116     apply f.ker.isQuotientMap_mkQ.of_comp_isQuotientMap
117     simpa only [hcomp] using hf
118   refine { e with continuous_toFun := he.continuous, continuous_invFun := ?_ }
119   apply he.continuous_iff.2
120   convert (continuous_id : Continuous (id : X ⧸ f.ker → X ⧸ f.ker)) using 1
121   funext x
122   exact e.symm_apply_apply x
123 
124 @[simp]
125 theorem quotientEquiv_apply_mk (f : X →L[𝕜] Y) (hf : IsQuotientMap f) (x : X) :
126     quotientEquiv f hf (f.ker.mkQ x) = f x :=
127   LinearMap.quotKerEquivOfSurjective_apply_mk f.toLinearMap hf.surjective x
128 
129 end Quotient
130 
131 end PaperIRelease.TopologyTransport

Back to source controls