English
In the above situation, when we evaluate the lift on the element whose i-th component is the class of x_i and all other components are zero, the result is the class of the sum of the images f_i(x_i) across all i. More precisely, the lift applied to the tuple (Quotient.mk (x_i)) equals Quotient.mk (lsum_i f_i(x_i)).
Русский
В вышеприведённой ситуации, при подстановке в лифтинг элемента, у которого на i-м месте стоит класс x_i, а на остальных местах нули, результатом является класс суммы изображений f_i(x_i) по всем i.
LaTeX
$$$\\text{For } x=(x_i)_i\\in \\prod_i M_i,\\ (\\pi\\mathrel{−}\\text{QuotientLift}\,p\\,q\\,f\\,hf)(\\Pi_i\\,\\text{Quotient.mk}(x_i))=\\text{Quotient.mk}\\left(\\sum_i f_i(x_i)\\right).$$$
Lean4
@[simp]
theorem piQuotientLift_mk [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)) (x : ∀ i, Ms i) :
(piQuotientLift p q f hf fun i => Quotient.mk (x i)) = Quotient.mk (lsum _ _ R f x) :=
by
rw [piQuotientLift, lsum_apply, sum_apply, ← mkQ_apply, lsum_apply, sum_apply, _root_.map_sum]
simp only [coe_proj, mapQ_apply, mkQ_apply, comp_apply]
