NYLL
Module

Derivative.lean

Nyll.ProCGroups.FoxDifferential.Discrete.FoxCalculus.Derivative
13 declarations indexed from sourceView source ↗

Module documentation

Fox differential: discrete — fox calculus — derivative

The principal declarations in this module are:

  • relativeFreeGroupFoxLift

The semidirect-product lift whose left component is the Fox derivative pushed forward by \(\psi\), and whose right component is \(\psi\) itself.

  • relativeFreeGroupFoxDerivative

The Fox derivative of a free-group word, with coefficients pushed forward to \(\mathbb{Z}[H]\) by \(\psi\).

  • relativeFreeGroupFoxLift_right

The right component of the relative Fox lift is the target homomorphism \(\psi\).

  • relativeFreeGroupFoxDerivative_one

The relative Fox derivative of the identity word is zero.

Imports3
Imported by2

Declarations

def

relativeFreeGroupFoxLift

L49 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxLift
Documentation

The semidirect-product lift whose left component is the Fox derivative pushed forward by \(\psi\), and whose right component is \(\psi\) itself.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators commutatorElement
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · statement
def relativeFreeGroupFoxLift :
    FreeGroup X →* CrossedSemidirectProduct (RelativeFoxAction (H := H) X)
def

relativeFreeGroupFoxDerivative

L59 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative
Documentation

The Fox derivative of a free-group word, with coefficients pushed forward to \(\mathbb{Z}[H]\) by \(\psi\).

Source context 9 commands

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

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

relativeFreeGroupFoxLift_right

L65 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxLift_right
Documentation

The right component of the relative Fox lift is the target homomorphism \(\psi\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators commutatorElement
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · statement
theorem relativeFreeGroupFoxLift_right (w : FreeGroup X) :
    (relativeFreeGroupFoxLift (H := H) X ψ w).right = ψ w
theorem

relativeFreeGroupFoxDerivative_one

L79 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_one
Documentation

The relative Fox derivative of the identity word is zero.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators commutatorElement
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · statement
theorem relativeFreeGroupFoxDerivative_one :
    relativeFreeGroupFoxDerivative (H := H) X ψ (1 : FreeGroup X) = 0
theorem

relativeFreeGroupFoxDerivative_of

L86 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_of
Documentation

The relative Fox derivative of a free generator is the corresponding coordinate vector.

Source context 9 commands

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

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

relativeFreeGroupFoxDerivative_mul

L93 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_mul
Documentation

Relative Fox product rule.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators commutatorElement
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · statement
theorem relativeFreeGroupFoxDerivative_mul (w₁ w₂ : FreeGroup X) :
    relativeFreeGroupFoxDerivative (H := H) X ψ (w₁ * w₂) =
      relativeFreeGroupFoxDerivative (H := H) X ψ w₁ +
        (MonoidAlgebra.of ℤ H (ψ w₁) : GroupRing H) •
          relativeFreeGroupFoxDerivative (H := H) X ψ w₂
def

relativeFreeGroupFoxHom

L103 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxHom
Documentation

The relative free-group Fox derivative is a differential map for \(\psi\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators commutatorElement
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · full declaration
def relativeFreeGroupFoxHom :
    DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X) where
  toFun := relativeFreeGroupFoxDerivative (H := H) X ψ
  map_mul' := by
    intro w₁ w₂
    simpa only [scalarCrossedAction_apply, groupRingScalar_apply] using
      relativeFreeGroupFoxDerivative_mul (H := H) X ψ w₁ w₂
theorem

relativeFreeGroupFoxHom_apply

L114 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxHom_apply
Documentation

The bundled relative Fox crossed homomorphism evaluates to 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 commutatorElement
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · statement
theorem relativeFreeGroupFoxHom_apply (w : FreeGroup X) :
    relativeFreeGroupFoxHom (H := H) X ψ w =
      relativeFreeGroupFoxDerivative (H := H) X ψ w
theorem

relativeFreeGroupFoxDerivative_inv

L120 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_inv
Documentation

The relative Fox derivative satisfies the inverse rule.

Source context 9 commands

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

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

relativeFreeGroupFoxHom_unique

L131 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxHom_unique
Documentation

Uniqueness of the relative free-group Fox derivative among differential maps with standard coordinate values on free generators.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators commutatorElement
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · statement
theorem relativeFreeGroupFoxHom_unique
    (delta : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing H)) :
    delta = relativeFreeGroupFoxHom (H := H) X ψ
theorem

relativeFreeGroupFoxDerivative_pow

L149 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_pow
Documentation

Relative Fox derivative of a positive power.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators commutatorElement
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · full declaration
theorem relativeFreeGroupFoxDerivative_pow (w : FreeGroup X) (n : ℕ) :
    relativeFreeGroupFoxDerivative (H := H) X ψ (w ^ n) =
      (Finset.range n).sum (fun k =>
        (MonoidAlgebra.of ℤ H (ψ (w ^ k)) : GroupRing H) •
          relativeFreeGroupFoxDerivative (H := H) X ψ w) := by
  simpa only [relativeFreeGroupFoxHom_apply, groupRingScalar_apply, map_pow] using
    ScalarCrossedHom.map_pow (relativeFreeGroupFoxHom (H := H) X ψ) w n
theorem

relativeFreeGroupFoxDerivative_conj

L158 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_conj
Documentation

Relative Fox derivative of a conjugate.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators commutatorElement
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · statement
theorem relativeFreeGroupFoxDerivative_conj (g h : FreeGroup X) :
    relativeFreeGroupFoxDerivative (H := H) X ψ (g * h * g⁻¹) =
      relativeFreeGroupFoxDerivative (H := H) X ψ g +
        (MonoidAlgebra.of ℤ H (ψ g) : GroupRing H) •
          relativeFreeGroupFoxDerivative (H := H) X ψ h -
        (MonoidAlgebra.of ℤ H (ψ (g * h * g⁻¹)) : GroupRing H) •
          relativeFreeGroupFoxDerivative (H := H) X ψ g
theorem

relativeFreeGroupFoxDerivative_commutator

L170 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_commutator
Documentation

Relative Fox derivative of a commutator.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators commutatorElement
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
Lean source · statement
theorem relativeFreeGroupFoxDerivative_commutator (g h : FreeGroup X) :
    relativeFreeGroupFoxDerivative (H := H) X ψ ⁅g, h⁆ =
      relativeFreeGroupFoxDerivative (H := H) X ψ g +
        (MonoidAlgebra.of ℤ H (ψ g) : GroupRing H) •
          relativeFreeGroupFoxDerivative (H := H) X ψ h -
        (MonoidAlgebra.of ℤ H (ψ (g * h * g⁻¹)) : GroupRing H) •
          relativeFreeGroupFoxDerivative (H := H) X ψ g -
        (MonoidAlgebra.of ℤ H (ψ ⁅g, h⁆) : GroupRing H) •
          relativeFreeGroupFoxDerivative (H := H) X ψ h

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