Mathlib.CategoryTheory.InducedCategory

Module docstring

{"# 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 $$ HomC(X, Y) = HomD(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! "}

CategoryTheory.InducedCategory definition

(_F : C → D) : Type u₁

Full source

/-- `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`.
-/
@[nolint unusedArguments]
def InducedCategory (_F : C → D) : Type u₁ :=
  C

Induced category along $F$

Informal description

Given a category $\mathcal{D}$ and a function $F : C \to \mathcal{D}$ from a type $C$ to the objects of $\mathcal{D}$, the induced category structure on $C$ is defined such that the morphisms between objects $X$ and $Y$ in $C$ are precisely the morphisms between $F(X)$ and $F(Y)$ in $\mathcal{D}$. This makes $F$ a fully faithful functor.

CategoryTheory.InducedCategory.hasCoeToSort instance

{α : Sort*} [CoeSort D α] : CoeSort (InducedCategory D F) α

Full source

instance InducedCategory.hasCoeToSort {α : Sort*} [CoeSort D α] :
    CoeSort (InducedCategory D F) α :=
  ⟨fun c => F c⟩

Coercion from Induced Category to Base Category's Objects

Informal description

For any type $\alpha$ that can be coerced into objects of a category $\mathcal{D}$, the induced category along a function $F : C \to \mathcal{D}$ can also be coerced into $\alpha$.

CategoryTheory.InducedCategory.category instance

: Category.{v} (InducedCategory D F)

Full source

instance InducedCategory.category : Category.{v} (InducedCategory D F) where
  Hom X Y := F X ⟶ F Y
  id X := 𝟙 (F X)
  comp f g := f ≫ g

Category Structure on Induced Category

Informal description

For any category $\mathcal{D}$ and function $F : C \to \mathcal{D}$ from a type $C$ to the objects of $\mathcal{D}$, the induced category structure on $C$ forms a category where the morphisms between objects $X$ and $Y$ in $C$ are precisely the morphisms between $F(X)$ and $F(Y)$ in $\mathcal{D}$.

CategoryTheory.InducedCategory.isoMk definition

{X Y : InducedCategory D F} (f : F X ≅ F Y) : X ≅ Y

Full source

/-- Construct an isomorphism in the induced category
from an isomorphism in the original category. -/
@[simps] def InducedCategory.isoMk {X Y : InducedCategory D F} (f : F X ≅ F Y) : X ≅ Y where
  hom := f.hom
  inv := f.inv
  hom_inv_id := f.hom_inv_id
  inv_hom_id := f.inv_hom_id

Isomorphism construction in induced category

Informal description

Given an isomorphism $f : F(X) \cong F(Y)$ in the original category $\mathcal{D}$, this constructs the corresponding isomorphism $X \cong Y$ in the induced category along $F$, where the morphisms and their inverses are preserved.

CategoryTheory.inducedFunctor definition

: InducedCategory D F ⥤ D

Full source

/-- The forgetful functor from an induced category to the original category,
forgetting the extra data.
-/
@[simps]
def inducedFunctor : InducedCategoryInducedCategory D F ⥤ D where
  obj := F
  map f := f

Forgetful functor from induced category

Informal description

The forgetful functor from the induced category along $F$ to the original category $\mathcal{D}$, which maps each object $X$ in the induced category to $F(X)$ and each morphism $f$ to itself.

CategoryTheory.fullyFaithfulInducedFunctor definition

: (inducedFunctor F).FullyFaithful

Full source

/-- The induced functor `inducedFunctor F : InducedCategory D F ⥤ D` is fully faithful. -/
def fullyFaithfulInducedFunctor : (inducedFunctor F).FullyFaithful where
  preimage f := f

Fully faithful property of the induced functor

Informal description

The induced functor $F : \text{InducedCategory} \, D \, F \to D$ is fully faithful, meaning it is both full (surjective on morphisms between any two objects) and faithful (injective on morphisms between any two objects).

CategoryTheory.InducedCategory.full instance

: (inducedFunctor F).Full

Full source

instance InducedCategory.full : (inducedFunctor F).Full :=
  (fullyFaithfulInducedFunctor F).full

Fullness of the Induced Functor

Informal description

The forgetful functor from the induced category along $F$ to the original category $\mathcal{D}$ is full. That is, for any two objects $X$ and $Y$ in the induced category, the map $\text{Hom}(X, Y) \to \text{Hom}(F(X), F(Y))$ is surjective.

CategoryTheory.InducedCategory.faithful instance

: (inducedFunctor F).Faithful

Full source

instance InducedCategory.faithful : (inducedFunctor F).Faithful :=
  (fullyFaithfulInducedFunctor F).faithful

Faithfulness of the Induced Functor

Informal description

The forgetful functor from the induced category along $F$ to the original category $\mathcal{D}$ is faithful. That is, for any two objects $X$ and $Y$ in the induced category, the map $\text{Hom}(X, Y) \to \text{Hom}(F(X), F(Y))$ is injective.