NYLL
Module

Boundary.lean

Nyll.ProCGroups.FoxDifferential.Discrete.FoxCalculus.Boundary
10 declarations indexed from sourceView source ↗

Module documentation

Fox differential: discrete — fox calculus — boundary

The principal declarations in this module are:

  • relativeFreeGroupFoxBoundary

The pushed-forward Fox boundary \(a \mapsto \sum_x a_x (\psi(x) - 1)\).

  • relativeFreeGroupFoxBoundary_apply

The relative free-group Fox boundary is evaluated on canonical generators and then extended linearly to the coordinate module.

  • relativeFreeGroupFoxBoundary_single

The relative Fox boundary sends a coordinate basis vector to the corresponding augmentation generator.

  • toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap

Composing the universal boundary with the coordinate-to-differential map gives the pushed-forward Fox boundary.

Imports3
Imported by5

Declarations

def

relativeFreeGroupFoxBoundary

L49 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary
Documentation

The pushed-forward Fox boundary \(a \mapsto \sum_x a_x (\psi(x) - 1)\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
Lean source · statement
def relativeFreeGroupFoxBoundary :
    RelativeFreeFoxCoordinates (H := H) X →ₗ[GroupRing H] GroupRing H
theorem

relativeFreeGroupFoxBoundary_apply

L67 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_apply
Documentation

The relative free-group Fox boundary is evaluated on canonical generators and then extended linearly to the coordinate module.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
omit [DecidableEq X] in
Lean source · statement
theorem relativeFreeGroupFoxBoundary_apply
    (a : RelativeFreeFoxCoordinates (H := H) X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ a =
      ∑ x : X, a x * augmentationGenerator H (ψ (FreeGroup.of x))
theorem

relativeFreeGroupFoxBoundary_single

L78 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_single
Documentation

The relative Fox boundary sends a coordinate basis vector to the corresponding augmentation generator.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
Lean source · statement
theorem relativeFreeGroupFoxBoundary_single (x : X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ
        (Pi.single x (1 : GroupRing H)) =
      augmentationGenerator H (ψ (FreeGroup.of x))
theorem

toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap

L96 ↗
FoxDifferential.FoxCalculus.toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap
Documentation

Composing the universal boundary with the coordinate-to-differential map gives the pushed-forward Fox boundary.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
omit [DecidableEq X] in
Lean source · statement
theorem toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap :
    (toGroupRing ψ).comp
        (relativeFreeFoxCoordinatesLinearMap (H := H) X ψ) =
      relativeFreeGroupFoxBoundary (H := H) X ψ
theorem

relativeFreeGroupFoxDerivative_fundamental_formula

L116 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_fundamental_formula
Documentation

Relative Fox fundamental formula, also known as the Fox--Euler formula: \(\psi(w) - 1 = \sum_x (\partial w/\partial x) (\psi(x) - 1)\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
Lean source · statement
theorem relativeFreeGroupFoxDerivative_fundamental_formula (w : FreeGroup X) :
    groupRingBoundary ψ w =
      ∑ x : X,
        relativeFreeGroupFoxDerivative (H := H) X ψ w x *
          augmentationGenerator H (ψ (FreeGroup.of x))
theorem

relativeFreeGroupFoxBoundary_derivative

L130 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_derivative
Documentation

Fox boundary form of the relative Fox fundamental formula.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
Lean source · statement
theorem relativeFreeGroupFoxBoundary_derivative (w : FreeGroup X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ
        (relativeFreeGroupFoxDerivative (H := H) X ψ w) =
      groupRingBoundary ψ w
theorem

relativeFreeGroupFoxBoundary_of_crossedHom

L141 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary_of_crossedHom
Documentation

Conditional relative Fox boundary formula. Any differential map on a free group with the standard coordinate values satisfies the relative Fox boundary formula.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
Lean source · statement
theorem relativeFreeGroupFoxBoundary_of_crossedHom
    (delta : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing H))
    (w : FreeGroup X) :
    relativeFreeGroupFoxBoundary (H := H) X ψ (delta w) = groupRingBoundary ψ w
theorem

relativeFreeGroupFoxDerivative_fundamental_formula_of_crossedHom

L156 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
Documentation

Conditional relative Fox fundamental formula. The Fox-Euler sum computed from any differential map with standard coordinate values is \([\psi(w)]-1\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
Lean source · statement
theorem relativeFreeGroupFoxDerivative_fundamental_formula_of_crossedHom
    (delta : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing H))
    (w : FreeGroup X) :
    groupRingBoundary ψ w =
      ∑ x : X, delta w x * augmentationGenerator H (ψ (FreeGroup.of x))
theorem

relativeFreeGroupFoxDerivative_euler_formula_of_crossedHom

L167 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_euler_formula_of_crossedHom
Documentation

Explicit \(\psi(w)-1\) version of the conditional relative Fox-Euler formula.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
Lean source · statement
theorem relativeFreeGroupFoxDerivative_euler_formula_of_crossedHom
    (delta : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing H))
    (w : FreeGroup X) :
    (MonoidAlgebra.of ℤ H (ψ w) : GroupRing H) - 1 =
      ∑ x : X, delta w x * augmentationGenerator H (ψ (FreeGroup.of x))
theorem

relativeFreeGroupFoxDerivative_euler_formula

L179 ↗
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_euler_formula
Documentation

Explicit \(\psi(w)-1\) version of the relative Fox--Euler formula.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v
variable {H : Type v} [Group H]
variable (X : Type u)
variable [DecidableEq X]
variable (ψ : FreeGroup X →* H)
variable [Fintype X]
Lean source · statement
theorem relativeFreeGroupFoxDerivative_euler_formula (w : FreeGroup X) :
    (MonoidAlgebra.of ℤ H (ψ w) : GroupRing H) - 1 =
      ∑ x : X,
        relativeFreeGroupFoxDerivative (H := H) X ψ w x *
          augmentationGenerator H (ψ (FreeGroup.of x))

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