mapQ_mkQ — Mathlib

English

Let p ⊆ M and q ⊆ M₂ be submodules, and f: M →ₛₗ[τ₁₂] M₂ a semilinear map. Then the induced map on quotients commutes with the quotient maps, i.e., (mapQ p q f h) after composing with p.mkQ equals q.mkQ after composing with f.

Русский

Пусть p ⊆ M и q ⊆ M₂ — подмодули, и f: M →ₛₗ[τ₁₂] M₂ — полугладкое отображение. Тогда отображение на факторо‑модулях связывается с естественными картами факторов так, что (mapQ p q f h) ∘ p.mkQ = q.mkQ ∘ f.

LaTeX

$$$$ (mapQ\, p\, q\, f\, h) \\circ p.mkQ = q.mkQ \\circ f. $$$$

Lean4

theorem mapQ_mkQ (f : M →ₛₗ[τ₁₂] M₂) {h} : (mapQ p q f h).comp p.mkQ = q.mkQ.comp f := by ext x; rfl

Похожие утверждения