cancel_counitInv_right_assoc — Mathlib

English

A variant where we have additional morphisms f,g,h and their primed counterparts; right cancellation with a unit stays valid when inserting an extra morphism h.

Русский

Вариант с дополнительными морфизмами f,g,h; сохранение отмены справа при вставке дополнительного h через единицу.

LaTeX

$$$\forall {W,X,X',Y,Y',Z} (f: W\to X)(g: X\to Y)(h: Y\to Z)(f': W\to X')(g': X'\to Y')(h': Y'\to Z),\; \\ f \;\cdot\; g \;\cdot\; h \;\cdot\; u_Z = f' \;\cdot\; g' \;\cdot\; h' \;\cdot\; u_Z \iff f \cdot g \cdot h = f' \cdot g' \cdot h'$$$

Lean4

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

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