cancel_iso_hom_right_assoc — Mathlib

English

For any W,X,X',Y,Z and morphisms f, g, f', g' with an isomorphism h: Y ≅ Z, equality f ≫ g ≫ h.hom = f' ≫ g' ≫ h.hom holds iff f ≫ g = f' ≫ g'.

Русский

Для любых W,X,X',Y,Z и морфизмов f, g, f', g' с изоморфизмом h: Y ≅ Z, равенство f ≫ g ≫ h.hom = f' ≫ g' ≫ h.hom верно тогда и только тогда, когда f ≫ g = f' ≫ g'.

LaTeX

$$$f \\!\\circ\\! g \\!\\circ\\! h.hom = f' \\!\\circ\\! g' \\!\\circ\\! h.hom \\iff f \\!\\circ\\! g = f' \\!\\circ\\! g'$$$

Lean4

@[simp]
theorem cancel_iso_hom_right_assoc {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) (h : Y ≅ Z) :
    f ≫ g ≫ h.hom = f' ≫ g' ≫ h.hom ↔ f ≫ g = f' ≫ g' := by simp only [← Category.assoc, cancel_mono]

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