Module

Basic.lean

Nyll.ProCGroups.FoxDifferential.Discrete.Jacobian.Basic

14 declarations indexed from sourceView source ↗

Module documentation

Fox differential: discrete — jacobian — basic

The principal declarations in this module are:

freeGroupHomFoxJacobian

The relative Fox Jacobian of \(\varphi : \mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(Y)\), with coefficients pushed forward by \(\psi : \mathrm{FreeGroup}(Y) \to H\). The row indexed by \(x : X\) is the relative Fox derivative of the substituted generator \(\varphi(x)\) with respect to the \(Y\)-generators.

freeGroupHomFoxJacobianMatrix

The relative Fox Jacobian, packaged as a matrix.

freeGroupHomFoxJacobianMatrix_apply

Evaluating the bundled relative Fox Jacobian matrix at (x, y) returns the corresponding relative Fox derivative.

freeGroupHomFoxJacobian_eq_freeCrossedDifferentialWithCoeffJacobian

The usual relative Fox Jacobian is the coefficient-generic free crossed-differential Jacobian specialized to the group-ring coefficient homomorphism.

Imports1

Nyll.ProCGroups.FoxDifferential.Discrete.Absolute

Imported by2

def

freeGroupHomFoxJacobian

L48 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobian

Documentation

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}

Lean source · statement

def freeGroupHomFoxJacobian
    [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
    X → Y → GroupRing H

def

freeGroupHomFoxJacobianMatrix

L56 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix

Documentation

The relative Fox Jacobian, packaged as a matrix.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}

Lean source · statement

def freeGroupHomFoxJacobianMatrix
    [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
    Matrix X Y (GroupRing H)

theorem

freeGroupHomFoxJacobianMatrix_apply

L67 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix_apply

Documentation

Evaluating the bundled relative Fox Jacobian matrix at (x, y) returns the corresponding relative Fox derivative.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}

Lean source · statement

theorem freeGroupHomFoxJacobianMatrix_apply
    [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (x : X) (y : Y) :
    freeGroupHomFoxJacobianMatrix (H := H) ψ φ x y =
    freeGroupHomFoxJacobian (H := H) ψ φ x y

theorem

freeGroupHomFoxJacobian_eq_freeCrossedDifferentialWithCoeffJacobian

L79 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobian_eq_freeCrossedDifferentialWithCoeffJacobian

Documentation

The usual relative Fox Jacobian is the coefficient-generic free crossed-differential Jacobian specialized to the group-ring coefficient homomorphism.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}

Lean source · statement

theorem freeGroupHomFoxJacobian_eq_freeCrossedDifferentialWithCoeffJacobian
    [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
    freeGroupHomFoxJacobian (H := H) ψ φ =
      freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (groupRingScalar ψ) φ

theorem

freeGroupHomFoxJacobianMatrix_eq_freeCrossedDifferentialWithCoeffJacobianMatrix

L92 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix_eq_freeCrossedDifferentialWithCoeffJacobianMatrix

Documentation

Matrix form of the comparison between the usual relative Fox Jacobian and the coefficient-generic free crossed-differential Jacobian.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}

Lean source · statement

theorem freeGroupHomFoxJacobianMatrix_eq_freeCrossedDifferentialWithCoeffJacobianMatrix
    [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
    freeGroupHomFoxJacobianMatrix (H := H) ψ φ =
      freeCrossedDifferentialWithCoeffJacobianMatrix
        (X := X) (Y := Y) (groupRingScalar ψ) φ

def

freeGroupHomFoxJacobianAbsolute

L105 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsolute

Documentation

The absolute Fox Jacobian of a homomorphism between free groups.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}

Lean source · statement

def freeGroupHomFoxJacobianAbsolute
    [DecidableEq Y]
    (φ : FreeGroup X →* FreeGroup Y) :
    X → Y → GroupRing (FreeGroup Y)

def

freeGroupHomFoxJacobianAbsoluteMatrix

L112 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsoluteMatrix

Documentation

The absolute Fox Jacobian, packaged as a matrix.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}

Lean source · statement

def freeGroupHomFoxJacobianAbsoluteMatrix
    [DecidableEq Y]
    (φ : FreeGroup X →* FreeGroup Y) :
    Matrix X Y (GroupRing (FreeGroup Y))

theorem

