ker_liftQ — Mathlib

English

Let p ⊆ M and f: M →ₛₗ[τ₁₂] M₂ be a linear map with lifting h. Then the kernel of the lifted map equals the image of the kernel of f under mkQ p: ker (p.liftQ f h) = (ker f).map (mkQ p).

Русский

Пусть p ⊆ M и f: M →ₛₗ[τ₁₂] M₂ — линейное отображение с подъёмом h. Тогда ядро подъёма равно образу ядра f под mkQ p: ker (p.liftQ f h) = (ker f).map (mkQ p).

LaTeX

$$$$ \\ker (p.liftQ f h) = (\\ker f).map (mkQ p). $$$$

Lean4

theorem ker_liftQ (f : M →ₛₗ[τ₁₂] M₂) (h) : ker (p.liftQ f h) = (ker f).map (mkQ p) :=
  comap_liftQ _ _ _ _

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