grading by submonoids maths question

Stream: maths

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[David Wärn]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

Isn't that docs#direct_sum.component?

[Kevin Buzzard]

Aah yes it is for modules, but I have monoids

[Scott Morrison]

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]

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

[Adam Topaz]

J can be infinite

[Scott Morrison]

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

[Adam Topaz]

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

[Eric Wieser]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

That's there already, its monoid_algebra.has_mul

[Kevin Buzzard]

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

[Kevin Buzzard]

No, but it's a certain kind of hom

[Eric Wieser]

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

[Kevin Buzzard]

The fundamental construction is something else

[Kevin Buzzard]

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]

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

[Eric Wieser]

I feel like monoid_algebra is a distraction here

[Eric Wieser]

It's just direct_sum without dependent types

[Kevin Buzzard]

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]

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]

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]

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]

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

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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]

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]

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

[Kevin Buzzard]

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]

Making it an A-algebra hom requires commutativity of A

[Kevin Buzzard]

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]

@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