ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Fundamental

6 Theorems

The principal declarations in this module are:

zcFreeGroupFoxBoundary_derivativeVector The boundary-map form of the completed Fox fundamental formula. - zcFreeGroupFoxBoundary_of_crossedHom Conditional completed Fox boundary formula. Any completed crossed differential on a free group with the standard basis values satisfies the completed Fox boundary formula. - zcFreeGroupFoxDerivative_fundamental_formula_of_crossedHom Conditional completed Fox fundamental formula. The finite Fox-Euler sum computed from any completed crossed differential with standard basis values is \([\psi(w)]-1\). - zcFreeGroupFoxDerivative_euler_formula_of_crossedHom The explicit \([\psi(w)]-1\) form of the conditional completed Fox-Euler formula.

import

ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Coordinates

Imported by

Theorem FoxDifferential.zcFreeGroupFoxBoundary_derivativeVector

theorem zcFreeGroupFoxBoundary_derivativeVector
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    zcFreeGroupFoxBoundary C ψ (zcFreeGroupFoxDerivativeVector C ψ w) =
      zcCompletedGroupAlgebraBoundary C ψ w

The boundary-map form of the completed Fox fundamental formula.

Show Lean proof

Theorem FoxDifferential.zcFreeGroupFoxBoundary_of_crossedHom

theorem zcFreeGroupFoxBoundary_of_crossedHom
    (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (w : FreeGroup X) :
    zcFreeGroupFoxBoundary C ψ (delta w) =
      zcCompletedGroupAlgebraBoundary C ψ w

Conditional completed Fox boundary formula. Any completed crossed differential on a free group with the standard basis values satisfies the completed Fox boundary formula.

Show Lean proof

Theorem FoxDifferential.zcFreeGroupFoxDerivative_fundamental_formula_of_crossedHom

theorem zcFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
    (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (w : FreeGroup X) :
    zcCompletedGroupAlgebraBoundary C ψ w =
      ∑ i : X,
        delta w i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)

Conditional completed Fox fundamental formula. The finite Fox-Euler sum computed from any completed crossed differential with standard basis values is \([\psi(w)]-1\).

Show Lean proof

Theorem FoxDifferential.zcFreeGroupFoxDerivative_euler_formula_of_crossedHom

theorem zcFreeGroupFoxDerivative_euler_formula_of_crossedHom
    (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (w : FreeGroup X) :
    zcGroupLike C H (ψ w) - 1 =
      ∑ i : X,
        delta w i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)

The explicit \([\psi(w)]-1\) form of the conditional completed Fox-Euler formula.

Show Lean proof

Theorem FoxDifferential.zcFreeGroupFoxDerivative_fundamental_formula

theorem zcFreeGroupFoxDerivative_fundamental_formula
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    zcCompletedGroupAlgebraBoundary C ψ w =
      ∑ i : X,
        zcFreeGroupFoxDerivative C ψ i w *
          (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)

The completed Fox fundamental formula, also known as the completed Fox-Euler formula: \([\psi(w)]-1 = \sum_i (\partial w/\partial x_i)([\psi(x_i)]-1)\).

Show Lean proof

Theorem FoxDifferential.zcFreeGroupFoxDerivative_euler_formula

theorem zcFreeGroupFoxDerivative_euler_formula
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    zcGroupLike C H (ψ w) - 1 =
      ∑ i : X,
        zcFreeGroupFoxDerivative C ψ i w *
          (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)

The explicit \([\psi(w)]-1\) form of the completed Fox-Euler formula.

Show Lean proof

ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Fundamental

Declarations