FoxDifferential.Completed.FiniteStage.SourceCycleReduction
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
Imported by
def finiteFoxStageSourceBoundaryCycleSubmodule [Fintype X] :
Submodule (finiteFoxStageSourceGroupAlgebra (X := X) N n)
(finiteFoxStageSourceCoordinateVector (X := X) N n) :=
LinearMap.ker (finiteFoxStageSourceFoxBoundary (X := X) N n)Source boundary cycles in the source coordinate module.
theorem mem_finiteFoxStageSourceBoundaryCycleSubmodule [Fintype X]
{p : finiteFoxStageSourceCoordinateVector (X := X) N n} :
p ∈ finiteFoxStageSourceBoundaryCycleSubmodule (X := X) N n ↔
finiteFoxStageSourceFoxBoundary (X := X) N n p = 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 finiteFoxStageSourceCycleProjectionExact [Fintype X] : Prop :=
∀ p : finiteFoxStageSourceCoordinateVector (X := X) N n,
p ∈ finiteFoxStageSourceBoundaryCycleSubmodule (X := X) N n →
finiteFoxStageCoordinateSourceToTarget (X := X) N n p ∈
finiteFoxStageRelationBoundarySubmodule (X := X) N nSource-cycle projection exactness: every source Fox cycle maps to the target relation-boundary submodule. This is the source-quotient analogue of exactness before the relation-ideal correction.
def finiteFoxStageSourceBoundaryLeftRelationReduction [Fintype X] : Prop :=
∀ a : finiteFoxStageSourceCoordinateVector (X := X) N n,
finiteFoxStageSourceFoxBoundary (X := X) N n a ∈
finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n →
finiteFoxStageCoordinateSourceToTarget (X := X) N n a ∈
finiteFoxStageRelationBoundarySubmodule (X := X) N nLeft-submodule version of the source-boundary reduction.
theorem finiteFoxStageSourceBoundaryLeftRelationReduction_of_sourceCycleProjectionExact
[Fintype X]
(hcycle : finiteFoxStageSourceCycleProjectionExact (X := X) N n) :
finiteFoxStageSourceBoundaryLeftRelationReduction (X := X) N nSource-cycle projection exactness implies the reduction for the left relation-augmentation submodule, because elements of the left relation-augmentation submodule have explicit relation-compatible primitives.
Show proof
by
intro a ha
rcases finiteFoxStageSourceBoundaryPrimitive_of_mem_relationAugmentationLeftSubmodule
(X := X) N n ha with ⟨p, hpboundary, hprel⟩
have hcycle_ap :
a - p ∈ finiteFoxStageSourceBoundaryCycleSubmodule (X := X) N n := by
change finiteFoxStageSourceFoxBoundary (X := X) N n (a - p) = 0
rw [map_sub, hpboundary]
exact sub_self _
have haprel := hcycle (a - p) hcycle_ap
have hmap :
finiteFoxStageCoordinateSourceToTarget (X := X) N n a =
finiteFoxStageCoordinateSourceToTarget (X := X) N n p +
finiteFoxStageCoordinateSourceToTarget (X := X) N n (a - p) := by
have hsub := map_sub (finiteFoxStageCoordinateSourceToTarget (X := X) N n) a p
calc
finiteFoxStageCoordinateSourceToTarget (X := X) N n a =
finiteFoxStageCoordinateSourceToTarget (X := X) N n p +
(finiteFoxStageCoordinateSourceToTarget (X := X) N n a -
finiteFoxStageCoordinateSourceToTarget (X := X) N n p) := by
abel
_ = finiteFoxStageCoordinateSourceToTarget (X := X) N n p +
finiteFoxStageCoordinateSourceToTarget (X := X) N n (a - p) := by
rw [← hsub]
rw [hmap]
exact (finiteFoxStageRelationBoundarySubmodule (X := X) N n).add_mem hprel haprelProof. 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 finiteFoxStageSourceBoundaryRelationIdealReduction_of_relationIdeal_le_leftSubmodule
[Fintype X]
(hideal_left :
∀ x : finiteFoxStageSourceGroupAlgebra (X := X) N n,
x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N n →
x ∈ finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n)
(hcycle : finiteFoxStageSourceCycleProjectionExact (X := X) N n) :
finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N nIf the two-sided relation augmentation ideal is already generated by the same relation augmentation elements as a left source-submodule, source-cycle projection exactness implies the source-boundary relation-ideal reduction used in the finite-stage exactness file.
Show proof
by
intro a ha
exact finiteFoxStageSourceBoundaryLeftRelationReduction_of_sourceCycleProjectionExact
(X := X) N n hcycle a (hideal_left _ ha)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_relIdealLeftGen_and_sourceCycleProjExact
[Fintype X]
(hideal_left :
∀ x : finiteFoxStageSourceGroupAlgebra (X := X) N n,
x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N n →
x ∈ finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n)
(hcycle : finiteFoxStageSourceCycleProjectionExact (X := X) N n) :
finiteFoxStageRelationBoundaryModuleExact (X := X) N nFinite-stage source-cycle projection exactness gives relation-boundary module exactness.
Show proof
finiteFoxStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
(X := X) N n
(finiteFoxStageSourceBoundaryRelationIdealReduction_of_relationIdeal_le_leftSubmodule
(X := X) N n hideal_left hcycle)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 finiteFoxStageBoundaryCyclesCovered_of_relIdealLeftGen_and_sourceCycleProjExact
[Fintype X]
(hideal_left :
∀ x : finiteFoxStageSourceGroupAlgebra (X := X) N n,
x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N n →
x ∈ finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n)
(hcycle : finiteFoxStageSourceCycleProjectionExact (X := X) N n) :
finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N nThe same inputs give finite coordinate coverage.
Show proof
finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact
(X := X) N n
(finiteFoxStageRelationBoundaryModuleExact_of_relIdealLeftGen_and_sourceCycleProjExact
(X := X) N n hideal_left hcycle)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_relIdealLeftGen_and_sourceCycleProjExact
[Fintype X]
(hideal_left :
∀ x : finiteFoxStageSourceGroupAlgebra (X := X) N n,
x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N n →
x ∈ finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n)
(hcycle : finiteFoxStageSourceCycleProjectionExact (X := X) N n) :
finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N nRelation-ideal left generation together with exactness of the source-cycle projection covers the finite semidirect boundary cycles.
Show proof
finiteFoxStageSemiBoundaryCyclesCovered_of_sourceBoundaryRelReduction
(X := X) N n
(finiteFoxStageSourceBoundaryRelationIdealReduction_of_relationIdeal_le_leftSubmodule
(X := X) N n hideal_left hcycle)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.
□