Mathlib.Algebra.Group.Action.Pretransitive

Module docstring

{"# 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. ","### Additive, Multiplicative "}

AddAction.IsPretransitive structure

(M α : Type*) [VAdd M α]

Full source

/-- `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 AddAction.IsPretransitive (M α : Type*) [VAdd M α] : Prop where
  /-- There is `g` such that `g +ᵥ x = y`. -/
  exists_vadd_eq : ∀ x y : α, ∃ g : M, g +ᵥ x = y

Pretransitive additive action

Informal description

An additive action of a type `M` on a type `α` is called *pretransitive* if for any two elements `x` and `y` in `α`, there exists an element `g` in `M` such that `g +ᵥ x = y`. Here, `+ᵥ` denotes the additive action of `M` on `α`. A transitive action additionally requires `α` to be nonempty.

MulAction.IsPretransitive structure

(M α : Type*) [SMul M α]

Full source

/-- `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 MulAction.IsPretransitive (M α : Type*) [SMul M α] : Prop where
  /-- There is `g` such that `g • x = y`. -/
  exists_smul_eq : ∀ x y : α, ∃ g : M, g • x = y

Pretransitive group action

Informal description

A group action of $ M $ on $ \alpha $ is called *pretransitive* if for any two elements $ x, y \in \alpha $, there exists an element $ g \in M $ such that $ g \cdot x = y $. A *transitive* action further requires that $ \alpha $ is nonempty.

MulAction.exists_smul_eq theorem

(x y : α) : ∃ m : M, m • x = y

Full source

@[to_additive]
lemma exists_smul_eq (x y : α) : ∃ m : M, m • x = y := IsPretransitive.exists_smul_eq x y

Existence of Group Action Element Mapping $x$ to $y$ in Pretransitive Action

Informal description

For any two elements $x, y$ in a type $\alpha$ with a pretransitive group action by $M$, there exists an element $m \in M$ such that $m \cdot x = y$.

MulAction.surjective_smul theorem

(x : α) : Surjective fun c : M ↦ c • x

Full source

@[to_additive]
lemma surjective_smul (x : α) : Surjective fun c : M ↦ c • x := exists_smul_eq M x

Surjectivity of the Group Action Map $c \mapsto c \cdot x$ in Pretransitive Actions

Informal description

For any element $x$ in a type $\alpha$ with a pretransitive group action by $M$, the function $c \mapsto c \cdot x$ from $M$ to $\alpha$ is surjective. That is, for every $y \in \alpha$, there exists some $c \in M$ such that $c \cdot x = y$.

MulAction.Regular.isPretransitive instance

[Group G] : IsPretransitive G G

Full source

/-- The left regular action of a group on itself is transitive. -/
@[to_additive "The regular action of a group on itself is transitive."]
instance Regular.isPretransitive [Group G] : IsPretransitive G G :=
  ⟨fun x y ↦ ⟨y * x⁻¹, inv_mul_cancel_right _ _⟩⟩

Transitivity of the Left Regular Group Action

Informal description

For any group $G$, the left regular action of $G$ on itself is pretransitive. That is, for any two elements $x, y \in G$, there exists an element $g \in G$ such that $g \cdot x = y$.

MulAction.Regular.isPretransitive_mulOpposite instance

[Group G] : IsPretransitive Gᵐᵒᵖ G

Full source

/-- The right regular action of a group on itself is transitive. -/
@[to_additive "The right regular action of an additive group on itself is transitive."]
instance Regular.isPretransitive_mulOpposite [Group G] : IsPretransitive Gᵐᵒᵖ G :=
  ⟨fun x y ↦ ⟨.op (x⁻¹ * y), mul_inv_cancel_left _ _⟩⟩

Transitivity of the Right Regular Group Action

Informal description

For any group $G$, the right regular action of $G$ on itself is pretransitive. That is, for any two elements $x, y \in G$, there exists an element $g \in G$ such that $x \cdot g = y$.

MulAction.IsPretransitive.of_smul_eq theorem

 {M N α : Type*} [SMul M α] [SMul N α] [IsPretransitive M α] (f : M → N) (hf : ∀ {c : M} {x : α}, f c • x = c • x) :
  IsPretransitive N α

Full source

@[to_additive]
lemma IsPretransitive.of_smul_eq {M N α : Type*} [SMul M α] [SMul N α] [IsPretransitive M α]
    (f : M → N) (hf : ∀ {c : M} {x : α}, f c • x = c • x) : IsPretransitive N α where
  exists_smul_eq x y := (exists_smul_eq x y).elim fun m h ↦ ⟨f m, hf.trans h⟩

Pretransitivity Preservation Under Scalar Action Equivalence

Informal description

Let $M$ and $N$ be types with scalar multiplication actions on a type $\alpha$. If the action of $M$ on $\alpha$ is pretransitive and there exists a function $f: M \to N$ such that for all $c \in M$ and $x \in \alpha$, we have $f(c) \cdot x = c \cdot x$, then the action of $N$ on $\alpha$ is also pretransitive.

MulAction.IsPretransitive.of_isScalarTower theorem

 (M : Type*) {N α : Type*} [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α]
  [IsPretransitive M α] : IsPretransitive N α

Full source

@[to_additive]
lemma MulAction.IsPretransitive.of_isScalarTower (M : Type*) {N α : Type*} [Monoid N] [SMul M N]
    [MulAction N α] [SMul M α] [IsScalarTower M N α] [IsPretransitive M α] : IsPretransitive N α :=
  of_smul_eq (fun x : M ↦ x • 1) (smul_one_smul N _ _)

Pretransitivity via Scalar Tower Condition

Informal description

Let $M$, $N$, and $\alpha$ be types, where $N$ is a monoid with a scalar multiplication action on $\alpha$, and $M$ has a scalar multiplication action on both $N$ and $\alpha$. If the action of $M$ on $\alpha$ is pretransitive and the actions form a scalar tower (i.e., for all $m \in M$, $n \in N$, and $x \in \alpha$, we have $m \cdot (n \cdot x) = (m \cdot n) \cdot x$), then the action of $N$ on $\alpha$ is also pretransitive.

Additive.addAction_isPretransitive instance

[Monoid α] [MulAction α β] [MulAction.IsPretransitive α β] : AddAction.IsPretransitive (Additive α) β

Full source

instance Additive.addAction_isPretransitive [Monoid α] [MulAction α β]
    [MulAction.IsPretransitive α β] : AddAction.IsPretransitive (Additive α) β :=
  ⟨@MulAction.exists_smul_eq α _ _ _⟩

Pretransitive Action via Additive Monoid

Informal description

For any monoid $\alpha$ acting pretransitively on a type $\beta$ via multiplicative action, the additive monoid $\text{Additive}\,\alpha$ also acts pretransitively on $\beta$ via additive action.

Multiplicative.mulAction_isPretransitive instance

[AddMonoid α] [AddAction α β] [AddAction.IsPretransitive α β] : MulAction.IsPretransitive (Multiplicative α) β

Full source

instance Multiplicative.mulAction_isPretransitive [AddMonoid α] [AddAction α β]
    [AddAction.IsPretransitive α β] : MulAction.IsPretransitive (Multiplicative α) β :=
  ⟨@AddAction.exists_vadd_eq α _ _ _⟩

Pretransitive Action via Multiplicative Monoid

Informal description

For any additive monoid $\alpha$ acting pretransitively on a type $\beta$, the multiplicative monoid $\text{Multiplicative}\,\alpha$ also acts pretransitively on $\beta$.