Module

RelativeAugmentation.lean

Nyll.GaloisCohomology.GroupTheory.Transfer.RelativeAugmentation

74 declarations indexed from sourceView source ↗

Module documentation

Transfer and relative augmentation quotients

This file constructs the transfer on abelianizations and the concrete relative augmentation quotient

(I_H + I_G I_H) / I_G I_H.

The two vertical augmentation maps in the transfer square are developed from the integral group rings themselves.

Imports3

Nyll.GaloisCohomology.GroupTheory.Augmentation
Mathlib.Algebra.MonoidAlgebra.MapDomain
Mathlib.GroupTheory.Transfer

Imported by2

def

transferToAbelianization

L39 ↗

GroupTheory.Transfer.RelativeAugmentation.transferToAbelianization

Documentation

Transfer from G to the abelianization of a finite-index subgroup.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def transferToAbelianization
    (H : Subgroup G) [H.FiniteIndex] :
    G →* Abelianization H

def

abelianizedTransfer

L45 ↗

GroupTheory.Transfer.RelativeAugmentation.abelianizedTransfer

Documentation

The transfer factors through the abelianization of G.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def abelianizedTransfer
    (H : Subgroup G) [H.FiniteIndex] :
    Abelianization G →* Abelianization H

theorem

abelianizedTransfer_of

L51 ↗

GroupTheory.Transfer.RelativeAugmentation.abelianizedTransfer_of

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem abelianizedTransfer_of
    (H : Subgroup G) [H.FiniteIndex] (g : G) :
    abelianizedTransfer H (Abelianization.of g) =
      transferToAbelianization H g

theorem

abelianizedTransfer_of_eq_diff

L59 ↗

GroupTheory.Transfer.RelativeAugmentation.abelianizedTransfer_of_eq_diff

Documentation

The explicit transversal formula for the top horizontal map in the relative augmentation construction.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem abelianizedTransfer_of_eq_diff
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal) (g : G) :
    abelianizedTransfer H (Abelianization.of g) =
      Subgroup.leftTransversals.diff
        (Abelianization.of : H →* Abelianization H)
        T (g • T)

def

subgroupRingMap

L70 ↗

GroupTheory.Transfer.RelativeAugmentation.subgroupRingMap

Documentation

The inclusion of the subgroup ring ℤ[H] into ℤ[G].

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def subgroupRingMap (H : Subgroup G) :
    IntegralGroupRing H →+* IntegralGroupRing G

theorem

subgroupRingMap_single

L75 ↗

GroupTheory.Transfer.RelativeAugmentation.subgroupRingMap_single

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem subgroupRingMap_single
    (H : Subgroup G) (h : H) (n : ℤ) :
    subgroupRingMap H (MonoidAlgebra.single h n) =
      MonoidAlgebra.single (h : G) n

theorem

subgroupRingMap_injective

L81 ↗

GroupTheory.Transfer.RelativeAugmentation.subgroupRingMap_injective

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem subgroupRingMap_injective
    (H : Subgroup G) :
    Function.Injective (subgroupRingMap H)

def

subgroupIdealEmbedding

L87 ↗

GroupTheory.Transfer.RelativeAugmentation.subgroupIdealEmbedding

Documentation

The additive embedding I_H → ℤ[G].

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · full declaration

def subgroupIdealEmbedding (H : Subgroup G) :
    ideal H →+ IntegralGroupRing G where
  toFun x := subgroupRingMap H (x : IntegralGroupRing H)
  map_zero' := (subgroupRingMap H).map_zero
  map_add' x y := (subgroupRingMap H).map_add x y

theorem

subgroupIdealEmbedding_injective

L93 ↗

GroupTheory.Transfer.RelativeAugmentation.subgroupIdealEmbedding_injective

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem subgroupIdealEmbedding_injective
    (H : Subgroup G) :
    Function.Injective (subgroupIdealEmbedding H)

theorem

subgroupIdealEmbedding_apply

L102 ↗

GroupTheory.Transfer.RelativeAugmentation.subgroupIdealEmbedding_apply

Documentation

Evaluation of the subgroup-ideal embedding in the ambient group ring.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem subgroupIdealEmbedding_apply
    (H : Subgroup G) (x : ideal H) :
    subgroupIdealEmbedding H x =
      subgroupRingMap H (x : IntegralGroupRing H)

