Wide subcategories

A wide subcategory of a category C is a subcategory containing all the objects of C.

Main declarations

Given a category D, a function F : C → D from a type C to the objects of D, and a morphism property P on D which contains identities and is stable under composition, the type class InducedWideCategory D F P is a typeclass synonym for C which comes equipped with a category structure whose morphisms X ⟶ Y are the morphisms in D which have the property P.

The instance WideSubcategory.category provides a category structure on WideSubcategory P whose objects are the objects of C and morphisms are the morphisms in C which have the property P.

def CategoryTheory.InducedWideCategory {C : Type u₁} (D : Type u₂) [Category.{v₁, u₂} D] (_F : C → D) (_P : MorphismProperty D) [_P.IsMultiplicative] : Type u₁

InducedWideCategory D F P, 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 which satisfy a property P : MorphismProperty D that is multiplicative.

Equations

• CategoryTheory.InducedWideCategory D _F _P = C

@[implicit_reducible]

instance CategoryTheory.InducedWideCategory.hasCoeToSort {C : Type u₁} {D : Type u₂} [Category.{v₁, u₂} D] (F : C → D) (P : MorphismProperty D) [P.IsMultiplicative] {α : Sort u_1} [CoeSort D α] : CoeSort (InducedWideCategory D F P) α

Equations

• CategoryTheory.InducedWideCategory.hasCoeToSort F P = { coe := fun (c : CategoryTheory.InducedWideCategory D F P) => CoeSort.coe (F c) }

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

The type of morphisms in InducedWideCategory D F P between X and Y is a 2-field structure consisting of a morphism F X ⟶ F Y in D that satisfies the property P.

• hom : F X ⟶ F Y

  The underlying morphism.

• property : P self.hom

  The property that the morphism satisfies.

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

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

@[implicit_reducible]

instance CategoryTheory.InducedWideCategory.category {C : Type u₁} {D : Type u₂} [Category.{v₁, u₂} D] (F : C → D) (P : MorphismProperty D) [P.IsMultiplicative] : Category.{v₁, u₁} (InducedWideCategory D F P)

Equations

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

@[simp]

theorem CategoryTheory.InducedWideCategory.category_id_hom {C : Type u₁} {D : Type u₂} [Category.{v₁, u₂} D] (F : C → D) (P : MorphismProperty D) [P.IsMultiplicative] (X : InducedWideCategory D F P) : (CategoryStruct.id X).hom = CategoryStruct.id (F X)

@[simp]

theorem CategoryTheory.InducedWideCategory.category_comp_hom {C : Type u₁} {D : Type u₂} [Category.{v₁, u₂} D] (F : C → D) (P : MorphismProperty D) [P.IsMultiplicative] {x✝ x✝¹ x✝² : InducedWideCategory D F P} (f : x✝.Hom x✝¹) (g : x✝¹.Hom x✝²) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

def CategoryTheory.wideInducedFunctor {C : Type u₁} {D : Type u₂} [Category.{v₁, u₂} D] (F : C → D) (P : MorphismProperty D) [P.IsMultiplicative] : Functor (InducedWideCategory D F P) D

The forgetful functor from an induced wide category to the original category.

Equations

