ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Fundamental

6 Theorems

The principal declarations in this module are:

residueFreeGroupFoxBoundary_derivativeVector Boundary-map form of the residue Fox fundamental formula. - residueFreeGroupFoxBoundary_of_crossedHom Any residue crossed homomorphism with the standard basis values satisfies the residue Fox boundary formula. - residueFreeGroupFoxDerivative_fundamental_formula_of_crossedHom The residue Fox-Euler sum computed from a crossed homomorphism with standard basis values is \([\psi(w)]-1\). - residueFreeGroupFoxDerivative_euler_formula_of_crossedHom The explicit \([\psi(w)]-1\) form of the residue Fox-Euler formula for a crossed homomorphism.

import

ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Boundary

Imported by

ProCGroups.FoxDifferential.Completed.Residue.FreeGroup

Theorem FoxDifferential.residueFreeGroupFoxBoundary_derivativeVector

theorem residueFreeGroupFoxBoundary_derivativeVector
    (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    residueFreeGroupFoxBoundary n ψ
        (residueFreeGroupFoxDerivativeVector n ψ w) =
      residueGroupRingBoundary n ψ w

Boundary-map form of the residue Fox fundamental formula.

Show Lean proof

Theorem FoxDifferential.residueFreeGroupFoxBoundary_of_crossedHom

theorem residueFreeGroupFoxBoundary_of_crossedHom
    (n : ℕ) (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (residueGroupRingScalar n ψ)
      (ResidueFreeFoxCoordinates n H X))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : ResidueGroupRing n H))
    (w : FreeGroup X) :
    residueFreeGroupFoxBoundary n ψ (delta w) =
      residueGroupRingBoundary n ψ w

Any residue crossed homomorphism with the standard basis values satisfies the residue Fox boundary formula.

Show Lean proof

Theorem FoxDifferential.residueFreeGroupFoxDerivative_fundamental_formula_of_crossedHom

theorem residueFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
    (n : ℕ) (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (residueGroupRingScalar n ψ)
      (ResidueFreeFoxCoordinates n H X))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : ResidueGroupRing n H))
    (w : FreeGroup X) :
    residueGroupRingBoundary n ψ w =
      ∑ i : X,
        delta w i *
          (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)

The residue Fox-Euler sum computed from a crossed homomorphism with standard basis values is \([\psi(w)]-1\).

Show Lean proof

Theorem FoxDifferential.residueFreeGroupFoxDerivative_euler_formula_of_crossedHom

theorem residueFreeGroupFoxDerivative_euler_formula_of_crossedHom
    (n : ℕ) (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (residueGroupRingScalar n ψ)
      (ResidueFreeFoxCoordinates n H X))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : ResidueGroupRing n H))
    (w : FreeGroup X) :
    (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ w) : ResidueGroupRing n H) - 1 =
      ∑ i : X,
        delta w i *
          (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)

The explicit \([\psi(w)]-1\) form of the residue Fox-Euler formula for a crossed homomorphism.

Show Lean proof

Theorem FoxDifferential.residueFreeGroupFoxDerivative_fundamental_formula

theorem residueFreeGroupFoxDerivative_fundamental_formula
    (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    residueGroupRingBoundary n ψ w =
      ∑ i : X,
        residueFreeGroupFoxDerivative n ψ i w *
          (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)

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

Show Lean proof

Theorem FoxDifferential.residueFreeGroupFoxDerivative_euler_formula

theorem residueFreeGroupFoxDerivative_euler_formula
    (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ w) : ResidueGroupRing n H) - 1 =
      ∑ i : X,
        residueFreeGroupFoxDerivative n ψ i w *
          (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)

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

Show Lean proof

ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Fundamental

Declarations