Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.GroupLike
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Multiplicative
3/-!
4# Fox differential: prime-power completed group algebra — system — ring — group like
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraOf`
9 The canonical map sends a group element to its compatible family of prime-power finite-stage
10 group-like elements.
11- `primePowerCompletedGroupAlgebraProjection_one`
12 The finite-stage projection sends \(1\) to \(1\).
13- `primePowerCompletedGroupAlgebraProjection_mul`
14 The finite-stage projection preserves multiplication.
15- `primePowerCompletedGroupAlgebraProjection_of`
16 The prime-power completed group-algebra projection sends a group-like element to its finite-stage
17 group-like class.
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]
32omit [Fact (0 < ℓ)] in
33/-- The finite-stage projection sends \(1\) to \(1\). -/
34@[simp]
35theorem primePowerCompletedGroupAlgebraProjection_one
36 (i : PrimePowerCompletedGroupAlgebraIndex G) :
37 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
38 (1 : PrimePowerCompletedGroupAlgebra ℓ G) = 1 := by
39 change (1 : PrimePowerCompletedGroupAlgebraStage ℓ G i) = 1
40 rfl
42omit [Fact (0 < ℓ)] in
43/-- The finite-stage projection preserves multiplication. -/
44@[simp]
45theorem primePowerCompletedGroupAlgebraProjection_mul
46 (i : PrimePowerCompletedGroupAlgebraIndex G)
47 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
48 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x * y) =
49 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x *
50 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i y := by
51 change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (x * y).1 i) =
52 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) *
53 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)
54 rfl
56omit [Fact (0 < ℓ)] in
57/--
58The canonical map sends a group element to its compatible family of prime-power finite-stage
59group-like elements.
60-/
61def primePowerCompletedGroupAlgebraOf
62 (ell : Nat)
63 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (h : H) :
64 PrimePowerCompletedGroupAlgebra ell H := by
65 refine ⟨fun i => ?_, ?_⟩
66 · exact
67 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
68 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2)
69 (QuotientGroup.mk h)
70 · intro i j hij
71 change primePowerCompletedGroupAlgebraTransition (ℓ := ell) (G := H) hij
72 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ j.1))
73 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H j.2)
74 (QuotientGroup.mk h)) =
75 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
76 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2)
77 (QuotientGroup.mk h)
78 rw [primePowerCompletedGroupAlgebraTransition_of]
79 rfl
81/--
82The prime-power completed group-algebra projection sends a group-like element to its
83finite-stage group-like class.
84-/
85@[simp]
86theorem primePowerCompletedGroupAlgebraProjection_of
87 (ell : Nat)
88 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
89 (i : PrimePowerCompletedGroupAlgebraIndex H) (h : H) :
90 primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
91 (primePowerCompletedGroupAlgebraOf (ell := ell) h) =
92 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
93 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2)
94 (QuotientGroup.mk h) := by
95 rfl
97/-- The canonical map to the prime-power completed group algebra sends \(1\) to \(1\). -/
98@[simp]
99theorem primePowerCompletedGroupAlgebraOf_one
100 (ell : Nat)
101 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
102 primePowerCompletedGroupAlgebraOf (ell := ell) (1 : H) = 1 := by
103 apply (primePowerCompletedGroupAlgebraSystem ell H).ext
104 intro i
105 change primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
106 (primePowerCompletedGroupAlgebraOf (ell := ell) (1 : H)) =
107 primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
108 (1 : PrimePowerCompletedGroupAlgebra ell H)
109 rw [primePowerCompletedGroupAlgebraProjection_of,
110 primePowerCompletedGroupAlgebraProjection_one]
111 exact map_one
112 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
113 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2))
115/-- The canonical map to the prime-power completed group algebra preserves multiplication. -/
116@[simp]
117theorem primePowerCompletedGroupAlgebraOf_mul
118 (ell : Nat)
119 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (h₁ h₂ : H) :
120 primePowerCompletedGroupAlgebraOf (ell := ell) (h₁ * h₂) =
121 primePowerCompletedGroupAlgebraOf (ell := ell) h₁ *
122 primePowerCompletedGroupAlgebraOf (ell := ell) h₂ := by
123 apply (primePowerCompletedGroupAlgebraSystem ell H).ext
124 intro i
125 change primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
126 (primePowerCompletedGroupAlgebraOf (ell := ell) (h₁ * h₂)) =
127 primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
128 (primePowerCompletedGroupAlgebraOf (ell := ell) h₁ *
129 primePowerCompletedGroupAlgebraOf (ell := ell) h₂)
130 rw [primePowerCompletedGroupAlgebraProjection_of,
131 primePowerCompletedGroupAlgebraProjection_mul,
132 primePowerCompletedGroupAlgebraProjection_of,
133 primePowerCompletedGroupAlgebraProjection_of]
134 change
135 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
136 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2))
137 (QuotientGroup.mk (h₁ * h₂)) =
138 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
139 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2))
140 (QuotientGroup.mk h₁) *
141 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
142 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2))
143 (QuotientGroup.mk h₂)
144 rw [QuotientGroup.mk_mul]
145 exact map_mul
146 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
147 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2))
148 (QuotientGroup.mk h₁) (QuotientGroup.mk h₂)
150end
152end FoxDifferential