## Stream: maths

### Topic: grading by submonoids maths question

#### Kevin Buzzard (Apr 23 2021 at 17:54):

Let $M$ be an additive monoid. I want to grade stuff by $M$. According to the semiring police I shouldn't be grading a ring by $M$, decomposing it into an internal (possibly infinite) direct sum of add_subgroups indexed by $M$, I should instead be grading a semiring by $M$, decomposing it into an internal direct sum of add_submonoids. Here's the definition we've been working with, out of interest:

/-- If M is an additive monoid, then an M-grading on a ring R is a decomposition of R as
an internal direct sum R = ⨁Rₘ into submonoids indexed by m : M, where the decomposition
respects 1 and *, in the sense that 1 ∈ R₀ and Rₘ*Rₙ ⊆ R_{m+n} -/
structure add_monoid_grading (M : Type*) [add_monoid M] [decidable_eq M] (R : Type*) [semiring R] :=
(graded_piece : M → add_submonoid R)
(direct_sum : direct_sum.add_submonoid_is_internal graded_piece)
(grading_one : (1 : R) ∈ graded_piece 0)
(grading_mul : ∀ (m n : M) (r s : R),
r ∈ graded_piece m → s ∈ graded_piece n → r * s ∈ graded_piece (m + n))


Explanation of direct_sum: I'll write $R_m$ for the add_submonoid graded_piece m of $R$ corresponding to $m\in M$, and direct_sum says that the natural map from the abstract external direct sum $\oplus_{m\in M}R_m$ to $R$ is bijective. The other axioms are that $1\in R_0$ and $R_mR_n\subseteq R_{m+n}$. [This isn't an MWE or anything, this is a maths question and I just posted the Lean code so you can see the axioms we went for. If you want an MWE it's in the Liquid project here)]. Eric and Damiano have shown that this can be made into a working definition of grading: Eric graded the polynomial ring $R[X]$ by $\mathbb{N}$ and Damiano graded the monoid algebra $R[M]$ by $M$, for example.

I've now started to work on my intended application, where $R$ is a commutative ring, and I've realised that I can't see why $R_0$ should be a subring or more precisely an additive subgroup. If $R_0$ contains $-1$ then this is all one needs: multiplication by $-1$ proves that all the $R_m$ are add_subgroups, and conversely if all the $R_m$ are add_subgroups then $-1\in R_0$. It seems to me that there are three ways to proceed:

1) Prove the theorem, if it's true. Question: if I grade a ring (commutative if necessary) by a monoid (commutative if necessary) in the sense of the above Lean definition (i.e. by submonoids), is $-1\in R_0$? Thoughts: by definition $-1=\sum_{m\in I}r_m$, a finite sum, and so $1=\sum_{a,b\in I}r_ar_b$, meaning that if $s_c:=\sum_{a,b\in I, a+b=c}r_ar_b$ then $s_c=0$ for $c\not=0$ and $s_0=1$, but I can't get it from this. One might even more generally ask for an example of a commutative additive group which can be written as a direct sum of submonoids which are not subgroups -- can anyone give an example of this?

2) Give up on the theorem and make a second definition, where I do the thing I always wanted to do and grade a ring by add_subgroups.

3) Just ditch the definition above completely and change the definition to a grading of a ring by add_subgroups, thus meaning for example that we will not be able to grade $R[X]$ by $\mathbb{N}$ if $R$ is a semiring, thus upsetting the semiring theorists who specialise in graded semirings (if any such people exist) but meaning that I can proceed.

@Damiano Testa you raised this earlier, and I think @Eric Wieser said something which made you happy but I'm not sure I'm happy yet.

#### Kevin Buzzard (Apr 23 2021 at 17:58):

Oh I've got it! If R is a ring then adding 1 induces an injection $R_m\to R_m$ and a bijection on $R$, so it must be a bijection on all $R_m$ :D Thanks for listening :D

#### Eric Wieser (Apr 23 2021 at 17:59):

I feel like 2) or 3) might still be the better choice, even if it sounds like the statement needed for 1) is true

#### Kevin Buzzard (Apr 23 2021 at 18:03):

