Theorems · Theorem · category theory

CategoryTheory.Sheaf.isSeparating

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

Defined in

Mathlib.CategoryTheory.Generator.Sheaf

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasCoproductsCategoryTheory.HasWeakSheafify