TC resolution

Stream: new members

[Andre Knispel]

I'm trying to define and experiment with graded rings and I have a few issues with type classes. Here's my code:

import data.equiv.algebra
import data.polynomial
import algebra.module
import algebra.direct_sum

universes u v
variables (α : Type u) (M : Type v)
variables [add_monoid M] [decidable_eq M]

class graded_ring extends ring α :=
(pieces : M → Type u) (groups : ∀ m : M, add_comm_group (pieces m))
(iso : α ≃+ direct_sum M pieces)
(of : Π m : M, pieces m → α := λ (m : M) (r : pieces m), iso.inv_fun (direct_sum.of pieces m r))
(mul_respects_grading : ∀ (m m' : M) (r : pieces m) (r' : pieces m'),
  ∃ s : pieces (m + m'), of m r * of m' r' = of (m + m') s)

variables [comm_ring α] [r : ring α]

noncomputable instance : graded_ring (polynomial α) ℕ :=
@graded_ring.mk (polynomial α) ℕ _ _ (comm_ring.to_ring (polynomial α))
  (λ _ : ℕ, α) (λ _ : ℕ, @ring.to_add_comm_group α r) _ _ _

First, I don't understand why the ring instance of polynomial isn't found. If I make it implicit, the search tries increasingly complicated versions of dfinsupp.add_monoid before giving up. Is there a nicer way to do this, ideally so that I can use the record syntax? Second, is there a nicer way to write the commutative group instance of α?

[Scott Morrison]

There's a rule that you shouldn't use extend when adding more data to a class, if you need to have more parameters than the thing you're extending.

[Scott Morrison]

So I'd suggest you want to substantially reformulate this.

[Kevin Buzzard]

These rules are extremely hard to find unless you're a regular here.

[Kevin Buzzard]

You just get people like you, Reid or Mario saying "oh this is an antipattern" occasionally

[Kevin Buzzard]

What would be really nice would be a resource with some simple bad classes and perhaps not an explanation of why they're bad but at least a description of the rules of thumb to follow. I don't know these rules at all. I am still really bad at making definitions in Lean which is why I'm making so much fuss on another thread about exactly what the definition of yet another concept of finiteness / cardinality should be.

[Scott Morrison]

I think the problem is just that it introduces a "bad instance", because now whenever Lean wants to check if something is a ring, is has to check if it is a graded ring, and suddenly there's a metavariable for the type M introduced into the typeclass search problem.

[Kevin Buzzard]

Yeah I'm sure that if you actually understand the typeclass system (which I certainly don't) then it's all obvious. The problem is that if a mathematician beginner comes along they can write something which looks completely mathematically reasonable but is somehow impossible to use because of some issue regarding [foo X] v extends foo X

[Kevin Buzzard]

or some issue regarding universe parameters in the definition

[Kevin Buzzard]

or some issue regarding something having a different number of variables to something else

[Kevin Buzzard]

or some other issue -- these things are too numerous to mention. Classes are extremely well understood now, and the "gotchas" are all known to the experts, but whenever I want to make a new definition in Lean I run it past the Zulip chat before I do anything with it at all because I don't know all the pitfalls

[Andre Knispel]

Ah, now that I know what I'm looking for, I found the loop ring -> graded_ring -> monoid (for M) -> ... -> ring. I've looked at modules, because they should have the same issue, but the only thing I see is set_option default_priority 100. Does this make the priority for the classes there very low?

[Scott Morrison]

I don't think module is comparable, because it is not using extends like you are.

[Scott Morrison]

I would guess that you just want an additional typeclass, so you write [ring R] [graded_ring R] to summon one.

[Scott Morrison]

You might also look at src#category_theory.graded_object for the bundled version.

[Andre Knispel]

Thanks, that helped!

[Jalex Stark]

Kevin Buzzard said:

What would be really nice would be a resource with some simple bad classes and perhaps not an explanation of why they're bad but at least a description of the rules of thumb to follow. I don't know these rules at all. I am still really bad at making definitions in Lean which is why I'm making so much fuss on another thread about exactly what the definition of yet another concept of finiteness / cardinality should be.

I guess some of these rules have been implemented in code. Maybe the document you want starts out as docs for the linter?