English
For X, Y objects and a binary biproduct isBilimit-bicone b, the isomorphism conePointUniqueUpToIso with respect to the binary biproduct limit is equal to biprod.lift of the first and second projections: (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).hom = biprod.lift b.fst b.snd.
Русский
Для объектов X, Y и биконуса b, являющегося билимтом бинарного биобразования, единичный конус точки уникальности до изоморфизма равен биобразованию biprod.lift первых и вторых проекций: (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).hom = biprod.lift b.fst b.snd.
LaTeX
$$$\left( hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)\right).hom = \mathrm{biprod.lift} \ b.fst \ b.snd$$$
Lean4
/-- Auxiliary lemma for `biprod.uniqueUpToIso`. -/
theorem conePointUniqueUpToIso_hom (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y} (hb : b.IsBilimit) :
(hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit _ _)).hom = biprod.lift b.fst b.snd :=
rfl
