Preservation of multicoequalizers #
Let J : MultispanShape
and d : MultispanIndex J C
.
If F : C ⥤ D
, we define d.map F : MultispanIndex J D
and
an isomorphism of functors (d.map F).multispan ≅ d.multispan ⋙ F
(see MultispanIndex.multispanMapIso
).
If c : Multicofork d
, we define c.map F : Multicofork (d.map F)
and
obtain a bijection IsColimit (F.mapCocone c) ≃ IsColimit (c.map F)
(see Multicofork.isColimitMapEquiv
). As a result, if F
preserves
the colimit of d.multispan
, we deduce that if c
is a colimit,
then c.map F
also is (see Multicofork.isColimitMapOfPreserves
).
The multispan index obtained by applying a functor.
Equations
Instances For
If d : MultispanIndex J C
and F : C ⥤ D
, this is the obvious isomorphism
(d.map F).multispan ≅ d.multispan ⋙ F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If d : MultispanIndex J C
, c : Multicofork d
and F : C ⥤ D
,
this is the induced multicofork of d.map F
.
Equations
Instances For
If d : MultispanIndex J C
, c : Multicofork d
and F : C ⥤ D
,
the cocone F.mapCocone c
is colimit iff the multicofork c.map F
is.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If d : MultispanIndex J C
, c : Multicofork d
is a colimit multicofork,
and F : C ⥤ D
is a functor which preserves the colimit of d.multispan
,
then the multicofork c.map F
is colimit.
Equations
- c.isColimitMapOfPreserves F hc = (c.isColimitMapEquiv F) (CategoryTheory.Limits.isColimitOfPreserves F hc)