whiskerEquivalenceEquiv — Mathlib

English

Given an equivalence of diagrams e: K ≌ J, the IsLimit structure is transported along whiskering: there is an equivalence IsLimit s ≃ IsLimit (s.whisker e.functor).

Русский

Пусть e: K ≌ J — эквивалентность диаграмм; IsLimit конуса переводится вдоль whisker: IsLimit s ≃ IsLimit (s.whisker e.functor).

LaTeX

$$$\\text{whiskerEquivalenceEquiv } e:\\ IsLimit(s) \\simeq IsLimit(s.\\text{whisker } e.functor) $$$

Lean4

/-- Given an equivalence of diagrams `e`, `s` is a limit cone iff `s.whisker e.functor` is.
-/
def whiskerEquivalenceEquiv {s : Cone F} (e : K ≌ J) : IsLimit s ≃ IsLimit (s.whisker e.functor) :=
  ⟨fun h => h.whiskerEquivalence e, ofWhiskerEquivalence e, by cat_disch, by cat_disch⟩

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