Zulip Chat Archive

Stream: maths

Topic: grading by submonoids maths question


view this post on Zulip Kevin Buzzard (Apr 23 2021 at 17:54):

Let MM be an additive monoid. I want to grade stuff by MM. According to the semiring police I shouldn't be grading a ring by MM, decomposing it into an internal (possibly infinite) direct sum of add_subgroups indexed by MM, I should instead be grading a semiring by MM, 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 RmR_m for the add_submonoid graded_piece m of RR corresponding to mMm\in M, and direct_sum says that the natural map from the abstract external direct sum mMRm\oplus_{m\in M}R_m to RR is bijective. The other axioms are that 1R01\in R_0 and RmRnRm+nR_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]R[X] by N\mathbb{N} and Damiano graded the monoid algebra R[M]R[M] by MM, for example.

I've now started to work on my intended application, where RR is a commutative ring, and I've realised that I can't see why R0R_0 should be a subring or more precisely an additive subgroup. If R0R_0 contains 1-1 then this is all one needs: multiplication by 1-1 proves that all the RmR_m are add_subgroups, and conversely if all the RmR_m are add_subgroups then 1R0-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 1R0-1\in R_0? Thoughts: by definition 1=mIrm-1=\sum_{m\in I}r_m, a finite sum, and so 1=a,bIrarb1=\sum_{a,b\in I}r_ar_b, meaning that if sc:=a,bI,a+b=crarbs_c:=\sum_{a,b\in I, a+b=c}r_ar_b then sc=0s_c=0 for c0c\not=0 and s0=1s_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]R[X] by N\mathbb{N} if RR 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.

view this post on Zulip Kevin Buzzard (Apr 23 2021 at 17:58):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Apr 23 2021 at 18:06):

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

view this post on Zulip David Wärn (Apr 23 2021 at 18:45):

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Apr 23 2021 at 19:26):

Isn't that docs#direct_sum.component?

view this post on Zulip Kevin Buzzard (Apr 23 2021 at 19:57):

Aah yes it is for modules, but I have monoids

view this post on Zulip 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. :-(

view this post on Zulip Adam Topaz (Apr 23 2021 at 23:49):

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

view this post on Zulip Adam Topaz (Apr 23 2021 at 23:49):

J can be infinite

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 27 2021 at 16:14):

Let MM be an additive monoid and let RR be a (semi)ring which is internally MM-graded (i.e. RmRmR\cong\bigoplus_mR_m with RmR_m submonoids of RR satisfying 1R01\in R_0 and RsRtRs+tR_sR_t\subseteq R_{s+t}). I want to say "if r=abr=ab then rm=s+t=masbtr_m=\sum_{s+t=m}a_sb_t". Here m,s,tm,s,t are in the monoid and rmr_m is notation for "the mm th component of rr, considered as an element of RR". 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    asbt=0s+t=m\implies a_sb_t=0 and I want to prove rm=0r_m=0. My instinct is to write this as a finsum because summing over the subset of M2M^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 Rs+t=Rs+tR_{s+t}=R_{s'+t'}? However there's the finsupp approach, which has mrmm\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):=s+t=mf(s)g(t)(fg)(m):=\sum_{s+t=m}f(s)g(t)) and show that the natural map from RR 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_?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Apr 27 2021 at 16:27):

That's there already, its monoid_algebra.has_mul

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 27 2021 at 16:28):

No, but it's a certain kind of hom

view this post on Zulip Eric Wieser (Apr 27 2021 at 16:28):

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

view this post on Zulip Kevin Buzzard (Apr 27 2021 at 16:28):

The fundamental construction is something else

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 27 2021 at 16:30):

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

view this post on Zulip Eric Wieser (Apr 27 2021 at 16:31):

I feel like monoid_algebra is a distraction here

view this post on Zulip Eric Wieser (Apr 27 2021 at 16:31):

It's just direct_sum without dependent types

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Apr 27 2021 at 16:35):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 AA[G]A\to A[G] so anything AA-linear is automatically kk-linear for any map k ->*+ A

view this post on Zulip Eric Wieser (Apr 27 2021 at 16:39):

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

view this post on Zulip 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 AA[G]AA\to A[G]\to A is the identity where the first map is the boring one (otherwise known as the GG-grading where A1=AA_1=A and Ag=0A_g=0 otherwise).

view this post on Zulip Eric Wieser (Apr 27 2021 at 16:43):

Making it an A-algebra hom requires commutativity of A

view this post on Zulip 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

view this post on Zulip 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