TopologyPresentations.lean

1 import PaperIRelease.TopologyDenseCompletion
2 import KomorebiVerification.SeedRankBasics
3 
4 /-! # Actual free evaluation and restricted quotient completion -/
5 
6 noncomputable section
7 open Set Function UniformSpace
8 
9 namespace PaperIRelease.TopologyDenseCompletion
10 
11 section FreePresentation
12 
13 variable {A X : Type*} [Ring A] [AddCommGroup X] [Module A X]
14 variable [UniformSpace X] [IsUniformAddGroup X] [UniformContinuousConstSMul A X]
15 variable [CompleteSpace X] [T0Space X]
16 
17 omit [IsUniformAddGroup X] [UniformContinuousConstSMul A X] [CompleteSpace X] [T0Space X] in
18 /-- Dense generation is exactly dense range of the actual seed evaluation
19 map, with no surjectivity assumption. -/
20 theorem dense_free_evaluation {ι : Type*} (s : ι → X)
21     (hS : Dense (Submodule.span A (Set.range s) : Set X)) :
22     DenseRange (Komorebi.SeedRankBasics.multiSeedMap A X s) := by
23   change Dense (LinearMap.range (Komorebi.SeedRankBasics.multiSeedMap A X s) : Set X)
24   rwa [Komorebi.SeedRankBasics.range_multiSeedMap]
25 
26 /-- Literal finite free-presentation completion. `r = 0` and the zero
27 target are included. The equivalence is linear over the acting ring `A`,
28 so it simultaneously intertwines every element of the acting algebra. -/
29 def completedFreePresentation (r : ℕ) (s : Fin r → X)
30     (hS : Dense (Submodule.span A (Set.range s) : Set X)) :=
31   completedQuotientEquiv (Komorebi.SeedRankBasics.multiSeedMap A X s)
32     (dense_free_evaluation s hS)
33 
34 end FreePresentation
35 
36 section RestrictedQuotient
37 
38 variable {𝕜 X Y : Type*} [Ring 𝕜]
39 variable [AddCommGroup X] [Module 𝕜 X]
40 variable [AddCommGroup Y] [Module 𝕜 Y] [UniformSpace Y]
41 variable [IsUniformAddGroup Y] [UniformContinuousConstSMul 𝕜 Y]
42 variable [CompleteSpace Y] [T0Space Y]
43 
44 omit [UniformSpace Y] [IsUniformAddGroup Y] [UniformContinuousConstSMul 𝕜 Y]
45   [CompleteSpace Y] [T0Space Y] in
46 /-- The relation module of the restriction to `D` is exactly `D ∩ ker f`,
47 expressed as a submodule of `D`. -/
48 theorem restricted_kernel (f : X →ₗ[𝕜] Y) (D : Submodule 𝕜 X) :
49     (f.comp D.subtype).ker = f.ker.comap D.subtype := rfl
50 
51 omit [IsUniformAddGroup Y] [UniformContinuousConstSMul 𝕜 Y] [CompleteSpace Y] [T0Space Y] in
52 /-- Density of the image `f(D)` is density of the restricted presentation. -/
53 theorem restricted_dense (f : X →ₗ[𝕜] Y) (D : Submodule 𝕜 X)
54     (hd : Dense (f '' (D : Set X))) : DenseRange (f.comp D.subtype) := by
55   have he : Set.range (f.comp D.subtype) = f '' (D : Set X) := by
56     ext y
57     constructor
58     · rintro ⟨x, rfl⟩
59       exact ⟨x, x.property, rfl⟩
60     · rintro ⟨x, hx, rfl⟩
61       exact ⟨⟨x, hx⟩, rfl⟩
62   change Dense (Set.range (f.comp D.subtype))
63   rwa [he]
64 
65 /-- The completed realization from the actual quotient `D/(D ∩ ker f)`.
66 Its topology is pulled back from `Y`; it need not be the quotient topology
67 inherited from the original domain. -/
68 def completedRestrictedQuotient (f : X →ₗ[𝕜] Y) (D : Submodule 𝕜 X)
69     (hd : Dense (f '' (D : Set X))) :=
70   completedQuotientEquiv (f.comp D.subtype) (restricted_dense f D hd)
71 
72 end RestrictedQuotient
73 
74 end PaperIRelease.TopologyDenseCompletion

Back to source controls