unit_map_one — Mathlib

English

For any morphism f, the unit map sends 1 to 1: unit map preserves multiplicative identity under restriction maps.

Русский

Для любого морфизма f единичное отображение отправляет 1 в 1: отображение единицы сохраняет тождество умножения при ограничении.

LaTeX

$$$ (unit\ R).map\ f (1) = (1).$$$$

Lean4

theorem unit_map_one {X Y : Cᵒᵖ} (f : X ⟶ Y) : (unit R).map f (1 : R.obj X) = (1 : R.obj Y) :=
  (R.map f).hom.map_one

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