FoxDifferential.Completed.FiniteStage.CoeffMap.Augmentation
Fox Differential / Completed / Finite Stage / Coefficient Map / Augmentation.
theorem finiteFoxCommutatorPowerSourceGAAugmentation_powerSourceGAMap
(N : Subgroup (FreeGroup X)) (hnm : n₀ ∣ m₀)
(x : finiteFoxStageSourceGroupAlgebra (X := X) N m₀) :
finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N n₀
(finiteFoxStagePowerSourceGroupAlgebraMap (X := X) N hnm x) =
modNCompletedCoeffMap (n := n₀) (m := m₀) hnm
(finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N m₀ x)Source augmentation commutes with finite-stage coefficient/source reduction.
Show proof
by
refine MonoidAlgebra.induction_on
(p := fun x =>
finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N n₀
(finiteFoxStagePowerSourceGroupAlgebraMap (X := X) N hnm x) =
modNCompletedCoeffMap (n := n₀) (m := m₀) hnm
(finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N m₀ x))
x ?_ ?_ ?_
· intro q
rcases QuotientGroup.mk'_surjective
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N m₀) q with ⟨w, rfl⟩
rw [finiteFoxStagePowerSourceGroupAlgebraMap_of,
finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient,
finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient]
exact (map_one (modNCompletedCoeffMap (n := n₀) (m := m₀) hnm)).symm
· intro x y hx hy
simp only [map_add, hx, hy]
· intro a x hx
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
rw [Algebra.smul_def]
change
((finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N n₀).toRingHom.comp
(finiteFoxStagePowerSourceGroupAlgebraMap (X := X) N hnm))
(algebraMap (ModNCompletedCoeff m₀)
(finiteFoxStageSourceGroupAlgebra (X := X) N m₀)
(t : ModNCompletedCoeff m₀) * x) =
((modNCompletedCoeffMap (n := n₀) (m := m₀) hnm).comp
(finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N m₀).toRingHom)
(algebraMap (ModNCompletedCoeff m₀)
(finiteFoxStageSourceGroupAlgebra (X := X) N m₀)
(t : ModNCompletedCoeff m₀) * x)
rw [RingHom.map_mul, RingHom.map_mul]
have hx' :
((finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N n₀).toRingHom.comp
(finiteFoxStagePowerSourceGroupAlgebraMap (X := X) N hnm)) x =
((modNCompletedCoeffMap (n := n₀) (m := m₀) hnm).comp
(finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N m₀).toRingHom) x := by
simpa [RingHom.comp_apply] using hx
rw [hx']
have hcoeff :
((finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N n₀).toRingHom.comp
(finiteFoxStagePowerSourceGroupAlgebraMap (X := X) N hnm))
(algebraMap (ModNCompletedCoeff m₀)
(finiteFoxStageSourceGroupAlgebra (X := X) N m₀)
(t : ModNCompletedCoeff m₀)) =
((modNCompletedCoeffMap (n := n₀) (m := m₀) hnm).comp
(finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N m₀).toRingHom)
(algebraMap (ModNCompletedCoeff m₀)
(finiteFoxStageSourceGroupAlgebra (X := X) N m₀)
(t : ModNCompletedCoeff m₀)) := by
simp only [finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation, AlgHom.toRingHom_eq_coe,
finiteFoxStagePowerSourceGroupAlgebraMap, finiteFoxStageSameSourceGroupAlgebraCoeffMap,
modNCompletedGroupRingCoeffMap, MonoidAlgebra.mapDomainRingHom, finiteFoxStagePowerSourceQuotientMap, map_intCast,
modNCompletedCoeffMap]
rw [hcoeff]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.
□