def

embeddedSubgroupIdeal

L109 ↗

GroupTheory.Transfer.RelativeAugmentation.embeddedSubgroupIdeal

Documentation

The embedded copy of I_H in ℤ[G].

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def embeddedSubgroupIdeal (H : Subgroup G) :
    AddSubgroup (IntegralGroupRing G)

def

mixedAugmentationProduct

L114 ↗

GroupTheory.Transfer.RelativeAugmentation.mixedAugmentationProduct

Documentation

The additive product I_G I_H occurring in the relative augmentation construction.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def mixedAugmentationProduct (H : Subgroup G) :
    AddSubgroup (IntegralGroupRing G)

def

relativeAugmentationNumerator

L121 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeAugmentationNumerator

Documentation

The numerator I_H + I_G I_H.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def relativeAugmentationNumerator (H : Subgroup G) :
    AddSubgroup (IntegralGroupRing G)

def

mixedProductInNumerator

L126 ↗

GroupTheory.Transfer.RelativeAugmentation.mixedProductInNumerator

Documentation

The denominator, viewed inside the numerator.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · full declaration

def mixedProductInNumerator (H : Subgroup G) :
    AddSubgroup (relativeAugmentationNumerator H) where
  carrier :=
    {x | (x : IntegralGroupRing G) ∈ mixedAugmentationProduct H}
  zero_mem' := (mixedAugmentationProduct H).zero_mem
  add_mem' := (mixedAugmentationProduct H).add_mem
  neg_mem' := (mixedAugmentationProduct H).neg_mem

theorem

mem_mixedProductInNumerator_iff

L137 ↗

GroupTheory.Transfer.RelativeAugmentation.mem_mixedProductInNumerator_iff

Documentation

Membership in the mixed product after forgetting the relative-numerator subtype.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem mem_mixedProductInNumerator_iff
    (H : Subgroup G) (x : relativeAugmentationNumerator H) :
    x ∈ mixedProductInNumerator H ↔
      (x : IntegralGroupRing G) ∈ mixedAugmentationProduct H

abbrev

RelativeAugmentationQuotient

L144 ↗

GroupTheory.Transfer.RelativeAugmentation.RelativeAugmentationQuotient

Documentation

The lower-right group in the diagram of the relative augmentation construction.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

abbrev RelativeAugmentationQuotient (H : Subgroup G)

def

embeddedDelta

L148 ↗

GroupTheory.Transfer.RelativeAugmentation.embeddedDelta

Documentation

The element h - 1, embedded from ℤ[H] into ℤ[G].

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def embeddedDelta (H : Subgroup G) (h : H) :
    IntegralGroupRing G

theorem

embeddedDelta_eq

L153 ↗

GroupTheory.Transfer.RelativeAugmentation.embeddedDelta_eq

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem embeddedDelta_eq (H : Subgroup G) (h : H) :
    embeddedDelta H h =
      (deltaElement G (h : G) : IntegralGroupRing G)

theorem

embeddedDelta_mem_ideal

L158 ↗

GroupTheory.Transfer.RelativeAugmentation.embeddedDelta_mem_ideal

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem embeddedDelta_mem_ideal
    (H : Subgroup G) (h : H) :
    embeddedDelta H h ∈ ideal G

theorem

embeddedDelta_mem_embeddedSubgroupIdeal

L164 ↗

GroupTheory.Transfer.RelativeAugmentation.embeddedDelta_mem_embeddedSubgroupIdeal

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem embeddedDelta_mem_embeddedSubgroupIdeal
    (H : Subgroup G) (h : H) :
    embeddedDelta H h ∈ embeddedSubgroupIdeal H

def

relativeDeltaElement

L170 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaElement

Documentation

The relative augmentation element in the numerator.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def relativeDeltaElement (H : Subgroup G) (h : H) :
    relativeAugmentationNumerator H

def

relativeDeltaClass

L178 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaClass

Documentation

The class of h - 1 in (I_H + I_G I_H) / I_G I_H.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def relativeDeltaClass (H : Subgroup G) (h : H) :
    RelativeAugmentationQuotient H

theorem

relativeDeltaClass_one

L184 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaClass_one

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem relativeDeltaClass_one (H : Subgroup G) :
    relativeDeltaClass H 1 = 0

theorem

relativeDeltaClass_mul

