Source: ProCGroups.CompletedGroupAlgebra.Augmentation.Functoriality
1import ProCGroups.CompletedGroupAlgebra.Augmentation.AugmentationIdeal
3/-!
4# Functoriality of augmentation
6Maps of in-class completed group algebras commute with canonical augmentation. This file derives
7the corresponding comap and image formulas for augmentation ideals, including the surjective
8case.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
19open ProCGroups.InverseSystems
20open ProCGroups.Completion
22universe u v w
24variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
25variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
26variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
28/-- The in-class canonical augmentation is natural under functorial completed maps. -/
29@[simp 900]
30theorem completedGroupAlgebraCanonicalAugmentationInClass_map
31 (C : ProCGroups.FiniteGroupClass.{v})
33 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
34 (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C R G) :
35 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C
36 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x) =
37 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C x := by
38 let V : CompletedGroupAlgebraIndexInClass H C :=
39 terminalCompletedGroupAlgebraIndexInClass (G := H) C
40 calc
41 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C
42 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x)
43 =
44 completedGroupAlgebraAugmentationAtInClass C R H V
45 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x) := by
46 exact completedGroupAlgebraCanonicalAugmentationInClass_eq_at
47 (R := R) (G := H) C V
48 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x)
49 _ =
50 completedGroupAlgebraStageAugmentationInClass C R H V
51 (completedGroupAlgebraFunctorialStageMapInClass
52 (G := G) (H := H) C hHer (R := R) φ hφ V
53 (completedGroupAlgebraProjectionInClass C R G
54 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)) := by
55 rw [completedGroupAlgebraAugmentationAtInClass,
56 completedGroupAlgebraProjectionInClass_map]
57 _ =
58 completedGroupAlgebraStageAugmentationInClass C R G
59 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
60 (completedGroupAlgebraProjectionInClass C R G
61 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x) := by
62 have hstage := congrFun
63 (congrArg DFunLike.coe
64 (completedGroupAlgebraStageAugmentationInClass_comp_functorialStageMapInClass
65 (R := R) (G := G) (H := H) C hHer φ hφ V))
66 (completedGroupAlgebraProjectionInClass C R G
67 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
68 exact hstage
69 _ =
70 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C x := by
71 exact (completedGroupAlgebraCanonicalAugmentationInClass_eq_at
72 (R := R) (G := G) C
73 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x).symm
75/-- Composing an in-class completed map with augmentation gives the source augmentation. -/
76@[simp]
77theorem completedGroupAlgebraCanonicalAugmentationInClass_comp_map
78 (C : ProCGroups.FiniteGroupClass.{v})
80 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
81 (φ : G →* H) (hφ : Continuous φ) :
82 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C ).comp
83 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ) =
84 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C := by
85 apply RingHom.ext
86 intro x
87 exact completedGroupAlgebraCanonicalAugmentationInClass_map
88 (R := R) (G := G) (H := H) C hHer φ hφ x
90/--
91A functorial in-class completed group-algebra map preserves and reflects membership in the
92canonical augmentation ideal.
93-/
94@[simp]
95theorem completedGroupAlgebraMapInClass_mem_canonicalAugmentationIdeal_iff
96 {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R]
97 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
98 {C : ProCGroups.FiniteGroupClass.{v}}
100 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
101 (φ : G →* H) (hφ : Continuous φ)
102 {x : CompletedGroupAlgebraInClass C R G} :
103 completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x ∈
104 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C ↔
105 x ∈ completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C := by
106 rw [mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff,
107 mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff,
108 completedGroupAlgebraCanonicalAugmentationInClass_map]
110/-- The \(C\)-indexed canonical augmentation ideal is pulled back to itself by functorial maps. -/
111@[simp]
112theorem completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_map
113 (C : ProCGroups.FiniteGroupClass.{v})
115 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
116 (φ : G →* H) (hφ : Continuous φ) :
117 Ideal.comap (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)
118 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C ) =
119 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C := by
120 ext x
121 exact completedGroupAlgebraMapInClass_mem_canonicalAugmentationIdeal_iff
122 (R := R) (G := G) (H := H) (C := C) hHer φ hφ
124/--
125A surjective functorial map sends the \(C\)-indexed canonical augmentation ideal onto the target
126canonical augmentation ideal.
127-/
128theorem completedGACanonicalAugmentationIdealInClass_map_functorial_of_surj
129 (C : ProCGroups.FiniteGroupClass.{v})
131 (hForm : ProCGroups.FiniteGroupClass.Formation C)
132 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
133 [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
134 (hH : HasOpenNormalBasisInClass C H)
135 (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ) :
136 Ideal.map (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)
137 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ) =
138 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C := by
139 rw [← completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_map
140 (R := R) (G := G) (H := H) C hHer φ hφ]
141 exact Ideal.map_comap_of_surjective
142 (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)
143 (completedGroupAlgebraMapInClass_surjective_of_surjective
144 (R := R) (G := G) (H := H) C hForm hHer hH φ hφ hφsurj)
145 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C )
147end
149end CompletedGroupAlgebra