I'm reviewing my abstract algebra a bit. Currently looking at UFDs. In this context, Gauss's lemma (or part of it, at least) says that the product of two primitive polynomials over a UFD is primitive.
It seems to me that Gauss's lemma follows pretty easily from the Theorem that $R[x]$ is a UFD when $R$ is. However, this is a bit logically backwards, since I think Gauss's lemma is a sort of a preliminary step towards proving exactly that theorem?
Argument: Let $R$ be a UFD. Suppose that $p(x)q(x)$ is not primitve, where $p(x),q(x) \in R[x]$. Thus, there must be some nonunit element of $R$ dividing $p(x)q(x)$. It follows that there is an irreducible $r$ of $R$ which divides $p(x)q(x)$. Now it is easy to see that an irreducible element of $R$ is still an irreducible element of $R[x]$ (degrees add, so you can't factor a constant into anything but constants). Since $R[x]$ is a UFD, its irreducibles are also prime, so $r$ is a prime element of $R[x]$. Then, from $r|p(x)q(x)$, we get that $r|p(x)$ or $r|q(x)$, so one of $p(x)$ or $q(x)$ is not primitive.
My question is sort of a philisophical one:
Question: Is it correct to think of Gauss's lemma as just a partial result which is then superseded by the Theorem: "$R$ a UFD implies $R[x]$ a UFD", or am I somehow missing out on something here? In other words, is this roughly how you think of Gauss's Lemma, or do you view it as a useful result in its own right?
There seem to be two different approaches to thinking about Gauss' Lemma.
The first approach, the one you're talking about, does not quite require unique factorization, but holds for arbitrary GCD domains, where factorizations into irreducibles may not exist at all. The proof resembles the classical proof using a notion of "content".
But there is a second approach that avoids this entirely—that doesn't work for all UFDs, but works for $\mathbb{Z}$—which is to use the fact that $\mathbb{Z}$ is a [Bézout domain] to show that the coefficients of primitive polynomials generate the unit ideal, then using only basic commutative ring theory.