English
Let S1 and S2 be ShortComplex objects in a category with zero morphisms. If φ : S1 → S2 is a morphism whose τ₂ component is an isomorphism and whose τ₃ component is monic, and S1 and S2 carry left homology data h1 and h2, then the induced morphism cyclesMap' φ h1 h2 is an isomorphism.
Русский
Пусть S1 и S2 — короткие комплексы в категории с нулевыми морфизмами. Пусть φ : S1 → S2 — морфизм, такой что компонент τ₂ φ является изоморфизмом, а τ₃ φ — мономоризм, и у S1,S2 заданы данные левой гомологии h1 и h2. Тогда индуцированное отображение cyclesMap' φ h1 h2 является изоморфизмом.
LaTeX
$$$ (IsIso \, (\tau_2)) \land (Mono \, (\tau_3)) \rightarrow IsIso (cyclesMap' \, \phi \, h_1 \, h_2) $$$
Lean4
theorem isIso_cyclesMap'_of_isIso_of_mono (φ : S₁ ⟶ S₂) (h₂ : IsIso φ.τ₂) (h₃ : Mono φ.τ₃) (h₁ : S₁.LeftHomologyData)
(h₂ : S₂.LeftHomologyData) : IsIso (cyclesMap' φ h₁ h₂) :=
by
refine ⟨h₁.liftK (h₂.i ≫ inv φ.τ₂) ?_, ?_, ?_⟩
· simp only [assoc, ← cancel_mono φ.τ₃, zero_comp, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, h₂.wi]
· simp only [← cancel_mono h₁.i, assoc, h₁.liftK_i, cyclesMap'_i_assoc, IsIso.hom_inv_id, comp_id, id_comp]
· simp only [← cancel_mono h₂.i, assoc, cyclesMap'_i, h₁.liftK_i_assoc, IsIso.inv_hom_id, comp_id, id_comp]
