Yamaguchi Lean 4 Library
FoxDifferential/Completed/FreeProC/CofinalQuotientKernelBasis.lean
FoxDifferential/Completed/FreeProC/CofinalQuotientKernelBasis/Source

FoxDifferential/Completed/FreeProC/CofinalQuotientKernelBasis.lean

1import FoxDifferential.Completed.FreeProC.QuotientKernelBasis
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FreeProC/CofinalQuotientKernelBasis.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Cofinal quotient-kernel bases for completed Fox approximation
14The completed Crowell density route is usually proved with all finite quotient stages, while the
15actual constructions are often made on a cofinal subfamily such as prime-power coefficient stages.
16This file records the purely topological reindexing API needed to replace a large quotient family
17by a cofinal refinement without changing the closure argument.
18-/
20namespace FoxDifferential
22noncomputable section
24open scoped Topology
26universe u v w
28section CofinalReindexing
30variable {Y : Type u} [Group Y] [TopologicalSpace Y]
31variable {J : Type v} {K : Type w}
32variable {Q : J → Type*} [∀ j, Group (Q j)]
33variable {Q' : K → Type*} [∀ k, Group (Q' k)]
34variable (π : ∀ j : J, Y →* Q j)
35variable (π' : ∀ k : K, Y →* Q' k)
37/-- Reindex an identity-neighbourhood quotient-kernel basis along a cofinal refinement of
38kernels.
40The hypothesis says that every kernel in the original quotient family contains the kernel of some
41refined quotient. This is the exact topological input needed to pass from all finite quotients to
42prime-power or otherwise cofinal stages. -/
43theorem HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
45 (hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker) :
47 intro U hU hUone
48 rcases hbasis U hU hUone with ⟨j, hj⟩
49 rcases hcofinal j with ⟨k, hk⟩
50 refine ⟨k, ?_⟩
51 intro z hz
52 exact hj z (hk hz)
54/-- Reindex a left-coset quotient-kernel basis along a cofinal refinement of kernels. -/
55theorem HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
57 (hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker) :
59 intro y U hU hyU
60 rcases hbasis y U hU hyU with ⟨j, hj⟩
61 rcases hcofinal j with ⟨k, hk⟩
62 refine ⟨k, ?_⟩
63 intro z hz
64 exact hj z (hk hz)
66/-- A factorization of the refined quotient through an original quotient gives the required kernel
67inclusion for identity-neighbourhood reindexing. -/
68theorem HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_factor
70 (hrefine : ∀ j : J, ∃ k : K, ∃ τ : Q' k →* Q j, τ.comp (π' k) = π j) :
72 refine
73 HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
74 (Y := Y) (π := π) (π' := π') hbasis ?_
75 intro j
76 rcases hrefine j with ⟨k, τ, hτ⟩
77 refine ⟨k, ?_⟩
78 intro z hz
79 change π j z = 1
80 have hz' : τ (π' k z) = 1 := by
81 rw [hz]
82 exact map_one τ
83 simpa [← hτ, MonoidHom.comp_apply] using hz'
85/-- A factorization of the refined quotient through an original quotient gives the required kernel
86inclusion for left-coset reindexing. -/
87theorem HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_factor
89 (hrefine : ∀ j : J, ∃ k : K, ∃ τ : Q' k →* Q j, τ.comp (π' k) = π j) :
91 refine
92 HasLeftQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
93 (Y := Y) (π := π) (π' := π') hbasis ?_
94 intro j
95 rcases hrefine j with ⟨k, τ, hτ⟩
96 refine ⟨k, ?_⟩
97 intro z hz
98 change π j z = 1
99 have hz' : τ (π' k z) = 1 := by
100 rw [hz]
101 exact map_one τ
102 simpa [← hτ, MonoidHom.comp_apply] using hz'
104/-- Closure approximation can be checked on any cofinal refinement of quotient kernels. -/
106 [IsTopologicalGroup Y]
107 {S T : Set Y}
109 (hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker)
110 (happrox :
111 ∀ y : Y, y ∈ T → ∀ k : K,
112 ∃ s : Y, s ∈ S ∧ π' k s = π' k y) :
113 T ⊆ closure S :=
115 (Y := Y) (S := S) (T := T) π'
116 (HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
117 (Y := Y) (π := π) (π' := π') hbasis hcofinal)
118 happrox
120/-- Stage-exact closure approximation can be checked on a cofinal refined quotient family. -/
122 [IsTopologicalGroup Y]
123 {S T : Set Y}
125 (hcofinal : ∀ j : J, ∃ k : K, (π' k).ker ≤ (π j).ker)
126 (Sstage Tstage : ∀ k : K, Set (Q' k))
127 (hTstage : ∀ y : Y, y ∈ T → ∀ k : K, π' k y ∈ Tstage k)
128 (hstage_exact : ∀ k : K, Tstage k ⊆ Sstage k)
129 (hlift_stage : ∀ k : K, ∀ q : Q' k, q ∈ Sstage k →
130 ∃ s : Y, s ∈ S ∧ π' k s = q) :
131 T ⊆ closure S :=
133 (Y := Y) (S := S) (T := T) π'
134 (HasIdentityQuotientKernelNeighbourhoodBasis.reindex_of_ker_le
135 (Y := Y) (π := π) (π' := π') hbasis hcofinal)
136 Sstage Tstage hTstage hstage_exact hlift_stage
138end CofinalReindexing
140end
142end FoxDifferential