range_eq_top_of_epi — Mathlib

English

If f is an epimorphism in ModuleCat, then the range of the underlying linear map is all of the codomain.

Русский

Если f является эпиморфизмом в ModuleCat, то образ подля линейного отображения f равен всему кодомодуля.

LaTeX

$$$\\text{Epi}(f) \\Rightarrow \\operatorname{range}(f.hom) = \\top$$$

Lean4

theorem range_eq_top_of_epi [Epi f] : LinearMap.range f.hom = ⊤ :=
  LinearMap.range_eq_top_of_cancel fun u v h =>
    ModuleCat.hom_ext_iff.mp <| (@cancel_epi _ _ _ _ _ f _ (↟u) (↟v)).1 <| ModuleCat.hom_ext_iff.mpr h

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