transfiniteCompositionsOfShape_map_of_preserves

English

If a functor G preserves shape J well-ordered transfinite limits and colimits, then a transfinite composition of shape Fin J is preserved under G: if a morphism is a transfinite composition in D, its image under G is a transfinite composition in C.

Русский

Если функтор G сохраняет трансфинитные пределы и колимиты формы J, то отображение трансфинитной композиции через G сохраняется: если морфизм является трансфинитной композицией в D, его образ в C тоже таковым является.

LaTeX

$$$(P.inverseImage G).transfiniteCompositionsOfShape J f \\Rightarrow P.transfiniteCompositionsOfShape J (G.map f)$$$

Lean4

theorem transfiniteCompositionsOfShape_map_of_preserves (G : C ⥤ D) [PreservesWellOrderContinuousOfShape J G] {X Y : C}
    (f : X ⟶ Y) {P : MorphismProperty D} [PreservesColimitsOfShape J G]
    (h : (P.inverseImage G).transfiniteCompositionsOfShape J f) : P.transfiniteCompositionsOfShape J (G.map f) :=
  h.some.map.mem

Похожие утверждения