Module

GroupLike.lean

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

4 declarations indexed from sourceView source ↗

Module documentation

Fox differential: in class — system — ring — group like

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.

Imports1

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

Imported by1

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.All

def

primePowerCompletedGroupAlgebraOfInClass

L39 ↗

FoxDifferential.primePowerCompletedGroupAlgebraOfInClass

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def primePowerCompletedGroupAlgebraOfInClass
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (C : ProCGroups.FiniteGroupClass.{u}) (h : H) :
    PrimePowerCompletedGroupAlgebraInClass ell H C

theorem

primePowerCompletedGroupAlgebraProjectionInClass_of

L79 ↗

FoxDifferential.primePowerCompletedGroupAlgebraProjectionInClass_of

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

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)

theorem

primePowerCompletedGroupAlgebraOfInClass_one

L95 ↗

FoxDifferential.primePowerCompletedGroupAlgebraOfInClass_one

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

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

theorem

primePowerCompletedGroupAlgebraOfInClass_mul

L117 ↗

FoxDifferential.primePowerCompletedGroupAlgebraOfInClass_mul

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

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₂

Module documentation

Fox differential: in class — system — ring — group like

Declarations

primePowerCompletedGroupAlgebraOfInClass

primePowerCompletedGroupAlgebraProjectionInClass_of

primePowerCompletedGroupAlgebraOfInClass_one

primePowerCompletedGroupAlgebraOfInClass_mul