ProCGroups.FoxDifferential.Common.FreeCrossedDifferential

35 Theorems | 15 Definitions

The principal declarations in this module are:

freeCrossedHomActionLift The standard semidirect-product lift producing a free crossed homomorphism for an arbitrary additive action. - freeCrossedHomForAction The free crossed homomorphism with prescribed generator values for a general additive action. This is the canonical action-level construction; scalar Fox differentials specialize it via scalarCrossedAction. - freeCrossedHomActionLift_right The free-group component of semidirect multiplication. - freeCrossedHomForAction_of The free crossed homomorphism takes each free generator to its prescribed basis value.

imports

ProCGroups.FoxDifferential.Common.CrossedDifferential
ProCGroups.FoxDifferential.Common.Jacobian
Mathlib.GroupTheory.FreeGroup.Basic

Imported by

Definition FoxDifferential.freeCrossedHomActionLift

def freeCrossedHomActionLift :
    FreeGroup X →* CrossedSemidirectProduct action :=
  FreeGroup.lift fun x => ⟨Multiplicative.ofAdd (basisValue x), FreeGroup.of x⟩

The standard semidirect-product lift producing a free crossed homomorphism for an arbitrary additive action.

Theorem FoxDifferential.freeCrossedHomActionLift_right

@[simp]
theorem freeCrossedHomActionLift_right (w : FreeGroup X) :
    (freeCrossedHomActionLift action basisValue w).right = w

The free-group component of semidirect multiplication.

Show Lean proof

Definition FoxDifferential.freeCrossedHomForAction

def freeCrossedHomForAction : CrossedHom action :=
  CrossedHom.ofSemidirectMonoidHom
    (freeCrossedHomActionLift action basisValue)
    (freeCrossedHomActionLift_right action basisValue)

The free crossed homomorphism with prescribed generator values for a general additive action. This is the canonical action-level construction; scalar Fox differentials specialize it via scalarCrossedAction.

Theorem FoxDifferential.freeCrossedHomForAction_of

@[simp]
theorem freeCrossedHomForAction_of (x : X) :
    freeCrossedHomForAction action basisValue (FreeGroup.of x) = basisValue x

The free crossed homomorphism takes each free generator to its prescribed basis value.

Show Lean proof

Theorem FoxDifferential.freeCrossedHomForAction_unique

theorem freeCrossedHomForAction_unique
    (delta : CrossedHom action)
    (hbasis : ∀ x : X, delta (FreeGroup.of x) = basisValue x) :
    delta = freeCrossedHomForAction action basisValue

A crossed homomorphism on a free group is determined by its values on the free generators, for an arbitrary additive action.

Show Lean proof

Definition FoxDifferential.crossedHomForActionEquivGeneratorValues

def crossedHomForActionEquivGeneratorValues : CrossedHom action ≃ (X → A) where
  toFun delta x := delta (FreeGroup.of x)
  invFun values := freeCrossedHomForAction action values
  left_inv delta := (freeCrossedHomForAction_unique action
    (fun x => delta (FreeGroup.of x)) delta (by intro x; rfl)).symm
  right_inv values := by
    funext x
    exact freeCrossedHomForAction_of action values x

General-action crossed homomorphisms on a free group are equivalent to generator-value assignments.

Definition FoxDifferential.freeCrossedDifferentialWithCoeffLift

def freeCrossedDifferentialWithCoeffLift :
    FreeGroup X →* CrossedSemidirectProduct (scalarCrossedAction (A := A) coeff) :=
  freeCrossedHomActionLift (scalarCrossedAction (A := A) coeff) basisValue

The semidirect lift whose left component is the free crossed differential with prescribed generator values.

Definition FoxDifferential.freeCrossedDifferentialWithCoeff

def freeCrossedDifferentialWithCoeff (w : FreeGroup X) : A :=
  Multiplicative.toAdd
    (freeCrossedDifferentialWithCoeffLift (A := A) coeff basisValue w).left

The free crossed differential with coefficient homomorphism coeff and prescribed generator values basisValue.

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffLift_right

@[simp]
theorem freeCrossedDifferentialWithCoeffLift_right (w : FreeGroup X) :
    (freeCrossedDifferentialWithCoeffLift (A := A) coeff basisValue w).right = w

