Module

SourceDerivativeVector.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.SourceDerivativeVector

9 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — source derivative vector

The principal declarations in this module are:

foxAlgebraicStageSourceDerivativeVector

Source-valued derivative vector of a source quotient element.

foxAlgebraicStageSourceGroupAlgebraDerivativeVector

Source-valued derivative vector of an arbitrary source group-algebra element.

foxAlgebraicStageSourceDerivativeVector_apply

The finite-stage source derivative vector evaluates the source word at the chosen coordinate.

foxAlgebraicStageSourceGroupAlgebraDerivativeVector_apply

The finite-stage source group-algebra derivative vector is evaluated coordinatewise in the source finite quotient.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.SourceBoundary

Imported by2

def

foxAlgebraicStageSourceDerivativeVector

L38 ↗

FoxDifferential.foxAlgebraicStageSourceDerivativeVector

Documentation

Source-valued derivative vector of a source quotient element.

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

def foxAlgebraicStageSourceDerivativeVector
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageSourceCoordinateVector (X := X) N n

theorem

foxAlgebraicStageSourceDerivativeVector_apply

L49 ↗

FoxDifferential.foxAlgebraicStageSourceDerivativeVector_apply

Documentation

The finite-stage source derivative vector evaluates the source word at the chosen coordinate.

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 [N.Normal] in

Lean source · statement

theorem foxAlgebraicStageSourceDerivativeVector_apply
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
    (i : X) :
    foxAlgebraicStageSourceDerivativeVector (X := X) N n q i =
      foxAlgebraicStageSourceGroupAlgebraDerivative (X := X) N n i
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q)

def

foxAlgebraicStageSourceGroupAlgebraDerivativeVector

L59 ↗

FoxDifferential.foxAlgebraicStageSourceGroupAlgebraDerivativeVector

Documentation

Source-valued derivative vector of an arbitrary source group-algebra element.

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 foxAlgebraicStageSourceGroupAlgebraDerivativeVector :
    foxAlgebraicStageSourceGroupAlgebra (X := X) N n →ₗ[ModNCompletedCoeff n]
      foxAlgebraicStageSourceCoordinateVector (X := X) N n where
  toFun x := fun i => foxAlgebraicStageSourceGroupAlgebraDerivative (X := X) N n i x
  map_add' := by
    intro x y
    funext i
    simp only [map_add, Pi.add_apply]
  map_smul' := by
    intro a x
    funext i
    simp only [map_smul, RingHom.id_apply, Pi.smul_apply]

theorem

foxAlgebraicStageSourceGroupAlgebraDerivativeVector_apply

L78 ↗

FoxDifferential.foxAlgebraicStageSourceGroupAlgebraDerivativeVector_apply

Documentation

The finite-stage source group-algebra derivative vector is evaluated coordinatewise in the source finite quotient.

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 [N.Normal] in

Lean source · statement

theorem foxAlgebraicStageSourceGroupAlgebraDerivativeVector_apply
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) (i : X) :
    foxAlgebraicStageSourceGroupAlgebraDerivativeVector (X := X) N n x i =
      foxAlgebraicStageSourceGroupAlgebraDerivative (X := X) N n i x

theorem

foxAlgebraicStageSourceFoxBoundary_sourceDerivativeVector

L86 ↗

FoxDifferential.foxAlgebraicStageSourceFoxBoundary_sourceDerivativeVector

Documentation

The source boundary of the source-valued derivative of a source quotient element is \(q-1\).

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 [N.Normal] in

Lean source · statement

theorem foxAlgebraicStageSourceFoxBoundary_sourceDerivativeVector
    [Fintype X]
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageSourceFoxBoundary (X := X) N n
        (foxAlgebraicStageSourceDerivativeVector (X := X) N n q) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q - 1

theorem

foxAlgebraicStageSourceFoxBoundary_sourceGroupAlgebraDerivativeVector

L102 ↗

FoxDifferential.foxAlgebraicStageSourceFoxBoundary_sourceGroupAlgebraDerivativeVector

Documentation

The source boundary of the source-valued derivative of a group-algebra element is the usual source augmentation formula.

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 [N.Normal] in

Lean source · statement

theorem foxAlgebraicStageSourceFoxBoundary_sourceGroupAlgebraDerivativeVector
    [Fintype X]
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
    foxAlgebraicStageSourceFoxBoundary (X := X) N n
        (foxAlgebraicStageSourceGroupAlgebraDerivativeVector (X := X) N n x) =
      x -
        algebraMap (ModNCompletedCoeff n)
          (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)
          (foxCommutatorPowerSourceGroupAlgebraAugmentation
            (F := FreeGroup X) N n x)

theorem

foxAlgebraicStageCoordinateSourceToTarget_smul_source

L118 ↗

FoxDifferential.foxAlgebraicStageCoordinateSourceToTarget_smul_source

Documentation

The source-to-target coordinate map commutes with source scalar multiplication.

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 foxAlgebraicStageCoordinateSourceToTarget_smul_source
    (a : foxAlgebraicStageSourceGroupAlgebra (X := X) N n)
    (v : foxAlgebraicStageSourceCoordinateVector (X := X) N n) :
    foxAlgebraicStageCoordinateSourceToTarget (X := X) N n (a • v) =
      foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n a •
        foxAlgebraicStageCoordinateSourceToTarget (X := X) N n v

theorem

foxAlgebraicStageCoordinateSourceToTarget_sourceDerivativeVector

L137 ↗

FoxDifferential.foxAlgebraicStageCoordinateSourceToTarget_sourceDerivativeVector

Documentation

Applying source-to-target coordinates to a source derivative vector gives the target-valued finite derivative 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 foxAlgebraicStageCoordinateSourceToTarget_sourceDerivativeVector
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageCoordinateSourceToTarget (X := X) N n
        (foxAlgebraicStageSourceDerivativeVector (X := X) N n q) =
      foxAlgebraicStageQuotientDerivativeVector (X := X) N n q

theorem

foxAlgebraicStageCoordinateSourceToTarget_sourceGroupAlgebraDerivativeVector

L153 ↗

FoxDifferential.foxAlgebraicStageCoordinateSourceToTarget_sourceGroupAlgebraDerivativeVector

Documentation

Applying source-to-target coordinates to the group-algebra source derivative vector gives the coordinatewise target group-algebra derivative.

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

theorem foxAlgebraicStageCoordinateSourceToTarget_sourceGroupAlgebraDerivativeVector
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
    foxAlgebraicStageCoordinateSourceToTarget (X := X) N n
        (foxAlgebraicStageSourceGroupAlgebraDerivativeVector (X := X) N n x) =
      fun i => foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i x := by
  funext i
  rw [foxAlgebraicStageCoordinateSourceToTarget_apply,
    foxAlgebraicStageSourceGroupAlgebraDerivativeVector_apply]
  exact foxAlgebraicStageSourceGroupAlgebraDerivative_map
    (X := X) (N := N) (n := n) i x

Module documentation

Fox differential: completed — finite stage — source derivative vector

Declarations