NYLL
Module

Universal.lean

Nyll.ProCGroups.FoxDifferential.Discrete.FoxCalculus.Universal
6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: discrete — fox calculus — universal

The principal declarations in this module are:

  • relativeDifferentialToFreeFoxCoordinates

The universal map \(A_{\psi}\) \(\to\) \(\mathbb{Z}[H]^X\) induced by the relative Fox derivative.

  • relativeFreeFoxCoordinatesLinearMap

The linear map from pushed-forward Fox-coordinate vectors to \(A_{\psi}\), sending the coordinate basis vector at \(x\) to \(\mathrm{universalDifferential}(\psi)(x)\).

  • relativeDifferentialToFreeFoxCoordinates_d

The coordinate map out of the universal differential module sends \(\mathrm{universalDifferential}(w)\) to the Fox derivative of \(w\).

  • relativeFreeFoxCoordinatesLinearMap_single

The coordinate-to-differential map sends a coordinate basis vector to the corresponding universal generator differential.

Imports1
Imported by3

Declarations

def

relativeDifferentialToFreeFoxCoordinates

L48 ↗
FoxDifferential.FoxCalculus.relativeDifferentialToFreeFoxCoordinates
Documentation

The universal map \(A_{\psi}\) \(\to\) \(\mathbb{Z}[H]^X\) induced by the relative Fox derivative.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · statement
def relativeDifferentialToFreeFoxCoordinates :
    DifferentialModule ψ →ₗ[GroupRing H] RelativeFreeFoxCoordinates (H := H) X
theorem

relativeDifferentialToFreeFoxCoordinates_d

L60 ↗
FoxDifferential.FoxCalculus.relativeDifferentialToFreeFoxCoordinates_d
Documentation

The coordinate map out of the universal differential module sends \(\mathrm{universalDifferential}(w)\) to the Fox derivative of \(w\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · statement
theorem relativeDifferentialToFreeFoxCoordinates_d (w : FreeGroup X) :
    relativeDifferentialToFreeFoxCoordinates (H := H) X ψ (universalDifferential ψ w) =
      relativeFreeGroupFoxDerivative (H := H) X ψ w
def

relativeFreeFoxCoordinatesLinearMap

L81 ↗
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap
Documentation

The linear map from pushed-forward Fox-coordinate vectors to \(A_{\psi}\), sending the coordinate basis vector at \(x\) to \(\mathrm{universalDifferential}(\psi)(x)\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
Lean source · statement
def relativeFreeFoxCoordinatesLinearMap :
    RelativeFreeFoxCoordinates (H := H) X →ₗ[GroupRing H] DifferentialModule ψ
theorem

relativeFreeFoxCoordinatesLinearMap_single

L98 ↗
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap_single
Documentation

The coordinate-to-differential map sends a coordinate basis vector to the corresponding universal generator differential.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
Lean source · statement
theorem relativeFreeFoxCoordinatesLinearMap_single (x : X) :
    relativeFreeFoxCoordinatesLinearMap (H := H) X ψ
        (Pi.single x (1 : GroupRing H)) =
      universalDifferential ψ (FreeGroup.of x)
theorem

relativeFreeGroupDifferential_inv

L115 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupDifferential_inv
Documentation

The universal relative differential on a free group satisfies the inverse rule.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
omit [DecidableEq X] [Fintype X] in
Lean source · statement
theorem relativeFreeGroupDifferential_inv (w : FreeGroup X) :
    universalDifferential ψ w⁻¹ =
      -((MonoidAlgebra.of ℤ H (ψ w⁻¹) : GroupRing H) • universalDifferential ψ w)
theorem

relativeFreeFoxCoordinatesLinearMap_derivative

L123 ↗
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap_derivative
Documentation

The relative Fox-coordinate formula recovers the universal differential in \(A_{\psi}\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
Lean source · statement
theorem relativeFreeFoxCoordinatesLinearMap_derivative (w : FreeGroup X) :
    relativeFreeFoxCoordinatesLinearMap (H := H) X ψ
        (relativeFreeGroupFoxDerivative (H := H) X ψ w) =
      universalDifferential ψ w

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.