The right component of the free crossed-differential lift is the identity on the free group.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeff_one

@[simp]
theorem freeCrossedDifferentialWithCoeff_one :
    freeCrossedDifferentialWithCoeff (A := A) coeff basisValue 1 = 0

The free crossed differential sends the identity word to zero.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeff_of

@[simp]
theorem freeCrossedDifferentialWithCoeff_of (x : X) :
    freeCrossedDifferentialWithCoeff (A := A) coeff basisValue (FreeGroup.of x) =
      basisValue x

The free crossed differential sends a free generator to its prescribed value.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeff_mul

theorem freeCrossedDifferentialWithCoeff_mul (u v : FreeGroup X) :
    freeCrossedDifferentialWithCoeff (A := A) coeff basisValue (u * v) =
      freeCrossedDifferentialWithCoeff (A := A) coeff basisValue u +
        coeff u • freeCrossedDifferentialWithCoeff (A := A) coeff basisValue v

Product rule for the free crossed differential with arbitrary coefficients.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeff_inv

theorem freeCrossedDifferentialWithCoeff_inv (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeff (A := A) coeff basisValue w⁻¹ =
      -(coeff w⁻¹ • freeCrossedDifferentialWithCoeff (A := A) coeff basisValue w)

Inverse rule for the free crossed differential with arbitrary coefficients.

Show Lean proof

Definition FoxDifferential.freeCrossedHomWithCoeff

def freeCrossedHomWithCoeff : ScalarCrossedHom coeff A :=
  freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue

The free crossed differential with coefficient homomorphism \(\mathrm{coeff}\) and prescribed generator values \(\mathrm{basisValue}\).

Theorem FoxDifferential.freeCrossedHomWithCoeff_apply

@[simp]
theorem freeCrossedHomWithCoeff_apply (w : FreeGroup X) :
    freeCrossedHomWithCoeff (A := A) coeff basisValue w =
      freeCrossedDifferentialWithCoeff (A := A) coeff basisValue w

Evaluating the bundled free crossed homomorphism gives the corresponding free crossed differential.

Show Lean proof

Theorem FoxDifferential.freeCrossedHomWithCoeff_of

@[simp]
theorem freeCrossedHomWithCoeff_of (x : X) :
    freeCrossedHomWithCoeff (A := A) coeff basisValue (FreeGroup.of x) = basisValue x

The free crossed differential sends a free generator to its prescribed value.

Show Lean proof

Theorem FoxDifferential.freeCrossedHomWithCoeff_unique

theorem freeCrossedHomWithCoeff_unique
    (delta : ScalarCrossedHom coeff A)
    (hbasis : ∀ x : X, delta (FreeGroup.of x) = basisValue x) :
    delta = freeCrossedHomWithCoeff (A := A) coeff basisValue

Uniqueness of crossed differentials on a free group from their generator values, for an arbitrary coefficient homomorphism.

Show Lean proof

Theorem FoxDifferential.existsUnique_freeCrossedHomWithCoeff

theorem existsUnique_freeCrossedHomWithCoeff :
    ∃! delta : ScalarCrossedHom coeff A,
      ∀ x : X, delta (FreeGroup.of x) = basisValue x

Existence and uniqueness of crossed differentials on a free group from arbitrary generator values and an arbitrary coefficient homomorphism.

Show Lean proof

Definition FoxDifferential.crossedHomEquivGeneratorValues

def crossedHomEquivGeneratorValues : ScalarCrossedHom coeff A ≃ (X → A) where
  toFun delta := fun x => delta (FreeGroup.of x)
  invFun basisValue := freeCrossedHomWithCoeff (A := A) coeff basisValue
  left_inv delta := by
    exact (freeCrossedHomWithCoeff_unique (A := A) coeff
      (fun x => delta (FreeGroup.of x)) delta (by intro x; rfl)).symm
  right_inv basisValue := by
    funext x
    exact freeCrossedHomWithCoeff_of (A := A) coeff basisValue x

Crossed differentials on a free group are equivalent to assignments of values on the free generators.

Definition FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates

def freeCrossedDifferentialWithCoeffCoordinates
    (coeff : FreeGroup X →* S) (w : FreeGroup X) : X → S :=
  freeCrossedDifferentialWithCoeff
    (A := X → S) coeff (fun x => Pi.single x (1 : S)) w

The universal Fox-coordinate crossed differential for an arbitrary coefficient homomorphism to a ring.

Definition FoxDifferential.freeCrossedHomWithCoeffCoordinates

def freeCrossedHomWithCoeffCoordinates
    (coeff : FreeGroup X →* S) : ScalarCrossedHom coeff (X → S) :=
  freeCrossedHomWithCoeff
    (A := X → S) coeff (fun x => Pi.single x (1 : S))

The universal Fox-coordinate crossed differential for an arbitrary coefficient homomorphism to a ring.

Theorem FoxDifferential.freeCrossedHomWithCoeffCoordinates_apply

@[simp]
theorem freeCrossedHomWithCoeffCoordinates_apply
    (coeff : FreeGroup X →* S) (w : FreeGroup X) :
    freeCrossedHomWithCoeffCoordinates (X := X) coeff w =
      freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff w

Evaluating the bundled coordinate crossed homomorphism gives the unbundled coordinate differential.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates_one

@[simp]
theorem freeCrossedDifferentialWithCoeffCoordinates_one
    (coeff : FreeGroup X →* S) :
    freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff (1 : FreeGroup X) = 0

The coordinate crossed differential sends the identity word to zero.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates_of

@[simp]
theorem freeCrossedDifferentialWithCoeffCoordinates_of
    (coeff : FreeGroup X →* S) (x : X) :
    freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff (FreeGroup.of x) =
      Pi.single x (1 : S)

The coordinate crossed differential sends a generator to the standard coordinate vector.

Show Lean proof

Definition FoxDifferential.freeCrossedDifferentialWithCoeffExpansionLinearMap

def freeCrossedDifferentialWithCoeffExpansionLinearMap
    [Fintype X] (basisValue : X → B) : (X → S) →ₗ[S] B where
  toFun v := ∑ x : X, v x • basisValue x
  map_add' v w := by
    simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
  map_smul' a v := by
    simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum, smul_smul]

