Documentation

Mathlib.CategoryTheory.Widesubcategory

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₂) [CategoryTheory.Category.{v₁, u₂} D] (_F : CD) (_P : CategoryTheory.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
Instances For
    @[simp]
    theorem CategoryTheory.wideInducedFunctor_obj {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CD) (P : CategoryTheory.MorphismProperty D) [P.IsMultiplicative] :
    ∀ (a : C), (CategoryTheory.wideInducedFunctor F P).obj a = F a

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

    Equations
    Instances For

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

      Equations
      • =
      theorem CategoryTheory.WideSubcategory.ext_iff {C : Type u₁} :
      ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {_P : CategoryTheory.MorphismProperty C} {inst_1 : _P.IsMultiplicative} {x y : CategoryTheory.WideSubcategory _P}, x = y x.obj = y.obj
      theorem CategoryTheory.WideSubcategory.ext {C : Type u₁} :
      ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {_P : CategoryTheory.MorphismProperty C} {inst_1 : _P.IsMultiplicative} {x y : CategoryTheory.WideSubcategory _P}, x.obj = y.objx = y

      Structure for wide subcategories. Objects ignore the morphism property.

      • obj : C

        The category of which this is a wide subcategory

      Instances For

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

        Equations
        Instances For

          The inclusion of a wide subcategory is faithful.

          Equations
          • =