## Stream: maths

### Topic: has_scalar for monoid actions

#### Johan Commelin (Mar 21 2019 at 09:48):

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

#### Johan Commelin (Mar 21 2019 at 14:57):

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

#### Johan Commelin (Mar 21 2019 at 14:57):

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

#### Johan Commelin (Mar 21 2019 at 14:58):

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

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

#### Johan Commelin (Mar 22 2019 at 20:46):

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

#### Chris Hughes (Mar 22 2019 at 20:46):

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

#### Johan Commelin (Mar 22 2019 at 20:47):

Was it related code?

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

#### Chris Hughes (Mar 22 2019 at 20:48):

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

#### Chris Hughes (Mar 22 2019 at 20:49):

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

#### Johan Commelin (Mar 22 2019 at 20:49):

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

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

#### Chris Hughes (Mar 22 2019 at 20:50):

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

#### Johan Commelin (Mar 22 2019 at 20:51):

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

#### Chris Hughes (Mar 22 2019 at 20:55):

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

#### Mario Carneiro (Mar 22 2019 at 21:06):

what if you put an intermediate type ascription to int?

#### Johan Commelin (Mar 22 2019 at 21:08):

Doesn't fix it )-;

It works for me.

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

#### Kevin Buzzard (Mar 23 2019 at 09:19):

What is an intermediate type ascription?

#### Mario Carneiro (Mar 23 2019 at 09:37):

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

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

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

#### Patrick Massot (Mar 23 2019 at 11:51):

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

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

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

#### Johan Commelin (Mar 23 2019 at 12:05):

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

#### Johan Commelin (Mar 23 2019 at 12:06):

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

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

#### Johan Commelin (Mar 23 2019 at 12:07):

But maybe that is an issue for another time.

Travis is happy

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

#### 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?

#### Johan Commelin (Mar 23 2019 at 14:17):

Done #846

Last updated: May 14 2021 at 19:21 UTC