Source: ProCGroups.CompletedGroupAlgebra.FunctorialityComposition
1import ProCGroups.CompletedGroupAlgebra.Separation
3/-!
4# Completed Group Algebra / Functoriality Composition
6This module records compatibility of completed group algebra functoriality with composition.
7-/
9open scoped Topology
11namespace CompletedGroupAlgebra
13noncomputable section
15open ProCGroups
16open ProCGroups.ProC
17open ProCGroups.InverseSystems
18open ProCGroups.Completion
20universe u v w
22variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
23variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
26variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
28/-- Lemma 5.3.5(e), composition law for the completed-group-algebra functor. -/
29theorem completedGroupAlgebraMap_comp
30 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
31 (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
32 (completedGroupAlgebraMap (G := H) (H := K) R ψ hψ).comp
33 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ) =
34 completedGroupAlgebraMap (G := G) (H := K) R (ψ.comp φ) (hψ.comp hφ) := by
35 apply completedGroupAlgebraRingHom_ext_of_comp_toCompleted (R := R) (G := G) (H := K)
36 · exact (continuous_completedGroupAlgebraMap (R := R) (G := H) (H := K) ψ hψ).comp
37 (continuous_completedGroupAlgebraMap (R := R) (G := G) (H := H) φ hφ)
38 · exact continuous_completedGroupAlgebraMap (R := R) (G := G) (H := K)
39 (ψ.comp φ) (hψ.comp hφ)
40 · apply RingHom.ext
41 intro x
42 have hφdense := congrFun
43 (congrArg DFunLike.coe
44 (completedGroupAlgebraMap_comp_toCompletedGroupAlgebra (R := R) (G := G) (H := H)
45 φ hφ))
46 x
47 have hψdense := congrFun
48 (congrArg DFunLike.coe
49 (completedGroupAlgebraMap_comp_toCompletedGroupAlgebra (R := R) (G := H) (H := K)
50 ψ hψ))
51 (MonoidAlgebra.mapDomainRingHom R φ x)
52 have hdomain := congrFun
53 (congrArg DFunLike.coe
54 (finiteGroupAlgebra_mapDomainRingHom_comp R G H K φ ψ))
55 x
56 have hcompdense := congrFun
57 (congrArg DFunLike.coe
58 (completedGroupAlgebraMap_comp_toCompletedGroupAlgebra (R := R) (G := G) (H := K)
59 (ψ.comp φ) (hψ.comp hφ)))
60 x
61 calc
62 (((completedGroupAlgebraMap (G := H) (H := K) R ψ hψ).comp
63 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)).comp
64 (toCompletedGroupAlgebraRingHom R G)) x
65 =
66 completedGroupAlgebraMap (G := H) (H := K) R ψ hψ
67 (completedGroupAlgebraMap (G := G) (H := H) R φ hφ
68 (toCompletedGroupAlgebraRingHom R G x)) := rfl
69 _ =
70 completedGroupAlgebraMap (G := H) (H := K) R ψ hψ
71 (toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x)) := by
72 have hφdense' :
73 completedGroupAlgebraMap (G := G) (H := H) R φ hφ
74 (toCompletedGroupAlgebraRingHom R G x) =
75 toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x) := by
76 simpa [RingHom.comp_apply] using hφdense
77 exact congrArg (completedGroupAlgebraMap (G := H) (H := K) R ψ hψ) hφdense'
78 _ =
79 toCompletedGroupAlgebraRingHom R K
80 (MonoidAlgebra.mapDomainRingHom R ψ (MonoidAlgebra.mapDomainRingHom R φ x)) := by
81 simpa [RingHom.comp_apply] using hψdense
82 _ =
83 toCompletedGroupAlgebraRingHom R K
84 (MonoidAlgebra.mapDomainRingHom R (ψ.comp φ) x) := by
85 exact congrArg (toCompletedGroupAlgebraRingHom R K) (by
86 change (MonoidAlgebra.mapDomainRingHom R ψ)
87 ((MonoidAlgebra.mapDomainRingHom R φ) x) =
88 (MonoidAlgebra.mapDomainRingHom R (ψ.comp φ)) x at hdomain
89 exact hdomain)
90 _ =
91 ((completedGroupAlgebraMap (G := G) (H := K) R (ψ.comp φ) (hψ.comp hφ)).comp
92 (toCompletedGroupAlgebraRingHom R G)) x := by
93 simpa [RingHom.comp_apply] using hcompdense.symm
95/--
96Lemma 5.3.5(e), composition law for the completed-group-algebra functor, as an \(R\)-algebra
97homomorphism.
98-/
99theorem completedGroupAlgebraMapAlgHom_comp
100 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
101 (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
102 (completedGroupAlgebraMapAlgHom (G := H) (H := K) R ψ hψ).comp
103 (completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ) =
104 completedGroupAlgebraMapAlgHom (G := G) (H := K) R (ψ.comp φ) (hψ.comp hφ) := by
105 apply AlgHom.ext
106 intro x
107 have h := congrFun
108 (congrArg DFunLike.coe
109 (completedGroupAlgebraMap_comp (R := R) (G := G) (H := H) (K := K)
110 φ hφ ψ hψ))
111 x
112 simpa [RingHom.comp_apply] using h
113end
115end CompletedGroupAlgebra