Question about Graded Stuff

Stream: maths

[Wanyi He]

Hi, I meet some problems when using API of GradedRing.

I want to give ring R a gradation by quotient of its additive subgroup. But it seems that graduations which are not indexed by the same thing on the ring is still missing. So I have no idea what to do now :smiling_face_with_tear: . Should I extend the definition of GradedRing in mathlib4? (I think DirectSum.Decomposition need to be extended too)

Btw, I tried DirectSum.of to map the quotient into its direct sum, and proved it's bijective. However, it caused slow instance inference and I don't think it's a right/efficient way.(I have to use set_option synthInstance.maxHeartbeats 0)

I'd be grateful if anyone can help me :laughing:

[Eric Wieser]

What do you mean by:

But it seems that graduations which are not indexed by the same thing on the ring

[Wanyi He]

For example:

Consider a filtered ring $R$ together with a filtration $fil$ s.t $\forall n\in \mathbb{Z},fil_nR$ is additive subgroup of $R$ and satisfies some properties.

Now we can construct a graded ring $\oplus_{n}fil_nR/fil_{n-1}R$. But in this case, these quotients are not the same type.

(It's too late in my time zone and I'll be back in 8 h.)

[Eric Wieser]

The whole point of docs#GradedRing is to allow each piece to be a different type! whoops, I got confused, and meant GRing!

[Eric Wieser]

But indeed constructing the associated graded algebra for a filtered algebra is not easy.

[Eric Wieser]

Concretely, you want to make a GRing fun i => fil i ⧸ (fil (i - 1)).comap (fil i).subtype instance

[Wanyi He]

Eric Wieser said:

The whole point of docs#GradedRing is to allow each piece to be a different type!

Why? I'm really sorry I do not understand that. Here's my mwe. Simply write GradedRing (fun i => fil i ⧸ (fil (i - 1)).comap (fil i).subtype) doesn't work.

import Mathlib

universe u

variable {R : Type u} [Ring R]

variable (fil : ℤ → AddSubgroup R)

instance : GradedRing (fun i => fil i ⧸ (fil (i - 1)).comap (fil i).subtype) := sorry
-- failed to synthesize SetLike (Type u) ?m.337

[Wanyi He]

Eric Wieser said:

Concretely, you want to make a GRing fun i => fil i \bigsolidus (fil (i - 1)).comap (fil i).subtype instance

Yep, I know GRing instance is needed here.

[Wanyi He]

Wanyi He said:

Eric Wieser said:

The whole point of docs#GradedRing is to allow each piece to be a different type!

Why? I'm really sorry I do not understand that. Here's my mwe. Simply write GradedRing (fun i => fil i ⧸ (fil (i - 1)).comap (fil i).subtype) doesn't work.

import Mathlib

universe u

variable {R : Type u} [Ring R]

variable (fil : ℤ → AddSubgroup R)

instance : GradedRing (fun i => fil i ⧸ (fil (i - 1)).comap (fil i).subtype) := sorry
-- failed to synthesize SetLike (Type u) ?m.337

Another way is

import Mathlib

universe u

variable {R : Type u} [Ring R] (fil : ℤ → AddSubgroup R)

abbrev GradedPiece (i : ℤ) := fil i ⧸ (fil (i - 1)).comap (fil i).subtype

def GradedPiece' (i : ℤ) := (DirectSum.of (GradedPiece fil) i).range

instance : DirectSum.GSemiring (GradedPiece fil) := sorry

instance : GradedRing (GradedPiece' fil) := sorry

[Eric Wieser]

Sorry, I misspoke above; you should just be avoiding GradedRing entirely and using GRing

[Wanyi He]

Oh I see. I'll try that. Thanks!