FoxDifferential.Completed.FiniteStage.CoeffMap.Target
Fox Differential / Completed / Finite Stage / Coefficient Map / Target.
def finiteFoxStageTargetGroupAlgebraCoeffMap
(N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) :
finiteFoxStageTargetGroupAlgebra (X := X) N m₀ →+*
finiteFoxStageTargetGroupAlgebra (X := X) N n₀ :=
modNCompletedGroupRingCoeffMap
(n := n₀) (m := m₀) (finiteFoxStageTargetQuotient (X := X) N) hnmCoefficient-reduction map on finite-stage target group algebras for a divisor \(n \mid m\).
theorem finiteFoxStageTargetGroupAlgebraCoeffMap_of
(N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) (w : FreeGroup X) :
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm
(MonoidAlgebra.of (ModNCompletedCoeff m₀)
(finiteFoxStageTargetQuotient (X := X) N) (QuotientGroup.mk' N w)) =
MonoidAlgebra.of (ModNCompletedCoeff n₀)
(finiteFoxStageTargetQuotient (X := X) N) (QuotientGroup.mk' N w)Evaluation of target coefficient reduction on a represented quotient word.
Show proof
by
simpa [finiteFoxStageTargetGroupAlgebraCoeffMap] using
(modNCompletedGroupRingCoeffMap_of
(n := n₀) (m := m₀)
(H := finiteFoxStageTargetQuotient (X := X) N) hnm (QuotientGroup.mk' N w))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 finiteFoxStageTargetGroupAlgebraCoeffMap_of_quotient
(N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
(q : finiteFoxStageTargetQuotient (X := X) N) :
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm
(MonoidAlgebra.of (ModNCompletedCoeff m₀)
(finiteFoxStageTargetQuotient (X := X) N) q) =
MonoidAlgebra.of (ModNCompletedCoeff n₀)
(finiteFoxStageTargetQuotient (X := X) N) qEvaluation of target coefficient reduction on a quotient basis element.
Show proof
by
rcases QuotientGroup.mk'_surjective N q with ⟨w, rfl⟩
exact finiteFoxStageTargetGroupAlgebraCoeffMap_of (X := X) N hnm wProof. 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 finiteFoxStageTargetGroupAlgebraCoeffMap_single_apply
(N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
(q : finiteFoxStageTargetQuotient (X := X) N)
(a : ModNCompletedCoeff m₀) :
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm
(MonoidAlgebra.single q a) =
MonoidAlgebra.single q (modNCompletedCoeffMap (n := n₀) (m := m₀) hnm a)The coefficient-change map is evaluated coordinatewise: the support in the finite quotient is unchanged and every coefficient is carried through the given ring homomorphism.
Show proof
by
letI : Algebra (ModNCompletedCoeff m₀) (ModNCompletedCoeff n₀) :=
ZMod.algebra' (R := ModNCompletedCoeff n₀) (m := n₀) (n := m₀) hnm
have hcoeff :
algebraMap (ModNCompletedCoeff m₀) (ModNCompletedCoeff n₀) a =
modNCompletedCoeffMap (n := n₀) (m := m₀) hnm a := by
rfl
rw [finiteFoxStageTargetGroupAlgebraCoeffMap]
ext r
simp only [modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, MonoidAlgebra.single, RingHom.coe_coe,
MonoidAlgebra.lift_single, MonoidAlgebra.of_apply, Algebra.smul_def, MonoidAlgebra.coe_algebraMap,
Function.comp_apply, hcoeff, MonoidAlgebra.single_mul_single, one_mul, mul_one]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 finiteFoxStageTargetGroupAlgebraCoeffMap_eq_mapRange
(N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) :
(finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm).toAddMonoidHom =
(Finsupp.mapRange.addMonoidHom
(modNCompletedCoeffMap (n := n₀) (m := m₀) hnm).toAddMonoidHom :
finiteFoxStageTargetGroupAlgebra (X := X) N m₀ →+
finiteFoxStageTargetGroupAlgebra (X := X) N n₀)Target coefficient reduction is the finsupp map-range operation on coefficients.
Show proof
by
apply Finsupp.addHom_ext
intro q a
change
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm
(MonoidAlgebra.single q a) =
(Finsupp.mapRange.addMonoidHom
(modNCompletedCoeffMap (n := n₀) (m := m₀) hnm).toAddMonoidHom :
finiteFoxStageTargetGroupAlgebra (X := X) N m₀ →+
finiteFoxStageTargetGroupAlgebra (X := X) N n₀)
(Finsupp.single q a)
rw [finiteFoxStageTargetGroupAlgebraCoeffMap_single_apply]
simp only [Finsupp.mapRange.addMonoidHom, RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.coe_coe,
AddMonoidHom.coe_mk, ZeroHom.coe_mk, Finsupp.mapRange_single]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 finiteFoxStageTargetGroupAlgebraCoeffMap_apply
(N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
(x : finiteFoxStageTargetGroupAlgebra (X := X) N m₀)
(q : finiteFoxStageTargetQuotient (X := X) N) :
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm x q =
modNCompletedCoeffMap (n := n₀) (m := m₀) hnm (x q)The coefficient-change map is evaluated coordinatewise: the support in the finite quotient is unchanged and every coefficient is carried through the given ring homomorphism.
Show proof
by
have h :=
DFunLike.congr_fun
(finiteFoxStageTargetGroupAlgebraCoeffMap_eq_mapRange
(X := X) N hnm) x
simpa [Finsupp.mapRange] using congrArg (fun y => y q) hProof. 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 finiteFoxStageTargetGroupAlgebraCoeffMap_rfl
(N : Subgroup (FreeGroup X)) [N.Normal] :
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) (n₀ := n₀) (m₀ := n₀) N dvd_rfl =
RingHom.id _Target coefficient reduction is the identity map when the modulus is unchanged.
Show proof
by
apply RingHom.ext
intro x
refine MonoidAlgebra.induction_on
(p := fun x =>
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) (n₀ := n₀) (m₀ := n₀) N
dvd_rfl x = x)
x ?_ ?_ ?_
· intro q
rcases QuotientGroup.mk'_surjective N q with ⟨w, rfl⟩
rw [finiteFoxStageTargetGroupAlgebraCoeffMap_of]
· intro x y hx hy
simp only [RingHom.map_add, hx, hy]
· intro a x hx
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
rw [Algebra.smul_def, RingHom.map_mul, hx]
simp only [finiteFoxStageTargetGroupAlgebraCoeffMap, modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe,
map_intCast]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 finiteFoxStageTargetGroupAlgebraCoeffMap_comp
{k₀ : ℕ}
(N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) (hmk : m₀ ∣ k₀) :
(finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm).comp
(finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hmk) =
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N (dvd_trans hnm hmk)Target coefficient reductions compose along divisibility.
Show proof
by
apply RingHom.ext
intro x
refine MonoidAlgebra.induction_on
(p := fun x =>
((finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hnm).comp
(finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N hmk)) x =
finiteFoxStageTargetGroupAlgebraCoeffMap (X := X) N (dvd_trans hnm hmk) x)
x ?_ ?_ ?_
· intro q
rcases QuotientGroup.mk'_surjective N q with ⟨w, rfl⟩
rw [RingHom.comp_apply, finiteFoxStageTargetGroupAlgebraCoeffMap_of,
finiteFoxStageTargetGroupAlgebraCoeffMap_of, finiteFoxStageTargetGroupAlgebraCoeffMap_of]
· intro x y hx hy
simp only [RingHom.map_add, hx, hy]
· intro a x hx
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
simp only [finiteFoxStageTargetGroupAlgebraCoeffMap, modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe,
map_intCast, RingHom.coe_coe]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.
□