Module

SequenceMaps.lean

Nyll.ProCGroups.CrowellExactSequence.Discrete.SequenceMaps

6 declarations indexed from sourceView source ↗

Module documentation

Discrete Crowell sequence maps

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.

Imports4

Imported by3

def

freeGroupPresentationMiddleCoordinateEquiv

L34 ↗

CrowellExactSequence.FoxCalculus.freeGroupPresentationMiddleCoordinateEquiv

Documentation

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

Source context 5 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
namespace FoxCalculus
variable {H : Type} [Group H]

Lean source · statement

def freeGroupPresentationMiddleCoordinateEquiv
    (r : Nat) (ψ : FreeGroup (Fin r) →* H) :
    DifferentialModule ψ ≃ₗ[GroupRing H] (Fin r → GroupRing H)

def

freeGroupPresentationAugmentationGenerators

L41 ↗

CrowellExactSequence.FoxCalculus.freeGroupPresentationAugmentationGenerators

Documentation

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

Source context 5 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
namespace FoxCalculus
variable {H : Type} [Group H]

Lean source · statement

def freeGroupPresentationAugmentationGenerators
    (r : Nat) (ψ : FreeGroup (Fin r) →* H) : Fin r → GroupRing H

def

freeGroupPresentationBlanchfieldLyndonTailMap

L46 ↗

CrowellExactSequence.FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap

Documentation

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

Source context 5 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
namespace FoxCalculus
variable {H : Type} [Group H]

Lean source · statement

def freeGroupPresentationBlanchfieldLyndonTailMap
    (r : Nat) (ψ : FreeGroup (Fin r) →* H) :
    (Fin r → GroupRing H) →ₗ[GroupRing H] GroupRing H

theorem

freeGroupPresentationBlanchfieldLyndonTailMap_apply

L57 ↗

CrowellExactSequence.FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap_apply

Documentation

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

Source context 5 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
namespace FoxCalculus
variable {H : Type} [Group H]

Lean source · statement

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))

def

freeGroupPresentationRelativeDerivativeHeadMap

L66 ↗

CrowellExactSequence.FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap

Documentation

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

Source context 5 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
namespace FoxCalculus
variable {H : Type} [Group H]

Lean source · full declaration

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ψ)

theorem

freeGroupPresentationRelativeDerivativeHeadMap_of

L76 ↗

CrowellExactSequence.FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap_of

Documentation

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

Source context 5 commands

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

namespace CrowellExactSequence
noncomputable section
open FoxDifferential
namespace FoxCalculus
variable {H : Type} [Group H]

Lean source · full declaration

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 := by
  let := kernelAbelianizationModuleOfSurjective ψ hψ
  change
    (freeGroupPresentationMiddleCoordinateEquiv (H := H) r ψ).toLinearMap
        (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
          (Additive.ofMul (Abelianization.of n))) =
      FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1
  rw [kernelAbelianizationBoundaryLinearOfSurjective_of]
  change
    FoxDifferential.FoxCalculus.relativeDifferentialToFreeFoxCoordinates
        (H := H) (Fin r) ψ (universalDifferential ψ n.1) =
      FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1
  exact FoxDifferential.FoxCalculus.relativeDifferentialToFreeFoxCoordinates_d
    (H := H) (Fin r) ψ n.1

Module documentation

Discrete Crowell sequence maps

Declarations

freeGroupPresentationMiddleCoordinateEquiv

freeGroupPresentationAugmentationGenerators

freeGroupPresentationBlanchfieldLyndonTailMap

freeGroupPresentationBlanchfieldLyndonTailMap_apply

freeGroupPresentationRelativeDerivativeHeadMap

freeGroupPresentationRelativeDerivativeHeadMap_of