# 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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For