Source: ProCGroups.FoxDifferential.Completed.FreeProC.QuotientKernelBasis
1import ProCGroups.FoxDifferential.Completed.FreeProC.StageApproximation
3/-!
4# Fox differential: completed — free pro-\(C\) — quotient kernel basis
6The principal declarations in this module are:
8- `HasIdentityQuotientKernelNeighbourhoodBasis`
9 Quotient kernels form a neighborhood basis at the identity. For every open neighborhood of 1, some
10 finite-stage kernel is contained in it. In a topological group this is the natural form obtained
11 from finite quotient separation; it implies the left-coset basis used by
12 subset_closure_of_quotientKernel_approximation.
13- `HasIdentityQuotientKernelNeighbourhoodBasis.to_left`
14 Identity-neighborhood quotient kernels give the left quotient-kernel basis.
15- `subset_closure_of_identityQuotientKernel_approximation`
16 Closure criterion using identity-neighborhood quotient kernels directly.
17- `subset_closure_of_identityQuotientKernel_stage_exact`
18 The closure criterion with identity-neighborhood quotient kernels can be checked at finite stages.
19-/
21namespace FoxDifferential
23noncomputable section
25open scoped Topology
27universe u v
29section QuotientKernelIdentityBasis
31variable {Y : Type u} [Group Y] [TopologicalSpace Y]
32variable {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
33variable (π : ∀ j : J, Y →* Q j)
35/--
36Quotient kernels form a neighborhood basis at the identity. For every open neighborhood of 1,
37some finite-stage kernel is contained in it. In a topological group this is the natural form
38obtained from finite quotient separation; it implies the left-coset basis used by
39subset_closure_of_quotientKernel_approximation.
40-/
41def HasIdentityQuotientKernelNeighbourhoodBasis : Prop :=
42 ∀ U : Set Y, IsOpen U → (1 : Y) ∈ U →
43 ∃ j : J, ∀ z : Y, z ∈ (π j).ker → z ∈ U
45/-- Identity-neighborhood quotient kernels give the left quotient-kernel basis. -/
46theorem HasIdentityQuotientKernelNeighbourhoodBasis.to_left
47 [IsTopologicalGroup Y]
48 (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π) :
49 HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π := by
50 intro y U hU hyU
51 let W : Set Y := {z : Y | y * z ∈ U}
52 have hWopen : IsOpen W := by
53 have hmul : Continuous fun z : Y => y * z :=
54 (continuous_const : Continuous fun _ : Y => y).mul continuous_id
55 exact hU.preimage hmul
56 have hWone : (1 : Y) ∈ W := by
57 simp only [Set.mem_setOf_eq, mul_one, hyU, W]
58 rcases hbasis W hWopen hWone with ⟨j, hj⟩
59 refine ⟨j, ?_⟩
60 intro z hz
61 exact hj z hz
63/-- Closure criterion using identity-neighborhood quotient kernels directly. -/
64theorem subset_closure_of_identityQuotientKernel_approximation
65 [IsTopologicalGroup Y]
66 {S T : Set Y}
67 (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
68 (happrox :
69 ∀ y : Y, y ∈ T → ∀ j : J,
70 ∃ s : Y, s ∈ S ∧ π j s = π j y) :
71 T ⊆ closure S :=
72 subset_closure_of_quotientKernel_approximation
73 (Y := Y) (S := S) (T := T) π
74 (HasIdentityQuotientKernelNeighbourhoodBasis.to_left (Y := Y) (π := π) hbasis)
75 happrox
77/--
78The closure criterion with identity-neighborhood quotient kernels can be checked at finite
79stages.
80-/
81theorem subset_closure_of_identityQuotientKernel_stage_exact
82 [IsTopologicalGroup Y]
83 {S T : Set Y}
84 (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)
85 (Sstage Tstage : ∀ j : J, Set (Q j))
86 (hTstage : ∀ y : Y, y ∈ T → ∀ j : J, π j y ∈ Tstage j)
87 (hstage_exact : ∀ j : J, Tstage j ⊆ Sstage j)
88 (hlift_stage : ∀ j : J, ∀ q : Q j, q ∈ Sstage j →
89 ∃ s : Y, s ∈ S ∧ π j s = q) :
90 T ⊆ closure S :=
91 subset_closure_of_quotientKernel_stage_exact
92 (Y := Y) (S := S) (T := T) π
93 (HasIdentityQuotientKernelNeighbourhoodBasis.to_left (Y := Y) (π := π) hbasis)
94 Sstage Tstage hTstage hstage_exact hlift_stage
96end QuotientKernelIdentityBasis
98end
100end FoxDifferential