English
The factor map from p to p' is the canonical linear map sending a coset modulo p to the corresponding coset modulo p'.
Русский
Картирование фактор‑модуля от p к p' есть канонический линейный переход, отправляющий косет по p в косет по p'.
LaTeX
$$$$ \\text{factor} : M/ p \\to M/ p' \quad\\text{with } p \\le p'. $$$$
Lean4
/-- The linear map from the quotient by a smaller submodule to the quotient by a larger submodule.
This is the `Submodule.Quotient` version of `Quot.Factor`
When the two submodules are of the form `I ^ m • ⊤` and `I ^ n • ⊤` and `n ≤ m`,
please refer to the dedicated version `Submodule.factorPow`. -/
abbrev factor (H : p ≤ p') : M ⧸ p →ₗ[R] M ⧸ p' :=
mapQ _ _ LinearMap.id H