L193 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaClass_mul

Documentation

The relative identity δ(hk)=δh+δk modulo I_G I_H.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem relativeDeltaClass_mul
    (H : Subgroup G) (h k : H) :
    relativeDeltaClass H (h * k) =
      relativeDeltaClass H h + relativeDeltaClass H k

def

relativeDeltaMonoidHom

L223 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaMonoidHom

Documentation

Multiplicative form of the relative augmentation map.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · full declaration

def relativeDeltaMonoidHom (H : Subgroup G) :
    H →* Multiplicative (RelativeAugmentationQuotient H) where
  toFun h := Multiplicative.ofAdd (relativeDeltaClass H h)
  map_one' := by
    apply Multiplicative.toAdd.injective
    exact relativeDeltaClass_one H
  map_mul' h k := by
    apply Multiplicative.toAdd.injective
    exact relativeDeltaClass_mul H h k

def

relativeDeltaAbelianization

L234 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaAbelianization

Documentation

The right vertical augmentation map in the relative augmentation construction.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def relativeDeltaAbelianization (H : Subgroup G) :
    Abelianization H →*
      Multiplicative (RelativeAugmentationQuotient H)

theorem

relativeDeltaAbelianization_of

L240 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaAbelianization_of

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem relativeDeltaAbelianization_of
    (H : Subgroup G) (h : H) :
    relativeDeltaAbelianization H (Abelianization.of h) =
      Multiplicative.ofAdd (relativeDeltaClass H h)

def

transversalComponent

L247 ↗

GroupTheory.Transfer.RelativeAugmentation.transversalComponent

Documentation

The H-component of g with respect to a left transversal.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def transversalComponent
    (H : Subgroup G) (T : H.LeftTransversal) (g : G) : H

theorem

transversalComponent_mul_right

L252 ↗

GroupTheory.Transfer.RelativeAugmentation.transversalComponent_mul_right

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem transversalComponent_mul_right
    (H : Subgroup G) (T : H.LeftTransversal)
    (g : G) (h : H) :
    transversalComponent H T (g * (h : G)) =
      transversalComponent H T g * h

def

transversalCoefficientToAbelianization

L278 ↗

GroupTheory.Transfer.RelativeAugmentation.transversalCoefficientToAbelianization

Documentation

A coefficient at g records its transversal H-component in Hᵃᵇ.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · full declaration

def transversalCoefficientToAbelianization
    (H : Subgroup G) (T : H.LeftTransversal) (g : G) :
    ℤ →+ Additive (Abelianization H) where
  toFun n :=
    n • Additive.ofMul
      (Abelianization.of (transversalComponent H T g))
  map_zero' := zero_zsmul _
  map_add' _ _ := add_zsmul _ _ _

def

transversalLinearization

L288 ↗

GroupTheory.Transfer.RelativeAugmentation.transversalLinearization

Documentation

Transversal linearization of ℤ[G] in Hᵃᵇ.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def transversalLinearization
    (H : Subgroup G) (T : H.LeftTransversal) :
    IntegralGroupRing G →+ Additive (Abelianization H)

theorem

transversalLinearization_single

L298 ↗

GroupTheory.Transfer.RelativeAugmentation.transversalLinearization_single

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem transversalLinearization_single
    (H : Subgroup G) (T : H.LeftTransversal)
    (g : G) (n : ℤ) :
    transversalLinearization H T
        (MonoidAlgebra.single g n) =
      n • Additive.ofMul
        (Abelianization.of (transversalComponent H T g))

theorem

transversalLinearization_embeddedDelta

L311 ↗

GroupTheory.Transfer.RelativeAugmentation.transversalLinearization_embeddedDelta

Documentation

On the embedded subgroup ideal, transversal linearization is the ordinary abelianization linearization.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem transversalLinearization_embeddedDelta
    (H : Subgroup G) (T : H.LeftTransversal) (h : H) :
    transversalLinearization H T (embeddedDelta H h) =
      Additive.ofMul (Abelianization.of h)

theorem

transversalLinearization_delta_mul_embeddedDelta

L326 ↗

GroupTheory.Transfer.RelativeAugmentation.transversalLinearization_delta_mul_embeddedDelta

Documentation

