Zulip Chat Archive

Stream: maths

Topic: Grading the `tensor_algebra`


view this post on Zulip Eric Wieser (Sep 28 2020 at 18:11):

I'm trying to put a grading on the tensor algebra,

def grades : (tensor_algebra R M) →ₗ[R] ( →₀ tensor_algebra R M) :=  sorry

by lifting the trivial map finsupp.single 1. To do this, I need to define an appropriate algebra structure on some copy of ℕ →₀ tensor_algebra R M

I'm immediately running into trouble defining the one of this algebra structure,

def one :  →₀ tensor_algebra R M := {
  support := {0},
  to_fun := λ n, if n = 0 then 1 else 0,
  mem_support_to_fun := λ k, begin
    rw finset.mem_singleton,
    split_ifs; simp [h],
    sorry -- ⊢ (1 : tensor_algebra R M) ≠ 0
  end
}

I suspect I can't prove1 ≠ 0, since the base ring of the algebra may also not have that property.

Is there a typeclass I can include to assume that my ring is not the zero ring?

view this post on Zulip Reid Barton (Sep 28 2020 at 18:23):

This looks too low-level--isn't there finsupp.single or something?

view this post on Zulip Reid Barton (Sep 28 2020 at 18:24):

wait, you even mentioned it in your question... so I'm confused

view this post on Zulip Eric Wieser (Sep 28 2020 at 18:25):

You're quite right, I'm being dumb here

view this post on Zulip Eric Wieser (Sep 28 2020 at 18:26):

one := finsupp.single 0 1

view this post on Zulip Eric Wieser (Sep 28 2020 at 19:26):

Although that needs noncomputable, but I can deal with that for now.

view this post on Zulip Eric Wieser (Sep 28 2020 at 19:26):

Will try and bash out a proof for mul tomorrow,

noncomputable def mul (a b :  →₀ tensor_algebra R M) :  →₀ tensor_algebra R M := {
  support := a.support + b.support,
  to_fun := λ n,  i in (a.support.product b.support), if i.1 + i.2 = n then a i.1 * b i.2 else 0,
  mem_support_to_fun := sorry}

view this post on Zulip Reid Barton (Sep 28 2020 at 19:27):

By the way, is this notion of graded object used in mathlib somewhere?

view this post on Zulip Eric Wieser (Sep 28 2020 at 19:33):

I don't see it yet - there was a thread a while back about CDGA, but that was more of a dfinsupp api

view this post on Zulip Adam Topaz (Sep 28 2020 at 19:34):

If you're already planning to do this, maybe you should grade the free algebra that @Scott Morrison recently introduced? the grading on the tensor algebra is induced from that.

view this post on Zulip Eric Wieser (Sep 28 2020 at 19:43):

I suspect that what I write will work on either anyway

view this post on Zulip Eric Wieser (Sep 28 2020 at 19:44):

All of my pain right now is being caused by finsupp

view this post on Zulip Adam Topaz (Sep 28 2020 at 20:20):

I think it will be slightly easier to define the grading on the free algebra. Of course, one will have to prove some linearity statement in order to descend the grading to the tensor algebra.

view this post on Zulip Eric Wieser (Sep 28 2020 at 20:21):

Here's what I'm stuck on right now:

example {α β : Type*} [add_comm_monoid β] (s : finset α) (f : α  β) (h :  x in s, f x  0) :  x  s, f x  0 := begin
  simp,
end

view this post on Zulip Eric Wieser (Sep 28 2020 at 20:21):

If the sum is nonzero, then there exists a nonzero element

view this post on Zulip Mario Carneiro (Sep 28 2020 at 20:23):

by contrapositive

view this post on Zulip Eric Wieser (Sep 28 2020 at 20:25):

contrapose h, I assume you mean

view this post on Zulip Eric Wieser (Sep 28 2020 at 20:25):

I knew that existed, and could not find the spelling

view this post on Zulip Mario Carneiro (Sep 28 2020 at 20:25):

I mean you should prove it by contraposition

view this post on Zulip Eric Wieser (Sep 29 2020 at 06:15):

Turns out I was looking for docs#add_monoid_algebra

view this post on Zulip Eric Wieser (Sep 29 2020 at 14:41):

Adam Topaz said:

If you're already planning to do this, maybe you should grade the free algebra that Scott Morrison recently introduced? the grading on the tensor algebra is induced from that.

Went ahead and did as you suggested, primarily because it reduced my build time. Progress so far is #4321, but I think I'm missing a trick somewhere.

view this post on Zulip Adam Topaz (Sep 29 2020 at 14:48):

