NYLL
Module

Boundary.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Derivative.Boundary
7 declarations indexed from sourceView source ↗

Module documentation

Fox differential: finite stage — stage — derivative — boundary

The principal declarations in this module are:

  • foxAlgebraicStageFoxBoundary

The finite-stage Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([x_i] - 1)\) on coordinate vectors.

  • foxAlgebraicStageFoxBoundary_apply

The finite-stage Fox boundary is evaluated on the canonical generators and then extended linearly to the finite-stage coordinate module.

  • foxAlgebraicStageFoxBoundary_single

The finite-stage Fox boundary sends a coordinate basis vector to its augmentation generator.

  • foxAlgebraicStageDerivative_fundamental_formula

Finite-stage Fox fundamental formula for a free-group word.

Imports3
Imported by3

Declarations

def

foxAlgebraicStageFoxBoundary

L44 ↗
FoxDifferential.foxAlgebraicStageFoxBoundary
Documentation

The finite-stage Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([x_i] - 1)\) on coordinate vectors.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
Lean source · full declaration
def foxAlgebraicStageFoxBoundary [Fintype X] :
    foxAlgebraicStageCoordinateVector (X := X) N n →ₗ[
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n]
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n where
  toFun v :=
    ∑ i : X,
      v i *
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N)
          (QuotientGroup.mk' N (FreeGroup.of i)) - 1)
  map_add' := by
    intro v w
    simp only [Pi.add_apply, QuotientGroup.mk'_apply, MonoidAlgebra.of_apply, add_mul,
        Finset.sum_add_distrib]
  map_smul' := by
    intro r v
    simp only [Pi.smul_apply, smul_eq_mul, QuotientGroup.mk'_apply, MonoidAlgebra.of_apply,
        mul_assoc,
  RingHom.id_apply, Finset.mul_sum]
theorem

foxAlgebraicStageFoxBoundary_apply

L69 ↗
FoxDifferential.foxAlgebraicStageFoxBoundary_apply
Documentation

The finite-stage Fox boundary is evaluated on the canonical generators and then extended linearly to the finite-stage coordinate module.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in
Lean source · statement
theorem foxAlgebraicStageFoxBoundary_apply [Fintype X]
    (v : foxAlgebraicStageCoordinateVector (X := X) N n) :
    foxAlgebraicStageFoxBoundary (X := X) N n v =
      ∑ i : X,
        v i *
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N)
            (QuotientGroup.mk' N (FreeGroup.of i)) - 1)
theorem

foxAlgebraicStageFoxBoundary_single

L81 ↗
FoxDifferential.foxAlgebraicStageFoxBoundary_single
Documentation

The finite-stage Fox boundary sends a coordinate basis vector to its augmentation generator.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
Lean source · statement
theorem foxAlgebraicStageFoxBoundary_single [Fintype X] (i : X) :
    foxAlgebraicStageFoxBoundary (X := X) N n
        (Pi.single i (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n)) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N)
        (QuotientGroup.mk' N (FreeGroup.of i)) - 1
theorem

foxAlgebraicStageDerivative_fundamental_formula

L96 ↗
FoxDifferential.foxAlgebraicStageDerivative_fundamental_formula
Documentation

Finite-stage Fox fundamental formula for a free-group word.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
Lean source · statement
theorem foxAlgebraicStageDerivative_fundamental_formula
    [Fintype X] (w : FreeGroup X) :
    MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) (QuotientGroup.mk' N w) - 1 =
      ∑ i : X,
        foxAlgebraicStageDerivative (X := X) N n i w *
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N)
            (QuotientGroup.mk' N (FreeGroup.of i)) - 1)
theorem

foxAlgebraicStageFoxBoundary_derivativeVector

L214 ↗
FoxDifferential.foxAlgebraicStageFoxBoundary_derivativeVector
Documentation

Boundary-map form of the finite-stage Fox fundamental formula.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
Lean source · statement
theorem foxAlgebraicStageFoxBoundary_derivativeVector [Fintype X] (w : FreeGroup X) :
    foxAlgebraicStageFoxBoundary (X := X) N n
        (foxAlgebraicStageDerivativeVector (X := X) N n w) =
      foxAlgebraicStageCoefficient (X := X) N n w - 1
theorem

foxAlgebraicStageFoxBoundary_of_crossedHom

L226 ↗
FoxDifferential.foxAlgebraicStageFoxBoundary_of_crossedHom
Documentation

Any scalar crossed homomorphism with the standard generator values satisfies the finite-stage Fox boundary formula.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
Lean source · statement
theorem foxAlgebraicStageFoxBoundary_of_crossedHom
    [Fintype X]
    (delta : ScalarCrossedHom
      (foxAlgebraicStageCoefficient (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n))
    (w : FreeGroup X) :
    foxAlgebraicStageFoxBoundary (X := X) N n (delta w) =
      foxAlgebraicStageCoefficient (X := X) N n w - 1
theorem

foxAlgebraicStageDerivative_fundamental_formula_of_crossedHom

L247 ↗
FoxDifferential.foxAlgebraicStageDerivative_fundamental_formula_of_crossedHom
Documentation

The Fox--Euler sum for any scalar crossed homomorphism with the standard generator values is \([w]-1\).

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
Lean source · statement
theorem foxAlgebraicStageDerivative_fundamental_formula_of_crossedHom
    [Fintype X]
    (delta : ScalarCrossedHom
      (foxAlgebraicStageCoefficient (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n))
    (hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n))
    (w : FreeGroup X) :
    foxAlgebraicStageCoefficient (X := X) N n w - 1 =
      ∑ i : X,
        delta w i *
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N)
            (QuotientGroup.mk' N (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.