HepLean 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
    theorem AddAction.IsPretransitive.exists_vadd_eq {M : Type u_5} {α : Type u_6} :
    ∀ {inst : VAdd M α} [self : AddAction.IsPretransitive M α] (x y : α), ∃ (g : M), g +ᵥ x = y

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

    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.exists_smul_eq {M : Type u_5} {α : Type u_6} :
      ∀ {inst : SMul M α} [self : MulAction.IsPretransitive M α] (x y : α), ∃ (g : M), g • x = y

      There is g such that g • x = y.

      source
      theorem AddAction.exists_vadd_eq (M : Type u_1) {α : Type u_3} [VAdd M α] [AddAction.IsPretransitive M α] (x : α) (y : α) :
      ∃ (m : M), m +ᵥ x = y
      source
      theorem MulAction.exists_smul_eq (M : Type u_1) {α : Type u_3} [SMul M α] [MulAction.IsPretransitive M α] (x : α) (y : α) :
      ∃ (m : M), m • x = y
      source
      theorem AddAction.surjective_vadd (M : Type u_1) {α : Type u_3} [VAdd M α] [AddAction.IsPretransitive M α] (x : α) :
      Function.Surjective fun (c : M) => c +ᵥ x
      source
      theorem MulAction.surjective_smul (M : Type u_1) {α : Type u_3} [SMul M α] [MulAction.IsPretransitive M α] (x : α) :
      Function.Surjective fun (c : M) => c • x
      source
      instance AddAction.Regular.isPretransitive {G : Type u_2} [AddGroup G] :
      AddAction.IsPretransitive G G

      The regular action of a group on itself is transitive.

      Equations
      • ⋯ = ⋯
      source
      instance MulAction.Regular.isPretransitive {G : Type u_2} [Group G] :
      MulAction.IsPretransitive G G

      The regular action of a group on itself is transitive.

      Equations
      • ⋯ = ⋯
      source
      theorem AddAction.isPretransitive_compHom {E : Type u_5} {F : Type u_6} {G : Type u_7} [AddMonoid E] [AddMonoid F] [AddAction F G] [AddAction.IsPretransitive F G] {f : E →+ F} (hf : Function.Surjective ⇑f) :
      AddAction.IsPretransitive E G
      source
      theorem MulAction.isPretransitive_compHom {E : Type u_5} {F : Type u_6} {G : Type u_7} [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.

      source
      theorem AddAction.IsPretransitive.of_vadd_eq {M : Type u_5} {N : Type u_6} {α : Type u_7} [VAdd M α] [VAdd N α] [AddAction.IsPretransitive M α] (f : M → N) (hf : ∀ {c : M} {x : α}, f c +ᵥ x = c +ᵥ x) :
      AddAction.IsPretransitive N α
      source
      theorem MulAction.IsPretransitive.of_smul_eq {M : Type u_5} {N : Type u_6} {α : Type u_7} [SMul M α] [SMul N α] [MulAction.IsPretransitive M α] (f : M → N) (hf : ∀ {c : M} {x : α}, f c • x = c • x) :
      MulAction.IsPretransitive N α
      source
      theorem AddAction.IsPretransitive.of_compHom {M : Type u_5} {N : Type u_6} {α : Type u_7} [AddMonoid M] [AddMonoid N] [AddAction N α] (f : M →+ N) [h : AddAction.IsPretransitive M α] :
      AddAction.IsPretransitive N α
      source
      theorem MulAction.IsPretransitive.of_compHom {M : Type u_5} {N : Type u_6} {α : Type u_7} [Monoid M] [Monoid N] [MulAction N α] (f : M →* N) [h : MulAction.IsPretransitive M α] :
      MulAction.IsPretransitive N α
      source
      theorem AddAction.IsPretransitive.of_isScalarTower (M : Type u_5) {N : Type u_6} {α : Type u_7} [AddMonoid N] [VAdd M N] [AddAction N α] [VAdd M α] [VAddAssocClass M N α] [AddAction.IsPretransitive M α] :
      AddAction.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 α] [MulAction.IsPretransitive M α] :
      MulAction.IsPretransitive N α

      Additive, Multiplicative #

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