The finite linear map evaluating a coordinate vector on prescribed generator values.

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffExpansionLinearMap_apply

omit [DecidableEq X] in
@[simp]
theorem freeCrossedDifferentialWithCoeffExpansionLinearMap_apply
    [Fintype X] (basisValue : X → B) (v : X → S) :
    freeCrossedDifferentialWithCoeffExpansionLinearMap (X := X) basisValue v =
      ∑ x : X, v x • basisValue x

The coefficient-expansion linear map evaluates v as ∑ x, v x • basisValue x.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffExpansionLinearMap_single

@[simp]
theorem freeCrossedDifferentialWithCoeffExpansionLinearMap_single
    [Fintype X] (basisValue : X → B) (x : X) :
    freeCrossedDifferentialWithCoeffExpansionLinearMap (X := X) basisValue
        (Pi.single x (1 : S)) =
      basisValue x

The expansion linear map sends a standard coordinate vector to the corresponding value.

Show Lean proof

Definition FoxDifferential.freeCrossedDifferentialWithCoeffExpansion

def freeCrossedDifferentialWithCoeffExpansion
    [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B)
    (w : FreeGroup X) : B :=
  freeCrossedDifferentialWithCoeffExpansionLinearMap (X := X) basisValue
    (freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff w)

The Fox-coordinate expansion determined by arbitrary coefficient coordinates.

Definition FoxDifferential.freeCrossedHomWithCoeffExpansion

def freeCrossedHomWithCoeffExpansion
    [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) :
    ScalarCrossedHom coeff B :=
  ScalarCrossedHom.mapLinear
    (freeCrossedHomWithCoeffCoordinates (X := X) coeff)
    (freeCrossedDifferentialWithCoeffExpansionLinearMap (X := X) basisValue)

Arbitrary coefficient coordinates determine the Fox-coordinate expansion.

Theorem FoxDifferential.freeCrossedHomWithCoeffExpansion_apply

