Zulip Chat Archive

Stream: maths

Topic: Gradings on a ring


view this post on Zulip Kevin Buzzard (Apr 13 2021 at 17:27):

Over in #condensed mathematics we've been discussing gradings on a ring. There seems to be an almost lattice-theoretic part to the definition: an M-grading (M an add_comm_monoid) on a ring R is a map from M to the lattice of add_subgroups of R which (amongst other things) induces an isomorphism of add_comm_groups between the direct sum of the subgroups and R. It seems that there is a purely lattice-theoretic way to say this: we want the Sup of all the subgroups to be top, and we want the inf of (one subgroup) and (the Sup of all the other subgroups) to be bot. It almost feels like this is some kind of "basis" for the lattice. Is this a thing in lattice theory? Is this something to do with matroids @Peter Nelson ? Rather annoyingly, docs#complete_lattice.independent works with sets of elements rather than maps from a type (rather like the issue we had with bases of a vector space recently).

view this post on Zulip Eric Wieser (Apr 13 2021 at 17:30):

The thread in question starts about here in Johan Commelin's message

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 17:30):

The proposal so far is to refactor independent so that it works with an indexed family but just to spell out independent and span explicitly, lattice-theoretically, however if there's something there already it might be possible to use it

view this post on Zulip Eric Wieser (Apr 13 2021 at 17:34):

Comparing the definitions, this is what we have in mathlib today:

def independent {α : Type*} [complete_lattice α] (s : set α): Prop :=
 a : α⦄, a  s  disjoint a (Sup (s \ {a}))

and this I think is the indexed alternative we're wishing we had:

def independent' {ι : Sort*} {α : Type*} [complete_lattice α] (s : ι  α): Prop :=
 i : ι⦄, disjoint (s i) ( (j  i), s j)

view this post on Zulip Peter Nelson (Apr 13 2021 at 17:41):

Kevin Buzzard said:

Over in #condensed mathematics we've been discussing gradings on a ring. There seems to be an almost lattice-theoretic part to the definition: an M-grading (M an add_comm_monoid) on a ring R is a map from M to the lattice of add_subgroups of R which (amongst other things) induces an isomorphism of add_comm_groups between the direct sum of the subgroups and R. It seems that there is a purely lattice-theoretic way to say this: we want the Sup of all the subgroups to be top, and we want the inf of (one subgroup) and (the Sup of all the other subgroups) to be bot. It almost feels like this is some kind of "basis" for the lattice. Is this a thing in lattice theory? Is this something to do with matroids Peter Nelson ? Rather annoyingly, docs#complete_lattice.independent works with sets of elements rather than maps from a type (rather like the issue we had with bases of a vector space recently).

When you say 'direct sum of the subgroups', which collection of subgroups are you summing over?

view this post on Zulip Eric Wieser (Apr 13 2021 at 17:42):

I'm struggling to tidily prove it, but independent s ↔ independent' (coe : s → α), so clearly the primed version is more powerful

view this post on Zulip Eric Wieser (Apr 13 2021 at 17:45):

view this post on Zulip Adam Topaz (Apr 13 2021 at 17:51):

We could also forget about all the independence business completely and take a function M \to subgroup R, say mHmm \mapsto H_m such that the canonical map
mMHmR \bigoplus_{m \in M} H_m \to R
is bijective

view this post on Zulip Adam Topaz (Apr 13 2021 at 17:52):

Well, I guess we need to ensure that the HmH_m are nontrivial

view this post on Zulip Adam Topaz (Apr 13 2021 at 17:57):

Actually I now think the independence condition is not what we want anyway! What if I want to consider k[X]/(X2)k[X]/(X^2) as a N\mathbb{N}-graded ring whose components in degree 2\geq 2 are all trivial?

view this post on Zulip Adam Topaz (Apr 13 2021 at 17:58):

The collection {k,xk[X]/(X2),0,0,}\{k, x \cdot k[X]/(X^2), 0, 0, \ldots\} is not an independent collection of subgroups of k[X]/(X2)k[X]/(X^2).

