CompletedGroupAlgebra/InClassFunctoriality/Comparison.lean

1import CompletedGroupAlgebra.InClassFunctoriality.GroupLike

2import CompletedGroupAlgebra.UniversalProperty.Basic

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/CompletedGroupAlgebra/InClassFunctoriality/Comparison.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

11-/

12/-!

13# Functoriality of completed group algebras

15The completed group algebra is presented as an inverse limit of finite group algebras, together with canonical augmentation, augmentation ideal, finite-stage maps, functoriality, and profinite module universal properties.

16-/

17open scoped Topology

19namespace CompletedGroupAlgebra

21noncomputable section

23open ProCGroups

24open ProCGroups.ProC

25open ProCGroups.InverseSystems

27universe u v w

29variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

31variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

33/-- The all-finite completed group algebra comparison sends group-like elements to the

34`C`-indexed group-like elements. -/

35@[simp]

36theorem completedGroupAlgebraToInClass_of

37 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)

38 (g : G) :

39 completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC

40 (completedGroupAlgebraOf R G g) =

41 completedGroupAlgebraOfInClass C hC R G g := by

42 change ((completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC).comp

43 (toCompletedGroupAlgebraRingHom R G)) (MonoidAlgebra.of R G g) =

44 toCompletedGroupAlgebraInClassRingHom C hC R G (MonoidAlgebra.of R G g)

45 exact congrFun

46 (congrArg DFunLike.coe

47 (completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra

48 (R := R) (G := G) C hC))

49 (MonoidAlgebra.of R G g)

51/-- The comparison map to a class-indexed completion sends all-finite augmentation generators to class-indexed generators. -/

52@[simp]

53theorem completedGroupAlgebraToInClass_of_sub_one

54 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)

55 (g : G) :

56 completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC

57 (completedGroupAlgebraOf R G g - 1) =

58 completedGroupAlgebraOfInClass C hC R G g - 1 := by

59 rw [map_sub, completedGroupAlgebraToInClass_of, map_one]

61/-- After restricting scalars along `[[R G]] -> [[R G]]_C`, the all-finite

62augmentation generator acts as the matching `C`-indexed generator. -/

63@[simp]

64theorem completedGroupAlgebraToInClass_restrictScalars_sub_one_smul

65 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)

66 (A : Type w) [AddCommGroup A] [Module (CompletedGroupAlgebraInClass C hC R G) A]

67 (g : G) (a : A) :

68 letI : Module (Carrier R G) A :=

69 Module.compHom A (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)

70 (completedGroupAlgebraOf R G g - 1) • a =

71 (completedGroupAlgebraOfInClass C hC R G g - 1) • a := by

72 letI : Module (Carrier R G) A :=

73 Module.compHom A (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)

74 change (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC

75 (completedGroupAlgebraOf R G g - 1)) • a =

76 (completedGroupAlgebraOfInClass C hC R G g - 1) • a

77 rw [completedGroupAlgebraToInClass_of_sub_one]

79/-- The comparison map from a class-indexed completion sends class-indexed group-like elements to all-finite group-like elements. -/

80@[simp]

81theorem completedGroupAlgebraFromInClass_of

82 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)

83 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (g : G) :

84 completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG

85 (completedGroupAlgebraOfInClass C hC R G g) =

86 completedGroupAlgebraOf R G g := by

87 change ((completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG).comp

88 (toCompletedGroupAlgebraInClassRingHom C hC R G)) (MonoidAlgebra.of R G g) =

89 toCompletedGroupAlgebraRingHom R G (MonoidAlgebra.of R G g)

90 exact congrFun

91 (congrArg DFunLike.coe

92 (completedGroupAlgebraFromInClassRingHom_comp_toCompletedGroupAlgebraInClass

93 (R := R) (G := G) C hC hForm hG))

94 (MonoidAlgebra.of R G g)

96/-- The comparison map from a class-indexed completion sends class-indexed augmentation generators to all-finite generators. -/

97@[simp]

98theorem completedGroupAlgebraFromInClass_of_sub_one

99 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)

100 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (g : G) :

101 completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG

102 (completedGroupAlgebraOfInClass C hC R G g - 1) =

103 completedGroupAlgebraOf R G g - 1 := by

104 change completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG

105 (completedGroupAlgebraOfInClass C hC R G g - 1) =

106 completedGroupAlgebraOf R G g - 1

107 rw [map_sub, map_one]

108 change completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG

109 (completedGroupAlgebraOfInClass C hC R G g) - 1 =

110 completedGroupAlgebraOf R G g - 1

111 rw [completedGroupAlgebraFromInClass_of]

112

113/-- After restricting scalars along `[[R G]]_C -> [[R G]]`, the `C`-indexed

114augmentation generator acts as the matching all-finite generator. -/

115@[simp]

116theorem completedGroupAlgebraFromInClass_restrictScalars_sub_one_smul

117 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)

118 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G)

119 (A : Type w) [AddCommGroup A] [Module (Carrier R G) A]

120 (g : G) (a : A) :

121 letI : Module (CompletedGroupAlgebraInClass C hC R G) A :=

122 Module.compHom A (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG)

123 (completedGroupAlgebraOfInClass C hC R G g - 1) • a =

124 (completedGroupAlgebraOf R G g - 1) • a := by

125 letI : Module (CompletedGroupAlgebraInClass C hC R G) A :=

126 Module.compHom A (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG)

127 change (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG

128 (completedGroupAlgebraOfInClass C hC R G g - 1)) • a =

129 (completedGroupAlgebraOf R G g - 1) • a

130 rw [completedGroupAlgebraFromInClassRingHom_apply,

131 completedGroupAlgebraFromInClass_of_sub_one]

132

133/-- The class-indexed functorial map sends completed group-like elements to completed group-like elements. -/

134@[simp]

135theorem completedGroupAlgebraMapInClass_of

136 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)

137 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)

138 (φ : G →* H) (hφ : Continuous φ) (g : G) :

139 completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ

140 (completedGroupAlgebraOfInClass C hC R G g) =

141 completedGroupAlgebraOfInClass C hC R H (φ g) := by

142 simpa [completedGroupAlgebraOfInClass] using

143 completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_of

144 (R := R) (G := G) (H := H) C hC hHer φ hφ g

145

146/-- The class-indexed functorial map sends group-like augmentation generators to their images. -/

147@[simp]

148theorem completedGroupAlgebraMapInClass_of_sub_one

149 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)

150 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)

151 (φ : G →* H) (hφ : Continuous φ) (g : G) :

152 completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ

153 (completedGroupAlgebraOfInClass C hC R G g - 1) =

154 completedGroupAlgebraOfInClass C hC R H (φ g) - 1 := by

155 rw [map_sub, completedGroupAlgebraMapInClass_of, map_one]

156

157end

158

159end CompletedGroupAlgebra