forget_preservesLimitsOfShape — Mathlib

English

The forgetful functor Mon.forget C: Mon C → C preserves limits of shape J when C has them.

Русский

Функтор забывания Mon.forget сохраняет пределы формы J, если C имеет пределы этой формы.

LaTeX

$$$ \text{PreservesLimitsOfShape } J (Mon.forget C)$$$

Lean4

instance forget_preservesLimitsOfShape : PreservesLimitsOfShape J (Mon.forget C) where
  preservesLimit := fun {F} =>
    preservesLimit_of_preserves_limit_cone (limitConeIsLimit F)
      (IsLimit.ofIsoLimit (limit.isLimit (F ⋙ Mon.forget C)) (forgetMapConeLimitConeIso F).symm)

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