A basic generator of I_G I_H is killed by transversal linearization.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem transversalLinearization_delta_mul_embeddedDelta
    (H : Subgroup G) (T : H.LeftTransversal)
    (g : G) (h : H) :
    transversalLinearization H T
        ((deltaElement G g : IntegralGroupRing G) *
          embeddedDelta H h) =
      0

theorem

transversalLinearization_mul_eq_zero

L352 ↗

GroupTheory.Transfer.RelativeAugmentation.transversalLinearization_mul_eq_zero

Documentation

Transversal linearization kills a product of an augmentation-zero element of ℤ[G] with an embedded augmentation-zero element of ℤ[H].

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem transversalLinearization_mul_eq_zero
    (H : Subgroup G) (T : H.LeftTransversal)
    (x : IntegralGroupRing G) (hx : x ∈ ideal G)
    (y : IntegralGroupRing G) (hy : y ∈ embeddedSubgroupIdeal H) :
    transversalLinearization H T (x * y) = 0

theorem

transversalLinearization_eq_zero_of_mem_mixed

L382 ↗

GroupTheory.Transfer.RelativeAugmentation.transversalLinearization_eq_zero_of_mem_mixed

Documentation

Transversal linearization vanishes on I_G I_H.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem transversalLinearization_eq_zero_of_mem_mixed
    (H : Subgroup G) (T : H.LeftTransversal)
    (z : IntegralGroupRing G)
    (hz : z ∈ mixedAugmentationProduct H) :
    transversalLinearization H T z = 0

def

relativeLinearizationOnNumerator

L402 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeLinearizationOnNumerator

Documentation

Transversal linearization restricted to I_H + I_G I_H.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · full declaration

def relativeLinearizationOnNumerator
    (H : Subgroup G) (T : H.LeftTransversal) :
    relativeAugmentationNumerator H →+
      Additive (Abelianization H) where
  toFun x :=
    transversalLinearization H T
      (x : IntegralGroupRing G)
  map_zero' := (transversalLinearization H T).map_zero
  map_add' x y := (transversalLinearization H T).map_add x y

def

relativeQuotientLinearization

L413 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeQuotientLinearization

Documentation

The inverse linearization on the relative augmentation quotient.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def relativeQuotientLinearization
    (H : Subgroup G) (T : H.LeftTransversal) :
    RelativeAugmentationQuotient H →+
      Additive (Abelianization H)

theorem

relativeQuotientLinearization_deltaClass

L426 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeQuotientLinearization_deltaClass

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem relativeQuotientLinearization_deltaClass
    (H : Subgroup G) (T : H.LeftTransversal) (h : H) :
    relativeQuotientLinearization H T
        (relativeDeltaClass H h) =
      Additive.ofMul (Abelianization.of h)

def

relativeQuotientLinearizationMonoidHom

L434 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeQuotientLinearizationMonoidHom

Documentation

Multiplicative form of inverse relative linearization.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def relativeQuotientLinearizationMonoidHom
    (H : Subgroup G) (T : H.LeftTransversal) :
    Multiplicative (RelativeAugmentationQuotient H) →*
      Abelianization H

theorem

relativeQuotientLinearizationMonoidHom_deltaClass

L441 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeQuotientLinearizationMonoidHom_deltaClass

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem relativeQuotientLinearizationMonoidHom_deltaClass
    (H : Subgroup G) (T : H.LeftTransversal) (h : H) :
    relativeQuotientLinearizationMonoidHom H T
        (Multiplicative.ofAdd (relativeDeltaClass H h)) =
      Abelianization.of h

theorem

relativeQuotientLinearizationMonoidHom_deltaAbelianization

L449 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeQuotientLinearizationMonoidHom_deltaAbelianization

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem relativeQuotientLinearizationMonoidHom_deltaAbelianization
    (H : Subgroup G) (T : H.LeftTransversal)
    (a : Abelianization H) :
    relativeQuotientLinearizationMonoidHom H T
        (relativeDeltaAbelianization H a) =
      a

theorem

relativeDeltaAbelianization_injective

L462 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaAbelianization_injective

Documentation

The right vertical augmentation map is injective.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem relativeDeltaAbelianization_injective
    (H : Subgroup G) :
    Function.Injective (relativeDeltaAbelianization H)

def

embeddedIdealElement

L479 ↗

GroupTheory.Transfer.RelativeAugmentation.embeddedIdealElement

Documentation

