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_5) (α : Type u_6) [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.

Instances

• AddAction.Regular.isPretransitive
• AddAction.Regular.isPretransitive_addOpposite
• AddAction.instIsPretransitiveElemOrbit
• AddAction.instIsPretransitiveElemOrbit_1
• AddAction.instIsPretransitiveOfSubsingleton
• AddAction.isPretransitive_quotient
• Additive.addAction_isPretransitive
• SeparationQuotient.instIsPretransitiveVAdd

class MulAction.IsPretransitive (M : Type u_5) (α : Type u_6) [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.

Instances

• MulAction.Regular.isPretransitive
• MulAction.Regular.isPretransitive_mulOpposite
• MulAction.instIsPretransitiveElemOrbit
• MulAction.instIsPretransitiveElemOrbit_1
• MulAction.instIsPretransitiveOfSubsingleton
• MulAction.isPretransitive_quotient
• Multiplicative.mulAction_isPretransitive
• SeparationQuotient.instIsPretransitiveSMul

instance MulAction.instIsPretransitiveOfSubsingleton {M : Type u_5} {α : Type u_6} [Monoid M] [MulAction M α] [Subsingleton α] : IsPretransitive M α

instance AddAction.instIsPretransitiveOfSubsingleton {M : Type u_5} {α : Type u_6} [AddMonoid M] [AddAction M α] [Subsingleton α] : IsPretransitive M α

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

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

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

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

The regular action of a group on itself is transitive.

instance MulAction.Regular.isPretransitive_mulOpposite {G : Type u_2} [Group G] : IsPretransitive Gᵐᵒᵖ G

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

instance AddAction.Regular.isPretransitive_addOpposite {G : Type u_2} [AddGroup G] : IsPretransitive Gᵃᵒᵖ G

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 : M → N) (hf : ∀ {c : M} {x : α}, f c • x = c • x) : IsPretransitive N α

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

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 α] : IsPretransitive N α

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 α] : IsPretransitive N α

Additive, Multiplicative

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

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