import
theorem finiteFoxStageSourceKernelDerivativeSet_zsmul_mem
(m : ℤ) {v : finiteFoxStageCoordinateVector (X := X) N n}
(hv : v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n) :
m • v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N nThe additive source-kernel derivative set is closed under integer multiples.
Show proof
by
have hv' : v ∈ finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n := hv
exact (finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n).zsmul_mem hv' 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.
□theorem finiteFoxStageSourceKernelDerivativeSet_basis_smul_mem
(h : finiteFoxStageTargetQuotient (X := X) N)
{v : finiteFoxStageCoordinateVector (X := X) N n}
(hv : v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n) :
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) h) • v ∈
finiteFoxStageSourceKernelDerivativeSet (X := X) N nThe source-kernel derivative set is stable under multiplication by target-group basis coefficients. This is the finite algebraic form of conjugating a relation by a chosen lift of a target quotient element.
Show proof
by
have hvRange : v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n := hv
exact finiteFoxStageRelationBoundaryRange_basis_smul_mem (X := X) N n h 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 finiteFoxStageKernelWordDerivativeSet_basis_smul_mem
(h : finiteFoxStageTargetQuotient (X := X) N)
{v : finiteFoxStageCoordinateVector (X := X) N n}
(hv : v ∈ finiteFoxStageKernelWordDerivativeSet (X := X) N n) :
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) h) • v ∈
finiteFoxStageKernelWordDerivativeSet (X := X) N nWord-level finite relation derivatives are stable under multiplication by target-group basis coefficients, after rewriting the source-kernel and word-level descriptions.
Show proof
by
rw [← finiteFoxStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet (X := X) N n]
rw [← finiteFoxStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet (X := X) N n] at hv
exact finiteFoxStageSourceKernelDerivativeSet_basis_smul_mem (X := X) N n h 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 finiteFoxStageRelationBoundaryExact_of_relationBoundaryModuleExact
[Fintype X]
(hexact : finiteFoxStageRelationBoundaryModuleExact (X := X) N n) :
finiteFoxStageRelationBoundaryExact (X := X) N nShow proof
finiteFoxStageRelationBoundaryExact_of_boundaryCyclesCoveredBySourceKernel
(X := X) N n
(finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact
(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.
□theorem finiteFoxStageSemiBoundaryCyclesCovered_of_relBoundaryModuleExact
[Fintype X]
(hexact : finiteFoxStageRelationBoundaryModuleExact (X := X) N n) :
finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N nShow proof
(finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff (X := X) N n).2
(finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact
(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.
□