feat(group_theory/group_action): add a few instances (#10310)

* regular and opposite regular actions of a group on itself are transitive;
* the action of a group on an orbit is transitive.

Author: urkud

src/algebra/opposites.lean

@@ -286,6 +286,12 @@ instance _root_.has_mul.to_has_opposite_scalar [has_mul α] : has_scalar (opposi
 
 @[simp] lemma op_smul_eq_mul [has_mul α] {a a' : α} : op a • a' = a' * a := rfl
 
+-- TODO: add an additive version once we have additive opposites
+/-- The right regular action of a group on itself is transitive. -/
+instance _root_.mul_action.opposite_regular.is_pretransitive {G : Type*} [group G] :
+  mul_action.is_pretransitive Gᵒᵖ G :=
+⟨λ x y, ⟨op (x⁻¹ * y), mul_inv_cancel_left _ _⟩⟩
+
 instance _root_.semigroup.opposite_smul_comm_class [semigroup α] :
   smul_comm_class (opposite α) α α :=
 { smul_comm := λ x y z, (mul_assoc _ _ _) }

src/group_theory/group_action/basic.lean

@@ -97,40 +97,12 @@ def stabilizer.submonoid (b : β) : submonoid α :=
 @[simp, to_additive] lemma mem_stabilizer_submonoid_iff {b : β} {a : α} :
   a ∈ stabilizer.submonoid α b ↔ a • b = b := iff.rfl
 
-variables (α β)
-/-- `α` acts pretransitively on `β` if for any `x y` there is `g` such that `g • x = y`.
-  A transitive action should furthermore have `β` nonempty. -/
-class is_pretransitive : Prop :=
-(exists_smul_eq : ∀ x y : β, ∃ g : α, g • x = y)
-
-variables {β}
-
-lemma exists_smul_eq [is_pretransitive α β] (x y : β) :
-  ∃ m : α, m • x = y := is_pretransitive.exists_smul_eq x y
-
-lemma surjective_smul [is_pretransitive α β] (x : β) :
-  surjective (λ c : α, c • x) :=
-exists_smul_eq α x
-
-lemma orbit_eq_univ [is_pretransitive α β] (x : β) :
+@[to_additive] lemma orbit_eq_univ [is_pretransitive α β] (x : β) :
   orbit α x = set.univ :=
 (surjective_smul α x).range_eq
 
 end mul_action
 
-namespace add_action
-variables (α β) [add_monoid α] [add_action α β]
-
-/-- `α` acts pretransitively on `β` if for any `x y` there is `g` such that `g +ᵥ x = y`.
-  A transitive action should furthermore have `β` nonempty. -/
-class is_pretransitive : Prop :=
-(exists_vadd_eq : ∀ x y : β, ∃ g : α, g +ᵥ x = y)
-
-attribute [to_additive] mul_action.is_pretransitive mul_action.exists_smul_eq
-  mul_action.surjective_smul mul_action.orbit_eq_univ
-
-end add_action
-
 namespace mul_action
 variable (α)
 variables [group α] [mul_action α β]
@@ -159,6 +131,11 @@ variables {α} {β}
   calc orbit α b = orbit α (a⁻¹ • a • b) : by rw inv_smul_smul
              ... ⊆ orbit α (a • b)       : orbit_smul_subset _ _
 
+/-- The action of a group on an orbit is transitive. -/
+@[to_additive "The action of an additive group on an orbit is transitive."]
+instance (x : β) : is_pretransitive α (orbit α x) :=
+⟨by { rintro ⟨_, a, rfl⟩ ⟨_, b, rfl⟩, use b * a⁻¹, ext1, simp [mul_smul] }⟩
+
 @[to_additive] lemma orbit_eq_iff {a b : β} :
    orbit α a = orbit α b ↔ a ∈ orbit α b:=
 ⟨λ h, h ▸ mem_orbit_self _, λ ⟨c, hc⟩, hc ▸ orbit_smul _ _⟩

src/group_theory/group_action/defs.lean

@@ -22,7 +22,8 @@ notation classes `has_scalar` and its additive version `has_vadd`:
 
 The hierarchy is extended further by `module`, defined elsewhere.
 
-Also provided are type-classes regarding the interaction of different group actions,
+Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the
+interaction of different group actions,
 
 * `smul_comm_class M N α` and its additive version `vadd_comm_class M N α`;
 * `is_scalar_tower M N α` (no additive version).
@@ -46,6 +47,10 @@ variables {M N G A B α β γ : Type*}
 
 open function
 
+/-!
+### Faithful actions
+-/
+
 /-- Typeclass for faithful actions. -/
 class has_faithful_vadd (G : Type*) (P : Type*) [has_vadd G P] : Prop :=
 (eq_of_vadd_eq_vadd : ∀ {g₁ g₂ : G}, (∀ p : P, g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂)
@@ -79,6 +84,47 @@ class mul_action (α : Type*) (β : Type*) [monoid α] extends has_scalar α β
 (one_smul : ∀ b : β, (1 : α) • b = b)
 (mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b)
 
+/-!
+### (Pre)transitive action
+
+`M` acts pretransitively on `α` if for any `x y` there is `g` such that `g • x = y` (or `g +ᵥ x = y`
+for an additive action). A transitive action should furthermore have `α` nonempty.
+
+In this section we define typeclasses `mul_action.is_pretransitive` and
+`add_action.is_pretransitive` and provide `mul_action.exists_smul_eq`/`add_action.exists_vadd_eq`,
+`mul_action.surjective_smul`/`add_action.surjective_vadd` as public interface to access this
+property. We do not provide typeclasses `*_action.is_transitive`; users should assume
+`[mul_action.is_pretransitive M α] [nonempty α]` instead. -/
+
+/-- `M` acts pretransitively on `α` if for any `x y` there is `g` such that `g +ᵥ x = y`.
+  A transitive action should furthermore have `α` nonempty. -/
+class add_action.is_pretransitive (M α : Type*) [has_vadd M α] : Prop :=
+(exists_vadd_eq : ∀ x y : α, ∃ g : M, g +ᵥ x = y)
+
+/-- `M` acts pretransitively on `α` if for any `x y` there is `g` such that `g • x = y`.
+  A transitive action should furthermore have `α` nonempty. -/
+@[to_additive] class mul_action.is_pretransitive (M α : Type*) [has_scalar M α] : Prop :=
+(exists_smul_eq : ∀ x y : α, ∃ g : M, g • x = y)
+
+namespace mul_action
+
+variables (M) {α} [has_scalar M α] [is_pretransitive M α]
+
+@[to_additive] lemma exists_smul_eq (x y : α) : ∃ m : M, m • x = y :=
+is_pretransitive.exists_smul_eq x y
+
+@[to_additive] lemma surjective_smul (x : α) : surjective (λ c : M, c • x) := exists_smul_eq M x
+
+/-- The regular action of a group on itself is transitive. -/
+@[to_additive] instance regular.is_pretransitive [group G] : is_pretransitive G G :=
+⟨λ x y, ⟨y * x⁻¹, inv_mul_cancel_right _ _⟩⟩
+
+end mul_action
+
+/-!
+### Scalar tower and commuting actions
+-/
+
 /-- A typeclass mixin saying that two additive actions on the same space commute. -/
 class vadd_comm_class (M N α : Type*) [has_vadd M α] [has_vadd N α] : Prop :=
 (vadd_comm : ∀ (m : M) (n : N) (a : α), m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a))