An embedded augmentation-ideal element, intrinsically valued in the relative numerator.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def embeddedIdealElement
    (H : Subgroup G) (x : IntegralGroupRing H)
    (hx : x ∈ ideal H) :
    relativeAugmentationNumerator H

theorem

relativeDeltaAbelianization_deltaPreimage

L490 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaAbelianization_deltaPreimage

Documentation

The coefficient expression supplies a preimage for every embedded augmentation-ideal element.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem relativeDeltaAbelianization_deltaPreimage
    (H : Subgroup G) (x : IntegralGroupRing H)
    (hx : x ∈ ideal H) :
    relativeDeltaAbelianization H (deltaPreimage H x) =
      Multiplicative.ofAdd
        (QuotientAddGroup.mk' (mixedProductInNumerator H)
          (embeddedIdealElement H x hx))

theorem

relativeDeltaAbelianization_surjective

L538 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaAbelianization_surjective

Documentation

The right vertical augmentation map is surjective.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem relativeDeltaAbelianization_surjective
    (H : Subgroup G) :
    Function.Surjective (relativeDeltaAbelianization H)

def

relativeDeltaAbelianizationEquiv

L572 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaAbelianizationEquiv

Documentation

The right vertical isomorphism in the diagram of the relative augmentation construction.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def relativeDeltaAbelianizationEquiv
    (H : Subgroup G) :
    Abelianization H ≃*
      Multiplicative (RelativeAugmentationQuotient H)

theorem

relativeDeltaAbelianizationEquiv_apply

L581 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaAbelianizationEquiv_apply

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem relativeDeltaAbelianizationEquiv_apply
    (H : Subgroup G) (a : Abelianization H) :
    relativeDeltaAbelianizationEquiv H a =
      relativeDeltaAbelianization H a

theorem

relativeDeltaAbelianizationEquiv_of

L588 ↗

GroupTheory.Transfer.RelativeAugmentation.relativeDeltaAbelianizationEquiv_of

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem relativeDeltaAbelianizationEquiv_of
    (H : Subgroup G) (h : H) :
    relativeDeltaAbelianizationEquiv H
        (Abelianization.of h) =
      Multiplicative.ofAdd (relativeDeltaClass H h)

def

augmentationTransfer

L598 ↗

GroupTheory.Transfer.RelativeAugmentation.augmentationTransfer

Documentation

The lower horizontal map in the relative augmentation construction, obtained from transfer through the two canonical augmentation isomorphisms.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def augmentationTransfer
    (H : Subgroup G) [H.FiniteIndex] :
    Multiplicative (Quotient G) →*
      Multiplicative (RelativeAugmentationQuotient H)

theorem

augmentationTransfer_apply

L609 ↗

GroupTheory.Transfer.RelativeAugmentation.augmentationTransfer_apply

Documentation

Evaluation of the lower transfer map before using the augmentation isomorphism.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem augmentationTransfer_apply
    (H : Subgroup G) [H.FiniteIndex]
    (q : Multiplicative (Quotient G)) :
    augmentationTransfer H q =
      relativeDeltaAbelianization H
        (abelianizedTransfer H
          ((deltaAbelianizationEquiv G).symm q))

theorem

augmentationTransfer_deltaAbelianization

L619 ↗

GroupTheory.Transfer.RelativeAugmentation.augmentationTransfer_deltaAbelianization

Documentation

Commutativity of the transfer/augmentation square.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem augmentationTransfer_deltaAbelianization
    (H : Subgroup G) [H.FiniteIndex]
    (a : Abelianization G) :
    augmentationTransfer H (deltaAbelianization G a) =
      relativeDeltaAbelianization H
        (abelianizedTransfer H a)

theorem

augmentationTransfer_deltaClass

L630 ↗

GroupTheory.Transfer.RelativeAugmentation.augmentationTransfer_deltaClass

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem augmentationTransfer_deltaClass
    (H : Subgroup G) [H.FiniteIndex] (g : G) :
    augmentationTransfer H
        (Multiplicative.ofAdd (deltaClass G g)) =
      relativeDeltaAbelianization H
        (transferToAbelianization H g)

def

leftRepresentative

L641 ↗

GroupTheory.Transfer.RelativeAugmentation.leftRepresentative

Documentation

