hasLimit_equivalence_comp — Mathlib

English

If e is an equivalence K ≌ J and HasLimit (e.functor ⋙ F), then HasLimit (e.functor ⋙ F).

Русский

Если e — эквивалентность K ≌ J и существует предел у (e.functor ⋙ F), то существует предел у той же композиции.

LaTeX

$$$\\mathrm{HasLimit}(e.functor \\;\\cdot\\; F)$$$

Lean4

instance hasLimit_equivalence_comp (e : K ≌ J) [HasLimit F] : HasLimit (e.functor ⋙ F) :=
  HasLimit.mk
    { cone := Cone.whisker e.functor (limit.cone F)
      isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) e }
      -- not entirely sure why this is needed

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