mathlib documentation

algebra.category.Ring.adjunctions

Multivariable polynomials on a type is the left adjoint of the forgetful functor from commutative rings to types.

noncomputable def CommRing.free  :
Type u CommRing

The free functor Type u ⥤ CommRing sending a type X to the multivariable (commutative) polynomials with variables x : X.

Equations
@[simp]
theorem CommRing.free_obj_coe {α : Type u} :
@[simp]
theorem CommRing.free_map_coe {α β : Type u} {f : α → β} :

The free-forgetful adjunction for commutative rings.

Equations