FoxDifferential.Completed.FiniteStage.BoundaryCycleHom
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
abbrev finiteFoxStageSourceKernel : Type u :=
(finiteFoxCommutatorPowerQuotientMapToNormalQuotient
(F := FreeGroup X) N n).kerThe kernel of the finite source-to-target quotient \(F/[N,N]N^n \to F/N\).
def finiteFoxStageSourceKernelDerivativeAddHom :
Additive (finiteFoxStageSourceKernel (X := X) N n) →+
finiteFoxStageCoordinateVector (X := X) N n where
toFun q :=
finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1
map_zero' := by
change finiteFoxStageQuotientDerivativeVector (X := X) N n
(1 : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) = 0
simp only [finiteFoxStageQuotientDerivativeVector_one]
map_add' := by
intro q r
change finiteFoxStageQuotientDerivativeVector (X := X) N n
((Additive.toMul q).1 * (Additive.toMul r).1) =
finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1 +
finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul r).1
rw [finiteFoxStageQuotientDerivativeVector_mul]
have hqcoeff :
finiteFoxStageQuotientCoefficient (X := X) N n (Additive.toMul q).1 = 1 :=
finiteFoxStageQuotientCoefficient_eq_one_of_kernel (X := X) N n
(Additive.toMul q).2
rw [hqcoeff]
simp only [one_smul]
@[simp]The descended finite-stage Fox derivative, restricted to the source quotient kernel, is an additive homomorphism.
theorem finiteFoxStageSourceKernelDerivativeAddHom_of
(q : finiteFoxStageSourceKernel (X := X) N n) :
finiteFoxStageSourceKernelDerivativeAddHom (X := X) N n (Additive.ofMul q) =
finiteFoxStageQuotientDerivativeVector (X := X) N n q.1The finite-stage boundary or derivative construction defines the corresponding additive homomorphism.
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.
□theorem finiteFoxStageSourceKernelDerivativeAddHom_range_eq :
AddMonoidHom.range (finiteFoxStageSourceKernelDerivativeAddHom (X := X) N n) =
finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N nThe range of the additive source-kernel derivative map is exactly the source-kernel derivative additive subgroup already used in the finite-stage density target.
Show proof
by
ext v
constructor
· intro hv
rcases hv with ⟨q, rfl⟩
refine ⟨(Additive.toMul q).1, (Additive.toMul q).2, rfl⟩
· intro hv
rcases hv with ⟨q, hq, rfl⟩
exact ⟨Additive.ofMul
(⟨q, hq⟩ : finiteFoxStageSourceKernel (X := X) N n), rfl⟩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.
□def finiteFoxStageSourceKernelDerivativeToBoundaryCycles [Fintype X] :
Additive (finiteFoxStageSourceKernel (X := X) N n) →+
finiteFoxStageBoundaryCycleSubmodule (X := X) N n where
toFun q :=
⟨finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1,
finiteFoxStageSourceKernelDerivativeSet_subset_boundaryCycleSubmodule (X := X) N n
⟨(Additive.toMul q).1, (Additive.toMul q).2, rfl⟩⟩
map_zero' := by
apply Subtype.ext
change finiteFoxStageQuotientDerivativeVector (X := X) N n
(1 : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) = 0
simp only [finiteFoxStageQuotientDerivativeVector_one]
map_add' := by
intro q r
apply Subtype.ext
change finiteFoxStageQuotientDerivativeVector (X := X) N n
((Additive.toMul q).1 * (Additive.toMul r).1) =
finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1 +
finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul r).1
rw [finiteFoxStageQuotientDerivativeVector_mul]
have hqcoeff :
finiteFoxStageQuotientCoefficient (X := X) N n (Additive.toMul q).1 = 1 :=
finiteFoxStageQuotientCoefficient_eq_one_of_kernel (X := X) N n
(Additive.toMul q).2
rw [hqcoeff]
simp only [one_smul]
@[simp]The source-kernel derivative map, with codomain restricted to finite Fox boundary cycles.
theorem finiteFoxStageSourceKernelDerivativeToBoundaryCycles_val
[Fintype X] (q : finiteFoxStageSourceKernel (X := X) N n) :
(finiteFoxStageSourceKernelDerivativeToBoundaryCycles (X := X) N n
(Additive.ofMul q) : finiteFoxStageCoordinateVector (X := X) N n) =
finiteFoxStageQuotientDerivativeVector (X := X) N n q.1Show 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 finiteFoxStageBoundaryCyclesCovered_iff_surj_derivativeToBoundaryCycles
[Fintype X] :
finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n ↔
Function.Surjective
(finiteFoxStageSourceKernelDerivativeToBoundaryCycles (X := X) N n)The finite-stage coverage statement is precisely surjectivity of the source-kernel derivative map onto the boundary-cycle subgroup.
Show proof
by
constructor
· intro hcover y
rcases hcover y.2 with ⟨q, hq, hqy⟩
refine ⟨Additive.ofMul
(⟨q, hq⟩ : finiteFoxStageSourceKernel (X := X) N n), ?_⟩
apply Subtype.ext
simpa using hqy
· intro hsurj v hv
rcases hsurj ⟨v, hv⟩ with ⟨q, hq⟩
refine ⟨(Additive.toMul q).1, (Additive.toMul q).2, ?_⟩
exact congrArg Subtype.val hqProof. 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 finiteFoxStageSourceKernelDerivativeSet_eq_boundaryCycleSubmodule_of_surjective
[Fintype X]
(hsurj : Function.Surjective
(finiteFoxStageSourceKernelDerivativeToBoundaryCycles (X := X) N n)) :
finiteFoxStageSourceKernelDerivativeSet (X := X) N n =
(finiteFoxStageBoundaryCycleSubmodule (X := X) N n :
Set (finiteFoxStageCoordinateVector (X := X) N n))If the restricted source-kernel derivative map is surjective, then the source-kernel image is all of the finite boundary-cycle subgroup.
Show proof
by
exact
(finiteFoxStageSourceKernelDerivativeSet_eq_boundaryCycleSubmodule_iff
(X := X) N n).2
((finiteFoxStageBoundaryCyclesCovered_iff_surj_derivativeToBoundaryCycles
(X := X) N n).2 hsurj)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.
□