# Zulip Chat Archive

## 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_submonoid`s 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_subgroup`s 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_submodule`s 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