isColimit_iff_isIso_inl — Mathlib

English

If X is initial, then a binary cofan X → Y is colimit iff its left inclusion is an isomorphism.

Русский

Если X начальный, то двоичный кофан X → Y предел когоморфизма тогда и только тогда, когда инл является изоморфизмом.

LaTeX

$$$$ (\exists H: IsColimit\, c) \iff IsIso(c.inl). $$$$

Lean4

theorem isColimit_iff_isIso_inl {X Y : C} (h : IsInitial Y) (c : BinaryCofan X Y) :
    Nonempty (IsColimit c) ↔ IsIso c.inl := by
  constructor
  · rintro ⟨H⟩
    obtain ⟨l, hl, -⟩ := BinaryCofan.IsColimit.desc' H (𝟙 X) (h.to X)
    refine ⟨⟨l, hl, BinaryCofan.IsColimit.hom_ext H (?_) (h.hom_ext _ _)⟩⟩
    rw [Category.comp_id]
    have e : (inl c ≫ l) ≫ inl c = 𝟙 X ≫ inl c := congrArg (· ≫ inl c) hl
    rwa [Category.assoc, Category.id_comp] at e
  · intro
    exact
      ⟨BinaryCofan.IsColimit.mk _ (fun f _ => inv c.inl ≫ f) (fun _ _ => IsIso.hom_inv_id_assoc _ _)
          (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ => (IsIso.eq_inv_comp _).mpr e⟩

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