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

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

3 Theorems | 1 Definition

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraOfInClass The class-restricted completed group-algebra element represented by a group element. - primePowerCompletedGroupAlgebraProjectionInClass_of The \(C\)-indexed prime-power completed group-algebra projection sends a group-like element to its finite-stage group-like class. - primePowerCompletedGroupAlgebraOfInClass_one The canonical map to the class-indexed prime-power completed group algebra sends \(1\) to \(1\). - primePowerCompletedGroupAlgebraOfInClass_mul The canonical map to the class-indexed prime-power completed group algebra preserves multiplication.
import
Imported by

Declarations

Definition FoxDifferential.primePowerCompletedGroupAlgebraOfInClass 
def primePowerCompletedGroupAlgebraOfInClass
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (C : ProCGroups.FiniteGroupClass.{u}) (h : H) :
    PrimePowerCompletedGroupAlgebraInClass ell H C := by
  refine ⟨fun i => ?_, ?_⟩
  · exact
      MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
        (CompletedGroupAlgebraQuotientInClass H C i.2)
        (QuotientGroup.mk h)
  · intro i j hij
    change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ell) (G := H) C hij
        (MonoidAlgebra.of (ModNCompletedCoeff (ell ^ j.1))
          (CompletedGroupAlgebraQuotientInClass H C j.2)
          (QuotientGroup.mk h)) =
      MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
        (CompletedGroupAlgebraQuotientInClass H C i.2)
        (QuotientGroup.mk h)
    rw [primePowerCompletedGroupAlgebraTransitionInClass_of]
    rfl

The class-restricted completed group-algebra element represented by a group element.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_of 
@[simp]
theorem primePowerCompletedGroupAlgebraProjectionInClass_of
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass H C)
    (h : H) :
    primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ell) (G := H) C i
        (primePowerCompletedGroupAlgebraOfInClass (ell := ell) C h) =
      MonoidAlgebra.of (ModNCompletedCoeff (ell ^ i.1))
        (CompletedGroupAlgebraQuotientInClass H C i.2)
        (QuotientGroup.mk h)

The \(C\)-indexed prime-power completed group-algebra projection sends a group-like element to its finite-stage group-like class.

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraOfInClass_one 
@[simp]
theorem primePowerCompletedGroupAlgebraOfInClass_one
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (C : ProCGroups.FiniteGroupClass.{u}) :
    primePowerCompletedGroupAlgebraOfInClass (ell := ell) (H := H) C 1 = 1

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

Show Lean proof
Theorem FoxDifferential.primePowerCompletedGroupAlgebraOfInClass_mul 
@[simp]
theorem primePowerCompletedGroupAlgebraOfInClass_mul
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (C : ProCGroups.FiniteGroupClass.{u}) (h₁ h₂ : H) :
    primePowerCompletedGroupAlgebraOfInClass (ell := ell) C (h₁ * h₂) =
      primePowerCompletedGroupAlgebraOfInClass (ell := ell) C h₁ *
        primePowerCompletedGroupAlgebraOfInClass (ell := ell) C h₂

The canonical map to the class-indexed prime-power completed group algebra preserves multiplication.

Show Lean proof