Documentation

Mathlib.CategoryTheory.ObjectProperty.Equivalence

Equivalence of full subcategories #

The inclusion functor P.FullSubcategory ⥤ Q.FullSubcategory induced by an inequality P ≤ Q in ObjectProperty C is an equivalence iff Q ≤ P.isoClosure.

source
theorem CategoryTheory.ObjectProperty.essSurj_ιOfLE_iff {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} (h : P ≤ Q) :
(ιOfLE h).EssSurj ↔ Q ≤ P.isoClosure
source
theorem CategoryTheory.ObjectProperty.isEquivalence_ιOfLE_iff {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} (h : P ≤ Q) :
(ιOfLE h).IsEquivalence ↔ Q ≤ P.isoClosure
source
instance CategoryTheory.ObjectProperty.instIsEquivalenceFullSubcategoryIsoClosureιOfLE {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} :
(ιOfLE ⋯).IsEquivalence
source
def CategoryTheory.ObjectProperty.topEquivalence (C : Type u) [Category.{v, u} C] :
⊤.FullSubcategory ≌ C

The equivalence between the full subcategory ⊤ of a category C and C itself.

Instances For
    source
    @[simp]
    theorem CategoryTheory.ObjectProperty.topEquivalence_counitIso (C : Type u) [Category.{v, u} C] :
    (topEquivalence C).counitIso = Iso.refl ((⊤.lift (Functor.id C) ⋯).comp ⊤.ι)
    source
    @[simp]
    theorem CategoryTheory.ObjectProperty.topEquivalence_unitIso (C : Type u) [Category.{v, u} C] :
    (topEquivalence C).unitIso = Iso.refl (Functor.id ⊤.FullSubcategory)
    source
    @[simp]
    theorem CategoryTheory.ObjectProperty.topEquivalence_inverse (C : Type u) [Category.{v, u} C] :
    (topEquivalence C).inverse = ⊤.lift (Functor.id C) ⋯
    source
    @[simp]
    theorem CategoryTheory.ObjectProperty.topEquivalence_functor (C : Type u) [Category.{v, u} C] :
    (topEquivalence C).functor = ⊤.ι
    source
    theorem CategoryTheory.ObjectProperty.isEquivalence_ι {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (h : P = ⊤) :
    P.ι.IsEquivalence
    source
    def CategoryTheory.Equivalence.congrFullSubcategory {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {P : ObjectProperty C} {Q : ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) :
    P.FullSubcategory ≌ Q.FullSubcategory

    The equivalence of categories between two fullsubcategories P and Q of categories C and D that is induced by an equivalence e : C ≌ D when Q.inverseImage e.functor = P and Q respects isomorphisms.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.Equivalence.congrFullSubcategory_functor {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {P : ObjectProperty C} {Q : ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) :
      (e.congrFullSubcategory h).functor = Q.lift (P.ι.comp e.functor) ⋯
      source
      @[simp]
      theorem CategoryTheory.Equivalence.congrFullSubcategory_unitIso {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {P : ObjectProperty C} {Q : ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) :
      (e.congrFullSubcategory h).unitIso = (P.fullyFaithfulι.whiskeringRight P.FullSubcategory).preimageIso (P.ι.isoWhiskerLeft e.unitIso)
      source
      @[simp]
      theorem CategoryTheory.Equivalence.congrFullSubcategory_inverse {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {P : ObjectProperty C} {Q : ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) :
      (e.congrFullSubcategory h).inverse = P.lift (Q.ι.comp e.inverse) ⋯
      source
      @[simp]
      theorem CategoryTheory.Equivalence.congrFullSubcategory_counitIso {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {P : ObjectProperty C} {Q : ObjectProperty D} (e : C ≌ D) [Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P) :
      (e.congrFullSubcategory h).counitIso = (Q.fullyFaithfulι.whiskeringRight Q.FullSubcategory).preimageIso (Q.ι.isoWhiskerLeft e.counitIso)