Multivariable polynomials on a type is the left adjoint of the forgetful functor from commutative rings to types.
The free functor Type u ⥤ CommRing sending a type X to the multivariable (commutative)
polynomials with variables x : X.
Equations
- CommRing.free = {obj := λ (α : Type u), CommRing.of (mv_polynomial α ℤ), map := λ (X Y : Type u) (f : X ⟶ Y), mv_polynomial.rename f, map_id' := CommRing.free._proof_1, map_comp' := CommRing.free._proof_2}
@[simp]
@[simp]
theorem
CommRing.free_map_coe
{α β : Type u}
{f : α → β} :
⇑(CommRing.free.map f) = ⇑(mv_polynomial.rename f)
The free-forgetful adjunction for commutative rings.
Equations
- CommRing.adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Type (max u_1 u_2)) (R : CommRing), mv_polynomial.hom_equiv, hom_equiv_naturality_left_symm' := CommRing.adj._proof_1, hom_equiv_naturality_right' := CommRing.adj._proof_2}