mathlib documentation

category_theory.full_subcategory

Induced categories and full subcategories #

Given a category D and a function F : C → Dfrom a type C to the objects of D, there is an essentially unique way to give C a category structure such that F becomes a fully faithful functor, namely by taking $$ Hom_C(X, Y) = Hom_D(FX, FY) $$. We call this the category induced from D along F.

As a special case, if C is a subtype of D, this produces the full subcategory of D on the objects belonging to C. In general the induced category is equivalent to the full subcategory of D on the image of F.

Implementation notes #

It looks odd to make D an explicit argument of induced_category, when it is determined by the argument F anyways. The reason to make D explicit is in order to control its syntactic form, so that instances like induced_category.has_forget₂ (elsewhere) refer to the correct form of D. This is used to set up several algebraic categories like

def CommMon : Type (u+1) := induced_category Mon (bundled.map @comm_monoid.to_monoid) -- not induced_category (bundled monoid) (bundled.map @comm_monoid.to_monoid), -- even though Mon = bundled monoid!

source
@[nolint]
def category_theory.induced_category {C : Type u₁} (D : Type u₂) [category_theory.category D] (F : C → D) :
Type u₁

induced_category D F, where F : C → D, is a typeclass synonym for C, which provides a category structure so that the morphisms X ⟶ Y are the morphisms in D from F X to F Y.

Equations
source
@[protected, instance]
def category_theory.induced_category.has_coe_to_sort {C : Type u₁} {D : Type u₂} [category_theory.category D] (F : C → D) {α : Sort u_1} [has_coe_to_sort D α] :
has_coe_to_sort (category_theory.induced_category D F) α
Equations
source
@[protected, instance]
def category_theory.induced_category.category {C : Type u₁} {D : Type u₂} [category_theory.category D] (F : C → D) :
category_theory.category (category_theory.induced_category D F)
Equations
source
def category_theory.induced_functor {C : Type u₁} {D : Type u₂} [category_theory.category D] (F : C → D) :
category_theory.induced_category D F ⥤ D

The forgetful functor from an induced category to the original category, forgetting the extra data.

