Documentation

Mathlib.GroupTheory.GroupAction.Group

Group actions applied to various types of group #

This file contains lemmas about SMul on GroupWithZero, and Group.

@[simp]
theorem neg_vadd_vadd {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (c : α) (x : β) :
-c +ᵥ (c +ᵥ x) = x
@[simp]
theorem inv_smul_smul {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (c : α) (x : β) :
c⁻¹ c x = x
@[simp]
theorem vadd_neg_vadd {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (c : α) (x : β) :
c +ᵥ (-c +ᵥ x) = x
@[simp]
theorem smul_inv_smul {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (c : α) (x : β) :
c c⁻¹ x = x
def AddAction.toPerm {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (a : α) :

Given an action of an additive group α on β, each g : α defines a permutation of β.

Equations
@[simp]
theorem AddAction.toPerm_apply {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (a : α) (x : β) :
↑(AddAction.toPerm a) x = a +ᵥ x
@[simp]
theorem AddAction.toPerm_symm_apply {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (a : α) (x : β) :
@[simp]
theorem MulAction.toPerm_apply {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (a : α) (x : β) :
↑(MulAction.toPerm a) x = a x
@[simp]
theorem MulAction.toPerm_symm_apply {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (a : α) (x : β) :
def MulAction.toPerm {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (a : α) :

Given an action of a group α on β, each g : α defines a permutation of β.

Equations
theorem AddAction.toPerm_injective {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] [inst : FaithfulVAdd α β] :
Function.Injective AddAction.toPerm

AddAction.toPerm is injective on faithful actions.

theorem MulAction.toPerm_injective {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] [inst : FaithfulSMul α β] :
Function.Injective MulAction.toPerm

MulAction.toPerm is injective on faithful actions.

@[simp]
theorem MulAction.toPermHom_apply (α : Type u) (β : Type v) [inst : Group α] [inst : MulAction α β] (a : α) :
def MulAction.toPermHom (α : Type u) (β : Type v) [inst : Group α] [inst : MulAction α β] :

Given an action of a group α on a set β, each g : α defines a permutation of β.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddAction.toPermHom_apply_apply (β : Type v) (α : Type u_1) [inst : AddGroup α] [inst : AddAction α β] (a : α) (x : β) :
↑(↑(AddAction.toPermHom β α) a) x = a +ᵥ x
@[simp]
theorem AddAction.toPermHom_apply_symm_apply (β : Type v) (α : Type u_1) [inst : AddGroup α] [inst : AddAction α β] (a : α) (x : β) :
↑(Equiv.symm (↑(AddAction.toPermHom β α) a)) x = (Multiplicative.ofAdd a)⁻¹ x
def AddAction.toPermHom (β : Type v) (α : Type u_1) [inst : AddGroup α] [inst : AddAction α β] :

Given an action of a additive group α on a set β, each g : α defines a permutation of β.

Equations
instance Equiv.Perm.applyMulAction (α : Type u_1) :

The tautological action by Equiv.Perm α on α.

This generalizes Function.End.applyMulAction.

Equations
@[simp]
theorem Equiv.Perm.smul_def {α : Type u_1} (f : Equiv.Perm α) (a : α) :
f a = f a
theorem neg_vadd_eq_iff {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] {a : α} {x : β} {y : β} :
-a +ᵥ x = y x = a +ᵥ y
theorem inv_smul_eq_iff {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] {a : α} {x : β} {y : β} :
a⁻¹ x = y x = a y
theorem eq_neg_vadd_iff {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] {a : α} {x : β} {y : β} :
x = -a +ᵥ y a +ᵥ x = y
theorem eq_inv_smul_iff {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] {a : α} {x : β} {y : β} :
x = a⁻¹ y a x = y
theorem smul_inv {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] [inst : Group β] [inst : SMulCommClass α β β] [inst : IsScalarTower α β β] (c : α) (x : β) :
theorem smul_zpow {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] [inst : Group β] [inst : SMulCommClass α β β] [inst : IsScalarTower α β β] (c : α) (x : β) (p : ) :
(c x) ^ p = c ^ p x ^ p
@[simp]
theorem Commute.smul_right_iff {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] [inst : Mul β] [inst : SMulCommClass α β β] [inst : IsScalarTower α β β] {a : β} {b : β} (r : α) :
Commute a (r b) Commute a b
@[simp]
theorem Commute.smul_left_iff {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] [inst : Mul β] [inst : SMulCommClass α β β] [inst : IsScalarTower α β β] {a : β} {b : β} (r : α) :
Commute (r a) b Commute a b
theorem AddAction.bijective {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) :
Function.Bijective ((fun x x_1 => x +ᵥ x_1) g)
theorem MulAction.bijective {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) :
Function.Bijective ((fun x x_1 => x x_1) g)
theorem AddAction.injective {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) :
Function.Injective ((fun x x_1 => x +ᵥ x_1) g)
theorem MulAction.injective {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) :
Function.Injective ((fun x x_1 => x x_1) g)
theorem AddAction.surjective {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) :
Function.Surjective ((fun x x_1 => x +ᵥ x_1) g)
theorem MulAction.surjective {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) :
Function.Surjective ((fun x x_1 => x x_1) g)
theorem vadd_left_cancel {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) {x : β} {y : β} (h : g +ᵥ x = g +ᵥ y) :
x = y
theorem smul_left_cancel {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) {x : β} {y : β} (h : g x = g y) :
x = y
@[simp]
theorem vadd_left_cancel_iff {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) {x : β} {y : β} :
g +ᵥ x = g +ᵥ y x = y
@[simp]
theorem smul_left_cancel_iff {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) {x : β} {y : β} :
g x = g y x = y
theorem vadd_eq_iff_eq_neg_vadd {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) {x : β} {y : β} :
g +ᵥ x = y x = -g +ᵥ y
theorem smul_eq_iff_eq_inv_smul {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) {x : β} {y : β} :
g x = y x = g⁻¹ y
instance CancelMonoidWithZero.faithfulSMul {α : Type u} [inst : CancelMonoidWithZero α] [inst : Nontrivial α] :

Monoid.toMulAction is faithful on nontrivial cancellative monoids with zero.

Equations
@[simp]
theorem inv_smul_smul₀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst : MulAction α β] {c : α} (hc : c 0) (x : β) :
c⁻¹ c x = x
@[simp]
theorem smul_inv_smul₀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst : MulAction α β] {c : α} (hc : c 0) (x : β) :
c c⁻¹ x = x
theorem inv_smul_eq_iff₀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) {x : β} {y : β} :
a⁻¹ x = y x = a y
theorem eq_inv_smul_iff₀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) {x : β} {y : β} :
x = a⁻¹ y a x = y
@[simp]
theorem Commute.smul_right_iff₀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst : MulAction α β] [inst : Mul β] [inst : SMulCommClass α β β] [inst : IsScalarTower α β β] {a : β} {b : β} {c : α} (hc : c 0) :
Commute a (c b) Commute a b
@[simp]
theorem Commute.smul_left_iff₀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst : MulAction α β] [inst : Mul β] [inst : SMulCommClass α β β] [inst : IsScalarTower α β β] {a : β} {b : β} {c : α} (hc : c 0) :
Commute (c a) b Commute a b
theorem MulAction.bijective₀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) :
Function.Bijective ((fun x x_1 => x x_1) a)
theorem MulAction.injective₀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) :
Function.Injective ((fun x x_1 => x x_1) a)
theorem MulAction.surjective₀ {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) :
Function.Surjective ((fun x x_1 => x x_1) a)
@[simp]
theorem DistribMulAction.toAddEquiv_apply {α : Type u} (β : Type v) [inst : Group α] [inst : AddMonoid β] [inst : DistribMulAction α β] (x : α) :
∀ (a : β), ↑(DistribMulAction.toAddEquiv β x) a = x a
@[simp]
theorem DistribMulAction.toAddEquiv_symm_apply {α : Type u} (β : Type v) [inst : Group α] [inst : AddMonoid β] [inst : DistribMulAction α β] (x : α) :
∀ (a : β), ↑(AddEquiv.symm (DistribMulAction.toAddEquiv β x)) a = x⁻¹ a
def DistribMulAction.toAddEquiv {α : Type u} (β : Type v) [inst : Group α] [inst : AddMonoid β] [inst : DistribMulAction α β] (x : α) :
β ≃+ β

Each element of the group defines an additive monoid isomorphism.

This is a stronger version of MulAction.toPerm.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem DistribMulAction.toAddAut_apply (α : Type u) (β : Type v) [inst : Group α] [inst : AddMonoid β] [inst : DistribMulAction α β] (x : α) :
def DistribMulAction.toAddAut (α : Type u) (β : Type v) [inst : Group α] [inst : AddMonoid β] [inst : DistribMulAction α β] :
α →* AddAut β

Each element of the group defines an additive monoid isomorphism.

This is a stronger version of MulAction.toPermHom.

Equations
  • One or more equations did not get rendered due to their size.
theorem smul_eq_zero_iff_eq {α : Type u} {β : Type v} [inst : Group α] [inst : AddMonoid β] [inst : DistribMulAction α β] (a : α) {x : β} :
a x = 0 x = 0
theorem smul_ne_zero_iff_ne {α : Type u} {β : Type v} [inst : Group α] [inst : AddMonoid β] [inst : DistribMulAction α β] (a : α) {x : β} :
a x 0 x 0
theorem smul_eq_zero_iff_eq' {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst : AddMonoid β] [inst : DistribMulAction α β] {a : α} (ha : a 0) {x : β} :
a x = 0 x = 0
theorem smul_ne_zero_iff_ne' {α : Type u} {β : Type v} [inst : GroupWithZero α] [inst : AddMonoid β] [inst : DistribMulAction α β] {a : α} (ha : a 0) {x : β} :
a x 0 x 0
@[simp]
theorem MulDistribMulAction.toMulEquiv_apply {α : Type u} (β : Type v) [inst : Group α] [inst : Monoid β] [inst : MulDistribMulAction α β] (x : α) :
∀ (a : β), ↑(MulDistribMulAction.toMulEquiv β x) a = x a
@[simp]
theorem MulDistribMulAction.toMulEquiv_symm_apply {α : Type u} (β : Type v) [inst : Group α] [inst : Monoid β] [inst : MulDistribMulAction α β] (x : α) :
∀ (a : β), ↑(MulEquiv.symm (MulDistribMulAction.toMulEquiv β x)) a = x⁻¹ a
def MulDistribMulAction.toMulEquiv {α : Type u} (β : Type v) [inst : Group α] [inst : Monoid β] [inst : MulDistribMulAction α β] (x : α) :
β ≃* β

Each element of the group defines a multiplicative monoid isomorphism.

This is a stronger version of MulAction.toPerm.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem MulDistribMulAction.toMulAut_apply (α : Type u) (β : Type v) [inst : Group α] [inst : Monoid β] [inst : MulDistribMulAction α β] (x : α) :
def MulDistribMulAction.toMulAut (α : Type u) (β : Type v) [inst : Group α] [inst : Monoid β] [inst : MulDistribMulAction α β] :
α →* MulAut β

Each element of the group defines an multiplicative monoid isomorphism.

This is a stronger version of MulAction.toPermHom.

Equations
  • One or more equations did not get rendered due to their size.
def arrowAddAction.proof_2 {G : Type u_3} {A : Type u_1} {B : Type u_2} [inst : SubtractionMonoid G] [inst : AddAction G A] (x : G) (y : G) (f : AB) :
(fun a => f (-(x + y) +ᵥ a)) = fun a => f (-y +ᵥ (-x +ᵥ a))
Equations
def arrowAddAction.proof_1 {G : Type u_3} {A : Type u_1} {B : Type u_2} [inst : SubtractionMonoid G] [inst : AddAction G A] (f : AB) :
(fun x => f (-0 +ᵥ x)) = f
Equations
  • (_ : (fun x => f (-0 +ᵥ x)) = f) = (_ : (fun x => f (-0 +ᵥ x)) = f)
def arrowAddAction {G : Type u_1} {A : Type u_2} {B : Type u_3} [inst : SubtractionMonoid G] [inst : AddAction G A] :
AddAction G (AB)

If G acts on A, then it acts also on A → B→ B, by (g +ᵥ F) a = F (g⁻¹ +ᵥ a)⁻¹ +ᵥ a)

Equations
  • arrowAddAction = AddAction.mk (_ : ∀ (f : AB), (fun x => f (-0 +ᵥ x)) = f) (_ : ∀ (x y : G) (f : AB), (fun a => f (-(x + y) +ᵥ a)) = fun a => f (-y +ᵥ (-x +ᵥ a)))
@[simp]
theorem arrowAction_smul {G : Type u_1} {A : Type u_2} {B : Type u_3} [inst : DivisionMonoid G] [inst : MulAction G A] (g : G) (F : AB) (a : A) :
SMul.smul G (AB) MulAction.toSMul g F a = F (g⁻¹ a)
@[simp]
theorem arrowAddAction_vadd {G : Type u_1} {A : Type u_2} {B : Type u_3} [inst : SubtractionMonoid G] [inst : AddAction G A] (g : G) (F : AB) (a : A) :
VAdd.vadd G (AB) AddAction.toVAdd g F a = F (-g +ᵥ a)
def arrowAction {G : Type u_1} {A : Type u_2} {B : Type u_3} [inst : DivisionMonoid G] [inst : MulAction G A] :
MulAction G (AB)

If G acts on A, then it acts also on A → B→ B, by (g • F) a = F (g⁻¹ • a)⁻¹ • a).

