isoClosure_strictColimitsOfShape — Mathlib

English

The iso-closure of strictColimitsOfShape equals colimitsOfShape: (P.strictColimitsOfShape J).isoClosure = P.colimitsOfShape J.

Русский

Изоморфное замыкание строгих колимитов по форме J совпадает с обычным колимитом: (P.strictColimitsOfShape J).isoClosure = P.colimitsOfShape J.

LaTeX

$$$$ (P.strictColimitsOfShape(J)).isoClosure = P.colimitsOfShape(J). $$$$

Lean4

@[simp]
theorem isoClosure_strictColimitsOfShape : (P.strictColimitsOfShape J).isoClosure = P.colimitsOfShape J :=
  by
  refine le_antisymm ?_ ?_
  · rw [isoClosure_le_iff]
    apply strictColimitsOfShape_le_colimitsOfShape
  · intro X ⟨h⟩
    have := h.hasColimit
    exact
      ⟨colimit h.diag, strictColimitsOfShape.colimit h.diag h.prop_diag_obj,
        ⟨h.isColimit.coconePointUniqueUpToIso (colimit.isColimit _)⟩⟩

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