forget_map_apply — Mathlib

English

For any morphism f in RingCat and any x in the forgetful target of the source, applying the forgetful functor to f and then evaluating at x yields the same result as applying f to x.

Русский

Для любого морфизма f в RingCat и любого x в источникe, применение забывающего функторa к f и затем вычисление на x даёт тот же результат, что и применение f к x.

LaTeX

$$$\forall f:\, R \to S,\forall x:\, (\mathrm{forget}\,RingCat).obj R,\; (\mathrm{forget}\,RingCat).map\;f\;x = f\;x$$$

Lean4

theorem forget_map_apply {R S : RingCat} (f : R ⟶ S) (x : (CategoryTheory.forget RingCat).obj R) :
    (forget _).map f x = f x :=
  rfl

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