The representative of a left coset selected by T.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def leftRepresentative
    (H : Subgroup G) (T : H.LeftTransversal)
    (q : G ⧸ H) : G

def

transferComponent

L647 ↗

GroupTheory.Transfer.RelativeAugmentation.transferComponent

Documentation

The H-factor comparing T with its translate by g.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def transferComponent
    (H : Subgroup G) (T : H.LeftTransversal)
    (g : G) (q : G ⧸ H) : H

theorem

leftRepresentative_mul_transferComponent

L657 ↗

GroupTheory.Transfer.RelativeAugmentation.leftRepresentative_mul_transferComponent

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem leftRepresentative_mul_transferComponent
    (H : Subgroup G) (T : H.LeftTransversal)
    (g : G) (q : G ⧸ H) :
    leftRepresentative H T q *
        (transferComponent H T g q : G) =
      leftRepresentative H (g • T) q

theorem

abelianizedTransfer_of_eq_prod_transferComponent

L666 ↗

GroupTheory.Transfer.RelativeAugmentation.abelianizedTransfer_of_eq_prod_transferComponent

Documentation

The transfer is the product of the transversal components.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · full declaration

theorem abelianizedTransfer_of_eq_prod_transferComponent
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal) (g : G) :
    abelianizedTransfer H (Abelianization.of g) =
      letI := H.fintypeQuotientOfFiniteIndex
      ∏ q : G ⧸ H,
        Abelianization.of (transferComponent H T g q) := by
  let := H.fintypeQuotientOfFiniteIndex
  rw [abelianizedTransfer_of_eq_diff H T g]
  rfl

def

transversalNormElement

L678 ↗

GroupTheory.Transfer.RelativeAugmentation.transversalNormElement

Documentation

The group-ring norm element attached to a left transversal.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def transversalNormElement
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal) :
    IntegralGroupRing G

theorem

sum_shifted_leftRepresentatives

L687 ↗

GroupTheory.Transfer.RelativeAugmentation.sum_shifted_leftRepresentatives

Documentation

Translating a transversal translates its group-ring sum.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · full declaration

theorem sum_shifted_leftRepresentatives
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal) (g : G) :
    letI := H.fintypeQuotientOfFiniteIndex
    ∑ q : G ⧸ H,
        MonoidAlgebra.single
          (leftRepresentative H (g • T) q) (1 : ℤ) =
      MonoidAlgebra.single g 1 *
        transversalNormElement H T := by
  let := H.fintypeQuotientOfFiniteIndex
  calc
    ∑ q : G ⧸ H,
        MonoidAlgebra.single
          (leftRepresentative H (g • T) q) (1 : ℤ) =
        ∑ q : G ⧸ H,
          MonoidAlgebra.single
            (leftRepresentative H (g • T) (g • q)) 1 := by
              exact
                (Equiv.sum_comp (MulAction.toPerm g)
                  (fun q : G ⧸ H =>
                    MonoidAlgebra.single
                      (leftRepresentative H (g • T) q)
                      (1 : ℤ))).symm
    _ = ∑ q : G ⧸ H,
          MonoidAlgebra.single
            (g * leftRepresentative H T q) 1 := by
              apply Finset.sum_congr rfl
              intro q _
              congr 2
              exact
                (Subgroup.smul_leftQuotientEquiv
                  g T q).symm
    _ = MonoidAlgebra.single g 1 *
        transversalNormElement H T := by
          simp [transversalNormElement,
            Finset.mul_sum]

theorem

single_mul_embeddedDelta_mem_numerator

L726 ↗

GroupTheory.Transfer.RelativeAugmentation.single_mul_embeddedDelta_mem_numerator

Documentation

Multiplying an embedded augmentation difference by a transversal representative stays in I_H + I_G I_H.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem single_mul_embeddedDelta_mem_numerator
    (H : Subgroup G) (r : G) (h : H) :
    MonoidAlgebra.single r 1 * embeddedDelta H h ∈
      relativeAugmentationNumerator H

theorem

delta_mul_transversalNormElement_mem_numerator

L756 ↗

GroupTheory.Transfer.RelativeAugmentation.delta_mul_transversalNormElement_mem_numerator

Documentation

The group-ring element δg · ∑ρ belongs to the relative augmentation numerator.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem delta_mul_transversalNormElement_mem_numerator
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal) (g : G) :
    (deltaElement G g : IntegralGroupRing G) *
        transversalNormElement H T ∈
      relativeAugmentationNumerator H

