tensor algebras and a construction

Stream: maths

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

it's called direct_sum.of

[Kevin Buzzard]

Right

[Eric Wieser]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Kevin Buzzard]

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

[Eric Wieser]

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]

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]

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

[Mario Carneiro]

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