forget₂_module_obj — Mathlib

English

For any X in AlgCat R, the forget₂ functor to ModuleCat R sends X to ModuleCat.of R X.

Русский

Для любого X в AlgCat R забывающий функтор отправляет X в ModuleCat.of R X.

LaTeX

$$$(\\mathrm{forget}_2 (\\mathrm{AlgCat}\\ R) (\\mathrm{ModuleCat}\\ R)).\\mathrm{obj} X = \\mathrm{ModuleCat.of} R X$$$

Lean4

@[simp]
theorem forget₂_module_obj (X : AlgCat.{v} R) : (forget₂ (AlgCat.{v} R) (ModuleCat.{v} R)).obj X = ModuleCat.of R X :=
  rfl

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