forget₂_preservesEpimorphisms — Mathlib

English

MorphismProperty surjective equals epimorphisms if and only if forgetful functor preserves epimorphisms.

Русский

Свойство сюръективности морфизмов равно эпиморфизмам тогда и только тогда, когда забывающий функтор сохраняет эпиморфизмы.

LaTeX

$$$\text{surjective } C = \text{epimorphisms } C \iff (\text{forget } C).PreservesEpimorphisms$$$

Lean4

instance forget₂_preservesEpimorphisms (C : Type u) (D : Type u') [Category.{v} C] [HasForget.{w} C] [Category.{v'} D]
    [HasForget.{w} D] [HasForget₂ C D] [(forget C).PreservesEpimorphisms] : (forget₂ C D).PreservesEpimorphisms :=
  have : (forget₂ C D ⋙ forget D).PreservesEpimorphisms :=
    by
    simp only [HasForget₂.forget_comp]
    infer_instance
  Functor.preservesEpimorphisms_of_preserves_of_reflects _ (forget D)

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