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
.
As a special case, if C
is a subtype of D
,
this produces the full subcategory of D
on the objects belonging to C
.
In general the induced category is equivalent to the full subcategory of D
on the
image of 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
!
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
.
Instances For
The forgetful functor from an induced category to the original category, forgetting the extra data.
Instances For
- obj : C
The category of which this is a full subcategory
- property : Z s.obj
The predicate satisfied by all objects in this subcategory
A subtype-like structure for full subcategories. Morphisms just ignore the property. We don't use
actual subtypes since the simp-normal form ↑X
of X.val
does not work well for full
subcategories.
See https://stacks.math.columbia.edu/tag/001D. We do not define 'strictly full' subcategories.
Instances For
The forgetful functor from a full subcategory into the original category ("forgetting" the condition).
Instances For
An implication of predicates Z → Z'
induces a functor between full subcategories.
Instances For
A functor which maps objects to objects satisfying a certain property induces a lift through the full subcategory of objects satisfying that property.
Instances For
Composing the lift of a functor through a full subcategory with the inclusion yields the original functor. This is actually true definitionally.