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

Equations

• CategoryTheory.ObjectProperty.FullSubcategory.category P = CategoryTheory.InducedCategory.category CategoryTheory.ObjectProperty.FullSubcategory.obj

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

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 = CategoryStruct.comp f g

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

Equations

• P.ι = CategoryTheory.inducedFunctor CategoryTheory.ObjectProperty.FullSubcategory.obj

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

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

Equations

• P.fullyFaithfulι = CategoryTheory.fullyFaithfulInducedFunctor CategoryTheory.ObjectProperty.FullSubcategory.obj

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 : P.ι.obj X ≅ P.ι.obj Y) : X ≅ Y

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

Equations

• P.isoMk e = { hom := e.hom, inv := e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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 = f

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

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.

Equations

• One or more equations did not get rendered due to their size.

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

@[deprecated "use ιOfLECompιIso" (since := "2025-03-04")]

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

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

Equations

• CategoryTheory.ObjectProperty.ιOfLECompιIso h = CategoryTheory.Iso.refl ((CategoryTheory.ObjectProperty.ιOfLE h).comp 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.

Equations

• P.lift F hF = { obj := fun (X : C) => { obj := F.obj X, property := ⋯ }, map := fun {X Y : C} (f : X ⟶ Y) => F.map f, map_id := ⋯, map_comp := ⋯ }

@[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 = F.map f

@[deprecated "use liftCompιIso" (since := "2025-03-04")]

theorem CategoryTheory.ObjectProperty.FullSubcategory.lift_comp_inclusion_eq {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

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.

Equations

• P.liftCompιIso F hF = CategoryTheory.Iso.refl ((P.lift F hF).comp P.ι)

@[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 _.

Equations

• P.liftCompιOfLEIso F hF h = CategoryTheory.Iso.refl ((P.lift F hF).comp (CategoryTheory.ObjectProperty.ιOfLE h))

@[deprecated "Use liftCompιOfLEIso" (since := "2025-03-04")]

theorem CategoryTheory.ObjectProperty.FullSubcategory.lift_comp_map {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 ⋯

@[deprecated CategoryTheory.ObjectProperty.FullSubcategory (since := "2025-03-04")]

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

Alias of CategoryTheory.ObjectProperty.FullSubcategory.

---

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.

Equations

• @CategoryTheory.FullSubcategory = @CategoryTheory.ObjectProperty.FullSubcategory

@[deprecated CategoryTheory.ObjectProperty.ι (since := "2025-03-04")]

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

Alias of CategoryTheory.ObjectProperty.ι.

---

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

Equations

• @CategoryTheory.fullSubcategoryInclusion = @CategoryTheory.ObjectProperty.ι

@[deprecated CategoryTheory.ObjectProperty.ι_obj (since := "2025-03-04")]

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

Alias of CategoryTheory.ObjectProperty.ι_obj.

@[deprecated CategoryTheory.ObjectProperty.ι_map (since := "2025-03-04")]

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

Alias of CategoryTheory.ObjectProperty.ι_map.

@[deprecated CategoryTheory.ObjectProperty.fullyFaithfulι (since := "2025-03-04")]

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

Alias of CategoryTheory.ObjectProperty.fullyFaithfulι.

---

The inclusion of a full subcategory is fully faithful.

Equations

• @CategoryTheory.fullyFaithfulFullSubcategoryInclusion = @CategoryTheory.ObjectProperty.fullyFaithfulι

@[deprecated CategoryTheory.ObjectProperty.ιOfLE (since := "2025-03-04")]

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

Alias of CategoryTheory.ObjectProperty.ιOfLE.

---

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

Equations

• @CategoryTheory.FullSubcategory.map = @CategoryTheory.ObjectProperty.ιOfLE

@[deprecated CategoryTheory.ObjectProperty.lift (since := "2025-03-04")]

def CategoryTheory.FullSubcategory.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

Alias of CategoryTheory.ObjectProperty.lift.

---

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

Equations

• @CategoryTheory.FullSubcategory.lift = @CategoryTheory.ObjectProperty.lift

@[deprecated CategoryTheory.ObjectProperty.liftCompιIso (since := "2025-03-04")]

def CategoryTheory.FullSubcategory.lift_comp_inclusion {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

Alias of CategoryTheory.ObjectProperty.liftCompιIso.

---

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

Equations

• @CategoryTheory.FullSubcategory.lift_comp_inclusion = @CategoryTheory.ObjectProperty.liftCompιIso

@[deprecated CategoryTheory.ObjectProperty.ι_obj_lift_obj (since := "2025-03-04")]

theorem CategoryTheory.fullSubcategoryInclusion_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

Alias of CategoryTheory.ObjectProperty.ι_obj_lift_obj.

@[deprecated CategoryTheory.ObjectProperty.ι_obj_lift_map (since := "2025-03-04")]

theorem CategoryTheory.fullSubcategoryInclusion_map_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

Alias of CategoryTheory.ObjectProperty.ι_obj_lift_map.