# 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`.

## 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`!

source
def CategoryTheory.InducedCategory {C : Type u₁} (D : Type u₂) (_F : C → D) :
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

- CategoryTheory.InducedCategory D _F = C

Instances For

source
instance CategoryTheory.InducedCategory.hasCoeToSort {C : Type u₁} {D : Type u₂} (F : C → D) {α : Sort u_1} [CoeSort D α] :
CoeSort (InducedCategory D F) α
Equations

- CategoryTheory.InducedCategory.hasCoeToSort F = { coe := fun (c : CategoryTheory.InducedCategory D F) => CoeSort.coe (F c) }

source
instance CategoryTheory.InducedCategory.category {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] (F : C → D) :
Category.{v, u₁} (InducedCategory D F)
Equations

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

source
def CategoryTheory.InducedCategory.isoMk {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} {X Y : InducedCategory D F} (f : F X ≅ F Y) :
X ≅ Y

Construct an isomorphism in the induced category from an isomorphism in the original category.

Equations

- CategoryTheory.InducedCategory.isoMk f = { hom := f.hom, inv := f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.InducedCategory.isoMk_inv {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} {X Y : InducedCategory D F} (f : F X ≅ F Y) :
(isoMk f).inv = f.inv
source
@[simp]
theorem CategoryTheory.InducedCategory.isoMk_hom {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} {X Y : InducedCategory D F} (f : F X ≅ F Y) :
(isoMk f).hom = f.hom
source
def CategoryTheory.inducedFunctor {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] (F : C → D) :
Functor (InducedCategory D F) D

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

Equations

- CategoryTheory.inducedFunctor F = { obj := F, map := fun {X Y : CategoryTheory.InducedCategory D F} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.inducedFunctor_map {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] (F : C → D) {X✝ Y✝ : InducedCategory D F} (f : X✝ ⟶ Y✝) :
(inducedFunctor F).map f = f
source
@[simp]
theorem CategoryTheory.inducedFunctor_obj {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] (F : C → D) (a✝ : C) :
(inducedFunctor F).obj a✝ = F a✝
source
def CategoryTheory.fullyFaithfulInducedFunctor {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] (F : C → D) :
(inducedFunctor F).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

source
instance CategoryTheory.InducedCategory.full {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] (F : C → D) :
(inducedFunctor F).Full
source
instance CategoryTheory.InducedCategory.faithful {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] (F : C → D) :
(inducedFunctor F).Faithful