ProCGroups.FoxDifferential.Discrete.FoxCalculus.Derivative

10 Theorems | 3 Definitions

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.

imports

Imported by

Definition FoxDifferential.FoxCalculus.relativeFreeGroupFoxLift

def relativeFreeGroupFoxLift :
    FreeGroup X →* CrossedSemidirectProduct (RelativeFoxAction (H := H) X) :=
  FreeGroup.lift fun x =>
    { left := Multiplicative.ofAdd (Pi.single x (1 : GroupRing H))
      right := ψ (FreeGroup.of x) }

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

Definition FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative

def relativeFreeGroupFoxDerivative (w : FreeGroup X) :
    RelativeFreeFoxCoordinates (H := H) X :=
  Multiplicative.toAdd (relativeFreeGroupFoxLift (H := H) X ψ w).left

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

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxLift_right

@[simp]
theorem relativeFreeGroupFoxLift_right (w : FreeGroup X) :
    (relativeFreeGroupFoxLift (H := H) X ψ w).right = ψ w

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_one

@[simp]
theorem relativeFreeGroupFoxDerivative_one :
    relativeFreeGroupFoxDerivative (H := H) X ψ (1 : FreeGroup X) = 0

The relative Fox derivative of the identity word is zero.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_of

@[simp]
theorem relativeFreeGroupFoxDerivative_of (x : X) :
    relativeFreeGroupFoxDerivative (H := H) X ψ (FreeGroup.of x) =
      Pi.single x (1 : GroupRing H)

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_mul

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₂

Relative Fox product rule.

Show Lean proof

Definition FoxDifferential.FoxCalculus.relativeFreeGroupFoxHom

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₂

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

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxHom_apply

@[simp]
theorem relativeFreeGroupFoxHom_apply (w : FreeGroup X) :
    relativeFreeGroupFoxHom (H := H) X ψ w =
      relativeFreeGroupFoxDerivative (H := H) X ψ w

The bundled relative Fox crossed homomorphism evaluates to the relative Fox derivative.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_inv

theorem relativeFreeGroupFoxDerivative_inv (w : FreeGroup X) :
    relativeFreeGroupFoxDerivative (H := H) X ψ w⁻¹ =
      -((MonoidAlgebra.of ℤ H (ψ w⁻¹) : GroupRing H) •
        relativeFreeGroupFoxDerivative (H := H) X ψ w)

The relative Fox derivative satisfies the inverse rule.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxHom_unique

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 ψ

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_pow

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)

Relative Fox derivative of a positive power.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_conj

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

Relative Fox derivative of a conjugate.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_commutator

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

Relative Fox derivative of a commutator.

Show Lean proof

ProCGroups.FoxDifferential.Discrete.FoxCalculus.Derivative

Declarations