Subcanonical Grothendieck topologies

This file provides some API for the Yoneda embedding into the category of sheaves for a subcanonical Grothendieck topology.

def CategoryTheory.GrothendieckTopology.yonedaEquiv {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X : C} {F : Sheaf J (Type v)} : (J.yoneda.obj X ⟶ F) ≃ F.obj.obj (Opposite.op X)

The equivalence between natural transformations from the yoneda embedding (to the sheaf category) and elements of F.val.obj X.

Equations

• J.yonedaEquiv = (CategoryTheory.fullyFaithfulSheafToPresheaf J (Type ?u.24)).homEquiv.trans CategoryTheory.yonedaEquiv

theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_apply {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X : C} {F : Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F) : J.yonedaEquiv f = (ConcreteCategory.hom (f.hom.app (Opposite.op X))) (CategoryStruct.id X)

@[simp]

theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X : C} {F : Sheaf J (Type v)} (x : F.obj.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X) : (ConcreteCategory.hom ((J.yonedaEquiv.symm x).hom.app Y)) f = (ConcreteCategory.hom (F.obj.map f.op)) x

theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : C} {F : Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F) (g : Y ⟶ X) : (ConcreteCategory.hom (F.obj.map g.op)) (J.yonedaEquiv f) = J.yonedaEquiv (CategoryStruct.comp (J.yoneda.map g) f)

See also yonedaEquiv_naturality' for a more general version.

theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality' {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} {F : Sheaf J (Type v)} (f : J.yoneda.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : (ConcreteCategory.hom (F.obj.map g)) (J.yonedaEquiv f) = J.yonedaEquiv (CategoryStruct.comp (J.yoneda.map g.unop) f)

Variant of yonedaEquiv_naturality with general g. This is technically strictly more general than yonedaEquiv_naturality, but yonedaEquiv_naturality is sometimes preferable because it can avoid the "motive is not type correct" error.

theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_comp {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X : C} {F G : Sheaf J (Type v)} (α : J.yoneda.obj X ⟶ F) (β : F ⟶ G) : J.yonedaEquiv (CategoryStruct.comp α β) = (ConcreteCategory.hom (β.hom.app (Opposite.op X))) (J.yonedaEquiv α)

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

theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_left {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X X' : C} (f : X' ⟶ X) (F : Sheaf J (Type v)) (x : F.obj.obj (Opposite.op X)) : CategoryStruct.comp (J.yoneda.map f) (J.yonedaEquiv.symm x) = J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x)

theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : C) {F F' : Sheaf J (Type v)} (f : F ⟶ F') (x : F.obj.obj (Opposite.op X)) : CategoryStruct.comp (J.yonedaEquiv.symm x) f = J.yonedaEquiv.symm ((ConcreteCategory.hom (f.hom.app (Opposite.op X))) x)

theorem CategoryTheory.GrothendieckTopology.map_yonedaEquiv {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : C} {F : Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F) (g : Y ⟶ X) : (ConcreteCategory.hom (F.obj.map g.op)) (J.yonedaEquiv f) = (ConcreteCategory.hom (f.hom.app (Opposite.op Y))) g

See also map_yonedaEquiv' for a more general version.

theorem CategoryTheory.GrothendieckTopology.map_yonedaEquiv' {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} {F : Sheaf J (Type v)} (f : J.yoneda.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : (ConcreteCategory.hom (F.obj.map g)) (J.yonedaEquiv f) = (ConcreteCategory.hom (f.hom.app Y)) g.unop

Variant of map_yonedaEquiv with general g. This is technically strictly more general than map_yonedaEquiv, but map_yonedaEquiv is sometimes preferable because it can avoid the "motive is not type correct" error.

theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : Sheaf J (Type v)} (t : F.obj.obj X) : J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f)) t) = CategoryStruct.comp (J.yoneda.map f.unop) (J.yonedaEquiv.symm t)

theorem CategoryTheory.GrothendieckTopology.hom_ext_yoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {P Q : Sheaf J (Type v)} {f g : P ⟶ Q} (h : ∀ (X : C) (p : J.yoneda.obj X ⟶ P), CategoryStruct.comp p f = CategoryStruct.comp p g) : f = g

