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.

source
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
    source
    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
      source
      theorem MulAction.isPretransitive_iff (M : Type u_5) (α : Type u_6) [SMul M α] :
      IsPretransitive M α ↔ ∀ (x y : α), ∃ (g : M), g • x = y
      source
      theorem AddAction.isPretransitive_iff (M : Type u_5) (α : Type u_6) [VAdd M α] :
      IsPretransitive M α ↔ ∀ (x y : α), ∃ (g : M), g +ᵥ x = y
      source
      instance MulAction.instIsPretransitiveOfSubsingleton {M : Type u_5} {α : Type u_6} [Monoid M] [MulAction M α] [Subsingleton α] :
      IsPretransitive M α
      source
      instance AddAction.instIsPretransitiveOfSubsingleton {M : Type u_5} {α : Type u_6} [AddMonoid M] [AddAction M α] [Subsingleton α] :
      IsPretransitive M α
      source
      theorem MulAction.exists_smul_eq (M : Type u_1) {α : Type u_3} [SMul M α] [IsPretransitive M α] (x y : α) :
      ∃ (m : M), m • x = y
      source
      theorem AddAction.exists_vadd_eq (M : Type u_1) {α : Type u_3} [VAdd M α] [IsPretransitive M α] (x y : α) :
      ∃ (m : M), m +ᵥ x = y
      source
      theorem MulAction.surjective_smul (M : Type u_1) {α : Type u_3} [SMul M α] [IsPretransitive M α] (x : α) :
      Function.Surjective fun (c : M) => c • x
      source
      theorem AddAction.surjective_vadd (M : Type u_1) {α : Type u_3} [VAdd M α] [IsPretransitive M α] (x : α) :
      Function.Surjective fun (c : M) => c +ᵥ x
      source
      instance MulAction.Regular.isPretransitive {G : Type u_2} [Group G] :
      IsPretransitive G G

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

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

      The regular action of a group on itself is transitive.

      source
      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.

      source
      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.

      source
      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 α
      source
      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 α
      source
      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 α
      source
      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 #

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