FoxDifferential.Completed.FiniteStage.RelationAction
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
def finiteFoxStageRelationConjBySource
(s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(q : finiteFoxStageRelationGroup (X := X) N n) :
finiteFoxStageRelationGroup (X := X) N n :=
⟨s * q.1 * s⁻¹, by
change finiteFoxCommutatorPowerQuotientMapToNormalQuotient
(F := FreeGroup X) N n (s * q.1 * s⁻¹) = 1
rw [map_mul, map_mul, map_inv, q.2]
simp only [mul_one, mul_inv_cancel]⟩theorem finiteFoxStageRelationConjBySource_val
(s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(q : finiteFoxStageRelationGroup (X := X) N n) :
(finiteFoxStageRelationConjBySource (X := X) N n s q).1 = s * q.1 * s⁻¹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 finiteFoxStageRelationBoundary_conjBySource
(s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(q : finiteFoxStageRelationGroup (X := X) N n) :
finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n
(Additive.ofMul (finiteFoxStageRelationConjBySource (X := X) N n s q)) =
finiteFoxStageQuotientCoefficient (X := X) N n s •
finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q)Relation-boundary equivariance for conjugation by a source-quotient element.
Show proof
by
rw [finiteFoxStageRelationBoundaryAddMonoidHom_of,
finiteFoxStageRelationBoundaryAddMonoidHom_of,
finiteFoxStageRelationConjBySource_val]
have hconj :=
IsCrossedDifferential.conj
(finiteFoxStageQuotientDerivativeVector_isCrossedDifferential (X := X) N n)
s q.1
have hcoeff :
finiteFoxStageQuotientCoefficient (X := X) N n (s * q.1 * s⁻¹) = 1 := by
have htarget :
finiteFoxCommutatorPowerQuotientMapToNormalQuotient
(F := FreeGroup X) N n (s * q.1 * s⁻¹) = 1 := by
rw [map_mul, map_mul, map_inv, q.2]
simp only [mul_one, mul_inv_cancel]
rw [finiteFoxStageQuotientCoefficient_apply, htarget]
rfl
calc
finiteFoxStageQuotientDerivativeVector (X := X) N n (s * q.1 * s⁻¹) =
finiteFoxStageQuotientDerivativeVector (X := X) N n s +
finiteFoxStageQuotientCoefficient (X := X) N n s •
finiteFoxStageQuotientDerivativeVector (X := X) N n q.1 -
finiteFoxStageQuotientCoefficient (X := X) N n (s * q.1 * s⁻¹) •
finiteFoxStageQuotientDerivativeVector (X := X) N n s := hconj
_ = finiteFoxStageQuotientCoefficient (X := X) N n s •
finiteFoxStageQuotientDerivativeVector (X := X) N n q.1 := by
rw [hcoeff, one_smul]
abelProof. 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 finiteFoxStageTargetQuotientLiftToSource
(h : finiteFoxStageTargetQuotient (X := X) N) :
FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n :=
Classical.choose
(finiteFoxCommutatorPowerQuotientMapToNormalQuotient_surjective
(F := FreeGroup X) N n h)A chosen source-quotient lift of an element of \(F/N\).
theorem finiteFoxStageTargetQuotientLiftToSource_spec
(h : finiteFoxStageTargetQuotient (X := X) N) :
finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n
(finiteFoxStageTargetQuotientLiftToSource (X := X) N n h) = hThe chosen lift to the source quotient satisfies its finite-stage target specification.
Show proof
Classical.choose_spec
(finiteFoxCommutatorPowerQuotientMapToNormalQuotient_surjective
(F := FreeGroup X) N n h)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 finiteFoxStageQuotientCoefficient_targetLift
(h : finiteFoxStageTargetQuotient (X := X) N) :
finiteFoxStageQuotientCoefficient (X := X) N n
(finiteFoxStageTargetQuotientLiftToSource (X := X) N n h) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) hThe coefficient of a chosen source lift is the corresponding group-ring basis element.
Show proof
by
rw [finiteFoxStageQuotientCoefficient_apply,
finiteFoxStageTargetQuotientLiftToSource_spec]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 finiteFoxStageRelationBoundary_of_basis_smul
(h : finiteFoxStageTargetQuotient (X := X) N)
(q : finiteFoxStageRelationGroup (X := X) N n) :
finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n
(Additive.ofMul
(finiteFoxStageRelationConjBySource (X := X) N n
(finiteFoxStageTargetQuotientLiftToSource (X := X) N n h) q)) =
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) h) •
finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q)The relation boundary is equivariant on basis elements over \(\mathbb{Z}/n\mathbb{Z}[F/N]\).
Show proof
by
rw [finiteFoxStageRelationBoundary_conjBySource,
finiteFoxStageQuotientCoefficient_targetLift]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_basis_smul_mem
(h : finiteFoxStageTargetQuotient (X := X) N)
{v : finiteFoxStageCoordinateVector (X := X) N n}
(hv : v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n) :
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) h) • v ∈
finiteFoxStageRelationBoundaryRange (X := X) N nThe relation-boundary image is stable under multiplication by target group basis elements.
Show proof
by
rw [mem_finiteFoxStageRelationBoundaryRange_iff (X := X) N n] at hv
rcases hv with ⟨q, hq⟩
let qmul : finiteFoxStageRelationGroup (X := X) N n := Additive.toMul q
rw [mem_finiteFoxStageRelationBoundaryRange_iff (X := X) N n]
refine ⟨Additive.ofMul
(finiteFoxStageRelationConjBySource (X := X) N n
(finiteFoxStageTargetQuotientLiftToSource (X := X) N n h) qmul), ?_⟩
calc
finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n
(Additive.ofMul
(finiteFoxStageRelationConjBySource (X := X) N n
(finiteFoxStageTargetQuotientLiftToSource (X := X) N n h) qmul)) =
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) h) •
finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n
(Additive.ofMul qmul) := by
exact finiteFoxStageRelationBoundary_of_basis_smul (X := X) N n h qmul
_ = (MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) h) • v := by
have hqmul :
finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n
(Additive.ofMul qmul) = v := by
simpa [qmul] using hq
rw [hqmul]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.
□