Zulip Chat Archive

I'm back thinking about graded rings and how better to do #9717 . I think that we need some internally graded ring. Do we have something like this already? I just looked around and found internally graded monoids, groups and modules, but not rings:

import algebra.direct_sum.basic

variables {R : Type*} [comm_ring R] {ι : Type*} [add_comm_monoid ι]
  (A : ι → add_subgroup R) [decidable_eq ι]

def plays_well_with_multiplication : Prop :=
∀ (i j : ι) (a b : R), a ∈ A i → b ∈ A j → a * b ∈ A (i + j)

def ring_is_internally_graded : Prop :=
direct_sum.add_subgroup_is_internal A ∧ plays_well_with_multiplication A

Furthermore, should it be a typeclass?

Johan Commelin (Oct 26 2021 at 14:39):

cc @Eric Wieser

Eric Wieser (Oct 26 2021 at 15:45):

I think docs#direct_sum.gsemiring.of_submodules is the closest we have

Eric Wieser (Oct 26 2021 at 15:46):

I think what you're proposing is replacing its arguments with typeclasses

Eric Wieser (Oct 26 2021 at 15:53):

Also don't you need that the bijection implied by is_internal preserves multiplication? Or is that always true?

Kevin Buzzard (Oct 26 2021 at 16:41):

I didn't define the external multiplication at all

Kevin Buzzard (Oct 26 2021 at 16:41):

so you can just define it to be the internal multiplication

Kevin Buzzard (Oct 26 2021 at 16:44):

I suspect I can make a term of type direct_sum.gsemiring (lam x, \u(A x)) knowing just plays_well_with_multiplication and also plays_well_with_identity : 1 \in A 0 (which I forgot above).

Eric Wieser (Oct 26 2021 at 17:59):

Yes, I'm sure you can make that instance

Eric Wieser (Oct 26 2021 at 18:01):

My question is whether you have enough to follow up with R ≃+* ⊕ i, A i

Kevin Buzzard (Oct 26 2021 at 18:13):

And I claim that mathematically I do, although one will need to know that an abelian group homomorphism from $\oplus_i A_i$ to somewhere is determined by what it does on each $A_i$ .

Eric Wieser (Oct 26 2021 at 18:16):

That's docs#direct_sum.to_semiring

Eric Wieser (Oct 26 2021 at 18:17):

Oh, or maybe just docs#direct_sum.to_monoid since you said abelian group not ring

Eric Wieser (Oct 26 2021 at 18:18):

I think the pieces you need are mostly there, just not the API

Kevin Buzzard (Oct 26 2021 at 19:09):

I haven't written any non-teaching Lean code for so long, so I thought I'd have a go; I didn't finish though and now I need to go and cook:

import algebra.direct_sum.algebra

variables {R : Type*} [comm_ring R] {ι : Type*} [add_comm_monoid ι]
  (A : ι → add_subgroup R) [decidable_eq ι]

def plays_well_with_multiplication : Prop :=
∀ {i j : ι} {a b : R}, a ∈ A i → b ∈ A j → a * b ∈ A (i + j)

def plays_well_with_one : Prop :=
(1 : R) ∈ A 0

def ring_is_internally_graded : Prop :=
direct_sum.add_subgroup_is_internal A ∧
  plays_well_with_one A ∧
  plays_well_with_multiplication A

def gsemiring.of_ring_is_internally_graded (h : ring_is_internally_graded A) :
  direct_sum.gsemiring (λ i, A i) :=
let ⟨hint, hone, hmul⟩ := h in
{ mul := λ i j ai aj, ⟨ai.1 * aj.1, hmul ai.2 aj.2⟩,
  mul_zero := λ i j ai, by {ext, exact mul_zero _},
  zero_mul := λ _ _ _, by {ext, exact zero_mul _},
  mul_add := λ _ _ _ _ _, by {ext, exact mul_add _ _ _ },
  add_mul := λ _ _ _ _ _, by {ext, exact add_mul _ _ _ },
  one := ⟨(1 : R), hone⟩,
  one_mul := by {rintro ⟨i, ai⟩, unfold has_one.one, unfold has_mul.mul, ext; simp, },
  mul_one := by {rintro ⟨i, ai⟩, unfold has_one.one, unfold has_mul.mul, ext; simp, },
  mul_assoc := by {rintro ⟨i, ai⟩ ⟨j, aj⟩ ⟨k, ak⟩, unfold has_mul.mul, ext; simp [add_assoc, mul_assoc], },
  gnpow := λ n i, nat.rec_on n (λ ai, ⟨(1 : R), by convert hone; exact zero_smul _ _⟩)
    (λ n f ai, ⟨ai.1 * (f ai).1, by convert hmul ai.2 (f ai).2; exact succ_nsmul i n⟩),
  gnpow_zero' := sorry,
  gnpow_succ' := sorry
  }

Kevin Buzzard (Oct 26 2021 at 19:09):

What are the correct names for all these things which I'm giving silly names to?

Eric Wieser (Oct 26 2021 at 20:02):

Your last def would be shorter and sorry-free in terms of docs#direct_sum.gsemiring.of_add_subgroups

