English
Let I be a finite index set and let (M_i)_{i∈I} be R-modules. For each i, let p_i ⊆ M_i be a submodule and let q ⊆ N be a submodule of an R-module N. Suppose f_i: M_i → N are linear maps with p_i ⊆ f_i^{-1}(q) (i.e. f_i(p_i) ⊆ q). Then there exists a unique R-linear map from the direct sum of the quotients ⊕_{i∈I} (M_i / p_i) to the quotient N/q, which on a pure tuple (x_i mod p_i) sends it to the class of the sum ∑ f_i(x_i) modulo q.
Русский
Пусть I — конечное множество индексов, иMb_i — R-модули. Для каждого i пусть p_i ⊆ M_i — подмодуль, q ⊆ N — подмодуль, и пусть f_i: M_i → N — линейные отображения такие, что p_i ⊆ f_i^{-1}(q) (то есть f_i(p_i) ⊆ q). Тогда существует единственный R-линейный отображение\n⊕_{i∈I} (M_i / p_i) → N/q,\nкоторое на элементе вида (x_i mod p_i) отправляет класс ∑ f_i(x_i) по модулю q.
LaTeX
$$$\\text{Let } I \\text{ be finite and } (M_i)_{i\\in I} \\text{ be } R\\text{-modules.\\ For each } i, p_i \\leq M_i, q \\leq N,\\ f_i: M_i \\to N.\\ Suppose } p_i \\subseteq f_i^{-1}(q) \\text{ for all } i.\\ Then there exists a unique } R\\text{-linear map } L: \\bigoplus_{i\\in I} (M_i/p_i) \\to N/q \\text{ such that }\\ L([x_i]_{i\\in I}) = [\\sum_{i\\in I} f_i(x_i)].$$$
Lean4
/-- Lift a family of maps to the direct sum of quotients. -/
def piQuotientLift [Fintype ι] [DecidableEq ι] (p : ∀ i, Submodule R (Ms i)) (q : Submodule R N) (f : ∀ i, Ms i →ₗ[R] N)
(hf : ∀ i, p i ≤ q.comap (f i)) : (∀ i, Ms i ⧸ p i) →ₗ[R] N ⧸ q :=
lsum R (fun i => Ms i ⧸ p i) R fun i => (p i).mapQ q (f i) (hf i)
