Quotient by MulAction and transitivity

Stream: Is there code for X?

[Christian Merten]

I did not find that given a group G acting on a non-empty type α, the action is transitive if and only if the quotient by the action has exactly one element, i.e.

import Mathlib

variable (G : Type*) [Group G] (α : Type*) [MulAction G α]

lemma MulAction.pretransitive_iff_subsingleton_quotient :
    MulAction.IsPretransitive G α ↔ Subsingleton (MulAction.orbitRel.Quotient G α) := by
  constructor
  · intro _
    refine ⟨fun a b ↦ Quot.inductionOn a (fun x ↦ ?_)⟩
    exact Quot.inductionOn b (fun y ↦ Quot.sound <| MulAction.exists_smul_eq G y x)
  · intro _
    refine ⟨fun a b ↦ ?_⟩
    have h : Quotient.mk (MulAction.orbitRel G α) b = ⟦a⟧ := Subsingleton.elim _ _
    exact Quotient.eq_rel.mp h

lemma MulAction.pretransitive_iff_unique_quotient_of_nonempty [Nonempty α] :
    MulAction.IsPretransitive G α ↔ Nonempty (Unique <| MulAction.orbitRel.Quotient G α) := by
  rw [unique_iff_subsingleton_and_nonempty, MulAction.pretransitive_iff_subsingleton_quotient]
  simp only [iff_self_and]
  exact fun _ ↦ (nonempty_quotient_iff _).mpr inferInstance

Did I miss something? If not, should this be somewhere? If yes, where? docs#Mathlib.GroupTheory.GroupAction.Basic is already quite long.

[Kevin Buzzard]

Is the action of G on the empty set transitive? This is just a matter of definitions, but 1 is not prime and the empty set is not connected, I was wondering if it was one of those situations. If it's not (and if there's a notion of being pretransitive like we have preprime and preconnected) then you don't need the nonempty assumption :-)

[Christian Merten]

Yes, there is IsPretransitive and no, I would say the action of G on the empty set is not transitive. That's why there are two versions: The first one is: the action is pretransitive iff the quotient is a subsingleton and the second one is: the action is transitive iff the quotient is a singleton.

[Christian Merten]

I guess I could make the Nonempty assumption part of the left hand side of the equivalence in the second lemma, but I have the impression that this makes applications more annoying.

[Christian Merten]

(there is no Transitive typeclass)

[Kevin Buzzard]

Oh nice! I didn't actually look at the code at all, I was just commenting on the text you wrote :-) Now I see that indeed there is a concept of pretransitive :-)