instFullSemiRingCatForget₂ — Mathlib

English

The forgetful functor forget₂ CommSemiRingCat SemiRingCat is full; i.e., every semiring-hom between forgetful images arises as the image of some commutative semiring-hom.

Русский

Забывающий функтор forget₂ CommSemiRingCat SemiRingCat является полным; то есть любой полугомоморфизм между забытыми образами является образом некоторого коммутативного полукольцевого гомоморфизма.

LaTeX

$$$(\text{forget₂ CommSemiRingCat SemiRingCat}).{\text{Full}}$; equivalently, for all X,Y, the map$$

Lean4

instance : (forget₂ CommSemiRingCat SemiRingCat).Full :=
  fullyFaithfulForget₂ToSemiRingCat.full

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