Module

Universal.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Derivative.Quotient.Universal

3 declarations indexed from sourceView source ↗

Module documentation

Fox differential: stage — derivative — quotient — universal

The principal declarations in this module are:

foxAlgebraicStageQuotientDerivativeVectorLinearMap

The linear map from the quotient universal crossed-differential module representing the descended finite-stage Fox derivative vector.

foxAlgebraicStageQuotientDerivativeVectorLinearMap_universal

The quotient derivative-vector linear map evaluates on the universal differential as the descended finite-stage Fox derivative vector.

existsUnique_foxAlgebraicStageQuotientDerivativeVectorLinearMap

Existence and uniqueness of the linear map representing the descended finite-stage Fox derivative vector on the finite source quotient.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Derivative.Quotient.Basic

Imported by1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Derivative.Quotient.All

def

foxAlgebraicStageQuotientDerivativeVectorLinearMap

L41 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivativeVectorLinearMap

Documentation

The linear map from the quotient universal crossed-differential module representing the descended finite-stage Fox 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

def foxAlgebraicStageQuotientDerivativeVectorLinearMap :
    CrossedDifferentialModule (foxAlgebraicStageQuotientCoefficient (X := X) N n) →ₗ[
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n]
      foxAlgebraicStageCoordinateVector (X := X) N n

theorem

foxAlgebraicStageQuotientDerivativeVectorLinearMap_universal

L55 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivativeVectorLinearMap_universal

Documentation

The quotient derivative-vector linear map evaluates on the universal differential as the descended finite-stage Fox 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 foxAlgebraicStageQuotientDerivativeVectorLinearMap_universal
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageQuotientDerivativeVectorLinearMap (X := X) N n
        (universalCrossedDifferential (foxAlgebraicStageQuotientCoefficient (X := X) N n) q) =
      foxAlgebraicStageQuotientDerivativeVector (X := X) N n q

theorem

existsUnique_foxAlgebraicStageQuotientDerivativeVectorLinearMap

L69 ↗

FoxDifferential.existsUnique_foxAlgebraicStageQuotientDerivativeVectorLinearMap

Documentation

Existence and uniqueness of the linear map representing the descended finite-stage Fox derivative vector on the finite source quotient.

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 existsUnique_foxAlgebraicStageQuotientDerivativeVectorLinearMap :
    ∃! f :
        CrossedDifferentialModule (foxAlgebraicStageQuotientCoefficient (X := X) N n) →ₗ[
          foxAlgebraicStageTargetGroupAlgebra (X := X) N n]
          foxAlgebraicStageCoordinateVector (X := X) N n,
      ∀ q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n,
        f (universalCrossedDifferential (foxAlgebraicStageQuotientCoefficient (X := X) N n) q) =
          foxAlgebraicStageQuotientDerivativeVector (X := X) N n q

Module documentation

Fox differential: stage — derivative — quotient — universal

Declarations

foxAlgebraicStageQuotientDerivativeVectorLinearMap

foxAlgebraicStageQuotientDerivativeVectorLinearMap_universal

existsUnique_foxAlgebraicStageQuotientDerivativeVectorLinearMap