instEpiFunctorWhiskerRightOfPreservesEpimorphisms

English

If f is epi and H preserves epimorphisms, then whiskerRight f H is epi.

Русский

Если f — эпиморфизм и H сохраняет эпиморфизмы, то whiskerRight f H — эпиморфизм.

LaTeX

$$$[\\mathrm{Epi}\, f] (H) \\Rightarrow \\mathrm{whiskerRight}\, f\, H \\text{ is epi}.$$$

Lean4

instance [Epi f] (H : C ⥤ D) [H.PreservesEpimorphisms] : Epi (whiskerRight f H) :=
  by
  have : ∀ X, Epi ((whiskerRight f H).app X) := by intros; dsimp; infer_instance
  apply NatTrans.epi_of_epi_app

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