@Eric Wieser I'm confused.... what is add_monoid_algebra? Is it just the usual monoid algebra?

view this post on Zulip Adam Topaz (Sep 29 2020 at 14:53):

If so, why should an algebra AA ever be isomorphic to A[N]A[\mathbf{N}]?

view this post on Zulip Eric Wieser (Sep 29 2020 at 14:57):

add_monoid_algebra seems to have all the properties that I'd associate with grading; namely elementwise addition and convolutional multiplication. I think I see your point though - clearly the mapping from AA to A[N]A[N] is injective and not bijective

view this post on Zulip Eric Wieser (Sep 29 2020 at 14:57):

(also it turns out I don't know how to typeset math here after all...)

view this post on Zulip Adam Topaz (Sep 29 2020 at 14:57):

Use double $

view this post on Zulip Eric Wieser (Sep 29 2020 at 15:00):

Elaborating on my last point - add_monoid_algebra behaves exactly as I want for splitting an element of tensor_algebra into grades through lift - but the part of I that I actually care about is a subalgebra of it.

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:14):

Isn't the map you defined from free_algebra R X to add_monoid_algebra (free_algebra R X) N just the "obvious" inclusion from free_algebra R X to the monoid algebra? This would not give the right answer, even if you consider the image of this embedding (since the image is concentrated in degree 0).

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:15):

Oh nevermind, it's okay since you're lifting the map from XX which sends elements to elements of degree 11.

view this post on Zulip Eric Wieser (Sep 29 2020 at 15:15):

My understanding is that it's the mapping that turns vectors into the single 1 v elements, and products and sums into the appropriate elements. eg v * w goes to single 2 (v * w) thanks to the convolution product

view this post on Zulip Eric Wieser (Sep 29 2020 at 15:15):

Yeah

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:15):

So yeah, the grading is given by the image of this map.

view this post on Zulip Eric Wieser (Sep 29 2020 at 15:16):

I'm tempted to use algebra.adjoin R {f | ∃ (x : X), f = @grading_fun R X _ x } to restrict the output type to exactly that image

view this post on Zulip Eric Wieser (Sep 29 2020 at 15:16):

Although I suspect I'll end up with some awkward proofs...

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:16):

I think it would be easier to just take the image of this map.

view this post on Zulip Eric Wieser (Sep 29 2020 at 15:20):

And just avoid defining the equivalence?

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:27):

Hmmmm..... I think it's a bit more complicated....

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:27):

You really want to represent elements of free_algebra R X as sums of products of elements of X with coefficients in R and not something random in free_algebra R X.

view this post on Zulip Reid Barton (Sep 29 2020 at 15:43):

I don't follow. What's this about an isomorphism/image?
If AA is an RR-algebra, then we can specify a N\mathbb{N}-indexed grading on AA by giving an RR-algebra map AA[N]A \to A[\mathbb{N}] (more commonly written as, say, A[T]A[T]).

view this post on Zulip Reid Barton (Sep 29 2020 at 15:45):

Which I think is what you did, but then more things are happening after that which I don't understand.

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:47):

What's the graded degree nn piece?

view this post on Zulip Reid Barton (Sep 29 2020 at 15:47):

All those aa that get sent to aTna T^n

view this post on Zulip Reid Barton (Sep 29 2020 at 15:49):

Do I need some further conditions? Really it's supposed to be a comodule for the coalgebra R[T]R[T], Δ(T)=TT\Delta(T) = T \otimes T.

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:49):

No, I think you're right.
I was just worried about the fact that we want the graded parts to be R-modules, but this follows since Ris central.

view this post on Zulip Reid Barton (Sep 29 2020 at 15:49):

But I'm under the impression that it's automatic somehow.

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:51):

I mean in this case there really is some isomorphism with an obviously graded object.

view this post on Zulip Eric Wieser (Sep 29 2020 at 15:52):

but then more things are happening after that which I don't understand.

I wanted to define a mapping to take me back in the other direction, and I was foolish enough to miss that lift R $ grading_fun is not injective. So the question is, do we either:

  • Just stick with the injective mapping, T →ₐ (ℕ →₀ T) (where in the PR (ℕ →₀ T) is substituted with add_monoid_algebra which has the nice bonus of having a compatible multiplication)
  • Insist on an isomorphism T ≃ₐ grades_of T, and invent a new type for the destination algebra

I started off down the second path, but needed @Adam Topaz to point out the part after the comma

view this post on Zulip Reid Barton (Sep 29 2020 at 15:54):

OK, now that I think about it more it does seem like you need the comodule properties.

