comap_liftQ — Mathlib

English

Let p ⊆ M and q ⊆ M₂ be submodules, f: M →ₛₗ[τ₁₂] M₂ a linear map, and h a hypothesis ensuring lift to the quotient. Then the comapped submodule equality holds: q.comap (p.liftQ f h) = (q.comap f).map (mkQ p).

Русский

Пусть p ⊆ M и q ⊆ M₂ — подмодули, f: M →ₛₗ[τ₁₂] M₂, и h — условие для подъёма в фактор‑модуль; тогда выполняется равенство подмодулов: q.comap (p.liftQ f h) = (q.comap f).map (mkQ p).

LaTeX

$$$$ q.comap (p.liftQ f h) = (q.comap f).map (mkQ p). $$$$

Lean4

theorem comap_liftQ (f : M →ₛₗ[τ₁₂] M₂) (h) : q.comap (p.liftQ f h) = (q.comap f).map (mkQ p) :=
  le_antisymm (by rintro ⟨x⟩ hx; exact ⟨_, hx, rfl⟩) (by rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ])

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