Comparison between Subfunctor, MonoOver and Subobject

Given a type-valued functor F : C ⥤ Type w, we define an equivalence of categories Subfunctor.equivalenceMonoOver F : Subfunctor F ≌ MonoOver F and an order isomorphism Subfunctor.orderIsoSubject F : Subfunctor F ≃o Subobject F.

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

The equivalence of categories Subfunctor F ≌ MonoOver F.

Equations

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

@[simp]

theorem CategoryTheory.Subfunctor.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.Subfunctor.equivalenceMonoOver_functor_obj {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) (A : Subfunctor F) : (equivalenceMonoOver F).functor.obj A = MonoOver.mk A.ι

@[simp]

theorem CategoryTheory.Subfunctor.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.Subfunctor.equivalenceMonoOver_functor_map {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {A B : Subfunctor F} (f : A ⟶ B) : (equivalenceMonoOver F).functor.map f = MonoOver.homMk (homOfLe ⋯) ⋯

@[simp]

theorem CategoryTheory.Subfunctor.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.Subfunctor.equivalenceMonoOver_unitIso {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : (equivalenceMonoOver F).unitIso = NatIso.ofComponents (fun (A : Subfunctor F) => eqToIso ⋯) ⋯

@[simp]

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

@[simp]

theorem CategoryTheory.Subfunctor.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.Subfunctor.orderIsoSubobject {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) : Subfunctor F ≃o Subobject F

The order isomorphism Subfunctor F ≃o MonoOver F.

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.Subfunctor.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