@[simp]
theorem freeCrossedHomWithCoeffExpansion_apply
    [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) (w : FreeGroup X) :
    freeCrossedHomWithCoeffExpansion (X := X) coeff basisValue w =
      freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue w

Evaluating the bundled coordinate expansion gives the corresponding unbundled Fox expansion.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffExpansion_of

@[simp]
theorem freeCrossedDifferentialWithCoeffExpansion_of
    [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) (x : X) :
    freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue (FreeGroup.of x) =
      basisValue x

The coefficient-coordinate expansion sends each generator to its prescribed value.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeff_eq_expansion

theorem freeCrossedDifferentialWithCoeff_eq_expansion
    [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeff (A := B) coeff basisValue w =
      freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue w

A free crossed differential is its coefficient-coordinate expansion.

Show Lean proof

Theorem FoxDifferential.freeCrossedHomWithCoeff_comp_expansion

theorem freeCrossedHomWithCoeff_comp_expansion
    [Fintype X]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (delta : ScalarCrossedHom coeff B) (w : FreeGroup X) :
    delta (φ w) =
      freeCrossedDifferentialWithCoeffExpansion
        (X := X) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) w

Abstract Fox chain rule: composing a crossed differential with a free-group homomorphism is the coordinate expansion using the pulled-back coefficient homomorphism.

Show Lean proof

Definition FoxDifferential.freeCrossedDifferentialWithCoeffJacobian

omit [DecidableEq X] in
def freeCrossedDifferentialWithCoeffJacobian
    [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
    X → Y → S :=
  fun x => freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ (FreeGroup.of x))

The abstract Fox-Jacobian of a homomorphism of free sources, with coefficients in S.

Definition FoxDifferential.freeCrossedDifferentialWithCoeffJacobianMatrix

omit [DecidableEq X] in
def freeCrossedDifferentialWithCoeffJacobianMatrix
    [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
    Matrix X Y S :=
  foxJacobianMatrix (freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ)

The abstract Fox-Jacobian of a free-source homomorphism as a matrix.

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffJacobianMatrix_apply

omit [DecidableEq X] in
@[simp]
theorem freeCrossedDifferentialWithCoeffJacobianMatrix_apply
    [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (x : X) (y : Y) :
    freeCrossedDifferentialWithCoeffJacobianMatrix (X := X) coeff φ x y =
      freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x y

The abstract Fox-Jacobian matrix entry is the corresponding Fox-Jacobian component.

Show Lean proof

Definition FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap

omit [DecidableEq X] in
def freeCrossedDifferentialWithCoeffJacobianLinearMap
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
    (X → S) →ₗ[S] (Y → S) :=
  foxJacobianLinearMap (freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ)

The abstract Fox-Jacobian determines a finite linear map between the corresponding free coefficient modules.

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap_apply

omit [DecidableEq X] in
@[simp]
theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_apply
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (v : X → S) (y : Y) :
    freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ v y =
      ∑ x : X, v x * freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x y

Evaluation of the linear map associated with the abstract Fox-Jacobian is computed by the corresponding matrix coefficient formula.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap_single

@[simp]
theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_single
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) (x : X) :
    freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ
        (Pi.single x (1 : S)) =
      freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x

The abstract Fox-Jacobian linear map sends a source basis vector to the corresponding row.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap_eq_vecMul

omit [DecidableEq X] in
theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_eq_vecMul
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) (v : X → S) :
    freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ v =
      Matrix.vecMul v
        (freeCrossedDifferentialWithCoeffJacobianMatrix (X := X) coeff φ)

The abstract Fox-Jacobian linear map is row-vector multiplication by its matrix.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffJacobian_id