freeGroupHomFoxJacobianAbsoluteMatrix_apply

L123 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsoluteMatrix_apply

Documentation

Evaluating the bundled absolute Fox Jacobian matrix at (x, y) returns the corresponding absolute Fox derivative.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}

Lean source · statement

theorem freeGroupHomFoxJacobianAbsoluteMatrix_apply
    [DecidableEq Y]
    (φ : FreeGroup X →* FreeGroup Y) (x : X) (y : Y) :
    freeGroupHomFoxJacobianAbsoluteMatrix φ x y =
      freeGroupHomFoxJacobianAbsolute φ x y

theorem

freeGroupHomFoxJacobianAbsolute_id

L132 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsolute_id

Documentation

The absolute Fox Jacobian of the identity homomorphism is the coordinate identity family.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}

Lean source · full declaration

theorem freeGroupHomFoxJacobianAbsolute_id
    [DecidableEq X] :
    freeGroupHomFoxJacobianAbsolute (MonoidHom.id (FreeGroup X)) =
      fun x : X => Pi.single x (1 : GroupRing (FreeGroup X)) := by
  funext x y
  simp only [freeGroupHomFoxJacobianAbsolute, freeGroupHomFoxJacobian, MonoidHom.id_apply,
  relativeFreeGroupFoxDerivative_of]

theorem

freeGroupHomFoxJacobianAbsoluteMatrix_id

L142 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsoluteMatrix_id

Documentation

The absolute Fox Jacobian matrix of the identity homomorphism is the identity matrix.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}

Lean source · statement

theorem freeGroupHomFoxJacobianAbsoluteMatrix_id
    [DecidableEq X] :
    freeGroupHomFoxJacobianAbsoluteMatrix (MonoidHom.id (FreeGroup X)) =
      (1 : Matrix X X (GroupRing (FreeGroup X)))

theorem

freeGroupHomFoxJacobian_mapDomain_apply

L165 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobian_mapDomain_apply

Documentation

Postcomposing the coefficient homomorphism maps each relative Fox Jacobian entry through the induced group-ring map.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}
variable {K : Type t} [Group K]

Lean source · statement

theorem freeGroupHomFoxJacobian_mapDomain_apply
    [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (η : H →* K)
    (φ : FreeGroup X →* FreeGroup Y) (x : X) (y : Y) :
    freeGroupHomFoxJacobian (H := K) (η.comp ψ) φ x y =
      groupRingMap η (freeGroupHomFoxJacobian (H := H) ψ φ x y)

theorem

freeGroupHomFoxJacobianMatrix_mapDomain

L174 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix_mapDomain

Documentation

Fox Jacobians are natural under coefficient push-forward, matrix form.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}
variable {K : Type t} [Group K]

Lean source · statement

theorem freeGroupHomFoxJacobianMatrix_mapDomain
    [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (η : H →* K)
    (φ : FreeGroup X →* FreeGroup Y) :
    freeGroupHomFoxJacobianMatrix (H := K) (η.comp ψ) φ =
      (freeGroupHomFoxJacobianMatrix (H := H) ψ φ).map (groupRingMap η)

theorem

freeGroupHomFoxJacobian_eq_map_absolute_apply

L191 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobian_eq_map_absolute_apply

Documentation

A relative Fox Jacobian entry is the image of the corresponding absolute entry under the coefficient group-ring map.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}
variable {K : Type t} [Group K]

Lean source · statement

theorem freeGroupHomFoxJacobian_eq_map_absolute_apply
    [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (x : X) (y : Y) :
    freeGroupHomFoxJacobian (H := H) ψ φ x y =
      groupRingMap ψ (freeGroupHomFoxJacobianAbsolute φ x y)

theorem

freeGroupHomFoxJacobianMatrix_eq_map_absolute

L203 ↗

FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix_eq_map_absolute

Documentation

Matrix form of the absolute-to-relative comparison for Fox Jacobians.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}
variable {K : Type t} [Group K]

Lean source · statement

theorem freeGroupHomFoxJacobianMatrix_eq_map_absolute
    [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
    freeGroupHomFoxJacobianMatrix (H := H) ψ φ =
      (freeGroupHomFoxJacobianAbsoluteMatrix φ).map (groupRingMap ψ)

Module documentation

Fox differential: discrete — jacobian — basic

Declarations