ProCGroups.FoxDifferential.Discrete.GroupRing

19 Theorems | 9 Definitions

The principal declarations in this module are:

augmentationAlgHom The augmentation algebra homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\). - augmentation The augmentation ring homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\). - augmentation_of The augmentation map has the stated value on group-ring elements. - augmentation_one The augmentation sends the group identity to \(1\).

imports

ProCGroups.FoxDifferential.Discrete.DifferentialModule.Boundary
Mathlib.Algebra.MonoidAlgebra.Basic
Mathlib.RingTheory.Ideal.Maps

Imported by

Definition FoxDifferential.augmentationAlgHom

def augmentationAlgHom : GroupRing H →ₐ[ℤ] ℤ :=
  MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)

The augmentation algebra homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\).

Definition FoxDifferential.augmentation

def augmentation : GroupRing H →+* ℤ :=
  (augmentationAlgHom H).toRingHom

The augmentation ring homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\).

Definition FoxDifferential.augmentationIdeal

def augmentationIdeal : Ideal (GroupRing H) :=
  RingHom.ker (augmentation H)

The augmentation ideal of the integral group ring \(\mathbb{Z}[H]\).

Definition FoxDifferential.augmentationGeneratorIdeal

def augmentationGeneratorIdeal : Ideal (GroupRing H) :=
  Ideal.span (Set.range (augmentationGenerator H))

The ideal generated by the standard augmentation generators \(h-1\).

Theorem FoxDifferential.augmentation_of

@[simp]
theorem augmentation_of (h : H) :
    augmentation H (MonoidAlgebra.of ℤ H h) = 1

The augmentation map has the stated value on group-ring elements.

Show Lean proof

Theorem FoxDifferential.augmentation_one

@[simp]
theorem augmentation_one :
    augmentation H (1 : GroupRing H) = 1

The augmentation sends the group identity to \(1\).

Show Lean proof

Theorem FoxDifferential.mem_augmentationIdeal_iff

@[simp]
theorem mem_augmentationIdeal_iff {x : GroupRing H} :
    x ∈ augmentationIdeal H ↔ augmentation H x = 0

A group-ring element lies in the Fox augmentation ideal iff its augmentation is zero.

Show Lean proof

Theorem FoxDifferential.groupRingBoundary_mem_augmentationIdeal

@[simp]
theorem groupRingBoundary_mem_augmentationIdeal
    {G : Type*} [Group G] (ψ : G →* H) (g : G) :
    groupRingBoundary ψ g ∈ augmentationIdeal H

The group-ring boundary value \([\psi(g)]-1\) lies in the augmentation ideal.

Show Lean proof

Theorem FoxDifferential.augmentationGenerator_mem_augmentationIdeal

@[simp]
theorem augmentationGenerator_mem_augmentationIdeal (h : H) :
    augmentationGenerator H h ∈ augmentationIdeal H

Each standard generator \(h-1\) lies in the ordinary group-ring augmentation ideal.

Show Lean proof

Theorem FoxDifferential.augmentationGenerator_mem_augmentationGeneratorIdeal

@[simp]
theorem augmentationGenerator_mem_augmentationGeneratorIdeal (h : H) :
    augmentationGenerator H h ∈ augmentationGeneratorIdeal H

Augmentation generators lie in the augmentation-generator ideal.

Show Lean proof

Theorem FoxDifferential.augmentationGeneratorIdeal_le_augmentationIdeal

theorem augmentationGeneratorIdeal_le_augmentationIdeal :
    augmentationGeneratorIdeal H ≤ augmentationIdeal H

The generator-defined augmentation ideal is contained in the ordinary group-ring augmentation ideal.

Show Lean proof

Theorem FoxDifferential.exists_mem_augmentationGeneratorIdeal_add

theorem exists_mem_augmentationGeneratorIdeal_add (x : GroupRing H) :
    ∃ y ∈ augmentationGeneratorIdeal H, x = y + (augmentation H x : GroupRing H)

