# Zulip Chat Archive

## Stream: maths

### Topic: finite presentation of element of a tensor product

#### Kevin Buzzard (Feb 26 2021 at 01:38):

If $R$ is a commutative ring and $M$ and $N$ are $R$-modules, then it's a standard fact that every element of $M\otimes_RN$ can be written as a finite sum of things of the form $m_i\otimes n_i$. I was merrily on my way proving this by induction, and in the addition case I have to prove that if $x$ and $y$ are a finite sum of $m_i\otimes n_i$ then so is $x+y$. The annoying thing is that these two finite subsets of $M\times N$ might overlap and in this case I have to replace $m\otimes n$ with $2m\otimes n$. This is certainly possible but it's a bit of a kerfuffle. Am I missing a trick? Please don't make me use multisets. Do we even have multiset.sum? Maybe I shouldn't be using `finsum_in`

? My problem is that I want a finite index set mapping to $M\times N$ and then to $M\otimes_R N$, (because then I could just take the disjoint union of the index sets) but this looks to me to be a bit too general for the finset.sum set-up because $M\times N$ isn't an add_comm_monoid.

#### Thomas Browning (Feb 26 2021 at 01:42):

Is there also a further problem that $2m \otimes n$ might conflict with an existing summand?

#### Adam Topaz (Feb 26 2021 at 03:06):

```
import linear_algebra.tensor_product
open_locale tensor_product
variables {A M N : Type*} [comm_ring A] [add_comm_group M] [add_comm_group N] [module A M] [module A N]
theorem foo {α : M ⊗[A] N} : ∃ L : list (M × N),
α = (L.map $ λ t : M × N, tensor_product.tmul A t.1 t.2).sum :=
begin
apply tensor_product.induction_on α,
{ refine ⟨[], by simp⟩ },
{ intros x y,
refine ⟨[(x,y)], by simp⟩ },
{ rintros x y ⟨L1,hL1⟩ ⟨L2,hL2⟩,
refine ⟨L1 ++ L2, _⟩,
simp [hL1, hL2] }
end
```

#### Adam Topaz (Feb 26 2021 at 03:06):

Some glue is needed if you absolutely need a statement involving `finset`

s.

#### Johan Commelin (Feb 26 2021 at 06:05):

Can't you just coerce the list to a finset afterwards?

#### Scott Morrison (Feb 26 2021 at 06:14):

But this would throw out multiplicities.

#### Johan Commelin (Feb 26 2021 at 06:38):