view this post on Zulip Adam Topaz (Apr 13 2021 at 18:18):

import algebra.direct_sum
import group_theory.subgroup
import algebra

open_locale direct_sum

variables (R : Type*) [ring R]

open_locale classical

noncomputable theory

--rename me
def foo {A : Type*} [add_comm_group A] {ι : Type*}
  (f : ι  add_subgroup A) : ( i, f i) →+ A :=
dfinsupp.sum_add_hom (λ i : ι, (f i).subtype)

structure grading (M : Type*) [add_monoid M] :=
(graded_part : M  add_subgroup R)
(iso : function.bijective $ foo graded_part)
(grading_one : (1 : R)  graded_part 0)
(grading_mul {r s m n} :
  r  graded_part m  s  graded_part n  (r * s)  graded_part (m+n))

view this post on Zulip Eric Wieser (Apr 13 2021 at 19:17):

I might go further and require an explicit inverse

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

Adam Topaz said:

The collection {k,xk[X]/(X2),0,0,}\{k, x \cdot k[X]/(X^2), 0, 0, \ldots\} is not an independent collection of subgroups of k[X]/(X2)k[X]/(X^2).

Isn't it? The zero subgroup should be disjoint from everything

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:21):

I mean, I guess it depends on the definition?

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:22):

But I guess you're right @David Wärn with the way independence is defined now

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

Another issue that came up is that independence is defined for sets and not parameterized families, so one would have to enforce some injectivity condittion on the family to make it compatible with the set-wise definition, and having multiple 0's as above would break this.

view this post on Zulip David Wärn (Apr 13 2021 at 19:26):

Aha. Yes, we need the indexed-family version of independence to make sense of this example

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

I posted a version of that above

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:27):

But @David Wärn 's comment shows that independence (for objects in a lattice) really does need to be defined in terms of families and not sets ;))

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

I think if we add a tidy version of spoiler'd lemma, it should be easy to change the definition in mathlib

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

(and punt actually changing the downstream statements to a future PR)

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:29):

@Eric Wieser what imports am I missing from your spoiler code?

view this post on Zulip Eric Wieser (Apr 13 2021 at 19:29):

Right, @David Wärn's example shows injectivity may be too strong a constraint

view this post on Zulip Eric Wieser (Apr 13 2021 at 19:29):

order.complete_lattice

view this post on Zulip David Wärn (Apr 13 2021 at 19:33):

I was taught the terminology "internal / external direct sum" (in the binary case). The external direct sum is the explicit finsupp construction. An internal direct sum is when you have some submodules of a given module. You can define it either as "the canonical map from the external direct sum is an isomorphism", or as "together the submodules span the entire module, and moreover they are independent"

view this post on Zulip Eric Wieser (Apr 13 2021 at 19:35):

I assume you mean dfinsupp not finsupp?

view this post on Zulip Eric Wieser (Apr 13 2021 at 19:36):

Note that "internal direct sum" is a missing item in undergrad.yaml

view this post on Zulip Johan Commelin (Apr 13 2021 at 19:42):

It is missing, because it's such an awkard notion... it asserts two things at the same time.

view this post on Zulip Johan Commelin (Apr 13 2021 at 19:43):

Also, is "internal direct sum" just a predicate on two submodules? Or is it a predicate + a construction?

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

It should be a subsingleton at least. Normally you'd use it for two submodules but in this situation we have an M-indexed family of submodules

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 19:45):

Right now I'm torn between the "map from direct sum is bijective" and (independent' + "Sup = top" ). Maybe it doesn't matter what the definition is because probably it should be proved that they're the same thing

view this post on Zulip Eric Wieser (Apr 13 2021 at 19:46):

How about a statement submodule.direct_sum_is_internal X that states what adam put in his definition about a family X?

view this post on Zulip Eric Wieser (Apr 13 2021 at 19:47):

And ditto for submonoid and subgroup

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 19:47):

Aargh I think that people might allow internal direct sum of two subgroups of a noncommutative group :-/

view this post on Zulip Eric Wieser (Apr 13 2021 at 19:47):