An augmentation-zero group-ring element can be decomposed using the standard augmentation generators.

Show Lean proof

Theorem FoxDifferential.augmentationIdeal_le_augmentationGeneratorIdeal

theorem augmentationIdeal_le_augmentationGeneratorIdeal :
    augmentationIdeal H ≤ augmentationGeneratorIdeal H

The ordinary group-ring augmentation ideal is contained in the ideal generated by the elements \(g-1\).

Show Lean proof

Theorem FoxDifferential.augmentationGeneratorIdeal_eq_augmentationIdeal

theorem augmentationGeneratorIdeal_eq_augmentationIdeal :
    augmentationGeneratorIdeal H = augmentationIdeal H

The ideal generated by the standard elements \(g-1\) is the ordinary augmentation ideal.

Show Lean proof

Definition FoxDifferential.augmentationBoundary

def augmentationBoundary (ψ : G →* H) (g : G) : augmentationIdeal H :=
  ⟨groupRingBoundary ψ g, groupRingBoundary_mem_augmentationIdeal (H := H) ψ g⟩

The Crowell boundary map with codomain restricted to the augmentation ideal.

Definition FoxDifferential.augmentationGeneratorSubtype

def augmentationGeneratorSubtype (h : H) : augmentationIdeal H :=
  ⟨augmentationGenerator H h, augmentationGenerator_mem_augmentationIdeal H h⟩

The standard generators \(h-1\) of the augmentation ideal, viewed in the ideal itself.

Theorem FoxDifferential.toGroupRing_mem_augmentationIdeal

theorem toGroupRing_mem_augmentationIdeal (ψ : G →* H) (x : DifferentialModule ψ) :
    toGroupRing ψ x ∈ augmentationIdeal H

The group-ring image of any differential-module element lies in the augmentation ideal.

Show Lean proof

Definition FoxDifferential.toAugmentationIdeal

def toAugmentationIdeal (ψ : G →* H) :
    DifferentialModule ψ →ₗ[GroupRing H] augmentationIdeal H :=
  LinearMap.codRestrict (augmentationIdeal H) (toGroupRing ψ)
    (toGroupRing_mem_augmentationIdeal (H := H) ψ)

The factorization \(A_{\psi} \to I(\mathbb{Z}[H])\) of the boundary map through the augmentation ideal.

Theorem FoxDifferential.toAugmentationIdeal_d

@[simp]
theorem toAugmentationIdeal_d (ψ : G →* H) (g : G) :
    toAugmentationIdeal (H := H) ψ (universalDifferential ψ g) =
      augmentationBoundary (H := H) ψ g

The universal differential maps into the ordinary group-ring augmentation ideal.

Show Lean proof

Theorem FoxDifferential.subtype_comp_toAugmentationIdeal

@[simp]
theorem subtype_comp_toAugmentationIdeal (ψ : G →* H) :
    (augmentationIdeal H).subtype.comp (toAugmentationIdeal (H := H) ψ) =
      toGroupRing ψ

Composing the boundary factorization through the augmentation ideal with the subtype map gives the original boundary map.

Show Lean proof

Theorem FoxDifferential.span_augmentationGeneratorSubtype_eq_top

theorem span_augmentationGeneratorSubtype_eq_top :
    Submodule.span (GroupRing H) (Set.range (augmentationGeneratorSubtype (H := H))) = ⊤

The standard augmentation generators span the augmentation ideal as a module.

Show Lean proof

Theorem FoxDifferential.toAugmentationIdeal_surjective

