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
🔸 coverage
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.

Instances For
    source
    📐 coverage
    @[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
    📐 coverage
    @[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
    📐 coverage
    @[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
    📐 coverage
    @[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
    📐 coverage
    @[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
    📐 coverage
    @[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
    📐 coverage
    @[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
    📐 coverage
    @[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
    🔸 coverage
    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.

    Instances For
      source
      📐 coverage
      @[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
      📐 coverage
      @[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
      source
      🔸 coverage
      @[deprecated CategoryTheory.Subfunctor.equivalenceMonoOver (since := "2025-12-11")]
      def CategoryTheory.Subfunctor.Subpresheaf.equivalenceMonoOver {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) :
      Subfunctor F ≌ MonoOver F

      Alias of CategoryTheory.Subfunctor.equivalenceMonoOver.

      The equivalence of categories Subfunctor F ≌ MonoOver F.

      Instances For
        source
        📐 coverage
        @[deprecated CategoryTheory.Subfunctor.range_subobjectMk_ι (since := "2025-12-11")]
        theorem CategoryTheory.Subfunctor.Subpresheaf.range_subobjectMk_ι {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (A : Subfunctor F) :
        Subfunctor.range (Subobject.mk A.ι).arrow = A

        Alias of CategoryTheory.Subfunctor.range_subobjectMk_ι.

        source
        📐 coverage
        @[deprecated CategoryTheory.Subfunctor.subobjectMk_range_arrow (since := "2025-12-11")]
        theorem CategoryTheory.Subfunctor.Subpresheaf.subobjectMk_range_arrow {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (X : Subobject F) :
        Subobject.mk (Subfunctor.range X.arrow).ι = X

        Alias of CategoryTheory.Subfunctor.subobjectMk_range_arrow.

        source
        🔸 coverage
        @[deprecated CategoryTheory.Subfunctor.orderIsoSubobject (since := "2025-12-11")]
        def CategoryTheory.Subfunctor.Subpresheaf.orderIsoSubobject {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) :
        Subfunctor F ≃o Subobject F

        Alias of CategoryTheory.Subfunctor.orderIsoSubobject.

        The order isomorphism Subfunctor F ≃o MonoOver F.

        Instances For