Module

Derivative.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Fundamental.Derivative

6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: finite stage — stage — fundamental — derivative

The principal declarations in this module are:

foxAlgebraicStageGroupAlgebraDerivative

Linear extension of a descended finite-stage Fox derivative coordinate to the source group algebra.

foxAlgebraicStageGroupAlgebraDerivative_of_quotient

Evaluation of the finite-stage group-algebra derivative on a quotient basis element.

foxAlgebraicStageGroupAlgebraDerivative_of

Evaluation of the finite-stage group-algebra derivative on a represented word.

foxAlgebraicStageGroupAlgebraDerivative_one

The finite-stage group-algebra derivative sends the unit to zero.

Imports4

Imported by2

def

foxAlgebraicStageGroupAlgebraDerivative

L49 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivative

Documentation

Linear extension of a descended finite-stage Fox derivative coordinate to the source group algebra.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageGroupAlgebraDerivative (i : X) :
    MonoidAlgebra (ModNCompletedCoeff n)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) →ₗ[
      ModNCompletedCoeff n]
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n

theorem

foxAlgebraicStageGroupAlgebraDerivative_of_quotient

L60 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivative_of_quotient

Documentation

Evaluation of the finite-stage group-algebra derivative on a quotient basis element.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageGroupAlgebraDerivative_of_quotient
    (i : X)
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q) =
      foxAlgebraicStageQuotientDerivative (X := X) N n i q

theorem

foxAlgebraicStageGroupAlgebraDerivative_of

L76 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivative_of

Documentation

Evaluation of the finite-stage group-algebra derivative on a represented word.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageGroupAlgebraDerivative_of
    (i : X) (w : FreeGroup X) :
    foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
          (QuotientGroup.mk'
            (foxCommutatorPowerSubgroup (F := FreeGroup X) N n) w)) =
      foxAlgebraicStageDerivative (X := X) N n i w

theorem

foxAlgebraicStageGroupAlgebraDerivative_one

L89 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivative_one

Documentation

The finite-stage group-algebra derivative sends the unit to zero.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageGroupAlgebraDerivative_one (i : X) :
    foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i
        (1 : MonoidAlgebra (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)) = 0

theorem

foxAlgebraicStageGroupAlgebraDerivative_of_quotient_mul

L102 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivative_of_quotient_mul

Documentation

Product rule for the finite-stage group-algebra derivative on quotient basis elements.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageGroupAlgebraDerivative_of_quotient_mul
    (i : X)
    (q r : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
          (q * r)) =
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q) +
        foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) q) *
          foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i
            (MonoidAlgebra.of (ModNCompletedCoeff n)
              (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) r)

theorem

foxAlgebraicStageGroupAlgebraDerivative_mul

L140 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivative_mul

Documentation

Product rule for the finite-stage group-algebra derivative on arbitrary source group-algebra elements.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageGroupAlgebraDerivative_mul
    (i : X)
    (x y : MonoidAlgebra (ModNCompletedCoeff n)
      (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)) :
    foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i (x * y) =
      foxCommutatorPowerSourceGroupAlgebraAugmentation
          (F := FreeGroup X) N n y •
        foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i x +
      foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x *
        foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i y

Module documentation

Fox differential: finite stage — stage — fundamental — derivative

Declarations

foxAlgebraicStageGroupAlgebraDerivative

foxAlgebraicStageGroupAlgebraDerivative_of_quotient

foxAlgebraicStageGroupAlgebraDerivative_of

foxAlgebraicStageGroupAlgebraDerivative_one

foxAlgebraicStageGroupAlgebraDerivative_of_quotient_mul

foxAlgebraicStageGroupAlgebraDerivative_mul