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
.
Equations
- CategoryTheory.InducedCategory D _F = C
Instances For
Equations
- CategoryTheory.InducedCategory.hasCoeToSort F = { coe := fun (c : CategoryTheory.InducedCategory D F) => CoeSort.coe (F c) }
Equations
The forgetful functor from an induced category to the original category, forgetting the extra data.
Equations
- CategoryTheory.inducedFunctor F = { toPrefunctor := { obj := F, map := fun {X Y : CategoryTheory.InducedCategory D F} (f : X ⟶ Y) => f }, map_id := ⋯, map_comp := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
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
- obj : C
The category of which this is a full subcategory
- property : Z self.obj
The predicate satisfied by all objects in this subcategory
Instances For
Equations
- CategoryTheory.FullSubcategory.category Z = CategoryTheory.InducedCategory.category CategoryTheory.FullSubcategory.obj
The forgetful functor from a full subcategory into the original category ("forgetting" the condition).
Equations
- CategoryTheory.fullSubcategoryInclusion Z = CategoryTheory.inducedFunctor CategoryTheory.FullSubcategory.obj
Instances For
Equations
- CategoryTheory.FullSubcategory.full Z = CategoryTheory.InducedCategory.full CategoryTheory.FullSubcategory.obj
Equations
- ⋯ = ⋯
An implication of predicates Z → Z'
induces a functor between full subcategories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
A functor which maps objects to objects satisfying a certain property induces a lift through the full subcategory of objects satisfying that property.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Composing the lift of a functor through a full subcategory with the inclusion yields the original functor. This is actually true definitionally.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