English
For f,g : P.Hom P', and x,y ∈ P.Ring, the quantity f(xy) − g(xy) − (P'.σ(αx)(f(y) − g(y)) + P'.σ(αy)(f(x) − g(x))) lies in the square of the kernel of P'.ker.
Русский
Для отображений f,g и элементов x,y из P.Ring выражение, содержащее разности значений на произведении, принадлежит квадрату ядра.
LaTeX
$$$\\bigl(f.toAlgHom(xy) - g.toAlgHom(xy)\\bigr) - \\bigl(P'.\\sigma(\\mathit{algebraMap}(P.Ring S') x)\,(f(y) - g(y)) + P'.\\sigma(\\mathit{algebraMap}(P.Ring S') y)\,(f(x) - g(x))\\bigr) \\in (P'.ker)^2$$$
Lean4
/-- If `f` and `g` are two maps `P → P'` between presentations,
then the image of `f - g` is in the kernel of `P' → S`.
-/
@[simps! apply_coe]
noncomputable def subToKer (f g : Hom P P') : P.Ring →ₗ[R] P'.ker :=
by
refine ((f.toAlgHom.toLinearMap - g.toAlgHom.toLinearMap).codRestrict (P'.ker.restrictScalars R) ?_)
intro x
simp only [LinearMap.sub_apply, AlgHom.toLinearMap_apply, ker, Submodule.restrictScalars_mem, RingHom.mem_ker,
map_sub, algebraMap_toRingHom, sub_self, toAlgHom_apply]