Two morphisms of sheaves of types P ⟶ Q coincide if the precompositions with morphisms yoneda.obj X ⟶ P agree.

def CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : J.yoneda.op.comp coyoneda ≅ (evaluation Cᵒᵖ (Type v)).comp (((Functor.whiskeringRight (Functor Cᵒᵖ (Type v)) (Type v) (Type (max v u))).obj uliftFunctor.{u, v}).comp ((Functor.whiskeringLeft (Sheaf J (Type v)) (Functor Cᵒᵖ (Type v)) (Type (max v u))).obj (sheafToPresheaf J (Type v))))

The Yoneda lemma for sheaves.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (X✝ : Sheaf J (Type v)) : (J.yonedaOpCompCoyoneda.inv.app X).app X✝ = CategoryStruct.comp ((largeCurriedYonedaLemma.inv.app X).app X✝.obj) (CategoryStruct.comp (TypeCat.ofHom fun (g : CategoryTheory.yoneda.obj (Opposite.unop X) ⟶ X✝.obj) => CategoryStruct.comp (J.yonedaCompSheafToPresheaf.hom.app (Opposite.unop X)) g) ((sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.hom.app (Opposite.op (J.yoneda.obj (Opposite.unop X)))).app X✝))

@[simp]

theorem CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_hom_apply_down {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (X✝ : Sheaf J (Type v)) (a✝ : ((J.yoneda.op.comp coyoneda).obj X).obj X✝) : ((ConcreteCategory.hom ((J.yonedaOpCompCoyoneda.hom.app X).app X✝)) a✝).down = CategoryTheory.yonedaEquiv ((CategoryStruct.comp ((sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.inv.app (Opposite.op (J.yoneda.obj (Opposite.unop X)))).app X✝) (TypeCat.ofHom fun (g : CategoryTheory.yoneda.obj (Opposite.unop X) ⟶ X✝.obj) => CategoryStruct.comp (J.yonedaCompSheafToPresheaf.inv.app (Opposite.unop X)) g)).hom' a✝)

def CategoryTheory.GrothendieckTopology.uliftYonedaEquiv {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X : C} {F : Sheaf J (Type (max v v'))} : ((uliftYoneda.{v', v, u} J).obj X ⟶ F) ≃ F.obj.obj (Opposite.op X)

A version of yonedaEquiv for uliftYoneda.

Equations

• J.uliftYonedaEquiv = (CategoryTheory.fullyFaithfulSheafToPresheaf J (Type (max ?u.40 ?u.41))).homEquiv.trans CategoryTheory.uliftYonedaEquiv

theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X : C} {F : Sheaf J (Type (max v v'))} (f : (uliftYoneda.{v', v, u} J).obj X ⟶ F) : J.uliftYonedaEquiv f = (ConcreteCategory.hom (f.hom.app (Opposite.op X))) { down := CategoryStruct.id X }

@[simp]

theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X : C} {F : Sheaf J (Type (max v v'))} (x : F.obj.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X) : (ConcreteCategory.hom ((J.uliftYonedaEquiv.symm x).hom.app Y)) { down := f } = (ConcreteCategory.hom (F.obj.map f.op)) x

theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : C} {F : Sheaf J (Type (max v v'))} (f : (uliftYoneda.{v', v, u} J).obj X ⟶ F) (g : Y ⟶ X) : (ConcreteCategory.hom (F.obj.map g.op)) (J.uliftYonedaEquiv f) = J.uliftYonedaEquiv (CategoryStruct.comp ((uliftYoneda.{v', v, u} J).map g) f)

See also uliftYonedaEquiv_naturality' for a more general version.

theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality' {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} {F : Sheaf J (Type (max v v'))} (f : (uliftYoneda.{v', v, u} J).obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : (ConcreteCategory.hom (F.obj.map g)) (J.uliftYonedaEquiv f) = J.uliftYonedaEquiv (CategoryStruct.comp ((uliftYoneda.{v', v, u} J).map g.unop) f)

Variant of uliftYonedaEquiv_naturality with general g. This is technically strictly more general than uliftYonedaEquiv_naturality, but uliftYonedaEquiv_naturality is sometimes preferable because it can avoid the "motive is not type correct" error.

theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X : C} {F G : Sheaf J (Type (max v v'))} (α : (uliftYoneda.{v', v, u} J).obj X ⟶ F) (β : F ⟶ G) : J.uliftYonedaEquiv (CategoryStruct.comp α β) = (ConcreteCategory.hom (β.hom.app (Opposite.op X))) (J.uliftYonedaEquiv α)

theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : C} (f : X ⟶ Y) : J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map f) = { down := f }

theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_left {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X X' : C} (f : X' ⟶ X) (F : Sheaf J (Type (max v v'))) (x : F.obj.obj (Opposite.op X)) : CategoryStruct.comp ((uliftYoneda.{v', v, u} J).map f) (J.uliftYonedaEquiv.symm x) = J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x)

theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : C) {F F' : Sheaf J (Type (max v v'))} (f : F ⟶ F') (x : F.obj.obj (Opposite.op X)) : CategoryStruct.comp (J.uliftYonedaEquiv.symm x) f = J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (f.hom.app (Opposite.op X))) x)

theorem CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : C} {F : Sheaf J (Type (max v v'))} (f : (uliftYoneda.{v', v, u} J).obj X ⟶ F) (g : Y ⟶ X) : (ConcreteCategory.hom (F.obj.map g.op)) (J.uliftYonedaEquiv f) = (ConcreteCategory.hom (f.hom.app (Opposite.op Y))) { down := g }

See also map_yonedaEquiv' for a more general version.

theorem CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv' {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} {F : Sheaf J (Type (max v v'))} (f : (uliftYoneda.{v', v, u} J).obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : (ConcreteCategory.hom (F.obj.map g)) (J.uliftYonedaEquiv f) = (ConcreteCategory.hom (f.hom.app Y)) { down := g.unop }

Variant of map_uliftYonedaEquiv with general g. This is technically strictly more general than map_uliftYonedaEquiv, but map_uliftYonedaEquiv is sometimes preferable because it can avoid the "motive is not type correct" error.

theorem CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : Sheaf J (Type (max v v'))} (t : F.obj.obj X) : J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f)) t) = CategoryStruct.comp ((uliftYoneda.{v', v, u} J).map f.unop) (J.uliftYonedaEquiv.symm t)

theorem CategoryTheory.GrothendieckTopology.hom_ext_uliftYoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {P Q : Sheaf J (Type (max v v'))} {f g : P ⟶ Q} (h : ∀ (X : C) (p : (uliftYoneda.{v', v, u} J).obj X ⟶ P), CategoryStruct.comp p f = CategoryStruct.comp p g) : f = g

Two morphisms of sheaves of types P ⟶ Q coincide if the precompositions with morphisms uliftYoneda.obj X ⟶ P agree.

def CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : (uliftYoneda.{v', v, u} J).op.comp coyoneda ≅ (evaluation Cᵒᵖ (Type (max v v'))).comp (((Functor.whiskeringRight (Functor Cᵒᵖ (Type (max v v'))) (Type (max v v')) (Type (max (max v v') u))).obj uliftFunctor.{u, max v v'}).comp ((Functor.whiskeringLeft (Sheaf J (Type (max v v'))) (Functor Cᵒᵖ (Type (max v v'))) (Type (max (max v v') u))).obj (sheafToPresheaf J (Type (max v v')))))

A variant of the Yoneda lemma for sheaves with a raise in the universe level.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_hom_apply_hom_app_hom_apply {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (X✝ : Sheaf J (Type (max v' v))) (a✝ : (((evaluation Cᵒᵖ (Type (max v v'))).comp (((Functor.whiskeringRight (Functor Cᵒᵖ (Type (max v v'))) (Type (max v v')) (Type (max (max v v') u))).obj uliftFunctor.{u, max v v'}).comp ((Functor.whiskeringLeft (Sheaf J (Type (max v v'))) (Functor Cᵒᵖ (Type (max v v'))) (Type (max (max v v') u))).obj (sheafToPresheaf J (Type (max v v')))))).obj X).obj X✝) (X✝¹ : Cᵒᵖ) (a✝¹ : (Opposite.unop (((uliftYoneda.{v', v, u} J).comp (sheafToPresheaf J (Type (max v v')))).op.obj X)).obj X✝¹) : (ConcreteCategory.hom (((ConcreteCategory.hom ((J.uliftYonedaOpCompCoyoneda.inv.app X).app X✝)) a✝).hom.app X✝¹)) a✝¹ = ((((CategoryTheory.uliftYonedaOpCompCoyoneda.inv.app X).app X✝.obj).hom' a✝).app X✝¹).hom' (((J.uliftYonedaCompSheafToPresheaf.hom.app (Opposite.unop X)).app X✝¹).hom' a✝¹)

@[simp]

theorem CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_hom_apply_down {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (X✝ : Sheaf J (Type (max v' v))) (a✝ : (((J.yoneda.op.comp (sheafCompose J uliftFunctor.{v', v}).op).comp coyoneda).obj X).obj X✝) : ((ConcreteCategory.hom ((J.uliftYonedaOpCompCoyoneda.hom.app X).app X✝)) a✝).down = CategoryTheory.uliftYonedaEquiv ((CategoryStruct.comp ((sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.inv.app (Opposite.op ((sheafCompose J uliftFunctor.{v', v}).obj (J.yoneda.obj (Opposite.unop X))))).app X✝) (TypeCat.ofHom fun (g : ((uliftYoneda.{v', v, u} J).obj (Opposite.unop X)).obj ⟶ X✝.obj) => CategoryStruct.comp (J.uliftYonedaCompSheafToPresheaf.inv.app (Opposite.unop X)) g)).hom' a✝)

theorem CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (F : Sheaf J (Type (max v v'))) (s : ULift.{u, max v v'} (F.obj.obj X)) : (ConcreteCategory.hom ((J.uliftYonedaOpCompCoyoneda.inv.app X).app F)) s = J.uliftYonedaEquiv.symm s.down

theorem CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (F : Sheaf J (Type (max v v'))) : (J.uliftYonedaOpCompCoyoneda.app X).app F = (J.uliftYonedaEquiv.trans Equiv.ulift.symm).toIso

instance CategoryTheory.GrothendieckTopology.preservesLimitsOfSize_yoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : Limits.PreservesLimitsOfSize.{u_1, u_2, v, max u v, u, max u (v + 1)} J.yoneda

noncomputable def CategoryTheory.GrothendieckTopology.isColimitCofanMkYoneda {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {ι : Type u_1} (X : ι → C) {c : Limits.Cofan X} (H : Sieve.ofArrows X c.inj ∈ J c.pt) [∀ (i : ι), Mono (c.inj i)] (hempty : ∀ (Y : C) (a : Limits.IsInitial Y), ⊥ ∈ J Y) (hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), CategoryStruct.comp a (c.inj i) = CategoryStruct.comp b (c.inj j) → Nonempty (Limits.IsInitial Y)) : Limits.IsColimit (Limits.Cofan.mk (J.yoneda.obj c.pt) fun (i : ι) => J.yoneda.map (c.inj i))

Let { Xᵢ ⟶ Y } be a family of pairwise disjoint maps that form a cover in J. Then its image under the yoneda embedding to J-sheaves is a coproduct.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.GrothendieckTopology.preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {ι : Type u_1} [Limits.CoproductsOfShapeDisjoint C ι] [Limits.HasPullbacks C] [Limits.HasStrictInitialObjects C] (hcov : ∀ {X : ι → C} {c : Limits.Cofan X} (x : Limits.IsColimit c), Sieve.ofArrows X c.inj ∈ J c.pt) (htriv : ∀ (Y : C) (a : Limits.IsInitial Y), ⊥ ∈ J Y) : Limits.PreservesColimitsOfShape (Discrete ι) J.yoneda

If the coproduct inclusions form a covering of J and coproducts are disjoint, the yoneda embedding to J-sheaves preserves coproducts.

theorem CategoryTheory.GrothendieckTopology.subcanonical_of_full_of_faithful {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v', u_1} D] (F : Functor C D) (J : GrothendieckTopology C) (K : GrothendieckTopology D) [F.Full] [F.Faithful] [F.IsContinuous J K] [K.Subcanonical] : J.Subcanonical