Zulip Chat Archive

Stream: Is there code for X?

Topic: transitive group action


view this post on Zulip David Wärn (Apr 01 2021 at 10:14):

Is there a typeclass expressing that a docs#mul_action is transitive?

view this post on Zulip Kevin Buzzard (Apr 01 2021 at 10:16):

What does that mean?

view this post on Zulip Kevin Buzzard (Apr 01 2021 at 10:16):

Oh -- just has one orbit? I don't think there is! This is a completely different usage of the word transitive to the equivalence relation usage, right? (I agree it's standard though, I was just temporarily confused by this)

view this post on Zulip Eric Wieser (Apr 01 2021 at 11:17):

What does that mean as a lean theorem statement?

view this post on Zulip Eric Wieser (Apr 01 2021 at 11:21):

From the wikipedia page, we have "sharply transitive" as docs#add_torsor (swapping the + symbol for *). Yury has a PR that unifies the * and + versions of these things

view this post on Zulip Eric Wieser (Apr 01 2021 at 11:23):

Since @Yury G. Kudryashov's PR makes the analogy between and +ᵥ, should we introduce a •⁻¹ to parallel -ᵥ?

view this post on Zulip Kevin Buzzard (Apr 01 2021 at 11:52):

import group_theory.group_action.defs

variables (M S : Type*) [monoid M] [mul_action M S]

def is_transitive : Prop :=
 (s t : S),  (m : M), m  s = t

def is_torsor [nonempty S] : Prop :=
 (s t : S), ∃! (m : M), m  s = t

view this post on Zulip Kevin Buzzard (Apr 01 2021 at 11:57):

Now fix some s : S (by nonemptiness) and you can prove that m : M has an inverse by considering the unique term of type M which bubs m • s back to s and using uniqueness. The "exists unique" thing is a nonconstructive (multiplicative) version of vsub.

view this post on Zulip Yury G. Kudryashov (Apr 01 2021 at 14:28):

BTW, this pr is awaiting review

view this post on Zulip Johan Commelin (Apr 01 2021 at 14:29):

Sorry, which PR number?

view this post on Zulip Eric Wieser (Apr 01 2021 at 14:29):

#6914

view this post on Zulip Johan Commelin (Apr 01 2021 at 14:31):

Ooh, that looks like a nice refactor! Sorry, I had missed it before

view this post on Zulip Johan Commelin (Apr 01 2021 at 14:31):

Eric just left a question, but otherwise: LGTM from me

view this post on Zulip Eric Wieser (Apr 01 2021 at 14:32):

I think I was waiting for a merge with master and forgot about it


Last updated: May 19 2021 at 02:10 UTC