ChainRule.lean

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

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

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 := by
  funext y
  exact relativeFreeGroupFoxDerivative_comp_apply (H := H) ψ φ w y

theorem freeGroupHomFoxJacobian_id
    [DecidableEq X]
    (ψ : FreeGroup X →* H) :
    freeGroupHomFoxJacobian (H := H) ψ (MonoidHom.id (FreeGroup X)) =
      fun x : X => Pi.single x (1 : GroupRing H) := by
  funext x y
  simp only [freeGroupHomFoxJacobian, MonoidHom.id_apply, relativeFreeGroupFoxDerivative_of]

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

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 := by
  funext x z
  exact freeGroupHomFoxJacobian_comp_apply (H := H) ψ φ χ x z

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

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) ψ φ

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

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