Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.GroupLike
ProCGroups/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System/Ring/GroupLike

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.GroupLike

5 Theorems | 1 Definition

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraOf The canonical map sends a group element to its compatible family of prime-power finite-stage group-like elements. - primePowerCompletedGroupAlgebraProjection_one The finite-stage projection sends \(1\) to \(1\). - primePowerCompletedGroupAlgebraProjection_mul The finite-stage projection preserves multiplication. - primePowerCompletedGroupAlgebraProjection_of The prime-power completed group-algebra projection sends a group-like element to its finite-stage group-like class.
import
Imported by

Declarations

Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjection_one 
omit [Fact (0 < ℓ)] in
@[simp]
theorem primePowerCompletedGroupAlgebraProjection_one
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
        (1 : PrimePowerCompletedGroupAlgebra ℓ G) = 1

The finite-stage projection sends \(1\) to \(1\).

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjection_mul 
omit [Fact (0 < ℓ)] in
@[simp]
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 y

The finite-stage projection preserves multiplication.

Show Lean proof
Definition FoxDifferential.primePowerCompletedGroupAlgebraOf 
omit [Fact (0 < ℓ)] in
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]
    rfl

The canonical map sends a group element to its compatible family of prime-power finite-stage group-like elements.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjection_of 
@[simp]
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 Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraOf_one 
@[simp]
theorem primePowerCompletedGroupAlgebraOf_one
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    primePowerCompletedGroupAlgebraOf (ell := ell) (1 : H) = 1

The canonical map to the prime-power completed group algebra sends \(1\) to \(1\).

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraOf_mul 
@[simp]
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 Lean proof