FoxDifferential.Completed.FiniteStage.BoundaryCycles
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
def finiteFoxStageBoundaryCycleSubmodule [Fintype X] :
Submodule (finiteFoxStageTargetGroupAlgebra (X := X) N n)
(finiteFoxStageCoordinateVector (X := X) N n) :=
LinearMap.ker (finiteFoxStageFoxBoundary (X := X) N n)theorem mem_finiteFoxStageBoundaryCycleSubmodule [Fintype X]
{v : finiteFoxStageCoordinateVector (X := X) N n} :
v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n ↔
finiteFoxStageFoxBoundary (X := X) N n v = 0Membership in the finite-stage boundary-cycle object is characterized by the corresponding boundary-vanishing condition.
Show proof
Iff.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 finiteFoxStageSourceKernelDerivativeSet :
Set (finiteFoxStageCoordinateVector (X := X) N n) :=
{ v | ∃ q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n,
finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q = 1 ∧
finiteFoxStageQuotientDerivativeVector (X := X) N n q = v }def finiteFoxStageKernelWordDerivativeSet :
Set (finiteFoxStageCoordinateVector (X := X) N n) :=
{ v | ∃ w : FreeGroup X,
w ∈ N ∧ finiteFoxStageDerivativeVector (X := X) N n w = v }Word-level kernel derivatives in the finite stage. This is the algebraic form obtained from actual relation words w \(\in\) N.
theorem finiteFoxStageCoefficient_eq_one_of_mem
{w : FreeGroup X} (hw : w ∈ N) :
finiteFoxStageCoefficient (X := X) N n w = 1A word lying in the normal subgroup \(N\) has finite-stage coefficient equal to \(1\) in the quotient by \(N\).
Show proof
by
rw [finiteFoxStageCoefficient_apply]
have hq : QuotientGroup.mk' N w = 1 :=
(QuotientGroup.eq_one_iff (N := N) w).2 hw
rw [hq]
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 finiteFoxStageQuotientCoefficient_eq_one_of_kernel
{q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n}
(hq : finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q = 1) :
finiteFoxStageQuotientCoefficient (X := X) N n q = 1Show proof
by
rw [finiteFoxStageQuotientCoefficient_apply, hq]
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 finiteFoxStageSourceKernelDerivativeAddSubgroup :
AddSubgroup (finiteFoxStageCoordinateVector (X := X) N n) where
carrier := finiteFoxStageSourceKernelDerivativeSet (X := X) N n
zero_mem' := by
refine ⟨1, ?_, ?_⟩
· simp only [map_one]
· simp only [finiteFoxStageQuotientDerivativeVector_one]
add_mem' := by
intro a b ha hb
rcases ha with ⟨q, hq, hqa⟩
rcases hb with ⟨r, hr, hrb⟩
refine ⟨q * r, ?_, ?_⟩
· rw [map_mul, hq, hr, one_mul]
· rw [finiteFoxStageQuotientDerivativeVector_mul]
rw [finiteFoxStageQuotientCoefficient_eq_one_of_kernel (X := X) N n hq]
simp only [hqa, hrb, one_smul]
neg_mem' := by
intro a ha
rcases ha with ⟨q, hq, hqa⟩
refine ⟨q⁻¹, ?_, ?_⟩
· rw [map_inv, hq]
simp only [inv_one]
· rw [IsCrossedDifferential.inv
(finiteFoxStageQuotientDerivativeVector_isCrossedDifferential (X := X) N n)]
have hcoeff :
finiteFoxStageQuotientCoefficient (X := X) N n q⁻¹ = 1 := by
apply finiteFoxStageQuotientCoefficient_eq_one_of_kernel (X := X) N n
rw [map_inv, hq]
simp only [inv_one]
rw [hcoeff]
simp only [hqa, one_smul]
@[simp]theorem finiteFoxStageSourceKernelDerivativeAddSubgroup_coe :
((finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n :
AddSubgroup (finiteFoxStageCoordinateVector (X := X) N n)) :
Set (finiteFoxStageCoordinateVector (X := X) N n)) =
finiteFoxStageSourceKernelDerivativeSet (X := X) N nThe finite-stage source-kernel derivative additive subgroup coerces to its defining carrier.
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 finiteFoxStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet :
finiteFoxStageSourceKernelDerivativeSet (X := X) N n =
finiteFoxStageKernelWordDerivativeSet (X := X) N nThe quotient-level and word-level descriptions of finite-stage source-kernel derivatives coincide.
Show proof
by
ext v
constructor
· rintro ⟨q, hq, hv⟩
rcases QuotientGroup.mk'_surjective
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q with ⟨w, rfl⟩
have hwN : w ∈ N := by
have hwq : QuotientGroup.mk' N w = 1 := by
simpa only [finiteFoxCommutatorPowerQuotientMapToNormalQuotient_mk] using hq
exact (QuotientGroup.eq_one_iff (N := N) w).1 hwq
refine ⟨w, hwN, ?_⟩
simpa using hv
· rintro ⟨w, hwN, hv⟩
refine ⟨QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) w, ?_, ?_⟩
· rw [finiteFoxCommutatorPowerQuotientMapToNormalQuotient_mk]
exact (QuotientGroup.eq_one_iff (N := N) w).2 hwN
· simpa [finiteFoxStageQuotientDerivativeVector_mk] using hvProof. 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 finiteFoxStageKernelWordDerivativeAddSubgroup :
AddSubgroup (finiteFoxStageCoordinateVector (X := X) N n) :=
finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n
@[simp]Word-level kernel derivatives form an additive subgroup, transported from the quotient-level source-kernel subgroup.
theorem finiteFoxStageKernelWordDerivativeAddSubgroup_coe :
((finiteFoxStageKernelWordDerivativeAddSubgroup (X := X) N n :
AddSubgroup (finiteFoxStageCoordinateVector (X := X) N n)) :
Set (finiteFoxStageCoordinateVector (X := X) N n)) =
finiteFoxStageKernelWordDerivativeSet (X := X) N nThe finite-stage kernel-word derivative additive subgroup coerces to its defining carrier.
Show proof
by
rw [finiteFoxStageKernelWordDerivativeAddSubgroup,
finiteFoxStageSourceKernelDerivativeAddSubgroup_coe,
finiteFoxStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet]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 finiteFoxStageSourceKernelDerivativeSet_subset_boundaryCycleSubmodule
[Fintype X] :
finiteFoxStageSourceKernelDerivativeSet (X := X) N n ⊆
(finiteFoxStageBoundaryCycleSubmodule (X := X) N n :
Set (finiteFoxStageCoordinateVector (X := X) N n))Show proof
by
intro v hv
rcases hv with ⟨q, hq, rfl⟩
change finiteFoxStageFoxBoundary (X := X) N n
(finiteFoxStageQuotientDerivativeVector (X := X) N n q) = 0
rw [finiteFoxStageFoxBoundary_quotientDerivativeVector]
rw [finiteFoxStageQuotientCoefficient_eq_one_of_kernel (X := X) N n hq]
simp only [sub_self]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 finiteFoxStageBoundaryCyclesCoveredBySourceKernel [Fintype X] : Prop :=
(finiteFoxStageBoundaryCycleSubmodule (X := X) N n :
Set (finiteFoxStageCoordinateVector (X := X) N n)) ⊆
finiteFoxStageSourceKernelDerivativeSet (X := X) N ntheorem finiteFoxStageBoundaryCyclesCoveredBySourceKernel_iff_words
[Fintype X] :
finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n ↔
(finiteFoxStageBoundaryCycleSubmodule (X := X) N n :
Set (finiteFoxStageCoordinateVector (X := X) N n)) ⊆
finiteFoxStageKernelWordDerivativeSet (X := X) N nThe finite-stage exactness target is equivalent to the formulation using actual kernel words.
Show proof
by
rw [finiteFoxStageBoundaryCyclesCoveredBySourceKernel,
finiteFoxStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet]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 finiteFoxStageSourceKernelDerivativeSet_eq_boundaryCycleSubmodule_iff
[Fintype X] :
finiteFoxStageSourceKernelDerivativeSet (X := X) N n =
(finiteFoxStageBoundaryCycleSubmodule (X := X) N n :
Set (finiteFoxStageCoordinateVector (X := X) N n)) ↔
finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N nShow proof
by
constructor
· intro h v hv
rw [h]
exact hv
· intro h
apply le_antisymm
· exact finiteFoxStageSourceKernelDerivativeSet_subset_boundaryCycleSubmodule (X := X) N n
· exact hProof. 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.
□