English
If F preserves well-order continuity and colimits, then mapping a transfinite composition along F yields a transfinite composition of shape J for F.map f.
Русский
Если F сохраняет непрерывность по Well-Order и колимиты, то отображение трансфинитной композиции через F даёт трансфинитную композицию формы J для F.map f.
LaTeX
$$$\text{TransfiniteCompositionOfShape}(J, f) \xrightarrow{\mathrm{map}} \text{TransfiniteCompositionOfShape}(J, F.map\, f)$$$
Lean4
/-- If `f` is a transfinite composition of shape `J`, then `F.map f` also is
provided `F` preserves suitable colimits. -/
@[simps]
noncomputable def map (F : C ⥤ D) [PreservesWellOrderContinuousOfShape J F] [PreservesColimitsOfShape J F] :
TransfiniteCompositionOfShape J (F.map f) where
F := c.F ⋙ F
isoBot := F.mapIso c.isoBot
incl := Functor.whiskerRight c.incl F ≫ (Functor.constComp _ _ _).hom
isColimit := IsColimit.ofIsoColimit (isColimitOfPreserves F c.isColimit) (Cocones.ext (Iso.refl _))
fac := by simp [← Functor.map_comp]
