isLimitMapConeEquiv — Mathlib

English

There is an equivalence between IsLimit structures after applying G to a kernel fork and the mapped kernel fork, i.e., the map of a kernel fork is limit iff the mapped one is.

Русский

Существуют эквивалентности пределов после применения G к ядровому форку и к мапу ядрового форка, то есть предел образованной конструкции эквивалентен пределу отображенного форка.

LaTeX

$$$\\text{isLimitMapConeEquiv} : \\IsLimit(G.mapCone c) \\simeq \\IsLimit(c.map G)$$$

Lean4

/-- The underlying cone of a kernel fork is mapped to a limit cone if and only if
the mapped kernel fork is limit. -/
def isLimitMapConeEquiv : IsLimit (G.mapCone c) ≃ IsLimit (c.map G) :=
  by
  refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)
  refine parallelPair.ext (Iso.refl _) (Iso.refl _) ?_ ?_ <;> simp
  exact Cones.ext (Iso.refl _) (by rintro (_ | _) <;> cat_disch)

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