hasForgetToModule — Mathlib

English

There is a forgetful functor from AlgCat R to ModuleCat R, sending an algebra to its underlying module and an algebra homomorphism to its underlying linear map.

Русский

Существует забывающий функтор из AlgCat R в ModuleCat R, отправляющий алгебру в её базовый модуль и алгебраический гомоморфизм — в соответствующую линейную карту.

LaTeX

$$$\\text{forget}_2: \\mathrm{AlgCat}(R) \\to \\mathrm{ModuleCat}(R),\\ A \\mapsto \\mathrm{ModuleCat.of} R A,\\ f \\mapsto \\mathrm{ModuleCat.ofHom}(f.hom.toLinearMap)$$$

Lean4

instance hasForgetToModule : HasForget₂ (AlgCat.{v} R) (ModuleCat.{v} R) where
  forget₂ :=
    { obj := fun M => ModuleCat.of R M
      map := fun f => ModuleCat.ofHom f.hom.toLinearMap }

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