Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.GroupLike
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection
3/-!
4# Fox differential: in class — system — ring — group like
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraOfInClass`
9 The class-restricted completed group-algebra element represented by a group element.
10- `primePowerCompletedGroupAlgebraProjectionInClass_of`
11 The \(C\)-indexed prime-power completed group-algebra projection sends a group-like element to its
12 finite-stage group-like class.
13- `primePowerCompletedGroupAlgebraOfInClass_one`
14 The canonical map to the class-indexed prime-power completed group algebra sends \(1\) to \(1\).
15- `primePowerCompletedGroupAlgebraOfInClass_mul`
16 The canonical map to the class-indexed prime-power completed group algebra preserves
17 multiplication.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.InverseSystems
25open ProCGroups.ProC
27universe u
29variable (ℓ : ℕ) [Fact (0 < ℓ)]
30variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32/-- The class-restricted completed group-algebra element represented by a group element. -/
33def primePowerCompletedGroupAlgebraOfInClass
34 (ell : Nat)
35 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
36 (C : ProCGroups.FiniteGroupClass.{u}) (h : H) :
37 PrimePowerCompletedGroupAlgebraInClass ell H C := by
38 refine ⟨fun i => ?_, ?_⟩
39 · exact
40 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
41 (CompletedGroupAlgebraQuotientInClass H C i.2)
42 (QuotientGroup.mk h)
43 · intro i j hij
44 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ell) (G := H) C hij
45 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ j.1))
46 (CompletedGroupAlgebraQuotientInClass H C j.2)
47 (QuotientGroup.mk h)) =
48 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
49 (CompletedGroupAlgebraQuotientInClass H C i.2)
50 (QuotientGroup.mk h)
51 rw [primePowerCompletedGroupAlgebraTransitionInClass_of]
52 rfl
54/--
55The \(C\)-indexed prime-power completed group-algebra projection sends a group-like element to
56its finite-stage group-like class.
57-/
58@[simp]
59theorem primePowerCompletedGroupAlgebraProjectionInClass_of
60 (ell : Nat)
61 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
62 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass H C)
63 (h : H) :
64 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ell) (G := H) C i
65 (primePowerCompletedGroupAlgebraOfInClass (ell := ell) C h) =
66 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
67 (CompletedGroupAlgebraQuotientInClass H C i.2)
68 (QuotientGroup.mk h) := by
69 rfl
71/--
72The canonical map to the class-indexed prime-power completed group algebra sends \(1\) to \(1\).
73-/
74@[simp]
75theorem primePowerCompletedGroupAlgebraOfInClass_one
76 (ell : Nat)
77 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
78 (C : ProCGroups.FiniteGroupClass.{u}) :
79 primePowerCompletedGroupAlgebraOfInClass (ell := ell) (H := H) C 1 = 1 := by
80 apply Subtype.ext
81 funext i
82 change primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ell) (G := H) C i
83 (primePowerCompletedGroupAlgebraOfInClass (ell := ell) (H := H) C 1) =
84 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ell) (G := H) C i
85 (1 : PrimePowerCompletedGroupAlgebraInClass ell H C)
86 rw [primePowerCompletedGroupAlgebraProjectionInClass_of,
87 primePowerCompletedGroupAlgebraProjectionInClass_one]
88 exact map_one
89 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
90 (CompletedGroupAlgebraQuotientInClass H C i.2))
92/--
93The canonical map to the class-indexed prime-power completed group algebra preserves
94multiplication.
95-/
96@[simp]
97theorem primePowerCompletedGroupAlgebraOfInClass_mul
98 (ell : Nat)
99 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
100 (C : ProCGroups.FiniteGroupClass.{u}) (h₁ h₂ : H) :
101 primePowerCompletedGroupAlgebraOfInClass (ell := ell) C (h₁ * h₂) =
102 primePowerCompletedGroupAlgebraOfInClass (ell := ell) C h₁ *
103 primePowerCompletedGroupAlgebraOfInClass (ell := ell) C h₂ := by
104 apply Subtype.ext
105 funext i
106 change primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ell) (G := H) C i
107 (primePowerCompletedGroupAlgebraOfInClass (ell := ell) C (h₁ * h₂)) =
108 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ell) (G := H) C i
109 (primePowerCompletedGroupAlgebraOfInClass (ell := ell) C h₁ *
110 primePowerCompletedGroupAlgebraOfInClass (ell := ell) C h₂)
111 rw [primePowerCompletedGroupAlgebraProjectionInClass_of,
112 primePowerCompletedGroupAlgebraProjectionInClass_mul,
113 primePowerCompletedGroupAlgebraProjectionInClass_of,
114 primePowerCompletedGroupAlgebraProjectionInClass_of]
115 change
116 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
117 (CompletedGroupAlgebraQuotientInClass H C i.2))
118 (QuotientGroup.mk (h₁ * h₂)) =
119 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
120 (CompletedGroupAlgebraQuotientInClass H C i.2))
121 (QuotientGroup.mk h₁) *
122 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
123 (CompletedGroupAlgebraQuotientInClass H C i.2))
124 (QuotientGroup.mk h₂)
125 rw [QuotientGroup.mk_mul]
126 exact map_mul
127 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
128 (CompletedGroupAlgebraQuotientInClass H C i.2))
129 (QuotientGroup.mk h₁) (QuotientGroup.mk h₂)
131end
133end FoxDifferential