extendIsoEquiv — Mathlib

English

A cocone extends along an isomorphism of apexes, and this extension gives an equivalence of IsColimit structures between the original cocone and its extension.

Русский

Кокон продолжается вдоль изоморфизма вершины, и это продолжение задаёт эквивалентность структур IsColimit между исходным коконом и его продолжением.

LaTeX

$$$ \text{extendIsoEquiv} : IsColimit s \simeq IsColimit (s.extend i) $$$

Lean4

/-- A cocone is a colimit cocone iff its extension by an isomorphism is. -/
def extendIsoEquiv {s : Cocone F} {X : C} (i : s.pt ⟶ X) [IsIso i] : IsColimit s ≃ IsColimit (s.extend i) :=
  equivOfSubsingletonOfSubsingleton (extendIso i) (ofExtendIso i)

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