Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Multiplicative
3/-!
4# Fox differential: in class — system — ring — projection
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraProjectionInClass_one`
9 The finite-stage projection sends \(1\) to \(1\).
10- `primePowerCompletedGroupAlgebraProjectionInClass_mul`
11 The finite-stage projection preserves multiplication.
12- `primePowerCompletedGroupAlgebraProjectionInClass_zero`
13 The finite-stage projection sends \(0\) to \(0\).
14- `primePowerCompletedGroupAlgebraProjectionInClass_add`
15 The prime-power finite-stage projection preserves addition.
16-/
18namespace FoxDifferential
20noncomputable section
22open ProCGroups.InverseSystems
23open ProCGroups.ProC
25universe u
27variable (ℓ : ℕ) [Fact (0 < ℓ)]
28variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30omit [Fact (0 < ℓ)] in
31/-- The finite-stage projection sends \(1\) to \(1\). -/
32@[simp]
33theorem primePowerCompletedGroupAlgebraProjectionInClass_one
34 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
35 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i
36 (1 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) = 1 := by
37 rfl
39omit [Fact (0 < ℓ)] in
40/-- The finite-stage projection preserves multiplication. -/
41@[simp]
42theorem primePowerCompletedGroupAlgebraProjectionInClass_mul
43 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
44 (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
45 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x * y) =
46 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x *
47 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y := by
48 rfl
50omit [Fact (0 < ℓ)] in
51/-- The finite-stage projection sends \(0\) to \(0\). -/
52@[simp]
53theorem primePowerCompletedGroupAlgebraProjectionInClass_zero
54 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
55 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i
56 (0 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) = 0 := by
57 rfl
59omit [Fact (0 < ℓ)] in
60/-- The prime-power finite-stage projection preserves addition. -/
61@[simp]
62theorem primePowerCompletedGroupAlgebraProjectionInClass_add
63 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
64 (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
65 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x + y) =
66 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x +
67 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y := by
68 rfl
70omit [Fact (0 < ℓ)] in
71/-- The prime-power finite-stage projection preserves negation. -/
72@[simp]
73theorem primePowerCompletedGroupAlgebraProjectionInClass_neg
74 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
75 (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
76 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (-x) =
77 -primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x := by
78 rfl
80omit [Fact (0 < ℓ)] in
81/-- The prime-power finite-stage projection preserves subtraction. -/
82@[simp]
83theorem primePowerCompletedGroupAlgebraProjectionInClass_sub
84 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
85 (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
86 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x - y) =
87 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x -
88 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i y := by
89 rfl
91omit [Fact (0 < ℓ)] in
92/-- The finite-stage projection is compatible with natural-number scalar multiplication. -/
93@[simp]
94theorem primePowerCompletedGroupAlgebraProjectionInClass_nsmul
95 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
96 (m : ℕ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
97 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (m • x) =
98 m • primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x := by
99 rfl
101omit [Fact (0 < ℓ)] in
102/-- The finite-stage projection is compatible with integer scalar multiplication. -/
103@[simp]
104theorem primePowerCompletedGroupAlgebraProjectionInClass_zsmul
105 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
106 (m : ℤ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
107 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (m • x) =
108 m • primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x := by
109 rfl
111end
113end FoxDifferential