instFullRingCatForget₂ — Mathlib

English

The underlying ring homomorphism component of a morphism f in CommRingCat coincides with the hom component of its image under the forgetful functor to RingCat.

Русский

Компонента кольцевого гомоморфизма f в CommRingCat совпадает с гомоморфизмом f при отображении через забывающий функтор к RingCat.

LaTeX

$$$((\mathrm{forget₂} CommRingCat RingCat).map f).hom = f.hom$$$

Lean4

instance : (forget₂ CommRingCat RingCat).Full :=
  fullyFaithfulForget₂ToRingCat.full

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