Zulip Chat Archive

Stream: maths

Topic: has_scalar for monoid actions


view this post on Zulip Johan Commelin (Mar 21 2019 at 09:48):

Is there a reason why we are not using to denote monoid/group actions?

view this post on Zulip Johan Commelin (Mar 21 2019 at 14:56):

Please take a look at the last line of 6.20 on page 50 of http://math.stanford.edu/~conrad/Perfseminar/refs/wedhornadic.pdf

view this post on Zulip Johan Commelin (Mar 21 2019 at 14:57):

There is a calculation that involves taking products of sets and subgroups

view this post on Zulip Johan Commelin (Mar 21 2019 at 14:57):

s • G is defined as add_group.closure {x | ∃ (r ∈ s) (g ∈ G), x = r g}.

view this post on Zulip Johan Commelin (Mar 21 2019 at 14:58):

This calculation becomes completely unreadable without the correct notation and framework.

view this post on Zulip Johan Commelin (Mar 22 2019 at 18:37):

I would appreciate if people could review this patch:
https://github.com/leanprover-community/mathlib/commit/02baf145de6a796bd0b946caf7735f416330b854

I introduce notation for monoid/group actions, and refactor sylow.lean which is the only place where group actions are used.
It seems to work quite nicely in the two files that I edited. However... for some reason that I really don't understand, it is now no longer possible to coerce from units int to an arbitrary ring. And this is causing breakage in determinant.lean. I have no clue why this coercion is affected...

view this post on Zulip Johan Commelin (Mar 22 2019 at 20:46):

@Chris Hughes @Kenny Lau Do you have a clue what is the cause of the breakage?

view this post on Zulip Chris Hughes (Mar 22 2019 at 20:46):

No, but I have had the same problem with code I wrote affecting that coercion.

view this post on Zulip Johan Commelin (Mar 22 2019 at 20:47):

Was it related code?

view this post on Zulip Johan Commelin (Mar 22 2019 at 20:48):

It would be sad if we have to make that coercion explicit... Otoh, it isn't too much trouble to make determinant.lean a bit less fragile.

view this post on Zulip Chris Hughes (Mar 22 2019 at 20:48):

I just ended up import group_theory/subgroup or something into that file, which broke it.

view this post on Zulip Chris Hughes (Mar 22 2019 at 20:49):

Is algebra/module the only thing that has changed that is imported by determinant?

view this post on Zulip Johan Commelin (Mar 22 2019 at 20:49):

I think so. algebra.module now imports group_action because of the notation.

view this post on Zulip Johan Commelin (Mar 22 2019 at 20:50):

I could put that notation in a separate file... but I was planning on making module extend monoid_action by definition... so that would only be a temporary fix.

view this post on Zulip Chris Hughes (Mar 22 2019 at 20:50):

You could dump it in algebra/group. It's not really a long term fix.

view this post on Zulip Johan Commelin (Mar 22 2019 at 20:51):

@Mario Carneiro Do you know how to make these thing play nice together?

view this post on Zulip Chris Hughes (Mar 22 2019 at 20:55):

FYI the coe that breaks is from units int to a ring.

view this post on Zulip Mario Carneiro (Mar 22 2019 at 21:06):

what if you put an intermediate type ascription to int?

view this post on Zulip Johan Commelin (Mar 22 2019 at 21:08):

Doesn't fix it )-;

view this post on Zulip Chris Hughes (Mar 22 2019 at 22:23):

It works for me.

view this post on Zulip Johan Commelin (Mar 23 2019 at 07:15):

Hmm, maybe what I tried was to recreate the coercion with that intermediate type ascription...
Anyway, if you say it worked for you, I'll try to follow that approach. It's likely the best way forward.

view this post on Zulip Kevin Buzzard (Mar 23 2019 at 09:19):

What is an intermediate type ascription?

view this post on Zulip Mario Carneiro (Mar 23 2019 at 09:37):

if x : A and you want a C and you write (x : B)

view this post on Zulip Patrick Massot (Mar 23 2019 at 11:40):

As a small contribution to this discussion, I pushed https://github.com/leanprover-community/mathlib/commit/0d92ca165e83f0d37f9e2c42ac9510c258113526 It fixes the file determinant.lean by pushing all coercions into a local notation (which improves readability anyway). I'm not saying this is perfect, but I like it so far

view this post on Zulip Patrick Massot (Mar 23 2019 at 11:43):

Don't worry about the Travis fail, I realized while reading the diff on GitHub that I missed one coercion to remove, so I forced pushed and amended commit

view this post on Zulip Patrick Massot (Mar 23 2019 at 11:51):

Oh, you didn't say dimension.lean was also broken. Hence the Travis fail

view this post on Zulip Patrick Massot (Mar 23 2019 at 11:59):

I fixed that one https://github.com/leanprover-community/mathlib/commit/84ed310358a818b9b779e18ff81ee07f17c94af7 We'll see what Travis has to say during my lunch

view this post on Zulip Johan Commelin (Mar 23 2019 at 12:04):

I stopped the compile after two screen fills of breakage in determinant.lean. There might well be more breakage.

view this post on Zulip Johan Commelin (Mar 23 2019 at 12:05):

Thanks for contributing @Patrick Massot I really like what you've done.

view this post on Zulip Johan Commelin (Mar 23 2019 at 12:06):

If this passes Travis, I think we can PR it.

view this post on Zulip Johan Commelin (Mar 23 2019 at 12:07):

One thing I realised is that almost all instances of has_pow are also monoid/group actions... I don't know if/how we should unify that...

view this post on Zulip Johan Commelin (Mar 23 2019 at 12:07):

But maybe that is an issue for another time.

view this post on Zulip Patrick Massot (Mar 23 2019 at 12:56):

Travis is happy

view this post on Zulip Patrick Massot (Mar 23 2019 at 13:02):

Globally, I think it's a good idea not to type or . If Lean needs them then an explicit type ascription is probably much better for readability and maintenance. I think the case of is a bit different because there probably less ambiguity

view this post on Zulip Johan Commelin (Mar 23 2019 at 13:07):

@Patrick Massot Do you agree that we can PR this? Or would you want to add other stuff?

view this post on Zulip Johan Commelin (Mar 23 2019 at 14:17):

Done #846


Last updated: May 14 2021 at 19:21 UTC