I want to change graded_piece to add_monoid_graded_piece and just add a new add_monoid_grading.graded_piece to be the add_subgroup if R is a ring. Then I think everyone will be happy.

#### Eric Wieser (Apr 23 2021 at 18:06):

I'm imagining the has_coe_to_sort I suggested before that links it to direct_sum being troublesome definitionally for users of subgroups

#### Eric Wieser (Apr 23 2021 at 18:06):

But if that does happen it's easy to fall back to option 2

#### David Wärn (Apr 23 2021 at 18:45):

Generally if you have a direct sum $\bigoplus_m A_m$ of additive monoids and $a \in A_m$, then $a$ has an additive inverse in $\bigoplus_m A_m$ iff it does in $A_m$, since the inclusion into the direct sum has a section. Isn't this enough?

#### Kevin Buzzard (Apr 23 2021 at 19:22):

Yes! Thanks! I was making a meal of it on paper beforehand because I had thought it was a question about rings (see my comments about multiplication by -1, which led me completely the wrong way). When I realised it was a question about groups (which I only did as I was typing it in and it occurred to me that I couldn't make a direct sum of nongroupy monoids into a group) it all became math-easy. I'm currently writing an API for the section, which apparently we don't have in mathlib :-/

def projection (j : ι) : (⨁ i, A i) →+ A j :=
{ to_fun := λ f, f j,
map_zero' := rfl,
map_add' := λ x y, x.add_apply y j }


etc. Thanks!

#### Kevin Buzzard (Apr 23 2021 at 19:24):

I tried to use direct_sum.to_add_monoid for this initially, and ended up in eq.rec hell.

#### Eric Wieser (Apr 23 2021 at 19:25):

That definition looks sensible to me - it's basically the dfinsupp version of docs#add_monoid_hom.apply

#### Eric Wieser (Apr 23 2021 at 19:26):

Isn't that docs#direct_sum.component?

#### Kevin Buzzard (Apr 23 2021 at 19:57):

Aah yes it is for modules, but I have monoids

#### Scott Morrison (Apr 23 2021 at 23:47):

So sad that we need to write def projection (j : ι) : (⨁ i, A i) →+ A j := when we already have def biproduct.π (f : J → C) [has_biproduct f] (b : J) : ⨁ f ⟶ f b := ... in every category with biproducts. :-(

#### Adam Topaz (Apr 23 2021 at 23:49):

I don't think this is a biproduct though...

#### Adam Topaz (Apr 23 2021 at 23:49):

J can be infinite

#### Scott Morrison (Apr 23 2021 at 23:53):

ah, good point. We need categorical direct sums (the image of the comparison map from the coproduct to the product?) I guess.

#### Adam Topaz (Apr 23 2021 at 23:54):

But it's a bit silly as the comparison map is defined in terms of the projections :)

#### Eric Wieser (Apr 26 2021 at 22:39):

What should this family of definitions be called?

import algebra.direct_sum
import linear_algebra.direct_sum_module
import group_theory.submonoid.operations

variables {M : Type*} [decidable_eq ι] [add_comm_monoid M] (Mᵢ : ι → add_submonoid M)

open_locale direct_sum
open direct_sum

/-- The canonical map from a direct sum of add_submonoids to their carrier type-/
def name_me_add_submonoid  {ι M : Type*} [decidable_eq ι] [add_comm_monoid M]
(Mᵢ : ι → add_submonoid M) :
(⨁ i, Mᵢ i) →+ M :=
to_add_monoid $λ i, (Mᵢ i).subtype /-- The canonical map from a direct sum of add_subgroups to their carrier type -/ def name_me_add_subgroup {ι M : Type*} [decidable_eq ι] [add_comm_group M] (Mᵢ : ι → add_subgroup M) : (⨁ i, Mᵢ i) →+ M := to_add_monoid$ λ i, (Mᵢ i).subtype

/-- The canonical map from a direct sum of add_submodules to their carrier type -/
def name_me_submodule {ι R M : Type*} [decidable_eq ι] [semiring R] [add_comm_monoid M] [module R M]
(Mᵢ : ι → submodule M) :
(⨁ i, Mᵢ i)  →ₗ[R] M :=
to_module R ι M $λ i, (Mᵢ i).subtype -- probably will eventually want this for lie_submodules etc too  These definitions are desirable because the elaborator is often unhappy with to_add_monoid$ λ i, (Mᵢ i).subtype without a definition to help it work out the types; but abbreviation would be fine too.

#### Eric Wieser (Apr 26 2021 at 22:44):

Some ideas I've had so far are direct_sum.coe_add_submonoid, direct_sum.to_add_monoid_carrier, and direct_sum.sum_add_submonoids (and the obvious add_group and module variants).

#### Kevin Buzzard (Apr 27 2021 at 08:01):

Mathematically sum feels closest to what's going on. Any reason for the extra s in the sum case? Coe is also good -- both short

#### Eric Wieser (Apr 27 2021 at 08:09):

.sum_add_submonoid without a trailing s risks implying "the add_submonoid which holds a sum" or similar

#### Kevin Buzzard (Apr 27 2021 at 16:14):

Let $M$ be an additive monoid and let $R$ be a (semi)ring which is internally $M$-graded (i.e. $R\cong\bigoplus_mR_m$ with $R_m$ submonoids of $R$ satisfying $1\in R_0$ and $R_sR_t\subseteq R_{s+t}$). I want to say "if $r=ab$ then $r_m=\sum_{s+t=m}a_sb_t$". Here $m,s,t$ are in the monoid and $r_m$ is notation for "the $m$ th component of $r$, considered as an element of $R$". The maths proof is "this is true by definition of product". I am not even sure how I want to say this. In my application probably any formalisation will do, because I can prove that $s+t=m\implies a_sb_t=0$ and I want to prove $r_m=0$. My instinct is to write this as a finsum because summing over the subset of $M^2$ looks much easier to me than any other option; I think that any dependent attempt to do this might well end up in dependent type hell because how do I know $R_{s+t}=R_{s'+t'}$? However there's the finsupp approach, which has $m\mapsto r_m$ as a term of type M →₀ R and in this situation one could define a product on M →₀ R (by $(fg)(m):=\sum_{s+t=m}f(s)g(t)$) and show that the natural map from $R$ to M →₀ R was an injective ring hom.
Is this product on M →₀ R already there?

The external version of this might be a nightmare to even _state_?

#### Eric Wieser (Apr 27 2021 at 16:25):

I think your statement falls out something like

calc r = a*b : _
... = to_add_monoid_carrier (decompose (a * b)) : equiv.apply_symm_apply to_add_monoid_carrier _
... = to_add_monoid_carrier (decompose a * decompose b)
: _ -- #7380 includes a proof that to_add_monoid_carrier maps multiplication, which must also apply to the inverse
... = sorry : _ -- I'm not sure how best to state the final goal


#### Kevin Buzzard (Apr 27 2021 at 16:27):

Right -- half the question is how to state it. I propose using finsum, but another approach is to put a multiplication on M →₀ R -- or is this there already?

#### Eric Wieser (Apr 27 2021 at 16:27):

That's there already, its monoid_algebra.has_mul

#### Kevin Buzzard (Apr 27 2021 at 16:27):

Is a grading on R the same thing as a ring hom from R to monoid_algebra M R?

#### Kevin Buzzard (Apr 27 2021 at 16:28):

No, but it's a certain kind of hom

#### Eric Wieser (Apr 27 2021 at 16:28):

That was what I argued all that time ago in #4321

#### Kevin Buzzard (Apr 27 2021 at 16:28):

The fundamental construction is something else

#### Kevin Buzzard (Apr 27 2021 at 16:29):

A grading on R is a ring hom from R to monoid_algebra M R which has a bunch of weird properties, and my instinct is still that this is not the right definition

#### Kevin Buzzard (Apr 27 2021 at 16:30):

I'm not sure I can even classify which ring homs are internal direct sums

#### Eric Wieser (Apr 27 2021 at 16:31):

I feel like monoid_algebra is a distraction here

#### Eric Wieser (Apr 27 2021 at 16:31):

It's just direct_sum without dependent types

#### Kevin Buzzard (Apr 27 2021 at 16:31):

One interesting property is that there's a canonical map monoid_algebra M R -> R given by finsupp.sum which is a one-sided inverse

#### Kevin Buzzard (Apr 27 2021 at 16:32):

Yes, but internal direct sums should be easier than external direct sums precisely because we can use this trick to avoid all the dependent type hell

#### Eric Wieser (Apr 27 2021 at 16:32):

I assume you're describing this mapping from #4321?

def sum_id {A : Type*} [comm_semiring k] [semiring A] [algebra k A] [monoid G] :
monoid_algebra A G →ₐ[k] A :=
lift_nc_alg_hom (alg_hom.id k A) ⟨λ g, 1, by simp, λ a b, by simp⟩ (by simp)

lemma sum_id_apply {A : Type*} [comm_semiring k] [semiring A] [algebra k A] [monoid G] (g : monoid_algebra A G) :
sum_id k g = g.sum (λ _ gi, gi) :=
by simp [sum_id, lift_nc_alg_hom, lift_nc_ring_hom, lift_nc, alg_hom.id, ring_hom.id]


#### Kevin Buzzard (Apr 27 2021 at 16:34):

Yes, that's the map. The result I need is that the composite of the map given by the grading A -> monoid_algebra A G and the map above is the identity function.

#### Eric Wieser (Apr 27 2021 at 16:35):

Right, which is exactly docs#direct_sum.add_submonoid_is_internal with the dependent types removed

#### Eric Wieser (Apr 27 2021 at 16:36):

direct_sum.to_add_monoid (λ (i : ι), (A i).subtype) is the dependent version of sum_id, which has the benefit of having a two-sided inverse

#### Kevin Buzzard (Apr 27 2021 at 16:36):

The reason I was asking about moving from dfinsupp to finsupp recently was precisely to make this kind of statement.

#### Eric Wieser (Apr 27 2021 at 16:37):

Admittedly sum_id has more structure: it's a →ₐ[k], whereas to_add_monoid is only a →+; but #7380 introduces to_semiring which is a →+* which is probably good enough for now

#### Eric Wieser (Apr 27 2021 at 16:39):

Coming up with good names here, and where possible using the same ones for monoid_algebra and direct_sum, would help a lot.

#### Kevin Buzzard (Apr 27 2021 at 16:39):

I think that the extra structure on sum_id is bogus. If you can prove the map is a ring homomorphism then it's automatically a k-algebra homomorphism because the k-algebra structure on monoid_algebra A G is coming from the boring map $A\to A[G]$ so anything $A$-linear is automatically $k$-linear for any map k ->*+ A

#### Eric Wieser (Apr 27 2021 at 16:39):

Sure, but that boring structure isn't there for direct_sum.

#### Kevin Buzzard (Apr 27 2021 at 16:42):

Right, but all I'm saying is that sum_id is trivially equivalent to the version where there is no k and you just demand it's an A-algebra hom, although now I see that getting this from ring hom is the same as proving that $A\to A[G]\to A$ is the identity where the first map is the boring one (otherwise known as the $G$-grading where $A_1=A$ and $A_g=0$ otherwise).

#### Eric Wieser (Apr 27 2021 at 16:43):

Making it an A-algebra hom requires commutativity of A

#### Kevin Buzzard (Apr 27 2021 at 16:44):

oh lol, all rings are commutative for me, I retract my last comments if they don't work in the non-commutative case

#### Kevin Buzzard (Apr 27 2021 at 23:09):

@Eric Wieser I've just realised that the map from R to monoid_algebra R M induced by an internal M-grading on R isn't a ring homomorphism. It's an additive group hom and a one sided inverse to the augmentation map but it might not preserve multiplication. Example : I think you can grade the complexes by the monoid +-1 by sending +1 to the reals and -1 to the pure imaginary numbers, but i^2=-1 and the image of i in the monoid map has square +1

Last updated: Jun 17 2021 at 16:20 UTC