Eric Wieser (Oct 26 2021 at 20:05):

(and does not use the fact the grading is internal!)

Kevin Buzzard (Oct 26 2021 at 20:06):

@Jujian Zhang do you want to take over? I'm not sure I'll have any more time for this today

Eric Wieser (Oct 26 2021 at 20:10):

I think to make the API worthwhile, the plays_well_with_multiplication defs probably ought to be typeclasses

Jujian Zhang (Oct 26 2021 at 21:46):

import algebra.direct_sum.algebra

open_locale classical

variables {R : Type*} [comm_ring R] {ι : Type*} [add_comm_monoid ι]
  (A : ι → add_subgroup R)

variable (R)
class graded_ring :=
( is_internal :  direct_sum.add_subgroup_is_internal A )
( one_degree_zero : (1 : R) ∈ A 0 )
( mul_respect_grading : ∀ {i j : ι} {a b : R}, a ∈ A i → b ∈ A j → a * b ∈ A (i + j))

noncomputable def gsemiring.of_ring_is_internally_graded [graded_ring R A] :
  direct_sum.gsemiring (λ i, A i) :=
direct_sum.gsemiring.of_add_subgroups A (graded_ring.one_degree_zero) (λ i j ai aj, graded_ring.mul_respect_grading ai.2 aj.2)

Jujian Zhang (Oct 26 2021 at 21:47):

By typeclass, do you mean something like this? Maybe pr #9717 should be rewritten using internal definitions so that homogeneous ideals and other lemmas would work for mv_polynomial

Kevin Buzzard (Oct 26 2021 at 22:07):

Can you construct the ring isomorphism $R\cong \oplus_i A_i$ ?

Kevin Buzzard (Oct 26 2021 at 22:08):

I guess ≃+* will be docs#ring_equiv

Jujian Zhang (Oct 26 2021 at 22:28):

