Module

Basic.lean

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

15 declarations indexed from sourceView source ↗

Module documentation

Fox differential: stage — derivative — quotient — basic

The principal declarations in this module are:

foxAlgebraicStageQuotientLift

The finite-stage lift descended to the source quotient \(F/[N,N]N^n\).

foxAlgebraicStageQuotientCoefficient

Coefficient homomorphism for the finite-stage quotient crossed homomorphism.

foxAlgebraicStageQuotientLift_mk

Evaluation of the descended finite-stage lift on a representative.

foxAlgebraicStageQuotientLift_right

The right component of the descended finite-stage lift is the quotient map from \(F/[N,N]N^n\) to \(F/N\).

Imports2

Imported by3

def

foxAlgebraicStageQuotientLift

L39 ↗

FoxDifferential.foxAlgebraicStageQuotientLift

Documentation

The finite-stage lift descended to the source quotient \(F/[N,N]N^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

def foxAlgebraicStageQuotientLift :
    FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n →*
      FoxAlgebraicStageSemidirect (X := X) N n

theorem

foxAlgebraicStageQuotientLift_mk

L50 ↗

FoxDifferential.foxAlgebraicStageQuotientLift_mk

Documentation

Evaluation of the descended finite-stage lift on a representative.

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 foxAlgebraicStageQuotientLift_mk (w : FreeGroup X) :
    foxAlgebraicStageQuotientLift (X := X) N n
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N n) w) =
      foxAlgebraicStageLift (X := X) N n w

theorem

foxAlgebraicStageQuotientLift_right

L62 ↗

FoxDifferential.foxAlgebraicStageQuotientLift_right

Documentation

The right component of the descended finite-stage lift is the quotient map from \(F/[N,N]N^n\) 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 foxAlgebraicStageQuotientLift_right
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    (foxAlgebraicStageQuotientLift (X := X) N n q).right =
      foxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q

def

foxAlgebraicStageQuotientCoefficient

L72 ↗

FoxDifferential.foxAlgebraicStageQuotientCoefficient

Documentation

Coefficient homomorphism for the finite-stage quotient crossed homomorphism.

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 foxAlgebraicStageQuotientCoefficient :
    (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) →*
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n

def

foxAlgebraicStageQuotientDerivativeVector

L83 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivativeVector

Documentation

The finite-stage derivative vector descended to \(F/[N,N]N^n\), 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 foxAlgebraicStageQuotientDerivativeVector :
    ScalarCrossedHom
      (foxAlgebraicStageQuotientCoefficient (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n) where
  toFun q := (foxAlgebraicStageQuotientLift (X := X) N n q).left
  map_mul' := by
    intro q r
    simp only [scalarCrossedAction_apply, map_mul,
      FoxAlgebraicStageSemidirect.mul_left,
      foxAlgebraicStageQuotientLift_right,
      foxAlgebraicStageQuotientCoefficient, MonoidHom.coe_comp,
      Function.comp_apply, MonoidAlgebra.of_apply]

theorem

foxAlgebraicStageQuotientDerivativeVector_mk

L98 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivativeVector_mk

Documentation

Evaluation of the descended derivative vector on a representative.

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 foxAlgebraicStageQuotientDerivativeVector_mk (w : FreeGroup X) :
    foxAlgebraicStageQuotientDerivativeVector (X := X) N n
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N n) w) =
      foxAlgebraicStageDerivativeVector (X := X) N n w

def

foxAlgebraicStageQuotientDerivative

L106 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivative

Documentation

A coordinate of the descended finite-stage derivative on the 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

def foxAlgebraicStageQuotientDerivative (i : X)
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageTargetGroupAlgebra (X := X) N n

theorem

foxAlgebraicStageQuotientDerivative_mk

L113 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivative_mk

Documentation

Evaluation of a descended derivative coordinate on a representative.

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 foxAlgebraicStageQuotientDerivative_mk (i : X) (w : FreeGroup X) :
    foxAlgebraicStageQuotientDerivative (X := X) N n i
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N n) w) =
      foxAlgebraicStageDerivative (X := X) N n i w

theorem

foxAlgebraicStageQuotientCoefficient_apply

L126 ↗

FoxDifferential.foxAlgebraicStageQuotientCoefficient_apply

Documentation

The finite Fox-stage quotient coefficient is evaluated by projecting the group coordinate and reducing the coefficient.

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 foxAlgebraicStageQuotientCoefficient_apply
    (q : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
    foxAlgebraicStageQuotientCoefficient (X := X) N n q =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N)
        (foxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q)

theorem

foxAlgebraicStageQuotientCoefficient_mk

L140 ↗

FoxDifferential.foxAlgebraicStageQuotientCoefficient_mk

Documentation

The quotient coefficient homomorphism agrees with the free-group coefficient homomorphism on representatives.

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 foxAlgebraicStageQuotientCoefficient_mk (w : FreeGroup X) :
    foxAlgebraicStageQuotientCoefficient (X := X) N n
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N n) w) =
      foxAlgebraicStageCoefficient (X := X) N n w

theorem

foxAlgebraicStageQuotientDerivative_one

L149 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivative_one

Documentation

The descended 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 foxAlgebraicStageQuotientDerivative_one (i : X) :
    foxAlgebraicStageQuotientDerivative (X := X) N n i
        (1 : FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n) = 0

theorem

foxAlgebraicStageQuotientDerivativeVector_of

L158 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivativeVector_of

Documentation

Generator value for the descended finite-stage 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 foxAlgebraicStageQuotientDerivativeVector_of (x : X) :
    foxAlgebraicStageQuotientDerivativeVector (X := X) N n
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N n) (FreeGroup.of x)) =
      Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n)

theorem

foxAlgebraicStageQuotientDerivative_of

L167 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivative_of

Documentation

At a generator, the descended finite-stage derivative has the corresponding component value.

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 foxAlgebraicStageQuotientDerivative_of (i x : X) :
    foxAlgebraicStageQuotientDerivative (X := X) N n i
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N n) (FreeGroup.of x)) =
      (Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n) :
        X → foxAlgebraicStageTargetGroupAlgebra (X := X) N n) i

theorem

foxAlgebraicStageQuotientDerivativeVector_unique

L179 ↗

FoxDifferential.foxAlgebraicStageQuotientDerivativeVector_unique

Documentation

The bundled descended derivative vector is uniquely determined by its values on quotient 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 foxAlgebraicStageQuotientDerivativeVector_unique
    (delta : ScalarCrossedHom
      (foxAlgebraicStageQuotientCoefficient (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n))
    (hbasis :
      ∀ x : X,
        delta
          (QuotientGroup.mk'
            (foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
            (FreeGroup.of x)) =
          Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n)) :
    delta = foxAlgebraicStageQuotientDerivativeVector (X := X) N n

theorem

existsUnique_foxAlgebraicStageQuotientDerivativeVector

L231 ↗

FoxDifferential.existsUnique_foxAlgebraicStageQuotientDerivativeVector

Documentation

Existence and uniqueness theorem for 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_foxAlgebraicStageQuotientDerivativeVector :
    ∃! delta : ScalarCrossedHom
        (foxAlgebraicStageQuotientCoefficient (X := X) N n)
        (foxAlgebraicStageCoordinateVector (X := X) N n),
      ∀ x : X,
        delta
          (QuotientGroup.mk'
            (foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
            (FreeGroup.of x)) =
          Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n)

Module documentation

Fox differential: stage — derivative — quotient — basic

Declarations