Limits and colimits in the category of algebras #
This file shows that the forgetful functor forget T : Algebra T ⥤ C
for a monad T : C ⥤ C
creates limits and creates any colimits which T
preserves.
This is used to show that Algebra T
has any limits which C
has, and any colimits which C
has
and T
preserves.
This is generalised to the case of a monadic functor D ⥤ C
.
TODO #
Dualise for the category of coalgebras and comonadic left adjoints.
(Impl) The natural transformation used to define the new cone
Instances For
(Impl) This new cone is used to construct the algebra structure
Instances For
The algebra structure which will be the apex of the new limit cone for D
.
Instances For
(Impl) Construct the lifted cone in Algebra T
which will be limiting.
Instances For
(Impl) Prove that the lifted cone is limiting.
Instances For
The forgetful functor from the Eilenberg-Moore category creates limits.
D ⋙ forget T
has a limit, then D
has a limit.
(Impl)
The natural transformation given by the algebra structure maps, used to construct a cocone c
with
apex colimit (D ⋙ forget T)
.
Instances For
(Impl)
A cocone for the diagram (D ⋙ forget T) ⋙ T
found by composing the natural transformation γ
with the colimiting cocone for D ⋙ forget T
.
Instances For
(Impl)
Define the map λ : TL ⟶ L
, which will serve as the structure of the coalgebra on L
, and
we will show is the colimiting object. We use the cocone constructed by c
and the fact that
T
preserves colimits to produce this morphism.
Instances For
(Impl) The key property defining the map λ : TL ⟶ L
.
(Impl)
Construct the colimiting algebra from the map λ : TL ⟶ L
given by lambda
. We are required to
show it satisfies the two algebra laws, which follow from the algebra laws for the image of D
and
our commuting
lemma.
Instances For
(Impl) Construct the lifted cocone in Algebra T
which will be colimiting.
Instances For
(Impl) Prove that the lifted cocone is colimiting.
Instances For
The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit which the monad itself preserves.
For D : J ⥤ Algebra T
, D ⋙ forget T
has a colimit, then D
has a colimit provided colimits
of shape J
are preserved by T
.
Any monadic functor creates limits.
Instances For
The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit which the monad itself preserves.
Instances For
A monadic functor creates any colimits of shapes it preserves.
Instances For
A monadic functor creates colimits if it preserves colimits.
Instances For
If C
has limits of shape J
then any reflective subcategory has limits of shape J
.
If C
has limits then any reflective subcategory has limits.
If C
has colimits of shape J
then any reflective subcategory has colimits of shape J
.
If C
has colimits then any reflective subcategory has colimits.
The reflector always preserves terminal objects. Note this in general doesn't apply to any other limit.