## Stream: maths

### Topic: Gradings on a ring

#### 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).

#### Eric Wieser (Apr 13 2021 at 17:30):

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

#### 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

#### 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)


#### 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?

#### 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

#### 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 $m \mapsto H_m$ such that the canonical map
$\bigoplus_{m \in M} H_m \to R$
is bijective

#### Adam Topaz (Apr 13 2021 at 17:52):

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

#### 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]/(X^2)$ as a $\mathbb{N}$-graded ring whose components in degree $\geq 2$ are all trivial?

#### Adam Topaz (Apr 13 2021 at 17:58):

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

#### 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] :=
(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))  #### Eric Wieser (Apr 13 2021 at 19:17): I might go further and require an explicit inverse #### David Wärn (Apr 13 2021 at 19:18): Adam Topaz said: The collection $\{k, x \cdot k[X]/(X^2), 0, 0, \ldots\}$ is not an independent collection of subgroups of $k[X]/(X^2)$. Isn't it? The zero subgroup should be disjoint from everything #### Adam Topaz (Apr 13 2021 at 19:21): I mean, I guess it depends on the definition? #### Adam Topaz (Apr 13 2021 at 19:22): But I guess you're right @David Wärn with the way independence is defined now #### 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. #### 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 #### Eric Wieser (Apr 13 2021 at 19:26): I posted a version of that above #### 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 ;)) #### 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 #### Eric Wieser (Apr 13 2021 at 19:27): (and punt actually changing the downstream statements to a future PR) #### Adam Topaz (Apr 13 2021 at 19:29): @Eric Wieser what imports am I missing from your spoiler code? #### Eric Wieser (Apr 13 2021 at 19:29): Right, @David Wärn's example shows injectivity may be too strong a constraint #### Eric Wieser (Apr 13 2021 at 19:29): order.complete_lattice #### 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" #### Eric Wieser (Apr 13 2021 at 19:35): I assume you mean dfinsupp not finsupp? #### Eric Wieser (Apr 13 2021 at 19:36): Note that "internal direct sum" is a missing item in undergrad.yaml #### 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. #### 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? #### 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 #### 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 #### 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? #### Eric Wieser (Apr 13 2021 at 19:47): And ditto for submonoid and subgroup #### 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 :-/ #### Eric Wieser (Apr 13 2021 at 19:47): Two is just a direct sum over bool :) #### Kevin Buzzard (Apr 13 2021 at 19:47): Maybe that's "internal product"? #### Kevin Buzzard (Apr 13 2021 at 19:48): No the issue here is that the underlying monoid law might not be abelian #### Eric Wieser (Apr 13 2021 at 19:48): Why does that matter? #### Adam Topaz (Apr 13 2021 at 19:48): The monoid law has nothing to do with the direct sum issue, #### Adam Topaz (Apr 13 2021 at 19:49): it only comes in play in the compatibility with the ring structure #### 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))


#### Kevin Buzzard (Apr 13 2021 at 19:52):

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

Oh I see.

#### Adam Topaz (Apr 13 2021 at 19:52):

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

#### Kevin Buzzard (Apr 13 2021 at 19:52):

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

#### David Wärn (Apr 13 2021 at 19:53):

Yes product and sum of groups are not the same

#### 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.

Groups are awful

#### Adam Topaz (Apr 13 2021 at 19:55):

Internal direct product should not be a thing

#### Adam Topaz (Apr 13 2021 at 19:55):

since $X \to Y$ and $Z \to Y$ gives $X \coprod Z \to Y$

#### 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

#### 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

#### 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.

#### 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"

#### 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

#### 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.

#### 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?

#### 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