NYLL
Module

Witt.lean

Nyll.GaloisCohomology.GroupTheory.Transfer.Witt
68 declarations indexed from sourceView source ↗

Module documentation

Witt's transfer theorem

For a finitely generated group G with finite abelianization, the transfer from G / G' to G' / G'' is trivial.

The proof follows Witt's group-ring argument. This file first constructs the required right Fox coefficients directly from free words; no presentation relations are assumed as extra input.

Imports11
Imported by2

Declarations

instance

finiteAbelianizationOfFiniteIndex

L48 ↗
GroupTheory.Transfer.Witt.finiteAbelianizationOfFiniteIndex
Documentation

Finite index of the commutator gives finiteness of the abelianization.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
instance finiteAbelianizationOfFiniteIndex
    [FiniteIndex (commutator G)] :
    Finite (Abelianization G)
def

commutatorTransfer

L57 ↗
GroupTheory.Transfer.Witt.commutatorTransfer
Documentation

The transfer between the successive commutator abelianizations G / G' and G' / G''.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
def commutatorTransfer
    [FiniteIndex (commutator G)] :
    Abelianization G →* Abelianization (commutator G)
theorem

commutatorTransfer_of

L66 ↗
GroupTheory.Transfer.Witt.commutatorTransfer_of
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem commutatorTransfer_of
    [FiniteIndex (commutator G)] (g : G) :
    commutatorTransfer (G := G) (Abelianization.of g) =
      MonoidHom.transfer
        (Abelianization.of :
          commutator G →* Abelianization (commutator G)) g
def

groupRingDelta

L75 ↗
GroupTheory.Transfer.Witt.groupRingDelta
Documentation

The integral group-ring element [g] - 1.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
def groupRingDelta (g : G) : IntegralGroupRing G
theorem

groupRingDelta_one

L80 ↗
GroupTheory.Transfer.Witt.groupRingDelta_one
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem groupRingDelta_one :
    groupRingDelta (1 : G) = 0
theorem

groupRingDelta_mul

L84 ↗
GroupTheory.Transfer.Witt.groupRingDelta_mul
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem groupRingDelta_mul (g h : G) :
    groupRingDelta (g * h) =
      groupRingDelta g * MonoidAlgebra.single h 1 +
        groupRingDelta h
theorem

groupRingDelta_mul_left

L97 ↗
GroupTheory.Transfer.Witt.groupRingDelta_mul_left
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem groupRingDelta_mul_left (g h : G) :
    groupRingDelta (g * h) =
      MonoidAlgebra.single g 1 * groupRingDelta h +
        groupRingDelta g
theorem

groupRingDelta_inv

L110 ↗
GroupTheory.Transfer.Witt.groupRingDelta_inv
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem groupRingDelta_inv (g : G) :
    groupRingDelta g⁻¹ =
      groupRingDelta g *
        (-MonoidAlgebra.single g⁻¹ 1)
theorem

groupRingDelta_inv_left

L129 ↗
GroupTheory.Transfer.Witt.groupRingDelta_inv_left
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem groupRingDelta_inv_left (g : G) :
    groupRingDelta g⁻¹ =
      (-MonoidAlgebra.single g⁻¹ 1) *
        groupRingDelta g
theorem

augmentation_groupRingDelta

L147 ↗
GroupTheory.Transfer.Witt.augmentation_groupRingDelta
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem augmentation_groupRingDelta (g : G) :
    augmentation G (groupRingDelta g) = 0
def

wordExponent

L152 ↗
GroupTheory.Transfer.Witt.wordExponent
Documentation

The exponent-sum vector of a free word.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
def wordExponent {X : Type*} (w : FreeGroup X) : X →₀ ℤ
theorem

wordExponent_one

L157 ↗
GroupTheory.Transfer.Witt.wordExponent_one
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem wordExponent_one {X : Type*} :
    wordExponent (1 : FreeGroup X) = 0
theorem

wordExponent_of

L162 ↗
GroupTheory.Transfer.Witt.wordExponent_of
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem wordExponent_of {X : Type*} (x : X) :
    wordExponent (FreeGroup.of x) =
      Finsupp.single x 1
