isIso_opcyclesMap'_of_isIso_of_epi

English

If φ is an isomorphism on τ2 and epi on τ1, then opcyclesMap φ is an isomorphism between left cycles data.

Русский

Если φ изоморфен на τ2 и эпиморфизм на τ1, то opcyclesMap φ — изоморфизм между данными левых опциклов.

LaTeX

$$$\\text{IsIso}(\\mathrm{opcyclesMap}\\ φ)$$$

Lean4

theorem isIso_opcyclesMap'_of_isIso_of_epi (φ : S₁ ⟶ S₂) (h₂ : IsIso φ.τ₂) (h₁ : Epi φ.τ₁) (h₁ : S₁.RightHomologyData)
    (h₂ : S₂.RightHomologyData) : IsIso (opcyclesMap' φ h₁ h₂) :=
  by
  refine ⟨h₂.descQ (inv φ.τ₂ ≫ h₁.p) ?_, ?_, ?_⟩
  · simp only [← cancel_epi φ.τ₁, comp_zero, φ.comm₁₂_assoc, IsIso.hom_inv_id_assoc, h₁.wp]
  · simp only [← cancel_epi h₁.p, p_opcyclesMap'_assoc, h₂.p_descQ, IsIso.hom_inv_id_assoc, comp_id]
  · simp only [← cancel_epi h₂.p, h₂.p_descQ_assoc, assoc, p_opcyclesMap', IsIso.inv_hom_id_assoc, comp_id]

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