A crash course in tensor products
We've defined \(\widehat{\mathbb{Q}}\) to be \(\mathbb{Q}\otimes\widehat{\mathbb{Z}}\). Whatever does this mean? Well just to orient yourself, if \(A\) and \(B\) are additive abelian groups, then \(A\otimes B\) is also an abelian group. And if \(A\) and \(B\) are commutative rings (as they are in our case), then \(A\otimes B\) is also a commutative ring.
Even if \(A\) and \(B\) are completely concrete commutative rings, their tensor product \(A\otimes B\) might be incomprehensible. For example \(\mathbb{C}\otimes\mathbb{C}\) is completely incomprehensible (note that we are tensoring over the integers). It is not like the product of groups or the disjoint union of two sets, where you have a completely explicit unambiguous formula for each element.
In this sense, the theory of tensor products is a bit like the theory of continuous functions. Humanity started off studying concrete polynomial equations such as \(x^2+1\) and then moved on to concrete analytic functions such as \(\log(x)\) and \(\sin(x)\), but eventually the abstract concept of a continuous function from the reals to the reals was born. There is no “formula” for a general continuous function, and continuous functions such as \(e^{-1/x^2}\) or \(|x|\) have no power series. Even if there were a formula for a specific continuous function of interest, it is not clear in general how to make sense of the claim that it's the “best” formula. In other words, there is no "canonical form" for a general continuous function, and yet we prove things about them anyway. We shall adopt the same attitude for elements of \(A\otimes B\).
The first thing to know about the tensor product \(A\otimes B\) of two abelian groups \(A\) and \(B\) is a “constructor” for the type. In other words, how can we make elements \(A\otimes B\)? Well, it turns out that given elements \(a\in A\) and \(b\in B\), we can form the element \(a\otimes_t b\in A\otimes B\).
Example. Recall that the sum of all the factorials is an element \(e\in\widehat{\mathbb{Z}}\), and \(22/7\) is certainly a rational number, so we can make the element \(\frac{22}{7}\otimes_te\in\widehat{\mathbb{Q}}\).
This example is in the Lean code.
Elements of the form \(a\otimes_t b\in A\otimes B\) are known as pure tensors. In the literature, pure tensors are often written \(a\otimes b\), but we shall follow mathlib's convention in reserving the \(\otimes\) symbol for groups like \(A \otimes B\), and adorning it with a \(t\) when using it on elements of the groups (or, as Lean calls them, terms, which explains the notation).
Addition of pure tensors obeys the “distributivity” rules \(a\otimes_t b_1+a\otimes_t b_2=a\otimes_t(b_1+b_2)\) and \(a_1\otimes_t b+a_2\otimes_t b=(a_1+a_2)\otimes_t b\), but there is no rule which simplifies a general sum \(a\otimes_t b + c\otimes_t d\) into a pure tensor. Indeed, in general it is not the case that every element of a tensor product \(A\otimes B\) is of the form \(a\otimes_t b\); there can be tensors which aren't pure. However every element of \(A\otimes B\) is a finite sum of pure tensors, with the result that one can attempt to define additive maps from \(A\otimes B\) by saying what they do on pure tensors, and then extending linearly.
Another thing worth understanding is that just like how rational numbers can be written as quotients of integers in several ways (for example \(1/2=2/4=3/6=\cdots\)), a general pure tensor in \(A\otimes B\) can be represented as \(a\otimes_t b\) in many ways. For example, in \(\widehat{\mathbb{Q}}\) we have \(1\otimes_t 2=2\otimes_t 1\). A general rule for equality of pure tensors is that if \(a\in A\) and \(b\in B\) and \(z\in\mathbb{Z}\), then \(za\otimes_tb=a\otimes_tzb\); integers can move over the tensor symbol. But equality is hard: in general there may not be an algorithm to decide whether two pure tensors \(a\otimes_t b\) and \(c\otimes_t d\) are equal in \(A\otimes B\).
Remark. A summary of the situation: if \(A\) and \(B\) are abelian groups, then every element of \(A\otimes B\) can be written in the form \(\sum_{i=1}^Na_i\otimes_tb_i\). It's just that this representation is highly nonunique, and furthermore given explicit elements \(a_1,a_2\in A\) and \(b_1,b_2\in B\) it might be a hard problem to figure out if \(a_1\otimes_t b_1=a_2\otimes_t b_2\).
For example, it turns out that \((\mathbb{Z}/2\mathbb{Z})\otimes(\mathbb{Z}/3\mathbb{Z})=0\) and so in this tensor product all the \(a\otimes_t b\) are equal to each other and to \(0\otimes 0\).
Having said all of that, one nice property of \(\widehat{\mathbb{Q}}\) is that every tensor is pure; let's prove this now.
LemmaQHat.canonicalForm#
Every element of \(\widehat{\mathbb{Q}}:=\mathbb{Q}\otimes\widehat{\mathbb{Z}}\) can be written as \(q\otimes_t z\) with \(q\in\mathbb{Q}\) and \(z\in\widehat{\mathbb{Z}}\). Furthermore one can even assume that \(q=\frac{1}{N}\) for some positive integer \(N\).
Proof
A proof I would write on the board would look like the following. Take a general element of \(\widehat{\mathbb{Q}}\); we know it can be expressed as a finite sum \(\sum_i q_i\otimes_t z_i\) with \(q_i\in\mathbb{Q}\) and \(z_i\in\widehat{\mathbb{Z}}\). Now choose a large positive integer \(N\), the lowest common multiple of all the denominators showing up in the \(q_i\), and then rewrite \(\sum_i q_i\otimes_t z_i\) as \(\sum_i \frac{n_i}{N}\otimes z_i\) with \(n_i\in\mathbb{Z}\). Now using the fundamental fact that \(na\otimes_t b=a\otimes_t nb\) for \(n\in\mathbb{Z}\), we can rewrite the sum as \(\sum_i \frac{1}{N}\otimes_t n_i z_i\) which is equal to the pure tensor \(\frac{1}{N}\otimes(\sum_i n_i z_i)\).
In Lean I would prove this using TensorProduct.induction_on, which quickly reduces us to the claim that the sum of two pure tensors is pure, which we can prove using the above technique whilst avoiding the general theory of finite sums.
Lean
Formalized as QHat.canonicalForm.
Sources
Uses 2 · Used by 2
Be careful though: just because every element of \(\widehat{\mathbb{Q}}\) can be written as \(q\otimes z\), this representation may not be unique. For example \(2\otimes 1=1\otimes 2\). However, writing \(\frac{1}{N}\otimes_t z\) as \(z/N\) does tempt us into the following definition.
DefinitionQHat.IsCoprime#
If \(N\in\mathbb{N}^+\) and \(z\in\widehat{\mathbb{Z}}\) then we say that \(N\) and \(z\) are coprime if \(z_N\in(\mathbb{Z}/N\mathbb{Z})^\times\). We write \(z/N\) as notation for the element \(\frac{1}{N}\otimes_tz\).
Uses 1 · Used by 1
LemmaQHat.lowestTerms#
Every element of \(\widehat{\mathbb{Q}}\) can be uniquely written as \(z/N\) with \(z\in\widehat{\mathbb{Z}}\), \(N\in\mathbb{N}^+\), and with \(N\) and \(z\) coprime.
Proof
Existence: by the previous lemma, an arbitrary element can be written as \(z/N\); let \(D\) be the greatest common divisor of \(N\) and \(z_N\) (lifted to a natural). If \(D=1\) then the fraction is by definition in lowest terms. However if \(1\lt D\mid N\) then \(z_D\) is the reduction of \(z_N\) and is hence 0. By lemma ZHat.multiples we deduce that \(z=Dy\) is a multiple of \(D\), and hence \(z/N=\frac{1}{N}\otimes_tDy=\frac{1}{E}\otimes y\), where \(E=N/D\). Now if a natural divided both \(y_E\) and \(E\) then this natural would divide both \(z_N/D\) and \(N/D\), contradicting the fact that \(D\) is the greatest common divisor.
Uniqueness: if \(z/N=w/M\), we deduce \(1\otimes_t Mz=1\otimes_t Nw\), and by injectivity of \(\widehat{\mathbb{Z}}\to\widehat{\mathbb{Q}}\) we deduce that \(Mz=Nw=y\). In particular, if \(L\) is the lowest common multiple of \(M\) and \(N\) then \(y_L\) is a multiple of both \(M\) and \(N\) and is hence zero, so \(y=Lx\) is a multiple of \(L\) by ZHat.multiples, and we deduce from torsionfreeness that \(z=(L/M)x\) and \(w=(L/N)x\). If some prime divided \(L/M\) then it would have to divide \(N\) which means that \(z\) is not in lowest terms; similarly if some prime divided \(L/N\) then \(w/M\) would not be in lowest terms. We deduce that \(L=M=N\) and hence \(z=w\) by torsionfreeness.
Lean
Stated as QHat.lowestTerms; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 2
If \(A\) and \(B\) are additive abelian groups then \(A\otimes B\) is also an additive abelian group. However if \(A\) and \(B\) are commutative rings, then \(A\otimes B\) also inherits the structure of a commutative ring, with \(0=0\otimes_t 0\) and \(1=1\otimes_t 1\). Pure tensors multiply in the obvious way: the product of \(a_1\otimes_t b_1\) and \(a_2\otimes_t b_2\) is \(a_1a_2\otimes_t b_1b_2.\) There are ring homomorphisms \(A\to A\otimes B\) and \(B\to A\otimes B\) sending \(a\) to \(a\otimes_t 1\) and \(b\) to \(1\otimes_t b\). In general such maps are not injective, but in the case of \(\widehat{\mathbb{Q}}=\mathbb{Q}\otimes\widehat{\mathbb{Z}}\) both maps from \(\mathbb{Q}\) and \(\widehat{\mathbb{Z}}\) are inclusions.
LemmaQHat.injective_rat#
The ring homomorphism \(\mathbb{Q}\to\widehat{\mathbb{Q}}\) sending \(q\) to \(q\otimes_t 1\) is injective.
Proof
We have seen that the map from \(\mathbb{Z}\) to \(\widehat{\mathbb{Z}}\) is injective. Now \(\mathbb{Q}\) is a flat \(\mathbb{Z}\)-module, because it's torsion-free, so tensoring up we deduce that the map from \(\mathbb{Q}=\mathbb{Q}\otimes\mathbb{Z}\) to \(\widehat{\mathbb{Q}}=\mathbb{Q}\otimes\widehat{\mathbb{Z}}\) is also injective. There is no doubt a more elementary proof of this fact.
Lean
Formalized as QHat.injective_rat.
Sources
Uses 2
LemmaQHat.injective_zHat#
The ring homomorphism \(\widehat{\mathbb{Z}}\to\widehat{\mathbb{Q}}\) sending \(z\) to \(1\otimes_t z\) is injective.
Proof
The map from \(\mathbb{Z}\) to \(\mathbb{Q}\) is injective, and we have seen that \(\widehat{\mathbb{Z}}\) is a torsion-free and thus flat \(\mathbb{Z}\)-module, so the map from \(\widehat{\mathbb{Z}}\) to \(\widehat{\mathbb{Q}}\) is also injective.
Lean
Formalized as QHat.injective_zHat.
Sources
Uses 2
We can thus identify \(\mathbb{Q}=\mathbb{Q}\otimes\mathbb{Z}\) and \(\widehat{\mathbb{Z}}=\mathbb{Z}\otimes\widehat{\mathbb{Z}}\) with subrings of \(\widehat{\mathbb{Q}}=\mathbb{Q}\otimes\widehat{\mathbb{Z}}\). Note that, being commutative rings, \(\mathbb{Q}\) and \(\widehat{\mathbb{Z}}\) both contain a copy of \(\mathbb{Z}\) as a subring, and the corresponding copies of \(\mathbb{Z}\) in \(\widehat{\mathbb{Q}}\) are equal; this is because \(1\otimes a=a\otimes 1\) for all \(a\in\mathbb{Z}\).
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.