finite presentation of element of a tensor product

Stream: maths

[Kevin Buzzard]

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]

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

[Adam Topaz]

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]

Some glue is needed if you absolutely need a statement involving finsets.

[Johan Commelin]

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

[Scott Morrison]

But this would throw out multiplicities.

[Johan Commelin]

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

[Damiano Testa]

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]

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]

@Damiano Testa your way of thinking about polynomials is what polynomial.induction_on would give you, right?

[Damiano Testa]

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]

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]

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]

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]

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]

begin
  ...
  work_over_an_affine,
  ...
end

[Kevin Buzzard]

You mean wlog : is_affine S of course.

[Kevin Buzzard]

That would be a pretty neat wlog extension :D

[Damiano Testa]

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]

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]

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)