NYLL
Module

Rules.lean

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

Module documentation

Fox differential: finite stage — stage — derivative — rules

The principal declarations in this module are:

  • foxAlgebraicStageDerivativeVectorCrossedHom

The finite-stage Fox derivative vector, bundled with its scalar Fox--Leibniz law.

  • foxAlgebraicStageDerivative_one

The finite-stage derivative sends the identity word to zero componentwise.

  • foxAlgebraicStageDerivativeVector_of

The finite-stage derivative vector sends a free generator to the corresponding coordinate basis vector.

  • foxAlgebraicStageDerivative_mul

The finite-stage Fox product rule holds componentwise.

Imports2
Imported by5

Declarations

def

foxAlgebraicStageDerivativeVectorCrossedHom

L39 ↗
FoxDifferential.foxAlgebraicStageDerivativeVectorCrossedHom
Documentation

The finite-stage Fox derivative vector, bundled with its scalar Fox--Leibniz law.

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 foxAlgebraicStageDerivativeVectorCrossedHom :
    ScalarCrossedHom
      (foxAlgebraicStageCoefficient (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n) where
  toFun w := (foxAlgebraicStageLift (X := X) N n w).left
  map_mul' := by
    intro u v
    simp only [scalarCrossedAction_apply, map_mul,
      FoxAlgebraicStageSemidirect.mul_left, foxAlgebraicStageLift_right,
      foxAlgebraicStageCoefficient_apply, QuotientGroup.mk'_apply,
      MonoidAlgebra.of_apply]
theorem

foxAlgebraicStageDerivative_one

L53 ↗
FoxDifferential.foxAlgebraicStageDerivative_one
Documentation

The finite-stage derivative sends the identity word to zero componentwise.

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_one (i : X) :
    foxAlgebraicStageDerivative (X := X) N n i (1 : FreeGroup X) = 0
theorem

foxAlgebraicStageDerivativeVector_of

L64 ↗
FoxDifferential.foxAlgebraicStageDerivativeVector_of
Documentation

The finite-stage derivative vector sends a free generator to the corresponding coordinate basis vector.

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 foxAlgebraicStageDerivativeVector_of (x : X) :
    foxAlgebraicStageDerivativeVector (X := X) N n (FreeGroup.of x) =
      Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
theorem

foxAlgebraicStageDerivative_mul

L71 ↗
FoxDifferential.foxAlgebraicStageDerivative_mul
Documentation

The finite-stage Fox product rule holds componentwise.

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_mul (i : X) (u v : FreeGroup X) :
    foxAlgebraicStageDerivative (X := X) N n i (u * v) =
      foxAlgebraicStageDerivative (X := X) N n i u +
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) (QuotientGroup.mk' N u)) *
          foxAlgebraicStageDerivative (X := X) N n i v
theorem

foxAlgebraicStageDerivativeVector_unique

L91 ↗
FoxDifferential.foxAlgebraicStageDerivativeVector_unique
Documentation

The bundled finite-stage Fox derivative vector is uniquely determined by its values on free generators.

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 foxAlgebraicStageDerivativeVector_unique
    (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)) :
    delta = foxAlgebraicStageDerivativeVectorCrossedHom (X := X) N n
theorem

foxAlgebraicStageDerivativeVector_eq_residueFreeGroupFoxDerivativeVector

L122 ↗
FoxDifferential.foxAlgebraicStageDerivativeVector_eq_residueFreeGroupFoxDerivativeVector
Documentation

The finite-stage derivative is exactly the residue free Fox derivative for the quotient map \(\mathrm{FreeGroup}(X) \to F/N\).

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 foxAlgebraicStageDerivativeVector_eq_residueFreeGroupFoxDerivativeVector :
    foxAlgebraicStageDerivativeVector (X := X) N n =
      residueFreeGroupFoxDerivativeVector n (QuotientGroup.mk' N)
theorem

foxAlgebraicStageDerivativeVector_eq_zero_iff_residueUniversalDifferential_eq_zero

L138 ↗
FoxDifferential.foxAlgebraicStageDerivativeVector_eq_zero_iff_residueUniversalDifferential_eq_zero
Documentation

For a finite free basis, finite-stage derivative-vector zero is the same as zero of the residue universal differential.

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 foxAlgebraicStageDerivativeVector_eq_zero_iff_residueUniversalDifferential_eq_zero
    [Finite X]
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ} {w : FreeGroup X} :
    foxAlgebraicStageDerivativeVector (X := X) N n w = 0 ↔
      residueUniversalDifferential n (QuotientGroup.mk' N) w = 0

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