English
There is a canonical linear map from the quotient of the full direct product by the submodule of all tuples whose i-th component lies in p_i, to the product of the quotients M_i/p_i, defined componentwise by sending the class of a tuple (x_i)_i to the tuple (x_i mod p_i). If each p_i is mapped to zero under f_i, then this lift factors through to the product of Ns.
Русский
Существует каноническое линейное отображение из частной модуля прямой суммы, взятой по модулям p_i, в произведение квот, определённое по компонентам: класс кортежа (x_i)_i идёт в кортеж (x_i mod p_i).
LaTeX
$$$\\text{quotientPiLift}: (\\forall i, M_i) / (\\pi\\,Set.univ\\ p) \\to \\prod_i N_i$, с условиями, что $p_i \\le \\ker f_i$ и т.д.$$
Lean4
/-- Lift a family of maps to a quotient of direct sums. -/
def quotientPiLift (p : ∀ i, Submodule R (Ms i)) (f : ∀ i, Ms i →ₗ[R] Ns i) (hf : ∀ i, p i ≤ ker (f i)) :
(∀ i, Ms i) ⧸ pi Set.univ p →ₗ[R] ∀ i, Ns i :=
(pi Set.univ p).liftQ (LinearMap.pi fun i => (f i).comp (proj i)) fun x hx =>
mem_ker.mpr <| by
ext i
simpa using hf i (mem_pi.mp hx i (Set.mem_univ i))
