forgetToRingCat_obj — Mathlib

English

The underlying type of the forgetful image of a commutative ring object is exactly the ring's carrier as a type.

Русский

Типовая часть изображения через забывающий функтор совпадает с носителем кольца как тип.

LaTeX

$$$(((\mathrm{forget}\,2 \; CommRingCat\; RingCat).{\mathrm{obj}}\ R) : \mathrm{Type}) = R$$$

Lean4

@[simp]
theorem forgetToRingCat_obj {R : CommRingCat} : (((forget₂ CommRingCat RingCat).obj R) : Type u) = R :=
  rfl

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