mapActionPreservesLimit_of_preserves

English

Let J be a category and K : J ⥤ Action V G with HasLimit (K ⋙ forget V G) and PreservesLimit (K ⋙ forget V G) F. Then F.mapAction G preserves the limit of K.

Русский

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

LaTeX

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

Lean4

/-- `F.mapAction : Action V G ⥤ Action W G` preserves the limit of some `K : J ⥤ Action V G` if
`K ⋙ forget V G` has a limit and `F` preserves the limit of `K ⋙ forget V G`. -/
instance mapActionPreservesLimit_of_preserves (K : J ⥤ Action V G) [HasLimit (K ⋙ forget V G)]
    [PreservesLimit (K ⋙ Action.forget V G) F] : PreservesLimit K (F.mapAction G) :=
  Action.preservesLimit_of_preserves (F.mapAction G) K <| inferInstanceAs (PreservesLimit K (forget V G ⋙ F))

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