colimitEquivColimitType — Mathlib

English

There is a canonical (noncomputable) equivalence between the abstract colimit colimit F and the concrete quotient representation F.ColimitType, expressed as an equivalence of objects: colimit F ≃ F.ColimitType.

Русский

Существует каноническое (невычислимое) эквивалентность между абстрактным колимитом colimit F и конкретным представлением в виде квоты F.ColimitType: colimit F ≃ F.ColimitType.

LaTeX

$$$$ \text{colimit}_{F} \cong F.ColimitType. $$$$

Lean4

/-- The equivalence between the abstract colimit of `F` in `Type u`
and the "concrete" definition as a quotient.
-/
noncomputable def colimitEquivColimitType : colimit F ≃ F.ColimitType :=
  (IsColimit.coconePointUniqueUpToIso (colimit.isColimit F) (colimitCoconeIsColimit F)).toEquiv.trans
    (equivShrink _).symm

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