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.

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

@[simp]

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

P.ι.obj X = X.obj

source

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

source

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

source

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

P.ι.Full

source

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

P.ι.Faithful

source

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 := ⋯ }

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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.

source

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

(ιOfLE h).Full

source

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

(ιOfLE h).Faithful

source

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

source

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

source

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 := ⋯ }

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

instance CategoryTheory.ObjectProperty.instFaithfulFullSubcategoryLift_1 {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

source

instance CategoryTheory.ObjectProperty.instFullFullSubcategoryLift_1 {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

source

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

source

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

source

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

Equations

@CategoryTheory.FullSubcategory = @CategoryTheory.ObjectProperty.FullSubcategory

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Documentation

Mathlib.CategoryTheory.ObjectProperty.FullSubcategory

The full subcategory associated to a property of objects #