Group actions applied to various types of group #

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

source

ink

@[simp]

theorem AddAction.toPerm_apply {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (a : α) (x : β) :

↑(AddAction.toPerm a) x = a +ᵥ x

source

ink

@[simp]

theorem AddAction.toPerm_symm_apply {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (a : α) (x : β) :

↑(Equiv.symm (AddAction.toPerm a)) x = -a +ᵥ x

source

ink

@[simp]

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

↑(MulAction.toPerm a) x = a • x

source

ink

@[simp]

theorem MulAction.toPerm_symm_apply {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (a : α) (x : β) :

↑(Equiv.symm (MulAction.toPerm a)) x = a⁻¹ • x

source

ink

def MulAction.toPerm {α : Type u} {β : Type v} [inst : Group α] [inst : 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 := (_ : ∀ (x : β), a⁻¹ • a • x = x), right_inv := (_ : ∀ (x : β), a • a⁻¹ • x = x) }

source

ink

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.

source

ink

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.

source

ink

@[simp]

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

↑(MulAction.toPermHom α β) a = MulAction.toPerm a

source

ink

def MulAction.toPermHom (α : Type u) (β : Type v) [inst : Group α] [inst : MulAction α β] :

α →* Equiv.Perm β

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.

source

ink

@[simp]

theorem AddAction.toPermHom_apply_apply (β : Type v) (α : Type u_1) [inst : AddGroup α] [inst : AddAction α β] (a : α) (x : β) :

↑(↑(AddAction.toPermHom β α) a) x = a +ᵥ x

source

ink

@[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

source

ink

def AddAction.toPermHom (β : Type v) (α : Type u_1) [inst : AddGroup α] [inst : AddAction α β] :

α →+ Additive (Equiv.Perm β)

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

Equations

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

source

ink

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 (_ : ∀ (x : α), 1 • x = 1 • x) (_ : ∀ (x x_1 : Equiv.Perm α) (x_2 : α), (x * x_1) • x_2 = (x * x_1) • x_2)

source

ink

@[simp]

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

f • a = ↑f a

source

ink

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

FaithfulSMul (Equiv.Perm α) α

Equiv.Perm.applyMulAction is faithful.

Equations

Equiv.Perm.applyFaithfulSMul = Equiv.Perm.applyFaithfulSMul.proof_1

source

ink

theorem neg_vadd_eq_iff {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] {a : α} {x : β} {y : β} :

-a +ᵥ x = y ↔ x = a +ᵥ y

source

ink

theorem inv_smul_eq_iff {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] {a : α} {x : β} {y : β} :

a⁻¹ • x = y ↔ x = a • y

source

ink

theorem eq_neg_vadd_iff {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] {a : α} {x : β} {y : β} :

x = -a +ᵥ y ↔ a +ᵥ x = y

source

ink

theorem eq_inv_smul_iff {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] {a : α} {x : β} {y : β} :

x = a⁻¹ • y ↔ a • x = y

source

ink

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

(c • x)⁻¹ = c⁻¹ • x⁻¹

source

ink

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

source

ink

@[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

source

ink

@[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

source

ink

theorem AddAction.bijective {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) :

Function.Bijective ((fun x x_1 => x +ᵥ x_1) g)

source

ink

theorem MulAction.bijective {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) :

Function.Bijective ((fun x x_1 => x • x_1) g)

source

ink

theorem AddAction.injective {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) :

Function.Injective ((fun x x_1 => x +ᵥ x_1) g)

source

ink

theorem MulAction.injective {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) :

Function.Injective ((fun x x_1 => x • x_1) g)

source

ink

theorem AddAction.surjective {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) :

Function.Surjective ((fun x x_1 => x +ᵥ x_1) g)

source

ink

theorem MulAction.surjective {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) :

Function.Surjective ((fun x x_1 => x • x_1) g)

source

ink

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

x = y

source

ink

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

x = y

source

ink

@[simp]

theorem vadd_left_cancel_iff {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) {x : β} {y : β} :

g +ᵥ x = g +ᵥ y ↔ x = y

source

ink

@[simp]

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

g • x = g • y ↔ x = y

source

ink

theorem vadd_eq_iff_eq_neg_vadd {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) {x : β} {y : β} :

g +ᵥ x = y ↔ x = -g +ᵥ y

source

ink

theorem smul_eq_iff_eq_inv_smul {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) {x : β} {y : β} :

g • x = y ↔ x = g⁻¹ • y

source

ink

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

FaithfulSMul α α

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

Equations

@CancelMonoidWithZero.faithfulSMul = @CancelMonoidWithZero.faithfulSMul.proof_1

source

ink

@[simp]

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

c⁻¹ • c • x = x

source

ink

@[simp]

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

c • c⁻¹ • x = x

source

ink

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

source

ink

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

source

ink

@[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

source

ink

@[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

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

@[simp]

theorem DistribMulAction.toAddEquiv_apply {α : Type u} (β : Type v) [inst : Group α] [inst : AddMonoid β] [inst : DistribMulAction α β] (x : α) :

∀ (a : β), ↑(DistribMulAction.toAddEquiv β x) a = x • a

source

ink

@[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

source

ink

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.

source

ink

@[simp]

theorem DistribMulAction.toAddAut_apply (α : Type u) (β : Type v) [inst : Group α] [inst : AddMonoid β] [inst : DistribMulAction α β] (x : α) :

↑(DistribMulAction.toAddAut α β) x = DistribMulAction.toAddEquiv β x

source

ink

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.

source

ink

theorem smul_eq_zero_iff_eq {α : Type u} {β : Type v} [inst : Group α] [inst : AddMonoid β] [inst : DistribMulAction α β] (a : α) {x : β} :

a • x = 0 ↔ x = 0

source

ink

theorem smul_ne_zero_iff_ne {α : Type u} {β : Type v} [inst : Group α] [inst : AddMonoid β] [inst : DistribMulAction α β] (a : α) {x : β} :

a • x ≠ 0 ↔ x ≠ 0

source

ink

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

source

ink

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

source

ink

@[simp]

theorem MulDistribMulAction.toMulEquiv_apply {α : Type u} (β : Type v) [inst : Group α] [inst : Monoid β] [inst : MulDistribMulAction α β] (x : α) :

∀ (a : β), ↑(MulDistribMulAction.toMulEquiv β x) a = x • a

source

ink

@[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

source

ink

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.

source

ink

@[simp]

theorem MulDistribMulAction.toMulAut_apply (α : Type u) (β : Type v) [inst : Group α] [inst : Monoid β] [inst : MulDistribMulAction α β] (x : α) :

↑(MulDistribMulAction.toMulAut α β) x = MulDistribMulAction.toMulEquiv β x

source

ink

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.

source

ink

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 : A → B) :

(fun a => f (-(x + y) +ᵥ a)) = fun a => f (-y +ᵥ (-x +ᵥ a))

Equations

(_ : (fun a => f (-(x + y) +ᵥ a)) = fun a => f (-y +ᵥ (-x +ᵥ a))) = (_ : (fun a => f (-(x + y) +ᵥ a)) = fun a => f (-y +ᵥ (-x +ᵥ a)))

source

ink

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

(fun x => f (-0 +ᵥ x)) = f

Equations

(_ : (fun x => f (-0 +ᵥ x)) = f) = (_ : (fun x => f (-0 +ᵥ x)) = f)

source

ink

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

AddAction G (A → B)

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 : A → B), (fun x => f (-0 +ᵥ x)) = f) (_ : ∀ (x y : G) (f : A → B), (fun a => f (-(x + y) +ᵥ a)) = fun a => f (-y +ᵥ (-x +ᵥ a)))

source

ink

@[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 : A → B) (a : A) :

SMul.smul G (A → B) MulAction.toSMul g F a = F (g⁻¹ • a)

source

ink

@[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 : A → B) (a : A) :

VAdd.vadd G (A → B) AddAction.toVAdd g F a = F (-g +ᵥ a)

source

ink

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

MulAction G (A → B)

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

Equations

arrowAction = MulAction.mk (_ : ∀ (f : A → B), (fun x => f (1⁻¹ • x)) = f) (_ : ∀ (x y : G) (f : A → B), (fun a => f ((x * y)⁻¹ • a)) = fun a => f (y⁻¹ • x⁻¹ • a))

source

ink

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

MulDistribMulAction G (A → B)

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

Equations

arrowMulDistribMulAction = MulDistribMulAction.mk (_ : ∀ (x : G) (x_1 x_2 : A → B), x • (x_1 * x_2) = x • (x_1 * x_2)) (_ : ∀ (x : G), x • 1 = x • 1)

source

ink

@[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 : A → H) (a_1 : A), ↑(↑mulAutArrow x) a a_1 = (G • (A → H)) (A → H) instHSMul x a a_1

source

ink

@[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 : A → H) (a_1 : A), ↑(MulEquiv.symm (↑mulAutArrow x)) a a_1 = (G • (A → H)) (A → H) instHSMul x⁻¹ a a_1

source

ink

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 (A → H)

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

Equations

mulAutArrow = MulDistribMulAction.toMulAut G (A → H)

source

ink

abbrev IsAddUnit.vadd_left_cancel.match_1 {α : Type u_1} [inst : AddMonoid α] {a : α} (motive : IsAddUnit a → Prop) :

(ha : IsAddUnit a) → ((u : AddUnits α) → (hu : ↑u = a) → motive (_ : ∃ u, ↑u = a)) → motive ha

Equations

IsAddUnit.vadd_left_cancel.match_1 motive ha h_1 = Exists.casesOn ha fun w h => h_1 w h

source

ink

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

source

ink

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

source

ink

@[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

source

ink

@[simp]

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

IsUnit (g • m) ↔ IsUnit m

source

ink

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)