mathlib3 documentation

algebra.category.Ring.adjunctions

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

noncomputable def CommRing.free  :

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

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

The free-forgetful adjunction for commutative rings.

Equations