ofEpiOfIsIsoOfMono'_f' — Mathlib

English

For φ: S1 ⟶ S2 with h : LeftHomologyData S₂ and epi/iso/mono hypotheses, (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'.

Русский

Для φ: S1 ⟶ S2 при данных гипотез эпиморфизма/изоморфизма/моно, выполняется (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'.

LaTeX

$$$(ofEpiOfIsIsoOfMono'(\varphi,h)).f' = \varphi.\tau_1 \circ 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, f'_i, ofEpiOfIsIsoOfMono'_i, assoc, f'_i_assoc, φ.comm₁₂_assoc,
    IsIso.hom_inv_id, comp_id]

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