Source: ProCGroups.CompletedGroupAlgebra.Augmentation.StageAugmentation
1import ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.UnitRepresentation
3/-!
4# Augmentation at in-class quotient stages
6This file defines augmentation on each in-class finite stage and proves its values on basis
7elements and compatibility with transition, coefficient-change, and functorial stage maps.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14noncomputable section
16open ProCGroups
17open ProCGroups.ProC
18open ProCGroups.InverseSystems
19open ProCGroups.Completion
21universe u v w
23variable (R : Type u) [CommRing R]
24variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
25variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
27/-- The augmentation map on one \(C\)-indexed finite stage. -/
28def completedGroupAlgebraStageAugmentationInClass
29 (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
30 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31 (U : CompletedGroupAlgebraIndexInClass G C) :
32 CompletedGroupAlgebraStageInClass C R G U →+* R :=
33 groupAlgebraAugmentation R (CompletedGroupAlgebraQuotientInClass G C U)
35/-- The in-class finite-stage augmentation sends every group-like basis element to one. -/
36@[simp]
37theorem completedGroupAlgebraStageAugmentationInClass_of
38 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
39 (q : CompletedGroupAlgebraQuotientInClass G C U) :
40 completedGroupAlgebraStageAugmentationInClass C R G U (MonoidAlgebra.of R _ q) = 1 := by
41 simp only [completedGroupAlgebraStageAugmentationInClass, MonoidAlgebra.of_apply,
42 groupAlgebraAugmentation_single]
44/-- The in-class finite-stage augmentation sends a singleton to its coefficient. -/
45@[simp]
46theorem completedGroupAlgebraStageAugmentationInClass_single
47 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
48 (q : CompletedGroupAlgebraQuotientInClass G C U) (r : R) :
49 completedGroupAlgebraStageAugmentationInClass C R G U (MonoidAlgebra.single q r) = r := by
50 simp only [completedGroupAlgebraStageAugmentationInClass, groupAlgebraAugmentation_single]
52/-- In-class finite-stage augmentations are compatible with transition maps. -/
53@[simp]
54theorem completedGroupAlgebraStageAugmentationInClass_compatible
55 (C : ProCGroups.FiniteGroupClass.{v})
56 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
57 (completedGroupAlgebraStageAugmentationInClass C R G U).comp
58 (completedGroupAlgebraTransitionInClass C R G hUV) =
59 completedGroupAlgebraStageAugmentationInClass C R G V := by
60 apply RingHom.ext
61 intro x
62 exact groupAlgebraAugmentation_mapDomainRingHom R
63 (CompletedGroupAlgebraQuotientInClass G C V)
64 (CompletedGroupAlgebraQuotientInClass G C U)
65 (OpenNormalSubgroupInClass.map
66 (C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) x
68/--
69Composing the in-class finite-stage augmentation with the stage map gives the abstract
70augmentation.
71-/
72@[simp]
73theorem completedGroupAlgebraStageAugmentationInClass_comp_stageMapInClass
74 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
75 (completedGroupAlgebraStageAugmentationInClass C R G U).comp
76 (completedGroupAlgebraStageMapInClass C R G U) =
77 groupAlgebraAugmentation R G := by
78 apply RingHom.ext
79 intro x
80 exact groupAlgebraAugmentation_mapDomainRingHom R G
81 (CompletedGroupAlgebraQuotientInClass G C U)
82 (openNormalSubgroupInClassProj (C := C) (G := G) U) x
84/-- In-class finite-stage augmentation is natural in the coefficient ring. -/
85@[simp]
86theorem completedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMapInClass
87 (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S]
88 (f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C) :
89 (completedGroupAlgebraStageAugmentationInClass C S G U).comp
90 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U) =
91 f.comp (completedGroupAlgebraStageAugmentationInClass C R G U) := by
92 apply RingHom.ext
93 intro x
94 exact groupAlgebraAugmentation_mapRangeRingHom R S
95 (CompletedGroupAlgebraQuotientInClass G C U) f x
97/-- In-class finite-stage augmentation is natural for functorial finite-stage maps. -/
98@[simp]
99theorem completedGroupAlgebraStageAugmentationInClass_comp_functorialStageMapInClass
100 (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
101 (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
102 (completedGroupAlgebraStageAugmentationInClass C R H V).comp
103 (completedGroupAlgebraFunctorialStageMapInClass
104 (G := G) (H := H) C hHer (R := R) φ hφ V) =
105 completedGroupAlgebraStageAugmentationInClass C R G
106 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) := by
107 apply RingHom.ext
108 intro x
109 exact groupAlgebraAugmentation_mapDomainRingHom R
110 (CompletedGroupAlgebraQuotientInClass G C
111 (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
112 (CompletedGroupAlgebraQuotientInClass H C V)
113 (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V) x
115end
117end CompletedGroupAlgebra