hom_isIso — Mathlib

English

If s and t are cocones that are colimit cocones, then any morphism f: s ⟶ t is an isomorphism.

Русский

Если коконы s и t являются колимитными коконами, то любой морфизм f: s ⟶ t является изоморфизмом.

LaTeX

$$$ \forall {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (f : s ⟶ t), IsIso f $$$

Lean4

/-- Any cocone morphism between colimit cocones is an isomorphism. -/
theorem hom_isIso {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (f : s ⟶ t) : IsIso f :=
  ⟨⟨Q.descCoconeMorphism s, ⟨P.uniq_cocone_morphism, Q.uniq_cocone_morphism⟩⟩⟩

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