Two is just a direct sum over bool :)

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 19:47):

Maybe that's "internal product"?

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 19:48):

No the issue here is that the underlying monoid law might not be abelian

view this post on Zulip Eric Wieser (Apr 13 2021 at 19:48):

Why does that matter?

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:48):

The monoid law has nothing to do with the direct sum issue,

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

it only comes in play in the compatibility with the ring structure

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:51):

import algebra.direct_sum
import group_theory.subgroup
import algebra

open_locale direct_sum

open_locale classical

noncomputable theory

--rename me
def foo {A : Type*} [add_comm_group A] {ι : Type*}
  (f : ι  add_subgroup A) : ( i, f i) →+ A :=
dfinsupp.sum_add_hom (λ i : ι, (f i).subtype)

structure grading (M : Type*) (A : Type*) [add_comm_group A] :=
(graded_part : M  add_subgroup A)
(iso : function.bijective $ foo graded_part)

structure graded_ring (M : Type*) [add_monoid M] (A : Type*) [ring A]
  extends grading M A :=
(grading_one : (1 : A)  graded_part 0)
(grading_mul {r s m n} :
  r  graded_part m  s  graded_part n  (r * s)  graded_part (m+n))

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 19:52):

Just to be clear, I am talking about the assertion that if AA and BB are normal subgroups of a group GG such that G=ABG=AB and AB=1A\cap B=1 then GG is isomorphic to A×BA\times B and I was suggesting that "internal direct sum" might cover this situation, whereas nothing we're doing does.

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:52):

Oh I see.

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:52):

This can be done in any category with coproducts, and subobjects which form a complete lattice

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 19:52):

But I'm rather hoping that this is "internal direct product" :-)

view this post on Zulip David Wärn (Apr 13 2021 at 19:53):

Yes product and sum of groups are not the same

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:54):

But the issue is that the universal property of the product tells you how to map into it, not map out of it.

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:54):

Groups are awful

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:55):

Internal direct product should not be a thing

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:55):

since XYX \to Y and ZYZ \to Y gives XZYX \coprod Z \to Y

view this post on Zulip David Wärn (Apr 13 2021 at 19:56):

I think for internal direct product you might want a family of quotients instead of subobjects

view this post on Zulip Adam Topaz (Apr 13 2021 at 19:56):

I guess you could parameterize the quotients of a group by the normal subgroups, and go that way

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 19:56):

Great -- if it shouldn't happen then I'm sure the French wouldn't be teaching it, they know what they're talking about. I'll stick to arbitrary internal direct sums and throw something into submonoid of a comm_monoid.

view this post on Zulip David Wärn (Apr 13 2021 at 20:01):

Anyway internal direct sums of submodules should be useful in other situations? They naturally generalize bases, and there are nice theorems like. "a f.d. complex representation of a finite group is the internal direct sum of its isotypical components", and "a f.d. complex vector space with an endomorphism is the internal direct sum of its generalised eigenspaces"

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 20:06):

Yes, I was really struck earlier about how one condition was called independent' and the other one span -- somehow I'd not put two and two together before

view this post on Zulip Kevin Buzzard (Apr 13 2021 at 20:12):

Ok so the plan is: refactor docs#complete_lattice.independent so that it takes an indexed family not a subset, prove that an indexed family of submonoids of a commutative monoid are independent iff the map from the direct sum is injective, the family spans iff the direct sum is surjective, do everything for additive monoids too, tick off internal direct sums in the undergraduate yaml, and then define a grading by a (not nec commutative) monoid on a (not necc commutative) semiring as an internal direct sum by additive submonoids (plus a couple of extra axioms saying that 1 and * play well with the monoid map). Thanks for the help everyone and let me know if I've missed something.

view this post on Zulip Eric Wieser (Apr 14 2021 at 14:41):

Using the bijective definition, do we want #7190 so that we can tick off the item in undergrad.yaml?

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

Given the context in the yaml, I'm wondering whether it should point to the submodule definition (everything else seems to be about vector spaces).


Last updated: May 10 2021 at 07:15 UTC