surjective_eq_epimorphisms_iff — Mathlib

English

Same equivalence as above: surjective morphisms are epimorphisms iff forgetful preserves epimorphisms.

Русский

Повторно та же эквивалентность: сюръективные морфизмы — эпиморфизм, если забывающий сохраняет эпиморфизмы.

LaTeX

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

Lean4

theorem surjective_eq_epimorphisms_iff :
    MorphismProperty.surjective C = epimorphisms C ↔ (forget C).PreservesEpimorphisms :=
  by
  constructor
  · intro h
    constructor
    rintro _ _ f (hf : epimorphisms C f)
    rw [epi_iff_surjective]
    rw [← h] at hf
    exact hf
  · intro
    apply le_antisymm (surjective_le_epimorphisms C)
    intro _ _ f hf
    have : Epi f := hf
    change Function.Surjective ((forget C).map f)
    rw [← epi_iff_surjective]
    infer_instance

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