ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Basic

3 Theorems | 2 Definitions | 1 Abbreviation

The principal declarations in this module are:

ResidueFreeFoxCoordinates Residue Fox-coordinate vectors with coefficients in \((\mathbb{Z}/n\mathbb{Z})[H]\). - residueFreeGroupFoxDerivativeVector Residue free-group Fox derivative vector, with coefficients pushed forward along \(\psi:\mathrm{FreeGroup}(X)\to H\). - residueFreeGroupFoxDerivativeVector_of The residue free-group derivative vector sends a free generator to the corresponding coordinate basis vector. - residueFreeGroupFoxDerivativeVector_unique Uniqueness of the residue free-group derivative vector among crossed differentials with standard coordinate values on free generators.

imports

Imported by

Abbreviation FoxDifferential.ResidueFreeFoxCoordinates

abbrev ResidueFreeFoxCoordinates (n : ℕ) (H : Type v) (X : Type u) : Type (max u v) :=
  X → ResidueGroupRing n H

Residue Fox-coordinate vectors with coefficients in \((\mathbb{Z}/n\mathbb{Z})[H]\).

Definition FoxDifferential.residueFreeGroupFoxDerivativeVector

def residueFreeGroupFoxDerivativeVector (n : ℕ) (ψ : FreeGroup X →* H)
    : ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueFreeFoxCoordinates n H X) :=
  freeCrossedHomWithCoeff
    (A := ResidueFreeFoxCoordinates n H X)
    (residueGroupRingScalar n ψ)
    (fun x => Pi.single x (1 : ResidueGroupRing n H))

Residue free-group Fox derivative vector, with coefficients pushed forward along \(\psi:\mathrm{FreeGroup}(X)\to H\).

Definition FoxDifferential.residueFreeGroupFoxDerivative

def residueFreeGroupFoxDerivative (n : ℕ) (ψ : FreeGroup X →* H) (i : X) :
    ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueGroupRing n H) :=
  (residueFreeGroupFoxDerivativeVector n ψ).mapLinear
    { toFun := fun v => v i
      map_add' := by intro v w; rfl
      map_smul' := by intro r v; rfl }

A coordinate of the residue free-group Fox derivative.

Theorem FoxDifferential.residueFreeGroupFoxDerivativeVector_of

@[simp]
theorem residueFreeGroupFoxDerivativeVector_of (n : ℕ) (ψ : FreeGroup X →* H) (x : X) :
    residueFreeGroupFoxDerivativeVector n ψ (FreeGroup.of x) =
      Pi.single x (1 : ResidueGroupRing n H)

The residue free-group derivative vector sends a free generator to the corresponding coordinate basis vector.

Show Lean proof

Theorem FoxDifferential.residueFreeGroupFoxDerivativeVector_unique

theorem residueFreeGroupFoxDerivativeVector_unique
    (n : ℕ) (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (residueGroupRingScalar n ψ)
      (ResidueFreeFoxCoordinates n H X))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : ResidueGroupRing n H)) :
    delta = residueFreeGroupFoxDerivativeVector n ψ

Uniqueness of the residue free-group derivative vector among crossed differentials with standard coordinate values on free generators.

Show Lean proof

Theorem FoxDifferential.existsUnique_residueFreeGroupFoxDerivativeVector

theorem existsUnique_residueFreeGroupFoxDerivativeVector
    (n : ℕ) (ψ : FreeGroup X →* H) :
    ∃! delta : ScalarCrossedHom (residueGroupRingScalar n ψ)
        (ResidueFreeFoxCoordinates n H X),
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : ResidueGroupRing n H)

Existence and uniqueness theorem for the residue free-group derivative vector.

Show Lean proof

ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Basic

Declarations