Source: ProCGroups.FoxDifferential.Completed.FreeProC.CofinalQuotientKernelBasis
1import ProCGroups.FoxDifferential.Completed.FreeProC.QuotientKernelBasis
3/-!
4# Fox differential: completed — free pro-\(C\) — cofinal quotient kernel basis
6The principal declarations in this module are:
8- `HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le`
9 Reindex an identity-neighborhood quotient-kernel basis along a cofinal refinement of kernels. The
10 hypothesis says that every kernel in the original quotient family contains the kernel of some
11 refined quotient. This is the topological input used to pass from all finite quotients to
12 prime-power or otherwise cofinal stages.
13- `HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le`
14 Reindex a left-neighborhood quotient-kernel basis along a cofinal refinement of kernels. Every
15 kernel in the original family is required to contain a kernel from the refined family.
16- `HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_factor`
17 A factorization of the refined quotient through an original quotient gives the required kernel
18 inclusion for identity-neighborhood reindexing.
19- `HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_factor`
20 A factorization of each refined quotient through an original quotient gives the kernel inclusion
21 needed to reindex a left-neighborhood quotient-kernel basis.
22-/
24namespace FoxDifferential
26noncomputable section
28open scoped Topology
30universe u v w
32section CofinalReindexing
34variable {Y : Type u} [Group Y] [TopologicalSpace Y]
35variable {J : Type v} {K : Type w}
36variable {Q : J → Type*} [∀ j, Group (Q j)]
37variable {Q' : K → Type*} [∀ k, Group (Q' k)]
38variable (π : ∀ j : J, Y →* Q j)
39variable (π' : ∀ k : K, Y →* Q' k)
41/--
42Reindex an identity-neighborhood quotient-kernel basis along a cofinal refinement of kernels.
43The hypothesis says that every kernel in the original quotient family contains the kernel of
44some refined quotient. This is the topological input used to pass from all finite quotients to
45prime-power or otherwise cofinal stages.
46-/
47theorem HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
48 (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
49 (hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker) :
50 HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π' := by
51 intro U hU hUone
52 rcases hbasis U hU hUone with ⟨j, hj⟩
53 rcases hcofinal j with ⟨k, hk⟩
54 refine ⟨k, ?_⟩
55 intro z hz
56 exact hj z (hk hz)
58/--
59Reindex a left-neighborhood quotient-kernel basis along a cofinal refinement of kernels. Every
60kernel in the original family is required to contain a kernel from the refined family.
61-/
62theorem HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
63 (hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
64 (hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker) :
65 HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π' := by
66 intro y U hU hyU
67 rcases hbasis y U hU hyU with ⟨j, hj⟩
68 rcases hcofinal j with ⟨k, hk⟩
69 refine ⟨k, ?_⟩
70 intro z hz
71 exact hj z (hk hz)
73/--
74A factorization of the refined quotient through an original quotient gives the required kernel
75inclusion for identity-neighborhood reindexing.
76-/
77theorem HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_factor
78 (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
79 (hrefine : ∀ j : J, ∃ k : K, ∃ τ : Q' k →* Q j, τ.comp (π' k) = π j) :
80 HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π' := by
81 refine
82 HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
83 (Y := Y) (π := π) (π' := π') hbasis ?_
84 intro j
85 rcases hrefine j with ⟨k, τ, hτ⟩
86 refine ⟨k, ?_⟩
87 intro z hz
88 change π j z = 1
89 have hz' : τ (π' k z) = 1 := by
90 rw [hz]
91 exact map_one τ
92 simpa [← hτ, MonoidHom.comp_apply] using hz'
94/--
95A factorization of each refined quotient through an original quotient gives the kernel inclusion
96needed to reindex a left-neighborhood quotient-kernel basis.
97-/
98theorem HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_factor
99 (hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
100 (hrefine : ∀ j : J, ∃ k : K, ∃ τ : Q' k →* Q j, τ.comp (π' k) = π j) :
101 HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π' := by
102 refine
103 HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
104 (Y := Y) (π := π) (π' := π') hbasis ?_
105 intro j
106 rcases hrefine j with ⟨k, τ, hτ⟩
107 refine ⟨k, ?_⟩
108 intro z hz
109 change π j z = 1
110 have hz' : τ (π' k z) = 1 := by
111 rw [hz]
112 exact map_one τ
113 simpa [← hτ, MonoidHom.comp_apply] using hz'
115/-- Closure approximation can be checked on any cofinal refinement of quotient kernels. -/
116theorem subset_closure_of_identityQuotientKernel_approximation_reindex
117 [IsTopologicalGroup Y]
118 {S T : Set Y}
119 (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
120 (hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker)
121 (happrox :
122 ∀ y : Y, y ∈ T → ∀ k : K,
123 ∃ s : Y, s ∈ S ∧ π' k s = π' k y) :
124 T ⊆ closure S :=
125 subset_closure_of_identityQuotientKernel_approximation
126 (Y := Y) (S := S) (T := T) π'
127 (HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
128 (Y := Y) (π := π) (π' := π') hbasis hcofinal)
129 happrox
131/-- The finite-stage closure approximation can be checked on a cofinal refined quotient family. -/
132theorem subset_closure_of_identityQuotientKernel_stage_exact_reindex
133 [IsTopologicalGroup Y]
134 {S T : Set Y}
135 (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
136 (hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker)
137 (Sstage Tstage : ∀ k : K, Set (Q' k))
138 (hTstage : ∀ y : Y, y ∈ T → ∀ k : K, π' k y ∈ Tstage k)
139 (hstage_exact : ∀ k : K, Tstage k ⊆ Sstage k)
140 (hlift_stage : ∀ k : K, ∀ q : Q' k, q ∈ Sstage k →
141 ∃ s : Y, s ∈ S ∧ π' k s = q) :
142 T ⊆ closure S :=
143 subset_closure_of_identityQuotientKernel_stage_exact
144 (Y := Y) (S := S) (T := T) π'
145 (HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
146 (Y := Y) (π := π) (π' := π') hbasis hcofinal)
147 Sstage Tstage hTstage hstage_exact hlift_stage
149end CofinalReindexing
151end
153end FoxDifferential