Theorems · Theorem · category theory

CategoryTheory.isSeparator_iff_epi

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C)
  [inst_1 : ∀ (A : C), CategoryTheory.Limits.HasCoproduct fun x => G],
  CategoryTheory.IsSeparator G ↔ ∀ (A : C), CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc fun f => f)

Defined in

Mathlib.CategoryTheory.Generator.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasCoproduct