Gradings on a ring

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Eric Wieser]

Don't PR this without cleanup!

lemma independent_iff {α : Type*} [complete_lattice α] (s : set α) :
  independent s ↔ independent' (coe : s → α) :=
begin
  unfold independent independent',
  rw set_coe.forall,
  apply forall_congr,
  intro a,
  apply forall_congr,
  intro ha,
  dunfold set.has_coe_to_sort,
  rw supr_subtype,
  rw Sup_eq_supr,
  simp,
  congr',
  ext,
  rw supr_and,
end

[Adam Topaz]

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]

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

[Adam Topaz]

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]

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]

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

[Eric Wieser]

I might go further and require an explicit inverse

[David Wärn]

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]

I mean, I guess it depends on the definition?

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Eric Wieser]

I posted a version of that above

[Adam Topaz]

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]

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

[Eric Wieser]

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

[Adam Topaz]

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

[Eric Wieser]

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

[Eric Wieser]

order.complete_lattice

[David Wärn]

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]

I assume you mean dfinsupp not finsupp?

[Eric Wieser]

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

[Johan Commelin]

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

[Johan Commelin]

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

[David Wärn]

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]

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]

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

[Eric Wieser]

And ditto for submonoid and subgroup

[Kevin Buzzard]

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

[Eric Wieser]

Two is just a direct sum over bool :)

[Kevin Buzzard]

Maybe that's "internal product"?

[Kevin Buzzard]

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

[Eric Wieser]

Why does that matter?

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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]

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.

[Adam Topaz]

Oh I see.

[Adam Topaz]

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

[Kevin Buzzard]

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

[David Wärn]

Yes product and sum of groups are not the same

[Adam Topaz]

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

[Adam Topaz]

Groups are awful

[Adam Topaz]

Internal direct product should not be a thing

[Adam Topaz]

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

[David Wärn]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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