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

3 Theorem | 1 Definition

Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / Within a Class / System / Ring / Group-Like.

Open this file on GitHub

import

FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection

Imported by

Definition FoxDifferential.primePowerCompletedGroupAlgebraOfInClass GitHub

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 GitHub

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 proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraOfInClass_one GitHub

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 proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraOfInClass_mul GitHub

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 proof

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

Declarations