This file develops the actual augmentation quotient I_G / I_G² used in the transfer/augmentation comparison. It is kept separate from the transfer calculation so that the group-ring identities can be reused in the proof of Witt's transfer theorem.
The integral group ring ℤ[G].
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]abbrev IntegralGroupRingThe augmentation homomorphism ℤ[G] → ℤ.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def augmentation : IntegralGroupRing G →+* ℤSurrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem augmentation_single (g : G) (n : ℤ) :
augmentation G (MonoidAlgebra.single g n) = nThe augmentation is the sum of the coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem augmentation_apply (x : IntegralGroupRing G) :
augmentation G x = x.coeff.sum (fun _ n => n) := by
classical
conv_lhs => rw [← MonoidAlgebra.sum_coeff_single x]
rw [map_finsuppSum]
simpThe augmentation ideal I_G.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def ideal : TwoSidedIdeal (IntegralGroupRing G)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem mem_ideal_iff (x : IntegralGroupRing G) :
x ∈ ideal G ↔ augmentation G x = 0The underlying additive subgroup of a two-sided ideal.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def underlyingAddSubgroup
{R : Type*} [NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R) : AddSubgroup R where
carrier := I
zero_mem' := I.zero_mem
add_mem' := I.add_mem
neg_mem' := I.neg_memThe product ideal I_G², generated by products of two augmentation elements.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def square : TwoSidedIdeal (IntegralGroupRing G)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem square_le_ideal :
square G ≤ ideal GI_G² as an additive subgroup of I_G.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def squareInIdeal : AddSubgroup (ideal G) where
carrier := {x | (x : IntegralGroupRing G) ∈ square G}
zero_mem' := (square G).zero_mem
add_mem' := (square G).add_mem
neg_mem' := (square G).neg_memMembership in I_G², expressed after forgetting the ambient augmentation-ideal subtype.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem mem_squareInIdeal_iff (x : ideal G) :
x ∈ squareInIdeal G ↔
(x : IntegralGroupRing G) ∈ square GThe augmentation quotient I_G / I_G².
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]abbrev QuotientThe element g - 1 of the augmentation ideal.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def deltaElement (g : G) : ideal GSurrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaElement_val (g : G) :
(deltaElement G g : IntegralGroupRing G) =
MonoidAlgebra.single g 1 -
MonoidAlgebra.single (1 : G) 1The canonical expression of an augmentation-zero group-ring element as a finite integral linear combination of the differences g - 1.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def deltaCombination (x : IntegralGroupRing G) :
IntegralGroupRing GSurrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaCombination_eq_of_mem_ideal
(x : IntegralGroupRing G) (hx : x ∈ ideal G) :
deltaCombination G x = xThe same finite combination, now intrinsically valued in I_G.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def deltaCombinationElement (x : IntegralGroupRing G) :
ideal GSurrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaCombinationElement_val
(x : IntegralGroupRing G) :
(deltaCombinationElement G x : IntegralGroupRing G) =
deltaCombination G xSurrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaCombinationElement_eq_of_mem_ideal
(x : IntegralGroupRing G) (hx : x ∈ ideal G) :
deltaCombinationElement G x = ⟨x, hx⟩The class of g - 1 in I_G / I_G².
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def deltaClass (g : G) : Quotient GSurrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaClass_one :
deltaClass G 1 = 0Modulo I_G², the identity δ(gh)=δg+δh makes the augmentation class a homomorphism from G to the additive quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaClass_mul (g h : G) :
deltaClass G (g * h) =
deltaClass G g + deltaClass G hMultiplicative spelling of g ↦ δg, convenient for passage through the abelianization.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def deltaMonoidHom :
G →* Multiplicative (Quotient G) where
toFun g := Multiplicative.ofAdd (deltaClass G g)
map_one' := by
apply Multiplicative.toAdd.injective
exact deltaClass_one G
map_mul' g h := by
apply Multiplicative.toAdd.injective
exact deltaClass_mul G g hThe augmentation class factors canonically through Gᵃᵇ.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def deltaAbelianization :
Abelianization G →* Multiplicative (Quotient G)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaAbelianization_of (g : G) :
deltaAbelianization G (Abelianization.of g) =
Multiplicative.ofAdd (deltaClass G g)A finite preimage in Gᵃᵇ for the coefficient combination attached to a group-ring element.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def deltaPreimage (x : IntegralGroupRing G) :
Abelianization GSurrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaAbelianization_deltaPreimage
(x : IntegralGroupRing G) (hx : x ∈ ideal G) :
deltaAbelianization G (deltaPreimage G x) =
Multiplicative.ofAdd
(QuotientAddGroup.mk' (squareInIdeal G) ⟨x, hx⟩)The augmentation map Gᵃᵇ → I_G/I_G² is surjective.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaAbelianization_surjective :
Function.Surjective (deltaAbelianization G)A coefficient at g contributes that many copies of the class of g in the abelianization.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def coefficientToAbelianization (g : G) :
ℤ →+ Additive (Abelianization G) where
toFun n := n • Additive.ofMul (Abelianization.of g)
map_zero' := zero_zsmul _
map_add' m n := add_zsmul _ m nLinearization of the integral group ring in the abelianization.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def linearization :
IntegralGroupRing G →+ Additive (Abelianization G)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem linearization_single (g : G) (n : ℤ) :
linearization G (MonoidAlgebra.single g n) =
n • Additive.ofMul (Abelianization.of g)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem linearization_deltaElement (g : G) :
linearization G (deltaElement G g) =
Additive.ofMul (Abelianization.of g)Products of two basic augmentation differences vanish after linearization.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem linearization_deltaElement_mul_deltaElement
(g h : G) :
linearization G
((deltaElement G g : IntegralGroupRing G) *
(deltaElement G h : IntegralGroupRing G)) =
0Linearization kills a product of two augmentation-zero elements.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem linearization_mul_eq_zero_of_mem_ideal
(x y : IntegralGroupRing G)
(hx : x ∈ ideal G) (hy : y ∈ ideal G) :
linearization G (x * y) = 0Linearization vanishes on the square of the augmentation ideal.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem linearization_eq_zero_of_mem_square
(z : IntegralGroupRing G) (hz : z ∈ square G) :
linearization G z = 0Linearization restricted to the augmentation ideal.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def linearizationOnIdeal :
ideal G →+ Additive (Abelianization G) where
toFun x := linearization G (x : IntegralGroupRing G)
map_zero' := (linearization G).map_zero
map_add' x y := (linearization G).map_add x yThe inverse linearization map on I_G/I_G².
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def quotientLinearization :
Quotient G →+ Additive (Abelianization G)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem quotientLinearization_deltaClass (g : G) :
quotientLinearization G (deltaClass G g) =
Additive.ofMul (Abelianization.of g)Multiplicative spelling of inverse linearization.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def quotientLinearizationMonoidHom :
Multiplicative (Quotient G) →* Abelianization GSurrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem quotientLinearizationMonoidHom_deltaClass (g : G) :
quotientLinearizationMonoidHom G
(Multiplicative.ofAdd (deltaClass G g)) =
Abelianization.of gInverse linearization is a left inverse to the augmentation-class map.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem quotientLinearizationMonoidHom_deltaAbelianization
(a : Abelianization G) :
quotientLinearizationMonoidHom G
(deltaAbelianization G a) =
aThe canonical augmentation-class map is injective.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaAbelianization_injective :
Function.Injective (deltaAbelianization G)The classical canonical isomorphism Gᵃᵇ ≃ I_G/I_G², in multiplicative notation on the target.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]def deltaAbelianizationEquiv :
Abelianization G ≃* Multiplicative (Quotient G)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaAbelianizationEquiv_apply (a : Abelianization G) :
deltaAbelianizationEquiv G a =
deltaAbelianization G aSurrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaAbelianizationEquiv_of (g : G) :
deltaAbelianizationEquiv G (Abelianization.of g) =
Multiplicative.ofAdd (deltaClass G g)Every commutator has zero augmentation class modulo I_G².
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Augmentation
variable (G : Type*) [Group G]theorem deltaClass_eq_zero_of_mem_commutator
{g : G} (hg : g ∈ commutator G) :
deltaClass G g = 0