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.val.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 = f.val.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.val.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X) : (J.yonedaEquiv.symm x).val.app Y f = F.val.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) : F.val.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) : F.val.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 α β) = β.val.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.val.obj (Opposite.op X)) : CategoryStruct.comp (J.yoneda.map f) (J.yonedaEquiv.symm x) = J.yonedaEquiv.symm (F.val.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.val.obj (Opposite.op X)) : CategoryStruct.comp (J.yonedaEquiv.symm x) f = J.yonedaEquiv.symm (f.val.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) : F.val.map g.op (J.yonedaEquiv f) = f.val.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) : F.val.map g (J.yonedaEquiv f) = f.val.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.val.obj X) : J.yonedaEquiv.symm (F.val.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.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.val.obj (Opposite.op X)

A version of yonedaEquiv for uliftYoneda.

Equations

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

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

def CategoryTheory.GrothendieckTopology.yonedaULiftEquiv {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.val.obj (Opposite.op X)

Alias of CategoryTheory.GrothendieckTopology.uliftYonedaEquiv.

---

A version of yonedaEquiv for uliftYoneda.

Equations

• @CategoryTheory.GrothendieckTopology.yonedaULiftEquiv = @CategoryTheory.GrothendieckTopology.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 = f.val.app (Opposite.op X) { down := CategoryStruct.id X }

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

theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_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 = f.val.app (Opposite.op X) { down := CategoryStruct.id X }

Alias of CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply.

@[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.val.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X) : (J.uliftYonedaEquiv.symm x).val.app Y { down := f } = F.val.map f.op x

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

theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_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.val.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X) : (J.uliftYonedaEquiv.symm x).val.app Y { down := f } = F.val.map f.op x

Alias of CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply.

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) : F.val.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.

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

theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_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) : F.val.map g.op (J.uliftYonedaEquiv f) = J.uliftYonedaEquiv (CategoryStruct.comp ((uliftYoneda.{v', v, u} J).map g) f)

Alias of CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality.

---

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) : F.val.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.

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

theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_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) : F.val.map g (J.uliftYonedaEquiv f) = J.uliftYonedaEquiv (CategoryStruct.comp ((uliftYoneda.{v', v, u} J).map g.unop) f)

Alias of CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality'.

---

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 α β) = β.val.app (Opposite.op X) (J.uliftYonedaEquiv α)

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

theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_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 α β) = β.val.app (Opposite.op X) (J.uliftYonedaEquiv α)

Alias of CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp.

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 }

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

theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_yonedaULift_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 }

Alias of CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map.

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.val.obj (Opposite.op X)) : CategoryStruct.comp ((uliftYoneda.{v', v, u} J).map f) (J.uliftYonedaEquiv.symm x) = J.uliftYonedaEquiv.symm (F.val.map f.op x)

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

theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_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.val.obj (Opposite.op X)) : CategoryStruct.comp ((uliftYoneda.{v', v, u} J).map f) (J.uliftYonedaEquiv.symm x) = J.uliftYonedaEquiv.symm (F.val.map f.op x)

Alias of CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_left.

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.val.obj (Opposite.op X)) : CategoryStruct.comp (J.uliftYonedaEquiv.symm x) f = J.uliftYonedaEquiv.symm (f.val.app (Opposite.op X) x)

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

theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_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.val.obj (Opposite.op X)) : CategoryStruct.comp (J.uliftYonedaEquiv.symm x) f = J.uliftYonedaEquiv.symm (f.val.app (Opposite.op X) x)

Alias of CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right.

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) : F.val.map g.op (J.uliftYonedaEquiv f) = f.val.app (Opposite.op Y) { down := g }

See also map_yonedaEquiv' for a more general version.

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

theorem CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv {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) : F.val.map g.op (J.uliftYonedaEquiv f) = f.val.app (Opposite.op Y) { down := g }

Alias of CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv.

---

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) : F.val.map g (J.uliftYonedaEquiv f) = f.val.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.

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

theorem CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv' {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) : F.val.map g (J.uliftYonedaEquiv f) = f.val.app Y { down := g.unop }

Alias of CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv'.

---

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.val.obj X) : J.uliftYonedaEquiv.symm (F.val.map f t) = CategoryStruct.comp ((uliftYoneda.{v', v, u} J).map f.unop) (J.uliftYonedaEquiv.symm t)

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

theorem CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_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.val.obj X) : J.uliftYonedaEquiv.symm (F.val.map f t) = CategoryStruct.comp ((uliftYoneda.{v', v, u} J).map f.unop) (J.uliftYonedaEquiv.symm t)

Alias of CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_map.

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.

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

theorem CategoryTheory.GrothendieckTopology.hom_ext_yonedaULift {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

Alias of CategoryTheory.GrothendieckTopology.hom_ext_uliftYoneda.

---

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