Group actions applied to various types of group

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

instance AddRightCancelMonoid.faithfulVAdd {α : Type u} [AddRightCancelMonoid α] : FaithfulVAdd α α

AddMonoid.toAddAction is faithful on additive cancellative monoids.

Equations

• ⋯ = ⋯

instance RightCancelMonoid.faithfulSMul {α : Type u} [RightCancelMonoid α] : FaithfulSMul α α

Monoid.toMulAction is faithful on cancellative monoids.

Equations

• ⋯ = ⋯

@[simp]

theorem neg_vadd_vadd {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (c : α) (x : β) : -c +ᵥ (c +ᵥ x) = x

@[simp]

theorem inv_smul_smul {α : Type u} {β : Type v} [Group α] [MulAction α β] (c : α) (x : β) : c⁻¹ • c • x = x

@[simp]

theorem vadd_neg_vadd {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (c : α) (x : β) : c +ᵥ (-c +ᵥ x) = x

@[simp]

theorem smul_inv_smul {α : Type u} {β : Type v} [Group α] [MulAction α β] (c : α) (x : β) : c • c⁻¹ • x = x

def AddAction.toPerm {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (a : α) : Equiv.Perm β

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

Equations

• AddAction.toPerm a = { toFun := fun (x : β) => a +ᵥ x, invFun := fun (x : β) => -a +ᵥ x, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MulAction.toPerm_apply {α : Type u} {β : Type v} [Group α] [MulAction α β] (a : α) (x : β) : (MulAction.toPerm a) x = a • x

@[simp]

theorem AddAction.toPerm_apply {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (a : α) (x : β) : (AddAction.toPerm a) x = a +ᵥ x

@[simp]

theorem MulAction.toPerm_symm_apply {α : Type u} {β : Type v} [Group α] [MulAction α β] (a : α) (x : β) : (MulAction.toPerm a).symm x = a⁻¹ • x

@[simp]

theorem AddAction.toPerm_symm_apply {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (a : α) (x : β) : (AddAction.toPerm a).symm x = -a +ᵥ x

def MulAction.toPerm {α : Type u} {β : Type v} [Group α] [MulAction α β] (a : α) : Equiv.Perm β

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

Equations

• MulAction.toPerm a = { toFun := fun (x : β) => a • x, invFun := fun (x : β) => a⁻¹ • x, left_inv := ⋯, right_inv := ⋯ }

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

AddAction.toPerm is injective on faithful actions.

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

MulAction.toPerm is injective on faithful actions.

@[simp]

theorem MulAction.toPermHom_apply (α : Type u) (β : Type v) [Group α] [MulAction α β] (a : α) : (MulAction.toPermHom α β) a = MulAction.toPerm a

def MulAction.toPermHom (α : Type u) (β : Type v) [Group α] [MulAction α β] : α →* Equiv.Perm β

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

Equations

• MulAction.toPermHom α β = { toOneHom := { toFun := MulAction.toPerm, map_one' := ⋯ }, map_mul' := ⋯ }

@[simp]

theorem AddAction.toPermHom_apply_symm_apply (β : Type v) (α : Type u_1) [AddGroup α] [AddAction α β] (a : α) (x : β) : ((AddAction.toPermHom β α) a).symm x = (Multiplicative.ofAdd a)⁻¹ • x

@[simp]

theorem AddAction.toPermHom_apply_apply (β : Type v) (α : Type u_1) [AddGroup α] [AddAction α β] (a : α) (x : β) : ((AddAction.toPermHom β α) a) x = a +ᵥ x

def AddAction.toPermHom (β : Type v) (α : Type u_1) [AddGroup α] [AddAction α β] : α →+ Additive (Equiv.Perm β)

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

Equations

• AddAction.toPermHom β α = MonoidHom.toAdditive'' (MulAction.toPermHom (Multiplicative α) β)

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

The tautological action by Equiv.Perm α on α.

This generalizes Function.End.applyMulAction.

Equations

• Equiv.Perm.applyMulAction α = MulAction.mk ⋯ ⋯

@[simp]

theorem Equiv.Perm.smul_def {α : Type u_1} (f : Equiv.Perm α) (a : α) : f • a = f a

instance Equiv.Perm.applyFaithfulSMul (α : Type u_1) : FaithfulSMul (Equiv.Perm α) α

Equiv.Perm.applyMulAction is faithful.

Equations

• ⋯ = ⋯

theorem neg_vadd_eq_iff {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] {a : α} {x : β} {y : β} : -a +ᵥ x = y ↔ x = a +ᵥ y

theorem inv_smul_eq_iff {α : Type u} {β : Type v} [Group α] [MulAction α β] {a : α} {x : β} {y : β} : a⁻¹ • x = y ↔ x = a • y

theorem eq_neg_vadd_iff {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] {a : α} {x : β} {y : β} : x = -a +ᵥ y ↔ a +ᵥ x = y

theorem eq_inv_smul_iff {α : Type u} {β : Type v} [Group α] [MulAction α β] {a : α} {x : β} {y : β} : x = a⁻¹ • y ↔ a • x = y

theorem smul_inv {α : Type u} {β : Type v} [Group α] [MulAction α β] [Group β] [SMulCommClass α β β] [IsScalarTower α β β] (c : α) (x : β) : (c • x)⁻¹ = c⁻¹ • x⁻¹

theorem smul_zpow {α : Type u} {β : Type v} [Group α] [MulAction α β] [Group β] [SMulCommClass α β β] [IsScalarTower α β β] (c : α) (x : β) (p : ℤ) : (c • x) ^ p = c ^ p • x ^ p

@[simp]

theorem Commute.smul_right_iff {α : Type u} {β : Type v} [Group α] [MulAction α β] [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {a : β} {b : β} (r : α) : Commute a (r • b) ↔ Commute a b

@[simp]

theorem Commute.smul_left_iff {α : Type u} {β : Type v} [Group α] [MulAction α β] [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {a : β} {b : β} (r : α) : Commute (r • a) b ↔ Commute a b

theorem AddAction.bijective {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) : Function.Bijective fun (x : β) => g +ᵥ x

theorem MulAction.bijective {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) : Function.Bijective fun (x : β) => g • x

theorem AddAction.injective {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) : Function.Injective fun (x : β) => g +ᵥ x

theorem MulAction.injective {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) : Function.Injective fun (x : β) => g • x

theorem AddAction.surjective {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) : Function.Surjective fun (x : β) => g +ᵥ x

theorem MulAction.surjective {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) : Function.Surjective fun (x : β) => g • x

theorem vadd_left_cancel {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) {x : β} {y : β} (h : g +ᵥ x = g +ᵥ y) : x = y

theorem smul_left_cancel {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) {x : β} {y : β} (h : g • x = g • y) : x = y

@[simp]

theorem vadd_left_cancel_iff {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) {x : β} {y : β} : g +ᵥ x = g +ᵥ y ↔ x = y

@[simp]

theorem smul_left_cancel_iff {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) {x : β} {y : β} : g • x = g • y ↔ x = y

theorem vadd_eq_iff_eq_neg_vadd {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (g : α) {x : β} {y : β} : g +ᵥ x = y ↔ x = -g +ᵥ y

theorem smul_eq_iff_eq_inv_smul {α : Type u} {β : Type v} [Group α] [MulAction α β] (g : α) {x : β} {y : β} : g • x = y ↔ x = g⁻¹ • y

@[simp]

theorem invOf_smul_smul {α : Type u} {β : Type v} [Monoid α] [MulAction α β] (c : α) (x : β) [Invertible c] : ⅟c • c • x = x

@[simp]

theorem smul_invOf_smul {α : Type u} {β : Type v} [Monoid α] [MulAction α β] (c : α) (x : β) [Invertible c] : c • ⅟c • x = x

theorem invOf_smul_eq_iff {α : Type u} {β : Type v} [Monoid α] [MulAction α β] {c : α} {x : β} {y : β} [Invertible c] : ⅟c • x = y ↔ x = c • y

theorem smul_eq_iff_eq_invOf_smul {α : Type u} {β : Type v} [Monoid α] [MulAction α β] {c : α} {x : β} {y : β} [Invertible c] : c • x = y ↔ x = ⅟c • y

instance CancelMonoidWithZero.faithfulSMul {α : Type u} [CancelMonoidWithZero α] [Nontrivial α] : FaithfulSMul α α

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

Equations

• ⋯ = ⋯

@[simp]

theorem inv_smul_smul₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {c : α} (hc : c ≠ 0) (x : β) : c⁻¹ • c • x = x

@[simp]

theorem smul_inv_smul₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {c : α} (hc : c ≠ 0) (x : β) : c • c⁻¹ • x = x

theorem inv_smul_eq_iff₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {x : β} {y : β} : a⁻¹ • x = y ↔ x = a • y

theorem eq_inv_smul_iff₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) {x : β} {y : β} : x = a⁻¹ • y ↔ a • x = y

@[simp]

theorem Commute.smul_right_iff₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {a : β} {b : β} {c : α} (hc : c ≠ 0) : Commute a (c • b) ↔ Commute a b

@[simp]

theorem Commute.smul_left_iff₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {a : β} {b : β} {c : α} (hc : c ≠ 0) : Commute (c • a) b ↔ Commute a b

@[simp]

theorem Equiv.smulRight_symm_apply {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (b : β) : (Equiv.smulRight ha).symm b = a⁻¹ • b

@[simp]

theorem Equiv.smulRight_apply {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) (b : β) : (Equiv.smulRight ha) b = a • b

def Equiv.smulRight {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) : β ≃ β

Right scalar multiplication as an order isomorphism.

Equations

• Equiv.smulRight ha = { toFun := fun (b : β) => a • b, invFun := fun (b : β) => a⁻¹ • b, left_inv := ⋯, right_inv := ⋯ }

theorem MulAction.bijective₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) : Function.Bijective fun (x : β) => a • x

theorem MulAction.injective₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) : Function.Injective fun (x : β) => a • x

theorem MulAction.surjective₀ {α : Type u} {β : Type v} [GroupWithZero α] [MulAction α β] {a : α} (ha : a ≠ 0) : Function.Surjective fun (x : β) => a • x

@[simp]

theorem DistribMulAction.toAddEquiv_apply {α : Type u} (β : Type v) [Group α] [AddMonoid β] [DistribMulAction α β] (x : α) : ∀ (a : β), (DistribMulAction.toAddEquiv β x) a = x • a

@[simp]

theorem DistribMulAction.toAddEquiv_symm_apply {α : Type u} (β : Type v) [Group α] [AddMonoid β] [DistribMulAction α β] (x : α) : ∀ (a : β), (AddEquiv.symm (DistribMulAction.toAddEquiv β x)) a = x⁻¹ • a

def DistribMulAction.toAddEquiv {α : Type u} (β : Type v) [Group α] [AddMonoid β] [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) [Group α] [AddMonoid β] [DistribMulAction α β] (x : α) : (DistribMulAction.toAddAut α β) x = DistribMulAction.toAddEquiv β x

def DistribMulAction.toAddAut (α : Type u) (β : Type v) [Group α] [AddMonoid β] [DistribMulAction α β] : α →* AddAut β

Each element of the group defines an additive monoid isomorphism.

This is a stronger version of MulAction.toPermHom.

Equations

• DistribMulAction.toAddAut α β = { toOneHom := { toFun := DistribMulAction.toAddEquiv β, map_one' := ⋯ }, map_mul' := ⋯ }

def DistribMulAction.toAddEquiv₀ {α : Type u_1} (β : Type u_2) [GroupWithZero α] [AddMonoid β] [DistribMulAction α β] (x : α) (hx : x ≠ 0) : β ≃+ β

Each non-zero element of a GroupWithZero defines an additive monoid isomorphism of an AddMonoid on which it acts distributively. This is a stronger version of DistribMulAction.toAddMonoidHom.

Equations

• One or more equations did not get rendered due to their size.

theorem smul_eq_zero_iff_eq {α : Type u} {β : Type v} [Group α] [AddMonoid β] [DistribMulAction α β] (a : α) {x : β} : a • x = 0 ↔ x = 0

theorem smul_ne_zero_iff_ne {α : Type u} {β : Type v} [Group α] [AddMonoid β] [DistribMulAction α β] (a : α) {x : β} : a • x ≠ 0 ↔ x ≠ 0

@[simp]

theorem MulDistribMulAction.toMulEquiv_symm_apply {α : Type u} (β : Type v) [Group α] [Monoid β] [MulDistribMulAction α β] (x : α) : ∀ (a : β), (MulEquiv.symm (MulDistribMulAction.toMulEquiv β x)) a = x⁻¹ • a

@[simp]

theorem MulDistribMulAction.toMulEquiv_apply {α : Type u} (β : Type v) [Group α] [Monoid β] [MulDistribMulAction α β] (x : α) : ∀ (a : β), (MulDistribMulAction.toMulEquiv β x) a = x • a

def MulDistribMulAction.toMulEquiv {α : Type u} (β : Type v) [Group α] [Monoid β] [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) [Group α] [Monoid β] [MulDistribMulAction α β] (x : α) : (MulDistribMulAction.toMulAut α β) x = MulDistribMulAction.toMulEquiv β x

def MulDistribMulAction.toMulAut (α : Type u) (β : Type v) [Group α] [Monoid β] [MulDistribMulAction α β] : α →* MulAut β

Each element of the group defines a multiplicative monoid isomorphism.

This is a stronger version of MulAction.toPermHom.

Equations

• MulDistribMulAction.toMulAut α β = { toOneHom := { toFun := MulDistribMulAction.toMulEquiv β, map_one' := ⋯ }, map_mul' := ⋯ }

def arrowAddAction {G : Type u_1} {A : Type u_2} {B : Type u_3} [SubtractionMonoid G] [AddAction G A] : AddAction G (A → B)

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

Equations

• arrowAddAction = AddAction.mk ⋯ ⋯

theorem arrowAddAction.proof_2 {G : Type u_3} {A : Type u_1} {B : Type u_2} [SubtractionMonoid G] [AddAction G A] (x : G) (y : G) (f : A → B) : (fun (a : A) => f (-(x + y) +ᵥ a)) = fun (a : A) => f (-y +ᵥ (-x +ᵥ a))

theorem arrowAddAction.proof_1 {G : Type u_3} {A : Type u_1} {B : Type u_2} [SubtractionMonoid G] [AddAction G A] (f : A → B) : (fun (x : A) => f (-0 +ᵥ x)) = f

@[simp]

theorem arrowAddAction_vadd {G : Type u_1} {A : Type u_2} {B : Type u_3} [SubtractionMonoid G] [AddAction G A] (g : G) (F : A → B) (a : A) : VAdd.vadd g F a = F (-g +ᵥ a)

@[simp]

theorem arrowAction_smul {G : Type u_1} {A : Type u_2} {B : Type u_3} [DivisionMonoid G] [MulAction G A] (g : G) (F : A → B) (a : A) : SMul.smul g F a = F (g⁻¹ • a)

def arrowAction {G : Type u_1} {A : Type u_2} {B : Type u_3} [DivisionMonoid G] [MulAction G A] : MulAction G (A → B)

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

Equations

• arrowAction = MulAction.mk ⋯ ⋯

def arrowMulDistribMulAction {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [MulAction G A] [Monoid B] : MulDistribMulAction G (A → B)

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

Equations

• arrowMulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯

@[simp]

theorem mulAutArrow_apply_apply {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [MulAction G A] [Monoid H] (x : G) : ∀ (a : A → H) (a_1 : A), (mulAutArrow x) a a_1 = (x • a) a_1

@[simp]

theorem mulAutArrow_apply_symm_apply {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [MulAction G A] [Monoid H] (x : G) : ∀ (a : A → H) (a_1 : A), (MulEquiv.symm (mulAutArrow x)) a a_1 = (x⁻¹ • a) a_1

def mulAutArrow {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [MulAction G A] [Monoid H] : G →* MulAut (A → H)

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

Equations

• mulAutArrow = MulDistribMulAction.toMulAut G (A → H)

theorem IsAddUnit.vadd_left_cancel {α : Type u} {β : Type v} [AddMonoid α] [AddAction α β] {a : α} (ha : IsAddUnit a) {x : β} {y : β} : a +ᵥ x = a +ᵥ y ↔ x = y

abbrev IsAddUnit.vadd_left_cancel.match_1 {α : Type u_1} [AddMonoid α] {a : α} (motive : IsAddUnit a → Prop) : ∀ (ha : IsAddUnit a), (∀ (u : AddUnits α) (hu : ↑u = a), motive ⋯) → motive ha

Equations

• ⋯ = ⋯

theorem IsUnit.smul_left_cancel {α : Type u} {β : Type v} [Monoid α] [MulAction α β] {a : α} (ha : IsUnit a) {x : β} {y : β} : a • x = a • y ↔ x = y

@[simp]

theorem IsUnit.smul_eq_zero {α : Type u} {β : Type v} [Monoid α] [AddMonoid β] [DistribMulAction α β] {u : α} (hu : IsUnit u) {x : β} : u • x = 0 ↔ x = 0

@[simp]

theorem isUnit_smul_iff {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction α β] [SMulCommClass α β β] [IsScalarTower α β β] (g : α) (m : β) : IsUnit (g • m) ↔ IsUnit m

theorem IsUnit.smul_sub_iff_sub_inv_smul {α : Type u} {β : Type v} [Group α] [Monoid β] [AddGroup β] [DistribMulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (r : α) (a : β) : IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)