The canonical topology on a category

We define the finest (largest) Grothendieck topology for which a given presheaf P is a sheaf. This is well defined since if P is a sheaf for a topology J, then it is a sheaf for any coarser (smaller) topology. Nonetheless we define the topology explicitly by specifying its sieves: A sieve S on X is covering for finestTopologySingle P iff for any f : Y ⟶ X, P satisfies the sheaf axiom for S.pullback f. Showing that this is a genuine Grothendieck topology (namely that it satisfies the transitivity axiom) forms the bulk of this file.

This generalises to a set of presheaves, giving the topology finestTopology Ps which is the finest topology for which every presheaf in Ps is a sheaf. Using Ps as the set of representable presheaves defines the canonicalTopology: the finest topology for which every representable is a sheaf.

A Grothendieck topology is called Subcanonical if it is smaller than the canonical topology, equivalently it is subcanonical iff every representable presheaf is a sheaf.

References

• https://ncatlab.org/nlab/show/canonical+topology
• https://ncatlab.org/nlab/show/subcanonical+coverage
• https://stacks.math.columbia.edu/tag/00Z9
• https://math.stackexchange.com/a/358709/

@[deprecated CategoryTheory.Presieve.isSheafFor_bind (since := "2026-02-06")]

theorem CategoryTheory.Sheaf.isSheafFor_bind {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (P : Functor Cᵒᵖ (Type u_1)) (U : Sieve X) (B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y) (hU : Presieve.IsSheafFor P U.arrows) (hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows) (hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows) : Presieve.IsSheafFor P (Sieve.bind U.arrows B).arrows

Alias of CategoryTheory.Presieve.isSheafFor_bind.

@[deprecated CategoryTheory.Presieve.isSheafFor_trans (since := "2026-02-06")]

theorem CategoryTheory.Sheaf.isSheafFor_trans {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (P : Functor Cᵒᵖ (Type u_1)) (R S : Sieve X) (hR : Presieve.IsSheafFor P R.arrows) (hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows) (hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows) : Presieve.IsSheafFor P S.arrows

Alias of CategoryTheory.Presieve.isSheafFor_trans.

def CategoryTheory.Sheaf.finestTopologySingle {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type v)) : GrothendieckTopology C

Construct the finest (largest) Grothendieck topology for which the given presheaf is a sheaf.

def CategoryTheory.Sheaf.finestTopology {C : Type u} [Category.{v, u} C] (Ps : Set (Functor Cᵒᵖ (Type v))) : GrothendieckTopology C

Construct the finest (largest) Grothendieck topology for which all the given presheaves are sheaves.

theorem CategoryTheory.Sheaf.sheaf_for_finestTopology {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type v)} (Ps : Set (Functor Cᵒᵖ (Type v))) (h : P ∈ Ps) : Presieve.IsSheaf (finestTopology Ps) P

Check that if P ∈ Ps, then P is indeed a sheaf for the finest topology on Ps.

theorem CategoryTheory.Sheaf.le_finestTopology {C : Type u} [Category.{v, u} C] (Ps : Set (Functor Cᵒᵖ (Type v))) (J : GrothendieckTopology C) (hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P) : J ≤ finestTopology Ps

Check that if each P ∈ Ps is a sheaf for J, then J is a subtopology of finestTopology Ps.

def CategoryTheory.Sheaf.canonicalTopology (C : Type u) [Category.{v, u} C] : GrothendieckTopology C

The canonicalTopology on a category is the finest (largest) topology for which every representable presheaf is a sheaf.

theorem CategoryTheory.Sheaf.isSheaf_yoneda_obj {C : Type u} [Category.{v, u} C] (X : C) : Presieve.IsSheaf (canonicalTopology C) (yoneda.obj X)

yoneda.obj X is a sheaf for the canonical topology.

theorem CategoryTheory.Sheaf.isSheaf_of_isRepresentable {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) [P.IsRepresentable] : Presieve.IsSheaf (canonicalTopology C) P

A representable functor is a sheaf for the canonical topology.

class CategoryTheory.GrothendieckTopology.Subcanonical {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : Prop

A subcanonical topology is a topology which is smaller than the canonical topology. Equivalently, a topology is subcanonical iff every representable is a sheaf.

• le_canonical : J ≤ Sheaf.canonicalTopology C

theorem CategoryTheory.GrothendieckTopology.le_canonical {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : J ≤ Sheaf.canonicalTopology C

instance CategoryTheory.GrothendieckTopology.instSubcanonicalCanonicalTopology {C : Type u} [Category.{v, u} C] : (Sheaf.canonicalTopology C).Subcanonical

theorem CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (h : ∀ (X : C), Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)) : J.Subcanonical

If every functor yoneda.obj X is a J-sheaf, then J is subcanonical.

theorem CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [J.Subcanonical] (P : Functor Cᵒᵖ (Type w)) [P.IsRepresentable] : Presieve.IsSheaf J P

If J is subcanonical, then any representable is a J-sheaf.

theorem CategoryTheory.GrothendieckTopology.Subcanonical.of_le {C : Type u} [Category.{v, u} C] {J K : GrothendieckTopology C} (h : J ≤ K) [K.Subcanonical] : J.Subcanonical

def CategoryTheory.GrothendieckTopology.yoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : Functor C (Sheaf J (Type v))

If J is subcanonical, we obtain a "Yoneda" functor from the defining site into the sheaf category.

@[simp]

theorem CategoryTheory.GrothendieckTopology.yoneda_map_hom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (J.yoneda.map f).hom = CategoryTheory.yoneda.map f

@[simp]

theorem CategoryTheory.GrothendieckTopology.yoneda_obj_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : C) : (J.yoneda.obj X).obj = CategoryTheory.yoneda.obj X

