Comparison between Subpresheaf, MonoOver and Subobject

Given a presheaf of types F : Cᵒᵖ ⥤ Type w, we define an equivalence of categories Subpresheaf.equivalenceMonoOver F : Subpresheaf F ≌ MonoOver F and an order isomorphism Subpresheaf.orderIsoSubject F : Subpresheaf F ≃o Subobject F.

noncomputable def CategoryTheory.Subpresheaf.equivalenceMonoOver {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) : Subpresheaf F ≌ MonoOver F

The equivalence of categories Subpresheaf F ≌ MonoOver F.

@[simp]

theorem CategoryTheory.Subpresheaf.equivalenceMonoOver_inverse_obj {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) (X : MonoOver F) : (equivalenceMonoOver F).inverse.obj X = range X.arrow

@[simp]

theorem CategoryTheory.Subpresheaf.equivalenceMonoOver_counitIso {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) : (equivalenceMonoOver F).counitIso = NatIso.ofComponents (fun (X : MonoOver F) => MonoOver.isoMk (asIso (toRange X.arrow)).symm ⋯) ⋯

@[simp]

theorem CategoryTheory.Subpresheaf.equivalenceMonoOver_functor_obj {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) (A : Subpresheaf F) : (equivalenceMonoOver F).functor.obj A = MonoOver.mk' A.ι

@[simp]

theorem CategoryTheory.Subpresheaf.equivalenceMonoOver_inverse_map {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) {X Y : MonoOver F} (f : X ⟶ Y) : (equivalenceMonoOver F).inverse.map f = homOfLE ⋯

@[simp]

theorem CategoryTheory.Subpresheaf.equivalenceMonoOver_unitIso {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) : (equivalenceMonoOver F).unitIso = NatIso.ofComponents (fun (A : Subpresheaf F) => eqToIso ⋯) ⋯

@[simp]

theorem CategoryTheory.Subpresheaf.equivalenceMonoOver_functor_map {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) {A B : Subpresheaf F} (f : A ⟶ B) : (equivalenceMonoOver F).functor.map f = MonoOver.homMk (homOfLe ⋯) ⋯

@[simp]

theorem CategoryTheory.Subpresheaf.range_subobjectMk_ι {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (A : Subpresheaf F) : range (Subobject.mk A.ι).arrow = A

@[simp]

theorem CategoryTheory.Subpresheaf.subobjectMk_range_arrow {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (X : Subobject F) : Subobject.mk (range X.arrow).ι = X

noncomputable def CategoryTheory.Subpresheaf.orderIsoSubobject {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) : Subpresheaf F ≃o Subobject F

The order isomorphism Subpresheaf F ≃o MonoOver F.

@[simp]

theorem CategoryTheory.Subpresheaf.orderIsoSubobject_symm_apply {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) (X : Subobject F) : (RelIso.symm (orderIsoSubobject F)) X = range X.arrow

@[simp]

theorem CategoryTheory.Subpresheaf.orderIsoSubobject_apply {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) (A : Subpresheaf F) : (orderIsoSubobject F) A = Subobject.mk A.ι