NYLL
Module

GroupLike.lean

Nyll.ProCGroups.ProP.Zassenhaus.GroupLike
10 declarations indexed from sourceView source ↗

Module documentation

Group-like differences in the mod-p completed group algebra

The element [g] - 1 translates multiplication, inversion, commutators, and p-th powers in a group into augmentation-filtration identities. Keeping these calculations in one leaf prevents later filtration proofs from re-elaborating large noncommutative ring expressions.

Imports2
Imported by3

Declarations

def

groupLikeDifference

L33 ↗
ClassFieldTower.ProP.groupLikeDifference
Documentation

The standard completed group-like difference [g] - 1.

Source context 7 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def groupLikeDifference (g : G) : ModPCompletedGroupAlgebra p G
theorem

groupLikeDifference_mem_augmentationIdeal

L38 ↗
ClassFieldTower.ProP.groupLikeDifference_mem_augmentationIdeal
Documentation

Every group-like difference lies in the augmentation ideal.

Source context 7 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem groupLikeDifference_mem_augmentationIdeal (g : G) :
    groupLikeDifference p G g ∈ modPAugmentationIdeal p G
theorem

groupLikeDifference_one

L47 ↗
ClassFieldTower.ProP.groupLikeDifference_one
Source context 7 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem groupLikeDifference_one : groupLikeDifference p G 1 = 0
theorem

continuous_groupLikeDifference

L51 ↗
ClassFieldTower.ProP.continuous_groupLikeDifference
Documentation

The group-like-difference map is continuous.

Source context 7 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem continuous_groupLikeDifference : Continuous (groupLikeDifference p G)
theorem

groupLikeDifference_mul

L57 ↗
ClassFieldTower.ProP.groupLikeDifference_mul
Documentation

First-order multiplication formula for group-like differences.

Source context 7 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem groupLikeDifference_mul (g h : G) :
    groupLikeDifference p G (g * h) =
      groupLikeDifference p G g + groupLikeDifference p G h +
        groupLikeDifference p G g * groupLikeDifference p G h
theorem

groupLikeDifference_inv

L66 ↗
ClassFieldTower.ProP.groupLikeDifference_inv
Documentation

Inversion formula for a group-like difference.

Source context 7 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem groupLikeDifference_inv (g : G) :
    groupLikeDifference p G g⁻¹ =
      -completedGroupAlgebraOfInClass
          (ProCGroups.FiniteGroupClass.pGroup p) (ZMod p) G g⁻¹ *
        groupLikeDifference p G g
theorem

commutatorDifference_identity

L96 ↗
ClassFieldTower.ProP.commutatorDifference_identity
Documentation

A ring identity underlying the commutator filtration calculation.

Source context 7 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem commutatorDifference_identity
    {R : Type*} [Ring R] (a b ai bi : R)
    (hai : a * ai = 1) (hbi : b * bi = 1) :
    a * b * ai * bi - 1 =
      ((a - 1) * (b - 1) - (b - 1) * (a - 1)) * ai * bi
theorem

groupLikeDifference_commutator

L110 ↗
ClassFieldTower.ProP.groupLikeDifference_commutator
Documentation

A group commutator becomes a difference of quadratic augmentation terms, up to multiplication by group-like units.

Source context 7 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem groupLikeDifference_commutator (g h : G) :
    groupLikeDifference p G ⁅g, h⁆ =
      (groupLikeDifference p G g * groupLikeDifference p G h -
        groupLikeDifference p G h * groupLikeDifference p G g) *
        completedGroupAlgebraOfInClass
          (ProCGroups.FiniteGroupClass.pGroup p) (ZMod p) G g⁻¹ *
        completedGroupAlgebraOfInClass
          (ProCGroups.FiniteGroupClass.pGroup p) (ZMod p) G h⁻¹
theorem

completedGroupAlgebraOfInClass_pow

L146 ↗
ClassFieldTower.ProP.completedGroupAlgebraOfInClass_pow
Documentation

Completed group-like elements preserve natural powers.

Source context 7 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem completedGroupAlgebraOfInClass_pow (g : G) (n : ℕ) :
    completedGroupAlgebraOfInClass
        (ProCGroups.FiniteGroupClass.pGroup p) (ZMod p) G (g ^ n) =
      completedGroupAlgebraOfInClass
        (ProCGroups.FiniteGroupClass.pGroup p) (ZMod p) G g ^ n
theorem

groupLikeDifference_pow_prime

L158 ↗
ClassFieldTower.ProP.groupLikeDifference_pow_prime
Documentation

In characteristic p, the difference of a p-th power is the p-th power of the difference.

Source context 7 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem groupLikeDifference_pow_prime (g : G) :
    groupLikeDifference p G (g ^ p) = groupLikeDifference p G g ^ p

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.