cancel_unit_right_assoc — Mathlib

English

For composable morphisms with a unit at the end, a right cancellation holds: f ≫ g ≫ unit Y = f' ≫ g' ≫ unit Y iff f ≫ g = f' ≫ g'.

Русский

Для правой композиции имеется тождественная отмена: f g = f' g' эквивалентно f g ≫ unit = f' g' ≫ unit.

LaTeX

$$$\forall {W,X,X',Y}\; (f: W\to X)(g: X\to Y)(f': W\to X')(g': X'\to Y),\; f\!\to\! g \;\text{и} \; f'\!\to\! g' \;\Rightarrow\; f \cdot g \cdot u_Y = f' \cdot g' \cdot u_Y \iff f \cdot g = f' \cdot g'$$$

Lean4

@[simp]
theorem cancel_unit_right_assoc {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) :
    f ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g' := by simp only [← Category.assoc, cancel_mono]

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