hasForgetToCommRing — Mathlib

English

There exists a forgetful functor from BoolRing to CommRingCat, which sends a Boolean ring to its underlying commutative ring and a Boolean-ring hom to the corresponding ring hom.

Русский

Существуeт забывающий функтор из BoolRing в CommRingCat, отображающий булево кольцо в его базовое коммутативное кольцо и гомоморфизм булевого кольца в соответствующий гомоморфизм колец.

LaTeX

$$$\\exists F: \\text{BoolRing} \\to \\text{CommRingCat}\\,.$$$

Lean4

instance hasForgetToCommRing : HasForget₂ BoolRing CommRingCat where
  forget₂ :=
    { obj := fun R ↦ CommRingCat.of R
      map := fun f ↦ CommRingCat.ofHom f.hom }

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