Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
add comment

1 Answer

up vote 2 down vote accepted

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.