Interaction between actions and endomorphisms/automorphisms

This file provides two things:

• The tautological actions by endomorphisms/automorphisms on their base type.
• An action by a monoid/group on a type is the same as a hom from the monoid/group to endomorphisms/automorphisms of the type.

Tags

monoid action, group action

Tautological actions

Tautological action by Function.End

instance Function.End.applyMulAction {α : Type u_5} : MulAction (Function.End α) α

The tautological action by Function.End α on α.

This is generalized to bundled endomorphisms by:

• Equiv.Perm.applyMulAction
• AddMonoid.End.applyDistribMulAction
• AddMonoid.End.applyModule
• AddAut.applyDistribMulAction
• MulAut.applyMulDistribMulAction
• LinearEquiv.applyDistribMulAction
• LinearMap.applyModule
• RingHom.applyMulSemiringAction
• RingAut.applyMulSemiringAction
• AlgEquiv.applyMulSemiringAction
• RelHom.applyMulAction
• RelEmbedding.applyMulAction
• RelIso.applyMulAction

Equations

• Function.End.applyMulAction = { smul := fun (x1 : Function.End α) (x2 : α) => x1 x2, one_smul := ⋯, mul_smul := ⋯ }

instance Function.End.applyAddAction {α : Type u_5} : AddAction (Additive (Function.End α)) α

The tautological additive action by Additive (Function.End α) on α.

Equations

• Function.End.applyAddAction = inferInstance

@[simp]

theorem Function.End.smul_def {α : Type u_5} (f : Function.End α) (a : α) : f • a = f a

theorem Function.End.mul_def {α : Type u_5} (f g : Function.End α) : f * g = f ∘ g

theorem Function.End.one_def {α : Type u_5} : 1 = id

instance Function.End.apply_FaithfulSMul {α : Type u_5} : FaithfulSMul (Function.End α) α

Function.End.applyMulAction is faithful.

Tautological action by Equiv.Perm

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

The tautological action by Equiv.Perm α on α.

This generalizes Function.End.applyMulAction.

Equations

• Equiv.Perm.applyMulAction α = { smul := fun (f : Equiv.Perm α) (a : α) => f a, one_smul := ⋯, mul_smul := ⋯ }

@[simp]

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

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

Equiv.Perm.applyMulAction is faithful.

instance Equiv.Perm.instIsPretransitive {α : Type u_5} : MulAction.IsPretransitive (Perm α) α

The permutation group of α acts transitively on α.

Tautological action by MulAut

instance MulAut.applyMulAction {M : Type u_2} [Monoid M] : MulAction (MulAut M) M

The tautological action by MulAut M on M.

Equations

• MulAut.applyMulAction = { smul := fun (x1 : MulAut M) (x2 : M) => x1 x2, one_smul := ⋯, mul_smul := ⋯ }

instance MulAut.applyMulDistribMulAction {M : Type u_2} [Monoid M] : MulDistribMulAction (MulAut M) M

The tautological action by MulAut M on M.

This generalizes Function.End.applyMulAction.

Equations

• MulAut.applyMulDistribMulAction = { smul := fun (x1 : MulAut M) (x2 : M) => x1 x2, one_smul := ⋯, mul_smul := ⋯, smul_mul := ⋯, smul_one := ⋯ }

@[simp]

theorem MulAut.smul_def {M : Type u_2} [Monoid M] (f : MulAut M) (a : M) : f • a = f a

instance MulAut.apply_faithfulSMul {M : Type u_2} [Monoid M] : FaithfulSMul (MulAut M) M

MulAut.applyDistribMulAction is faithful.

Tautological action by AddAut

instance AddAut.applyMulAction {M : Type u_2} [AddMonoid M] : MulAction (AddAut M) M

The tautological action by AddAut M on M.

Equations

• AddAut.applyMulAction = { smul := fun (x1 : AddAut M) (x2 : M) => x1 x2, one_smul := ⋯, mul_smul := ⋯ }

@[simp]

theorem AddAut.smul_def {M : Type u_2} [AddMonoid M] (f : AddAut M) (a : M) : f • a = f a

instance AddAut.apply_faithfulSMul {M : Type u_2} [AddMonoid M] : FaithfulSMul (AddAut M) M

AddAut.applyDistribMulAction is faithful.

