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

The type of morphisms between X and Y in InducedCategory D F is not definitionally equal to F X ⟶ F Y. Instead, this type is made a 1-field structure. Use InducedCategory.homMk to construct morphisms in induced categories.

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

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

structure CategoryTheory.InducedCategory.Hom {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} (X Y : InducedCategory D F) : Type v

The type of morphisms in InducedCategory D F between X and Y is a 1-field structure which identifies to F X ⟶ F Y.

• hom : F X ⟶ F Y

  The underlying morphism.

theorem CategoryTheory.InducedCategory.Hom.ext_iff {C : Type u₁} {D : Type u₂} {inst✝ : Category.{v, u₂} D} {F : C → D} {X Y : InducedCategory D F} {x y : X.Hom Y} : x = y ↔ x.hom = y.hom

theorem CategoryTheory.InducedCategory.Hom.ext {C : Type u₁} {D : Type u₂} {inst✝ : Category.{v, u₂} D} {F : C → D} {X Y : InducedCategory D F} {x y : X.Hom Y} (hom : x.hom = y.hom) : x = y

instance CategoryTheory.InducedCategory.instCategory {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.

@[simp]

theorem CategoryTheory.InducedCategory.id_hom {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} (X : InducedCategory D F) : (CategoryStruct.id X).hom = CategoryStruct.id (F X)

@[simp]

theorem CategoryTheory.InducedCategory.comp_hom {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} {X✝ Y✝ Z✝ : InducedCategory D F} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.InducedCategory.comp_hom_assoc {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} {X✝ Y✝ Z✝ : InducedCategory D F} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {Z : D} (h : F Z✝ ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g).hom h = CategoryStruct.comp f.hom (CategoryStruct.comp g.hom h)

theorem CategoryTheory.InducedCategory.hom_ext {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} {X Y : InducedCategory D F} {f g : X ⟶ Y} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.InducedCategory.hom_ext_iff {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} {X Y : InducedCategory D F} {f g : X ⟶ Y} : f = g ↔ f.hom = g.hom

def CategoryTheory.InducedCategory.homMk {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 a morphism in the induced category from a morphism in the original category.

Equations

• CategoryTheory.InducedCategory.homMk f = { hom := f }

@[simp]

theorem CategoryTheory.InducedCategory.homMk_hom {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} {X Y : InducedCategory D F} (f : F X ⟶ F Y) : (homMk f).hom = f

def CategoryTheory.InducedCategory.homEquiv {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} {X Y : InducedCategory D F} : (X ⟶ Y) ≃ (F X ⟶ F Y)

Morphisms in InducedCategory D F identify to morphisms in D.

Equations

• CategoryTheory.InducedCategory.homEquiv = { toFun := fun (f : X ⟶ Y) => f.hom, invFun := fun (f : F X ⟶ F Y) => CategoryTheory.InducedCategory.homMk f, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.InducedCategory.homEquiv_symm_apply_hom {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} {X Y : InducedCategory D F} (f : F X ⟶ F Y) : (homEquiv.symm f).hom = f

@[simp]

theorem CategoryTheory.InducedCategory.homEquiv_apply {C : Type u₁} {D : Type u₂} [Category.{v, u₂} D] {F : C → D} {X Y : InducedCategory D F} (f : X ⟶ Y) : homEquiv f = f.hom

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 := CategoryTheory.InducedCategory.homMk f.hom, inv := CategoryTheory.InducedCategory.homMk f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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 = homMk f.inv

@[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 = homMk f.hom

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.hom, map_id := ⋯, map_comp := ⋯ }

@[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✝

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

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.

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

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