English
Whiskering a bilimit bicone yields a bilimit bicone; the correspondence is an equivalence.
Русский
Whiskering билилимита биконеуса дает билилимитный биконус; соответствие — эквивалентность.
LaTeX
$$$$ \\text{WhiskerIsBilimit}(c,g) : (c.whisker g).IsBilimit \\simeq c.IsBilimit. $$$$
Lean4
/-- Whiskering a bicone with an equivalence between types preserves being a bilimit bicone. -/
noncomputable def whiskerIsBilimitIff {f : J → C} (c : Bicone f) (g : K ≃ J) : (c.whisker g).IsBilimit ≃ c.IsBilimit :=
by
refine equivOfSubsingletonOfSubsingleton (fun hc => ⟨?_, ?_⟩) fun hc => ⟨?_, ?_⟩
· let this := IsLimit.ofIsoLimit hc.isLimit (Bicone.whiskerToCone c g)
let this := (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _) this
exact IsLimit.ofWhiskerEquivalence (Discrete.equivalence g) this
· let this := IsColimit.ofIsoColimit hc.isColimit (Bicone.whiskerToCocone c g)
let this := (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _) this
exact IsColimit.ofWhiskerEquivalence (Discrete.equivalence g) this
· apply IsLimit.ofIsoLimit _ (Bicone.whiskerToCone c g).symm
apply (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _).symm _
exact IsLimit.whiskerEquivalence hc.isLimit (Discrete.equivalence g)
· apply IsColimit.ofIsoColimit _ (Bicone.whiskerToCocone c g).symm
apply (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _).symm _
exact IsColimit.whiskerEquivalence hc.isColimit (Discrete.equivalence g)
