Documentation

Mathlib.CategoryTheory.Subfunctor.Subobject

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.

source
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.
Instances For
    source
    @[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 ⋯
    source
    @[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.ι
    source
    @[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 ⋯) ⋯
    source
    @[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 ⋯) ⋯
    source
    @[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
    source
    @[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 ⋯) ⋯
    source
    @[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
    source
    @[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
    source
    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.
    Instances For
      source
      @[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.ι
      source
      @[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