Module

GroupLike.lean

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

6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime-power completed group algebra — system — ring — group like

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.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Multiplicative

Imported by2

theorem

primePowerCompletedGroupAlgebraProjection_one

L41 ↗

FoxDifferential.primePowerCompletedGroupAlgebraProjection_one

Documentation

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

Source context 8 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]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem primePowerCompletedGroupAlgebraProjection_one
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
        (1 : PrimePowerCompletedGroupAlgebra ℓ G) = 1

theorem

primePowerCompletedGroupAlgebraProjection_mul

L51 ↗

FoxDifferential.primePowerCompletedGroupAlgebraProjection_mul

Documentation

The finite-stage projection preserves multiplication.

Source context 8 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]
omit [Fact (0 < ℓ)] in

Lean source · statement

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

def

primePowerCompletedGroupAlgebraOf

L67 ↗

FoxDifferential.primePowerCompletedGroupAlgebraOf

Documentation

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

Source context 8 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]
omit [Fact (0 < ℓ)] in

Lean source · statement

def primePowerCompletedGroupAlgebraOf
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (h : H) :
    PrimePowerCompletedGroupAlgebra ell H

theorem

primePowerCompletedGroupAlgebraProjection_of

L108 ↗

FoxDifferential.primePowerCompletedGroupAlgebraProjection_of

Documentation

The 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 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)

theorem

primePowerCompletedGroupAlgebraOf_one

L121 ↗

FoxDifferential.primePowerCompletedGroupAlgebraOf_one

Documentation

The canonical map to the 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 primePowerCompletedGroupAlgebraOf_one
    (ell : Nat)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    primePowerCompletedGroupAlgebraOf (ell := ell) (1 : H) = 1

theorem

primePowerCompletedGroupAlgebraOf_mul

L139 ↗

FoxDifferential.primePowerCompletedGroupAlgebraOf_mul

Documentation

The canonical map to the 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 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₂

Module documentation

Fox differential: prime-power completed group algebra — system — ring — group like

Declarations

primePowerCompletedGroupAlgebraProjection_one

primePowerCompletedGroupAlgebraProjection_mul

primePowerCompletedGroupAlgebraOf

primePowerCompletedGroupAlgebraProjection_of

primePowerCompletedGroupAlgebraOf_one

primePowerCompletedGroupAlgebraOf_mul