conePointUniqueUpToIso_inv — Mathlib

English

The inverse of the conePointUniqueUpToIso is the biproduct desc of b.ι.

Русский

Обратный к изоморфизму conePointUniqueUpToIso — biproduct.desc b.ι.

LaTeX

$$$ (hb.isLimit.conePointUniqueUpToIso (biproduct.isLimit _)).inv = biproduct.desc b.ι $$$

Lean4

/-- Auxiliary lemma for `biproduct.uniqueUpToIso`. -/
theorem conePointUniqueUpToIso_inv (f : J → C) [HasBiproduct f] {b : Bicone f} (hb : b.IsBilimit) :
    (hb.isLimit.conePointUniqueUpToIso (biproduct.isLimit _)).inv = biproduct.desc b.ι := by
  classical
  refine biproduct.hom_ext' _ _ fun j => hb.isLimit.hom_ext fun j' => ?_
  rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app, biproduct.bicone_π,
    biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]

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