isIso_opcyclesMap_of_isIso_of_epi'

English

Let φ : S₁ ⟶ S₂ be a morphism of SnakeInputs with φ.τ₂ an isomorphism and φ.τ₁ epi; if S₁ and S₂ admit right homology, then opcyclesMap φ is an isomorphism.

Русский

Пусть φ: S₁ ⟶ S₂ — морфизм SnakeInput, причём φ.τ₂ изоморфно, а φ.τ₁ эпиморфизм; если S₁ и S₂ имеют правую однородность, то opcyclesMap φ является изоморфизмом.

LaTeX

$$$$ \operatorname{IsIso}(\mathrm{opcyclesMap}(\varphi)) $$$$

Lean4

theorem isIso_opcyclesMap_of_isIso_of_epi' (φ : S₁ ⟶ S₂) (h₂ : IsIso φ.τ₂) (h₁ : Epi φ.τ₁) [S₁.HasRightHomology]
    [S₂.HasRightHomology] : IsIso (opcyclesMap φ) :=
  isIso_opcyclesMap'_of_isIso_of_epi φ h₂ h₁ _ _

Похожие утверждения