Theorems · Inductive type · category theory

CategoryTheory.HasSheafify

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.GrothendieckTopology C → (A : Type u₂) → [CategoryTheory.Category.{v₂, u₂} A] → Prop

HasSheafify means that the inclusion functor from sheaves to presheaves admits a left exact left adjoint (sheafification). Given a functor, preserving finite limits, F : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A and an adjunction adj : F ⊣ sheafToPresheaf J A, use HasSheafify.mk' to construct a HasSheafify instance.

Defined in

Mathlib.CategoryTheory.Sites.Sheafification

Cited by

106 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category