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
.
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
Instances For
Equations
- CategoryTheory.InducedWideCategory.hasCoeToSort F P = { coe := fun (c : CategoryTheory.InducedWideCategory D F P) => CoeSort.coe (F c) }
Equations
The forgetful functor from an induced wide category to the original category.
Equations
- CategoryTheory.wideInducedFunctor F P = { obj := F, map := fun {X Y : CategoryTheory.InducedWideCategory D F P} (f : X ⟶ Y) => ↑f, map_id := ⋯, map_comp := ⋯ }
Instances For
The induced functor wideInducedFunctor F P : InducedWideCategory D F P ⥤ D
is faithful.
Equations
- ⋯ = ⋯
Structure for wide subcategories. Objects ignore the morphism property.
- obj : C
The category of which this is a wide subcategory
Instances For
Equations
- CategoryTheory.WideSubcategory.category P = CategoryTheory.InducedWideCategory.category CategoryTheory.WideSubcategory.obj P
The forgetful functor from a wide subcategory into the original category ("forgetting" the condition).
Equations
- CategoryTheory.wideSubcategoryInclusion P = CategoryTheory.wideInducedFunctor CategoryTheory.WideSubcategory.obj P
Instances For
The inclusion of a wide subcategory is faithful.
Equations
- ⋯ = ⋯