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.

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

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

instance CategoryTheory.ObjectProperty.instIsEquivalenceFullSubcategoryIsoClosureιOfLE {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} : (ιOfLE ⋯).IsEquivalence

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.

@[simp]

theorem CategoryTheory.ObjectProperty.topEquivalence_inverse (C : Type u) [Category.{v, u} C] : (topEquivalence C).inverse = ⊤.lift (Functor.id C) ⋯

@[simp]

theorem CategoryTheory.ObjectProperty.topEquivalence_unitIso (C : Type u) [Category.{v, u} C] : (topEquivalence C).unitIso = Iso.refl (Functor.id ⊤.FullSubcategory)

@[simp]

theorem CategoryTheory.ObjectProperty.topEquivalence_counitIso (C : Type u) [Category.{v, u} C] : (topEquivalence C).counitIso = Iso.refl ((⊤.lift (Functor.id C) ⋯).comp ⊤.ι)

@[simp]

theorem CategoryTheory.ObjectProperty.topEquivalence_functor (C : Type u) [Category.{v, u} C] : (topEquivalence C).functor = ⊤.ι

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.

@[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)

@[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) ⋯

@[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) ⋯

@[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)