Grading the `tensor_algebra`

Stream: maths

[Eric Wieser]

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]

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

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

one := finsupp.single 0 1

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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]

I suspect that what I write will work on either anyway

[Eric Wieser]

All of my pain right now is being caused by finsupp

[Adam Topaz]

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]

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]

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

[Mario Carneiro]

by contrapositive

[Eric Wieser]

contrapose h, I assume you mean

[Eric Wieser]

I knew that existed, and could not find the spelling

[Mario Carneiro]

I mean you should prove it by contraposition

[Eric Wieser]

Turns out I was looking for docs#add_monoid_algebra

[Eric Wieser]

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]

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

[Adam Topaz]

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

[Eric Wieser]

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 $A$ to $A[N]$ is injective and not bijective

[Eric Wieser]

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

[Adam Topaz]

Use double $

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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]

Yeah

[Adam Topaz]

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

[Eric Wieser]

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]

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

[Adam Topaz]

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

[Eric Wieser]

And just avoid defining the equivalence?

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Reid Barton]

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

[Adam Topaz]

What's the graded degree $n$ piece?

[Reid Barton]

All those $a$ that get sent to $a T^n$

[Reid Barton]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Eric Wieser]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

But rev (fwd x) = x

[Eric Wieser]

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

[Reid Barton]

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]

Any naming suggestions for the first two bullets?

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

[Reid Barton]

The rev map doesn't depend on the grading

[Reid Barton]

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]

It's the direct sum isn't it?

[Eric Wieser]

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

[Eric Wieser]

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]

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 $R$-module structure but I guess that one already exists.

[Eric Wieser]

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]

Eventually it should be a module over the add_monoid_algebra though.

[Eric Wieser]

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

[Reid Barton]

They refer to a hypothethical add_monoid_module

[Eric Wieser]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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.