τ₁_ofEpiOfIsIsoOfMono_f' — Mathlib

English

For φ: S1 ⟶ S2 with epi φ.τ1, iso φ.τ2, mono φ.τ3, the equality φ.τ1 ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f' holds.

Русский

Для φ: S1 ⟶ S2 при условии, что φ.τ1 равно эпиморфизму, φ.τ2 изоморфизм и φ.τ3 моно, выполняется равенство φ.τ1 ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f'.

LaTeX

$$$\varphi.\tau_1 \circ (ofEpiOfIsIsoOfMono(\varphi,h)).f' = h.f'$$$

Lean4

@[simp]
theorem τ₁_ofEpiOfIsIsoOfMono_f' (φ : S₁ ⟶ S₂) (h : LeftHomologyData S₁) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] :
    φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f' := by
  rw [← cancel_mono (ofEpiOfIsIsoOfMono φ h).i, assoc, f'_i, ofEpiOfIsIsoOfMono_i, f'_i_assoc, φ.comm₁₂]

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