FoxDifferential.Completed.FiniteStage.BoundaryQuotient
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
abbrev finiteFoxStageCoordinateModuloRelations : Type u :=
finiteFoxStageCoordinateVector (X := X) N n ⧸
finiteFoxStageRelationBoundarySubmodule (X := X) N nFinite coordinate vectors modulo the submodule generated by finite relation boundaries.
def finiteFoxStageBoundaryModuloRelations [Fintype X] :
finiteFoxStageCoordinateModuloRelations (X := X) N n →ₗ[
finiteFoxStageTargetGroupAlgebra (X := X) N n]
finiteFoxStageTargetGroupAlgebra (X := X) N n :=
Submodule.liftQ (finiteFoxStageRelationBoundarySubmodule (X := X) N n)
(finiteFoxStageFoxBoundary (X := X) N n)
(finiteFoxStageRelationBoundarySubmodule_le_boundaryCycleSubmodule (X := X) N n)
@[simp]The finite Fox boundary descends to the quotient by relation boundaries.
theorem finiteFoxStageBoundaryModuloRelations_mk
[Fintype X] (v : finiteFoxStageCoordinateVector (X := X) N n) :
finiteFoxStageBoundaryModuloRelations (X := X) N n
(Submodule.Quotient.mk v : finiteFoxStageCoordinateModuloRelations (X := X) N n) =
finiteFoxStageFoxBoundary (X := X) N n vShow proof
by
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 finiteFoxStageCoordinateModuloRelations_mk_eq_zero_of_cycle
[Fintype X]
(hexact : finiteFoxStageRelationBoundaryModuleExact (X := X) N n)
{v : finiteFoxStageCoordinateVector (X := X) N n}
(hv : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n) :
(Submodule.Quotient.mk v : finiteFoxStageCoordinateModuloRelations (X := X) N n) = 0Show proof
by
exact (Submodule.Quotient.mk_eq_zero
(p := finiteFoxStageRelationBoundarySubmodule (X := X) N n) (x := v)).2
(hexact hv)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 finiteFoxStageBoundaryModuloRelations_injective_of_relationBoundaryModuleExact
[Fintype X]
(hexact : finiteFoxStageRelationBoundaryModuleExact (X := X) N n) :
Function.Injective (finiteFoxStageBoundaryModuloRelations (X := X) N n)Show proof
by
have hker : ∀ q : finiteFoxStageCoordinateModuloRelations (X := X) N n,
finiteFoxStageBoundaryModuloRelations (X := X) N n q = 0 → q = 0 := by
intro q
refine Submodule.Quotient.induction_on
(p := finiteFoxStageRelationBoundarySubmodule (X := X) N n) q ?_
intro v hv
rw [finiteFoxStageBoundaryModuloRelations_mk] at hv
have hvcycle : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n := hv
exact finiteFoxStageCoordinateModuloRelations_mk_eq_zero_of_cycle
(X := X) N n hexact hvcycle
intro x y hxy
have hsub : finiteFoxStageBoundaryModuloRelations (X := X) N n (x - y) = 0 := by
rw [map_sub, hxy, sub_self]
exact sub_eq_zero.mp (hker (x - y) hsub)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 finiteFoxStageRelationBoundaryModuleExact_of_boundaryModuloRelations_injective
[Fintype X]
(hinj : Function.Injective (finiteFoxStageBoundaryModuloRelations (X := X) N n)) :
finiteFoxStageRelationBoundaryModuleExact (X := X) N nShow proof
by
intro v hv
have hq :
(Submodule.Quotient.mk v : finiteFoxStageCoordinateModuloRelations (X := X) N n) = 0 := by
apply hinj
calc
finiteFoxStageBoundaryModuloRelations (X := X) N n
(Submodule.Quotient.mk v : finiteFoxStageCoordinateModuloRelations (X := X) N n) =
finiteFoxStageFoxBoundary (X := X) N n v := by
rw [finiteFoxStageBoundaryModuloRelations_mk]
_ = 0 := hv
_ = finiteFoxStageBoundaryModuloRelations (X := X) N n
(0 : finiteFoxStageCoordinateModuloRelations (X := X) N n) := by
simp only [map_zero]
exact (Submodule.Quotient.mk_eq_zero
(p := finiteFoxStageRelationBoundarySubmodule (X := X) N n) (x := v)).1 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.
□