How to define graded ring isomorphisms?

Stream: mathlib4

[Kenny Lau]

Recall that a docs#GradedRing (𝒜 : ι → σ) requires (assumptions):

1. Semiring A
2. AddSubmonoidClass σ A
3. AddMonoid ι
4. GradedRing 𝒜 (I'll add itself to facilitate discussion)

and a graded ring isomorphism e satisfies (conditions):

1. x ∈ 𝒜 i → e x ∈ ℬ i
2. x ∈ 𝒜 i ↔ e x ∈ ℬ i

With the full list of assumptions (1, 2, 3, 4), conditions 1 and 2 are equivalent, so we should only ask for condition 1. So now there are two ways to set it up:

1. Require assumption 1 for GradedRingEquiv, and then delay 2, 3, 4 as much as possible.
2. Require assumptions 1, 2, 3, 4 for GradedRingEquiv.

It might seem stupid at first to not assume GradedRing for GradedRingEquiv, but notice that docs#RingEquiv also only assumes Mul and Add.

[Kenny Lau]

Kenny Lau said:

1. delay 2, 3, 4 as much as possible

note that it's basically only possible to define refl and trans, so 2 3 4 will be assumed very early in the file

[Eric Wieser]

I assume you did not mean for the two conditions to be the same?

[Aaron Liu]

there's an imp and there's an iff

[Aaron Liu]

not sure if these are the same under certain assumptions

[Kenny Lau]

they're the same when we have graded ring on both sides

[Kenny Lau]

(otherwise they're just random submodules)

[Eric Wieser]

I think you you use all four assumptions and the weaker condition

[Kenny Lau]

@Eric Wieser interesting, I went with the other approach in #30379 since I thought that would lessen the burden on typeclass searching, but as I remarked earlier, I ended up assuming 1, 2, 3, 4 as soon as Line 68.

[Eric Wieser]

That probably increases the burden because the typeclasses can't be immediately unified

[Eric Wieser]

But most importantly I claim the definition is just wrong if you can't define symm at the same level of generality as the definition

[Kenny Lau]

@Eric Wieser i've updated #30379 to use your suggested approach