Pretransitive group actions

This file defines a typeclass for pretransitive group actions.

Notation

• a • b is used as notation for SMul.smul a b.
• a +ᵥ b is used as notation for VAdd.vadd a b.

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_9) (α : Type u_10) [VAdd M α] : Prop

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.

theorem AddAction.IsPretransitive.exists_vadd_eq {M : Type u_9} {α : Type u_10} : ∀ {inst : VAdd M α} [self : AddAction.IsPretransitive M α] (x y : α), ∃ (g : M), g +ᵥ x = y

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

class MulAction.IsPretransitive (M : Type u_9) (α : Type u_10) [SMul M α] : Prop

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.

theorem MulAction.IsPretransitive.exists_smul_eq {M : Type u_9} {α : Type u_10} : ∀ {inst : SMul M α} [self : MulAction.IsPretransitive M α] (x y : α), ∃ (g : M), g • x = y

There is g such that g • x = y.

theorem AddAction.exists_vadd_eq (M : Type u_1) {α : Type u_5} [VAdd M α] [AddAction.IsPretransitive M α] (x : α) (y : α) : ∃ (m : M), m +ᵥ x = y

theorem MulAction.exists_smul_eq (M : Type u_1) {α : Type u_5} [SMul M α] [MulAction.IsPretransitive M α] (x : α) (y : α) : ∃ (m : M), m • x = y

theorem AddAction.surjective_vadd (M : Type u_1) {α : Type u_5} [VAdd M α] [AddAction.IsPretransitive M α] (x : α) : Function.Surjective fun (c : M) => c +ᵥ x

theorem MulAction.surjective_smul (M : Type u_1) {α : Type u_5} [SMul M α] [MulAction.IsPretransitive M α] (x : α) : Function.Surjective fun (c : M) => c • x

instance AddAction.Regular.isPretransitive {G : Type u_3} [AddGroup G] : AddAction.IsPretransitive G G

The regular action of a group on itself is transitive.

Equations

• ⋯ = ⋯

instance MulAction.Regular.isPretransitive {G : Type u_3} [Group G] : MulAction.IsPretransitive G G

The regular action of a group on itself is transitive.

Equations

• ⋯ = ⋯

theorem AddAction.isPretransitive_compHom {E : Type u_9} {F : Type u_10} {G : Type u_11} [AddMonoid E] [AddMonoid F] [AddAction F G] [AddAction.IsPretransitive F G] {f : E →+ F} (hf : Function.Surjective ⇑f) : AddAction.IsPretransitive E G

theorem MulAction.isPretransitive_compHom {E : Type u_9} {F : Type u_10} {G : Type u_11} [Monoid E] [Monoid F] [MulAction F G] [MulAction.IsPretransitive F G] {f : E →* F} (hf : Function.Surjective ⇑f) : MulAction.IsPretransitive E G

If an action is transitive, then composing this action with a surjective homomorphism gives again a transitive action.

theorem AddAction.IsPretransitive.of_vadd_eq {M : Type u_9} {N : Type u_10} {α : Type u_11} [VAdd M α] [VAdd N α] [AddAction.IsPretransitive M α] (f : M → N) (hf : ∀ {c : M} {x : α}, f c +ᵥ x = c +ᵥ x) : AddAction.IsPretransitive N α

theorem MulAction.IsPretransitive.of_smul_eq {M : Type u_9} {N : Type u_10} {α : Type u_11} [SMul M α] [SMul N α] [MulAction.IsPretransitive M α] (f : M → N) (hf : ∀ {c : M} {x : α}, f c • x = c • x) : MulAction.IsPretransitive N α

theorem AddAction.IsPretransitive.of_compHom {M : Type u_9} {N : Type u_10} {α : Type u_11} [AddMonoid M] [AddMonoid N] [AddAction N α] (f : M →+ N) [h : AddAction.IsPretransitive M α] : AddAction.IsPretransitive N α

theorem MulAction.IsPretransitive.of_compHom {M : Type u_9} {N : Type u_10} {α : Type u_11} [Monoid M] [Monoid N] [MulAction N α] (f : M →* N) [h : MulAction.IsPretransitive M α] : MulAction.IsPretransitive N α

theorem AddAction.IsPretransitive.of_isScalarTower (M : Type u_9) {N : Type u_10} {α : Type u_11} [AddMonoid N] [VAdd M N] [AddAction N α] [VAdd M α] [VAddAssocClass M N α] [AddAction.IsPretransitive M α] : AddAction.IsPretransitive N α

theorem MulAction.IsPretransitive.of_isScalarTower (M : Type u_9) {N : Type u_10} {α : Type u_11} [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] [MulAction.IsPretransitive M α] : MulAction.IsPretransitive N α

Additive, Multiplicative

instance Additive.addAction_isPretransitive {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] [MulAction.IsPretransitive α β] : AddAction.IsPretransitive (Additive α) β

Equations

• ⋯ = ⋯

instance Multiplicative.mulAction_isPretransitive {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddAction α β] [AddAction.IsPretransitive α β] : MulAction.IsPretransitive (Multiplicative α) β

Equations

• ⋯ = ⋯