FoxDifferential.Completed.FiniteStage.RelationIdeal
This module develops the augmentation side of the construction. It identifies the relevant kernels and ideals and compares the finite-stage and completed forms.
import
def finiteFoxStageRelationAugmentationGenerator
(q : finiteFoxStageRelationGroup (X := X) N n) :
finiteFoxStageSourceGroupAlgebra (X := X) N n :=
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q.1 - 1The augmentation generator \(q-1\) attached to a finite-stage relation \(q \in \ker(F/[N,N]N^n \to F/N)\).
def finiteFoxStageRelationAugmentationIdeal :
Ideal (finiteFoxStageSourceGroupAlgebra (X := X) N n) :=
Ideal.span
(Set.range (finiteFoxStageRelationAugmentationGenerator (X := X) N n))The source group-algebra ideal generated by finite-stage relation augmentation generators.
theorem finiteFoxStageRelationAugmentationGenerator_mem_relationAugmentationIdeal
(q : finiteFoxStageRelationGroup (X := X) N n) :
finiteFoxStageRelationAugmentationGenerator (X := X) N n q ∈
finiteFoxStageRelationAugmentationIdeal (X := X) N nA finite-stage relation augmentation generator belongs to the relation augmentation ideal.
Show proof
by
exact Ideal.subset_span ⟨q, rfl⟩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 finiteFoxStageRelationAugmentationGenerator_mem_groupAlgebraMapKernel
(q : finiteFoxStageRelationGroup (X := X) N n) :
finiteFoxStageRelationAugmentationGenerator (X := X) N n q ∈
finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N nA relation augmentation generator maps to zero in the target group algebra.
Show proof
by
rw [mem_finiteFoxStageGroupAlgebraMapKernelIdeal]
change finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q.1 - 1) = 0
rw [map_sub, map_one, finiteFoxCommutatorPowerGroupAlgebraMap_of_quotient,
finiteFoxStageRelationGroup_target_eq_one]
simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def, sub_self]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 finiteFoxStageRelationAugmentationIdeal_le_groupAlgebraMapKernel :
finiteFoxStageRelationAugmentationIdeal (X := X) N n ≤
finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N nThe generated relation augmentation ideal is contained in the kernel of the source-to-target finite group-algebra map.
Show proof
by
refine Ideal.span_le.2 ?_
rintro x ⟨q, rfl⟩
exact finiteFoxStageRelationAugmentationGenerator_mem_groupAlgebraMapKernel (X := X) N n qProof. 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 finiteFoxStageTargetGroupAlgebraSection :
finiteFoxStageTargetGroupAlgebra (X := X) N n →ₗ[ModNCompletedCoeff n]
finiteFoxStageSourceGroupAlgebra (X := X) N n :=
Finsupp.linearCombination (ModNCompletedCoeff n)
(fun h : finiteFoxStageTargetQuotient (X := X) N =>
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(finiteFoxStageTargetQuotientLiftToSource (X := X) N n h))A section of the source-to-target finite group-algebra map, obtained by choosing a source quotient lift for each target quotient basis element. This is only a \(\mathbb{Z}/n\mathbb{Z}\)-linear section; no multiplicativity is asserted.
theorem finiteFoxStageTargetGroupAlgebraSection_of
(h : finiteFoxStageTargetQuotient (X := X) N) :
finiteFoxStageTargetGroupAlgebraSection (X := X) N n
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) h) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(finiteFoxStageTargetQuotientLiftToSource (X := X) N n h)The finite-stage target group-algebra section sends a group-like quotient element to the chosen lifted group-like element.
Show proof
by
change
(Finsupp.linearCombination (ModNCompletedCoeff n)
(fun h : finiteFoxStageTargetQuotient (X := X) N =>
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(finiteFoxStageTargetQuotientLiftToSource (X := X) N n h)))
(Finsupp.single h (1 : ModNCompletedCoeff n)) = _
rw [Finsupp.linearCombination_single, one_smul]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 finiteFoxCommutatorPowerGroupAlgebraMap_section
(y : finiteFoxStageTargetGroupAlgebra (X := X) N n) :
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(finiteFoxStageTargetGroupAlgebraSection (X := X) N n y) = yThe chosen group-algebra section is a right inverse to the finite source-to-target map.
Show proof
by
classical
refine MonoidAlgebra.induction_on
(p := fun y : finiteFoxStageTargetGroupAlgebra (X := X) N n =>
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(finiteFoxStageTargetGroupAlgebraSection (X := X) N n y) = y)
y ?single ?add ?smul
· intro h
rw [finiteFoxStageTargetGroupAlgebraSection_of,
finiteFoxCommutatorPowerGroupAlgebraMap_of_quotient,
finiteFoxStageTargetQuotientLiftToSource_spec]
· intro x y hx hy
simp only [map_add, hx, hy]
· intro a x hx
rw [map_smul, finiteFoxCommutatorPowerGroupAlgebraMap_smul]
simp only [hx]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 finiteFoxCommutatorPowerGroupAlgebraMap_surjective :
Function.Surjective (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n)The finite source-to-target group-algebra map is surjective.
Show proof
by
intro y
exact ⟨finiteFoxStageTargetGroupAlgebraSection (X := X) N n y,
finiteFoxCommutatorPowerGroupAlgebraMap_section (X := X) N n y⟩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 finiteFoxStage_sourceBasis_sub_section_mem_relationAugmentationIdeal
(s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) s -
finiteFoxStageTargetGroupAlgebraSection (X := X) N n
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) s)) ∈
finiteFoxStageRelationAugmentationIdeal (X := X) N nA source basis element minus the chosen lift of its target image lies in the finite-stage relation augmentation ideal.
Show proof
by
let t : finiteFoxStageTargetQuotient (X := X) N :=
finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n s
let lift : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n :=
finiteFoxStageTargetQuotientLiftToSource (X := X) N n t
let q : finiteFoxStageRelationGroup (X := X) N n :=
⟨lift⁻¹ * s, by
change finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n
(lift⁻¹ * s) = 1
rw [map_mul, map_inv]
have hlift :
finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n lift = t := by
simp only [finiteFoxStageTargetQuotientLiftToSource_spec, lift, t]
rw [hlift]
simp only [inv_mul_cancel, t]⟩
have hsection :
finiteFoxStageTargetGroupAlgebraSection (X := X) N n
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) s)) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) lift := by
rw [finiteFoxCommutatorPowerGroupAlgebraMap_of_quotient,
finiteFoxStageTargetGroupAlgebraSection_of]
rw [hsection]
have hmul :
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) lift *
finiteFoxStageRelationAugmentationGenerator (X := X) N n q =
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) s -
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) lift := by
simp only [finiteFoxStageRelationAugmentationGenerator, q, MonoidAlgebra.of_apply]
rw [mul_sub, MonoidAlgebra.single_mul_single, mul_one]
simp only [mul_inv_cancel_left, mul_one]
rw [← hmul]
exact (finiteFoxStageRelationAugmentationIdeal (X := X) N n).mul_mem_left _
(finiteFoxStageRelationAugmentationGenerator_mem_relationAugmentationIdeal (X := X) N n q)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 finiteFoxStage_sub_section_map_mem_relationAugmentationIdeal
(x : finiteFoxStageSourceGroupAlgebra (X := X) N n) :
x - finiteFoxStageTargetGroupAlgebraSection (X := X) N n
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x) ∈
finiteFoxStageRelationAugmentationIdeal (X := X) N nEvery finite-stage source group-algebra element minus the chosen lift of its target image lies in the relation augmentation ideal.
Show proof
by
classical
refine MonoidAlgebra.induction_on
(p := fun x : finiteFoxStageSourceGroupAlgebra (X := X) N n =>
x - finiteFoxStageTargetGroupAlgebraSection (X := X) N n
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x) ∈
finiteFoxStageRelationAugmentationIdeal (X := X) N n)
x ?single ?add ?smul
· intro s
exact finiteFoxStage_sourceBasis_sub_section_mem_relationAugmentationIdeal (X := X) N n s
· intro x y hx hy
have hcalc :
x + y - finiteFoxStageTargetGroupAlgebraSection (X := X) N n
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (x + y)) =
(x - finiteFoxStageTargetGroupAlgebraSection (X := X) N n
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x)) +
(y - finiteFoxStageTargetGroupAlgebraSection (X := X) N n
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n y)) := by
rw [map_add, map_add]
abel
rw [hcalc]
exact (finiteFoxStageRelationAugmentationIdeal (X := X) N n).add_mem hx hy
· intro a x hx
have hcalc :
a • x - finiteFoxStageTargetGroupAlgebraSection (X := X) N n
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (a • x)) =
a • (x - finiteFoxStageTargetGroupAlgebraSection (X := X) N n
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x)) := by
rw [finiteFoxCommutatorPowerGroupAlgebraMap_smul, map_smul, smul_sub]
rw [hcalc]
rw [Algebra.smul_def]
exact (finiteFoxStageRelationAugmentationIdeal (X := X) N n).mul_mem_left _ hxProof. 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 finiteFoxStageGroupAlgebraMapKernelIdeal_eq_relationAugmentationIdeal :
finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N n =
finiteFoxStageRelationAugmentationIdeal (X := X) N nThe kernel ideal of the finite source-to-target group-algebra map is exactly the ideal spanned by relation augmentation generators.
Show proof
by
apply le_antisymm
· intro x hx
have hxmap :
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x = 0 :=
(mem_finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) (N := N) (n := n)).1 hx
have hdiff :=
finiteFoxStage_sub_section_map_mem_relationAugmentationIdeal (X := X) N n x
rw [hxmap, map_zero, sub_zero] at hdiff
exact hdiff
· exact finiteFoxStageRelationAugmentationIdeal_le_groupAlgebraMapKernel (X := X) N nProof. 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 finiteFoxStage_mem_groupAlgebraMapKernelIdeal_iff_relationAugmentationIdeal
{x : finiteFoxStageSourceGroupAlgebra (X := X) N n} :
x ∈ finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N n ↔
x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N nAt a finite Fox stage, membership in the source-to-target group-algebra map kernel ideal is equivalent to membership in the relation augmentation ideal.
Show proof
by
rw [finiteFoxStageGroupAlgebraMapKernelIdeal_eq_relationAugmentationIdeal]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.
□