@[simp]
theorem freeCrossedDifferentialWithCoeffJacobian_id (coeff : FreeGroup X →* S) :
    freeCrossedDifferentialWithCoeffJacobian
        (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
      foxJacobianId (R := S) (X := X)

The abstract Fox-Jacobian of the identity homomorphism is the identity family.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffJacobianMatrix_id

@[simp]
theorem freeCrossedDifferentialWithCoeffJacobianMatrix_id (coeff : FreeGroup X →* S) :
    freeCrossedDifferentialWithCoeffJacobianMatrix
        (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
      (1 : Matrix X X S)

The abstract Fox-Jacobian matrix of the identity homomorphism is the identity matrix.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap_id

@[simp]
theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_id
    [Fintype X] (coeff : FreeGroup X →* S) :
    freeCrossedDifferentialWithCoeffJacobianLinearMap
        (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
      (LinearMap.id : (X → S) →ₗ[S] (X → S))

The abstract Fox-Jacobian linear map of the identity homomorphism is the identity.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates_comp_linearMap

theorem freeCrossedDifferentialWithCoeffCoordinates_comp_linearMap
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ w) =
      freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ
        (freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w)

Abstract Fox chain rule for coordinate vectors, written as a Jacobian linear-map identity.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates_comp_apply

theorem freeCrossedDifferentialWithCoeffCoordinates_comp_apply
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) (y : Y) :
    freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ w) y =
      ∑ x : X,
        freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w x *
          freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x y

Component form of the abstract Fox chain rule: the pushed-forward coordinate is the sum over source coordinates weighted by the Fox-Jacobian.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates_comp_matrix

theorem freeCrossedDifferentialWithCoeffCoordinates_comp_matrix
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ w) =
      Matrix.vecMul
        (freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w)
        (freeCrossedDifferentialWithCoeffJacobianMatrix (X := X) coeff φ)

Abstract Fox chain rule for coordinate vectors, written as matrix multiplication.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffJacobian_comp_apply

omit [DecidableEq X] in
theorem freeCrossedDifferentialWithCoeffJacobian_comp_apply
    {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
    (coeff : FreeGroup Z →* S)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
    (x : X) (z : Z) :
    freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Z) coeff (φ.comp χ) x z =
      ∑ y : Y,
        freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (coeff.comp φ) χ x y *
          freeCrossedDifferentialWithCoeffJacobian (X := Y) (Y := Z) coeff φ y z

Component form of the abstract Fox-Jacobian chain rule for a composite of free-group homomorphisms.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffJacobian_comp

omit [DecidableEq X] in
theorem freeCrossedDifferentialWithCoeffJacobian_comp
    {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
    (coeff : FreeGroup Z →* S)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
    freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Z) coeff (φ.comp χ) =
      fun x z =>
        ∑ y : Y,
          freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (coeff.comp φ) χ x y *
            freeCrossedDifferentialWithCoeffJacobian (X := Y) (Y := Z) coeff φ y z

The abstract Fox-Jacobian chain rule is expressed in family form.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap_comp

omit [DecidableEq X] in
theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_comp
    {Z : Type*} [Fintype X] [Fintype Y] [DecidableEq Y] [DecidableEq Z]
    (coeff : FreeGroup Z →* S)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
    (freeCrossedDifferentialWithCoeffJacobianLinearMap (X := Y) (Y := Z) coeff φ).comp
        (freeCrossedDifferentialWithCoeffJacobianLinearMap
          (X := X) (Y := Y) (coeff.comp φ) χ) =
      freeCrossedDifferentialWithCoeffJacobianLinearMap
        (X := X) (Y := Z) coeff (φ.comp χ)

The abstract Fox-Jacobian chain rule is expressed in linear-map form.

Show Lean proof

Theorem FoxDifferential.freeCrossedDifferentialWithCoeffJacobianMatrix_comp

omit [DecidableEq X] in
theorem freeCrossedDifferentialWithCoeffJacobianMatrix_comp
    {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
    (coeff : FreeGroup Z →* S)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
    freeCrossedDifferentialWithCoeffJacobianMatrix
        (X := X) (Y := Z) coeff (φ.comp χ) =
      freeCrossedDifferentialWithCoeffJacobianMatrix
          (X := X) (Y := Y) (coeff.comp φ) χ *
        freeCrossedDifferentialWithCoeffJacobianMatrix
          (X := Y) (Y := Z) coeff φ

The abstract Fox-Jacobian chain rule is expressed in matrix form.

Show Lean proof

ProCGroups.FoxDifferential.Common.FreeCrossedDifferential

Declarations