## Stream: Is there code for X?

### Topic: transitive group action

#### David Wärn (Apr 01 2021 at 10:14):

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

#### Kevin Buzzard (Apr 01 2021 at 10:16):

What does that mean?

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

#### Eric Wieser (Apr 01 2021 at 11:17):

What does that mean as a lean theorem statement?

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

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

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


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

#### Yury G. Kudryashov (Apr 01 2021 at 14:28):

BTW, this pr is awaiting review

#### Johan Commelin (Apr 01 2021 at 14:29):

Sorry, which PR number?

#6914

#### Johan Commelin (Apr 01 2021 at 14:31):

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

#### Johan Commelin (Apr 01 2021 at 14:31):

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

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