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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CommRingCat.free_obj_coe {α : Type u} :
    ↑(CommRingCat.free.obj α) = MvPolynomial α ℤ
    source
    @[simp]
    theorem CommRingCat.free_map_coe {α β : Type u} {f : α → β} :
    ⇑(CommRingCat.free.map f).hom = ⇑(MvPolynomial.rename f)
    source
    def CommRingCat.adj :
    CommRingCat.free ⊣ CategoryTheory.forget CommRingCat

    The free-forgetful adjunction for commutative rings.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance CommRingCat.instIsRightAdjointForget :
      (CategoryTheory.forget CommRingCat).IsRightAdjoint