Module

RelationIdealDerivative.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.RelationIdealDerivative

16 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — relation ideal derivative

The principal declarations in this module are:

foxAlgebraicStageGroupAlgebraDerivativeVector

The vector of target-valued finite Fox derivatives of a source group-algebra element.

foxAlgebraicStageGroupAlgebraDerivativeVector_apply

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

foxAlgebraicStageGroupAlgebraDerivativeVector_zero

The finite-stage group-algebra derivative vector sends \(0\) to \(0\).

foxAlgebraicStageGroupAlgebraDerivativeVector_add

The finite-stage group-algebra derivative vector preserves addition.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.SourceBoundary

Imported by2

def

foxAlgebraicStageGroupAlgebraDerivativeVector

L38 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivativeVector

Documentation

The vector of target-valued finite Fox derivatives of a 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 · statement

def foxAlgebraicStageGroupAlgebraDerivativeVector
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
    foxAlgebraicStageCoordinateVector (X := X) N n

theorem

foxAlgebraicStageGroupAlgebraDerivativeVector_apply

L48 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivativeVector_apply

Documentation

The finite-stage group-algebra derivative vector is evaluated coordinatewise in the target finite 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 foxAlgebraicStageGroupAlgebraDerivativeVector_apply
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) (i : X) :
    foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n x i =
      foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i x

theorem

foxAlgebraicStageGroupAlgebraDerivativeVector_zero

L56 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivativeVector_zero

Documentation

The finite-stage group-algebra derivative vector sends \(0\) to \(0\).

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 foxAlgebraicStageGroupAlgebraDerivativeVector_zero :
    foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n 0 = 0

theorem

foxAlgebraicStageGroupAlgebraDerivativeVector_add

L63 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivativeVector_add

Documentation

