instIsIsoRightHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃

English

Given φ, h1, h2 with epi on τ1 and iso on τ2, the map rightHomologyMap' φ h1 h2 is an isomorphism.

Русский

При φ, h1, h2 с эпиморфизмом τ1 и изоморфизмом τ2 карта rightHomologyMap' φ h1 h2 является изоморфизмом.

LaTeX

$$$\\text{IsIso}(\\mathrm{rightHomologyMap}'\\ φ\\ h_1\\ h_2)$$$

Lean4

instance (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] :
    IsIso (rightHomologyMap' φ h₁ h₂) :=
  by
  let h₂' := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
  haveI : IsIso (rightHomologyMap' φ h₁ h₂') :=
    by
    rw [(RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).rightHomologyMap'_eq]
    dsimp
    infer_instance
  have eq := rightHomologyMap'_comp φ (𝟙 S₂) h₁ h₂' h₂
  rw [comp_id] at eq
  rw [eq]
  infer_instance

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