colimitsOfShape_isoClosure — Mathlib

English

Equality of colimits after iso-closure: P.isoClosure.colimitsOfShape J = P.colimitsOfShape J.

Русский

Равенство колимитов после изоморфического замыкания: P.isoClosure.colimitsOfShape J = P.colimitsOfShape J.

LaTeX

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

Lean4

@[simp]
theorem colimitsOfShape_isoClosure : P.isoClosure.colimitsOfShape J = P.colimitsOfShape J :=
  by
  refine le_antisymm ?_ (colimitsOfShape_monotone _ (P.le_isoClosure))
  intro X ⟨h⟩
  choose obj h₁ h₂ using h.prop_diag_obj
  exact
    ⟨{  toColimitPresentation := h.changeDiag (h.diag.isoCopyObj obj (fun j ↦ (h₂ j).some)).symm
        prop_diag_obj := h₁ }⟩

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