Documentation

instance Function.End.applyMulAction {α : Type u_5} :

MulAction (Function.End α) α

The tautological action by Function.End α on α.

This is generalized to bundled endomorphisms by:

Equations

instance Function.End.applyAddAction {α : Type u_5} :

AddAction (Additive (Function.End α)) α

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

Equations

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

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

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

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

@[simp]

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

(toPermHom G α) a = toPerm a

theorem MulAction.coe_toPermHom (G : Type u_1) (α : Type u_5) [Group G] [MulAction G α] :

⇑(toPermHom G α) = toPerm

theorem MulAction.toPerm_one (G : Type u_1) (α : Type u_5) [Group G] [MulAction G α] :

toPerm 1 = 1

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

Instances For

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

theorem AddAction.coe_toPermHom (G : Type u_1) (α : Type u_5) [AddGroup G] [AddAction G α] :

⇑(toPermHom G α) = toPerm

theorem AddAction.toPerm_zero (G : Type u_1) (α : Type u_5) [AddGroup G] [AddAction G α] :

toPerm 0 = 1

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

Instances For

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

Instances For

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

Instances For

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