isIso_homologyMap_of_isIso_opcyclesMap_of_mono

English

If opcyclesMap φ is an isomorphism and φ.τ₃ is mono, then homologyMap φ is an isomorphism.

Русский

Если opcyclesMap φ изоморфен и φ.τ₃ моно, то homologyMap φ изоморфен.

LaTeX

$$IsIso (homologyMap φ)$$

Lean4

theorem isIso_homologyMap_of_isIso_opcyclesMap_of_mono {φ : S₁ ⟶ S₂} [S₁.HasHomology] [S₂.HasHomology]
    (h₁ : IsIso (opcyclesMap φ)) (h₂ : Mono φ.τ₃) : IsIso (homologyMap φ) :=
  by
  have h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0 := by
    simp only [← cancel_mono φ.τ₃, zero_comp, assoc, ← fromOpcycles_naturality, IsIso.inv_hom_id_assoc,
      homologyι_comp_fromOpcycles]
  have ⟨z, hz⟩ := KernelFork.IsLimit.lift' S₁.homologyIsKernel _ h
  dsimp at hz
  refine ⟨⟨z, ?_, ?_⟩⟩
  · rw [← cancel_mono S₁.homologyι, id_comp, assoc, hz, homologyι_naturality_assoc, IsIso.hom_inv_id, comp_id]
  · rw [← cancel_mono S₂.homologyι, assoc, homologyι_naturality, reassoc_of% hz, IsIso.inv_hom_id, comp_id, id_comp]

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