FoxDifferential.Completed.FiniteStage.Stage.KernelIdeal
This module develops the augmentation side of the construction. It identifies the relevant kernels and ideals and compares the finite-stage and completed forms.
theorem finiteFoxStageSourceGeneratorSubOne_mem_sourceAugmentationIdeal
(i : X) :
MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(FreeGroup.of i)) - 1 ∈
finiteFoxStageSourceAugmentationIdeal (X := X) N nThe finite-stage source generator \([x_i]-1\) belongs to the source augmentation ideal.
Show proof
by
rw [mem_finiteFoxStageSourceAugmentationIdeal]
rw [map_sub,
finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient,
map_one, 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 finiteFoxStageGroupAlgebraMapKernel_mem_mulAugmentation_of_derivatives_eq_zero
[Finite X]
{x : finiteFoxStageSourceGroupAlgebra (X := X) N n}
(hderivative :
∀ i : X, finiteFoxStageGroupAlgebraDerivative (X := X) N n i x = 0)
(haugmentation :
finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N n x = 0) :
x ∈ finiteFoxStageGroupAlgebraMapKernelMulAugmentationIdeal (X := X) N nShow proof
by
classical
letI := Fintype.ofFinite X
have hcoeff_mem
(i : X) :
finiteFoxStageSourceGroupAlgebraDerivative (X := X) N n i x ∈
finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N n := by
rw [mem_finiteFoxStageGroupAlgebraMapKernelIdeal]
rw [finiteFoxStageSourceGroupAlgebraDerivative_map]
exact hderivative i
have hformula :=
finiteFoxStageSourceGroupAlgebraDerivative_groupAlgebra_fundamental_formula
(X := X) (N := N) (n := n) x
have hx_sum :
x =
∑ i : X,
finiteFoxStageSourceGroupAlgebraDerivative (X := X) N n i x *
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(FreeGroup.of i)) - 1) := by
calc
x =
x -
algebraMap (ModNCompletedCoeff n)
(finiteFoxStageSourceGroupAlgebra (X := X) N n) 0 := by
simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
Finsupp.single_zero, sub_zero]
_ =
x -
algebraMap (ModNCompletedCoeff n)
(finiteFoxStageSourceGroupAlgebra (X := X) N n)
(finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N n x) := by
rw [haugmentation]
_ =
∑ i : X,
finiteFoxStageSourceGroupAlgebraDerivative (X := X) N n i x *
(MonoidAlgebra.of (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
(FreeGroup.of i)) - 1) := hformula
rw [hx_sum]
exact
(finiteFoxStageGroupAlgebraMapKernelMulAugmentationIdeal (X := X) N n).sum_mem
(fun i _ =>
Ideal.mul_mem_mul (hcoeff_mem i)
(finiteFoxStageSourceGeneratorSubOne_mem_sourceAugmentationIdeal
(X := X) N n i))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.
□