Zulip Chat Archive

Stream: maths

Topic: tensor algebras and a construction


view this post on Zulip 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 x1±1x2±1xn±1x_1^{\pm1}x_2^{\pm1}\cdots x_n^{\pm1} with no two consecutive xix_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 RR 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 MM be an RR-module. It seems to me that the tensor algebra R[M]R[M] of MM is what you get if you evaluate the adjoint of the forgetful functor from (not necessarily commutative) RR-algebras to RR-modules, at MM. 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]R[M] as a quotient of the non-commutative multivariable polynomial algebra over RR on the type MM. Perhaps the analogue of the "concrete" construction is that we can define MiM^{\otimes i} to be MRMRRMM\otimes_R M\otimes_R\cdots\otimes_R M ii times, and let R[M]R[M] be the direct sum of the MiM^{\otimes i} for iNi\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 MiM^{\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 iNMi\oplus_{i\in\mathbb{N}}M^{\otimes i} as an RR-module (not hard), and then as an RR-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 II, and RR-modules M(i)M(i) for each iIi\in I, equipped with RR-bilinear maps M(i)×M(j)M(i+j)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)M(0) a ring structure, (b) this gives iM(i)\oplus_iM(i) an M(0)M(0)-algebra structure and (c) hence the direct sum is an RR-algebra (I'm happy to assume that M(0)M(0) is commutative if necessary). Does this construction have a name?

Once one has this, one can apply with I=NI=\mathbb{N} and M(i)=MiM(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)M((i+j)+k) and M(i+(j+k))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 MiM^{\otimes i} to R[M]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.

view this post on Zulip 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 iM(i)\oplus_iM(i). Since you are already apparently working with this type it seems best to use it here

view this post on Zulip Mario Carneiro (Oct 29 2020 at 15:41):

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

view this post on Zulip 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 iM(i)×iM(i)iM(i)\oplus_iM(i)\times \oplus_iM(i)\to \oplus_iM(i)

view this post on Zulip Mario Carneiro (Oct 29 2020 at 15:45):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Oct 29 2020 at 15:49):

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

view this post on Zulip Mario Carneiro (Oct 29 2020 at 15:49):

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

view this post on Zulip Kevin Buzzard (Oct 29 2020 at 15:49):

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

view this post on Zulip Mario Carneiro (Oct 29 2020 at 15:50):

it's called direct_sum.of

view this post on Zulip Kevin Buzzard (Oct 29 2020 at 15:50):

Right

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 29 2020 at 16:00):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 iM(i)×iM(i)iM(i)\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 β

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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