theorem toAugmentationIdeal_surjective (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Function.Surjective (toAugmentationIdeal (H := H) ψ)

The boundary factorization onto the augmentation ideal is surjective in the identity case.

Show Lean proof

Theorem FoxDifferential.toGroupRing_id_injective

theorem toGroupRing_id_injective :
    Function.Injective (toGroupRing (MonoidHom.id H))

The identity-case map from the differential module to the group ring is injective.

Show Lean proof

Definition FoxDifferential.augmentationIdealToIdentityDifferentialModule

def augmentationIdealToIdentityDifferentialModule :
    augmentationIdeal H →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) where
  toFun x :=
    monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1
  map_add' x y := by
    change
      monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (x.1 + y.1) =
        monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1 +
          monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) y.1
    simp only [map_add]
  map_smul' r x := by
    change
      monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (r * x.1) =
        r • monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1
    apply identityCrossedDifferentialBoundary_injective (S := ℤ) (G := H)
    have hxaug :
        (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) x.1 = 0 :=
      (mem_augmentationIdeal_iff (H := H)).1 x.2
    have hrxaug :
        (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) (r * x.1) = 0 := by
      rw [map_mul, hxaug, mul_zero]
    calc
      identityCrossedDifferentialBoundary (S := ℤ) (G := H)
          (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (r * x.1)) =
        r * x.1 := by
          exact
            idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
              (S := ℤ) (G := H) hrxaug
      _ =
        r * identityCrossedDifferentialBoundary (S := ℤ) (G := H)
          (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) := by
          exact congrArg (fun z => r * z)
            (idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
              (S := ℤ) (G := H) hxaug).symm
      _ =
        identityCrossedDifferentialBoundary (S := ℤ) (G := H)
          (r • monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) := by
          exact
            (LinearMap.map_smul
              (identityCrossedDifferentialBoundary (S := ℤ) (G := H)) r
              (monoidAlgebraToIdentityCrossedDifferentialModule
                (S := ℤ) (G := H) x.1)).symm

The inverse map from the augmentation ideal to the identity differential module, obtained by integrating an augmentation-zero group-ring element.

Theorem FoxDifferential.toAugmentationIdeal_augmentationIdealToIdentityDifferentialModule

theorem toAugmentationIdeal_augmentationIdealToIdentityDifferentialModule
    (x : augmentationIdeal H) :
    toAugmentationIdeal (H := H) (MonoidHom.id H)
        (augmentationIdealToIdentityDifferentialModule (H := H) x) = x

Composing from the augmentation ideal to the identity differential module and back gives the original augmentation-ideal element.

Show Lean proof

Theorem FoxDifferential.augmentationIdealToIdentityDifferentialModule_toAugmentationIdeal

theorem augmentationIdealToIdentityDifferentialModule_toAugmentationIdeal
    (x : DifferentialModule (MonoidHom.id H)) :
    augmentationIdealToIdentityDifferentialModule (H := H)
        (toAugmentationIdeal (H := H) (MonoidHom.id H) x) = x

Composing from the identity differential module to the augmentation ideal and back gives the original differential-module element.

Show Lean proof

Definition FoxDifferential.identityDifferentialModuleEquivAugmentationIdeal

def identityDifferentialModuleEquivAugmentationIdeal :
    DifferentialModule (MonoidHom.id H) ≃ₗ[GroupRing H] augmentationIdeal H where
  toLinearMap := toAugmentationIdeal (H := H) (MonoidHom.id H)
  invFun := augmentationIdealToIdentityDifferentialModule (H := H)
  left_inv := augmentationIdealToIdentityDifferentialModule_toAugmentationIdeal (H := H)
  right_inv := toAugmentationIdeal_augmentationIdealToIdentityDifferentialModule (H := H)

Universe-polymorphic identity case of the Crowell differential module: \(A_{\mathrm{id}}\) is the augmentation ideal of the integral group ring.

Theorem FoxDifferential.identityDifferentialModuleEquivAugmentationIdeal_toLinearMap

theorem identityDifferentialModuleEquivAugmentationIdeal_toLinearMap :
    (identityDifferentialModuleEquivAugmentationIdeal (H := H)).toLinearMap =
      toAugmentationIdeal (H := H) (MonoidHom.id H)

The linear map underlying the equivalence from the identity differential module to the augmentation ideal is the canonical map to that augmentation ideal.

Show Lean proof

ProCGroups.FoxDifferential.Discrete.GroupRing

Declarations