FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.GroupLike
Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / System / Ring / Group-Like.
Imported by
- FoxDifferential.Completed
- FoxDifferential.Completed.CoefficientRings
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Projection
theorem primePowerCompletedGroupAlgebraProjection_one
(i : PrimePowerCompletedGroupAlgebraIndex G) :
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
(1 : PrimePowerCompletedGroupAlgebra ℓ G) = 1The finite-stage projection sends \(1\) to \(1\).
Show proof
by
change (1 : PrimePowerCompletedGroupAlgebraStage ℓ G i) = 1
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraProjection_mul
(i : PrimePowerCompletedGroupAlgebraIndex G)
(x y : PrimePowerCompletedGroupAlgebra ℓ G) :
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x * y) =
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x *
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i yThe finite-stage projection preserves multiplication.
Show proof
by
change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (x * y).1 i) =
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) *
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□def primePowerCompletedGroupAlgebraOf
(ell : Nat)
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (h : H) :
PrimePowerCompletedGroupAlgebra ell H := by
refine ⟨fun i => ?_, ?_⟩
· exact
MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2)
(QuotientGroup.mk h)
· intro i j hij
change primePowerCompletedGroupAlgebraTransition (ℓ := ell) (G := H) hij
(MonoidAlgebra.of (ModNCompletedCoeff (ell ^ j.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H j.2)
(QuotientGroup.mk h)) =
MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2)
(QuotientGroup.mk h)
rw [primePowerCompletedGroupAlgebraTransition_of]
rflThe canonical map sends a group element to its compatible family of prime-power finite-stage group-like elements.
theorem primePowerCompletedGroupAlgebraProjection_of
(ell : Nat)
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(i : PrimePowerCompletedGroupAlgebraIndex H) (h : H) :
primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
(primePowerCompletedGroupAlgebraOf (ell := ell) h) =
MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2)
(QuotientGroup.mk h)The prime-power completed group-algebra projection sends a group-like element to its finite-stage group-like class.
Show proof
by
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraOf_one
(ell : Nat)
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
primePowerCompletedGroupAlgebraOf (ell := ell) (1 : H) = 1The canonical map to the prime-power completed group algebra sends \(1\) to \(1\).
Show proof
by
apply (primePowerCompletedGroupAlgebraSystem ell H).ext
intro i
change primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
(primePowerCompletedGroupAlgebraOf (ell := ell) (1 : H)) =
primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
(1 : PrimePowerCompletedGroupAlgebra ell H)
rw [primePowerCompletedGroupAlgebraProjection_of,
primePowerCompletedGroupAlgebraProjection_one]
simp only [MonoidAlgebra.of, MonoidAlgebra.single, QuotientGroup.mk_one, MonoidHom.coe_mk, OneHom.coe_mk,
MonoidAlgebra.one_def]Proof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraOf_mul
(ell : Nat)
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (h₁ h₂ : H) :
primePowerCompletedGroupAlgebraOf (ell := ell) (h₁ * h₂) =
primePowerCompletedGroupAlgebraOf (ell := ell) h₁ *
primePowerCompletedGroupAlgebraOf (ell := ell) h₂The canonical map to the prime-power completed group algebra preserves multiplication.
Show proof
by
apply (primePowerCompletedGroupAlgebraSystem ell H).ext
intro i
change primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
(primePowerCompletedGroupAlgebraOf (ell := ell) (h₁ * h₂)) =
primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i
(primePowerCompletedGroupAlgebraOf (ell := ell) h₁ *
primePowerCompletedGroupAlgebraOf (ell := ell) h₂)
rw [primePowerCompletedGroupAlgebraProjection_of,
primePowerCompletedGroupAlgebraProjection_mul,
primePowerCompletedGroupAlgebraProjection_of,
primePowerCompletedGroupAlgebraProjection_of]
simp only [MonoidAlgebra.of, QuotientGroup.mk_mul, MonoidHom.coe_mk, OneHom.coe_mk,
MonoidAlgebra.single_mul_single, mul_one]Proof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□