comp_mk_id — Mathlib

English

If α is a SmallHom from X to Y, composing with the identity morphism on Y yields α.

Русский

Если α — SmallHom от X к Y, композиция с тождественным морфизмом на Y не изменяет α.

LaTeX

$$$\alpha \circ \mathrm{mk}\,W\,\mathrm{id}_Y = \alpha$$$

Lean4

@[simp]
theorem comp_mk_id [HasSmallLocalizedHom.{w} W X Y] [HasSmallLocalizedHom.{w} W Y Y] (α : SmallHom.{w} W X Y) :
    α.comp (mk W (𝟙 Y)) = α :=
  (equiv W W.Q).injective (by simp [equiv_comp])

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