FoxDifferential.Completed.FiniteStage.RelationSubmodule
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
def finiteFoxStageRelationBoundarySubmodule :
Submodule (finiteFoxStageTargetGroupAlgebra (X := X) N n)
(finiteFoxStageCoordinateVector (X := X) N n) :=
Submodule.span (finiteFoxStageTargetGroupAlgebra (X := X) N n)
(finiteFoxStageRelationBoundaryRange (X := X) N n :
Set (finiteFoxStageCoordinateVector (X := X) N n))The \((\mathbb{Z}/n\mathbb{Z})[F/N]\)-submodule generated by finite-stage relation-boundary vectors.
theorem finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule :
(finiteFoxStageRelationBoundaryRange (X := X) N n :
Set (finiteFoxStageCoordinateVector (X := X) N n)) ⊆
finiteFoxStageRelationBoundarySubmodule (X := X) N nEvery actual relation-boundary vector lies in the generated relation-boundary submodule.
Show proof
by
exact Submodule.subset_spanProof. 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 finiteFoxStageRelationBoundaryAddMonoidHom_mem_relationBoundarySubmodule
(q : Additive (finiteFoxStageRelationGroup (X := X) N n)) :
finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n q ∈
finiteFoxStageRelationBoundarySubmodule (X := X) N nA relation boundary of a finite-stage relation lies in the generated submodule.
Show proof
by
apply finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule (X := X) N n
exact (mem_finiteFoxStageRelationBoundaryRange_iff (X := X) N n).2 ⟨q, 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.
□theorem finiteFoxStageRelationBoundaryRange_smul_mem
(a : finiteFoxStageTargetGroupAlgebra (X := X) N n)
{v : finiteFoxStageCoordinateVector (X := X) N n}
(hv : v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n) :
a • v ∈ finiteFoxStageRelationBoundaryRange (X := X) N nThe actual relation-boundary image is stable under arbitrary finite group-algebra scalars.
Show proof
by
classical
refine MonoidAlgebra.induction_linear
(M := finiteFoxStageTargetQuotient (X := X) N)
(R := ModNCompletedCoeff n)
(p := fun a : finiteFoxStageTargetGroupAlgebra (X := X) N n =>
a • v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n)
a ?zero ?add ?single
· simp only [zero_smul, zero_mem]
· intro a b ha hb
rw [add_smul]
exact (finiteFoxStageRelationBoundaryRange (X := X) N n).add_mem ha hb
· intro h c
rcases ZMod.intCast_surjective c with ⟨m, rfl⟩
have hbase :
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) h) • v ∈
finiteFoxStageRelationBoundaryRange (X := X) N n :=
finiteFoxStageRelationBoundaryRange_basis_smul_mem (X := X) N n h hv
have hsingle :
((MonoidAlgebra.single h (m : ModNCompletedCoeff n) :
finiteFoxStageTargetGroupAlgebra (X := X) N n) • v :
finiteFoxStageCoordinateVector (X := X) N n) =
(m : ℤ) •
((MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) h) • v :
finiteFoxStageCoordinateVector (X := X) N n) := by
have hsingleAlg :
(MonoidAlgebra.single h (m : ModNCompletedCoeff n) :
finiteFoxStageTargetGroupAlgebra (X := X) N n) =
(m : ModNCompletedCoeff n) •
MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) h := by
simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.smul_single, smul_eq_mul, mul_one]
rw [hsingleAlg]
rw [smul_assoc]
exact Int.cast_smul_eq_zsmul (ModNCompletedCoeff n) m
((MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) h) • v :
finiteFoxStageCoordinateVector (X := X) N n)
rw [hsingle]
exact (finiteFoxStageRelationBoundaryRange (X := X) N n).zsmul_mem hbase mProof. 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 finiteFoxStageRelationBoundaryImageSubmodule :
Submodule (finiteFoxStageTargetGroupAlgebra (X := X) N n)
(finiteFoxStageCoordinateVector (X := X) N n) where
carrier := finiteFoxStageRelationBoundaryRange (X := X) N n
zero_mem' := (finiteFoxStageRelationBoundaryRange (X := X) N n).zero_mem
add_mem' := by
intro x y hx hy
exact (finiteFoxStageRelationBoundaryRange (X := X) N n).add_mem hx hy
smul_mem' := by
intro a v hv
exact finiteFoxStageRelationBoundaryRange_smul_mem (X := X) N n a hv
@[simp]The actual relation-boundary image as a finite group-algebra submodule.
theorem finiteFoxStageRelationBoundaryImageSubmodule_coe :
((finiteFoxStageRelationBoundaryImageSubmodule (X := X) N n :
Submodule (finiteFoxStageTargetGroupAlgebra (X := X) N n)
(finiteFoxStageCoordinateVector (X := X) N n)) :
Set (finiteFoxStageCoordinateVector (X := X) N n)) =
finiteFoxStageSourceKernelDerivativeSet (X := X) N nThe relation-boundary image submodule has the finite-stage source-kernel derivative set as its underlying set.
Show proof
by
simp only [finiteFoxStageRelationBoundaryImageSubmodule, finiteFoxStageRelationBoundaryRange_coe,
Submodule.coe_set_mk, AddSubmonoid.coe_set_mk, AddSubsemigroup.coe_set_mk]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 finiteFoxStageRelationBoundarySubmodule_eq_imageSubmodule :
finiteFoxStageRelationBoundarySubmodule (X := X) N n =
finiteFoxStageRelationBoundaryImageSubmodule (X := X) N nThe generated relation-boundary submodule is the actual relation-boundary image, because the image is already stable under the finite target group algebra.
Show proof
by
apply le_antisymm
· refine Submodule.span_le.2 ?_
intro v hv
exact hv
· intro v hv
exact finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule (X := X) N n 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.
□theorem finiteFoxStageRelationBoundarySubmodule_le_boundaryCycleSubmodule
[Fintype X] :
finiteFoxStageRelationBoundarySubmodule (X := X) N n ≤
finiteFoxStageBoundaryCycleSubmodule (X := X) N nThe relation-boundary submodule is contained in the finite Fox boundary cycles.
Show proof
by
refine Submodule.span_le.2 ?_
intro v hv
exact finiteFoxStageRelationBoundary_range_le_boundaryCycleSubmodule (X := X) N n 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 finiteFoxStageRelationBoundaryModuleExact [Fintype X] : Prop :=
finiteFoxStageBoundaryCycleSubmodule (X := X) N n ≤
finiteFoxStageRelationBoundarySubmodule (X := X) N ntheorem finiteFoxStageRelationBoundaryModuleExact_of_relationBoundaryExact
[Fintype X]
(hexact : finiteFoxStageRelationBoundaryExact (X := X) N n) :
finiteFoxStageRelationBoundaryModuleExact (X := X) N nFunction-level relation-boundary exactness implies the module-level finite exactness target.
Show proof
by
intro v hv
have hcovered : finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n :=
finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryExact
(X := X) N n hexact
have hvsource : v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n :=
hcovered hv
have hvrange : v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n := by
change v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n
exact hvsource
exact finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule
(X := X) N n hvrangeProof. 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_boundaryCyclesCoveredBySourceKernel
[Fintype X]
(hcovered : finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n) :
finiteFoxStageRelationBoundaryModuleExact (X := X) N nShow proof
by
intro v hv
have hvsource : v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n := hcovered hv
have hvrange : v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n := by
change v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n
exact hvsource
exact finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule
(X := X) N n hvrangeProof. 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 finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact
[Fintype X]
(hexact : finiteFoxStageRelationBoundaryModuleExact (X := X) N n) :
finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N nShow proof
by
intro v hv
have hvrel : v ∈ finiteFoxStageRelationBoundarySubmodule (X := X) N n := hexact hv
rw [finiteFoxStageRelationBoundarySubmodule_eq_imageSubmodule (X := X) N n] at hvrel
simpa [finiteFoxStageRelationBoundaryImageSubmodule] using hvrelProof. 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_iff_submodule_eq_boundaryCycleSubmodule
[Fintype X] :
finiteFoxStageRelationBoundaryModuleExact (X := X) N n ↔
finiteFoxStageRelationBoundarySubmodule (X := X) N n =
finiteFoxStageBoundaryCycleSubmodule (X := X) N nModule exactness is equivalent to equality between \(\ker \partial\) and the generated relation-boundary submodule.
Show proof
by
constructor
· intro hexact
exact le_antisymm
(finiteFoxStageRelationBoundarySubmodule_le_boundaryCycleSubmodule (X := X) N n)
hexact
· intro h v hv
rw [h]
exact 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.
□theorem relationBoundarySubmodule_eq_boundaryCycleSubmodule_of_relExact
[Fintype X]
(hexact : finiteFoxStageRelationBoundaryExact (X := X) N n) :
finiteFoxStageRelationBoundarySubmodule (X := X) N n =
finiteFoxStageBoundaryCycleSubmodule (X := X) N nShow proof
(finiteFoxStageRelationBoundaryModuleExact_iff_submodule_eq_boundaryCycleSubmodule
(X := X) N n).1
(finiteFoxStageRelationBoundaryModuleExact_of_relationBoundaryExact
(X := X) N n hexact)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.
□