theorem

delta_mul_transversalNormElement_eq_sum

L785 ↗

GroupTheory.Transfer.RelativeAugmentation.delta_mul_transversalNormElement_eq_sum

Documentation

The group-ring identity underlying the norm-element formula.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · full declaration

theorem delta_mul_transversalNormElement_eq_sum
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal) (g : G) :
    letI := H.fintypeQuotientOfFiniteIndex
    (deltaElement G g : IntegralGroupRing G) *
        transversalNormElement H T =
      ∑ q : G ⧸ H,
        MonoidAlgebra.single
            (leftRepresentative H T q) 1 *
          embeddedDelta H (transferComponent H T g q) := by
  let := H.fintypeQuotientOfFiniteIndex
  simp only [embeddedDelta_eq, deltaElement_val]
  simp_rw [mul_sub]
  rw [Finset.sum_sub_distrib]
  simp_rw [MonoidAlgebra.single_mul_single]
  simp only [mul_one]
  simp_rw [leftRepresentative_mul_transferComponent H T g]
  rw [sum_shifted_leftRepresentatives H T g]
  simp [transversalNormElement, sub_mul, Finset.mul_sum]

def

singleMulEmbeddedDeltaElement

L807 ↗

GroupTheory.Transfer.RelativeAugmentation.singleMulEmbeddedDeltaElement

Documentation

A single summand in the norm formula, intrinsically valued in the relative numerator.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def singleMulEmbeddedDeltaElement
    (H : Subgroup G) (r : G) (h : H) :
    relativeAugmentationNumerator H

theorem

mk_singleMulEmbeddedDeltaElement_eq_relativeDeltaClass

L815 ↗

GroupTheory.Transfer.RelativeAugmentation.mk_singleMulEmbeddedDeltaElement_eq_relativeDeltaClass

Documentation

Multiplying by a representative does not change an embedded augmentation class modulo I_G I_H.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem mk_singleMulEmbeddedDeltaElement_eq_relativeDeltaClass
    (H : Subgroup G) (r : G) (h : H) :
    QuotientAddGroup.mk' (mixedProductInNumerator H)
        (singleMulEmbeddedDeltaElement H r h) =
      relativeDeltaClass H h

def

deltaNormElement

L842 ↗

GroupTheory.Transfer.RelativeAugmentation.deltaNormElement

Documentation

The element δg · ∑ρ, intrinsically in the relative numerator.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def deltaNormElement
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal) (g : G) :
    relativeAugmentationNumerator H

def

deltaNormClass

L851 ↗

GroupTheory.Transfer.RelativeAugmentation.deltaNormClass

Documentation

Its class in the lower-right quotient.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def deltaNormClass
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal) (g : G) :
    RelativeAugmentationQuotient H

theorem

deltaNormClass_eq_zero_iff

L860 ↗

GroupTheory.Transfer.RelativeAugmentation.deltaNormClass_eq_zero_iff

Documentation

Evaluation of vanishing for the norm class in the concrete mixed augmentation product.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem deltaNormClass_eq_zero_iff
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal) (g : G) :
    deltaNormClass H T g = 0 ↔
      (deltaElement G g : IntegralGroupRing G) *
          transversalNormElement H T ∈
        mixedAugmentationProduct H

theorem

sum_relativeDeltaClass_transferComponent_eq_deltaNormClass

L871 ↗

GroupTheory.Transfer.RelativeAugmentation.sum_relativeDeltaClass_transferComponent_eq_deltaNormClass

Documentation

The sum of transfer-component augmentation classes is the class of δg · ∑ρ.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · full declaration

