Module

Basic.lean

Nyll.ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Basic

6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — residue — free group — basic

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.

Imports2

Imported by3

abbrev

ResidueFreeFoxCoordinates

L40 ↗

FoxDifferential.ResidueFreeFoxCoordinates

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]

Lean source · statement

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

def

residueFreeGroupFoxDerivativeVector

L47 ↗

FoxDifferential.residueFreeGroupFoxDerivativeVector

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]

Lean source · statement

def residueFreeGroupFoxDerivativeVector (n : ℕ) (ψ : FreeGroup X →* H)
    : ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueFreeFoxCoordinates n H X)

def

residueFreeGroupFoxDerivative

L55 ↗

FoxDifferential.residueFreeGroupFoxDerivative

Documentation

A coordinate of the residue free-group Fox derivative.

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]

Lean source · statement

def residueFreeGroupFoxDerivative (n : ℕ) (ψ : FreeGroup X →* H) (i : X) :
    ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueGroupRing n H)

theorem

residueFreeGroupFoxDerivativeVector_of

L67 ↗

FoxDifferential.residueFreeGroupFoxDerivativeVector_of

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]

Lean source · statement

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

theorem

residueFreeGroupFoxDerivativeVector_unique

L78 ↗

FoxDifferential.residueFreeGroupFoxDerivativeVector_unique

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]

Lean source · statement

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 ψ

theorem

existsUnique_residueFreeGroupFoxDerivativeVector

L92 ↗

FoxDifferential.existsUnique_residueFreeGroupFoxDerivativeVector

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]

Lean source · statement

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)

Module documentation

Fox differential: completed — residue — free group — basic

Declarations

ResidueFreeFoxCoordinates

residueFreeGroupFoxDerivativeVector

residueFreeGroupFoxDerivative

residueFreeGroupFoxDerivativeVector_of

residueFreeGroupFoxDerivativeVector_unique

existsUnique_residueFreeGroupFoxDerivativeVector