ihom_obj — Mathlib

English

For field K and fg modules V,W, the internal hom object (ihom V).obj W is the FG-module corresponding to the space of linear maps V → W.

Русский

Для поля K и FG-модулей V,W внутреннее гом-объектное множество $(ihom V).obj W$ равно FG-модулю, соответствующему пространству линейных отображений $V \to W$.

LaTeX

$$$ (ihom\, V).\!\mathrm{obj}\!\; W = FGModuleCat.of\ K (V \to_W) $$$

Lean4

@[simp]
theorem ihom_obj : (ihom V).obj W = FGModuleCat.of K (V ⟶ W) :=
  rfl

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