hasForgetToBoolRing — Mathlib

English

There exists a forgetful functor from BoolAlg to BoolRing, sending a Boolean algebra to its underlying Boolean ring and a Boolean-algebra homomorphism to the corresponding ring homomorphism.

Русский

Существует забывающий функтор из BoolAlg в BoolRing, отправляющий булеву алгебру в соответствующее булево кольцо и гомоморфизм булевых алгебр в соответствующий гомоморфизм колец.

LaTeX

$$$\\exists F: \\text{BoolAlg} \\to \\text{BoolRing}$$$

Lean4

@[simps]
instance hasForgetToBoolRing : HasForget₂ BoolAlg BoolRing
    where
  forget₂.obj X := .of (AsBoolRing X)
  forget₂.map f := BoolRing.ofHom <| BoundedLatticeHom.asBoolRing f.hom

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