instConcreteCategoryRingHomCarrier

English

The category of Boolean rings is equipped with a concrete-category structure via the forgetful functor to ring homs.

Русский

У категории булевых колец имеется структура конкретной категории через забывающий функтор к гомоморфизмам колец.

LaTeX

$$$\text{BoolRing}.instConcreteCategoryRingHomCarrier$$$

Lean4

instance : ConcreteCategory BoolRing (· →+* ·) where
  hom f := f.hom'
  ofHom f := ⟨f⟩

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