range_liftQ — Mathlib

English

Let p ⊆ M and f: M →ₛₗ[τ₁₂] M₂ be a linear map with lifting h; then the range of the lifted map equals the range of f: range (p.liftQ f h) = range f.

Русский

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

LaTeX

$$$$ \\operatorname{range}(p.liftQ f h) = \\operatorname{range}(f). $$$$

Lean4

theorem range_liftQ [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h) : range (p.liftQ f h) = range f := by
  simpa only [range_eq_map] using map_liftQ _ _ _ _

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