FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System/Ring/GroupLike.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Multiplicative
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System/Ring/GroupLike.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed coefficient algebras
14Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups.InverseSystems
21open ProCGroups.ProC
23universe u
25variable (ℓ : ℕ) [Fact (0 < ℓ)]
26variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28omit [Fact (0 < ℓ)] in
29/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は単位元を単位元へ送る。 -/
30@[simp]
32 (i : PrimePowerCompletedGroupAlgebraIndex G) :
33 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
34 (1 : PrimePowerCompletedGroupAlgebra ℓ G) = 1 := by
35 change (1 : PrimePowerCompletedGroupAlgebraStage ℓ G i) = 1
36 rfl
38omit [Fact (0 < ℓ)] in
39/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は積を積へ送る。 -/
40@[simp]
43 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
44 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x * y) =
45 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x *
46 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i y := by
47 change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (x * y).1 i) =
48 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) *
49 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)
50 rfl
52omit [Fact (0 < ℓ)] in
53/-- Definition of primePowerCompletedGroupAlgebraOf. -/
55 (ell : Nat)
56 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (h : H) :
57 PrimePowerCompletedGroupAlgebra ell H := by
58 refine ⟨fun i => ?_, ?_⟩
59 · exact
60 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
61 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2)
62 (QuotientGroup.mk h)
63 · intro i j hij
64 change primePowerCompletedGroupAlgebraTransition (ℓ := ell) (G := H) hij
65 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ j.1))
66 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H j.2)
67 (QuotientGroup.mk h)) =
68 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
69 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2)
70 (QuotientGroup.mk h)
72 rfl
74/-- Evaluation formula for primePowerCompletedGroupAlgebraProjection_of. -/
75@[simp]
77 (ell : Nat)
78 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
79 (i : PrimePowerCompletedGroupAlgebraIndex H) (h : H) :
80 primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
81 (primePowerCompletedGroupAlgebraOf (ell := ell) h) =
82 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
83 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2)
84 (QuotientGroup.mk h) := by
85 rfl
87/-- 素冪係数段階で、群元から得られる group-like 元の有限段階像は単位元を単位元へ送る。 -/
88@[simp]
90 (ell : Nat)
91 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
92 primePowerCompletedGroupAlgebraOf (ell := ell) (1 : H) = 1 := by
93 apply (primePowerCompletedGroupAlgebraSystem ell H).ext
94 intro i
95 change primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
96 (primePowerCompletedGroupAlgebraOf (ell := ell) (1 : H)) =
97 primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
98 (1 : PrimePowerCompletedGroupAlgebra ell H)
101 simp only [MonoidAlgebra.of, MonoidAlgebra.single, QuotientGroup.mk_one, MonoidHom.coe_mk, OneHom.coe_mk,
102 MonoidAlgebra.one_def]
104/-- 素冪係数段階で、群元から得られる group-like 元の有限段階像は積を積へ送る。 -/
105@[simp]
107 (ell : Nat)
108 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (h₁ h₂ : H) :
109 primePowerCompletedGroupAlgebraOf (ell := ell) (h₁ * h₂) =
110 primePowerCompletedGroupAlgebraOf (ell := ell) h₁ *
111 primePowerCompletedGroupAlgebraOf (ell := ell) h₂ := by
112 apply (primePowerCompletedGroupAlgebraSystem ell H).ext
113 intro i
114 change primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
115 (primePowerCompletedGroupAlgebraOf (ell := ell) (h₁ * h₂)) =
116 primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
117 (primePowerCompletedGroupAlgebraOf (ell := ell) h₁ *
118 primePowerCompletedGroupAlgebraOf (ell := ell) h₂)
123 simp only [MonoidAlgebra.of, QuotientGroup.mk_mul, MonoidHom.coe_mk, OneHom.coe_mk,
124 MonoidAlgebra.single_mul_single, mul_one]
126end
128end FoxDifferential