English
Analogous to cones, whiskering a cocone corresponds to precomposition with a fixed equivalence and whiskering the cocone.
Русский
Аналогично конусам, whiskering коконуса соответствует предварительному композиции с фиксированной эквивалентностью и whisker-у коконуса.
LaTeX
$$$$ (c.whisker g).toCocone \\cong (Cocones.precompose (Discrete.functorComp f g).hom).obj (c.toCocone.whisker (Discrete.functor (Discrete.mk \\circ g))). $$$$
Lean4
/-- Taking the cocone of a whiskered bicone results in a cone isomorphic to one gained
by whiskering the cocone and precomposing with a suitable isomorphism. -/
def whiskerToCocone {f : J → C} (c : Bicone f) (g : K ≃ J) :
(c.whisker g).toCocone ≅
(Cocones.precompose (Discrete.functorComp f g).hom).obj
(c.toCocone.whisker (Discrete.functor (Discrete.mk ∘ g))) :=
Cocones.ext (Iso.refl _) (by simp)
