Yamaguchi Lean 4 Library
Source: ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.StageAugmentation
ProCGroups/CompletedGroupAlgebra/AllFiniteAugmentation/StageAugmentation/Source

Source: ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.StageAugmentation

1import ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.TerminalIndex
3/-!
4# Augmentation at all-finite quotient stages
6This file defines augmentation on each finite coefficient-and-group stage of the all-finite
7system and proves its formulas on basis elements and compatibility with transition, coefficient,
8and functorial stage maps.
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/--
29The augmentation map on a finite stage is the ring homomorphism \(R[G/U]\to R\) that sends every
30group-like basis element to \(1\).
31-/
32def completedGroupAlgebraStageAugmentation (R : Type u) (G : Type v) [CommRing R]
33 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
34 (U : CompletedGroupAlgebraIndex G) :
35 CompletedGroupAlgebraStage R G U →+* R :=
36 groupAlgebraAugmentation R (CompletedGroupAlgebraQuotient G U)
38omit [TopologicalSpace R] [IsTopologicalRing R] in
39/-- The finite-stage augmentation sends every group-like basis element to one. -/
40@[simp]
41theorem completedGroupAlgebraStageAugmentation_of
42 (U : CompletedGroupAlgebraIndex G) (q : CompletedGroupAlgebraQuotient G U) :
43 completedGroupAlgebraStageAugmentation R G U (MonoidAlgebra.of R _ q) = 1 := by
44 simp only [completedGroupAlgebraStageAugmentation, MonoidAlgebra.of_apply,
45 groupAlgebraAugmentation_single]
47omit [TopologicalSpace R] [IsTopologicalRing R] in
48/-- The finite-stage augmentation sends a singleton to its coefficient. -/
49@[simp]
50theorem completedGroupAlgebraStageAugmentation_single
51 (U : CompletedGroupAlgebraIndex G) (q : CompletedGroupAlgebraQuotient G U) (r : R) :
52 completedGroupAlgebraStageAugmentation R G U (MonoidAlgebra.single q r) = r := by
53 simp only [completedGroupAlgebraStageAugmentation, groupAlgebraAugmentation_single]
55omit [TopologicalSpace R] [IsTopologicalRing R] in
56/-- Finite-stage augmentations are compatible with transition maps. -/
57@[simp]
58theorem completedGroupAlgebraStageAugmentation_compatible
59 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
60 (completedGroupAlgebraStageAugmentation R G U).comp
61 (completedGroupAlgebraTransition R G hUV) =
62 completedGroupAlgebraStageAugmentation R G V := by
63 apply RingHom.ext
64 intro x
65 exact groupAlgebraAugmentation_mapDomainRingHom R
66 (CompletedGroupAlgebraQuotient G V) (CompletedGroupAlgebraQuotient G U)
67 (OpenNormalSubgroupInClass.map
69 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) x
71omit [TopologicalSpace R] [IsTopologicalRing R] in
72/-- Finite-stage augmentation after the stage map is the abstract group-algebra augmentation. -/
73@[simp]
74theorem completedGroupAlgebraStageAugmentation_comp_stageMap
75 (U : CompletedGroupAlgebraIndex G) :
76 (completedGroupAlgebraStageAugmentation R G U).comp
77 (completedGroupAlgebraStageMap R G U) =
78 groupAlgebraAugmentation R G := by
79 apply RingHom.ext
80 intro x
81 exact groupAlgebraAugmentation_mapDomainRingHom R G (CompletedGroupAlgebraQuotient G U)
82 (openNormalSubgroupInClassProj
85omit [TopologicalSpace R] [IsTopologicalRing R] in
86/-- Finite-stage augmentation is natural in the coefficient ring. -/
87@[simp]
88theorem completedGroupAlgebraStageAugmentation_comp_stageCoeffMap
89 (S : Type w) [CommRing S] (f : R →+* S) (U : CompletedGroupAlgebraIndex G) :
90 (completedGroupAlgebraStageAugmentation S G U).comp
91 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U) =
92 f.comp (completedGroupAlgebraStageAugmentation R G U) := by
93 apply RingHom.ext
94 intro x
95 exact groupAlgebraAugmentation_mapRangeRingHom R S
96 (CompletedGroupAlgebraQuotient G U) f x
98omit [TopologicalSpace R] [IsTopologicalRing R] in
99/-- Finite-stage augmentation is natural with respect to functorial finite-stage maps. -/
100@[simp]
101theorem completedGroupAlgebraStageAugmentation_comp_functorialStageMap
102 (φ : G →* H) (hφ : Continuous φ)
103 (V : CompletedGroupAlgebraIndex H) :
104 (completedGroupAlgebraStageAugmentation R H V).comp
105 (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V) =
106 completedGroupAlgebraStageAugmentation R G
107 (completedGroupAlgebraComapIndex (G := G) φ hφ V) := by
108 apply RingHom.ext
109 intro x
110 exact groupAlgebraAugmentation_mapDomainRingHom R
111 (CompletedGroupAlgebraQuotient G (completedGroupAlgebraComapIndex (G := G) φ hφ V))
112 (CompletedGroupAlgebraQuotient H V)
113 (completedGroupAlgebraComapQuotientMap (G := G) φ hφ V) x
114end
116end CompletedGroupAlgebra