# Induced categories and full subcategories #

Given a category D and a function F : C → D from 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 InducedCategory, 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 InducedCategory.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) := InducedCategory Mon (Bundled.map @CommMonoid.toMonoid) -- not InducedCategory (Bundled Monoid) (Bundled.map @CommMonoid.toMonoid), -- even though MonCat = Bundled Monoid!

def CategoryTheory.InducedCategory {C : Type u₁} (D : Type u₂) (_F : CD) :
Type u₁

InducedCategory 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
Instances For
instance CategoryTheory.InducedCategory.hasCoeToSort {C : Type u₁} {D : Type u₂} (F : CD) {α : Sort u_1} [CoeSort D α] :
Equations
instance CategoryTheory.InducedCategory.category {C : Type u₁} {D : Type u₂} [] (F : CD) :
Equations
@[simp]
theorem CategoryTheory.inducedFunctor_map {C : Type u₁} {D : Type u₂} [] (F : CD) :
∀ {X Y : } (f : X Y), .map f = f
@[simp]
theorem CategoryTheory.inducedFunctor_obj {C : Type u₁} {D : Type u₂} [] (F : CD) :
∀ (a : C), .obj a = F a
def CategoryTheory.inducedFunctor {C : Type u₁} {D : Type u₂} [] (F : CD) :

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

Equations
• = { obj := F, map := fun {X Y : } (f : X Y) => f, map_id := , map_comp := }
Instances For
def CategoryTheory.fullyFaithfulInducedFunctor {C : Type u₁} {D : Type u₂} [] (F : CD) :
.FullyFaithful

The induced functor inducedFunctor F : InducedCategory D F ⥤ D is fully faithful.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.InducedCategory.full {C : Type u₁} {D : Type u₂} [] (F : CD) :
.Full
Equations
• =
instance CategoryTheory.InducedCategory.faithful {C : Type u₁} {D : Type u₂} [] (F : CD) :
.Faithful
Equations
• =
theorem CategoryTheory.FullSubcategory.ext {C : Type u₁} {Z : CProp} (obj : x.obj = y.obj) :
x = y
theorem CategoryTheory.FullSubcategory.ext_iff {C : Type u₁} {Z : CProp} :
x = y x.obj = y.obj
structure CategoryTheory.FullSubcategory {C : Type u₁} (Z : CProp) :
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.

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

• obj : C

The category of which this is a full subcategory

• property : Z self.obj

The predicate satisfied by all objects in this subcategory

Instances For
theorem CategoryTheory.FullSubcategory.property {C : Type u₁} {Z : CProp} (self : ) :
Z self.obj

The predicate satisfied by all objects in this subcategory

