preservesLimitsOfSize_map — Mathlib

English

The functor map f in the Under category preserves limits of size w.r.t. forgetful functor, assuming the base category has the corresponding limits.

Русский

Функтор map f в Under сохраняет предельные объекты заданного размера, при условии, что в базовой категории соответствующие пределы существуют.

LaTeX

$$$ [\\text{HasLimitsOfSize } J\, C] \\Rightarrow [\\text{PreservesLimitsOfSize } (\\mathrm{Under.map}\, f)]. $$$

Lean4

instance preservesLimitsOfSize_map [HasLimitsOfSize.{w, w'} C] {Y : C} (f : X ⟶ Y) :
    PreservesLimitsOfSize.{w, w'} (map f) :=
  preservesLimits_of_reflects_of_preserves (map f) (forget X)

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