Zulip Chat Archive

Stream: general

Topic: Eckmann–Hilton


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:07):

Any comments are welcome.

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:08):

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

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:13):

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

view this post on Zulip Reid Barton (Sep 07 2018 at 08:13):

Nope I hadn't gotten that far. Cool!

view this post on Zulip 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. :)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:21):

Hmm, maybe I should.

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:21):

But those are non-breaking spaces.

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:24):

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

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:24):

They should know better.

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:24):

I'll use fishhooks, like you suggested.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:26):

Ok, fair enough.

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:26):

Anyway, it is fixed now.

view this post on Zulip Reid Barton (Sep 07 2018 at 08:35):

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

view this post on Zulip Johan Commelin (Sep 07 2018 at 08:38):

Yes! I thought that was hilarious :rolling_on_the_floor_laughing:

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Sep 10 2018 at 19:44):

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


Last updated: May 18 2021 at 16:25 UTC