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

def CommRingCat.free : CategoryTheory.Functor (Type u) CommRingCat

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

Equations

• CommRingCat.free = CategoryTheory.Functor.mk { obj := fun (α : Type u) => CommRingCat.of (MvPolynomial α ℤ), map := fun {X Y : Type u} (f : X ⟶ Y) => ↑(MvPolynomial.rename f) }

@[simp]

theorem CommRingCat.free_obj_coe {α : Type u} : ↑(CommRingCat.free.toPrefunctor.obj α) = MvPolynomial α ℤ

@[simp]

theorem CommRingCat.free_map_coe {α : Type u} {β : Type u} {f : α → β} : ⇑(CommRingCat.free.toPrefunctor.map f) = ⇑(MvPolynomial.rename f)

def CommRingCat.adj : CommRingCat.free ⊣ CategoryTheory.forget CommRingCat

The free-forgetful adjunction for commutative rings.

Equations

• CommRingCat.adj = CategoryTheory.Adjunction.mkOfHomEquiv (CategoryTheory.Adjunction.CoreHomEquiv.mk fun (X : Type u) (R : CommRingCat) => MvPolynomial.homEquiv)

instance CommRingCat.instIsRightAdjointTypeTypesCommRingCatInstCommRingCatLargeCategoryForgetInstConcreteCategoryCommRingCatInstCommRingCatLargeCategory : CategoryTheory.IsRightAdjoint (CategoryTheory.forget CommRingCat)

Equations

• One or more equations did not get rendered due to their size.