def CategoryTheory.GrothendieckTopology.uliftYoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : Functor C (Sheaf J (Type (max v w)))

Variant of the Yoneda embedding which allows a raise in the universe level for the category of types.

@[simp]

theorem CategoryTheory.GrothendieckTopology.uliftYoneda_map_hom_app_down {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) (a✝ : uliftFunctor.{w, v}.obj (((sheafToPresheaf J (Type v)).obj (J.yoneda.obj X✝)).obj X)) : (((uliftYoneda.{w, v, u} J).map f).hom.app X a✝).down = CategoryStruct.comp a✝.down f

@[simp]

theorem CategoryTheory.GrothendieckTopology.uliftYoneda_obj_obj_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : C) (X✝ : Cᵒᵖ) : ((uliftYoneda.{w, v, u} J).obj X).obj.obj X✝ = ULift.{w, v} (Opposite.unop X✝ ⟶ X)

@[simp]

theorem CategoryTheory.GrothendieckTopology.uliftYoneda_obj_obj_map_down {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (a✝ : uliftFunctor.{w, v}.obj (((sheafToPresheaf J (Type v)).obj (J.yoneda.obj X)).obj X✝)) : (((uliftYoneda.{w, v, u} J).obj X).obj.map f a✝).down = CategoryStruct.comp f.unop a✝.down

@[deprecated CategoryTheory.GrothendieckTopology.uliftYoneda (since := "2025-11-10")]

def CategoryTheory.GrothendieckTopology.yonedaULift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : Functor C (Sheaf J (Type (max v w)))

Alias of CategoryTheory.GrothendieckTopology.uliftYoneda.

---

Variant of the Yoneda embedding which allows a raise in the universe level for the category of types.

def CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda {C : Type u} [Category.{max w v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : uliftYoneda.{w, max v w, u} J ≅ J.yoneda

If C is a category with [Category.{max w v} C], this is the isomorphism uliftYoneda.{w} (C := C) ≅ yoneda.

@[simp]

theorem CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_hom_app_hom_app {C : Type u} [Category.{max w v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : C) (X✝ : Cᵒᵖ) (a✝ : ((sheafToPresheaf J (Type (max v w))).obj ((uliftYoneda.{w, max v w, u} J).obj X)).obj X✝) : (J.uliftYonedaIsoYoneda.hom.app X).hom.app X✝ a✝ = a✝.down

@[simp]

theorem CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_hom_app_down {C : Type u} [Category.{max w v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : C) (X✝ : Cᵒᵖ) (a✝ : ((sheafToPresheaf J (Type (max v w))).obj (J.yoneda.obj X)).obj X✝) : ((J.uliftYonedaIsoYoneda.inv.app X).hom.app X✝ a✝).down = a✝

def CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : J.yoneda.comp (sheafToPresheaf J (Type v)) ≅ CategoryTheory.yoneda

The yoneda embedding into the presheaf category factors through the one to the sheaf category.

def CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : (uliftYoneda.{w, v, u} J).comp (sheafToPresheaf J (Type (max v w))) ≅ CategoryTheory.uliftYoneda.{w, v, u}

A variant of yonedaCompSheafToPresheaf with a raise in the universe level.

@[simp]

theorem CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf_inv_app_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : C) (X✝ : Cᵒᵖ) (a✝ : (((uliftYoneda.{w, v, u} J).comp (sheafToPresheaf J (Type (max v w)))).obj X).obj X✝) : (J.uliftYonedaCompSheafToPresheaf.inv.app X).app X✝ a✝ = a✝

@[simp]

theorem CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf_hom_app_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : C) (X✝ : Cᵒᵖ) (a✝ : (((uliftYoneda.{w, v, u} J).comp (sheafToPresheaf J (Type (max v w)))).obj X).obj X✝) : (J.uliftYonedaCompSheafToPresheaf.hom.app X).app X✝ a✝ = a✝

def CategoryTheory.GrothendieckTopology.yonedaFullyFaithful {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : J.yoneda.FullyFaithful

The yoneda functor into the sheaf category is fully faithful

instance CategoryTheory.GrothendieckTopology.instFullSheafTypeYoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : J.yoneda.Full

instance CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeYoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : J.yoneda.Faithful

def CategoryTheory.GrothendieckTopology.fullyFaithfulUliftYoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : (uliftYoneda.{w, v, u} J).FullyFaithful

A variant of yonedaFullyFaithful with a raise in the universe level.

instance CategoryTheory.GrothendieckTopology.instFullSheafTypeUliftYoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : (uliftYoneda.{w, v, u} J).Full

instance CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeUliftYoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : (uliftYoneda.{w, v, u} J).Faithful