Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Comap
ProCGroups/FoxDifferential/Completed/DifferentialModule/Map/Comap/Source

Source: ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Comap

1import ProCGroups.FoxDifferential.Completed.DifferentialModule.Identity
3/-!
4# Fox differential: completed — differential module — map — comap
6The principal declarations in this module are:
8- `completedGroupAlgebraComapIndex`
9 The index map that sends a target finite quotient to its pullback finite quotient on the source.
10- `completedGroupAlgebraComapQuotientMap`
11 The quotient map from the pulled-back source quotient to the target quotient induced by the
12 original homomorphism.
13- `completedGroupAlgebraComapIndex_subgroup`
14 The subgroup underlying the comap index is the subgroup-theoretic comap.
15- `completedGroupAlgebraComapQuotientMap_mk`
16 The pullback quotient map sends the class of a source element to the class of its image in the
17 target quotient in the Fox differential construction.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups
25open ProCGroups.ProC
27universe u v
29variable (ℓ : ℕ) [Fact (0 < ℓ)]
30variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33/--
34The index map that sends a target finite quotient to its pullback finite quotient on the source.
35-/
36def completedGroupAlgebraComapIndex
37 (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
38 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G := by
39 let V : OpenNormalSubgroup H := (OrderDual.ofDual U).1
40 let W : OpenNormalSubgroup G := OpenNormalSubgroup.comap ψ.toMonoidHom ψ.continuous_toFun V
41 refine OrderDual.toDual ⟨W, ?_⟩
42 let q : G →* H ⧸ (V : Subgroup H) :=
43 (QuotientGroup.mk' (V : Subgroup H)).comp ψ.toMonoidHom
44 let f : G ⧸ (W : Subgroup G) → H ⧸ (V : Subgroup H) :=
45 QuotientGroup.map _ _ ψ.toMonoidHom (by
46 intro g hg
47 simpa [W] using hg)
48 have hf : Function.Injective f := by
49 intro x y hxy
50 rcases QuotientGroup.mk'_surjective (W : Subgroup G) x with ⟨a, rfl⟩
51 rcases QuotientGroup.mk'_surjective (W : Subgroup G) y with ⟨b, rfl⟩
52 apply QuotientGroup.eq.2
53 change ψ (a⁻¹ * b) ∈ (V : Subgroup H)
54 have hv : (ψ a)⁻¹ * ψ b ∈ (V : Subgroup H) := QuotientGroup.eq.1 hxy
55 simpa using hv
56 letI : Finite (H ⧸ (V : Subgroup H)) := (OrderDual.ofDual U).2
57 exact Finite.of_injective f hf
59omit [IsTopologicalGroup G] in
60/-- The subgroup underlying the comap index is the subgroup-theoretic comap. -/
61@[simp]
62theorem completedGroupAlgebraComapIndex_subgroup
63 (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
64 (((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U)).1 :
65 OpenNormalSubgroup G) : Subgroup G) =
66 Subgroup.comap ψ.toMonoidHom
67 (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H) := by
68 rfl
70/--
71The quotient map from the pulled-back source quotient to the target quotient induced by the
72original homomorphism.
73-/
74def completedGroupAlgebraComapQuotientMap
75 (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
76 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
77 (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U) →*
78 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H U :=
79 QuotientGroup.map _ _ ψ.toMonoidHom (by
80 intro g hg
81 simpa [completedGroupAlgebraComapIndex] using hg)
83/--
84The pullback quotient map sends the class of a source element to the class of its image in the
85target quotient in the Fox differential construction.
86-/
87@[simp]
88theorem completedGroupAlgebraComapQuotientMap_mk
89 (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex
90 H) (g : G) :
91 completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U
92 (QuotientGroup.mk' _ g) =
93 QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H) (ψ g) := by
94 rfl
97/--
98If \(\psi : G \to H\) is surjective, the induced map from the pulled-back finite quotient \(G /
99\psi^{-1}(U)\) to \(H / U\) is surjective. This is the finite-quotient input used later to lift
100coefficients in the completed free-derivative construction.
101-/
102theorem completedGroupAlgebraComapQuotientMap_surjective
103 (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
104 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
105 Function.Surjective
106 (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U) := by
107 intro q
108 rcases QuotientGroup.mk'_surjective
109 ((((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)) q with
110 ⟨h, rfl⟩
111 rcases hψ h with ⟨g, rfl⟩
112 refine ⟨QuotientGroup.mk'
113 ((((OrderDual.ofDual
114 (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U)).1 :
115 OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
116 rw [completedGroupAlgebraComapQuotientMap_mk]
118omit [IsTopologicalGroup G] in
119/-- Comap of all-finite completed-group-algebra indices is monotone. -/
120theorem completedGroupAlgebraComapIndex_mono
121 (ψ : ContinuousMonoidHom G H) {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex
122 H} (hUV : U ≤ V) :
123 completedGroupAlgebraComapIndex (G := G) (H := H) ψ U ≤
124 completedGroupAlgebraComapIndex (G := G) (H := H) ψ V := by
125 change
126 Subgroup.comap ψ.toMonoidHom
127 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H) ≤
128 Subgroup.comap ψ.toMonoidHom
129 (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)
130 exact Subgroup.comap_mono hUV
132/-- The comap quotient maps are compatible with refinement of finite quotients. -/
133@[simp]
134theorem completedGroupAlgebraComapQuotientMap_compatible
135 (ψ : ContinuousMonoidHom G H) {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex
136 H} (hUV : U ≤ V) :
137 (OpenNormalSubgroupInClass.map
139 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV).comp
140 (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ V) =
141 (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U).comp
142 (OpenNormalSubgroupInClass.map
144 (U := OrderDual.ofDual
145 (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U))
146 (V := OrderDual.ofDual
147 (completedGroupAlgebraComapIndex (G := G) (H := H) ψ V))
148 (completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hUV)) := by
149 ext q
150 rcases QuotientGroup.mk'_surjective
151 ((((OrderDual.ofDual
152 (completedGroupAlgebraComapIndex (G := G) (H := H) ψ V)).1 :
153 OpenNormalSubgroup G) : Subgroup G)) q with ⟨g, rfl⟩
154 rfl
156end
158end FoxDifferential