ProCGroups.FoxDifferential.Discrete.Jacobian.ChainRule

9 Theorems | 1 Definition

The principal declarations in this module are:

relativeFreeGroupFoxHom_comp The composed derivative \(w \mapsto D(\varphi(w))\) is a crossed differential. - relativeFreeGroupFoxDerivative_comp_apply The relative Fox derivative of a composite free-group homomorphism satisfies the coordinatewise chain-rule sum. - relativeFreeGroupFoxDerivative_comp Fox chain rule for homomorphisms between free groups in vector form. - freeGroupHomFoxJacobian_id The relative Fox Jacobian of the identity homomorphism is the coordinate identity family.

import

ProCGroups.FoxDifferential.Discrete.Jacobian.Basic

Imported by

ProCGroups.FoxDifferential.Discrete.Jacobian.Automorphism

Definition FoxDifferential.FoxCalculus.relativeFreeGroupFoxHom_comp

def relativeFreeGroupFoxHom_comp
    [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
    DifferentialHom (ψ.comp φ) (Y → GroupRing H) where
  toFun w := relativeFreeGroupFoxHom (H := H) Y ψ (φ w)
  map_mul' := by
    intro u v
    funext y
    simp only [scalarCrossedAction_apply, map_mul, ScalarCrossedHom.map_mul,
      MonoidAlgebra.of_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul,
      groupRingScalar, MonoidHom.coe_comp, Function.comp_apply]
    rfl

The composed derivative \(w \mapsto D(\varphi(w))\) is a crossed differential.

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_comp_apply

theorem relativeFreeGroupFoxDerivative_comp_apply
    [DecidableEq X] [Fintype X] [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) (y : Y) :
    relativeFreeGroupFoxDerivative (H := H) Y ψ (φ w) y =
      ∑ x : X,
        relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x *
          freeGroupHomFoxJacobian (H := H) ψ φ x y

The relative Fox derivative of a composite free-group homomorphism satisfies the coordinatewise chain-rule sum.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_comp

theorem relativeFreeGroupFoxDerivative_comp
    [DecidableEq X] [Fintype X] [DecidableEq Y]
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) :
    relativeFreeGroupFoxDerivative (H := H) Y ψ (φ w) =
      fun y : Y =>
        ∑ x : X,
          relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x *
            freeGroupHomFoxJacobian (H := H) ψ φ x y

Fox chain rule for homomorphisms between free groups in vector form.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobian_id

@[simp]
theorem freeGroupHomFoxJacobian_id
    [DecidableEq X]
    (ψ : FreeGroup X →* H) :
    freeGroupHomFoxJacobian (H := H) ψ (MonoidHom.id (FreeGroup X)) =
      fun x : X => Pi.single x (1 : GroupRing H)

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobian_comp_apply

theorem freeGroupHomFoxJacobian_comp_apply
    [DecidableEq Y] [Fintype Y] [DecidableEq Z]
    (ψ : FreeGroup Z →* H)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
    (x : X) (z : Z) :
    freeGroupHomFoxJacobian (H := H) ψ (φ.comp χ) x z =
      ∑ y : Y,
        freeGroupHomFoxJacobian (H := H) (ψ.comp φ) χ x y *
          freeGroupHomFoxJacobian (H := H) ψ φ y z

An entry of the relative Fox Jacobian of a composite is the group-ring-weighted sum of the corresponding Jacobian entries.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobian_comp

theorem freeGroupHomFoxJacobian_comp
    [DecidableEq Y] [Fintype Y] [DecidableEq Z]
    (ψ : FreeGroup Z →* H)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
    freeGroupHomFoxJacobian (H := H) ψ (φ.comp χ) =
      fun x z =>
        ∑ y : Y,
          freeGroupHomFoxJacobian (H := H) (ψ.comp φ) χ x y *
            freeGroupHomFoxJacobian (H := H) ψ φ y z

The Fox Jacobian chain rule for homomorphisms between free groups is expressed in matrix form.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix_id

@[simp]
theorem freeGroupHomFoxJacobianMatrix_id
    [DecidableEq X]
    (ψ : FreeGroup X →* H) :
    freeGroupHomFoxJacobianMatrix (H := H) ψ (MonoidHom.id (FreeGroup X)) =
      (1 : Matrix X X (GroupRing H))

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

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianMatrix_comp

theorem freeGroupHomFoxJacobianMatrix_comp
    [DecidableEq Y] [Fintype Y] [DecidableEq Z]
    (ψ : FreeGroup Z →* H)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
    freeGroupHomFoxJacobianMatrix (H := H) ψ (φ.comp χ) =
      freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp φ) χ *
        freeGroupHomFoxJacobianMatrix (H := H) ψ φ

Fox Jacobian chain rule, packaged as matrix multiplication.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsolute_comp_apply

theorem freeGroupHomFoxJacobianAbsolute_comp_apply
    [DecidableEq Y] [Fintype Y] [DecidableEq Z]
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
    (x : X) (z : Z) :
    freeGroupHomFoxJacobianAbsolute (φ.comp χ) x z =
      ∑ y : Y,
        groupRingMap φ (freeGroupHomFoxJacobianAbsolute χ x y) *
          freeGroupHomFoxJacobianAbsolute φ y z

An entry of the absolute Fox Jacobian of a composite is the group-ring-weighted chain-rule sum.

Show Lean proof

Theorem FoxDifferential.FoxCalculus.freeGroupHomFoxJacobianAbsoluteMatrix_comp

theorem freeGroupHomFoxJacobianAbsoluteMatrix_comp
    [DecidableEq Y] [Fintype Y] [DecidableEq Z]
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
    freeGroupHomFoxJacobianAbsoluteMatrix (φ.comp χ) =
      (freeGroupHomFoxJacobianAbsoluteMatrix χ).map (groupRingMap φ) *
        freeGroupHomFoxJacobianAbsoluteMatrix φ

The absolute Fox Jacobian chain rule is expressed in matrix form.

Show Lean proof

ProCGroups.FoxDifferential.Discrete.Jacobian.ChainRule

Declarations