FoxDifferential.Completed.FiniteStage.CoeffMap.Boundary
Fox Differential / Completed / Finite Stage / Coefficient Map / Boundary.
import
theorem finiteFoxStageFoxBoundary_coeffMap
[Fintype X]
(N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
(v : finiteFoxStageCoordinateVector (X := X) N m₀) :
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm
(finiteFoxStageFoxBoundary (X := X) N m₀ v) =
finiteFoxStageFoxBoundary (X := X) N n₀
(fun i : X =>
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm (v i))Coefficient reduction commutes with the finite-stage Fox boundary map.
Show proof
by
rw [finiteFoxStageFoxBoundary_apply, finiteFoxStageFoxBoundary_apply]
simp only [QuotientGroup.mk'_apply, MonoidAlgebra.of_apply, map_sum, map_mul, map_sub,
finiteFoxStageTargetGroupAlgebraCoeffMap_single_apply, map_one]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 finiteFoxStageBoundaryCycleSubmodule_coeffMap_mem
[Fintype X]
(N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
{v : finiteFoxStageCoordinateVector (X := X) N m₀}
(hv : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N m₀) :
(fun i : X =>
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm (v i)) ∈
finiteFoxStageBoundaryCycleSubmodule (X := X) N n₀A vector is a boundary cycle after coefficient reduction whenever it was one before reduction.
Show proof
by
rw [mem_finiteFoxStageBoundaryCycleSubmodule]
rw [← finiteFoxStageFoxBoundary_coeffMap (X := X) N hnm v]
rw [mem_finiteFoxStageBoundaryCycleSubmodule] at hv
rw [hv]
exact map_zero _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.
□