Equations
source
@[simp]
theorem category_theory.induced_functor_obj {C : Type u₁} {D : Type u₂} [category_theory.category D] (F : C → D) (ᾰ : C) :
(category_theory.induced_functor F).obj ᾰ = F ᾰ
source
@[simp]
theorem category_theory.induced_functor_map {C : Type u₁} {D : Type u₂} [category_theory.category D] (F : C → D) (x y : category_theory.induced_category D F) (f : x ⟶ y) :
(category_theory.induced_functor F).map f = f
source
@[protected, instance]
def category_theory.induced_category.full {C : Type u₁} {D : Type u₂} [category_theory.category D] (F : C → D) :
category_theory.full (category_theory.induced_functor F)
Equations
source
@[protected, instance]
def category_theory.induced_category.faithful {C : Type u₁} {D : Type u₂} [category_theory.category D] (F : C → D) :
category_theory.faithful (category_theory.induced_functor F)
source
@[protected, instance]
def category_theory.full_subcategory {C : Type u₁} [category_theory.category C] (Z : C → Prop) :
category_theory.category {X // Z X}

The category structure on a subtype; morphisms just ignore the property.

See https://stacks.math.columbia.edu/tag/001D. We do not define 'strictly full' subcategories.

Equations
source
def category_theory.full_subcategory_inclusion {C : Type u₁} [category_theory.category C] (Z : C → Prop) :
{X // Z X} ⥤ C

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

Equations
source
@[simp]
theorem category_theory.full_subcategory_inclusion.obj {C : Type u₁} [category_theory.category C] (Z : C → Prop) {X : {X // Z X}} :
(category_theory.full_subcategory_inclusion Z).obj X = X.val
source
@[simp]
theorem category_theory.full_subcategory_inclusion.map {C : Type u₁} [category_theory.category C] (Z : C → Prop) {X Y : {X // Z X}} {f : X ⟶ Y} :
(category_theory.full_subcategory_inclusion Z).map f = f
source
@[protected, instance]
def category_theory.full_subcategory.full {C : Type u₁} [category_theory.category C] (Z : C → Prop) :
category_theory.full (category_theory.full_subcategory_inclusion Z)
Equations
source
@[protected, instance]
def category_theory.full_subcategory.faithful {C : Type u₁} [category_theory.category C] (Z : C → Prop) :
category_theory.faithful (category_theory.full_subcategory_inclusion Z)
source
def category_theory.full_subcategory.map {C : Type u₁} [category_theory.category C] {Z Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) :
{X // Z X} ⥤ {X // Z' X}

An implication of predicates Z → Z' induces a functor between full subcategories.

Equations
source
@[simp]
theorem category_theory.full_subcategory.map_obj_coe {C : Type u₁} [category_theory.category C] {Z Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) (X : {X // Z X}) :
↑((category_theory.full_subcategory.map h).obj X) = X.val
source
@[simp]
theorem category_theory.full_subcategory.map_map {C : Type u₁} [category_theory.category C] {Z Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) (X Y : {X // Z X}) (f : X ⟶ Y) :
(category_theory.full_subcategory.map h).map f = f
source
@[protected, instance]
def category_theory.full_subcategory.map.full {C : Type u₁} [category_theory.category C] {Z Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) :
category_theory.full (category_theory.full_subcategory.map h)
Equations
source
@[protected, instance]
def category_theory.full_subcategory.map.faithful {C : Type u₁} [category_theory.category C] {Z Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) :
category_theory.faithful (category_theory.full_subcategory.map h)
source
@[simp]
theorem category_theory.full_subcategory.map_inclusion {C : Type u₁} [category_theory.category C] {Z Z' : C → Prop} (h : ∀ ⦃X : C⦄, Z X → Z' X) :
category_theory.full_subcategory.map h ⋙ category_theory.full_subcategory_inclusion Z' = category_theory.full_subcategory_inclusion Z
source
def category_theory.full_subcategory.lift {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (P : D → Prop) (F : C ⥤ D) (hF : ∀ (X : C), P (F.obj X)) :
C ⥤ {X // P X}

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

Equations
source
@[simp]
theorem category_theory.full_subcategory.lift_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (P : D → Prop) (F : C ⥤ D) (hF : ∀ (X : C), P (F.obj X)) (X Y : C) (f : X ⟶ Y) :
(category_theory.full_subcategory.lift P F hF).map f = F.map f
source
@[simp]
theorem category_theory.full_subcategory.lift_obj_coe {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (P : D → Prop) (F : C ⥤ D) (hF : ∀ (X : C), P (F.obj X)) (X : C) :
↑((category_theory.full_subcategory.lift P F hF).obj X) = F.obj X
source
def category_theory.full_subcategory.lift_comp_inclusion {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (P : D → Prop) (F : C ⥤ D) (hF : ∀ (X : C), P (F.obj X)) :
category_theory.full_subcategory.lift P F hF ⋙ category_theory.full_subcategory_inclusion P ≅ F

Composing the lift of a functor through a full subcategory with the inclusion yields the original functor. Unfortunately, this is not true by definition, so we only get a natural isomorphism, but it is pointwise definitionally true, see full_subcategory.inclusion_obj_lift_obj and full_subcategory.inclusion_map_lift_map.

Equations
source
@[simp]
theorem category_theory.full_subcategory.inclusion_obj_lift_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (P : D → Prop) (F : C ⥤ D) (hF : ∀ (X : C), P (F.obj X)) {X : C} :
(category_theory.full_subcategory_inclusion P).obj ((category_theory.full_subcategory.lift P F hF).obj X) = F.obj X
source
theorem category_theory.full_subcategory.inclusion_map_lift_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (P : D → Prop) (F : C ⥤ D) (hF : ∀ (X : C), P (F.obj X)) {X Y : C} (f : X ⟶ Y) :
(category_theory.full_subcategory_inclusion P).map ((category_theory.full_subcategory.lift P F hF).map f) = F.map f
source
@[protected, instance]
def category_theory.full_subcategory.lift.faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (P : D → Prop) (F : C ⥤ D) (hF : ∀ (X : C), P (F.obj X)) [category_theory.faithful F] :
category_theory.faithful (category_theory.full_subcategory.lift P F hF)
source
@[protected, instance]
def category_theory.full_subcategory.lift.full {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (P : D → Prop) (F : C ⥤ D) (hF : ∀ (X : C), P (F.obj X)) [category_theory.full F] :
category_theory.full (category_theory.full_subcategory.lift P F hF)
Equations
source
@[simp]
theorem category_theory.full_subcategory.lift_comp_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (P Q : D → Prop) (F : C ⥤ D) (hF : ∀ (X : C), P (F.obj X)) (h : ∀ ⦃X : D⦄, P X → Q X) :
category_theory.full_subcategory.lift P F hF ⋙ category_theory.full_subcategory.map h = category_theory.full_subcategory.lift Q F _