forget₂_module_map — Mathlib

English

The forget₂ map on morphisms is given by taking the underlying linear map, i.e., (forget₂ (AlgCat R) (ModuleCat R)).map f = ModuleCat.ofHom f.hom.toLinearMap.

Русский

Отображение forget₂ на отображениях задано через соответствующую линейную карту: (forget₂ ...).map f = ModuleCat.ofHom f.hom.toLinearMap.

LaTeX

$$$(forget_2 (AlgCat R) (ModuleCat R)).\\mathrm{map} f = \\mathrm{ModuleCat.ofHom} (f.hom.toLinearMap)$$$

Lean4

@[simp]
theorem forget₂_module_map {X Y : AlgCat.{v} R} (f : X ⟶ Y) :
    (forget₂ (AlgCat.{v} R) (ModuleCat.{v} R)).map f = ModuleCat.ofHom f.hom.toLinearMap :=
  rfl

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