Source: ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Existence
1import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Lift
2import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Morphism
4/-!
5# Fox differential: completed — free pro-\(C\) — uniqueness — existence
7The principal declarations in this module are:
9- `existsUnique_freeProCZCCompletedFoxSemidirectLift`
10 Existence and uniqueness of the continuous completed Fox semidirect lift from a free pro-\(C\)
11 source.
12- `existsUnique_freeProCZCCompletedFoxSemidirectLift_components`
13 Componentwise existence and uniqueness of the continuous completed Fox semidirect lift from a free
14 pro-\(C\) source.
15-/
17namespace FoxDifferential
19noncomputable section
21open ProCGroups.FreeProC
23universe u
26variable {C : ProCGroups.FiniteGroupClass.{u}}
27variable {X F H : Type u}
28variable [TopologicalSpace X]
29variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
30variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
31variable [DecidableEq X]
32variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
34variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
36section ProfiniteTarget
38variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
39variable [T2Space (ZCCompletedFoxSemidirect C X H)]
40variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
42/--
43Existence and uniqueness of the continuous completed Fox semidirect lift from a free pro-\(C\)
44source.
45-/
46theorem existsUnique_freeProCZCCompletedFoxSemidirectLift
47 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
48 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
49 (φ : X → H)
50 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
51 ∃! f : F →* ZCCompletedFoxSemidirect C X H,
52 Continuous f ∧
53 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x :=
54 hι.existsUnique_lift htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) hφ
56/--
57Componentwise existence and uniqueness of the continuous completed Fox semidirect lift from a
58free pro-\(C\) source.
59-/
60theorem existsUnique_freeProCZCCompletedFoxSemidirectLift_components
61 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
62 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
63 (φ : X → H)
64 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
65 ∃! f : F →* ZCCompletedFoxSemidirect C X H,
66 Continuous f ∧
67 (∀ x : X, (f (ι x)).left =
68 Pi.single x (1 : ZCCompletedGroupAlgebra C H)) ∧
69 ∀ x : X, (f (ι x)).right = φ x := by
70 refine ⟨freeProCZCCompletedFoxSemidirectLift
71 (C := C) hι htarget φ hφ, ?_, ?_⟩
72 · exact ⟨
73 continuous_freeProCZCCompletedFoxSemidirectLift
74 (C := C) hι htarget φ hφ,
75 freeProCZCCompletedFoxSemidirectLift_left_generator
76 (C := C) hι htarget φ hφ,
77 freeProCZCCompletedFoxSemidirectLift_right_generator
78 (C := C) hι htarget φ hφ⟩
79 · intro f hf
80 exact freeProCZCCompletedFoxSemidirectLift_unique_of_components
81 (C := C) hι htarget φ hφ f hf.1 hf.2.1 hf.2.2
83end ProfiniteTarget
85end
87end FoxDifferential