The full subcategory associated to a property of objects

Given a category C and P : ObjectProperty C, we define a category structure on the type P.FullSubcategory of objects in C satisfying P.

structure CategoryTheory.ObjectProperty.FullSubcategory {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Type u

A subtype-like structure for full subcategories. Morphisms just ignore the property. We don't use actual subtypes since the simp-normal form ↑X of X.val does not work well for full subcategories.

• obj : C

  The category of which this is a full subcategory

• property : P self.obj

  The predicate satisfied by all objects in this subcategory

theorem CategoryTheory.ObjectProperty.FullSubcategory.ext {C : Type u} {inst✝ : Category.{v, u} C} {P : ObjectProperty C} {x y : P.FullSubcategory} (obj : x.obj = y.obj) : x = y

theorem CategoryTheory.ObjectProperty.FullSubcategory.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {P : ObjectProperty C} {x y : P.FullSubcategory} : x = y ↔ x.obj = y.obj

instance CategoryTheory.ObjectProperty.FullSubcategory.category {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Category.{v, u} P.FullSubcategory

theorem CategoryTheory.ObjectProperty.hom_ext {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X Y : P.FullSubcategory} {f g : X ⟶ Y} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.ObjectProperty.hom_ext_iff {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : P.FullSubcategory} {f g : X ⟶ Y} : f = g ↔ f.hom = g.hom

def CategoryTheory.ObjectProperty.ι {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Functor P.FullSubcategory C

The forgetful functor from a full subcategory into the original category ("forgetting" the condition).

@[simp]

theorem CategoryTheory.ObjectProperty.ι_obj {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X : P.FullSubcategory} : P.ι.obj X = X.obj

@[simp]

theorem CategoryTheory.ObjectProperty.ι_map {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X Y : P.FullSubcategory} {f : X ⟶ Y} : P.ι.map f = f.hom

theorem CategoryTheory.ObjectProperty.prop_ι_obj {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : P.FullSubcategory) : P (P.ι.obj X)

@[simp]

theorem CategoryTheory.ObjectProperty.FullSubcategory.id_hom {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : P.FullSubcategory) : (CategoryStruct.id X).hom = CategoryStruct.id X.obj

@[simp]

theorem CategoryTheory.ObjectProperty.FullSubcategory.comp_hom {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.ObjectProperty.FullSubcategory.comp_hom_assoc {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z.obj ⟶ Z✝) : CategoryStruct.comp (CategoryStruct.comp f g).hom h = CategoryStruct.comp f.hom (CategoryStruct.comp g.hom h)

@[deprecated CategoryTheory.ObjectProperty.FullSubcategory.id_hom (since := "2025-12-18")]

theorem CategoryTheory.ObjectProperty.FullSubcategory.id_def {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : P.FullSubcategory) : (CategoryStruct.id X).hom = CategoryStruct.id X.obj

Alias of CategoryTheory.ObjectProperty.FullSubcategory.id_hom.

@[deprecated CategoryTheory.ObjectProperty.FullSubcategory.comp_hom (since := "2025-12-18")]

theorem CategoryTheory.ObjectProperty.FullSubcategory.comp_def {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

Alias of CategoryTheory.ObjectProperty.FullSubcategory.comp_hom.

def CategoryTheory.ObjectProperty.homMk {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : P.FullSubcategory} (f : X.obj ⟶ Y.obj) : X ⟶ Y

Constructor for morphisms in a full subcategory.

@[simp]

theorem CategoryTheory.ObjectProperty.homMk_hom {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : P.FullSubcategory} (f : X.obj ⟶ Y.obj) : (homMk f).hom = f

theorem CategoryTheory.ObjectProperty.homMk_surjective {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : P.FullSubcategory} : Function.Surjective homMk

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.fullyFaithfulι {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.ι.FullyFaithful

The inclusion of a full subcategory is fully faithful.

instance CategoryTheory.ObjectProperty.full_ι {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.ι.Full

instance CategoryTheory.ObjectProperty.faithful_ι {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.ι.Faithful

def CategoryTheory.ObjectProperty.isoMk {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X Y : P.FullSubcategory} (e : X.obj ≅ Y.obj) : X ≅ Y

Constructor for isomorphisms in P.FullSubcategory when P : ObjectProperty C.

@[simp]

theorem CategoryTheory.ObjectProperty.isoMk_inv {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X Y : P.FullSubcategory} (e : X.obj ≅ Y.obj) : (P.isoMk e).inv = homMk e.inv

@[simp]

theorem CategoryTheory.ObjectProperty.isoMk_hom {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X Y : P.FullSubcategory} (e : X.obj ≅ Y.obj) : (P.isoMk e).hom = homMk e.hom

@[simp]

theorem CategoryTheory.ObjectProperty.isoHom_inv_id_hom {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) : CategoryStruct.comp e.hom.hom e.inv.hom = CategoryStruct.id X.obj

@[simp]

theorem CategoryTheory.ObjectProperty.isoHom_inv_id_hom_assoc {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) {Z : C} (h : X.obj ⟶ Z) : CategoryStruct.comp e.hom.hom (CategoryStruct.comp e.inv.hom h) = h

@[simp]

theorem CategoryTheory.ObjectProperty.isoInv_hom_id_hom {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) : CategoryStruct.comp e.inv.hom e.hom.hom = CategoryStruct.id Y.obj

@[simp]

theorem CategoryTheory.ObjectProperty.isoInv_hom_id_hom_assoc {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) {Z : C} (h : Y.obj ⟶ Z) : CategoryStruct.comp e.inv.hom (CategoryStruct.comp e.hom.hom h) = h

def CategoryTheory.ObjectProperty.ιOfLE {C : Type u} [Category.{v, u} C] {P P' : ObjectProperty C} (h : P ≤ P') : Functor P.FullSubcategory P'.FullSubcategory

If P and P' are properties of objects such that P ≤ P', there is an induced functor P.FullSubcategory ⥤ P'.FullSubcategory.

@[simp]

theorem CategoryTheory.ObjectProperty.ιOfLE_obj_obj {C : Type u} [Category.{v, u} C] {P P' : ObjectProperty C} (h : P ≤ P') (X : P.FullSubcategory) : ((ιOfLE h).obj X).obj = X.obj

@[simp]

theorem CategoryTheory.ObjectProperty.ιOfLE_map {C : Type u} [Category.{v, u} C] {P P' : ObjectProperty C} (h : P ≤ P') {X✝ Y✝ : P.FullSubcategory} (f : X✝ ⟶ Y✝) : (ιOfLE h).map f = homMk f.hom

def CategoryTheory.ObjectProperty.fullyFaithfulιOfLE {C : Type u} [Category.{v, u} C] {P P' : ObjectProperty C} (h : P ≤ P') : (ιOfLE h).FullyFaithful

If h : P ≤ P', then ιOfLE h is fully faithful.

instance CategoryTheory.ObjectProperty.full_ιOfLE {C : Type u} [Category.{v, u} C] {P P' : ObjectProperty C} (h : P ≤ P') : (ιOfLE h).Full

instance CategoryTheory.ObjectProperty.faithful_ιOfLE {C : Type u} [Category.{v, u} C] {P P' : ObjectProperty C} (h : P ≤ P') : (ιOfLE h).Faithful

def CategoryTheory.ObjectProperty.ιOfLECompιIso {C : Type u} [Category.{v, u} C] {P P' : ObjectProperty C} (h : P ≤ P') : (ιOfLE h).comp P'.ι ≅ P.ι

If h : P ≤ P' is an inequality of properties of objects, this is the obvious isomorphism ιOfLE h ⋙ P'.ι ≅ P.ι.

def CategoryTheory.ObjectProperty.lift {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty D) (F : Functor C D) (hF : ∀ (X : C), P (F.obj X)) : Functor C P.FullSubcategory

A functor which maps objects to objects satisfying a certain property induces a lift through the full subcategory of objects satisfying that property.

@[simp]

theorem CategoryTheory.ObjectProperty.lift_obj_obj {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty D) (F : Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) : ((P.lift F hF).obj X).obj = F.obj X

@[simp]

theorem CategoryTheory.ObjectProperty.lift_map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty D) (F : Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (P.lift F hF).map f = homMk (F.map f)

def CategoryTheory.ObjectProperty.liftCompιIso {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty D) (F : Functor C D) (hF : ∀ (X : C), P (F.obj X)) : (P.lift F hF).comp P.ι ≅ F

Composing the lift of a functor through a full subcategory with the inclusion yields the original functor. This is actually true definitionally.

@[simp]

theorem CategoryTheory.ObjectProperty.ι_obj_lift_obj {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty D) (F : Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) : P.ι.obj ((P.lift F hF).obj X) = F.obj X

@[simp]

theorem CategoryTheory.ObjectProperty.ι_obj_lift_map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty D) (F : Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X Y : C} (f : X ⟶ Y) : P.ι.map ((P.lift F hF).map f) = F.map f

instance CategoryTheory.ObjectProperty.instFaithfulFullSubcategoryLift {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty D) (F : Functor C D) (hF : ∀ (X : C), P (F.obj X)) [F.Faithful] : (P.lift F hF).Faithful

instance CategoryTheory.ObjectProperty.instFullFullSubcategoryLift {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty D) (F : Functor C D) (hF : ∀ (X : C), P (F.obj X)) [F.Full] : (P.lift F hF).Full

def CategoryTheory.ObjectProperty.liftCompιOfLEIso {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty D) {Q : ObjectProperty D} (F : Functor C D) (hF : ∀ (X : C), P (F.obj X)) (h : P ≤ Q) : (P.lift F hF).comp (ιOfLE h) ≅ Q.lift F ⋯

When h : P ≤ Q, this is the canonical isomorphism P.lift F hF ⋙ ιOfLE h ≅ Q.lift F _.