epi_iff_surjective — Mathlib

English

In Type, a morphism f: X ⟶ Y is epi iff f is surjective.

Русский

В типах морфизм f: X ⟶ Y является эпиморфизмом тогда и только тогда, когда он сюръективен.

LaTeX

$$$$ \text{Epi } f \;\iff\; \text{Surjective } f. $$$$

Lean4

/-- A morphism in `Type` is an epimorphism if and only if it is surjective. -/
@[stacks 003C]
theorem epi_iff_surjective {X Y : Type u} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f :=
  by
  constructor
  · rintro ⟨H⟩
    refine Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => ?_
    rw [← Equiv.ulift.symm.injective.comp_left.eq_iff]
    apply H
    change ULift.up ∘ g₁ ∘ f = ULift.up ∘ g₂ ∘ f
    rw [hg]
  · exact fun H => ⟨fun g g' h => H.injective_comp_right h⟩

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