FoxDifferential.Completed.FiniteStage.BoundarySubgroups
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
def finiteFoxStageSemidirectBoundaryCycleSubgroup [Fintype X] :
Subgroup (FiniteFoxStageSemidirect (X := X) N n) where
carrier := finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n
one_mem' := by
constructor
· simp only [FiniteFoxStageSemidirect.one_right]
· exact (finiteFoxStageBoundaryCycleSubmodule (X := X) N n).zero_mem
mul_mem' := by
intro y z hy hz
rcases hy with ⟨hyright, hyleft⟩
rcases hz with ⟨hzright, hzleft⟩
constructor
· simp only [FiniteFoxStageSemidirect.mul_right, hyright, hzright, mul_one]
· rw [FiniteFoxStageSemidirect.mul_left, hyright]
have hone :
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) 1 :
finiteFoxStageTargetGroupAlgebra (X := X) N n) = 1 := by
simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]
rw [hone, one_smul]
exact (finiteFoxStageBoundaryCycleSubmodule (X := X) N n).add_mem hyleft hzleft
inv_mem' := by
intro y hy
rcases hy with ⟨hyright, hyleft⟩
constructor
· simp only [FiniteFoxStageSemidirect.inv_right, hyright, inv_one]
· rw [FiniteFoxStageSemidirect.inv_left, hyright, inv_one]
have hone :
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) 1 :
finiteFoxStageTargetGroupAlgebra (X := X) N n) = 1 := by
simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]
rw [hone, one_smul]
exact (finiteFoxStageBoundaryCycleSubmodule (X := X) N n).neg_mem hyleftFinite semidirect boundary cycles form a subgroup.
theorem finiteFoxStageSemidirectBoundaryCycleSubgroup_coe [Fintype X] :
((finiteFoxStageSemidirectBoundaryCycleSubgroup (X := X) N n :
Subgroup (FiniteFoxStageSemidirect (X := X) N n)) :
Set (FiniteFoxStageSemidirect (X := X) N n)) =
finiteFoxStageSemidirectBoundaryCycleSet (X := X) N nThe boundary-cycle subgroup of the finite Fox semidirect product has the boundary-cycle set as its underlying set.
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 finiteFoxStageSemidirectSourceKernelDerivativeSet_iff
{y : FiniteFoxStageSemidirect (X := X) N n} :
y ∈ finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n ↔
y.right = 1 ∧
y.left ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N nSource-kernel semidirect points are exactly points with right component \(1\) and left component in the source-kernel derivative subgroup.
Show proof
by
constructor
· rintro ⟨q, hq, hqy⟩
rw [← hqy]
exact ⟨rfl, ⟨q, hq, rfl⟩⟩
· rintro ⟨hyright, q, hq, hqleft⟩
refine ⟨q, hq, ?_⟩
apply FiniteFoxStageSemidirect.ext
· exact hqleft
· simpa [finiteFoxStageSemidirectSourceKernelPoint] using hyright.symmProof. 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 finiteFoxStageSemidirectSourceKernelDerivativeSubgroup :
Subgroup (FiniteFoxStageSemidirect (X := X) N n) where
carrier :=
{ y | y.right = 1 ∧
y.left ∈ finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n }
one_mem' := by
exact ⟨rfl, (finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n).zero_mem⟩
mul_mem' := by
intro y z hy hz
rcases hy with ⟨hyright, hyleft⟩
rcases hz with ⟨hzright, hzleft⟩
constructor
· simp only [FiniteFoxStageSemidirect.mul_right, hyright, hzright, mul_one]
· rw [FiniteFoxStageSemidirect.mul_left, hyright]
have hone :
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) 1 :
finiteFoxStageTargetGroupAlgebra (X := X) N n) = 1 := by
simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]
rw [hone, one_smul]
exact
(finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n).add_mem hyleft hzleft
inv_mem' := by
intro y hy
rcases hy with ⟨hyright, hyleft⟩
constructor
· simp only [FiniteFoxStageSemidirect.inv_right, hyright, inv_one]
· rw [FiniteFoxStageSemidirect.inv_left, hyright, inv_one]
have hone :
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) 1 :
finiteFoxStageTargetGroupAlgebra (X := X) N n) = 1 := by
simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]
rw [hone, one_smul]
exact (finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n).neg_mem hyleft
@[simp]Finite source-kernel derivative semidirect points form a subgroup.
theorem finiteFoxStageSemidirectSourceKernelDerivativeSubgroup_coe :
((finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :
Subgroup (FiniteFoxStageSemidirect (X := X) N n)) :
Set (FiniteFoxStageSemidirect (X := X) N n)) =
finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N nThe finite-stage semidirect source-kernel derivative subgroup coerces to its defining carrier.
Show proof
by
ext y
change
(y.right = 1 ∧
y.left ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n) ↔
y ∈ finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n
exact (finiteFoxStageSemidirectSourceKernelDerivativeSet_iff (X := X) N n).symmProof. 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 finiteFoxStageSemidirectSourceKernelDerivativeSubgroup_le_boundaryCycleSubgroup
[Fintype X] :
finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n ≤
finiteFoxStageSemidirectBoundaryCycleSubgroup (X := X) N nShow proof
by
intro y hy
have hyset :
y ∈ finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n := by
have hy' :
y ∈ ((finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :
Subgroup (FiniteFoxStageSemidirect (X := X) N n)) :
Set (FiniteFoxStageSemidirect (X := X) N n)) := hy
rw [finiteFoxStageSemidirectSourceKernelDerivativeSubgroup_coe (X := X) N n] at hy'
exact hy'
exact finiteFoxStageSemidirectSourceKernelDerivativeSet_subset_boundaryCycleSet
(X := X) N n hysetProof. 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 finiteFoxStageSemiBoundaryCycleSubgroup_le_sourceKernelDerivSubgroup_iff_coord
[Fintype X] :
finiteFoxStageSemidirectBoundaryCycleSubgroup (X := X) N n ≤
finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n ↔
finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N nSemidirect finite-stage coverage is equivalently subgroup inclusion.
Show proof
by
constructor
· intro hsub
exact
(finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff (X := X) N n).1
(by
intro y hy
have hy' : y ∈ finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :=
hsub hy
have hyset :
y ∈ ((finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :
Subgroup (FiniteFoxStageSemidirect (X := X) N n)) :
Set (FiniteFoxStageSemidirect (X := X) N n)) := hy'
rw [finiteFoxStageSemidirectSourceKernelDerivativeSubgroup_coe (X := X) N n] at hyset
exact hyset)
· intro hcoord y hy
have hyset :
y ∈ finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n :=
(finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff (X := X) N n).2
hcoord hy
change
y ∈ ((finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :
Subgroup (FiniteFoxStageSemidirect (X := X) N n)) :
Set (FiniteFoxStageSemidirect (X := X) N n))
rw [finiteFoxStageSemidirectSourceKernelDerivativeSubgroup_coe (X := X) N n]
exact hysetProof. 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.
□