Yamaguchi Lean 4 Library
ProCGroups.CrowellExactSequence.Discrete.SequenceMaps
ProCGroups/CrowellExactSequence/Discrete/SequenceMaps

ProCGroups.CrowellExactSequence.Discrete.SequenceMaps

2 Theorems | 4 Definitions

This file constructs the maps in the discrete presentation sequence: the middle coordinate equivalence, the augmentation-generator tail map, and the relative-derivative head map. It also records their formulas on free generators.

imports
Imported by

Declarations

Definition CrowellExactSequence.FoxCalculus.freeGroupPresentationMiddleCoordinateEquiv 
def freeGroupPresentationMiddleCoordinateEquiv
    (r : Nat) (ψ : FreeGroup (Fin r) →* H) :
    DifferentialModule ψ ≃ₗ[GroupRing H] (Fin r → GroupRing H) :=
  (FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearEquivDifferential
    (H := H) (Fin r) ψ).symm

For a finite free presentation \(\psi:F_r\to H\), the Crowell middle term is identified with the explicit module of relative Fox coordinates.

Definition CrowellExactSequence.FoxCalculus.freeGroupPresentationAugmentationGenerators 
def freeGroupPresentationAugmentationGenerators
    (r : Nat) (ψ : FreeGroup (Fin r) →* H) : Fin r → GroupRing H :=
  fun i => augmentationGenerator H (ψ (FreeGroup.of i))

The concrete BL tail generators \(\psi(x_i)-1\) for a finite free presentation.

Definition CrowellExactSequence.FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap 
def freeGroupPresentationBlanchfieldLyndonTailMap
    (r : Nat) (ψ : FreeGroup (Fin r) →* H) :
    (Fin r → GroupRing H) →ₗ[GroupRing H] GroupRing H :=
  blanchfieldLyndonFiniteFamilyMap
    (R := GroupRing H)
    (freeGroupPresentationAugmentationGenerators (H := H) r ψ)

The concrete Blanchfield--Lyndon tail map in relative Fox coordinates.

Theorem CrowellExactSequence.FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap_apply 
theorem freeGroupPresentationBlanchfieldLyndonTailMap_apply
    (r : Nat) (ψ : FreeGroup (Fin r) →* H) (a : Fin r → GroupRing H) :
    freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r ψ a =
      ∑ i : Fin r, a i * augmentationGenerator H (ψ (FreeGroup.of i))

The discrete Blanchfield--Lyndon tail map is evaluated on the canonical generators and then extended linearly to the coordinate module.

Show Lean proof
Definition CrowellExactSequence.FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap 
def freeGroupPresentationRelativeDerivativeHeadMap
    (r : Nat) (ψ : FreeGroup (Fin r) →* H) (hψ : Function.Surjective ψ) :
    letI := kernelAbelianizationModuleOfSurjective ψ hψ
    KernelAbelianizationAdd ψ →ₗ[GroupRing H] (Fin r → GroupRing H) := by
  letI := kernelAbelianizationModuleOfSurjective ψ hψ
  exact
    (freeGroupPresentationMiddleCoordinateEquiv (H := H) r ψ).toLinearMap.comp
      (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)

The concrete BL head map: the Crowell head map written in relative Fox coordinates.

Theorem CrowellExactSequence.FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap_of 
theorem freeGroupPresentationRelativeDerivativeHeadMap_of
    (r : Nat) (ψ : FreeGroup (Fin r) →* H) (hψ : Function.Surjective ψ)
    (n : ψ.ker) :
    letI := kernelAbelianizationModuleOfSurjective ψ hψ
    freeGroupPresentationRelativeDerivativeHeadMap (H := H) r ψ hψ
        (Additive.ofMul (Abelianization.of n)) =
      FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1

On a kernel element, the concrete BL head map is the relative Fox derivative vector.

Show Lean proof