whiskerEquivalence_iff — Mathlib

English

For equivalence e: J ≌ K, IsVanKampenColimit(c.whisker e.functor) iff IsVanKampenColimit c.

Русский

Для эквивалентности e: J ≌ K верно: IsVanKampenColimit(c.whisker e.functor) ⇔ IsVanKampenColimit c.

LaTeX

$$$\\IsVanKampenColimit(c.whisker e.functor) \\iff \\IsVanKampenColimit(c)$$$

Lean4

theorem whiskerEquivalence_iff {K : Type*} [Category K] (e : J ≌ K) {F : K ⥤ C} {c : Cocone F} :
    IsUniversalColimit (c.whisker e.functor) ↔ IsUniversalColimit c :=
  ⟨fun hc ↦
    ((hc.whiskerEquivalence e.symm).precompose_isIso (e.invFunIdAssoc F).inv).of_iso
      (Cocones.ext (Iso.refl _) (by simp)),
    IsUniversalColimit.whiskerEquivalence e⟩

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