Documentation

Mathlib.Algebra.Category.Ring.Adjunctions

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

source
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.

Instances For
    source
    @[simp]
    theorem CommRingCat.free_obj_coe {α : Type u} :
    ↑(CommRingCat.free.obj α) = MvPolynomial α ℤ
    source
    @[simp]
    theorem CommRingCat.free_map_coe {α : Type u} {β : Type u} {f : α → β} :
    ↑(CommRingCat.free.map f) = ↑(MvPolynomial.rename f)
    source
    def CommRingCat.adj :
    CommRingCat.free ⊣ CategoryTheory.forget CommRingCat

    The free-forgetful adjunction for commutative rings.

    Instances For
      source
      instance CommRingCat.instIsRightAdjointTypeTypesCommRingCatInstCommRingCatLargeCategoryForgetInstConcreteCategoryCommRingCatInstCommRingCatLargeCategory :
      CategoryTheory.IsRightAdjoint (CategoryTheory.forget CommRingCat)