• CategoryTheory.wideInducedFunctor F P = { obj := F, map := fun {x x_1 : CategoryTheory.InducedWideCategory D F P} (f : x ⟶ x_1) => f.hom, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.wideInducedFunctor_obj {C : Type u₁} {D : Type u₂} [Category.{v₁, u₂} D] (F : C → D) (P : MorphismProperty D) [P.IsMultiplicative] (a✝ : C) : (wideInducedFunctor F P).obj a✝ = F a✝

@[simp]

theorem CategoryTheory.wideInducedFunctor_map {C : Type u₁} {D : Type u₂} [Category.{v₁, u₂} D] (F : C → D) (P : MorphismProperty D) [P.IsMultiplicative] {x✝ x✝¹ : InducedWideCategory D F P} (f : x✝ ⟶ x✝¹) : (wideInducedFunctor F P).map f = f.hom

instance CategoryTheory.InducedWideCategory.faithful {C : Type u₁} {D : Type u₂} [Category.{v₁, u₂} D] (F : C → D) (P : MorphismProperty D) [P.IsMultiplicative] : (wideInducedFunctor F P).Faithful

The induced functor wideInducedFunctor F P : InducedWideCategory D F P ⥤ D is faithful.

structure CategoryTheory.WideSubcategory {C : Type u₁} [Category.{v₁, u₁} C] (_P : MorphismProperty C) [_P.IsMultiplicative] : Type u₁

Structure for wide subcategories. Objects ignore the morphism property.

• obj : C

  The category of which this is a wide subcategory

theorem CategoryTheory.WideSubcategory.ext {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {_P : MorphismProperty C} {inst✝¹ : _P.IsMultiplicative} {x y : WideSubcategory _P} (obj : x.obj = y.obj) : x = y

theorem CategoryTheory.WideSubcategory.ext_iff {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {_P : MorphismProperty C} {inst✝¹ : _P.IsMultiplicative} {x y : WideSubcategory _P} : x = y ↔ x.obj = y.obj

@[implicit_reducible]

instance CategoryTheory.WideSubcategory.category {C : Type u₁} [Category.{v₁, u₁} C] (P : MorphismProperty C) [P.IsMultiplicative] : Category.{v₁, u₁} (WideSubcategory P)

Equations

• CategoryTheory.WideSubcategory.category P = CategoryTheory.InducedWideCategory.category CategoryTheory.WideSubcategory.obj P

theorem CategoryTheory.WideSubcategory.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] (P : MorphismProperty C) [P.IsMultiplicative] {X Y : WideSubcategory P} {f g : X ⟶ Y} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.WideSubcategory.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {P : MorphismProperty C} [P.IsMultiplicative] {X Y : WideSubcategory P} {f g : X ⟶ Y} : f = g ↔ f.hom = g.hom

@[simp]

theorem CategoryTheory.WideSubcategory.id_def {C : Type u₁} [Category.{v₁, u₁} C] (P : MorphismProperty C) [P.IsMultiplicative] (X : WideSubcategory P) : (CategoryStruct.id X).hom = CategoryStruct.id X.obj

@[simp]

theorem CategoryTheory.WideSubcategory.comp_def {C : Type u₁} [Category.{v₁, u₁} C] (P : MorphismProperty C) [P.IsMultiplicative] {X Y Z : WideSubcategory P} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

def CategoryTheory.wideSubcategoryInclusion {C : Type u₁} [Category.{v₁, u₁} C] (P : MorphismProperty C) [P.IsMultiplicative] : Functor (WideSubcategory P) C

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

Equations

• CategoryTheory.wideSubcategoryInclusion P = CategoryTheory.wideInducedFunctor CategoryTheory.WideSubcategory.obj P

@[simp]

theorem CategoryTheory.wideSubcategoryInclusion.obj {C : Type u₁} [Category.{v₁, u₁} C] (P : MorphismProperty C) [P.IsMultiplicative] (X : WideSubcategory P) : (wideSubcategoryInclusion P).obj X = X.obj

@[simp]

theorem CategoryTheory.wideSubcategoryInclusion.map {C : Type u₁} [Category.{v₁, u₁} C] (P : MorphismProperty C) [P.IsMultiplicative] {X Y : WideSubcategory P} {f : X ⟶ Y} : (wideSubcategoryInclusion P).map f = f.hom

instance CategoryTheory.wideSubcategory.faithful {C : Type u₁} [Category.{v₁, u₁} C] (P : MorphismProperty C) [P.IsMultiplicative] : (wideSubcategoryInclusion P).Faithful

The inclusion of a wide subcategory is faithful.

def CategoryTheory.isoMk {C : Type u₁} [Category.{v₁, u₁} C] {P : MorphismProperty C} [P.IsMultiplicative] {X Y : WideSubcategory P} (e : X.obj ≅ Y.obj) (h₁ : P e.hom) (h₂ : P e.inv) : X ≅ Y

Build an isomorphism in WideSubcategory P from an isomorphism in C.

Equations

• CategoryTheory.isoMk e h₁ h₂ = { hom := { hom := e.hom, property := h₁ }, inv := { hom := e.inv, property := h₂ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.isoMk_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] {P : MorphismProperty C} [P.IsMultiplicative] {X Y : WideSubcategory P} (e : X.obj ≅ Y.obj) (h₁ : P e.hom) (h₂ : P e.inv) : (isoMk e h₁ h₂).inv.hom = e.inv

@[simp]

theorem CategoryTheory.isoMk_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] {P : MorphismProperty C} [P.IsMultiplicative] {X Y : WideSubcategory P} (e : X.obj ≅ Y.obj) (h₁ : P e.hom) (h₂ : P e.inv) : (isoMk e h₁ h₂).hom.hom = e.hom