forget_grp_preserves_epi — Mathlib

English

The forgetful functor from GrpCat to Type preserves epimorphisms.

Русский

Функтор забывания из GrpCat в Type сохраняет эпиморфизмы.

LaTeX

$$$$ \text{forget}_{GrpCat}.\text{PreservesEpimorphisms}. $$$$

Lean4

@[to_additive AddGrpCat.forget_grp_preserves_epi]
instance forget_grp_preserves_epi : (forget GrpCat).PreservesEpimorphisms where
  preserves f e := by rwa [epi_iff_surjective, ← CategoryTheory.epi_iff_surjective] at e

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