fullyFaithfulForget₂ToSemiRingCat

English

The forgetful functor is fully faithful from RingCat to SemiRingCat.

Русский

Забывающий функтор из RingCat в SemiRingCat полно и точно сохраняет морфизмы.

LaTeX

$$$ (forget₂ RingCat SemiRingCat).FullyFaithful. $$$

Lean4

/-- The forgetful functor from `RingCat` to `SemiRingCat` is fully faithful. -/
def fullyFaithfulForget₂ToSemiRingCat : (forget₂ RingCat SemiRingCat).FullyFaithful where preimage f := ofHom f.hom

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