uniqueUpToIso — Mathlib

Lean4
/-- Biproducts are unique up to isomorphism. This already follows because bilimits are limits,
but in the case of biproducts we can give an isomorphism with particularly nice definitional
properties, namely that `biproduct.lift b.π` and `biproduct.desc b.ι` are inverses of each
other. -/
@[simps]
def uniqueUpToIso (f : J → C) [HasBiproduct f] {b : Bicone f} (hb : b.IsBilimit) : b.pt ≅ ⨁ f
    where
  hom := biproduct.lift b.π
  inv := biproduct.desc b.ι
  hom_inv_id := by
    rw [← biproduct.conePointUniqueUpToIso_hom f hb, ← biproduct.conePointUniqueUpToIso_inv f hb, Iso.hom_inv_id]
  inv_hom_id := by
    rw [← biproduct.conePointUniqueUpToIso_hom f hb, ← biproduct.conePointUniqueUpToIso_inv f hb, Iso.inv_hom_id]
Похожие утверждения