NYLL
Module

FreeExpansion.lean

Nyll.ProCGroups.FoxDifferential.Discrete.FreeExpansion
7 declarations indexed from sourceView source ↗

Module documentation

Fox differential: discrete — free expansion

The principal declarations in this module are:

  • freeCrossedDifferentialExpansion

Prescribed values on the free generators determine the Fox-coordinate expansion.

  • freeCrossedDifferentialExpansionHom

The Fox-coordinate expansion is a crossed differential.

  • freeCrossedDifferentialExpansion_one

The Fox-coordinate expansion of the identity word is zero.

  • freeCrossedDifferentialExpansion_of

The Fox-coordinate expansion of a free generator returns its prescribed basis value.

Imports1
Imported by2

Declarations

def

freeCrossedDifferentialExpansion

L40 ↗
FoxDifferential.FoxCalculus.freeCrossedDifferentialExpansion
Documentation

Prescribed values on the free generators determine the Fox-coordinate expansion.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w
variable {H : Type v} [Group H]
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]
variable {X : Type u} [DecidableEq X] [Fintype X]
variable (ψ : FreeGroup X →* H) (basisValue : X → A)
Lean source · statement
def freeCrossedDifferentialExpansion (w : FreeGroup X) : A
theorem

freeCrossedDifferentialExpansion_one

L46 ↗
FoxDifferential.FoxCalculus.freeCrossedDifferentialExpansion_one
Documentation

The Fox-coordinate expansion of the identity word is zero.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w
variable {H : Type v} [Group H]
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]
variable {X : Type u} [DecidableEq X] [Fintype X]
variable (ψ : FreeGroup X →* H) (basisValue : X → A)
Lean source · statement
theorem freeCrossedDifferentialExpansion_one :
    freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue 1 = 0
theorem

freeCrossedDifferentialExpansion_of

L54 ↗
FoxDifferential.FoxCalculus.freeCrossedDifferentialExpansion_of
Documentation

The Fox-coordinate expansion of a free generator returns its prescribed basis value.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w
variable {H : Type v} [Group H]
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]
variable {X : Type u} [DecidableEq X] [Fintype X]
variable (ψ : FreeGroup X →* H) (basisValue : X → A)
Lean source · statement
theorem freeCrossedDifferentialExpansion_of (x : X) :
    freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue (FreeGroup.of x) =
      basisValue x
def

freeCrossedDifferentialExpansionHom

L66 ↗
FoxDifferential.FoxCalculus.freeCrossedDifferentialExpansionHom
Documentation

The Fox-coordinate expansion is a crossed differential.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w
variable {H : Type v} [Group H]
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]
variable {X : Type u} [DecidableEq X] [Fintype X]
variable (ψ : FreeGroup X →* H) (basisValue : X → A)
Lean source · full declaration
def freeCrossedDifferentialExpansionHom : DifferentialHom ψ A where
  toFun := freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue
  map_mul' := by
    intro u v
    simp only [scalarCrossedAction_apply, freeCrossedDifferentialExpansion]
    change
      (∑ x : X,
          relativeFreeGroupFoxDerivative (H := H) X ψ (u * v) x • basisValue x) =
        (∑ x : X,
          relativeFreeGroupFoxDerivative (H := H) X ψ u x • basisValue x) +
          (MonoidAlgebra.of ℤ H (ψ u) : GroupRing H) •
            (∑ x : X,
              relativeFreeGroupFoxDerivative (H := H) X ψ v x • basisValue x)
    rw [relativeFreeGroupFoxDerivative_mul]
    simp only [MonoidAlgebra.of_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul,
      add_smul, Finset.sum_add_distrib, Finset.smul_sum, smul_smul]
theorem

freeCrossedDifferentialWithCoeff_groupRingScalar_eq_expansion

L87 ↗
FoxDifferential.FoxCalculus.freeCrossedDifferentialWithCoeff_groupRingScalar_eq_expansion
Documentation

The coefficient-generic free crossed differential over a group ring is the Fox-coordinate expansion of its generator values.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w
variable {H : Type v} [Group H]
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]
variable {X : Type u} [DecidableEq X] [Fintype X]
variable (ψ : FreeGroup X →* H) (basisValue : X → A)
Lean source · statement
theorem freeCrossedDifferentialWithCoeff_groupRingScalar_eq_expansion (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeff (A := A) (groupRingScalar ψ) basisValue w =
      freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue w
theorem

freeCrossedDifferentialWithCoeffCoordinates_eq_relativeFreeGroupFoxDerivative

L101 ↗
FoxDifferential.FoxCalculus.freeCrossedDifferentialWithCoeffCoordinates_eq_relativeFreeGroupFoxDerivative
Documentation

The coefficient-generic coordinate crossed differential specializes to the usual relative Fox derivative over a group ring.

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 w
variable {H : Type v} [Group H]
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]
variable {X : Type u} [DecidableEq X] [Fintype X]
variable (ψ : FreeGroup X →* H) (basisValue : X → A)
omit [Fintype X] in
Lean source · statement
theorem freeCrossedDifferentialWithCoeffCoordinates_eq_relativeFreeGroupFoxDerivative
    (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeffCoordinates
        (X := X) (groupRingScalar ψ) w =
      relativeFreeGroupFoxDerivative (H := H) X ψ w
theorem

crossedHom_comp_relativeFreeGroupFoxDerivative

L116 ↗
FoxDifferential.FoxCalculus.crossedHom_comp_relativeFreeGroupFoxDerivative
Documentation

Abstract Fox chain rule for an arbitrary crossed differential.

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 w
variable {H : Type v} [Group H]
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]
variable {X : Type u} [DecidableEq X] [Fintype X]
variable (ψ : FreeGroup X →* H) (basisValue : X → A)
variable {Y : Type w}
Lean source · statement
theorem crossedHom_comp_relativeFreeGroupFoxDerivative
    (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
    (delta : DifferentialHom ψ A) (w : FreeGroup X) :
    delta (φ w) =
      ∑ x : X,
        relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x •
          delta (φ (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.