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.

Equations
    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.

      Equations
        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.

          Equations
            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.

              Equations
                Instances For