CompletedGroupAlgebra/Augmentation/Functoriality.lean
1import CompletedGroupAlgebra.Augmentation.AugmentationIdeal
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Augmentation/Functoriality.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Augmentation and augmentation ideals
14The 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.
15-/
16open scoped Topology
18namespace CompletedGroupAlgebra
20noncomputable section
22open ProCGroups
23open ProCGroups.ProC
24open ProCGroups.InverseSystems
25open ProCGroups.Completion
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 in-class canonical augmentation is natural under functorial completed maps. -/
34@[simp 900]
36 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
38 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
39 (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C hC R G) :
40 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C hC
41 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x) =
42 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC x := by
43 let V : CompletedGroupAlgebraIndexInClass H C :=
44 terminalCompletedGroupAlgebraIndexInClass (G := H) C
45 calc
46 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C hC
47 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x)
48 =
49 completedGroupAlgebraAugmentationAtInClass C R H hC V
50 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x) := by
52 (R := R) (G := H) C hC V
53 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x)
54 _ =
57 (G := G) (H := H) C hHer (R := R) φ hφ V
58 (completedGroupAlgebraProjectionInClass C hC R G
59 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)) := by
61 _ =
63 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
64 (completedGroupAlgebraProjectionInClass C hC R G
65 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x) := by
66 have hstage := congrFun
67 (congrArg DFunLike.coe
69 (R := R) (G := G) (H := H) C hHer φ hφ V))
70 (completedGroupAlgebraProjectionInClass C hC R G
71 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
72 exact hstage
73 _ =
74 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC x := by
76 (R := R) (G := G) C hC
77 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x).symm
79/-- Composing an in-class completed map with augmentation gives the source augmentation. -/
80@[simp]
82 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
84 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
85 (φ : G →* H) (hφ : Continuous φ) :
86 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C hC).comp
87 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ) =
88 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC := by
89 apply RingHom.ext
90 intro x
92 (R := R) (G := G) (H := H) C hC hHer φ hφ x
94/-- Functorial in-class completed maps preserve membership in the canonical augmentation ideal. -/
95@[simp]
97 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
99 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
100 (φ : G →* H) (hφ : Continuous φ)
101 (x : CompletedGroupAlgebraInClass C hC R G) :
102 completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x ∈
103 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C hC ↔
104 x ∈ completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC := by
109/-- The `C`-indexed canonical augmentation ideal is pulled back to itself by functorial maps. -/
110@[simp]
112 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
114 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
115 (φ : G →* H) (hφ : Continuous φ) :
116 Ideal.comap (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ)
117 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C hC) =
118 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC := by
119 ext x
121 (R := R) (G := G) (H := H) C hC hHer φ hφ x
123/-- A surjective functorial map sends the `C`-indexed canonical augmentation ideal onto the
124target canonical augmentation ideal. -/
126 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
128 (hForm : ProCGroups.FiniteGroupClass.Formation C)
129 (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
130 (hR : IsProfiniteRing R) (hH : IsProCGroup C H)
131 (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ) :
132 Ideal.map (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ)
133 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC) =
134 completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C hC := by
136 (R := R) (G := G) (H := H) C hC hHer φ hφ]
137 exact Ideal.map_comap_of_surjective
138 (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ)
140 (R := R) (G := G) (H := H) C hC hForm hHer hR hH φ hφ hφsurj)
141 (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C hC)
143end