view this post on Zulip Reid Barton (Sep 29 2020 at 15:54):

There is a map back (which corresponds to setting T=1T = 1) but it's not an isomorphism.

view this post on Zulip Reid Barton (Sep 29 2020 at 15:55):

But one of the compositions is the identity: if you apply the grading map and then the "forget grading" map you get back what you started with

view this post on Zulip Eric Wieser (Sep 29 2020 at 15:56):

Right, so maybe I cut back that PR to:

  • Define the forward map T →ₐ add_monoid_algebra T ℕ
  • Define the reverse map add_monoid_algebra T ℕ →ₐ T
  • Show that rev (fwd x) = x
  • Remove the attempt to show fwd (rev y) = y, because it doesn't

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:57):

But rev (fwd x) = x

view this post on Zulip Eric Wieser (Sep 29 2020 at 15:58):

Yes, that's my third bullet point and I managed to prove that already in the PR

view this post on Zulip Reid Barton (Sep 29 2020 at 16:00):

There's another property of fwd that I think says that if you look at the degree n part of fwd of anything, then its coefficient again gets sent to itself in degree n

view this post on Zulip Eric Wieser (Sep 29 2020 at 16:00):

Any naming suggestions for the first two bullets?

  • fwd: grades_of, grades, grade, grading, ...
  • rev: from_grades, of_grades, ungrade, ...

view this post on Zulip Reid Barton (Sep 29 2020 at 16:01):

The rev map doesn't depend on the grading

view this post on Zulip Reid Barton (Sep 29 2020 at 16:01):

Also, it would be good to have a version of this story for modules too. But I don't think we have "add_monoid_module", do we?

view this post on Zulip Adam Topaz (Sep 29 2020 at 16:02):

It's the direct sum isn't it?

view this post on Zulip Eric Wieser (Sep 29 2020 at 16:02):

add_monoid_module is just finsupp - indeed, it's built upon finsupp and adds the multiplication on top.

view this post on Zulip Eric Wieser (Sep 29 2020 at 16:02):

direct sum is dfinsupp, which is likely more trouble than it's worth here (I have an old implementation of grading via dfinsupp)

view this post on Zulip Reid Barton (Sep 29 2020 at 16:05):

I was going to say it needs the structure of a module over the monoid (in this case multiplicative nat I guess) but actually it doesn't seem to be needed for this story. It does need the RR-module structure but I guess that one already exists.

view this post on Zulip Eric Wieser (Sep 29 2020 at 16:06):

Reid Barton said:

The rev map doesn't depend on the grading

I suppose the rev map (grading_inv in the PR) could be part of the add_monoid_algebra API, but that makes naming it harder. sum_id perhaps?

view this post on Zulip Reid Barton (Sep 29 2020 at 16:06):

Eventually it should be a module over the add_monoid_algebra though.

view this post on Zulip Eric Wieser (Sep 29 2020 at 16:07):

Mind editing your its in the above messages to clarify what they refer to?

view this post on Zulip Reid Barton (Sep 29 2020 at 16:07):

They refer to a hypothethical add_monoid_module

view this post on Zulip Eric Wieser (Sep 29 2020 at 16:08):

Why would the add_monoid_module be a module over the add_monoid_algebra instead of over the monoid, when algebras are already modules?

view this post on Zulip Reid Barton (Sep 29 2020 at 16:09):

Like if MM is an RR-module then "M[T]M[T]" is an R[T]R[T]-module and in particular both an RR-module and a module over {1,T,T2,}\{1, T, T^2, \ldots\} = multiplicative nat.

view this post on Zulip Reid Barton (Sep 29 2020 at 16:11):

M[T]M[T] would be the add_monoid_module. And then a graded RR-module is an RR-module MM together with an RR-module map MM[T]M \to M[T] such that blah blah blah.

view this post on Zulip Reid Barton (Sep 29 2020 at 16:14):

I don't know if this is the best way to handle graded algebras/modules. But it's a nice point of view that comes up in algebraic geometry/homotopy theory. That's why I was wondering earlier whether mathlib was already doing this.

view this post on Zulip Reid Barton (Sep 29 2020 at 16:15):

It seems to at least have some advantages, for instance, the way the grading interacts with + and * is encoded neatly in saying that the grading map is an algebra homomorphism.

view this post on Zulip Eric Wieser (Sep 29 2020 at 16:51):

Eric Wieser said:

Right, so maybe I cut back that PR to: <snip>

I've gone ahead and done this, #1234 ought to now pass CI.


Last updated: May 10 2021 at 08:14 UTC