Converting actions to and from homs to the monoid/group of endomorphisms/automorphisms

def MulAction.toEndHom {M : Type u_2} {α : Type u_5} [Monoid M] [MulAction M α] : M →* Function.End α

The monoid hom representing a monoid action.

When M is a group, see MulAction.toPermHom.

Equations

• MulAction.toEndHom = { toFun := fun (x1 : M) (x2 : α) => x1 • x2, map_one' := ⋯, map_mul' := ⋯ }

@[reducible, inline]

abbrev MulAction.ofEndHom {M : Type u_2} {α : Type u_5} [Monoid M] (f : M →* Function.End α) : MulAction M α

The monoid action induced by a monoid hom to Function.End α

See note [reducible non-instances].

Equations

• MulAction.ofEndHom f = MulAction.compHom α f

def AddAction.toEndHom {M : Type u_2} {α : Type u_5} [AddMonoid M] [AddAction M α] : M →+ Additive (Function.End α)

The additive monoid hom representing an additive monoid action.

When M is a group, see AddAction.toPermHom.

Equations

• AddAction.toEndHom = MonoidHom.toAdditiveRight MulAction.toEndHom

@[reducible, inline]

abbrev AddAction.ofEndHom {M : Type u_2} {α : Type u_5} [AddMonoid M] (f : M →+ Additive (Function.End α)) : AddAction M α

The additive action induced by a hom to Additive (Function.End α)

See note [reducible non-instances].

Equations

• AddAction.ofEndHom f = AddAction.compHom α f

def MulAction.toPermHom (G : Type u_1) (α : Type u_5) [Group G] [MulAction G α] : G →* Equiv.Perm α

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

Equations

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

@[simp]

theorem MulAction.toPermHom_apply (G : Type u_1) (α : Type u_5) [Group G] [MulAction G α] (a : G) : (toPermHom G α) a = toPerm a

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

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

Equations

• AddAction.toPermHom G α = MonoidHom.toAdditiveRight (MulAction.toPermHom (Multiplicative G) α)

@[simp]

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

@[simp]

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

def MulDistribMulAction.toMulEquiv {G : Type u_1} (M : Type u_2) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) : M ≃* M

Each element of the group defines a multiplicative monoid isomorphism.

This is a stronger version of MulAction.toPerm.

Equations

• MulDistribMulAction.toMulEquiv M x = { toFun := (↑(MulDistribMulAction.toMonoidHom M x)).toFun, invFun := ((MulAction.toPermHom G M) x).invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem MulDistribMulAction.toMulEquiv_apply {G : Type u_1} (M : Type u_2) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) (a✝ : M) : (toMulEquiv M x) a✝ = x • a✝

@[simp]

theorem MulDistribMulAction.toMulEquiv_symm_apply {G : Type u_1} (M : Type u_2) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) (a✝ : M) : (toMulEquiv M x).symm a✝ = x⁻¹ • a✝

def MulDistribMulAction.toMulAut (G : Type u_1) (M : Type u_2) [Group G] [Monoid M] [MulDistribMulAction G M] : G →* MulAut M

Each element of the group defines a multiplicative monoid isomorphism.

This is a stronger version of MulAction.toPermHom.

Equations

• MulDistribMulAction.toMulAut G M = { toFun := MulDistribMulAction.toMulEquiv M, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MulDistribMulAction.toMulAut_apply (G : Type u_1) (M : Type u_2) [Group G] [Monoid M] [MulDistribMulAction G M] (x : G) : (toMulAut G M) x = toMulEquiv M x

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

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

Equations

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

@[simp]

theorem mulAutArrow_apply_apply {G : Type u_1} {M : Type u_2} {A : Type u_4} [Group G] [MulAction G A] [Monoid M] (x : G) (a✝ : A → M) (a✝¹ : A) : (mulAutArrow x) a✝ a✝¹ = (x • a✝) a✝¹

@[simp]

theorem mulAutArrow_apply_symm_apply {G : Type u_1} {M : Type u_2} {A : Type u_4} [Group G] [MulAction G A] [Monoid M] (x : G) (a✝ : A → M) (a✝¹ : A) : (MulEquiv.symm (mulAutArrow x)) a✝ a✝¹ = (x⁻¹ • a✝) a✝¹