Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Discrete.DifferentialModule.Boundary
ProCGroups/FoxDifferential/Discrete/DifferentialModule/Boundary

ProCGroups.FoxDifferential.Discrete.DifferentialModule.Boundary

9 Theorems | 4 Definitions

The principal declarations in this module are:

  • groupRingBoundary The standard map \(G \to \mathbb{Z}[H]\), \(g \mapsto \psi(g)-1\) is viewed as a differential map. - groupRingBoundaryHom The Fox boundary is itself a crossed differential. - groupRingBoundary_one The Fox boundary vanishes at the identity. - groupRingBoundary_eq_zero_of_mem_ker The Fox boundary is zero on elements in the kernel of \(\psi\).
import
Imported by

Declarations

Definition FoxDifferential.groupRingBoundary 
def groupRingBoundary (ψ : G →* H) (g : G) : GroupRing H :=
  MonoidAlgebra.of ℤ H (ψ g) - 1

The standard map \(G \to \mathbb{Z}[H]\), \(g \mapsto \psi(g)-1\) is viewed as a differential map.

Theorem FoxDifferential.groupRingBoundary_one 
@[simp]
theorem groupRingBoundary_one (ψ : G →* H) :
    groupRingBoundary ψ (1 : G) = 0

The Fox boundary vanishes at the identity.

Show Lean proof
Theorem FoxDifferential.groupRingBoundary_eq_zero_of_mem_ker 
@[simp]
theorem groupRingBoundary_eq_zero_of_mem_ker (ψ : G →* H) {g : G} (hg : ψ g = 1) :
    groupRingBoundary ψ g = 0

The Fox boundary is zero on elements in the kernel of \(\psi\).

Show Lean proof
Theorem FoxDifferential.groupRingBoundary_subtype_ker 
@[simp]
theorem groupRingBoundary_subtype_ker (ψ : G →* H) (g : ψ.ker) :
    groupRingBoundary ψ g = 0

The Fox boundary vanishes on the kernel subgroup of \(\psi\).

Show Lean proof
Definition FoxDifferential.groupRingBoundaryHom 
def groupRingBoundaryHom (ψ : G →* H) : DifferentialHom ψ (GroupRing H) where
  toFun := groupRingBoundary ψ
  map_mul' := by
    intro g₁ g₂
    simp only [scalarCrossedAction_apply, groupRingBoundary, map_mul,
      MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one, sub_eq_add_neg,
      add_comm, groupRingScalar_apply, smul_eq_mul, mul_add, mul_neg, add_assoc,
      add_neg_cancel_comm_assoc]

The Fox boundary is itself a crossed differential.

Theorem FoxDifferential.groupRingBoundaryHom_apply 
@[simp]
theorem groupRingBoundaryHom_apply (ψ : G →* H) (g : G) :
    groupRingBoundaryHom ψ g = groupRingBoundary ψ g

The bundled group-ring boundary homomorphism evaluates to the usual Fox boundary.

Show Lean proof
Theorem FoxDifferential.groupRingMap_groupRingBoundary 
@[simp]
theorem groupRingMap_groupRingBoundary {K : Type*} [Group K]
    (φ : H →* K) (ψ : G →* H) (g : G) :
    groupRingMap φ (groupRingBoundary ψ g) = groupRingBoundary (φ.comp ψ) g

Group-ring functoriality carries Fox boundaries to Fox boundaries.

Show Lean proof
Definition FoxDifferential.toGroupRing 
def toGroupRing (ψ : G →* H) : DifferentialModule ψ →ₗ[GroupRing H] GroupRing H :=
  differentialModuleLift (A := GroupRing H) ψ (groupRingBoundaryHom ψ)

The universal boundary map \(A_{\psi}\ \to \mathbb{Z}[H]\), \(universalDifferential(g) \mapsto \psi(g) - 1\).

Theorem FoxDifferential.toGroupRing_d 
theorem toGroupRing_d (ψ : G →* H) (g : G) :
    toGroupRing ψ (universalDifferential ψ g) = groupRingBoundary ψ g

The universal boundary sends universalDifferential g to \([\psi(g)] - 1\).

Show Lean proof
Definition FoxDifferential.augmentationGenerator 
def augmentationGenerator (H : Type*) [Group H] (h : H) : GroupRing H :=
  MonoidAlgebra.of Int H h - 1

The standard group-ring generator \(h-1\) appearing in Fox boundary formulas.

Theorem FoxDifferential.augmentationGenerator_one 
@[simp]
theorem augmentationGenerator_one (H : Type*) [Group H] :
    augmentationGenerator H (1 : H) = 0

The standard augmentation generator at the identity is zero.

Show Lean proof
Theorem FoxDifferential.augmentationGenerator_eq_groupRingBoundary 
@[simp]
theorem augmentationGenerator_eq_groupRingBoundary (H : Type*) [Group H] (h : H) :
    augmentationGenerator H h = groupRingBoundary (MonoidHom.id H) h

The augmentation generator is the identity-coefficient Fox boundary.

Show Lean proof
Theorem FoxDifferential.groupRingMap_augmentationGenerator 
@[simp]
theorem groupRingMap_augmentationGenerator {K : Type*} [Group K]
    (φ : H →* K) (h : H) :
    groupRingMap φ (augmentationGenerator H h) = augmentationGenerator K (φ h)

Group-ring functoriality carries augmentation generators to augmentation generators.

Show Lean proof