forget_map — Mathlib

English

The forgetful functor sends a morphism f in CommGrpCat to its underlying function between carriers.

Русский

Забывающий функтор отображает морфизм f в CommGrpCat к его базовой функции между носителями.

LaTeX

$$$ (\\mathrm{forget}\\,\\mathrm{CommGrpCat}).map f = (f : X \\to Y) $$$

Lean4

@[to_additive (attr := simp)]
theorem forget_map {X Y : CommGrpCat} (f : X ⟶ Y) : (forget CommGrpCat).map f = (f : X → Y) :=
  rfl

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