transitive group action

Stream: Is there code for X?

[David Wärn]

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

[Kevin Buzzard]

What does that mean?

[Kevin Buzzard]

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]

What does that mean as a lean theorem statement?

[Eric Wieser]

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]

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

[Kevin Buzzard]

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]

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]

BTW, this pr is awaiting review

[Johan Commelin]

Sorry, which PR number?

[Eric Wieser]

#6914

[Johan Commelin]

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

[Johan Commelin]

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

[Eric Wieser]

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