Yamaguchi Lean 4 Library
FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/GroupLike.lean
FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/GroupLike/Source

FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/GroupLike.lean

1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/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]
28/-- The class-restricted completed group-algebra element represented by a group element. -/
30 (ell : Nat)
31 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32 (C : ProCGroups.FiniteGroupClass.{u}) (h : H) :
34 refine ⟨fun i => ?_, ?_⟩
35 · exact
36 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
37 (CompletedGroupAlgebraQuotientInClass H C i.2)
38 (QuotientGroup.mk h)
39 · intro i j hij
40 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ell) (G := H) C hij
41 (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ j.1))
42 (CompletedGroupAlgebraQuotientInClass H C j.2)
43 (QuotientGroup.mk h)) =
44 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
45 (CompletedGroupAlgebraQuotientInClass H C i.2)
46 (QuotientGroup.mk h)
48 rfl
50/-- Evaluation formula for primePowerCompletedGroupAlgebraProjectionInClass_of. -/
51@[simp]
53 (ell : Nat)
54 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
55 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass H C)
56 (h : H) :
59 MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
60 (CompletedGroupAlgebraQuotientInClass H C i.2)
61 (QuotientGroup.mk h) := by
62 rfl
64/-- 素冪係数段階で、指定された有限群クラスに属する段階について、群元から得られる group-like 元の有限段階像は単位元を単位元へ送る。 -/
65@[simp]
67 (ell : Nat)
68 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
69 (C : ProCGroups.FiniteGroupClass.{u}) :
70 primePowerCompletedGroupAlgebraOfInClass (ell := ell) (H := H) C 1 = 1 := by
71 apply Subtype.ext
72 funext i
73 change primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ell) (G := H) C i
74 (primePowerCompletedGroupAlgebraOfInClass (ell := ell) (H := H) C 1) =
79 simp only [MonoidAlgebra.of, MonoidAlgebra.single, QuotientGroup.mk_one, MonoidHom.coe_mk, OneHom.coe_mk,
80 MonoidAlgebra.one_def]
82/-- 素冪係数段階で、指定された有限群クラスに属する段階について、群元から得られる group-like 元の有限段階像は積を積へ送る。 -/
83@[simp]
85 (ell : Nat)
86 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
87 (C : ProCGroups.FiniteGroupClass.{u}) (h₁ h₂ : H) :
88 primePowerCompletedGroupAlgebraOfInClass (ell := ell) C (h₁ * h₂) =
91 apply Subtype.ext
92 funext i
93 change primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ell) (G := H) C i
94 (primePowerCompletedGroupAlgebraOfInClass (ell := ell) C (h₁ * h₂)) =
102 simp only [MonoidAlgebra.of, QuotientGroup.mk_mul, MonoidHom.coe_mk, OneHom.coe_mk,
103 MonoidAlgebra.single_mul_single, mul_one]
105end
107end FoxDifferential