Complements to pretransitive actions

When f : X →ₑ[φ] Y is an equivariant map with respect to a map of monoids φ: M → N,

• MulAction.IsPretransitive.of_surjective_map shows that the action of N on Y is pretransitive if that of M on X is pretransitive.

• MulAction.isPretransitive_congr shows that when φ is surjective, the action of N on Y is pretransitive iff that of M on X is pretransitive.

Given MulAction G X where G is a group,

• MulAction.isPretransitive_iff_base G a shows that IsPretransitive G X iff every element is translated from a

• MulAction.isPretransitive_iff_orbit_eq_univ G a shows that MulAction.IsPretransitive G X iff MulAction.orbit G a is full.

theorem MulAction.isPretransitive_iff_base {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (a : X) : IsPretransitive G X ↔ ∀ (x : X), ∃ (g : G), g • a = x

An action of a group is pretransitive iff any element can be moved from a fixed given one.

theorem AddAction.isPretransitive_iff_base {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] (a : X) : IsPretransitive G X ↔ ∀ (x : X), ∃ (g : G), g +ᵥ a = x

An additive action of an additive group is pretransitive iff any element can be moved from a fixed given one.

theorem MulAction.isPretransitive_iff_orbit_eq_univ {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (a : X) : IsPretransitive G X ↔ orbit G a = Set.univ

An action of a group is pretransitive iff the orbit of every given element is full

theorem AddAction.isPretransitive_iff_orbit_eq_univ {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] (a : X) : IsPretransitive G X ↔ orbit G a = Set.univ

An action of a group is pretransitive iff the orbit of every given element is full

theorem MulAction.IsPretransitive.of_surjective_map {M : Type u_3} {N : Type u_4} {α : Type u_5} {β : Type u_6} [Monoid M] [Monoid N] [MulAction M α] [MulAction N β] {φ : M → N} {f : α →ₑ[φ] β} (hf : Function.Surjective ⇑f) (h : IsPretransitive M α) : IsPretransitive N β

theorem AddAction.IsPretransitive.of_surjective_map {M : Type u_3} {N : Type u_4} {α : Type u_5} {β : Type u_6} [AddMonoid M] [AddMonoid N] [AddAction M α] [AddAction N β] {φ : M → N} {f : α →ₑ[φ] β} (hf : Function.Surjective ⇑f) (h : IsPretransitive M α) : IsPretransitive N β

theorem MulAction.isPretransitive_congr {M : Type u_3} {N : Type u_4} {α : Type u_5} {β : Type u_6} [Monoid M] [Monoid N] [MulAction M α] [MulAction N β] {φ : M → N} {f : α →ₑ[φ] β} (hφ : Function.Surjective φ) (hf : Function.Bijective ⇑f) : IsPretransitive M α ↔ IsPretransitive N β

theorem AddAction.isPretransitive_congr {M : Type u_3} {N : Type u_4} {α : Type u_5} {β : Type u_6} [AddMonoid M] [AddMonoid N] [AddAction M α] [AddAction N β] {φ : M → N} {f : α →ₑ[φ] β} (hφ : Function.Surjective φ) (hf : Function.Bijective ⇑f) : IsPretransitive M α ↔ IsPretransitive N β