FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/Projection.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Multiplicative
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass/System/Ring/Projection.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 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
33 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i
34 (1 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) = 1 := by
35 rfl
37omit [Fact (0 < ℓ)] in
38/-- 素冪係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は積を積へ送る。 -/
39@[simp]
41 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
42 (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
43 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x * y) =
44 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x *
45 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y := by
46 rfl
48omit [Fact (0 < ℓ)] in
49/-- 素冪係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は零元を零元へ送る。 -/
50@[simp]
52 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
53 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i
54 (0 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) = 0 := by
55 rfl
57omit [Fact (0 < ℓ)] in
58/-- 素冪係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は和を和へ送る。 -/
59@[simp]
61 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
62 (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
63 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x + y) =
64 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x +
65 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y := by
66 rfl
68omit [Fact (0 < ℓ)] in
69/-- 素冪係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は負元を負元へ送る。 -/
70@[simp]
72 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
73 (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
74 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (-x) =
75 -primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x := by
76 rfl
78omit [Fact (0 < ℓ)] in
79/-- 素冪係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は差を差へ送る。 -/
80@[simp]
82 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
83 (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
84 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x - y) =
85 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x -
86 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y := by
87 rfl
89omit [Fact (0 < ℓ)] in
90/-- 素冪係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は自然数倍と両立する。 -/
91@[simp]
93 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
94 (m : ℕ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
95 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (m • x) =
96 m • primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x := by
97 rfl
99omit [Fact (0 < ℓ)] in
100/-- 素冪係数段階で、指定された有限群クラスに属する段階について、完備群環またはその augmentation ideal の有限段階射影は整数倍と両立する。 -/
101@[simp]
103 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
104 (m : ℤ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
105 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (m • x) =
106 m • primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x := by
107 rfl
109end
111end FoxDifferential