English
Let p ⊆ M and q ⊆ M₂ be submodules and f: M →ₛₗ[τ₁₂] M₂ a semilinear map such that p is contained in the pullback of q along f (i.e., the induced map on quotients is well defined). Then the induced map on quotients satisfies that the image of the class of x in M/p is the class of f(x) in M₂/q for every x ∈ M.
Русский
Пусть p ⊆ M и q ⊆ M₂ — подмодули, и f: M →ₛₗ[τ₁₂] M₂ — полугладкий отображение, такое что p ≤ comap f q (т.е. разложение на фактор‑модулях определено). Тогда индуцированное отображение между фактор‑модулями удовлетворяет: образ класса x по p отображается в класс f(x) по q для всех x ∈ M.
LaTeX
$$$$ (mapQ\, p\, q\, f\, h)(\\overline{x}) = \\overline{f(x)}. $$$$
Lean4
@[simp]
theorem mapQ_apply (f : M →ₛₗ[τ₁₂] M₂) {h} (x : M) : mapQ p q f h (Quotient.mk x) = Quotient.mk (f x) :=
rfl
