whiskerEquivalenceEquiv — Mathlib

English

IsColimit is preserved by whiskering with an equivalence of categories. The equivalence whiskerEquivalenceEquiv gives an IsColimit equivalence with whiskered cocones.

Русский

IsColimit сохраняется при отталкивании (whiskering) по эквивалентности категорий. whiskerEquivalenceEquiv задаёт эквивалентность IsColimit для коконов, подвергшихся whisker.

LaTeX

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

Lean4

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

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