CompletedGroupAlgebra/AllFiniteFunctoriality/Comap.lean
1import CompletedGroupAlgebra.Augmentation.Functoriality
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/AllFiniteFunctoriality/Comap.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
13-/
15open scoped Topology
17namespace CompletedGroupAlgebra
19noncomputable section
21open ProCGroups
22open ProCGroups.ProC
24universe u v w
26variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
27variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28variable {H : Type v} [Group H] [TopologicalSpace H]
30/-- The inverse image of an open finite quotient of `H` along a continuous homomorphism
32index-level operation underlying Lemma 5.3.5(e)'s functoriality in the group variable. -/
33def completedGroupAlgebraComapIndex
34 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
35 (V : CompletedGroupAlgebraIndex H) : CompletedGroupAlgebraIndex G :=
36 OrderDual.toDual
37 ⟨ProCGroups.OpenNormalSubgroup.comap φ hφ ((OrderDual.ofDual V).1 : OpenNormalSubgroup H), by
38 letI : CompactSpace G := ProCGroups.IsProfiniteGroup.compactSpace hG
39 exact ProCGroups.openNormalSubgroup_finiteQuotient (G := G)
40 (ProCGroups.OpenNormalSubgroup.comap φ hφ ((OrderDual.ofDual V).1 : OpenNormalSubgroup H))⟩
42/-- The subgroup underlying the comap index is the subgroup-theoretic comap. -/
43@[simp]
44theorem completedGroupAlgebraComapIndex_subgroup
45 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
46 (V : CompletedGroupAlgebraIndex H) :
47 (((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)).1 :
48 OpenNormalSubgroup G) : Subgroup G) =
49 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ :=
50 rfl
52/-- Comap of all-finite completed-group-algebra indices is monotone. -/
53theorem completedGroupAlgebraComapIndex_mono
54 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
55 {V W : CompletedGroupAlgebraIndex H} (hVW : V ≤ W) :
56 completedGroupAlgebraComapIndex (G := G) hG φ hφ V ≤
57 completedGroupAlgebraComapIndex (G := G) hG φ hφ W := by
58 change (((OrderDual.ofDual W).1 : OpenNormalSubgroup H) : Subgroup H).comap φ ≤
59 (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ
60 exact Subgroup.comap_mono hVW
62/-- The quotient homomorphism `G/φ⁻¹(V) -> H/V` induced by a continuous homomorphism
63`φ : G -> H`. -/
64def completedGroupAlgebraComapQuotientMap
65 [IsTopologicalGroup H]
66 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
67 (V : CompletedGroupAlgebraIndex H) :
68 CompletedGroupAlgebraQuotient G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) →*
69 CompletedGroupAlgebraQuotient H V :=
70 QuotientGroup.map _ _ φ (by
71 intro g hg
72 exact hg)
74/-- The comap quotient map sends the class of `g` to the class of its image. -/
75@[simp]
76theorem completedGroupAlgebraComapQuotientMap_mk
77 [IsTopologicalGroup H]
78 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
79 (V : CompletedGroupAlgebraIndex H) (g : G) :
80 completedGroupAlgebraComapQuotientMap (G := G) hG φ hφ V
81 (QuotientGroup.mk'
82 ((((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)).1 :
83 OpenNormalSubgroup G) : Subgroup G)) g) =
84 QuotientGroup.mk'
85 ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H)) (φ g) :=
86 rfl
88/-- A surjective homomorphism induces a surjective map on the comap quotients. -/
89theorem completedGroupAlgebraComapQuotientMap_surjective
90 [IsTopologicalGroup H]
91 (hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
92 (hφsurj : Function.Surjective φ) (V : CompletedGroupAlgebraIndex H) :
93 Function.Surjective (completedGroupAlgebraComapQuotientMap (G := G) hG φ hφ V) := by
94 intro q
95 rcases QuotientGroup.mk'_surjective
96 ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H)) q with
97 ⟨h, rfl⟩
98 rcases hφsurj h with ⟨g, rfl⟩
99 refine ⟨QuotientGroup.mk'
100 ((((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)).1 :
101 OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
102 rw [completedGroupAlgebraComapQuotientMap_mk]
104end