NYLL
Module

CanonicalFormula.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Free.CanonicalFormula
3 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — free — canonical formula

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.

Imports1
Imported by2

Declarations

theorem

freeProCZCCompletedFoxDerivativeVector_boundary

L59 ↗
FoxDifferential.freeProCZCCompletedFoxDerivativeVector_boundary
Documentation

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

Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
variable [DiscreteTopology X]
section CanonicalSourceFormula
variable [Fintype X]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
variable [T2Space (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
Lean source · statement
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
theorem

freeProCZCCompletedFoxDerivative_fundamental_formula

L96 ↗
FoxDifferential.freeProCZCCompletedFoxDerivative_fundamental_formula
Documentation

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

Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
variable [DiscreteTopology X]
section CanonicalSourceFormula
variable [Fintype X]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
variable [T2Space (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
Lean source · statement
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)
theorem

freeProCZCCompletedFoxDerivative_euler_formula

L121 ↗
FoxDifferential.freeProCZCCompletedFoxDerivative_euler_formula
Documentation

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

Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {F : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [TopologicalSpace X]
variable [DiscreteTopology X]
section CanonicalSourceFormula
variable [Fintype X]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
variable [T2Space (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C PUnit.{u + 1} H)]
Lean source · statement
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)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.