Equations
def arrowMulDistribMulAction {G : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Group G] [inst : MulAction G A] [inst : Monoid B] :

When B is a monoid, ArrowAction is additionally a MulDistribMulAction.

Equations
@[simp]
theorem mulAutArrow_apply_apply {G : Type u_1} {A : Type u_2} {H : Type u_3} [inst : Group G] [inst : MulAction G A] [inst : Monoid H] (x : G) :
∀ (a : AH) (a_1 : A), ↑(mulAutArrow x) a a_1 = (G (AH)) (AH) instHSMul x a a_1
@[simp]
theorem mulAutArrow_apply_symm_apply {G : Type u_1} {A : Type u_2} {H : Type u_3} [inst : Group G] [inst : MulAction G A] [inst : Monoid H] (x : G) :
∀ (a : AH) (a_1 : A), ↑(MulEquiv.symm (mulAutArrow x)) a a_1 = (G (AH)) (AH) instHSMul x⁻¹ a a_1
def mulAutArrow {G : Type u_1} {A : Type u_2} {H : Type u_3} [inst : Group G] [inst : MulAction G A] [inst : Monoid H] :
G →* MulAut (AH)

Given groups G H with G acting on A, G acts by multiplicative automorphisms on A → H→ H.

Equations
abbrev IsAddUnit.vadd_left_cancel.match_1 {α : Type u_1} [inst : AddMonoid α] {a : α} (motive : IsAddUnit aProp) :
(ha : IsAddUnit a) → ((u : AddUnits α) → (hu : u = a) → motive (_ : u, u = a)) → motive ha
Equations
theorem IsAddUnit.vadd_left_cancel {α : Type u} {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] {a : α} (ha : IsAddUnit a) {x : β} {y : β} :
a +ᵥ x = a +ᵥ y x = y
theorem IsUnit.smul_left_cancel {α : Type u} {β : Type v} [inst : Monoid α] [inst : MulAction α β] {a : α} (ha : IsUnit a) {x : β} {y : β} :
a x = a y x = y
@[simp]
theorem IsUnit.smul_eq_zero {α : Type u} {β : Type v} [inst : Monoid α] [inst : AddMonoid β] [inst : DistribMulAction α β] {u : α} (hu : IsUnit u) {x : β} :
u x = 0 x = 0
@[simp]
theorem isUnit_smul_iff {α : Type u} {β : Type v} [inst : Group α] [inst : Monoid β] [inst : MulAction α β] [inst : SMulCommClass α β β] [inst : IsScalarTower α β β] (g : α) (m : β) :
theorem IsUnit.smul_sub_iff_sub_inv_smul {α : Type u} {β : Type v} [inst : Group α] [inst : Monoid β] [inst : AddGroup β] [inst : DistribMulAction α β] [inst : IsScalarTower α β β] [inst : SMulCommClass α β β] (r : α) (a : β) :
IsUnit (r 1 - a) IsUnit (1 - r⁻¹ a)