Theorems · Theorem · category theory

CategoryTheory.Over.epi_of_epi_left

∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (k : f ⟶ g)
  [hk : CategoryTheory.Epi (CategoryTheory.Over.Hom.left k)], CategoryTheory.Epi k

If k.left is an epimorphism, then k is an epimorphism. In other words, Over.forget X reflects epimorphisms. The converse does not hold without additional assumptions on the underlying category, see CategoryTheory.Over.epi_left_of_epi.

Defined in

Mathlib.CategoryTheory.Comma.Over.Basic

Cited by

0 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Epi