theorem

wordExponent_inv

L168 ↗
GroupTheory.Transfer.Witt.wordExponent_inv
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem wordExponent_inv {X : Type*} (w : FreeGroup X) :
    wordExponent w⁻¹ = -wordExponent w
theorem

wordExponent_mul

L178 ↗
GroupTheory.Transfer.Witt.wordExponent_mul
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem wordExponent_mul {X : Type*} (u v : FreeGroup X) :
    wordExponent (u * v) =
      wordExponent u + wordExponent v
theorem

exists_rightFoxExpansion

L195 ↗
GroupTheory.Transfer.Witt.exists_rightFoxExpansion
Documentation

A right Fox expansion of a free word, together with the fact that the augmentation of each coefficient is the corresponding exponent sum.

This is the source-producing form needed for Witt's relation matrix.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem exists_rightFoxExpansion
    {X : Type*} [Fintype X]
    (φ : FreeGroup X →* G) (w : FreeGroup X) :
    ∃ μ : X → IntegralGroupRing G,
      groupRingDelta (φ w) =
          ∑ i : X,
            groupRingDelta (φ (FreeGroup.of i)) * μ i ∧
      ∀ i : X,
        augmentation G (μ i) =
          wordExponent w i
def

presentationMap

L269 ↗
GroupTheory.Transfer.Witt.presentationMap
Documentation

The map on free abelianizations induced by a free presentation.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
def presentationMap
    {X : Type*} (φ : FreeGroup X →* G) :
    FreeAbelianGroup X →+
      Additive (Abelianization G)
theorem

presentationMap_of

L276 ↗
GroupTheory.Transfer.Witt.presentationMap_of
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem presentationMap_of
    {X : Type*} (φ : FreeGroup X →* G) (x : X) :
    presentationMap φ (FreeAbelianGroup.of x) =
      Additive.ofMul
        (Abelianization.of (φ (FreeGroup.of x)))
theorem

presentationMap_surjective

L283 ↗
GroupTheory.Transfer.Witt.presentationMap_surjective
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem presentationMap_surjective
    {X : Type*} (φ : FreeGroup X →* G)
    (hφ : Function.Surjective φ) :
    Function.Surjective (presentationMap φ)
def

presentationLinearMap

L299 ↗
GroupTheory.Transfer.Witt.presentationLinearMap
Documentation

The same presentation map, regarded as a ℤ-linear map.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
def presentationLinearMap
    {X : Type*} (φ : FreeGroup X →* G) :
    FreeAbelianGroup X →ₗ[ℤ]
      Additive (Abelianization G)
theorem

presentationLinearMap_apply

L306 ↗
GroupTheory.Transfer.Witt.presentationLinearMap_apply
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem presentationLinearMap_apply
    {X : Type*} (φ : FreeGroup X →* G)
    (a : FreeAbelianGroup X) :
    presentationLinearMap φ a =
      presentationMap φ a
theorem

presentationKernel_finrank_eq

L315 ↗
GroupTheory.Transfer.Witt.presentationKernel_finrank_eq
Documentation

Finite abelianization makes the relation lattice of a finite free presentation have full rank.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem presentationKernel_finrank_eq
    {X : Type*} [Finite X]
    (φ : FreeGroup X →* G)
    [FiniteIndex (commutator G)] :
    Module.finrank ℤ (presentationLinearMap φ).ker =
      Module.finrank ℤ (FreeAbelianGroup X)
def

relationBasis

L357 ↗
GroupTheory.Transfer.Witt.relationBasis
Documentation

A basis of the relation lattice, indexed by the generators.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
def relationBasis
    {X : Type*} [Fintype X]
    (φ : FreeGroup X →* G)
    [FiniteIndex (commutator G)] :
    Module.Basis X ℤ (presentationLinearMap φ).ker
theorem

exists_relationWord

L370 ↗
GroupTheory.Transfer.Witt.exists_relationWord
Documentation

