English
There is a remainder map sending a polynomial to its remainder upon division by a monic polynomial g, giving a linear map from AdjoinRoot g to R[X].
Русский
Существет остаточный отображение при делении на моническое g, переходящее из AdjoinRoot g в R[X].
LaTeX
$$modByMonicHom(g.MonI)c: AdjoinRoot g →ₗ[R] R[X]$$
Lean4
/-- `AdjoinRoot.modByMonicHom` sends the equivalence class of `f` mod `g` to `f %ₘ g`.
This is a well-defined right inverse to `AdjoinRoot.mk`, see `AdjoinRoot.mk_leftInverse`. -/
def modByMonicHom (hg : g.Monic) : AdjoinRoot g →ₗ[R] R[X] :=
(Submodule.liftQ _ (Polynomial.modByMonicHom g) fun f (hf : f ∈ (Ideal.span { g }).restrictScalars R) =>
(mem_ker_modByMonic hg).mpr (Ideal.mem_span_singleton.mp hf)).comp <|
(Submodule.Quotient.restrictScalarsEquiv R (Ideal.span { g } : Ideal R[X])).symm.toLinearMap
