mapActionPreservesColimit_of_preserves

English

Let K : J ⥤ Action V G with HasColimit (K ⋙ forget V G) and PreservesColimit (K ⋙ forget V G) F. Then PreservesColimit K (F.mapAction G).

Русский

Пусть K : J ⥤ Action V G имеет колимит после забывания и F сохраняет колимит K ⋙ forget V G. Тогда F.mapAction G сохраняет колимит K.

LaTeX

$$$\\operatorname{PreservesColimit}(K, F.mapAction\\,G)$$$

Lean4

/-- `F.mapAction : Action V G ⥤ Action W G` preserves the colimit of some `K : J ⥤ Action V G` if
`K ⋙ forget V G` has a colimit and `F` preserves the colimit of `K ⋙ forget V G`. -/
instance mapActionPreservesColimit_of_preserves (K : J ⥤ Action V G) [HasColimit (K ⋙ forget V G)]
    [PreservesColimit (K ⋙ Action.forget V G) F] : PreservesColimit K (F.mapAction G) :=
  Action.preservesColimit_of_preserves (F.mapAction G) K <| inferInstanceAs (PreservesColimit K (forget V G ⋙ F))

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