Every vector in the relation lattice is represented by an actual relation word. The correction from a lift to a relation is made inside the commutator subgroup of the free group, so it does not change the free abelianization.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem exists_relationWord
    {X : Type*}
    (φ : FreeGroup X →* G)
    (hφ : Function.Surjective φ)
    (m : (presentationLinearMap φ).ker) :
    ∃ r : FreeGroup X,
      φ r = 1 ∧
      Additive.ofMul (Abelianization.of r) =
        (m : FreeAbelianGroup X)
def

abelianizationRingMap

L428 ↗
GroupTheory.Transfer.Witt.abelianizationRingMap
Documentation

The group-ring map induced by abelianization.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
def abelianizationRingMap :
    IntegralGroupRing G →+*
      IntegralGroupRing (Abelianization G)
theorem

abelianizationRingMap_single

L434 ↗
GroupTheory.Transfer.Witt.abelianizationRingMap_single
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem abelianizationRingMap_single
    (g : G) (n : ℤ) :
    abelianizationRingMap
        (MonoidAlgebra.single g n) =
      MonoidAlgebra.single (Abelianization.of g) n
theorem

abelianizationRingMap_groupRingDelta

L442 ↗
GroupTheory.Transfer.Witt.abelianizationRingMap_groupRingDelta
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem abelianizationRingMap_groupRingDelta
    (g : G) :
    abelianizationRingMap (groupRingDelta g) =
      groupRingDelta (Abelianization.of g)
theorem

augmentation_abelianizationRingMap

L449 ↗
GroupTheory.Transfer.Witt.augmentation_abelianizationRingMap
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem augmentation_abelianizationRingMap
    (x : IntegralGroupRing G) :
    augmentation (Abelianization G)
        (abelianizationRingMap x) =
      augmentation G x
def

abelianizationRingSection

L464 ↗
GroupTheory.Transfer.Witt.abelianizationRingSection
Documentation

An additive section of the group-ring abelianization map, obtained by choosing the quotient representative of every abelianization class.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · full declaration
def abelianizationRingSection :
    IntegralGroupRing (Abelianization G) →+
      IntegralGroupRing G where
  toFun :=
    MonoidAlgebra.mapDomain
      (fun a : Abelianization G => a.out)
  map_zero' := MonoidAlgebra.mapDomain_zero _
  map_add' := MonoidAlgebra.mapDomain_add _
theorem

abelianizationRingSection_single

L474 ↗
GroupTheory.Transfer.Witt.abelianizationRingSection_single
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem abelianizationRingSection_single
    (a : Abelianization G) (n : ℤ) :
    abelianizationRingSection
        (MonoidAlgebra.single a n) =
      MonoidAlgebra.single a.out n
theorem

abelianizationRingMap_section

L482 ↗
GroupTheory.Transfer.Witt.abelianizationRingMap_section
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem abelianizationRingMap_section
    (z : IntegralGroupRing (Abelianization G)) :
    abelianizationRingMap
        (abelianizationRingSection z) = z
theorem

ideal_mul_mem_mixed_of_abelianizationRingMap_eq_zero

L500 ↗
GroupTheory.Transfer.Witt.ideal_mul_mem_mixed_of_abelianizationRingMap_eq_zero
Documentation

