Endomorphisms, homomorphisms and group actions

This file defines Function.End as the monoid of endomorphisms on a type, and provides results relating group actions with these endomorphisms.

Notation

• a • b is used as notation for SMul.smul a b.
• a +ᵥ b is used as notation for VAdd.vadd a b.

Implementation details

This file should avoid depending on other parts of GroupTheory, to avoid import cycles. More sophisticated lemmas belong in GroupTheory.GroupAction.

Tags

group action

def MulAction.toFun (M : Type u_1) (α : Type u_3) [Monoid M] [MulAction M α] : α ↪ M → α

Embedding of α into functions M → α induced by a multiplicative action of M on α.

Equations

• MulAction.toFun M α = { toFun := fun (y : α) (x : M) => x • y, inj' := ⋯ }

def AddAction.toFun (M : Type u_1) (α : Type u_3) [AddMonoid M] [AddAction M α] : α ↪ M → α

Embedding of α into functions M → α induced by an additive action of M on α.

Equations

• AddAction.toFun M α = { toFun := fun (y : α) (x : M) => x +ᵥ y, inj' := ⋯ }

@[simp]

theorem MulAction.toFun_apply {M : Type u_1} {α : Type u_3} [Monoid M] [MulAction M α] (x : M) (y : α) : (toFun M α) y x = x • y

@[simp]

theorem AddAction.toFun_apply {M : Type u_1} {α : Type u_3} [AddMonoid M] [AddAction M α] (x : M) (y : α) : (toFun M α) y x = x +ᵥ y

def Function.End (α : Type u_3) : Type u_3

The monoid of endomorphisms.

Note that this is generalized by CategoryTheory.End to categories other than Type u.

Equations

• Function.End α = (α → α)

instance instMonoidEnd {α : Type u_3} : Monoid (Function.End α)

Equations

• instMonoidEnd = Monoid.mk ⋯ ⋯ (fun (n : ℕ) (f : Function.End α) => f^[n]) ⋯ ⋯

instance instInhabitedEnd {α : Type u_3} : Inhabited (Function.End α)

Equations

• instInhabitedEnd = { default := 1 }

instance Function.End.applyMulAction {α : Type u_3} : 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

Equations

• Function.End.applyMulAction = MulAction.mk ⋯ ⋯

instance Function.End.applyAddAction {α : Type u_3} : 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_3} (f : Function.End α) (a : α) : f • a = f a

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

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

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

Function.End.applyMulAction is faithful.

def MulAction.toEndHom {M : Type u_1} {α : Type u_3} [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' := ⋯ }

def AddAction.toEndHom {M : Type u_1} {α : Type u_3} [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.toAdditive'' MulAction.toEndHom

@[reducible, inline]

abbrev MulAction.ofEndHom {M : Type u_1} {α : Type u_3} [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

@[reducible, inline]

abbrev AddAction.ofEndHom {M : Type u_1} {α : Type u_3} [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