NYLL
Module

Fundamental.lean

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

Module documentation

Fox differential: completed — residue — free group — fundamental

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.

Imports1
Imported by1

Declarations

theorem

residueFreeGroupFoxBoundary_derivativeVector

L42 ↗
FoxDifferential.residueFreeGroupFoxBoundary_derivativeVector
Documentation

Boundary-map form of the residue Fox fundamental formula.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]
Lean source · statement
theorem residueFreeGroupFoxBoundary_derivativeVector
    (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    residueFreeGroupFoxBoundary n ψ
        (residueFreeGroupFoxDerivativeVector n ψ w) =
      residueGroupRingBoundary n ψ w
theorem

residueFreeGroupFoxBoundary_of_crossedHom

L85 ↗
FoxDifferential.residueFreeGroupFoxBoundary_of_crossedHom
Documentation

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

Source context 7 commands

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

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

residueFreeGroupFoxDerivative_fundamental_formula_of_crossedHom

L105 ↗
FoxDifferential.residueFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
Documentation

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

Source context 7 commands

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

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

residueFreeGroupFoxDerivative_euler_formula_of_crossedHom

L123 ↗
FoxDifferential.residueFreeGroupFoxDerivative_euler_formula_of_crossedHom
Documentation

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

Source context 7 commands

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

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

residueFreeGroupFoxDerivative_fundamental_formula

L145 ↗
FoxDifferential.residueFreeGroupFoxDerivative_fundamental_formula
Documentation

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

Source context 7 commands

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

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

residueFreeGroupFoxDerivative_euler_formula

L155 ↗
FoxDifferential.residueFreeGroupFoxDerivative_euler_formula
Documentation

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

Source context 7 commands

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

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

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