FoxDifferential.Completed.FiniteStage.SourceBoundary
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
import
abbrev finiteFoxStageSourceCoordinateVector : Type u :=
X → finiteFoxStageSourceGroupAlgebra (X := X) N nSource-valued coordinate vectors over \((\mathbb{Z}/n\mathbb{Z})[F/([N,N]N^n)]\).
def finiteFoxStageSourceFoxBoundary [Fintype X] :
finiteFoxStageSourceCoordinateVector (X := X) N n →ₗ[
finiteFoxStageSourceGroupAlgebra (X := X) N n]
finiteFoxStageSourceGroupAlgebra (X := X) N n where
toFun v :=
∑ i : X,
v i *
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(FreeGroup.of i)) - 1)
map_add' := by
intro v w
simp only [Pi.add_apply, QuotientGroup.mk'_apply, MonoidAlgebra.of_apply, add_mul, Finset.sum_add_distrib]
map_smul' := by
intro r v
simp only [Pi.smul_apply, smul_eq_mul, QuotientGroup.mk'_apply, MonoidAlgebra.of_apply, mul_assoc,
RingHom.id_apply, Finset.mul_sum]The source Fox boundary/Euler map \(a \mapsto \sum_i a_i([x_i]-1)\) over the source quotient.
theorem finiteFoxStageSourceFoxBoundary_apply [Fintype X]
(v : finiteFoxStageSourceCoordinateVector (X := X) N n) :
finiteFoxStageSourceFoxBoundary (X := X) N n v =
∑ i : X,
v i *
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(FreeGroup.of i)) - 1)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.
□def finiteFoxStageCoordinateSourceToTarget :
finiteFoxStageSourceCoordinateVector (X := X) N n →ₗ[ModNCompletedCoeff n]
finiteFoxStageCoordinateVector (X := X) N n where
toFun v := fun i =>
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (v i)
map_add' := by
intro v w
funext i
simp only [Pi.add_apply, map_add]
map_smul' := by
intro a v
funext i
simp only [Pi.smul_apply, finiteFoxCommutatorPowerGroupAlgebraMap_smul, RingHom.id_apply]Apply the finite source-to-target group-algebra map coordinatewise.
theorem finiteFoxStageCoordinateSourceToTarget_apply
(v : finiteFoxStageSourceCoordinateVector (X := X) N n) (i : X) :
finiteFoxStageCoordinateSourceToTarget (X := X) N n v i =
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (v i)The finite-stage source-to-target coordinate map is evaluated by applying the target quotient map to the chosen coordinate.
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_coordinateSourceToTarget
[Fintype X]
(v : finiteFoxStageSourceCoordinateVector (X := X) N n) :
finiteFoxStageFoxBoundary (X := X) N n
(finiteFoxStageCoordinateSourceToTarget (X := X) N n v) =
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(finiteFoxStageSourceFoxBoundary (X := X) N n v)The source boundary commutes with the source-to-target group-algebra map.
Show proof
by
rw [finiteFoxStageFoxBoundary_apply, finiteFoxStageSourceFoxBoundary_apply]
rw [map_sum]
apply Finset.sum_congr rfl
intro i hi
rw [finiteFoxStageCoordinateSourceToTarget_apply, RingHom.map_mul, map_sub, map_one,
finiteFoxCommutatorPowerGroupAlgebraMap_of]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 finiteFoxStageCoordinateSourceToTarget_surjective :
Function.Surjective (finiteFoxStageCoordinateSourceToTarget (X := X) N n)The finite-stage coordinatewise source-to-target map is surjective.
Show proof
by
intro v
have hcoord : ∀ i : X,
∃ a : finiteFoxStageSourceGroupAlgebra (X := X) N n,
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n a = v i := by
intro i
exact finiteFoxCommutatorPowerGroupAlgebraMap_surjective (X := X) N n (v i)
choose a ha using hcoord
refine ⟨a, ?_⟩
funext i
exact ha iProof. 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 finiteFoxStageSourceFoxBoundary_mem_groupAlgebraMapKernel_of_lift_cycle
[Fintype X]
{v : finiteFoxStageCoordinateVector (X := X) N n}
{a : finiteFoxStageSourceCoordinateVector (X := X) N n}
(ha : finiteFoxStageCoordinateSourceToTarget (X := X) N n a = v)
(hv : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n) :
finiteFoxStageSourceFoxBoundary (X := X) N n a ∈
finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N nIf a source coordinate vector lifts a target boundary cycle, then its source boundary lies in the source-to-target group-algebra kernel.
Show proof
by
rw [mem_finiteFoxStageGroupAlgebraMapKernelIdeal]
calc
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(finiteFoxStageSourceFoxBoundary (X := X) N n a) =
finiteFoxStageFoxBoundary (X := X) N n
(finiteFoxStageCoordinateSourceToTarget (X := X) N n a) := by
exact (finiteFoxStageFoxBoundary_coordinateSourceToTarget (X := X) N n a).symm
_ = finiteFoxStageFoxBoundary (X := X) N n v := by
rw [ha]
_ = 0 := 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 finiteFoxStageSourceFoxBoundary_mem_relationAugmentationIdeal_of_lift_cycle
[Fintype X]
{v : finiteFoxStageCoordinateVector (X := X) N n}
{a : finiteFoxStageSourceCoordinateVector (X := X) N n}
(ha : finiteFoxStageCoordinateSourceToTarget (X := X) N n a = v)
(hv : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n) :
finiteFoxStageSourceFoxBoundary (X := X) N n a ∈
finiteFoxStageRelationAugmentationIdeal (X := X) N nIf a source coordinate vector lifts a target boundary cycle, then its source boundary lies in the explicit relation augmentation ideal.
Show proof
by
rw [← finiteFoxStage_mem_groupAlgebraMapKernelIdeal_iff_relationAugmentationIdeal (X := X) N n]
exact finiteFoxStageSourceFoxBoundary_mem_groupAlgebraMapKernel_of_lift_cycle
(X := X) N n ha 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 exists_finiteFoxStageSourceCoordinate_lift_boundaryCycle_relationIdeal
[Fintype X]
(v : finiteFoxStageCoordinateVector (X := X) N n)
(hv : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n) :
∃ a : finiteFoxStageSourceCoordinateVector (X := X) N n,
finiteFoxStageCoordinateSourceToTarget (X := X) N n a = v ∧
finiteFoxStageSourceFoxBoundary (X := X) N n a ∈
finiteFoxStageRelationAugmentationIdeal (X := X) N nEvery finite target boundary cycle has a source-coordinate lift whose source boundary is in the relation augmentation ideal.
Show proof
by
rcases finiteFoxStageCoordinateSourceToTarget_surjective (X := X) N n v with ⟨a, ha⟩
exact ⟨a, ha,
finiteFoxStageSourceFoxBoundary_mem_relationAugmentationIdeal_of_lift_cycle
(X := X) N n ha 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.
□def finiteFoxStageSourceBoundaryRelationIdealReduction [Fintype X] : Prop :=
∀ a : finiteFoxStageSourceCoordinateVector (X := X) N n,
finiteFoxStageSourceFoxBoundary (X := X) N n a ∈
finiteFoxStageRelationAugmentationIdeal (X := X) N n →
finiteFoxStageCoordinateSourceToTarget (X := X) N n a ∈
finiteFoxStageRelationBoundarySubmodule (X := X) N nSource-boundary relation-ideal reduction: if every source coordinate vector whose source boundary lies in the relation augmentation ideal projects to a relation-boundary vector, then the finite-stage coordinate complex is exact.
theorem finiteFoxStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
[Fintype X]
(hreduce : finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N n) :
finiteFoxStageRelationBoundaryModuleExact (X := X) N nThe source-boundary relation-ideal reduction implies finite-stage module exactness.
Show proof
by
intro v hv
rcases exists_finiteFoxStageSourceCoordinate_lift_boundaryCycle_relationIdeal
(X := X) N n v hv with ⟨a, ha, hboundary⟩
have hrel := hreduce a hboundary
simpa [ha] using hrelProof. 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 finiteFoxStageBoundaryCyclesCovered_of_sourceBoundaryRelReduction
[Fintype X]
(hreduce : finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N n) :
finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N nThe source-boundary relation-ideal reduction implies finite-stage coordinate coverage.
Show proof
finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact
(X := X) N n
(finiteFoxStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
(X := X) N n hreduce)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_inj_of_sourceBoundaryRelReduction
[Fintype X]
(hreduce : finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N n) :
Function.Injective (finiteFoxStageBoundaryModuloRelations (X := X) N n)The source-boundary relation-ideal reduction gives injectivity of the finite quotient obstruction boundary.
Show proof
finiteFoxStageBoundaryModuloRelations_injective_of_relationBoundaryModuleExact
(X := X) N n
(finiteFoxStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
(X := X) N n hreduce)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_sourceBoundaryRelReduction
[Fintype X]
(hreduce : finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N n) :
finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N nThe source-boundary relation-ideal reduction gives the finite semidirect coverage statement.
Show proof
(finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff (X := X) N n).2
(finiteFoxStageBoundaryCyclesCovered_of_sourceBoundaryRelReduction
(X := X) N n hreduce)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.
□