hasForgetToAlgCat — Mathlib

English

There exists a forgetful two-step functor from CommAlgCat R to AlgCat R, sending a commutative algebra to its underlying algebra over R.

Русский

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

LaTeX

$$$\text{HasForget₂}\ (CommAlgCat\ R)\ (AlgCat\ R)$$$

Lean4

instance hasForgetToAlgCat : HasForget₂ (CommAlgCat.{v} R) (AlgCat.{v} R)
    where
  forget₂.obj A := .of R A
  forget₂.map f := AlgCat.ofHom f.hom

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