epi_map_iff_epi — Mathlib

English

If F preserves and reflects epimorphisms, then Epi (F.map f) iff Epi f.

Русский

Если F сохраняет и отражает эпиморфизмы, то Epi(F.map f) эквивалечно Epi f.

LaTeX

$$$$ \\operatorname{Epi}(F.map f) \\iff \\operatorname{Epi}(f). $$$$

Lean4

@[simp]
theorem epi_map_iff_epi [hF₁ : PreservesEpimorphisms F] [hF₂ : ReflectsEpimorphisms F] : Epi (F.map f) ↔ Epi f :=
  by
  constructor
  · exact F.epi_of_epi_map
  · intro h
    exact F.map_epi f

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