FoxDifferential.Completed.FiniteStage.RelationIdealDerivative

15 Theorem | 1 Definition

This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.

Open this file on GitHub

import

FoxDifferential.Completed.FiniteStage.SourceBoundary

Imported by

Definition FoxDifferential.finiteFoxStageGroupAlgebraDerivativeVector GitHub

def finiteFoxStageGroupAlgebraDerivativeVector
    (x : finiteFoxStageSourceGroupAlgebra (X := X) N n) :
    finiteFoxStageCoordinateVector (X := X) N n :=
  fun i => finiteFoxStageGroupAlgebraDerivative (X := X) N n i x

@[simp]

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

Theorem FoxDifferential.finiteFoxStageGroupAlgebraDerivativeVector_apply GitHub

theorem finiteFoxStageGroupAlgebraDerivativeVector_apply
    (x : finiteFoxStageSourceGroupAlgebra (X := X) N n) (i : X) :
    finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x i =
      finiteFoxStageGroupAlgebraDerivative (X := X) N n i x

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

Show proof

Theorem FoxDifferential.finiteFoxStageGroupAlgebraDerivativeVector_zero GitHub

theorem finiteFoxStageGroupAlgebraDerivativeVector_zero :
    finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n 0 = 0

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

Show proof

Theorem FoxDifferential.finiteFoxStageGroupAlgebraDerivativeVector_add GitHub

theorem finiteFoxStageGroupAlgebraDerivativeVector_add
    (x y : finiteFoxStageSourceGroupAlgebra (X := X) N n) :
    finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n (x + y) =
      finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x +
        finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n y

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

Show proof

Theorem FoxDifferential.finiteFoxStageGroupAlgebraDerivativeVector_neg GitHub

theorem finiteFoxStageGroupAlgebraDerivativeVector_neg
    (x : finiteFoxStageSourceGroupAlgebra (X := X) N n) :
    finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n (-x) =
      -finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x

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

Show proof

Theorem FoxDifferential.finiteFoxStageGroupAlgebraDerivativeVector_sub GitHub

theorem finiteFoxStageGroupAlgebraDerivativeVector_sub
    (x y : finiteFoxStageSourceGroupAlgebra (X := X) N n) :
    finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n (x - y) =
      finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x -
        finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n y

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

Show proof

Theorem FoxDifferential.finiteFoxStageGroupAlgebraDerivativeVector_mul GitHub

theorem finiteFoxStageGroupAlgebraDerivativeVector_mul
    (x y : finiteFoxStageSourceGroupAlgebra (X := X) N n) :
    finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n (x * y) =
      (algebraMap (ModNCompletedCoeff n)
        (finiteFoxStageTargetGroupAlgebra (X := X) N n)
        (finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
          (F := FreeGroup X) N n y)) •
        finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x +
    finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x •
        finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n y

Product rule for the vector of target-valued derivatives.

Show proof

Theorem FoxDifferential.finiteFoxStageGroupAlgebraDerivativeVector_relationAugmentationGenerator GitHub

theorem finiteFoxStageGroupAlgebraDerivativeVector_relationAugmentationGenerator
    (q : finiteFoxStageRelationGroup (X := X) N n) :
    finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n
        (finiteFoxStageRelationAugmentationGenerator (X := X) N n q) =
      finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q)

The derivative vector of a relation augmentation generator is the corresponding relation boundary vector.

Show proof

Theorem FoxDifferential.finiteFoxStageRelationAugmentationGenerator_sourceAugmentation_eq_zero GitHub

theorem finiteFoxStageRelationAugmentationGenerator_sourceAugmentation_eq_zero
    (q : finiteFoxStageRelationGroup (X := X) N n) :
    finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
        (F := FreeGroup X) N n
        (finiteFoxStageRelationAugmentationGenerator (X := X) N n q) = 0

Relation augmentation generators have zero source augmentation.

Show proof

Theorem FoxDifferential.finiteFoxStageRelationAugmentationGenerator_groupAlgebraMap_eq_zero GitHub

theorem finiteFoxStageRelationAugmentationGenerator_groupAlgebraMap_eq_zero
    (q : finiteFoxStageRelationGroup (X := X) N n) :
    finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
        (finiteFoxStageRelationAugmentationGenerator (X := X) N n q) = 0

Relation augmentation generators have zero target image.

Show proof

Theorem FoxDifferential.finiteFoxGADeriv_mem_relBoundarySubmodule_of_mem_relAugIdeal GitHub

theorem finiteFoxGADeriv_mem_relBoundarySubmodule_of_mem_relAugIdeal
    {x : finiteFoxStageSourceGroupAlgebra (X := X) N n}
    (hx : x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N n) :
    finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x ∈
      finiteFoxStageRelationBoundarySubmodule (X := X) N n

The derivative vector of every element of the finite relation augmentation ideal lies in the relation-boundary submodule. The proof keeps the two extra invariants used by the product rule: elements of this ideal have zero target image and zero augmentation.

Show proof

Theorem FoxDifferential.finiteFoxStageGroupAlgebraDerivativeVector_sourceFoxBoundary GitHub

theorem finiteFoxStageGroupAlgebraDerivativeVector_sourceFoxBoundary
    [Fintype X]
    (a : finiteFoxStageSourceCoordinateVector (X := X) N n) :
    finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n
        (finiteFoxStageSourceFoxBoundary (X := X) N n a) =
      finiteFoxStageCoordinateSourceToTarget (X := X) N n a

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

Show proof

Theorem FoxDifferential.finiteFoxStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives GitHub

theorem finiteFoxStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives
    [Fintype X] :
    finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N n

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.

Show proof

Theorem FoxDifferential.finiteFoxStageRelationBoundaryModuleExact_of_relationIdeal_derivatives GitHub

theorem finiteFoxStageRelationBoundaryModuleExact_of_relationIdeal_derivatives
    [Fintype X] :
    finiteFoxStageRelationBoundaryModuleExact (X := X) N n

Finite-stage relation-boundary module exactness follows from differentiating the relation augmentation ideal.

Show proof

Theorem FoxDifferential.finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationIdeal_derivatives GitHub

theorem finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationIdeal_derivatives
    [Fintype X] :
    finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

Finite-stage coordinate coverage follows from the relation-ideal derivative calculation.

Show proof

Theorem FoxDifferential.finiteFoxStageSemiBoundaryCyclesCovered_of_relDeriv GitHub

theorem finiteFoxStageSemiBoundaryCyclesCovered_of_relDeriv
    [Fintype X] :
    finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n

Finite-stage semidirect coverage follows from the relation-ideal derivative calculation.

Show proof

FoxDifferential.Completed.FiniteStage.RelationIdealDerivative

Declarations