instIsIsoLeftHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃

English

For φ: S1 ⟶ S2 with h1,h2 LeftHomologyData and epi/iso/mono hypotheses, the leftHomologyMap' φ h1 h2 is an isomorphism.

Русский

Для φ: S1 ⟶ S2 с данными левополной гомологии h1,h2 и условиями эпиморфизма/изоморфизма/моно, отображение leftHomologyMap' является изоморфизмом.

LaTeX

$$$leftHomologyMap'(\varphi\,h_{1}\,h_{2})$ is an isomorphism$$

Lean4

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

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