NYLL
Module

Fundamental.lean

Nyll.ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Fundamental
6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — \(\mathbb{Z}_C\) coefficients — free group — fundamental

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.

Imports1
Imported by3

Declarations

theorem

zcFreeGroupFoxBoundary_derivativeVector

L44 ↗
FoxDifferential.zcFreeGroupFoxBoundary_derivativeVector
Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]
Lean source · statement
theorem zcFreeGroupFoxBoundary_derivativeVector
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    zcFreeGroupFoxBoundary C ψ (zcFreeGroupFoxDerivativeVector C ψ w) =
      zcCompletedGroupAlgebraBoundary C ψ w
theorem

zcFreeGroupFoxBoundary_of_crossedHom

L91 ↗
FoxDifferential.zcFreeGroupFoxBoundary_of_crossedHom
Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]
Lean source · statement
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
theorem

zcFreeGroupFoxDerivative_fundamental_formula_of_crossedHom

L111 ↗
FoxDifferential.zcFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]
Lean source · statement
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)
theorem

zcFreeGroupFoxDerivative_euler_formula_of_crossedHom

L126 ↗
FoxDifferential.zcFreeGroupFoxDerivative_euler_formula_of_crossedHom
Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]
Lean source · statement
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)
theorem

zcFreeGroupFoxDerivative_fundamental_formula

L146 ↗
FoxDifferential.zcFreeGroupFoxDerivative_fundamental_formula
Documentation

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)\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]
Lean source · statement
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)
theorem

zcFreeGroupFoxDerivative_euler_formula

L156 ↗
FoxDifferential.zcFreeGroupFoxDerivative_euler_formula
Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section FiniteBasis
variable [Fintype X]
Lean source · statement
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)

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