ooh right... I now understand what kind of clue is needed (-;

#### Damiano Testa (Feb 26 2021 at 07:15):

I do not know a good answer to this, but I would be very interested in knowing how to do this!

I faced similar issues when working with polynomials: sometimes, I want the polynomial ring to be an "inductive ring" that has a constructor for each element of the ring and a new one, called `X`

. This would be *much* closer to how I think about polynomials.

In the case of polynomials, I added an extra layer of an induction on the `finset`

for one of them, reducing to the case of a single element, and then going by cases on whether the single elements is or is not in the support of the other. It was very annoying, but in the end it worked. I feel that there should be a better solution for this, that would solve at once also the issue with tensor products!

#### Johan Commelin (Feb 26 2021 at 07:17):

The list can be coerced to a multiset. An there is an equiv between `multiset X`

and `finsupp X nat`

. That finsupp will give you a `finset`

+ function that record the multiplicities.

#### Johan Commelin (Feb 26 2021 at 07:19):

@Damiano Testa your way of thinking about polynomials is what `polynomial.induction_on`

would give you, right?

#### Damiano Testa (Feb 26 2021 at 07:20):

It is related, but it does not work so well when there are two polynomials that you want to sum, since the pieces for one do not match with the pieces for the other, I think. At least, I thought that it would not work so smoothly...

#### Damiano Testa (Feb 26 2021 at 07:22):

Ultimately, (in the polynomial case) I have a feeling that these issues arise since you strive to write a polynomial as a linear combination of *distinct* monomials, instead of simply monomials. The issue with tensor products seems similar: you want to say that

`x \otimes y + x \otimes y + 2x \otimes y`

is an element of the tensor product since it is a combination of tensors and not worry about the fact that the "supports" overlap, possibly after summing.

#### Kevin Buzzard (Feb 26 2021 at 08:33):

Thanks for all the comments!

I posted this then went straight to bed, and this morning when I woke up my mind went straight back to it and instantly realised th at I could also formalise it as "there exists a fintype I equipped with a map to M x N such that the induced map to M tensor N has fintype.sum ... . I can then just use disjoint unions on the I's. Maybe Damiano this trick helps for you. But I like the solution with list.sum as well, I was worried about being forced into some exotic sum for which there was no API but this seems to work fine! Thanks Adam!

#### Kevin Buzzard (Feb 26 2021 at 08:35):

As Thomas points out, it's not even immediately true that the result is true for finsets, but I don't need it, I was only talking about finsets so I could use finset.sum

#### Kevin Buzzard (Feb 26 2021 at 09:19):

Here is the reason this came up -- it was in the context of Picard groups of schemes. If $S$ is a scheme then we could, perhaps unadvisedly, define the Picard monoid of $S$ as the isomorphism classes of sheaves of $\mathcal{O}_X$-modules of $S$ under tensor product, and then define the Picard group of $S$ as the units in this monoid. This reason this is a bit weird is that we dip our toes into set-theoretic issues here -- the Picard group of $S$ is in the same universe as $S$, but the Picard monoid is not (at least for non-empty $S$). Example: if $S$ is Spec(K) for `K : Type`

a field then the sheaves are just the $K$-vector spaces, the theory of bases tells us that the Picard monoid is hence the monoid of cardinals (thus in `Type 1`

) but the only solution to $X\times Y=1$ in cardinals is $X=Y=1$ so the Picard group is trivial, and hence can be demoted back to `Type`

.

One way of getting around this nonsense is to define the Picard monoid to be the isomorphism classes of sheaves with some finiteness condition (I guess coherent sheaves would be fine in the Noetherian case and perhaps maybe in general -- I know Grothendieck set up some some theory of coherent sheaves on an arbitrary scheme in EGA and that Hartshorne does not use G's definition in his book, he uses a simpler f.g. definition which is equivalent in the Noetherian case but not in general). This more refined definition of the Picard monoid doesn't suffer from any universe issues, so one definitely gets a Picard group which doesn't suffer from set-theoretic issues, but to make sure that one gets the same Picard group one now has to check that every invertible sheaf is coherent.

Here is the proof of this I came up with (of course I could look in the books, but where's the fun in that?): Say $$\mathcal{F}$ is an arbitrary sheaf of $\mathcal{O}_X$-modules, with inverse $\mathcal{F}^{-1}$. Work over an affine, so everything is really a module over a ring. Write $1\in\mathcal{O}_X=\mathcal{F}\otimes\mathcal{F}^{-1}$ as $\sum_i f_i\otimes g_i$, a finite sum, as above. I claim that $\mathcal{F}$ is generated by the $f_i$. Indeed, for an arbitrary section $m\in\mathcal{F}=\mathcal{F}\otimes\mathcal{F}^{-1}\otimes\mathcal{F}$ we have $m=m\otimes1=\sum_i m\otimes (g_i\otimes f_i)=\sum_i (m\otimes g_i)f_i=\sum_i r_if_i$ where $r_i=m\otimes g_i\in\mathcal{F}\times\mathcal{F}^{-1}=\mathcal{O}_X$.

What I especially like about this proof is that it looks like the kind of thing you could get away with on the board, especially if you mumble about all the identifications being canonical, but ultimately it relies on the canonical isomorphism $M=M\otimes_RR=M\otimes_R(N\otimes_R M)=(M\otimes_R N)\otimes_R M=R\otimes_R M=M$ being the identity map, an assertion which I am not entirely sure how to convince Lean about :-) I started to formalise the proof in the hope that it might bring some clarity to the situation, but if a passing algebraic geometer wants to bring some clarity too then that would be great :-) Is every invertible sheaf on a scheme coherent?

#### Scott Morrison (Feb 26 2021 at 11:13):

```
begin
...
work_over_an_affine,
...
end
```

#### Kevin Buzzard (Feb 26 2021 at 11:42):

You mean `wlog : is_affine S`

of course.

#### Kevin Buzzard (Feb 26 2021 at 11:42):

That would be a pretty neat `wlog`

extension :D

#### Damiano Testa (Feb 26 2021 at 12:09):

Kevin, your proof of finite generation is the proof that I have in mind to show that affine schemes are quasi-compact: refine an "open cover" by an "open cover by standard affines", then use that you obtain an identity for 1 as a combination of finitely many fractions and conclude!

It is the algebraic counterpart to partitions of unity.

#### Kevin Buzzard (Feb 26 2021 at 12:38):

Yes, and it has the added advantage that it works. I am not entirely sure that my map from M to M is the identity...

#### Kevin Buzzard (Feb 26 2021 at 12:45):

I think I can fix my proof by starting with m on the right hand side, pushing it along this unspecified isomorphism to get i(m) on the left hand side and then come back again with the argument above applied to i(m)

Last updated: May 06 2021 at 18:20 UTC