English
If W is a morphism property on D and F : C ⥤ D preserves the relevant well-ordered limits and colimits, then a transfinite composition of shape J in the inverse image of F maps to a transfinite composition of shape J in D after applying F.
Русский
Если W — свойство морфизмов в D и F: C ⥤ D сохраняет нужные пределы и сопряжённые колимиты, то трансфинитная композиция формы J в обратном образе F переходит в трансфинитную композицию формы J после применения F.
LaTeX
$$$[W^{-1}F].TransfiniteCompositionOfShape J f \Rightarrow W.TransfiniteCompositionOfShape J (F.map f)$$$
Lean4
/-- If `f` is a transfinite composition of shape `J` of morphisms
in `W.inverseImage F`, then `F` is a transfinite composition of shape `J`
of morphisms in `W` provided `F` preserves suitable colimits. -/
@[simps toTransfiniteCompositionOfShape]
noncomputable def map {W : MorphismProperty D} {F : C ⥤ D} [PreservesWellOrderContinuousOfShape J F]
[PreservesColimitsOfShape J F] (h : (W.inverseImage F).TransfiniteCompositionOfShape J f) :
W.TransfiniteCompositionOfShape J (F.map f)
where
__ := h.toTransfiniteCompositionOfShape.map F
map_mem j hj := h.map_mem j hj
