ProCGroups.FoxDifferential.Discrete.Jacobian.Basic

10 Theorems | 4 Definitions

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.

import

ProCGroups.FoxDifferential.Discrete.Absolute

Imported by

ProCGroups.FoxDifferential.Discrete.Jacobian.ChainRule

Definition FoxDifferential.FoxCalculus.freeGroupHomFoxJacobian

def freeGroupHomFoxJacobian
    [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
    X → Y → GroupRing H :=
  fun x =>
    relativeFreeGroupFoxDerivative (H := H) Y ψ (φ (FreeGroup.of x))

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.

Definition FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix

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

The relative Fox Jacobian, packaged as a matrix.

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix_apply

@[simp]
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

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobian_eq_freeCrossedDifferentialWithCoeffJacobian

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

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix_eq_freeCrossedDifferentialWithCoeffJacobianMatrix

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

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

Show Lean proof

Definition FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsolute

def freeGroupHomFoxJacobianAbsolute
    [DecidableEq Y]
    (φ : FreeGroup X →* FreeGroup Y) :
    X → Y → GroupRing (FreeGroup Y) :=
  freeGroupHomFoxJacobian (H := FreeGroup Y) (MonoidHom.id (FreeGroup Y)) φ

The absolute Fox Jacobian of a homomorphism between free groups.

Definition FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsoluteMatrix

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

The absolute Fox Jacobian, packaged as a matrix.

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsoluteMatrix_apply

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

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsolute_id

@[simp]
theorem freeGroupHomFoxJacobianAbsolute_id
    [DecidableEq X] :
    freeGroupHomFoxJacobianAbsolute (MonoidHom.id (FreeGroup X)) =
      fun x : X => Pi.single x (1 : GroupRing (FreeGroup X))

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsoluteMatrix_id

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

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobian_mapDomain_apply

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)

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix_mapDomain

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

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobian_eq_map_absolute_apply

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)

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix_eq_map_absolute

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

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

Show Lean proof

ProCGroups.FoxDifferential.Discrete.Jacobian.Basic

Declarations