theorem sum_relativeDeltaClass_transferComponent_eq_deltaNormClass
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal) (g : G) :
    letI := H.fintypeQuotientOfFiniteIndex
    ∑ q : G ⧸ H,
        relativeDeltaClass H (transferComponent H T g q) =
      deltaNormClass H T g := by
  let := H.fintypeQuotientOfFiniteIndex
  calc
    ∑ q : G ⧸ H,
        relativeDeltaClass H (transferComponent H T g q) =
        ∑ q : G ⧸ H,
          QuotientAddGroup.mk' (mixedProductInNumerator H)
            (singleMulEmbeddedDeltaElement H
              (leftRepresentative H T q)
              (transferComponent H T g q)) := by
                apply Finset.sum_congr rfl
                intro q _
                exact
                  (mk_singleMulEmbeddedDeltaElement_eq_relativeDeltaClass
                    H (leftRepresentative H T q)
                    (transferComponent H T g q)).symm
    _ = QuotientAddGroup.mk' (mixedProductInNumerator H)
          (∑ q : G ⧸ H,
            singleMulEmbeddedDeltaElement H
              (leftRepresentative H T q)
              (transferComponent H T g q)) := by
            rw [map_sum]
    _ = deltaNormClass H T g := by
      apply congrArg
        (QuotientAddGroup.mk' (mixedProductInNumerator H))
      apply Subtype.ext
      simpa [singleMulEmbeddedDeltaElement,
        deltaNormElement] using
          (delta_mul_transversalNormElement_eq_sum
            H T g).symm

theorem

augmentationTransfer_deltaClass_eq_deltaNorm

L911 ↗

GroupTheory.Transfer.RelativeAugmentation.augmentationTransfer_deltaClass_eq_deltaNorm

Documentation

The norm-element formula. On the class of g-1, the lower horizontal map is multiplication by the sum of a left transversal.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem augmentationTransfer_deltaClass_eq_deltaNorm
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal) (g : G) :
    augmentationTransfer H
        (Multiplicative.ofAdd (deltaClass G g)) =
      Multiplicative.ofAdd (deltaNormClass H T g)

theorem

ideal_mul_transversalNormElement_mem_numerator

L927 ↗

GroupTheory.Transfer.RelativeAugmentation.ideal_mul_transversalNormElement_mem_numerator

Documentation

Multiplication of an arbitrary augmentation-zero group-ring element by the transversal norm stays in the relative numerator.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem ideal_mul_transversalNormElement_mem_numerator
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal)
    (x : IntegralGroupRing G) (hx : x ∈ ideal G) :
    x * transversalNormElement H T ∈
      relativeAugmentationNumerator H

def

idealNormElement

L946 ↗

GroupTheory.Transfer.RelativeAugmentation.idealNormElement

Documentation

The group-ring norm multiple of x, intrinsically in the relative numerator.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def idealNormElement
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal)
    (x : IntegralGroupRing G) (hx : x ∈ ideal G) :
    relativeAugmentationNumerator H

def

idealNormClass

L956 ↗

GroupTheory.Transfer.RelativeAugmentation.idealNormClass

Documentation

The class of x · ∑ρ in the relative augmentation quotient.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

def idealNormClass
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal)
    (x : IntegralGroupRing G) (hx : x ∈ ideal G) :
    RelativeAugmentationQuotient H

theorem

sum_deltaNormClass_eq_idealNormClass

L965 ↗

GroupTheory.Transfer.RelativeAugmentation.sum_deltaNormClass_eq_idealNormClass

Documentation

The coefficient decomposition of the general norm-element class.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem sum_deltaNormClass_eq_idealNormClass
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal)
    (x : IntegralGroupRing G) (hx : x ∈ ideal G) :
    ∑ g ∈ x.coeff.support,
        x.coeff g • deltaNormClass H T g =
      idealNormClass H T x hx

theorem

augmentationTransfer_apply_quotientMk

L1009 ↗

GroupTheory.Transfer.RelativeAugmentation.augmentationTransfer_apply_quotientMk

Documentation

The full transfer/augmentation formula. For every x ∈ I_G,

S(x mod I_G²) = x · (∑ρ) mod I_G I_H.

Source context 8 commands

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

open scoped Pointwise
noncomputable section
namespace GroupTheory
namespace Transfer
namespace RelativeAugmentation
open GroupTheory.Augmentation
open Subgroup
variable {G : Type*} [Group G]

Lean source · statement

theorem augmentationTransfer_apply_quotientMk
    (H : Subgroup G) [H.FiniteIndex]
    (T : H.LeftTransversal)
    (x : IntegralGroupRing G) (hx : x ∈ ideal G) :
    augmentationTransfer H
        (Multiplicative.ofAdd
          (QuotientAddGroup.mk' (squareInIdeal G) ⟨x, hx⟩)) =
      Multiplicative.ofAdd (idealNormClass H T x hx)

Module documentation

Transfer and relative augmentation quotients

Declarations