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.28)).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.yonedaULift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] : Functor C (Sheaf J (Type (max v v')))

The Yoneda embedding into a category of sheaves taking values in sets possibly larger than the morphisms in the defining site.

Equations

• CategoryTheory.GrothendieckTopology.yonedaULift.{?u.21, ?u.20, ?u.19} J = J.yoneda.comp (CategoryTheory.sheafCompose J CategoryTheory.uliftFunctor.{?u.21, ?u.20})

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'))} : ((yonedaULift.{v', v, u} J).obj X ⟶ F) ≃ F.val.obj (Opposite.op X)

A version of yonedaEquiv for yonedaULift.

Equations

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

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 : (yonedaULift.{v', v, u} J).obj X ⟶ F) : J.yonedaULiftEquiv f = f.val.app (Opposite.op X) { down := CategoryStruct.id X }

@[simp]

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.yonedaULiftEquiv.symm x).val.app Y { down := f } = F.val.map f.op x

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 : (yonedaULift.{v', v, u} J).obj X ⟶ F) (g : Y ⟶ X) : F.val.map g.op (J.yonedaULiftEquiv f) = J.yonedaULiftEquiv (CategoryStruct.comp ((yonedaULift.{v', v, u} J).map g) f)

See also yonedaEquiv_naturality' for a more general version.

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 : (yonedaULift.{v', v, u} J).obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : F.val.map g (J.yonedaULiftEquiv f) = J.yonedaULiftEquiv (CategoryStruct.comp ((yonedaULift.{v', v, u} J).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.yonedaULiftEquiv_comp {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X : C} {F G : Sheaf J (Type (max v v'))} (α : (yonedaULift.{v', v, u} J).obj X ⟶ F) (β : F ⟶ G) : J.yonedaULiftEquiv (CategoryStruct.comp α β) = β.val.app (Opposite.op X) (J.yonedaULiftEquiv α)

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.yonedaULiftEquiv ((yonedaULift.{v', v, u} J).map f) = { down := f }

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 ((yonedaULift.{v', v, u} J).map f) (J.yonedaULiftEquiv.symm x) = J.yonedaULiftEquiv.symm (F.val.map f.op x)

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.yonedaULiftEquiv.symm x) f = J.yonedaULiftEquiv.symm (f.val.app (Opposite.op X) x)

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 : (yonedaULift.{v', v, u} J).obj X ⟶ F) (g : Y ⟶ X) : F.val.map g.op (J.yonedaULiftEquiv f) = f.val.app (Opposite.op Y) { down := g }

See also map_yonedaEquiv' for a more general version.

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 : (yonedaULift.{v', v, u} J).obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y) : F.val.map g (J.yonedaULiftEquiv f) = f.val.app Y { down := 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.yonedaULeftEquiv_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.yonedaULiftEquiv.symm (F.val.map f t) = CategoryStruct.comp ((yonedaULift.{v', v, u} J).map f.unop) (J.yonedaULiftEquiv.symm t)

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 : (yonedaULift.{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 yoneda.obj X ⟶ P agree.