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

ProCGroups.FoxDifferential.Discrete.Naturality

3 Theorems | 1 Definition

The principal declarations in this module are:

  • relativeFreeFoxCoordinatesMap A homomorphism of coefficient groups pushes a relative Fox-coordinate vector forward. - relativeFreeFoxCoordinatesMap_apply Pushing a relative Fox-coordinate vector along φ applies groupRingMap φ to the selected coordinate. - relativeFreeGroupFoxDerivative_mapDomain Relative Fox derivatives are natural under coefficient push-forward. - relativeFreeGroupFoxDerivative_mapDomain_apply Component form of coefficient-push-forward naturality for relative free-group Fox derivatives.
import
Imported by

Declarations

Definition FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesMap 
def relativeFreeFoxCoordinatesMap :
    RelativeFreeFoxCoordinates (H := H) X → RelativeFreeFoxCoordinates (H := K) X :=
  fun a x => groupRingMap φ (a x)

A homomorphism of coefficient groups pushes a relative Fox-coordinate vector forward.

Theorem FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesMap_apply 
omit [DecidableEq X] in
@[simp]
theorem relativeFreeFoxCoordinatesMap_apply
    (a : RelativeFreeFoxCoordinates (H := H) X) (x : X) :
    relativeFreeFoxCoordinatesMap (X := X) φ a x = groupRingMap φ (a x)

Pushing a relative Fox-coordinate vector along φ applies groupRingMap φ to the selected coordinate.

Show Lean proof
Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_mapDomain 
theorem relativeFreeGroupFoxDerivative_mapDomain (w : FreeGroup X) :
    relativeFreeGroupFoxDerivative (H := K) X (φ.comp ψ) w =
      relativeFreeFoxCoordinatesMap (X := X) φ
        (relativeFreeGroupFoxDerivative (H := H) X ψ w)

Relative Fox derivatives are natural under coefficient push-forward.

Show Lean proof
Theorem FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_mapDomain_apply 
theorem relativeFreeGroupFoxDerivative_mapDomain_apply (w : FreeGroup X) (x : X) :
    relativeFreeGroupFoxDerivative (H := K) X (φ.comp ψ) w x =
      groupRingMap φ (relativeFreeGroupFoxDerivative (H := H) X ψ w x)

Component form of coefficient-push-forward naturality for relative free-group Fox derivatives.

Show Lean proof