NYLL
Module

FiniteAugmentationSquare.lean

Nyll.ProCGroups.ProP.Zassenhaus.FiniteAugmentationSquare
11 declarations indexed from sourceView source ↗

Module documentation

The augmentation-square subgroup at a finite stage

This file packages the ordinary group elements for which [q]-1 belongs to the square of the mod-p augmentation ideal. Direct group-algebra identities show that this subgroup contains all p-th powers and commutators.

Imports4
Imported by2

Declarations

theorem

groupAlgebraAugmentationGenerator_mul

L34 ↗
ClassFieldTower.ProP.groupAlgebraAugmentationGenerator_mul
Documentation

Multiplication formula for ordinary augmentation generators.

Source context 7 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
Lean source · statement
theorem groupAlgebraAugmentationGenerator_mul (a b : Q) :
    groupAlgebraAugmentationGenerator (ZMod p) Q (a * b) =
      groupAlgebraAugmentationGenerator (ZMod p) Q a +
        groupAlgebraAugmentationGenerator (ZMod p) Q b +
          groupAlgebraAugmentationGenerator (ZMod p) Q a *
            groupAlgebraAugmentationGenerator (ZMod p) Q b
theorem

groupAlgebraAugmentationGenerator_inv

L45 ↗
ClassFieldTower.ProP.groupAlgebraAugmentationGenerator_inv
Documentation

Inversion formula for ordinary augmentation generators.

Source context 7 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
Lean source · statement
theorem groupAlgebraAugmentationGenerator_inv (a : Q) :
    groupAlgebraAugmentationGenerator (ZMod p) Q a⁻¹ =
      -MonoidAlgebra.of (ZMod p) Q a⁻¹ *
        groupAlgebraAugmentationGenerator (ZMod p) Q a
theorem

groupAlgebraOf_pow

L65 ↗
ClassFieldTower.ProP.groupAlgebraOf_pow
Documentation

Ordinary group-like elements preserve natural powers.

Source context 7 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
Lean source · statement
theorem groupAlgebraOf_pow (a : Q) (n : ℕ) :
    MonoidAlgebra.of (ZMod p) Q (a ^ n) = MonoidAlgebra.of (ZMod p) Q a ^ n
theorem

groupAlgebraAugmentationGenerator_pow_prime

L73 ↗
ClassFieldTower.ProP.groupAlgebraAugmentationGenerator_pow_prime
Documentation

In characteristic p, the augmentation generator of a^p is the p-th power of the augmentation generator of a.

Source context 7 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
Lean source · statement
theorem groupAlgebraAugmentationGenerator_pow_prime [Fact p.Prime] (a : Q) :
    groupAlgebraAugmentationGenerator (ZMod p) Q (a ^ p) =
      groupAlgebraAugmentationGenerator (ZMod p) Q a ^ p
instance

(anonymous instance)

L91 ↗
Source context 8 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
section AugmentationSquare
Lean source · statement
instance : (groupAlgebraAugmentationIdeal (ZMod p) Q).IsTwoSided
theorem

augmentationGenerator_mul_mem_sq

L95 ↗
ClassFieldTower.ProP.augmentationGenerator_mul_mem_sq
Source context 9 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
section AugmentationSquare
local instance : (groupAlgebraAugmentationIdeal (ZMod p) Q).IsTwoSided := by
  change (RingHom.ker (groupAlgebraAugmentation (ZMod p) Q)).IsTwoSided
  infer_instance
