refactor(ring_theory/ideals): avoid using type class inference for setoids in quotient rings and groups #212
Conversation
group_theory/coset.lean
Outdated
| quotient.eq' | ||
|
|
||
| lemma eq_class_eq_left_coset [group α] (s : set α) [is_subgroup s] (g : α) : | ||
| {x : α | (x : left_cosets s) = g} = left_coset g s := |
There was a problem hiding this comment.
Please indent this line
| section quotient_group | ||
|
|
||
| local attribute [instance] left_rel normal_subgroup.to_is_subgroup | ||
| namespace left_cosets | ||
|
|
||
| instance [group α] (s : set α) [normal_subgroup s] : group (left_cosets s) := |
There was a problem hiding this comment.
I'm wondering if you could shrink this instance using refine_struct (like in https://github.com/leanprover/mathlib/blob/master/algebra/pi_instances.lean)
There was a problem hiding this comment.
I gave it try, I might have a substitute proof for you in a few moments.
There was a problem hiding this comment.
Have a look at ChrisHughes24#9 and see if you find that it improves your PR.
There was a problem hiding this comment.
I'm not sure it's much of an improvement, it makes the proof harder to understand as far as I can see. I'll let the people who have to maintain it decide if it's an improvement.
There was a problem hiding this comment.
For only one proof it might not be an improvement, you're right but if you have a pattern of writing algebraic structures on quotient types, repeating the same proof over and over might not be too enlightening.
There was a problem hiding this comment.
I'm sure using refine_struct and a more or less specialize tactic is a good idea. I don't understand why Simon took the definition of mul and inv out of the initial structure, but the important part is https://github.com/cipher1024/mathlib/blob/7f14aa5c85f04645ba41fa4740e549a4efa2ca47/group_theory/coset.lean#L222-L225 which could be made into a derive_quotient_field tactic and reused in a lot of places.
There was a problem hiding this comment.
In my defence: I was feeling lazy. But more to the point, I wasn't sure how to automate the construction of those functions.
There was a problem hiding this comment.
I didn't mean those functions should be automated. Every automation is good of course, but the first targets here were clearly those repeated (λ ..., congr_arg mk (some_field ...)).
ChrisHughes24
changed the title
We shouldn't really be asking type class inference to guess which subgroup we want to quotient by, so I added a load of definitions in
data/quotwhich use unification rather than type class inference for setoids, and changed quotient groups and quotient rings to use these definitions.Also added a few proofs about ideals, which I couldn't add before because of type class inference problems.
TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list