0
$\begingroup$

Context: I am trying to formalize the definition of a polynomial ring in a programming language. One way to think about it, is to start by formulating the definition of a ring extension by adjoining elements. In my programming formulation, I created a type for rings, and a type for variables. I am working from the following definition for polynomial rings: Let $R$ be a ring and $x$ be a variable. $R[x]$ is a polynomial ring. That is, the smallest ring that contains both $R$ and $x$.

My question: What is the type for the 'adjoin' operator? My guess is $[\ ]: \mbox{Ring} \times \mbox{Variable} \rightarrow \mbox{Ring}$ (I'm just concerned with the type, not the semantics). Also, what is this called (a function that takes a ring and produces a ring)? Because I can use any properties of such operator (e.g. identity laws, associativity, etc.) in my program and do some reasoning.

Note: These are possibly the wrong tags.

1 Answers 1

2

That looks fine to me. In the language of category theory, "adjoin" is more than a function that produces rings from rings: it is a functor from the category of rings to itself because it also sends ring homomorphisms $R \to S$ to ring homomorphisms $R[x] \to S[x]$ in a way which satisfies certain natural compatibility conditions.