Lean source · statement
theorem augmentationGenerator_mul_mem_sq (a b : Q) :
    groupAlgebraAugmentationGenerator (ZMod p) Q a *
        groupAlgebraAugmentationGenerator (ZMod p) Q b ∈
      (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2
def

augmentationSquareSubgroup

L112 ↗
ClassFieldTower.ProP.augmentationSquareSubgroup
Documentation

Group elements whose standard augmentation generator lies in I².

Source context 9 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
section AugmentationSquare
local instance : (groupAlgebraAugmentationIdeal (ZMod p) Q).IsTwoSided := by
  change (RingHom.ker (groupAlgebraAugmentation (ZMod p) Q)).IsTwoSided
  infer_instance
Lean source · full declaration
def augmentationSquareSubgroup : Subgroup Q where
  carrier := {q | groupAlgebraAugmentationGenerator (ZMod p) Q q ∈
    (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2}
  one_mem' := by
    change groupAlgebraAugmentationGenerator (ZMod p) Q 1 ∈
      (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2
    simp only [groupAlgebraAugmentationGenerator, MonoidAlgebra.of_apply,
      ← MonoidAlgebra.one_def, sub_self]
    exact ((groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2).zero_mem
  mul_mem' := by
    intro a b ha hb
    change groupAlgebraAugmentationGenerator (ZMod p) Q a ∈
      (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2 at ha
    change groupAlgebraAugmentationGenerator (ZMod p) Q b ∈
      (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2 at hb
    change groupAlgebraAugmentationGenerator (ZMod p) Q (a * b) ∈
      (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2
    rw [groupAlgebraAugmentationGenerator_mul]
    exact ((groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2).add_mem
      (((groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2).add_mem ha hb)
      (augmentationGenerator_mul_mem_sq p Q a b)
  inv_mem' := by
    intro a ha
    change groupAlgebraAugmentationGenerator (ZMod p) Q a ∈
      (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2 at ha
    change groupAlgebraAugmentationGenerator (ZMod p) Q a⁻¹ ∈
      (groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2
    rw [groupAlgebraAugmentationGenerator_inv]
    exact ((groupAlgebraAugmentationIdeal (ZMod p) Q) ^ 2).mul_mem_left _ ha
theorem

powerSubgroup_le_augmentationSquareSubgroup

L143 ↗
ClassFieldTower.ProP.powerSubgroup_le_augmentationSquareSubgroup
Documentation

The subgroup generated by p-th powers lies in the augmentation-square subgroup.

Source context 9 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
section AugmentationSquare
local instance : (groupAlgebraAugmentationIdeal (ZMod p) Q).IsTwoSided := by
  change (RingHom.ker (groupAlgebraAugmentation (ZMod p) Q)).IsTwoSided
  infer_instance
Lean source · statement
theorem powerSubgroup_le_augmentationSquareSubgroup [Fact p.Prime] :
    powerSubgroup p Q ≤ augmentationSquareSubgroup p Q
theorem

groupAlgebraCommutatorDifference_identity

L154 ↗
ClassFieldTower.ProP.groupAlgebraCommutatorDifference_identity
Source context 9 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
section AugmentationSquare
local instance : (groupAlgebraAugmentationIdeal (ZMod p) Q).IsTwoSided := by
  change (RingHom.ker (groupAlgebraAugmentation (ZMod p) Q)).IsTwoSided
  infer_instance
Lean source · statement
theorem groupAlgebraCommutatorDifference_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

groupAlgebraAugmentationGenerator_commutator

L167 ↗
ClassFieldTower.ProP.groupAlgebraAugmentationGenerator_commutator
Documentation

A group commutator has augmentation generator in the square ideal.

Source context 9 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
section AugmentationSquare
local instance : (groupAlgebraAugmentationIdeal (ZMod p) Q).IsTwoSided := by
  change (RingHom.ker (groupAlgebraAugmentation (ZMod p) Q)).IsTwoSided
  infer_instance
Lean source · statement
theorem groupAlgebraAugmentationGenerator_commutator (a b : Q) :
    groupAlgebraAugmentationGenerator (ZMod p) Q ⁅a, b⁆ =
      (groupAlgebraAugmentationGenerator (ZMod p) Q a *
          groupAlgebraAugmentationGenerator (ZMod p) Q b -
        groupAlgebraAugmentationGenerator (ZMod p) Q b *
          groupAlgebraAugmentationGenerator (ZMod p) Q a) *
        MonoidAlgebra.of (ZMod p) Q a⁻¹ * MonoidAlgebra.of (ZMod p) Q b⁻¹
theorem

commutator_le_augmentationSquareSubgroup

L189 ↗
ClassFieldTower.ProP.commutator_le_augmentationSquareSubgroup
Documentation

The commutator subgroup lies in the augmentation-square subgroup.

Source context 9 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
noncomputable section
universe u
variable (p : ℕ)
variable (Q : Type u) [Group Q]
section AugmentationSquare
local instance : (groupAlgebraAugmentationIdeal (ZMod p) Q).IsTwoSided := by
  change (RingHom.ker (groupAlgebraAugmentation (ZMod p) Q)).IsTwoSided
  infer_instance
Lean source · statement
theorem commutator_le_augmentationSquareSubgroup :
    commutator Q ≤ augmentationSquareSubgroup p Q

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