English
Given φ, if mor1 and mor3 are isos, mor2 is iso.
Русский
Пусть дан φ; если mor1 и mor3 изоморфизмы, mor2 изоморфизм.
LaTeX
$$$(T,T' \\in \\mathrm{distTriang} \\, C) \\Rightarrow \\mathrm{IsIso}(\\phi.hom_1) \\Rightarrow \\mathrm{IsIso}(\\phi.hom_3) \\Rightarrow \\mathrm{IsIso}(\\phi.hom_2)$$$
Lean4
/-- Given a distinguished triangle `T` such that `T.mor₃ = 0` and the datum of morphisms
`inr : T.obj₃ ⟶ T.obj₂` and `fst : T.obj₂ ⟶ T.obj₁` satisfying suitable relations, this
is the binary biproduct data expressing that `T.obj₂` identifies to the binary
biproduct of `T.obj₁` and `T.obj₃`.
See also `exists_iso_binaryBiproduct_of_distTriang`. -/
@[simps]
def binaryBiproductData (T : Triangle C) (hT : T ∈ distTriang C) (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂)
(inr_snd : inr ≫ T.mor₂ = 𝟙 _) (fst : T.obj₂ ⟶ T.obj₁) (total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂) :
BinaryBiproductData T.obj₁ T.obj₃ := by
have : Mono T.mor₁ := T.mono₁ hT hT₀
have eq : fst ≫ T.mor₁ = 𝟙 T.obj₂ - T.mor₂ ≫ inr := by rw [← total, add_sub_cancel_right]
exact
{ bicone :=
{ pt := T.obj₂
fst := fst
snd := T.mor₂
inl := T.mor₁
inr := inr
inl_fst := by
simp only [← cancel_mono T.mor₁, assoc, id_comp, eq, comp_sub, comp_id,
comp_distTriang_mor_zero₁₂_assoc _ hT, zero_comp, sub_zero]
inl_snd := comp_distTriang_mor_zero₁₂ _ hT
inr_fst := by
simp only [← cancel_mono T.mor₁, assoc, eq, comp_sub, reassoc_of% inr_snd, comp_id, sub_self, zero_comp]
inr_snd := inr_snd }
isBilimit := isBinaryBilimitOfTotal _ total }
