Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.Continuous.Free.CanonicalFormula
ProCGroups/FoxDifferential/Completed/Continuous/Free/CanonicalFormula

ProCGroups.FoxDifferential.Completed.Continuous.Free.CanonicalFormula

3 Theorems

The principal declarations in this module are:

  • freeProCZCCompletedFoxDerivativeVector_boundary Boundary-map form of the source-shaped completed Fox formula for the canonical free pro-\(C\) semidirect lift. - freeProCZCCompletedFoxDerivative_fundamental_formula Source-shaped completed Fox fundamental formula for the canonical free pro-\(C\) semidirect lift. - freeProCZCCompletedFoxDerivative_euler_formula Explicit \([\rho g] - 1\) form of the source-shaped completed Fox-Euler formula for the canonical free pro-\(C\) semidirect lift.
import
Imported by

Declarations

Theorem FoxDifferential.freeProCZCCompletedFoxDerivativeVector_boundary 
theorem freeProCZCCompletedFoxDerivativeVector_boundary
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetUnit :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C PUnit H))
    (φ : X → H) (g : F) :
    freeProCZCCompletedFoxBoundary C φ
        (freeProCZCCompletedFoxDerivativeVector
          (C := C) hι htarget φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g) =
      zcCompletedGroupAlgebraBoundary C
        (freeProCZCCompletedFoxRightHom
          (C := C) hι htarget φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)) g

Boundary-map form of the source-shaped completed Fox formula for the canonical free pro-\(C\) semidirect lift.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxDerivative_fundamental_formula 
theorem freeProCZCCompletedFoxDerivative_fundamental_formula
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetUnit :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C PUnit H))
    (φ : X → H) (g : F) :
    zcCompletedGroupAlgebraBoundary C
        (freeProCZCCompletedFoxRightHom
          (C := C) hι htarget φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)) g =
      ∑ x : X,
        freeProCZCCompletedFoxDerivativeVector
            (C := C) hι htarget φ
            (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g x *
          (zcGroupLike C H (φ x) - 1)

Source-shaped completed Fox fundamental formula for the canonical free pro-\(C\) semidirect lift.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxDerivative_euler_formula 
theorem freeProCZCCompletedFoxDerivative_euler_formula
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htarget :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetUnit :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C PUnit H))
    (φ : X → H) (g : F) :
    zcGroupLike C H
        (freeProCZCCompletedFoxRightHom
          (C := C) hι htarget φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g) - 1 =
      ∑ x : X,
        freeProCZCCompletedFoxDerivativeVector
            (C := C) hι htarget φ
            (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g x *
          (zcGroupLike C H (φ x) - 1)

Explicit \([\rho g] - 1\) form of the source-shaped completed Fox-Euler formula for the canonical free pro-\(C\) semidirect lift.

Show Lean proof