Subobjects presheaf

Following Section I.3 of [Sheaves in Geometry and Logic][MM92], 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 category 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][MM92]

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 category 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_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (X : Cᵒᵖ) : (presheaf C).obj X = CategoryTheory.Subobject (Opposite.unop X)

@[simp]

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