hasForgetToBoolAlg — Mathlib

English

There exists a forgetful functor from BoolRing to BoolAlg, sending each Boolean ring to the corresponding Boolean algebra and each morphism to the induced Boolean-algebra morphism.

Русский

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

LaTeX

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

Lean4

@[simps]
instance hasForgetToBoolAlg : HasForget₂ BoolRing BoolAlg
    where
  forget₂.obj X := .of (AsBoolAlg X)
  forget₂.map f := BoolAlg.ofHom f.hom.asBoolAlg

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