Module

Absolute.lean

Nyll.ProCGroups.FoxDifferential.Discrete.Absolute

11 declarations indexed from sourceView source ↗

Module documentation

Fox differential: discrete — absolute

The principal declarations in this module are:

freeGroupFoxDerivative

The absolute Fox derivative of a free-group word, with coefficients in \(\mathbb{Z}[\mathrm{FreeGroup}(X)]\).

freeGroupFoxDerivative_one

The absolute Fox derivative of the identity word is zero.

freeGroupFoxDerivative_of

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

freeGroupFoxDerivative_mul

Product rule for the absolute Fox derivative.

Imports2

Imported by2

def

freeGroupFoxDerivative

L42 ↗

FoxDifferential.FoxCalculus.freeGroupFoxDerivative

Documentation

The absolute Fox derivative of a free-group word, with coefficients in \(\mathbb{Z}[\mathrm{FreeGroup}(X)]\).

Source context 6 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 {X : Type u} [DecidableEq X]

Lean source · statement

def freeGroupFoxDerivative (w : FreeGroup X) :
    RelativeFreeFoxCoordinates (H := FreeGroup X) X

theorem

freeGroupFoxDerivative_one

L49 ↗

FoxDifferential.FoxCalculus.freeGroupFoxDerivative_one

Documentation

The absolute Fox derivative of the identity word is zero.

Source context 6 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 {X : Type u} [DecidableEq X]

Lean source · statement

theorem freeGroupFoxDerivative_one :
    freeGroupFoxDerivative (X := X) (1 : FreeGroup X) = 0

theorem

freeGroupFoxDerivative_of

L55 ↗

FoxDifferential.FoxCalculus.freeGroupFoxDerivative_of

Documentation

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

Source context 6 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 {X : Type u} [DecidableEq X]

Lean source · statement

theorem freeGroupFoxDerivative_of (x : X) :
    freeGroupFoxDerivative (X := X) (FreeGroup.of x) =
      Pi.single x (1 : GroupRing (FreeGroup X))

theorem

freeGroupFoxDerivative_mul

L61 ↗

FoxDifferential.FoxCalculus.freeGroupFoxDerivative_mul

Documentation

Product rule for the absolute Fox derivative.

Source context 6 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 {X : Type u} [DecidableEq X]

Lean source · statement

theorem freeGroupFoxDerivative_mul (u v : FreeGroup X) :
    freeGroupFoxDerivative (X := X) (u * v) =
      freeGroupFoxDerivative (X := X) u +
        (MonoidAlgebra.of ℤ (FreeGroup X) u : GroupRing (FreeGroup X)) •
          freeGroupFoxDerivative (X := X) v

theorem

freeGroupFoxDerivative_inv

L71 ↗

FoxDifferential.FoxCalculus.freeGroupFoxDerivative_inv

Documentation

Inverse rule for the absolute Fox derivative.

Source context 6 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 {X : Type u} [DecidableEq X]

Lean source · statement

theorem freeGroupFoxDerivative_inv (w : FreeGroup X) :
    freeGroupFoxDerivative (X := X) w⁻¹ =
      -((MonoidAlgebra.of ℤ (FreeGroup X) w⁻¹ : GroupRing (FreeGroup X)) •
        freeGroupFoxDerivative (X := X) w)

theorem

freeGroupFoxDerivative_pow

L80 ↗

FoxDifferential.FoxCalculus.freeGroupFoxDerivative_pow

Documentation

Positive-power rule for the absolute Fox derivative.

Source context 6 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 {X : Type u} [DecidableEq X]

Lean source · full declaration

theorem freeGroupFoxDerivative_pow (w : FreeGroup X) (n : ℕ) :
    freeGroupFoxDerivative (X := X) (w ^ n) =
      (Finset.range n).sum (fun k =>
        (MonoidAlgebra.of ℤ (FreeGroup X) (w ^ k) : GroupRing (FreeGroup X)) •
          freeGroupFoxDerivative (X := X) w) := by
  simpa [freeGroupFoxDerivative] using
    relativeFreeGroupFoxDerivative_pow (H := FreeGroup X) X
      (MonoidHom.id (FreeGroup X)) w n

