Zulip Chat Archive

Stream: maths

Topic: Grading the `tensor_algebra`


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?

Reid Barton (Sep 28 2020 at 18:23):

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

Reid Barton (Sep 28 2020 at 18:24):

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

Eric Wieser (Sep 28 2020 at 18:25):

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

Eric Wieser (Sep 28 2020 at 18:26):

one := finsupp.single 0 1

Eric Wieser (Sep 28 2020 at 19:26):

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

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}

Reid Barton (Sep 28 2020 at 19:27):

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

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

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.

Eric Wieser (Sep 28 2020 at 19:43):

I suspect that what I write will work on either anyway

Eric Wieser (Sep 28 2020 at 19:44):

All of my pain right now is being caused by finsupp

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.

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

Eric Wieser (Sep 28 2020 at 20:21):

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

Mario Carneiro (Sep 28 2020 at 20:23):

by contrapositive

Eric Wieser (Sep 28 2020 at 20:25):

contrapose h, I assume you mean

Eric Wieser (Sep 28 2020 at 20:25):

I knew that existed, and could not find the spelling

Mario Carneiro (Sep 28 2020 at 20:25):

I mean you should prove it by contraposition

Eric Wieser (Sep 29 2020 at 06:15):

Turns out I was looking for docs#add_monoid_algebra

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.

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?

Adam Topaz (Sep 29 2020 at 14:53):

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

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

Eric Wieser (Sep 29 2020 at 14:57):

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

Adam Topaz (Sep 29 2020 at 14:57):

Use double $

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.

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).

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.

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

Eric Wieser (Sep 29 2020 at 15:15):

Yeah

Adam Topaz (Sep 29 2020 at 15:15):

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

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

Eric Wieser (Sep 29 2020 at 15:16):

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

Adam Topaz (Sep 29 2020 at 15:16):

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

Eric Wieser (Sep 29 2020 at 15:20):

And just avoid defining the equivalence?

Adam Topaz (Sep 29 2020 at 15:27):

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

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.

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]).

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.

Adam Topaz (Sep 29 2020 at 15:47):

What's the graded degree nn piece?

Reid Barton (Sep 29 2020 at 15:47):

All those aa that get sent to aTna T^n

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.

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.

Reid Barton (Sep 29 2020 at 15:49):

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

Adam Topaz (Sep 29 2020 at 15:51):

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

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

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.

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.

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

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

Adam Topaz (Sep 29 2020 at 15:57):

But rev (fwd x) = x

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

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

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, ...

Reid Barton (Sep 29 2020 at 16:01):

The rev map doesn't depend on the grading

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?

Adam Topaz (Sep 29 2020 at 16:02):

It's the direct sum isn't it?

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.

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)

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.

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?

Reid Barton (Sep 29 2020 at 16:06):

Eventually it should be a module over the add_monoid_algebra though.

Eric Wieser (Sep 29 2020 at 16:07):

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

Reid Barton (Sep 29 2020 at 16:07):

They refer to a hypothethical add_monoid_module

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?

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.

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.

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.

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.

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: Dec 20 2023 at 11:08 UTC