Yamaguchi Lean 4 Library
FoxDifferential.Discrete.FoxCalculus.Boundary
FoxDifferential/Discrete/FoxCalculus/Boundary

FoxDifferential.Discrete.FoxCalculus.Boundary

9 Theorem | 1 Definition

This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.

Open this file on GitHub
import
Imported by

Declarations

Definition FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary GitHub 
def relativeFreeGroupFoxBoundary :
    RelativeFreeFoxCoordinates (H := H) X →ₗ[GroupRing H] GroupRing H :=
  { toFun := fun a =>
      ∑ x : X, a x * augmentationGenerator H (ψ (FreeGroup.of x))
    map_add' := by
      intro a b
      simp only [Pi.add_apply, augmentationGenerator_eq_groupRingBoundary, add_mul, Finset.sum_add_distrib]
    map_smul' := by
      intro r a
      simp only [Pi.smul_apply, smul_eq_mul, augmentationGenerator_eq_groupRingBoundary, mul_assoc,
  RingHom.id_apply, Finset.mul_sum]}

The pushed-forward Fox boundary \(a \mapsto \sum_x a_x (\psi(x) - 1)\).

Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_apply GitHub 
theorem relativeFreeGroupFoxBoundary_apply
    (a : RelativeFreeFoxCoordinates (H := H) X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ a =
      ∑ x : X, a x * augmentationGenerator H (ψ (FreeGroup.of x))

The relative free-group Fox boundary is evaluated on canonical generators and then extended linearly to the coordinate module.

Show proof
Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_single GitHub 
theorem relativeFreeGroupFoxBoundary_single (x : X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ
        (Pi.single x (1 : GroupRing H)) =
      augmentationGenerator H (ψ (FreeGroup.of x))

The relative Fox boundary sends a coordinate basis vector to the corresponding augmentation generator.

Show proof
Theorem FoxDifferential.FoxCalculus.toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap GitHub 
theorem toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap :
    (toGroupRing ψ).comp
        (relativeFreeFoxCoordinatesLinearMap (H := H) X ψ) =
      relativeFreeGroupFoxBoundary (H := H) X ψ

Composing the universal boundary with the coordinate-to-differential map gives the pushed-forward Fox boundary.

Show proof
Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_fundamental_formula GitHub 
theorem relativeFreeGroupFoxDerivative_fundamental_formula (w : FreeGroup X) :
    groupRingBoundary ψ w =
      ∑ x : X,
        relativeFreeGroupFoxDerivative (H := H) X ψ w x *
          augmentationGenerator H (ψ (FreeGroup.of x))

Relative Fox fundamental formula, also known as the Fox--Euler formula: \(\psi(w) - 1 = \sum_x (\partial w/\partial x) (\psi(x) - 1)\).

Show proof
Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_derivative GitHub 
theorem relativeFreeGroupFoxBoundary_derivative (w : FreeGroup X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ
        (relativeFreeGroupFoxDerivative (H := H) X ψ w) =
      groupRingBoundary ψ w

Fox boundary form of the relative Fox fundamental formula.

Show proof
Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_of_differentialMap GitHub 
theorem relativeFreeGroupFoxBoundary_of_differentialMap
    (delta : FreeGroup X → RelativeFreeFoxCoordinates (H := H) X)
    (hdelta : IsDifferentialMap (A := RelativeFreeFoxCoordinates (H := H) X) ψ delta)
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : GroupRing H))
    (w : FreeGroup X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ (delta w) =
      groupRingBoundary ψ w

Conditional relative Fox boundary formula. Any differential map on a free group with the standard coordinate values satisfies the relative Fox boundary formula.

Show proof
Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_fundamental_formula_of_differentialMap GitHub 
theorem relativeFreeGroupFoxDerivative_fundamental_formula_of_differentialMap
    (delta : FreeGroup X → RelativeFreeFoxCoordinates (H := H) X)
    (hdelta : IsDifferentialMap (A := RelativeFreeFoxCoordinates (H := H) X) ψ delta)
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : GroupRing H))
    (w : FreeGroup X) :
    groupRingBoundary ψ w =
      ∑ x : X,
        delta w x * augmentationGenerator H (ψ (FreeGroup.of x))

Conditional relative Fox fundamental formula. The Fox-Euler sum computed from any differential map with standard coordinate values is \([\psi(w)]-1\).

Show proof
Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_euler_formula_of_differentialMap GitHub 
theorem relativeFreeGroupFoxDerivative_euler_formula_of_differentialMap
    (delta : FreeGroup X → RelativeFreeFoxCoordinates (H := H) X)
    (hdelta : IsDifferentialMap (A := RelativeFreeFoxCoordinates (H := H) X) ψ delta)
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : GroupRing H))
    (w : FreeGroup X) :
    (MonoidAlgebra.of ℤ H (ψ w) : GroupRing H) - 1 =
      ∑ x : X,
        delta w x * augmentationGenerator H (ψ (FreeGroup.of x))

Explicit \(\psi(w)-1\) version of the conditional relative Fox-Euler formula.

Show proof
Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_euler_formula GitHub 
theorem relativeFreeGroupFoxDerivative_euler_formula (w : FreeGroup X) :
    (MonoidAlgebra.of ℤ H (ψ w) : GroupRing H) - 1 =
      ∑ x : X,
        relativeFreeGroupFoxDerivative (H := H) X ψ w x *
          augmentationGenerator H (ψ (FreeGroup.of x))

Explicit \(\psi(w)-1\) version of the relative Fox--Euler formula.

Show proof