Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Discrete.Absolute
ProCGroups/FoxDifferential/Discrete/Absolute

ProCGroups.FoxDifferential.Discrete.Absolute

10 Theorems | 1 Definition

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.
imports
Imported by

Declarations

Definition FoxDifferential.FoxCalculus.freeGroupFoxDerivative 
def freeGroupFoxDerivative (w : FreeGroup X) :
    RelativeFreeFoxCoordinates (H := FreeGroup X) X :=
  relativeFreeGroupFoxDerivative (H := FreeGroup X) X
    (MonoidHom.id (FreeGroup X)) w

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

Theorem FoxDifferential.FoxCalculus.freeGroupFoxDerivative_one 
@[simp]
theorem freeGroupFoxDerivative_one :
    freeGroupFoxDerivative (X := X) (1 : FreeGroup X) = 0

The absolute Fox derivative of the identity word is zero.

Show Lean proof
Theorem FoxDifferential.FoxCalculus.freeGroupFoxDerivative_of 
@[simp]
theorem freeGroupFoxDerivative_of (x : X) :
    freeGroupFoxDerivative (X := X) (FreeGroup.of x) =
      Pi.single x (1 : GroupRing (FreeGroup X))

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

Show Lean proof
Theorem FoxDifferential.FoxCalculus.freeGroupFoxDerivative_mul 
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

Product rule for the absolute Fox derivative.

Show Lean proof
Theorem FoxDifferential.FoxCalculus.freeGroupFoxDerivative_inv 
theorem freeGroupFoxDerivative_inv (w : FreeGroup X) :
    freeGroupFoxDerivative (X := X) w⁻¹ =
      -((MonoidAlgebra.of ℤ (FreeGroup X) w⁻¹ : GroupRing (FreeGroup X)) •
        freeGroupFoxDerivative (X := X) w)

Inverse rule for the absolute Fox derivative.

Show Lean proof
Theorem FoxDifferential.FoxCalculus.freeGroupFoxDerivative_pow 
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)

Positive-power rule for the absolute Fox derivative.

Show Lean proof
Theorem FoxDifferential.FoxCalculus.freeGroupFoxDerivative_conj 
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

Conjugation rule for the absolute Fox derivative.

Show Lean proof
Theorem FoxDifferential.FoxCalculus.freeGroupFoxDerivative_commutator 
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

Commutator rule for the absolute Fox derivative.

Show Lean proof
Theorem FoxDifferential.FoxCalculus.freeGroupFoxDerivative_euler_formula 
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)

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

Show Lean proof
Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative 
omit [Fintype X] in
theorem relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    relativeFreeGroupFoxDerivative (H := H) X ψ w =
      relativeFreeFoxCoordinatesMap (X := X) ψ
        (freeGroupFoxDerivative (X := X) w)

Relative Fox derivatives are obtained from the absolute derivative by pushing coefficients forward along \(\psi\).

Show Lean proof
Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative_apply 
omit [Fintype X] in
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)

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

Show Lean proof