Zulip Chat Archive

Stream: general

Topic: Eckmann–Hilton

Johan Commelin (Sep 07 2018 at 08:07):

Today I thought it was a good idea to stretch the type class system a bit. In fact, I ended up not using it at all :rolling_on_the_floor_laughing:
https://gist.github.com/jcommelin/2e031b5446ca54089576ea9f66f12abf
Statement: Two unital binary operations that distribute over each other are in fact one and the same. Also, they are commutative and associative, so in fact a monoid structure.
This is used to prove that homotopy groups are abelian.

Johan Commelin (Sep 07 2018 at 08:07):

Any comments are welcome.

Johan Commelin (Sep 07 2018 at 08:08):

In particular, feel free to shoehorn this into the type class system.
Golfing is appreciated.

Johan Commelin (Sep 07 2018 at 08:13):

@Reid Barton Did you already have this somewhere in your repo?

Reid Barton (Sep 07 2018 at 08:13):

Nope I hadn't gotten that far. Cool!

Reid Barton (Sep 07 2018 at 08:15):

local notation a ` `m` ` b := @has_mul.mul X m a b

Does this really work? Also, it doesn't work for me. :)

Reid Barton (Sep 07 2018 at 08:17):

Oh nice. Copy and paste from github (even the raw page) doesn't preserve the source text correctly.

Reid Barton (Sep 07 2018 at 08:18):

Maybe you could choose something less sneaky like local notation a `<`m`>` b := @has_mul.mul X m a b

Johan Commelin (Sep 07 2018 at 08:21):

Hmm, maybe I should.

Johan Commelin (Sep 07 2018 at 08:21):

But those are non-breaking spaces.

Johan Commelin (Sep 07 2018 at 08:24):

Hmmm... that's really nasty of GitHub.

Johan Commelin (Sep 07 2018 at 08:24):

They should know better.

Johan Commelin (Sep 07 2018 at 08:24):

I'll use fishhooks, like you suggested.

Reid Barton (Sep 07 2018 at 08:24):

Somehow when I pasted the source into emacs, they turned into regular spaces.
Not sure whether github or firefox or emacs is to blame

Johan Commelin (Sep 07 2018 at 08:26):

Ok, fair enough.

Johan Commelin (Sep 07 2018 at 08:26):

Anyway, it is fixed now.

Reid Barton (Sep 07 2018 at 08:35):

Haha, Lean prints both mul operations as *. It knows!!

Johan Commelin (Sep 07 2018 at 08:38):

Yes! I thought that was hilarious :rolling_on_the_floor_laughing:

Johan Commelin (Sep 07 2018 at 10:16):

@Mario Carneiro @Johannes Hölzl What would be the proper place for this in mathlib? Somewhere in group_theory?

Johan Commelin (Sep 10 2018 at 19:44):

PR'd this: https://github.com/leanprover/mathlib/pull/335

Last updated: Dec 20 2023 at 11:08 UTC