instance CategoryTheory.FullSubcategory.category {C : Type u₁} [] (Z : CProp) :
Equations
theorem CategoryTheory.FullSubcategory.id_def {C : Type u₁} [] (Z : CProp) :
theorem CategoryTheory.FullSubcategory.comp_def {C : Type u₁} [] (Z : CProp) {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
def CategoryTheory.fullSubcategoryInclusion {C : Type u₁} [] (Z : CProp) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.fullSubcategoryInclusion.obj {C : Type u₁} [] (Z : CProp) :
= X.obj
@[simp]
theorem CategoryTheory.fullSubcategoryInclusion.map {C : Type u₁} [] (Z : CProp) {f : X Y} :
= f
@[reducible, inline]
abbrev CategoryTheory.fullyFaithfulFullSubcategoryInclusion {C : Type u₁} [] (Z : CProp) :
.FullyFaithful

The inclusion of a full subcategory is fully faithful.

Equations
Instances For
instance CategoryTheory.FullSubcategory.full {C : Type u₁} [] (Z : CProp) :
Equations
• =
instance CategoryTheory.FullSubcategory.faithful {C : Type u₁} [] (Z : CProp) :
.Faithful
Equations
• =
@[simp]
theorem CategoryTheory.FullSubcategory.map_obj_obj {C : Type u₁} [] {Z : CProp} {Z' : CProp} (h : ∀ ⦃X : C⦄, Z XZ' X) :
( X).obj = X.obj
@[simp]
theorem CategoryTheory.FullSubcategory.map_map {C : Type u₁} [] {Z : CProp} {Z' : CProp} (h : ∀ ⦃X : C⦄, Z XZ' X) :
∀ {X Y : } (f : X Y), f = f
def CategoryTheory.FullSubcategory.map {C : Type u₁} [] {Z : CProp} {Z' : CProp} (h : ∀ ⦃X : C⦄, Z XZ' X) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.FullSubcategory.full_map {C : Type u₁} [] {Z : CProp} {Z' : CProp} (h : ∀ ⦃X : C⦄, Z XZ' X) :
.Full
Equations
• =
instance CategoryTheory.FullSubcategory.faithful_map {C : Type u₁} [] {Z : CProp} {Z' : CProp} (h : ∀ ⦃X : C⦄, Z XZ' X) :
.Faithful
Equations
• =
@[simp]
theorem CategoryTheory.FullSubcategory.map_inclusion {C : Type u₁} [] {Z : CProp} {Z' : CProp} (h : ∀ ⦃X : C⦄, Z XZ' X) :
@[simp]
theorem CategoryTheory.FullSubcategory.lift_map {C : Type u₁} [] {D : Type u₂} [] (P : DProp) (F : ) (hF : ∀ (X : C), P (F.obj X)) :
∀ {X Y : C} (f : X Y), .map f = F.map f
@[simp]
theorem CategoryTheory.FullSubcategory.lift_obj_obj {C : Type u₁} [] {D : Type u₂} [] (P : DProp) (F : ) (hF : ∀ (X : C), P (F.obj X)) (X : C) :
(.obj X).obj = F.obj X
def CategoryTheory.FullSubcategory.lift {C : Type u₁} [] {D : Type u₂} [] (P : DProp) (F : ) (hF : ∀ (X : C), P (F.obj 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
• = { 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
@[simp]
theorem CategoryTheory.FullSubcategory.lift_comp_inclusion_eq {C : Type u₁} [] {D : Type u₂} [] (P : DProp) (F : ) (hF : ∀ (X : C), P (F.obj X)) :
= F
def CategoryTheory.FullSubcategory.lift_comp_inclusion {C : Type u₁} [] {D : Type u₂} [] (P : DProp) (F : ) (hF : ∀ (X : C), P (F.obj X)) :
F

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

Equations
Instances For
@[simp]
theorem CategoryTheory.fullSubcategoryInclusion_obj_lift_obj {C : Type u₁} [] {D : Type u₂} [] (P : DProp) (F : ) (hF : ∀ (X : C), P (F.obj X)) {X : C} :
(.obj X) = F.obj X
@[simp]
theorem CategoryTheory.fullSubcategoryInclusion_map_lift_map {C : Type u₁} [] {D : Type u₂} [] (P : DProp) (F : ) (hF : ∀ (X : C), P (F.obj X)) {X : C} {Y : C} (f : X Y) :
(.map f) = F.map f
instance CategoryTheory.instFaithfulFullSubcategoryLift {C : Type u₁} [] {D : Type u₂} [] (P : DProp) (F : ) (hF : ∀ (X : C), P (F.obj X)) [F.Faithful] :
.Faithful
Equations
• =
instance CategoryTheory.instFullFullSubcategoryLift {C : Type u₁} [] {D : Type u₂} [] (P : DProp) (F : ) (hF : ∀ (X : C), P (F.obj X)) [F.Full] :
.Full
Equations
• =
@[simp]
theorem CategoryTheory.FullSubcategory.lift_comp_map {C : Type u₁} [] {D : Type u₂} [] (P : DProp) (Q : DProp) (F : ) (hF : ∀ (X : C), P (F.obj X)) (h : ∀ ⦃X : D⦄, P XQ X) :