Source: ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.InClassComparison
1import ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.CanonicalAugmentation
2import ProCGroups.CompletedGroupAlgebra.Augmentation.CanonicalAugmentation
4/-!
5# Comparing all-finite and in-class augmentations
7The canonical comparison maps between the all-finite and in-class completions commute with their
8augmentations. This file records both directions of that compatibility.
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/--
29Composing the class-indexed canonical augmentation with the comparison map gives the all-finite
30augmentation.
31-/
32@[simp 900]
33theorem completedGroupAlgebraCanonicalAugmentationInClass_comp_toInClass
34 (C : ProCGroups.FiniteGroupClass.{v})
36 (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ).comp
37 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) =
38 completedGroupAlgebraCanonicalAugmentation R G := by
39 apply RingHom.ext
40 intro x
41 let Uc : CompletedGroupAlgebraIndexInClass G C :=
42 terminalCompletedGroupAlgebraIndexInClass (G := G) C
43 let U : CompletedGroupAlgebraIndex G :=
44 completedGroupAlgebraIndexInClassToAllFinite G C Uc
45 calc
46 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
47 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C x)
48 =
49 completedGroupAlgebraAugmentationAtInClass C R G Uc
50 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C x) := by
51 exact completedGroupAlgebraCanonicalAugmentationInClass_eq_at
52 (R := R) (G := G) C Uc
53 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C x)
54 _ =
55 completedGroupAlgebraStageAugmentationInClass C R G Uc
56 (completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C Uc x) := rfl
57 _ =
58 completedGroupAlgebraStageAugmentation R G U
59 (completedGroupAlgebraProjection R G U x) := rfl
60 _ = completedGroupAlgebraCanonicalAugmentation R G x := by
61 exact (completedGroupAlgebraCanonicalAugmentation_eq_at (R := R) (G := G) U x).symm
63/--
64The all-finite canonical augmentation after the comparison map from a class-indexed completion
65agrees with the class-indexed augmentation.
66-/
67@[simp]
68theorem completedGroupAlgebraCanonicalAugmentation_fromInClass
69 (C : ProCGroups.FiniteGroupClass.{v})
71 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)
72 (x : CompletedGroupAlgebraInClass C R G) :
73 completedGroupAlgebraCanonicalAugmentation R G
74 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x) =
75 completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C x := by
76 have h := congrFun
77 (congrArg DFunLike.coe
78 (completedGroupAlgebraCanonicalAugmentationInClass_comp_toInClass
79 (R := R) (G := G) C ))
80 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x)
81 change completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
82 (completedGroupAlgebraToInClass (R := R) (G := G) C
83 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x)) =
84 completedGroupAlgebraCanonicalAugmentation R G
85 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x) at h
86 rw [completedGroupAlgebraToInClass_fromInClass] at h
87 exact h.symm
88end
90end CompletedGroupAlgebra