instLinearModuleCatForget₂ — Mathlib

English

The forgetful functor FGModuleCat R → ModuleCat R is R-linear, i.e., it preserves the R-linear structure on hom-sets.

Русский

Функтор FGModuleCat R → ModuleCat R линейный над R; он сохраняет R-структуру на множестве морфизмов.

LaTeX

$$$\text{forget}_2: FGModuleCat(R) \to ModuleCat(R)$ is Linear over $R$: for all morphisms $f$, $g$ and scalars $\lambda$, $\text{forget}_2(\lambda f)=\lambda\,\text{forget}_2(f)$ and $\text{forget}_2(f+g)=\text{forget}_2(f)+\text{forget}_2(g)$.$$

Lean4

instance : (forget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R)).Linear R where

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