Theorems · Definition · category theory

CategoryTheory.HasGlobalSectionsFunctor

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

Typeclass stating that the constant sheaf functor has a right adjoint. This right adjoint will then be called the global sections functor and written Sheaf.Γ.

Defined in

Mathlib.CategoryTheory.Sites.GlobalSections

Cited by

14 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.HasWeakSheafify