Source: ProCGroups.FreeProC.Universe
1import ProCGroups.FreeProC.Basic
3/-!
4# Universe-polymorphic targets for free pro-\(C\) groups
6The original IsFreeProCGroup API keeps the source, free group, finite-group class, and target in
7one universe. This module factors the universal property for one fixed target into
8HasFreeLiftTo, then supplies an explicit extension whose target lives in an independent
9universe. Cross-universe membership is expressed by FiniteGroupClass.MemAcrossUniverses, so no
10ULift appears in the public universal property.
12An ordinary IsFreeProCGroup yields this extension only in its native target universe. There is
13deliberately no theorem promoting it to every target universe: such a promotion is not a
14consequence of the same-universe universal property.
15-/
17open Set
18open scoped Topology
20namespace ProCGroups.FreeProC
22universe u v
24open ProCGroups
26variable {C : FiniteGroupClass.{u}}
28/-- The universal extension property from F to one fixed pro-\(C\) target G.
30Keeping this target-specific property separate lets constructions prove exactly the
31cross-universe lifting statement they support, without claiming a nonexistent automatic
32promotion from the native universal property. -/
33def HasFreeLiftTo
34 {X : Type u} [TopologicalSpace X]
35 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
36 (ι : X → F)
37 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
38 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : Prop :=
39 ProC.HasOpenNormalBasisInClassAcrossUniverses C G →
40 ∀ (φ : X → G), Continuous φ →
41 ∃! f : F →* G, Continuous f ∧ ∀ x, f (ι x) = φ x
43namespace HasFreeLiftTo
45variable {X : Type u} [TopologicalSpace X]
46variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
47variable {ι : X → F}
48variable {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
49variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
51/-- Extend a continuous generator map to the fixed target. -/
52noncomputable def lift (h : HasFreeLiftTo (C := C) ι G)
53 (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
54 (φ : X → G) (hφ : Continuous φ) : F →* G :=
55 Classical.choose (ExistsUnique.exists (h hG φ hφ))
57/-- The fixed-target lift is continuous and has the prescribed generator values. -/
58theorem lift_spec (h : HasFreeLiftTo (C := C) ι G)
59 (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
60 (φ : X → G) (hφ : Continuous φ) :
61 Continuous (h.lift hG φ hφ) ∧ ∀ x, h.lift hG φ hφ (ι x) = φ x :=
62 Classical.choose_spec (ExistsUnique.exists (h hG φ hφ))
64/-- The fixed-target lift is unique among continuous homomorphisms with the prescribed values. -/
65theorem lift_unique (h : HasFreeLiftTo (C := C) ι G)
66 (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
67 (φ : X → G) (hφ : Continuous φ)
68 {f : F →* G} (hf : Continuous f) (hfac : ∀ x, f (ι x) = φ x) :
69 f = h.lift hG φ hφ :=
70 (h hG φ hφ).unique ⟨hf, hfac⟩ (h.lift_spec hG φ hφ)
72/-- Bundle the fixed-target lift as a continuous monoid homomorphism. -/
73noncomputable def liftHom (h : HasFreeLiftTo (C := C) ι G)
74 (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
75 (φ : X → G) (hφ : Continuous φ) : F →ₜ* G where
76 toMonoidHom := h.lift hG φ hφ
77 continuous_toFun := (h.lift_spec hG φ hφ).1
79end HasFreeLiftTo
81/-- The free pro-\(C\) universal property for targets in an explicitly independent universe.
83Lean cannot quantify over universe levels inside a proposition, so the target universe v is a
84universe parameter of this structure. The native universal property is retained as a parent, so
85this stronger witness is directly usable anywhere an IsFreeProCGroup is expected. -/
86structure IsFreeProCGroupForTargetUniverse
87 {X : Type u} [TopologicalSpace X]
88 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
89 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
90 (ι : X → F) : Prop extends IsFreeProCGroup (C := C) ι where
91 /--
92 For every pro-`C` target in universe `v`, continuous maps from `X` extend uniquely to
93 continuous homomorphisms from `F`.
94 -/
95 hasFreeLiftTo :
96 ∀ {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
97 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G],
98 HasFreeLiftTo (C := C) ι G
100namespace IsFreeProCGroupForTargetUniverse
102variable {X : Type u} [TopologicalSpace X]
103variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
104variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
105variable {ι : X → F}
107/-- Extend a continuous generator map to a homomorphism into a target in the chosen target
108universe. -/
109noncomputable def lift (hι : IsFreeProCGroupForTargetUniverse.{u, v} (C := C) ι)
110 {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
111 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
112 (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
113 (φ : X → G) (hφ : Continuous φ) : F →* G :=
114 (hι.hasFreeLiftTo (G := G)).lift hG φ hφ
116/-- The cross-universe lift is continuous and has the prescribed generator values. -/
117theorem lift_spec (hι : IsFreeProCGroupForTargetUniverse.{u, v} (C := C) ι)
118 {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
119 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
120 (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
121 (φ : X → G) (hφ : Continuous φ) :
122 Continuous (hι.lift hG φ hφ) ∧
123 ∀ x, hι.lift hG φ hφ (ι x) = φ x :=
124 (hι.hasFreeLiftTo (G := G)).lift_spec hG φ hφ
126/-- The cross-universe lift is unique among continuous homomorphisms with the prescribed values. -/
127theorem lift_unique (hι : IsFreeProCGroupForTargetUniverse.{u, v} (C := C) ι)
128 {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
129 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
130 (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
131 (φ : X → G) (hφ : Continuous φ)
132 {f : F →* G} (hf : Continuous f) (hfac : ∀ x, f (ι x) = φ x) :
133 f = hι.lift hG φ hφ := by
134 exact (hι.hasFreeLiftTo (G := G)).lift_unique hG φ hφ hf hfac
136/-- Bundle the cross-universe lift as a continuous monoid homomorphism. -/
137noncomputable def liftHom (hι : IsFreeProCGroupForTargetUniverse.{u, v} (C := C) ι)
138 {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
139 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
140 (hG : ProC.HasOpenNormalBasisInClassAcrossUniverses C G)
141 (φ : X → G) (hφ : Continuous φ) : F →ₜ* G where
142 toMonoidHom := hι.lift hG φ hφ
143 continuous_toFun := (hι.lift_spec hG φ hφ).1
145end IsFreeProCGroupForTargetUniverse
147namespace IsFreeProCGroup
149variable {X : Type u} [TopologicalSpace X]
150variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
151variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
152variable {ι : X → F}
154/-- The ordinary universal property, viewed as a fixed-target property in its native universe. -/
155theorem hasFreeLiftTo (hι : IsFreeProCGroup (C := C) ι)
156 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
157 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
158 HasFreeLiftTo (C := C) ι G := by
159 intro hG φ hφ
160 exact hι.existsUnique_lift
161 (ProC.hasOpenNormalBasisInClassAcrossUniverses_iff.1 hG) φ hφ
163/-- In the native target universe, the original property yields the explicit
164target-universe property. -/
165theorem toForTargetUniverse (hι : IsFreeProCGroup (C := C) ι) :
166 IsFreeProCGroupForTargetUniverse.{u, u} (C := C) ι where
167 toIsFreeProCGroup := hι
168 hasFreeLiftTo := hι.hasFreeLiftTo
170end IsFreeProCGroup
172end ProCGroups.FreeProC