theorem

freeGroupFoxDerivative_conj

L90 ↗

FoxDifferential.FoxCalculus.freeGroupFoxDerivative_conj

Documentation

Conjugation rule for the absolute Fox derivative.

Source context 6 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 {X : Type u} [DecidableEq X]

Lean source · statement

theorem freeGroupFoxDerivative_conj (g h : FreeGroup X) :
    freeGroupFoxDerivative (X := X) (g * h * g⁻¹) =
      freeGroupFoxDerivative (X := X) g +
        (MonoidAlgebra.of ℤ (FreeGroup X) g : GroupRing (FreeGroup X)) •
          freeGroupFoxDerivative (X := X) h -
        (MonoidAlgebra.of ℤ (FreeGroup X) (g * h * g⁻¹) :
          GroupRing (FreeGroup X)) •
          freeGroupFoxDerivative (X := X) g

theorem

freeGroupFoxDerivative_commutator

L103 ↗

FoxDifferential.FoxCalculus.freeGroupFoxDerivative_commutator

Documentation

Commutator rule for the absolute Fox derivative.

Source context 6 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 {X : Type u} [DecidableEq X]

Lean source · statement

theorem freeGroupFoxDerivative_commutator (g h : FreeGroup X) :
    freeGroupFoxDerivative (X := X) ⁅g, h⁆ =
      freeGroupFoxDerivative (X := X) g +
        (MonoidAlgebra.of ℤ (FreeGroup X) g : GroupRing (FreeGroup X)) •
          freeGroupFoxDerivative (X := X) h -
        (MonoidAlgebra.of ℤ (FreeGroup X) (g * h * g⁻¹) :
          GroupRing (FreeGroup X)) •
          freeGroupFoxDerivative (X := X) g -
        (MonoidAlgebra.of ℤ (FreeGroup X) ⁅g, h⁆ : GroupRing (FreeGroup X)) •
          freeGroupFoxDerivative (X := X) h

theorem

freeGroupFoxDerivative_euler_formula

L123 ↗

FoxDifferential.FoxCalculus.freeGroupFoxDerivative_euler_formula

Documentation

The Euler formula for the free-group Fox derivative expresses a word as the augmentation term plus the sum of generator derivatives.

Source context 7 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 {X : Type u} [DecidableEq X]
variable [Fintype X]

Lean source · statement

theorem freeGroupFoxDerivative_euler_formula (w : FreeGroup X) :
    (MonoidAlgebra.of ℤ (FreeGroup X) w : GroupRing (FreeGroup X)) - 1 =
      ∑ x : X,
        freeGroupFoxDerivative (X := X) w x *
          augmentationGenerator (FreeGroup X) (FreeGroup.of x)

theorem

relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative

L139 ↗

FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative

Documentation

Relative Fox derivatives are obtained from the absolute derivative by pushing coefficients forward along \(\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 {X : Type u} [DecidableEq X]
variable [Fintype X]
variable {H : Type v} [Group H]
omit [Fintype X] in

Lean source · statement

theorem relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    relativeFreeGroupFoxDerivative (H := H) X ψ w =
      relativeFreeFoxCoordinatesMap (X := X) ψ
        (freeGroupFoxDerivative (X := X) w)

theorem

relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative_apply

L154 ↗

FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative_apply

Documentation

Component form of the absolute-to-relative comparison: each relative Fox derivative coordinate is the group-ring image of the absolute coordinate.

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 {X : Type u} [DecidableEq X]
variable [Fintype X]
variable {H : Type v} [Group H]
omit [Fintype X] in

Lean source · statement

theorem relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative_apply
    (ψ : FreeGroup X →* H) (w : FreeGroup X) (x : X) :
    relativeFreeGroupFoxDerivative (H := H) X ψ w x =
      groupRingMap ψ (freeGroupFoxDerivative (X := X) w x)

Module documentation

Fox differential: discrete — absolute

Declarations