has_scalar for monoid actions

Stream: maths

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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...

[Johan Commelin]

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

[Chris Hughes]

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

[Johan Commelin]

Was it related code?

[Johan Commelin]

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.

[Chris Hughes]

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

[Chris Hughes]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Chris Hughes]

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

[Johan Commelin]

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

[Chris Hughes]

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

[Mario Carneiro]

what if you put an intermediate type ascription to int?

[Johan Commelin]

Doesn't fix it )-;

[Chris Hughes]

It works for me.

[Johan Commelin]

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.

[Kevin Buzzard]

What is an intermediate type ascription?

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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...

[Johan Commelin]

But maybe that is an issue for another time.

[Patrick Massot]

Travis is happy

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

Done #846