English
For a family of linear maps f_i: M → M_i, each with p ≤ ker f_i, the equality holds: LinearMap.pi (f i → p.liftQ (f_i) (h_i)) = p.liftQ (LinearMap.pi f) (LinearMap.ker_pi f ⊢ le_iInf h).
Русский
Для семейства линейных отображений f_i: M → M_i, если ∀ i, p ≤ ker f_i, то выполняется равенство: LinearMap.pi(...)=p.liftQ(LinearMap.pi f)...
LaTeX
$$$$ \\operatorname{LinearMap.pi} \\bigl( i \\mapsto p.liftQ (f_i) (h_i) \\bigr) = p.liftQ (\\operatorname{LinearMap.pi} f) \\bigl( \\operatorname{ker\\_pi} f \\; \\rhd \\; \\le_iInf h \\bigr). $$$$
Lean4
/-- The map from the quotient of `M` by submodule `p` to the quotient of `M₂` by submodule `q` along
`f : M → M₂` is linear. -/
def mapQ (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ comap f q) : M ⧸ p →ₛₗ[τ₁₂] M₂ ⧸ q :=
p.liftQ (q.mkQ.comp f) <| by simpa [ker_comp] using h
