cancel_unit_right — Mathlib

English

In an equivalence e, postcomposition with the unit at Y is injective on morphisms with fixed domain W and codomain Y; i.e., equality after composing with the unit implies equality of the original morphisms.

Русский

В эквивалентности e посткомпозиция по единице в Y инъективна на отображениях с фиксированными началом W и концом Y: равенство после композиции с единицей даёт равенство исходных морфизмов.

LaTeX

$$$\forall X,Y\, (f,g : X\to Y),\; f\,\xrightarrow{\;\mathrm{unit}\;Y\;} = g\,\xrightarrow{\;\mathrm{unit}\;Y\;} \;\Rightarrow\; f=g$$$

Lean4

@[simp]
theorem cancel_unit_right {X Y : C} (f f' : X ⟶ Y) : f ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f' := by
  simp only [cancel_mono]

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