FoxDifferential/Completed/DifferentialModule/Map/Comap.lean
1import FoxDifferential.Completed.DifferentialModule.Identity
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/DifferentialModule/Map/Comap.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed differential modules
14The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups
21open ProCGroups.ProC
23universe u v
25variable (ℓ : ℕ) [Fact (0 < ℓ)]
26variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
27variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
29/-- Definition of completedGroupAlgebraComapIndex. -/
30def completedGroupAlgebraComapIndex
31 (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
32 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G := by
33 let V : OpenNormalSubgroup H := (OrderDual.ofDual U).1
34 let W : OpenNormalSubgroup G := OpenNormalSubgroup.comap ψ.toMonoidHom ψ.continuous_toFun V
35 refine OrderDual.toDual ⟨W, ?_⟩
36 let q : G →* H ⧸ (V : Subgroup H) :=
37 (QuotientGroup.mk' (V : Subgroup H)).comp ψ.toMonoidHom
38 let f : G ⧸ (W : Subgroup G) → H ⧸ (V : Subgroup H) :=
39 QuotientGroup.map _ _ ψ.toMonoidHom (by
40 intro g hg
41 simpa [W] using hg)
42 have hf : Function.Injective f := by
43 intro x y hxy
44 rcases QuotientGroup.mk'_surjective (W : Subgroup G) x with ⟨a, rfl⟩
45 rcases QuotientGroup.mk'_surjective (W : Subgroup G) y with ⟨b, rfl⟩
46 apply QuotientGroup.eq.2
47 change ψ (a⁻¹ * b) ∈ (V : Subgroup H)
48 have hv : (ψ a)⁻¹ * ψ b ∈ (V : Subgroup H) := QuotientGroup.eq.1 hxy
49 simpa using hv
50 letI : Finite (H ⧸ (V : Subgroup H)) := (OrderDual.ofDual U).2
51 exact Finite.of_injective f hf
53omit [IsTopologicalGroup G] in
54/-- 標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
55@[simp]
56theorem completedGroupAlgebraComapIndex_subgroup
57 (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
58 (((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U)).1 :
59 OpenNormalSubgroup G) : Subgroup G) =
60 Subgroup.comap ψ.toMonoidHom
61 (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H) := by
62 rfl
64/-- Definition of completedGroupAlgebraComapQuotientMap. -/
65def completedGroupAlgebraComapQuotientMap
66 (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
67 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
68 (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U) →*
69 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H U :=
70 QuotientGroup.map _ _ ψ.toMonoidHom (by
71 intro g hg
72 simpa [completedGroupAlgebraComapIndex] using hg)
74/-- Evaluation formula for completedGroupAlgebraComapQuotientMap_mk. -/
75@[simp]
76theorem completedGroupAlgebraComapQuotientMap_mk
77 (ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) (g : G) :
78 completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U
79 (QuotientGroup.mk' _ g) =
80 QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H) (ψ g) := by
81 rfl
84/-- If `ψ : G → H` is surjective, the induced map from the pulled-back finite quotient
86lift coefficients in the completed free-derivative construction. -/
87theorem completedGroupAlgebraComapQuotientMap_surjective
88 (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
89 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
90 Function.Surjective
91 (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U) := by
92 intro q
93 rcases QuotientGroup.mk'_surjective
94 ((((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)) q with
95 ⟨h, rfl⟩
96 rcases hψ h with ⟨g, rfl⟩
97 refine ⟨QuotientGroup.mk'
98 ((((OrderDual.ofDual
99 (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U)).1 :
100 OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
101 rw [completedGroupAlgebraComapQuotientMap_mk]
103omit [IsTopologicalGroup G] in
104/-- 標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
105theorem completedGroupAlgebraComapIndex_mono
106 (ψ : ContinuousMonoidHom G H) {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H} (hUV : U ≤ V) :
107 completedGroupAlgebraComapIndex (G := G) (H := H) ψ U ≤
108 completedGroupAlgebraComapIndex (G := G) (H := H) ψ V := by
109 change
110 Subgroup.comap ψ.toMonoidHom
111 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H) ≤
112 Subgroup.comap ψ.toMonoidHom
113 (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)
114 exact Subgroup.comap_mono hUV
116/-- Compatibility lemma completedGroupAlgebraComapQuotientMap_compatible. -/
117@[simp]
119 (ψ : ContinuousMonoidHom G H) {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H} (hUV : U ≤ V) :
120 (OpenNormalSubgroupInClass.map
121 (C := ProCGroups.FiniteGroupClass.allFinite) (G := H)
122 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV).comp
123 (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ V) =
124 (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U).comp
125 (OpenNormalSubgroupInClass.map
126 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
127 (U := OrderDual.ofDual
128 (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U))
129 (V := OrderDual.ofDual
130 (completedGroupAlgebraComapIndex (G := G) (H := H) ψ V))
131 (completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hUV)) := by
132 ext q
133 rcases QuotientGroup.mk'_surjective
134 ((((OrderDual.ofDual
135 (completedGroupAlgebraComapIndex (G := G) (H := H) ψ V)).1 :
136 OpenNormalSubgroup G) : Subgroup G)) q with ⟨g, rfl⟩
137 rfl
139end
141end FoxDifferential