Multiplying an element of I_G by an element killed by ℤ[G] → ℤ[Gᵃᵇ] lands in I_G I_{G'}.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem ideal_mul_mem_mixed_of_abelianizationRingMap_eq_zero
    (x y : IntegralGroupRing G)
    (hx : x ∈ ideal G)
    (hy : abelianizationRingMap y = 0) :
    x * y ∈
      mixedAugmentationProduct
        (commutator G)
theorem

mul_mem_mixed

L578 ↗
GroupTheory.Transfer.Witt.mul_mem_mixed
Documentation

The mixed product is stable under left multiplication by arbitrary group-ring elements.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem mul_mem_mixed
    (H : Subgroup G)
    (z m : IntegralGroupRing G)
    (hm : m ∈ mixedAugmentationProduct H) :
    z * m ∈ mixedAugmentationProduct H
theorem

mul_det_eq_zero_of_vecMul_eq_zero

L603 ↗
GroupTheory.Transfer.Witt.mul_det_eq_zero_of_vecMul_eq_zero
Documentation

A row vector annihilating a square matrix is annihilated by its determinant.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem mul_det_eq_zero_of_vecMul_eq_zero
    {R : Type*} [CommRing R]
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (A : Matrix ι ι R) (v : ι → R)
    (h : Matrix.vecMul v A = 0) (i : ι) :
    v i * A.det = 0
def

relationWord

L628 ↗
GroupTheory.Transfer.Witt.relationWord
Documentation

The chosen relation word representing the corresponding relation basis vector.

Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
def relationWord (j : X) :
    FreeGroup X
theorem

relationWord_map

L634 ↗
GroupTheory.Transfer.Witt.relationWord_map
Source context 15 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
omit [DecidableEq X] in
Lean source · statement
theorem relationWord_map (j : X) :
    φ (relationWord φ hφ j) = 1
theorem

relationWord_abelianization

L640 ↗
GroupTheory.Transfer.Witt.relationWord_abelianization
Source context 15 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
omit [DecidableEq X] in
Lean source · statement
theorem relationWord_abelianization (j : X) :
    Additive.ofMul
        (Abelianization.of (relationWord φ hφ j)) =
      ((relationBasis φ j :
        (presentationLinearMap φ).ker) :
          FreeAbelianGroup X)
def

foxCoefficient

L651 ↗
GroupTheory.Transfer.Witt.foxCoefficient
Documentation

The chosen right Fox coefficient of the j-th relation at the i-th generator.

Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
def foxCoefficient (i j : X) :
    IntegralGroupRing G
theorem

foxExpansion_relation

L657 ↗
GroupTheory.Transfer.Witt.foxExpansion_relation
Source context 15 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
omit [DecidableEq X] in
Lean source · statement
theorem foxExpansion_relation (j : X) :
    ∑ i : X,
        groupRingDelta (φ (FreeGroup.of i)) *
          foxCoefficient φ hφ i j =
      0
theorem

augmentation_foxCoefficient

L673 ↗
GroupTheory.Transfer.Witt.augmentation_foxCoefficient
Source context 15 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
omit [DecidableEq X] in
Lean source · statement
theorem augmentation_foxCoefficient (i j : X) :
    augmentation G (foxCoefficient φ hφ i j) =
      wordExponent (relationWord φ hφ j) i
theorem

augmentation_foxCoefficient_eq_repr

L680 ↗
GroupTheory.Transfer.Witt.augmentation_foxCoefficient_eq_repr
Source context 15 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
omit [DecidableEq X] in
Lean source · statement
theorem augmentation_foxCoefficient_eq_repr
    (i j : X) :
    augmentation G (foxCoefficient φ hφ i j) =
      (FreeAbelianGroup.basis X).repr
        (((relationBasis φ j :
          (presentationLinearMap φ).ker) :
            FreeAbelianGroup X)) i
def

foxMatrix

L694 ↗
GroupTheory.Transfer.Witt.foxMatrix
Documentation

Witt's relation matrix, with entries reduced to the group ring of the finite abelianization.

Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
def foxMatrix :
    Matrix X X
      (IntegralGroupRing (Abelianization G))
def

adjugateCoefficientLift

L702 ↗
GroupTheory.Transfer.Witt.adjugateCoefficientLift
Documentation

A chosen lift of an adjugate-matrix entry back to ℤ[G].

Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
def adjugateCoefficientLift (j k : X) :
    IntegralGroupRing G
theorem

abelianizationRingMap_adjugateCoefficientLift

L708 ↗
GroupTheory.Transfer.Witt.abelianizationRingMap_adjugateCoefficientLift
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
theorem abelianizationRingMap_adjugateCoefficientLift
    (j k : X) :
    abelianizationRingMap
        (adjugateCoefficientLift φ hφ j k) =
      (foxMatrix φ hφ).adjugate j k
def

foxDeterminantLift

L716 ↗
GroupTheory.Transfer.Witt.foxDeterminantLift
Documentation

A chosen lift of the determinant.

Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
def foxDeterminantLift :
    IntegralGroupRing G
theorem

abelianizationRingMap_foxDeterminantLift

L721 ↗
GroupTheory.Transfer.Witt.abelianizationRingMap_foxDeterminantLift
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
theorem abelianizationRingMap_foxDeterminantLift :
    abelianizationRingMap
        (foxDeterminantLift φ hφ) =
      (foxMatrix φ hφ).det
def

foxAdjugateCoefficient

L729 ↗
GroupTheory.Transfer.Witt.foxAdjugateCoefficient
Documentation

The coefficients obtained by multiplying the Fox matrix by a lift of its adjugate.

Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
def foxAdjugateCoefficient (i k : X) :
    IntegralGroupRing G
theorem

abelianizationRingMap_foxAdjugateCoefficient

L735 ↗
GroupTheory.Transfer.Witt.abelianizationRingMap_foxAdjugateCoefficient
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · full declaration
theorem abelianizationRingMap_foxAdjugateCoefficient
    (i k : X) :
    abelianizationRingMap
        (foxAdjugateCoefficient φ hφ i k) =
      if i = k then (foxMatrix φ hφ).det else 0 := by
  calc
    abelianizationRingMap
        (foxAdjugateCoefficient φ hφ i k) =
        ∑ j : X,
          foxMatrix φ hφ i j *
            (foxMatrix φ hφ).adjugate j k := by
      simp [foxAdjugateCoefficient, foxMatrix]
    _ = ((foxMatrix φ hφ) *
          (foxMatrix φ hφ).adjugate) i k := by
      rw [Matrix.mul_apply]
    _ = if i = k then
          (foxMatrix φ hφ).det else 0 := by
      rw [Matrix.mul_adjugate]
      simp [Matrix.one_apply]
theorem

foxAdjugate_relation

L755 ↗
GroupTheory.Transfer.Witt.foxAdjugate_relation
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
theorem foxAdjugate_relation (k : X) :
    ∑ i : X,
        groupRingDelta (φ (FreeGroup.of i)) *
          foxAdjugateCoefficient φ hφ i k =
      0
theorem

generator_mul_foxDeterminantLift_mem_mixed

L766 ↗
GroupTheory.Transfer.Witt.generator_mul_foxDeterminantLift_mem_mixed
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
theorem generator_mul_foxDeterminantLift_mem_mixed
    (k : X) :
    groupRingDelta (φ (FreeGroup.of k)) *
        foxDeterminantLift φ hφ ∈
      mixedAugmentationProduct (commutator G)
theorem

delta_vecMul_foxMatrix

L842 ↗
GroupTheory.Transfer.Witt.delta_vecMul_foxMatrix
Source context 15 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
omit [DecidableEq X] in
Lean source · full declaration
theorem delta_vecMul_foxMatrix :
    Matrix.vecMul
        (fun i : X =>
          groupRingDelta
            (Abelianization.of
              (φ (FreeGroup.of i))))
        (foxMatrix φ hφ) =
      0 := by
  funext j
  have h :=
    congrArg abelianizationRingMap
      (foxExpansion_relation φ hφ j)
  simpa [Matrix.vecMul, dotProduct, foxMatrix,
    map_sum] using h
theorem

delta_generator_mul_foxMatrix_det

L857 ↗
GroupTheory.Transfer.Witt.delta_generator_mul_foxMatrix_det
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
theorem delta_generator_mul_foxMatrix_det (i : X) :
    groupRingDelta
          (Abelianization.of
            (φ (FreeGroup.of i))) *
        (foxMatrix φ hφ).det =
      0
theorem

delta_word_mul_foxMatrix_det

L871 ↗
GroupTheory.Transfer.Witt.delta_word_mul_foxMatrix_det
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
theorem delta_word_mul_foxMatrix_det
    (w : FreeGroup X) :
    groupRingDelta
          (Abelianization.of (φ w)) *
        (foxMatrix φ hφ).det =
      0
theorem

delta_mul_foxMatrix_det

L925 ↗
GroupTheory.Transfer.Witt.delta_mul_foxMatrix_det
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
theorem delta_mul_foxMatrix_det
    (a : Abelianization G) :
    groupRingDelta a * (foxMatrix φ hφ).det =
      0
theorem

single_mul_foxMatrix_det

L934 ↗
GroupTheory.Transfer.Witt.single_mul_foxMatrix_det
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
theorem single_mul_foxMatrix_det
    (a : Abelianization G) :
    MonoidAlgebra.single a 1 *
        (foxMatrix φ hφ).det =
      (foxMatrix φ hφ).det
theorem

augmentation_foxMatrix_det

L944 ↗
GroupTheory.Transfer.Witt.augmentation_foxMatrix_det
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · full declaration
theorem augmentation_foxMatrix_det :
    augmentation (Abelianization G)
        (foxMatrix φ hφ).det =
      (FreeAbelianGroup.basis X).det
        (fun j : X =>
          (((relationBasis φ j :
            (presentationLinearMap φ).ker) :
              FreeAbelianGroup X))) := by
  calc
    augmentation (Abelianization G)
        (foxMatrix φ hφ).det =
        (RingHom.mapMatrix
          (augmentation (Abelianization G))
          (foxMatrix φ hφ)).det :=
      RingHom.map_det
        (augmentation (Abelianization G))
        (foxMatrix φ hφ)
    _ = (FreeAbelianGroup.basis X).det
        (fun j : X =>
          (((relationBasis φ j :
            (presentationLinearMap φ).ker) :
              FreeAbelianGroup X))) := by
      rw [Module.Basis.det_apply]
      congr 1
      ext i j
      simp [foxMatrix, Module.Basis.toMatrix_apply,
        augmentation_foxCoefficient_eq_repr]
theorem

natAbs_augmentation_foxMatrix_det

L972 ↗
GroupTheory.Transfer.Witt.natAbs_augmentation_foxMatrix_det
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section Presentation
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
theorem natAbs_augmentation_foxMatrix_det :
    Int.natAbs
        (augmentation (Abelianization G)
          (foxMatrix φ hφ).det) =
      Nat.card (Abelianization G)
def

groupNormElement

L1002 ↗
GroupTheory.Transfer.Witt.groupNormElement
Documentation

The norm element of a finite group.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
def groupNormElement
    (Q : Type*) [Group Q] [Finite Q] :
    IntegralGroupRing Q
theorem

augmentation_groupNormElement

L1009 ↗
GroupTheory.Transfer.Witt.augmentation_groupNormElement
Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem augmentation_groupNormElement
    (Q : Type*) [Group Q] [Finite Q] :
    augmentation Q (groupNormElement Q) =
      Nat.card Q
theorem

abelianizationRingMap_transversalNormElement

L1018 ↗
GroupTheory.Transfer.Witt.abelianizationRingMap_transversalNormElement
Documentation

The image in the abelianized group ring of the sum of any left transversal is the norm element of the abelianization.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem abelianizationRingMap_transversalNormElement
    [FiniteIndex (commutator G)]
    (T : (commutator G).LeftTransversal) :
    abelianizationRingMap
        (transversalNormElement (commutator G) T) =
      groupNormElement (Abelianization G)
theorem

eq_coeff_one_smul_groupNormElement

L1035 ↗
GroupTheory.Transfer.Witt.eq_coeff_one_smul_groupNormElement
Documentation

A left-translation invariant element of a finite group ring is a scalar multiple of the norm element.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem eq_coeff_one_smul_groupNormElement
    {Q : Type*} [Group Q] [Finite Q]
    (z : IntegralGroupRing Q)
    (hz : ∀ q : Q,
      MonoidAlgebra.single q 1 * z = z) :
    z = z.coeff 1 • groupNormElement Q
theorem

exists_unit_foxMatrix_det_eq_smul_norm

L1063 ↗
GroupTheory.Transfer.Witt.exists_unit_foxMatrix_det_eq_smul_norm
Documentation

Witt's determinant is a unit multiple of the norm element of the finite abelianization.

Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section PresentationNorm
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
theorem exists_unit_foxMatrix_det_eq_smul_norm :
    ∃ u : ℤˣ,
      (foxMatrix φ hφ).det =
        (u : ℤ) •
          groupNormElement (Abelianization G)
theorem

exists_unit_foxDeterminantLift_eq_smul_section_norm

L1119 ↗
GroupTheory.Transfer.Witt.exists_unit_foxDeterminantLift_eq_smul_section_norm
Source context 14 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section PresentationNorm
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
Lean source · statement
theorem exists_unit_foxDeterminantLift_eq_smul_section_norm :
    ∃ u : ℤˣ,
      foxDeterminantLift φ hφ =
        (u : ℤ) •
          abelianizationRingSection
            (groupNormElement (Abelianization G))
theorem

generator_mul_section_norm_mem_mixed

L1133 ↗
GroupTheory.Transfer.Witt.generator_mul_section_norm_mem_mixed
Source context 16 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section PresentationNorm
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
omit [Fintype X] [DecidableEq X] in
include hφ in
Lean source · statement
theorem generator_mul_section_norm_mem_mixed [Finite X]
    (k : X) :
    groupRingDelta (φ (FreeGroup.of k)) *
        abelianizationRingSection
          (groupNormElement (Abelianization G)) ∈
      mixedAugmentationProduct (commutator G)
theorem

word_mul_section_norm_mem_mixed

L1186 ↗
GroupTheory.Transfer.Witt.word_mul_section_norm_mem_mixed
Source context 16 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section PresentationNorm
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
omit [Fintype X] [DecidableEq X] in
include hφ in
Lean source · statement
theorem word_mul_section_norm_mem_mixed [Finite X]
    (w : FreeGroup X) :
    groupRingDelta (φ w) *
        abelianizationRingSection
          (groupNormElement (Abelianization G)) ∈
      mixedAugmentationProduct (commutator G)
theorem

delta_mul_section_norm_mem_mixed

L1224 ↗
GroupTheory.Transfer.Witt.delta_mul_section_norm_mem_mixed
Source context 16 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section PresentationNorm
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
omit [Fintype X] [DecidableEq X] in
include hφ in
Lean source · statement
theorem delta_mul_section_norm_mem_mixed [Finite X]
    (g : G) :
    groupRingDelta g *
        abelianizationRingSection
          (groupNormElement (Abelianization G)) ∈
      mixedAugmentationProduct (commutator G)
theorem

delta_mul_transversalNormElement_mem_mixed

L1235 ↗
GroupTheory.Transfer.Witt.delta_mul_transversalNormElement_mem_mixed
Source context 16 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
section PresentationNorm
variable {X : Type*} [Fintype X] [DecidableEq X]
variable (φ : FreeGroup X →* G)
variable (hφ : Function.Surjective φ)
variable [FiniteIndex (commutator G)]
omit [Fintype X] [DecidableEq X] in
include hφ in
Lean source · statement
theorem delta_mul_transversalNormElement_mem_mixed [Finite X]
    (T : (commutator G).LeftTransversal) (g : G) :
    groupRingDelta g *
        transversalNormElement (commutator G) T ∈
      mixedAugmentationProduct (commutator G)
theorem

commutatorTransfer_eq_one_of_finite_abelianization

L1271 ↗
GroupTheory.Transfer.Witt.commutatorTransfer_eq_one_of_finite_abelianization
Documentation

If G is finitely generated and its abelianization is finite, then the commutator transfer G / G' → G' / G'' is trivial.

Source context 9 commands

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

open scoped BigOperators Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace Witt
open GroupTheory.Augmentation
open Subgroup
open GroupTheory.Transfer.RelativeAugmentation
variable {G : Type*} [Group G]
Lean source · statement
theorem commutatorTransfer_eq_one_of_finite_abelianization
    [Group.FG G] [FiniteIndex (commutator G)] :
    commutatorTransfer (G := G) = 1

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