postcomposeInvEquiv — Mathlib

English

If F and G are connected by an equivalence of functors, postcomposition with α.inv induces an equivalence IsLimit((Cones.postcompose α.inv).obj c) ≃ IsLimit c.

Русский

Если F и G связаны эквивалентностью функторов, постсоединение через α.inv задаёт эквивалентность IsLimit((Cones.postcompose α.inv).obj c) ≃ IsLimit c.

LaTeX

$$$ IsLimit((Cones.postcompose α.inv).obj c) \\simeq IsLimit(c) $$$

Lean4

/-- A cone postcomposed with the inverse of a natural isomorphism is a limit cone if and only if
the original cone is.
-/
def postcomposeInvEquiv {F G : J ⥤ C} (α : F ≅ G) (c : Cone G) :
    IsLimit ((Cones.postcompose α.inv).obj c) ≃ IsLimit c :=
  postcomposeHomEquiv α.symm c

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