Stream: maths

Topic: tensor algebras and a construction

Kevin Buzzard (Oct 29 2020 at 15:32):

There are two ways to build free groups that I know about. One involves basically writing down the proof of the adjoint functor theorem; one takes a huge product of groups and finds the free group as a subset. This way the universal property is easy, but proving that every element has a unique normal form of the form $x_1^{\pm1}x_2^{\pm1}\cdots x_n^{\pm1}$ with no two consecutive $x_i$ distinct is a pain; the other way involves defining a term of the free group to be a reduced word, and now proving things like associativity is where the work is.

Seems to me that the same might be true for tensor algebras. Let $R$ be a commutative ring (or non-commutative semiring -- I have no idea what generality stuff works in but I only care about commutative rings at this point) and let $M$ be an $R$-module. It seems to me that the tensor algebra $R[M]$ of $M$ is what you get if you evaluate the adjoint of the forgetful functor from (not necessarily commutative) $R$-algebras to $R$-modules, at $M$. That's one way of looking at it, and I wonder whether this is somehow closely related to the definition we have right now in mathlib of $R[M]$ as a quotient of the non-commutative multivariable polynomial algebra over $R$ on the type $M$. Perhaps the analogue of the "concrete" construction is that we can define $M^{\otimes i}$ to be $M\otimes_R M\otimes_R\cdots\otimes_R M$ $i$ times, and let $R[M]$ be the direct sum of the $M^{\otimes i}$ for $i\in\mathbb{N}$.

@Amelia Livingston is doing an MSc project with me on some homological algebra (Koszul complexes) and I am pretty sure she'll need this second description. She's made $M^{\otimes i}$ and has a map to the tensor algebra as defined in mathlib, but to get any further my instinct is that she should now make $\oplus_{i\in\mathbb{N}}M^{\otimes i}$ as an $R$-module (not hard), and then as an $R$-algebra (we'll get to this) and then define maps both ways between this and the tensor algebra as defined in mathlib and check that they are inverse ring isomorphisms.

When thinking about how to make the direct sum into a ring, it seemed that this was probably a special case of a more general construction. where one starts with an add_monoid $I$, and $R$-modules $M(i)$ for each $i\in I$, equipped with $R$-bilinear maps $M(i)\times M(j)\to M(i+j)$ satisfying some axioms (we'll get to this), and then prove that (a) this gives $M(0)$ a ring structure, (b) this gives $\oplus_iM(i)$ an $M(0)$-algebra structure and (c) hence the direct sum is an $R$-algebra (I'm happy to assume that $M(0)$ is commutative if necessary). Does this construction have a name?

Once one has this, one can apply with $I=\mathbb{N}$ and $M(i)=M^{\otimes i}$ and then hopefully prove the ring_equiv with tensor_algebra R M by writing down maps in both directions.

But there's a catch -- the "associativity" axioms are not well-typed if stated naively, because they assert the equality of an element of $M((i+j)+k)$ and $M(i+(j+k))$ -- the usual problem. Is there some cunning way to sigma-type my way out of this? I don't think I've ever fully internalised this trick which @Mario Carneiro can use to avoid problems. @Kenny Lau do you understand this now? One is trying to put a ring structure on a direct sum and one will have to prove something of the form "if associativity holds for the factors, then it holds for the direct sum" and if associativity is hard to use then this might be hard to prove.

I guess @Eric Wieser has been wrestling with these sorts of questions, but having just spent some time talking to Amelia about them I am now beginning to understand them better myself. Do people think that making this second "explicit" construction of a tensor algebra is a useful thing to do? Amelia needs that the map from $M^{\otimes i}$ to $R[M]$ is injective, and this seemed to me to be a nightmare from just the definition we currently have as a quotient of a non-commutative polynomial ring.

Mario Carneiro (Oct 29 2020 at 15:40):

As @Reid Barton observed in the CDGA thread, the sigma-type trick is inferior to the approach using a more algebra-respecting sum type, in this case $\oplus_iM(i)$. Since you are already apparently working with this type it seems best to use it here

Mario Carneiro (Oct 29 2020 at 15:41):

Basically, in order to state associativity, you construct the elements of $M((i+j)+k)$ and $M(i+(j+k))$, inject them both into $\oplus_iM(i)$ and then assert equality there

Mario Carneiro (Oct 29 2020 at 15:42):

Depending on how things work out you may also want to have the R-bilinear maps instead be components of one map $\oplus_iM(i)\times \oplus_iM(i)\to \oplus_iM(i)$

Mario Carneiro (Oct 29 2020 at 15:45):

In fact, with these modifications it may even be possible to abstract from the concrete representation $\oplus_iM(i)$ to another type $N$ equipped with appropriate structure relating it to the $M(i)$

Eric Wieser (Oct 29 2020 at 15:47):

Where "asserting equality there" is dfinsupp.single ((i + j) + k) x = dfinsupp.single (i + (j + k)) y, right?

Kevin Buzzard (Oct 29 2020 at 15:49):

Yes exactly. What I'm trying to do is to work around == !

Mario Carneiro (Oct 29 2020 at 15:49):

I hope it has a better name than dfinsupp.single though

Kevin Buzzard (Oct 29 2020 at 15:49):

yes I didn't plan on breaking the abstraction barrier!

Mario Carneiro (Oct 29 2020 at 15:50):

it's called direct_sum.of

Right

Eric Wieser (Oct 29 2020 at 15:59):

I think what you're trying to do here is likely a better-generalized version of #4812

Kevin Buzzard (Oct 29 2020 at 16:00):

I haven't looked at this PR yet, but I did look at #4321

Eric Wieser (Oct 29 2020 at 16:00):

I'd probably not look at the new one again until I pull in Kenny's feedback

Kevin Buzzard (Oct 29 2020 at 16:00):

I know from personal experience on the CDGA thread that this stuff can get really hairy really quickly.

Eric Wieser (Oct 30 2020 at 15:11):

Mario Carneiro said:

Depending on how things work out you may also want to have the R-bilinear maps instead be components of one map $\oplus_iM(i)\times \oplus_iM(i)\to \oplus_iM(i)$

Can you expand on this? Are you suggesting a definition like

/- lift an element-wise multiplication to a multiplication on the direct_sum -/
def lift_mul (dmul : Π i j k, β i → β j → β k) : (⨁ i, β i) → (⨁ i, β i) → (⨁ i, β i) := sorry


Perhaps there could be a has_dmul typeclass to generate has_mul (⨁ i, β i) from has_dmul β

Eric Wieser (Oct 30 2020 at 15:19):

Ah, that doesn't work , k needs to be finitely supported to define that. So

def lift_mul (dmul : Π i, β i → Π j, β j → Π₀ k, β k) : (⨁ i, β i) → (⨁ i, β i) → (⨁ i, β i) := sorry


or

def lift_mul (dmul : Π i, β i → Π j, β j → ⨁ k, β k) : (⨁ i, β i) → (⨁ i, β i) → (⨁ i, β i) := sorry


Mario Carneiro (Oct 30 2020 at 18:04):

@Eric Wieser No, I mean lifting it already at the mathematical level, and only axiomatizing lift_mul instead of dmul

Mario Carneiro (Oct 30 2020 at 18:07):

The first version is not correct because k is an output, not an input. It is more accurately Π i j, β i → β j → β (i + j), or Π i j, β i → β j → Σ k, β k if you want to be more abstract

Last updated: May 12 2021 at 07:17 UTC