FoxDifferential.Completed.FiniteStage.TargetMap
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
theorem finiteFoxStageSemidirectMap_left
(y : FiniteFoxStageSemidirect (X := X) N n) :
(finiteFoxStageSemidirectMap (X := X) hNM n y).left =
fun i : X => finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n (y.left i)The left coordinate of the finite-stage semidirect point is the specified derivative component.
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 finiteFoxStageSemidirectMap_right
(y : FiniteFoxStageSemidirect (X := X) N n) :
(finiteFoxStageSemidirectMap (X := X) hNM n y).right =
finiteFoxStageTargetQuotientMap (X := X) hNM y.rightThe right coordinate of the finite-stage semidirect point is the corresponding quotient component.
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 finiteFoxStageFoxBoundary_targetMap
[Fintype X]
(v : finiteFoxStageCoordinateVector (X := X) N n) :
finiteFoxStageFoxBoundary (X := X) M n
(fun i : X => finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n (v i)) =
finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n
(finiteFoxStageFoxBoundary (X := X) N n v)Show proof
by
rw [finiteFoxStageFoxBoundary_apply, finiteFoxStageFoxBoundary_apply, map_sum]
apply Finset.sum_congr rfl
intro i _
rw [map_mul, map_sub, finiteFoxStageTargetGroupAlgebraMap_of, 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_targetMap_mem
[Fintype X]
{v : finiteFoxStageCoordinateVector (X := X) N n}
(hv : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n) :
(fun i : X => finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n (v i)) ∈
finiteFoxStageBoundaryCycleSubmodule (X := X) M nShow proof
by
rw [mem_finiteFoxStageBoundaryCycleSubmodule]
rw [finiteFoxStageFoxBoundary_targetMap (X := X) hNM n 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.
□theorem finiteFoxStageSemidirectMap_mem_boundaryCycleSet
[Fintype X]
{y : FiniteFoxStageSemidirect (X := X) N n}
(hy : y ∈ finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n) :
finiteFoxStageSemidirectMap (X := X) hNM n y ∈
finiteFoxStageSemidirectBoundaryCycleSet (X := X) M nTarget-quotient refinement sends semidirect boundary-cycle points to boundary-cycle points.
Show proof
by
rcases hy with ⟨hyright, hyboundary⟩
constructor
· rw [finiteFoxStageSemidirectMap_right]
rw [hyright]
exact map_one (finiteFoxStageTargetQuotientMap (X := X) hNM)
· rw [finiteFoxStageSemidirectMap_left]
exact finiteFoxStageBoundaryCycleSubmodule_targetMap_mem (X := X) hNM n hyboundaryProof. 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 finiteFoxStageSemidirectMap_kernelWordPoint
(w : FreeGroup X) :
finiteFoxStageSemidirectMap (X := X) hNM n
(finiteFoxStageSemidirectKernelWordPoint (X := X) N n w) =
finiteFoxStageSemidirectKernelWordPoint (X := X) M n wShow proof
by
apply FiniteFoxStageSemidirect.ext
· funext i
change finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n
(finiteFoxStageDerivative (X := X) N n i w) =
finiteFoxStageDerivative (X := X) M n i w
exact finiteFoxStageDerivative_natural (X := X) hNM n i w
· rw [finiteFoxStageSemidirectMap_right]
simp only [finiteFoxStageSemidirectKernelWordPoint, 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 finiteFoxStageSemidirectMap_sourceKernelPoint
(q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
finiteFoxStageSemidirectMap (X := X) hNM n
(finiteFoxStageSemidirectSourceKernelPoint (X := X) N n q) =
finiteFoxStageSemidirectSourceKernelPoint (X := X) M n
(finiteFoxStageSourceQuotientMap (X := X) hNM n q)Show proof
by
rcases QuotientGroup.mk'_surjective
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q with ⟨w, rfl⟩
apply FiniteFoxStageSemidirect.ext
· funext i
change finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n
(finiteFoxStageQuotientDerivativeVector (X := X) N n
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) w) i) =
finiteFoxStageQuotientDerivativeVector (X := X) M n
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) M n) w) i
rw [finiteFoxStageQuotientDerivativeVector_mk, finiteFoxStageQuotientDerivativeVector_mk]
exact finiteFoxStageDerivative_natural (X := X) hNM n i w
· simp only [finiteFoxStageSemidirectSourceKernelPoint, QuotientGroup.mk'_apply,
finiteFoxStageSemidirectMap_right, 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 finiteFoxStageSemidirectMap_kernelWordDerivativeSet_subset :
(fun y : FiniteFoxStageSemidirect (X := X) N n =>
finiteFoxStageSemidirectMap (X := X) hNM n y) ''
finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) N n ⊆
finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) M nShow proof
by
intro y hy
rcases hy with ⟨z, hz, rfl⟩
rcases hz with ⟨w, hwN, hzw⟩
refine ⟨w, hNM hwN, ?_⟩
rw [← hzw]
exact (finiteFoxStageSemidirectMap_kernelWordPoint (X := X) hNM n w).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 finiteFoxStageSemidirectMap_sourceKernelDerivativeSet_subset :
(fun y : FiniteFoxStageSemidirect (X := X) N n =>
finiteFoxStageSemidirectMap (X := X) hNM n y) ''
finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n ⊆
finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) M nTarget refinement sends source-kernel derivative points into source-kernel derivative points.
Show proof
by
rw [finiteFoxStageSemidirectSourceKernelDerivativeSet_eq_kernelWordDerivativeSet (X := X) N n,
finiteFoxStageSemidirectSourceKernelDerivativeSet_eq_kernelWordDerivativeSet (X := X) M n]
exact finiteFoxStageSemidirectMap_kernelWordDerivativeSet_subset (X := X) hNM nProof. 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.
□