Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Discrete.FreeExpansion
ProCGroups/FoxDifferential/Discrete/FreeExpansion

ProCGroups.FoxDifferential.Discrete.FreeExpansion

5 Theorems | 2 Definitions

The principal declarations in this module are:

  • freeCrossedDifferentialExpansion Prescribed values on the free generators determine the Fox-coordinate expansion. - freeCrossedDifferentialExpansionHom The Fox-coordinate expansion is a crossed differential. - freeCrossedDifferentialExpansion_one The Fox-coordinate expansion of the identity word is zero. - freeCrossedDifferentialExpansion_of The Fox-coordinate expansion of a free generator returns its prescribed basis value.
import
Imported by

Declarations

Definition FoxDifferential.FoxCalculus.freeCrossedDifferentialExpansion 
def freeCrossedDifferentialExpansion (w : FreeGroup X) : A :=
  ∑ x : X,
    relativeFreeGroupFoxDerivative (H := H) X ψ w x • basisValue x

Prescribed values on the free generators determine the Fox-coordinate expansion.

Theorem FoxDifferential.FoxCalculus.freeCrossedDifferentialExpansion_one 
@[simp]
theorem freeCrossedDifferentialExpansion_one :
    freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue 1 = 0

The Fox-coordinate expansion of the identity word is zero.

Show Lean proof
Theorem FoxDifferential.FoxCalculus.freeCrossedDifferentialExpansion_of 
@[simp]
theorem freeCrossedDifferentialExpansion_of (x : X) :
    freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue (FreeGroup.of x) =
      basisValue x

The Fox-coordinate expansion of a free generator returns its prescribed basis value.

Show Lean proof
Definition FoxDifferential.FoxCalculus.freeCrossedDifferentialExpansionHom 
def freeCrossedDifferentialExpansionHom : DifferentialHom ψ A where
  toFun := freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue
  map_mul' := by
    intro u v
    simp only [scalarCrossedAction_apply, freeCrossedDifferentialExpansion]
    change
      (∑ x : X,
          relativeFreeGroupFoxDerivative (H := H) X ψ (u * v) x • basisValue x) =
        (∑ x : X,
          relativeFreeGroupFoxDerivative (H := H) X ψ u x • basisValue x) +
          (MonoidAlgebra.of ℤ H (ψ u) : GroupRing H) •
            (∑ x : X,
              relativeFreeGroupFoxDerivative (H := H) X ψ v x • basisValue x)
    rw [relativeFreeGroupFoxDerivative_mul]
    simp only [MonoidAlgebra.of_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul,
      add_smul, Finset.sum_add_distrib, Finset.smul_sum, smul_smul]

The Fox-coordinate expansion is a crossed differential.

Theorem FoxDifferential.FoxCalculus.freeCrossedDifferentialWithCoeff_groupRingScalar_eq_expansion 
theorem freeCrossedDifferentialWithCoeff_groupRingScalar_eq_expansion (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeff (A := A) (groupRingScalar ψ) basisValue w =
      freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue w

The coefficient-generic free crossed differential over a group ring is the Fox-coordinate expansion of its generator values.

Show Lean proof
Theorem FoxDifferential.FoxCalculus.freeCrossedDifferentialWithCoeffCoordinates_eq_relativeFreeGroupFoxDerivative 
omit [Fintype X] in
theorem freeCrossedDifferentialWithCoeffCoordinates_eq_relativeFreeGroupFoxDerivative
    (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeffCoordinates
        (X := X) (groupRingScalar ψ) w =
      relativeFreeGroupFoxDerivative (H := H) X ψ w

The coefficient-generic coordinate crossed differential specializes to the usual relative Fox derivative over a group ring.

Show Lean proof
Theorem FoxDifferential.FoxCalculus.crossedHom_comp_relativeFreeGroupFoxDerivative 
theorem crossedHom_comp_relativeFreeGroupFoxDerivative
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (delta : DifferentialHom ψ A) (w : FreeGroup X) :
    delta (φ w) =
      ∑ x : X,
        relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x •
          delta (φ (FreeGroup.of x))

Abstract Fox chain rule for an arbitrary crossed differential.

Show Lean proof