English
For a family of linear maps f_i, each with p ≤ ker f_i, the pi-lift equals the lift of the pi map:
Русский
Для семейства линейных отображений f_i, удовлетворяющих p ≤ ker f_i, выполняется равенство pi-liftQ = liftQ_pi.
LaTeX
$$$$ \\operatorname{LinearMap.pi}\\bigl( \\lambda i, p.liftQ (f_i) (\\,h_i\\, ) \\bigr) = p.liftQ\\bigl( \\operatorname{LinearMap.pi} f \\bigr)\\bigl( \\operatorname{ker\\_pi} f \\;\\rhd\\; \\bigl\\le_iInf h \\bigr). $$$$
Lean4
/-- The map from the quotient of `M` by a submodule `p` to `M₂` induced by a linear map `f : M → M₂`
vanishing on `p`, as a linear map. -/
def liftQ (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ ker f) : M ⧸ p →ₛₗ[τ₁₂] M₂ :=
{ QuotientAddGroup.lift p.toAddSubgroup f.toAddMonoidHom h with map_smul' := by rintro a ⟨x⟩; exact f.map_smulₛₗ a x }