noncomputable def test [graded_ring R A] : (⨁ i, A i) ≃+* R :=
{ to_fun :=  direct_sum.to_add_monoid (λ i, { to_fun := (A i).subtype, map_zero' := rfl, map_add' := λ _ _, rfl }),
  inv_fun := (equiv.of_bijective _ graded_ring.is_internal).symm,
  left_inv := λ x, begin refine equiv.symm_apply_apply _ _, end,
  right_inv := λ x, begin convert equiv.apply_symm_apply (equiv.of_bijective _ graded_ring.is_internal) _, end,
  map_mul' := λ x y, sorry,
  map_add' := λ x y, sorry, }

Jujian Zhang (Oct 26 2021 at 22:29):

This should work (mod sorries)

Kevin Buzzard (Oct 26 2021 at 22:30):

Oh very nice! I think map_mul' was the sorry Eric was concerned about

Kevin Buzzard (Oct 26 2021 at 22:33):

I think the next thing we want is a "project onto I'th factor" function proj i : R -> R and a proof that proj i r ∈ A i

Jujian Zhang (Oct 26 2021 at 22:37):

Can we define proj i to be the composition of $R \to \oplus_i A_i$ and $\oplus_i A_i \to A_i$ and $A_i \to R$

Jujian Zhang (Oct 26 2021 at 22:41):

map_mul' := λ x y, begin rw [direct_sum.eq_sum_of _ x, direct_sum.eq_sum_of _ y],
    rw [finset.sum_mul_sum, add_monoid_hom.map_sum, add_monoid_hom.map_sum, add_monoid_hom.map_sum, finset.sum_mul_sum],
    apply finset.sum_congr rfl,
    rintros ⟨i, j⟩ hmem,
    sorry
  end,

Kevin Buzzard (Oct 26 2021 at 22:42):

Right, this might be the only way to do it

Jujian Zhang (Oct 26 2021 at 22:42):

Something like this should work: write $x:\oplus_i A_i$ as $\sum_i x_i$ and $y:\oplus_j A_j$ as $\sum y_j$ . Then expand etc.

Eric Wieser (Oct 27 2021 at 00:03):

Using docs#direct_sum.to_semiring will be easier than using docs#direct_sum.to_add_monid and filling the map_mul manually (as I said upthread!)

Eric Wieser (Oct 27 2021 at 00:06):

@Jujian Zhang, your graded_ring typeclass is what my comment was suggesting yes.

Eric Wieser (Oct 27 2021 at 00:12):

I'd argue though that we should use a data-carrying typeclass:

class graded_ring :=
( decompose : R → ⊕ i, A i)
( left_inv : function.left_inverse decompose sorry )
( right_inv : function.left_inverse decompose sorry )
( one_degree_zero : (1 : R) ∈ A 0 )
( mul_respect_grading : ∀ {i j : ι} {a b : R}, a ∈ A i → b ∈ A j → a * b ∈ A (i + j))

Where the sorrys are the to_add_monoid subtype monster I don't want to type on mobile.

Jujian Zhang (Oct 27 2021 at 11:17):

I have opened another pr (#10002) containing the above code and an instance that mv_polynomial is graded

Johan Commelin (Oct 27 2021 at 11:21):

Thanks! Please update the title to follow the style guide.

Johan Commelin (Oct 27 2021 at 11:23):

At some point we will need/want graded algebras. Should we just do everything for graded algebras from the start?

Johan Commelin (Oct 27 2021 at 11:23):

So, should the A i be submodules over some base ring?

Johan Commelin (Oct 27 2021 at 11:24):

That would also deal with the ring/semiring distinction (in case someone wants to consider the grading of polynomials over ℕ)

Eric Wieser (Oct 27 2021 at 11:27):

We have all the pieces to build that too

Eric Wieser (Oct 27 2021 at 11:27):

I think the question is whether we want to force users to convert their add_submonoids and add_subgroups into nat and int-submodules.

Eric Wieser (Oct 27 2021 at 11:28):

At the moment, we just duplicate all the API for each of them

Johan Commelin (Oct 27 2021 at 11:28):

My hunch is that whatever the user is doing will almost always be an algebra already. Basically, I claim that every interesting lemma about graded rings also has a companion for graded algebras, and the user should be proving that one instead.

Eric Wieser (Oct 27 2021 at 11:29):

This was the type of problem I was trying to solve with set_like but lost steam on; if we had a typeclass saying "this is a subtype whose addition / smul / zero is the one induced by coercion", then we could generalize

Johan Commelin (Oct 27 2021 at 11:29):

I think there are very few cases where you genuinely want to work with a graded ℤ-algebra, instead of generalizing.

Eric Wieser (Oct 27 2021 at 11:30):

For reference, docs#direct_sum.to_algebra and docs#direct_sum.galgebra.of_submodules are the parallel defs to docs#direct_sum.to_semiring and docs#direct_sum.gsemiring.of_add_subgroups.

Jujian Zhang (Oct 29 2021 at 21:19):

If ring $R$ is graded by $\iota\to A_i$ , do we require that $A_i\cap A_j = \bot$ for $i\ne j$ ?

Yaël Dillies (Oct 29 2021 at 21:23):

Shameless plug of docs#set.pairwise_disjoint and #9898 which gives you the correct generality for what you just said.

Eric Wieser (Oct 29 2021 at 21:40):

No it won't, that statement isn't strong enough; you need the sup_indep PR for that, @Yaël Dillies.

Eric Wieser (Oct 29 2021 at 21:40):

Jujian Zhang, Are you looking for docs#direct_sum.submodule_is_internal.independent?

Yaël Dillies (Oct 29 2021 at 21:42):

Uh? Okay. But that's not what Jujian just wrote.

Jujian Zhang (Oct 29 2021 at 21:43):

Eric Wieser said:

Jujian Zhang, Are you looking for docs#direct_sum.submodule_is_internal.independent?

Thank you.

Jujian Zhang (Oct 29 2021 at 21:44):

Yaël Dillies said:

Uh? Okay. But that's not what Jujian just wrote.

I originally wrote $A_i \cap A_j = 0$ , I thought $0$ might be confused with empty set so I changed it to $\bot$

Yaël Dillies (Oct 29 2021 at 21:47):

No, that's not what I meant. There's a difference between asking pairwise disjointness and arbitrary disjointness.

Yaël Dillies (Oct 29 2021 at 21:49):

Typicall, take the vector subspaces of $\R^2$ (x, 0), (0, x), (x, x). They are pairwise disjoint but are each in the sup of the other two.

Yaël Dillies (Oct 29 2021 at 21:49):

That's the difference between docs#set.pairwise_disjoint and finset.sup_indep (introduced in #9867)/docs#complete_lattice.independent.

Jujian Zhang (Oct 29 2021 at 21:50):

@Eric Wieser , since each $A_i$ are only add_subgroup R, is there a version of direct_sum.add_subgroup_is_internal.independent? Thank you.

Eric Wieser (Oct 29 2021 at 21:50):

No, because it would have been annoying to repeat the proof two more times, so I didn't bother

Jujian Zhang (Oct 29 2021 at 21:51):

Let me try and copy paste then to see if I can do it.

Eric Wieser (Oct 29 2021 at 21:51):

There might be an easier way

Eric Wieser (Oct 29 2021 at 21:51):

You can use docs#add_subgroup.to_int_submodule to convert your subgroups into submodules

Eric Wieser (Oct 29 2021 at 21:51):

And then probably use the lemmas, then massage the results back into statements about add_subgroups

Eric Wieser (Oct 29 2021 at 21:52):

Alternative, abandon add_subgroup altogether and just work with submodule int R which is isomorphic anyway

Eric Wieser (Oct 29 2021 at 21:53):

Which is what @Johan Commelin suggested upthread I think. It feels sort of ugly, but repeating everything three times is more ugly, especially if we can't work out how to reuse the proofs

Jujian Zhang (Oct 29 2021 at 21:55):

The only reason I am asking for this is because I want the following lemma:

lemma graded_ring.proj_homogeneous_element {x : R} {i : ι} (hx : x ∈ A i) :
  graded_ring.proj R A i x = x := sorry

Jujian Zhang (Oct 29 2021 at 21:56):

I couldn't get it work without knowing trivial intersection. If I could get this lemma without trivial intersection then we can delay making the decesion whether we should use submodule int R