English
For X, Y objects with binary biproducts, and a bilimit-bicone b, the inverse cone point unique up to iso is the biprod.desc of inl and inr: (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv = biprod.desc b.inl b.inr.
Русский
Для X, Y объектов с бинарными биобразованиями и билилимитного биконуса b, обратный конус точки уникальности до изоморфизма равен biprod.desc b.inl b.inr.
LaTeX
$$$\left( hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)\right).inv = \mathrm{biprod.desc} \ b.inl \ b.inr$$$
Lean4
/-- Auxiliary lemma for `biprod.uniqueUpToIso`. -/
theorem conePointUniqueUpToIso_inv (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y} (hb : b.IsBilimit) :
(hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit _ _)).inv = biprod.desc b.inl b.inr :=
by
refine biprod.hom_ext' _ _ (hb.isLimit.hom_ext fun j => ?_) (hb.isLimit.hom_ext fun j => ?_)
all_goals
simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]
rcases j with ⟨⟨⟩⟩
all_goals simp
