Documentation

Mathlib.Algebra.Group.Action.Pretransitive

Pretransitive group actions #

This file defines a typeclass for pretransitive group actions.

Notation #

Implementation details #

This file should avoid depending on other parts of GroupTheory, to avoid import cycles. More sophisticated lemmas belong in GroupTheory.GroupAction.

Tags #

group action

(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 MulAction.IsPretransitive and AddAction.IsPretransitive and provide MulAction.exists_smul_eq/AddAction.exists_vadd_eq, MulAction.surjective_smul/AddAction.surjective_vadd as public interface to access this property. We do not provide typeclasses *Action.IsTransitive; users should assume [MulAction.IsPretransitive M α] [Nonempty α] instead.

class AddAction.IsPretransitive (M : Type u_5) (α : Type u_6) [VAdd M α] :

M acts pretransitively on α if for any x y there is g such that g +ᵥ x = y. A transitive action should furthermore have α nonempty.

  • exists_vadd_eq (x y : α) : (g : M), g +ᵥ x = y

    There is g such that g +ᵥ x = y.

Instances
class MulAction.IsPretransitive (M : Type u_5) (α : Type u_6) [SMul M α] :

M acts pretransitively on α if for any x y there is g such that g • x = y. A transitive action should furthermore have α nonempty.

  • exists_smul_eq (x y : α) : (g : M), g x = y

    There is g such that g • x = y.

Instances
theorem MulAction.exists_smul_eq (M : Type u_1) {α : Type u_3} [SMul M α] [IsPretransitive M α] (x y : α) :
(m : M), m x = y
theorem AddAction.exists_vadd_eq (M : Type u_1) {α : Type u_3} [VAdd M α] [IsPretransitive M α] (x y : α) :
(m : M), m +ᵥ x = y
theorem MulAction.surjective_smul (M : Type u_1) {α : Type u_3} [SMul M α] [IsPretransitive M α] (x : α) :
Function.Surjective fun (c : M) => c x
theorem AddAction.surjective_vadd (M : Type u_1) {α : Type u_3} [VAdd M α] [IsPretransitive M α] (x : α) :
Function.Surjective fun (c : M) => c +ᵥ x

The left regular action of a group on itself is transitive.

The regular action of a group on itself is transitive.

The right regular action of a group on itself is transitive.

The right regular action of an additive group on itself is transitive.

theorem MulAction.IsPretransitive.of_smul_eq {M : Type u_5} {N : Type u_6} {α : Type u_7} [SMul M α] [SMul N α] [IsPretransitive M α] (f : MN) (hf : ∀ {c : M} {x : α}, f c x = c x) :
theorem AddAction.IsPretransitive.of_vadd_eq {M : Type u_5} {N : Type u_6} {α : Type u_7} [VAdd M α] [VAdd N α] [IsPretransitive M α] (f : MN) (hf : ∀ {c : M} {x : α}, f c +ᵥ x = c +ᵥ x) :
theorem MulAction.IsPretransitive.of_isScalarTower (M : Type u_5) {N : Type u_6} {α : Type u_7} [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] [IsPretransitive M α] :
theorem AddAction.IsPretransitive.of_vaddAssocClass (M : Type u_5) {N : Type u_6} {α : Type u_7} [AddMonoid N] [VAdd M N] [AddAction N α] [VAdd M α] [VAddAssocClass M N α] [IsPretransitive M α] :

Additive, Multiplicative #