FoxDifferential.Completed.FiniteStage.SourceDerivativeVector
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
def finiteFoxStageSourceDerivativeVector
(q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
finiteFoxStageSourceCoordinateVector (X := X) N n :=
fun i =>
finiteFoxStageSourceGroupAlgebraDerivative (X := X) N n i
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q)Source-valued derivative vector of a source quotient element.
theorem finiteFoxStageSourceDerivativeVector_apply
(q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(i : X) :
finiteFoxStageSourceDerivativeVector (X := X) N n q i =
finiteFoxStageSourceGroupAlgebraDerivative (X := X) N n i
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q)The finite-stage source derivative vector evaluates the source word at the chosen coordinate.
Show proof
rflProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□def finiteFoxStageSourceGroupAlgebraDerivativeVector :
finiteFoxStageSourceGroupAlgebra (X := X) N n →ₗ[ModNCompletedCoeff n]
finiteFoxStageSourceCoordinateVector (X := X) N n where
toFun x := fun i => finiteFoxStageSourceGroupAlgebraDerivative (X := X) N n i x
map_add' := by
intro x y
funext i
simp only [map_add, Pi.add_apply]
map_smul' := by
intro a x
funext i
simp only [map_smul, RingHom.id_apply, Pi.smul_apply]Source-valued derivative vector of an arbitrary source group-algebra element.
theorem finiteFoxStageSourceGroupAlgebraDerivativeVector_apply
(x : finiteFoxStageSourceGroupAlgebra (X := X) N n) (i : X) :
finiteFoxStageSourceGroupAlgebraDerivativeVector (X := X) N n x i =
finiteFoxStageSourceGroupAlgebraDerivative (X := X) N n i xShow proof
rflProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem finiteFoxStageSourceFoxBoundary_sourceDerivativeVector
[Fintype X]
(q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
finiteFoxStageSourceFoxBoundary (X := X) N n
(finiteFoxStageSourceDerivativeVector (X := X) N n q) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q - 1The source boundary of the source-valued derivative of a source quotient element is \(q-1\).
Show proof
by
rw [finiteFoxStageSourceFoxBoundary_apply]
exact (finiteFoxStageSourceGroupAlgebraDerivative_of_quotient_fundamental_formula
(X := X) (N := N) (n := n) q).symmProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem finiteFoxStageSourceFoxBoundary_sourceGroupAlgebraDerivativeVector
[Fintype X]
(x : finiteFoxStageSourceGroupAlgebra (X := X) N n) :
finiteFoxStageSourceFoxBoundary (X := X) N n
(finiteFoxStageSourceGroupAlgebraDerivativeVector (X := X) N n x) =
x -
algebraMap (ModNCompletedCoeff n)
(finiteFoxStageSourceGroupAlgebra (X := X) N n)
(finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N n x)The source boundary of the source-valued derivative of a group-algebra element is the usual source augmentation formula.
Show proof
by
rw [finiteFoxStageSourceFoxBoundary_apply]
exact (finiteFoxStageSourceGroupAlgebraDerivative_groupAlgebra_fundamental_formula
(X := X) (N := N) (n := n) x).symmProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem finiteFoxStageCoordinateSourceToTarget_smul_source
(a : finiteFoxStageSourceGroupAlgebra (X := X) N n)
(v : finiteFoxStageSourceCoordinateVector (X := X) N n) :
finiteFoxStageCoordinateSourceToTarget (X := X) N n (a • v) =
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n a •
finiteFoxStageCoordinateSourceToTarget (X := X) N n vThe source-to-target coordinate map commutes with source scalar multiplication.
Show proof
by
funext i
rw [finiteFoxStageCoordinateSourceToTarget_apply]
simp only [Pi.smul_apply, finiteFoxStageCoordinateSourceToTarget_apply]
change
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (a * v i) =
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n a *
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (v i)
rw [RingHom.map_mul]Proof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem finiteFoxStageCoordinateSourceToTarget_sourceDerivativeVector
(q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
finiteFoxStageCoordinateSourceToTarget (X := X) N n
(finiteFoxStageSourceDerivativeVector (X := X) N n q) =
finiteFoxStageQuotientDerivativeVector (X := X) N n qApplying source-to-target coordinates to a source derivative vector gives the target-valued finite derivative vector.
Show proof
by
funext i
rw [finiteFoxStageCoordinateSourceToTarget_apply,
finiteFoxStageSourceDerivativeVector_apply]
rw [finiteFoxStageSourceGroupAlgebraDerivative_map_of_quotient,
finiteFoxStageGroupAlgebraDerivative_of_quotient]
rflProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem finiteFoxStageCoordinateSourceToTarget_sourceGroupAlgebraDerivativeVector
(x : finiteFoxStageSourceGroupAlgebra (X := X) N n) :
finiteFoxStageCoordinateSourceToTarget (X := X) N n
(finiteFoxStageSourceGroupAlgebraDerivativeVector (X := X) N n x) =
fun i => finiteFoxStageGroupAlgebraDerivative (X := X) N n i xApplying source-to-target coordinates to the group-algebra source derivative vector gives the coordinatewise target group-algebra derivative.
Show proof
by
funext i
rw [finiteFoxStageCoordinateSourceToTarget_apply,
finiteFoxStageSourceGroupAlgebraDerivativeVector_apply]
exact finiteFoxStageSourceGroupAlgebraDerivative_map
(X := X) (N := N) (n := n) i xProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□