The finite-stage group-algebra derivative vector preserves addition.

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 foxAlgebraicStageGroupAlgebraDerivativeVector_add
    (x y : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
    foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n (x + y) =
      foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n x +
        foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n y

theorem

foxAlgebraicStageGroupAlgebraDerivativeVector_neg

L73 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivativeVector_neg

Documentation

The finite-stage group-algebra derivative vector preserves negation.

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 foxAlgebraicStageGroupAlgebraDerivativeVector_neg
    (x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
    foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n (-x) =
      -foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n x

theorem

foxAlgebraicStageGroupAlgebraDerivativeVector_sub

L82 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivativeVector_sub

Documentation

The finite-stage group-algebra derivative vector preserves subtraction.

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 foxAlgebraicStageGroupAlgebraDerivativeVector_sub
    (x y : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
    foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n (x - y) =
      foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n x -
        foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n y

theorem

foxAlgebraicStageGroupAlgebraDerivativeVector_mul

L91 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivativeVector_mul

Documentation

Product rule for the vector of target-valued derivatives.

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 foxAlgebraicStageGroupAlgebraDerivativeVector_mul
    (x y : foxAlgebraicStageSourceGroupAlgebra (X := X) N n) :
    foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n (x * y) =
      (algebraMap (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
        (foxCommutatorPowerSourceGroupAlgebraAugmentation
          (F := FreeGroup X) N n y)) •
        foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n x +
    foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x •
        foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n y

theorem

foxAlgebraicStageGroupAlgebraDerivativeVector_relationAugmentationGenerator

L112 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivativeVector_relationAugmentationGenerator

Documentation

The derivative vector of a relation augmentation generator is the corresponding relation boundary 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 foxAlgebraicStageGroupAlgebraDerivativeVector_relationAugmentationGenerator
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n
        (foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q) =
      foxAlgebraicStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q)

theorem

foxAlgebraicStageRelationAugmentationGenerator_sourceAugmentation_eq_zero

L127 ↗

FoxDifferential.foxAlgebraicStageRelationAugmentationGenerator_sourceAugmentation_eq_zero

Documentation

Relation augmentation generators have zero source augmentation.

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 foxAlgebraicStageRelationAugmentationGenerator_sourceAugmentation_eq_zero
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxCommutatorPowerSourceGroupAlgebraAugmentation
        (F := FreeGroup X) N n
        (foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q) = 0

theorem

foxAlgebraicStageRelationAugmentationGenerator_groupAlgebraMap_eq_zero

L138 ↗

FoxDifferential.foxAlgebraicStageRelationAugmentationGenerator_groupAlgebraMap_eq_zero

Documentation

Relation augmentation generators have zero target image.

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 foxAlgebraicStageRelationAugmentationGenerator_groupAlgebraMap_eq_zero
    (q : foxAlgebraicStageRelationGroup (X := X) N n) :
    foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
        (foxAlgebraicStageRelationAugmentationGenerator (X := X) N n q) = 0

theorem

foxAlgebraicStageGADeriv_mem_relBoundarySubmodule_of_mem_relAugIdeal

L151 ↗

FoxDifferential.foxAlgebraicStageGADeriv_mem_relBoundarySubmodule_of_mem_relAugIdeal

Documentation

The derivative vector of every element of the finite relation augmentation ideal lies in the relation-boundary submodule; such elements have zero target image and zero augmentation.

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 foxAlgebraicStageGADeriv_mem_relBoundarySubmodule_of_mem_relAugIdeal
    {x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n}
    (hx : x ∈ foxAlgebraicStageRelationAugmentationIdeal (X := X) N n) :
    foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n x ∈
      foxAlgebraicStageRelationBoundarySubmodule (X := X) N n

theorem

foxAlgebraicStageGroupAlgebraDerivativeVector_sourceFoxBoundary

L208 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraDerivativeVector_sourceFoxBoundary

Documentation

Differentiating the source Fox boundary recovers the coordinatewise source-to-target image.

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 foxAlgebraicStageGroupAlgebraDerivativeVector_sourceFoxBoundary
    [Fintype X]
    (a : foxAlgebraicStageSourceCoordinateVector (X := X) N n) :
    foxAlgebraicStageGroupAlgebraDerivativeVector (X := X) N n
        (foxAlgebraicStageSourceFoxBoundary (X := X) N n a) =
      foxAlgebraicStageCoordinateSourceToTarget (X := X) N n a

theorem

foxAlgebraicStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives

L272 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives

Documentation

The source-boundary relation-ideal reduction is a theorem: if the source boundary of a lift is in the relation ideal, differentiating that boundary gives the desired relation-boundary 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 foxAlgebraicStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives
    [Fintype X] :
    foxAlgebraicStageSourceBoundaryRelationIdealReduction (X := X) N n

theorem

foxAlgebraicStageRelationBoundaryModuleExact_of_relationIdeal_derivatives

L286 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryModuleExact_of_relationIdeal_derivatives

Documentation

Differentiation of the relation augmentation ideal gives finite-stage relation-boundary module exactness.

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 foxAlgebraicStageRelationBoundaryModuleExact_of_relationIdeal_derivatives
    [Fintype X] :
    foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n

theorem

foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationIdeal_derivatives

L295 ↗

FoxDifferential.foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationIdeal_derivatives

Documentation

The relation-ideal derivative identity gives finite-stage coordinate coverage.

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 foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationIdeal_derivatives
    [Fintype X] :
    foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

theorem

foxAlgebraicStageSemiBoundaryCyclesCovered_of_relDeriv

L303 ↗

FoxDifferential.foxAlgebraicStageSemiBoundaryCyclesCovered_of_relDeriv

Documentation

The relation-ideal derivative identity gives finite-stage semidirect coverage.

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 foxAlgebraicStageSemiBoundaryCyclesCovered_of_relDeriv
    [Fintype X] :
    foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n

Module documentation

Fox differential: completed — finite stage — relation ideal derivative

Declarations