Theorems · Theorem · category theory

CategoryTheory.Presheaf.isSeparator

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] {ι : Type w} {S : ι → A},
  (CategoryTheory.ObjectProperty.ofObj S).IsSeparating →
    ∀
      [inst_3 :
        CategoryTheory.Limits.HasCoproduct fun x =>
          match x with
          | (X, i) => CategoryTheory.Presheaf.freeYoneda X (S i)]
      [CategoryTheory.Limits.HasZeroMorphisms A],
      CategoryTheory.IsSeparator
        (∐ fun x =>
          match x with
          | (X, i) => CategoryTheory.Presheaf.freeYoneda X (S i))

Defined in

Mathlib.CategoryTheory.Generator.Presheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasCoproductsCategoryTheory.Limits.HasCoproductCategoryTheory.Limits.HasZeroMorphisms