Theorems · Definition · category theory

CategoryTheory.Presheaf.IsSeparated

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        CategoryTheory.GrothendieckTopology C →
          CategoryTheory.Functor Cᵒᵖ A →
            {FA : A → A → Type u_1} →
              {CA : A → Type u_2} →
                [inst : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] → [CategoryTheory.ConcreteCategory A FA] → Prop

Condition that a presheaf with values in a concrete category is separated for a Grothendieck topology.

Defined in

Mathlib.CategoryTheory.Sites.Sheaf

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategory