postcomposeHomEquiv — Mathlib

English

From a natural isomorphism α: F ≅ G, and cones c and d with a given isomorphism w between post-composed cones, there is an equivalence IsLimit c ≃ IsLimit d.

Русский

Из натурального изоморфизма α: F ≅ G и конусов c и d с изоморфизмом w между конусами после композиции, следует эквивалентость IsLimit c ≃ IsLimit d.

LaTeX

$$$\\text{equivOfNatIsoOfIso }(\\alpha)(c)(d)(w): IsLimit(c) \\simeq IsLimit(d)$$$

Lean4

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

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