hasForgetToCommRingCat — Mathlib

English

There is a forgetful “two-object” functor from CommAlgCat R to CommRingCat R, i.e., a forgetful functor retaining only the underlying ring structure.

Русский

Существуют забывающие функторы из CommAlgCat R в CommRingCat R, сохраняющие лишь основанную кольцевую структуру.

LaTeX

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

Lean4

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

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