Lean4
/-- Binary 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 `biprod.lift b.fst b.snd` and `biprod.desc b.inl b.inr`
are inverses of each other. -/
@[simps]
def uniqueUpToIso (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y} (hb : b.IsBilimit) : b.pt ≅ X ⊞ Y
where
hom := biprod.lift b.fst b.snd
inv := biprod.desc b.inl b.inr
hom_inv_id := by
rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ← biprod.conePointUniqueUpToIso_inv X Y hb, Iso.hom_inv_id]
inv_hom_id := by
rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ← biprod.conePointUniqueUpToIso_inv X Y hb, Iso.inv_hom_id]
-- There are three further variations,
-- about `IsIso biprod.inr`, `IsIso biprod.fst` and `IsIso biprod.snd`,
-- but any one suffices to prove `indecomposable_of_simple`
-- and they are likely not separately useful.
