Subobjects presheaf

Following Section I.3 of Sheaves in Geometry and Logic, we define the subobjects presheaf Subobject.presheaf C mapping any object X to its type of subobjects Subobject X.

Main definitions

Let C refer to a category with pullbacks.

• CategoryTheory.Subobject.presheaf C is the presheaf that sends every object X : C to its type of subobjects Subobject X, and every morphism f : X ⟶ Y to the function Subobject Y → Subobject X that maps every subobject of Y to its pullback along f.

References

• S. MacLane and I. Moerdijk, Sheaves in geometry and logic: A first introduction to topos theory

Tags

subobject, representable functor, presheaf, topos theory

noncomputable def Subobject.presheaf (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Functor Cᵒᵖ (Type (max u v))

This is the presheaf that sends every object X : C to its type of subobjects Subobject X, and every morphism f : X ⟶ Y to the function Subobject Y → Subobject X that maps every subobject of Y to its pullback along f.

Equations

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

@[simp]

theorem Subobject.presheaf_map (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (presheaf C).map f = TypeCat.ofHom (CategoryTheory.Subobject.pullback f.unop).obj

@[simp]

theorem Subobject.presheaf_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (X : Cᵒᵖ) : (presheaf C).obj X = CategoryTheory.Subobject (Opposite.unop X)