Multivariable polynomials on a type is the left adjoint of the forgetful functor from commutative rings to types.
The free functor Type u ⥤ CommRingCat
sending a type X
to the multivariable (commutative)
polynomials with variables x : X
.
Instances For
@[simp]
@[simp]
theorem
CommRingCat.free_map_coe
{α : Type u}
{β : Type u}
{f : α → β}
:
↑(CommRingCat.free.map f) = ↑(MvPolynomial.rename f)
The free-forgetful adjunction for commutative rings.