Source: ProCGroups.FoxDifferential.Completed.Continuous.Free.DiscreteGenerators
1import ProCGroups.FoxDifferential.Completed.Continuous.Free.CanonicalFormula
2import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Existence
4/-!
5# Fox differential: completed — continuous — free — discrete generators
7The principal declarations in this module are:
9- `existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_of_discreteGenerators`
10 Continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique for
11 discrete generators, without a separate generator-continuity hypothesis.
12- `existsUnique_freeProCZCFoxSemiLiftHom_components_of_discreteGenerators`
13 Componentwise continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are
14 unique for discrete generators, without a separate generator-continuity hypothesis.
15- `existsUnique_freeProCZCCompletedFoxSemidirectLift_of_discreteGenerators`
16 Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique for discrete
17 generators, without a separate generator-continuity hypothesis.
18- `existsUnique_freeProCZCFoxSemiLift_components_of_discreteGenerators`
19 Componentwise continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique
20 for discrete generators, without a separate generator-continuity hypothesis.
21-/
23namespace FoxDifferential
25noncomputable section
27open scoped BigOperators
29universe u
32variable {C : ProCGroups.FiniteGroupClass.{u}}
33variable (X H : Type u) [DecidableEq X]
34variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
37variable {F : Type u}
38variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
39variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
40variable [TopologicalSpace X]
42variable [DiscreteTopology X]
44section ProfiniteTarget
46variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
47variable [T2Space (ZCCompletedFoxSemidirect C X H)]
48variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
50/--
51Continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique for
52discrete generators, without a separate generator-continuity hypothesis.
53-/
54theorem existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_of_discreteGenerators
55 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
56 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
57 (φ : X → H) :
58 ∃! f : F →ₜ* ZCCompletedFoxSemidirect C X H,
59 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x :=
60 existsUnique_freeProCZCCompletedFoxSemidirectLiftHom
61 (C := C) hι htarget φ
62 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)
64/--
65Componentwise continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are
66unique for discrete generators, without a separate generator-continuity hypothesis.
67-/
68theorem existsUnique_freeProCZCFoxSemiLiftHom_components_of_discreteGenerators
69 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
70 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
71 (φ : X → H) :
72 ∃! f : F →ₜ* ZCCompletedFoxSemidirect C X H,
73 (∀ x : X, (f (ι x)).left =
74 Pi.single x (1 : ZCCompletedGroupAlgebra C H)) ∧
75 ∀ x : X, (f (ι x)).right = φ x :=
76 existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_components
77 (C := C) hι htarget φ
78 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)
80/--
81Continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique for discrete
82generators, without a separate generator-continuity hypothesis.
83-/
84theorem existsUnique_freeProCZCCompletedFoxSemidirectLift_of_discreteGenerators
85 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
86 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
87 (φ : X → H) :
88 ∃! f : F →* ZCCompletedFoxSemidirect C X H,
89 Continuous f ∧
90 ∀ x : X, f (ι x) =
91 freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x :=
92 existsUnique_freeProCZCCompletedFoxSemidirectLift
93 (C := C) hι htarget φ
94 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)
96/--
97Componentwise continuous completed Fox semidirect lifts from a free pro-\(C\) source are unique
98for discrete generators, without a separate generator-continuity hypothesis.
99-/
100theorem existsUnique_freeProCZCFoxSemiLift_components_of_discreteGenerators
101 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
102 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
103 (φ : X → H) :
104 ∃! f : F →* ZCCompletedFoxSemidirect C X H,
105 Continuous f ∧
106 (∀ x : X, (f (ι x)).left =
107 Pi.single x (1 : ZCCompletedGroupAlgebra C H)) ∧
108 ∀ x : X, (f (ι x)).right = φ x :=
109 existsUnique_freeProCZCCompletedFoxSemidirectLift_components
110 (C := C) hι htarget φ
111 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)
113end ProfiniteTarget
116end
118end FoxDifferential