isColimit — Mathlib

English

For a colimit cocone c for F, the associated Equiv hc.equiv between F.ColimitType and c.pt is an isomorphism of colimits.

Русский

Для колимитного кокона c для F соответствующее сопряжение hc.equiv является изоморфизмом колимитов.

LaTeX

$$hc.equiv : F.ColimitType ≃ c.pt$$

Lean4

theorem isColimit (hc : IsColimitCore.{max u w₀ w₁} c) : c.IsColimit where
  bijective :=
    by
    let e : F.ColimitType ≃ c.pt :=
      { toFun := F.descColimitType c
        invFun := (down.{max u w₁} hc).desc F.coconeTypes
        left_inv
          y := by
          obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y
          simp
        right_inv :=
          by
          have : (F.descColimitType c).comp ((down.{max u w₁} hc).desc F.coconeTypes) = id :=
            (down.{max u w₀} hc).funext
              (fun j ↦ by rw [Function.id_comp, Function.comp_assoc, fac, coconeTypes_ι, descColimitType_comp_ι])
          exact congr_fun this }
    exact e.bijective

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