Source: ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Surjective
1import ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Limit
3/-!
4# Fox differential: completed — differential module — map — surjective
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraMapLiftOfSurjective`
9 A choice of a lift along the surjective completed group-algebra map \(\Lambda_G \to \Lambda_H\),
10 independent of the displayed differential premodule topology.
11- `primePowerCompletedGroupAlgebraMap_surjective`
12 If \(\psi : G \to H\) is surjective, then the induced map of prime-power completed group algebras
13 is surjective.
14- `primePowerCompletedGroupAlgebraMap_liftOfSurjective`
15 The chosen lift maps back to the target coefficient.
16-/
18namespace FoxDifferential
20noncomputable section
22open ProCGroups
23open ProCGroups.ProC
25universe u v
27variable (ℓ : ℕ) [Fact (0 < ℓ)]
28variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
31/--
32If \(\psi : G \to H\) is surjective, then the induced map of prime-power completed group
33algebras is surjective.
34-/
35theorem primePowerCompletedGroupAlgebraMap_surjective
36 (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ) :
37 Function.Surjective
38 (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ) := by
39 classical
40 let S := primePowerCompletedGroupAlgebraSystem ℓ H
41 let T := primePowerCompletedGroupAlgebraSystem ℓ G
42 let f : PrimePowerCompletedGroupAlgebra ℓ G → PrimePowerCompletedGroupAlgebra ℓ H :=
43 primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
44 letI : Nonempty (PrimePowerCompletedGroupAlgebraIndex H) :=
45 ⟨(0, _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex H)⟩
46 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, TopologicalSpace (S.X i) :=
47 fun i => S.topologicalSpace i
48 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, DiscreteTopology (S.X i) :=
49 fun _ => ⟨rfl⟩
50 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, CompactSpace (S.X i) :=
51 fun i => by
52 letI : Finite (S.X i) := by
53 dsimp [S, primePowerCompletedGroupAlgebraSystem]
54 infer_instance
55 letI : Fintype (S.X i) := Fintype.ofFinite _
56 infer_instance
57 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, T2Space (S.X i) :=
58 fun _ => inferInstance
59 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, TopologicalSpace (T.X i) :=
60 fun i => T.topologicalSpace i
61 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, DiscreteTopology (T.X i) :=
62 fun _ => ⟨rfl⟩
63 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, CompactSpace (T.X i) :=
64 fun i => by
65 letI : Finite (T.X i) := by
66 dsimp [T, primePowerCompletedGroupAlgebraSystem]
67 infer_instance
68 letI : Fintype (T.X i) := Fintype.ofFinite _
69 infer_instance
70 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, T2Space (T.X i) :=
71 fun _ => inferInstance
72 letI : CompactSpace (PrimePowerCompletedGroupAlgebra ℓ G) :=
73 inferInstance
74 letI : T2Space (PrimePowerCompletedGroupAlgebra ℓ H) :=
75 S.t2Space_inverseLimit
76 have hf_continuous : Continuous f :=
77 continuous_primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
78 have hclosed : IsClosed (Set.range f) :=
79 (isCompact_range hf_continuous).isClosed
80 have hprojection_images :
81 ∀ i : PrimePowerCompletedGroupAlgebraIndex H,
82 S.projection i '' Set.range f =
83 S.projection i '' (Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H)) := by
84 intro i
85 apply Set.Subset.antisymm
86 · rintro z ⟨y, _hy, rfl⟩
87 exact ⟨y, trivial, rfl⟩
88 · rintro z ⟨y, _hy, rfl⟩
89 rcases primePowerCompletedGroupAlgebraMapStage_surjective
90 (ℓ := ℓ) (G := G) (H := H) ψ hψ i (S.projection i y) with
91 ⟨c, hc⟩
92 let sourceIndex : PrimePowerCompletedGroupAlgebraIndex G :=
93 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)
94 rcases primePowerCompletedGroupAlgebraProjection_surjective
95 (ℓ := ℓ) (G := G) sourceIndex c with
96 ⟨x, hx⟩
97 refine ⟨f x, ⟨x, rfl⟩, ?_⟩
98 change primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := H) i
99 (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ x) =
100 S.projection i y
101 rw [primePowerCompletedGroupAlgebraProjection_map]
102 change primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
103 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) sourceIndex x) =
104 S.projection i y
105 rw [hx, hc]
106 have hclosure :
107 closure (Set.range f) =
108 (Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H)) := by
109 have hclosure' :
110 closure (Set.range f) =
111 closure (Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H)) :=
112 S.closure_eq_of_projection_images_eq_of_subsets
113 (directed_primePowerCompletedGroupAlgebraIndex (G := H))
114 (Set.range f)
115 (Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H))
116 hprojection_images
117 simpa using hclosure'
118 intro y
119 have hy_closure : y ∈ closure (Set.range f) := by
120 rw [hclosure]
121 simp only [Set.mem_univ]
122 have hy_range : y ∈ Set.range f := by
123 rwa [hclosed.closure_eq] at hy_closure
124 rcases hy_range with ⟨x, hx⟩
125 exact ⟨x, hx⟩
127/--
128A choice of a lift along the surjective completed group-algebra map \(\Lambda_G \to \Lambda_H\),
129independent of the displayed differential premodule topology.
130-/
131def primePowerCompletedGroupAlgebraMapLiftOfSurjective
132 (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
133 (a : PrimePowerCompletedGroupAlgebra ℓ H) :
134 PrimePowerCompletedGroupAlgebra ℓ G :=
135 Classical.choose
136 (primePowerCompletedGroupAlgebraMap_surjective
137 (ℓ := ℓ) (G := G) (H := H) ψ hψ a)
139/-- The chosen lift maps back to the target coefficient. -/
140@[simp]
141theorem primePowerCompletedGroupAlgebraMap_liftOfSurjective
142 (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
143 (a : PrimePowerCompletedGroupAlgebra ℓ H) :
144 primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
145 (primePowerCompletedGroupAlgebraMapLiftOfSurjective
146 (ℓ := ℓ) (G := G) (H := H) ψ hψ a) = a :=
147 Classical.choose_spec
148 (primePowerCompletedGroupAlgebraMap_surjective
149 (ℓ := ℓ) (G := G) (H := H) ψ hψ a)
151end
153end FoxDifferential