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

@[reducible, inline]

abbrev Function.Surjective.addActionLeft {R : Type u_9} {S : Type u_10} {M : Type u_11} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S M] (f : R →+ S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) : AddAction S M

Push forward the action of R on M along a compatible surjective map f : R →+ S.

Equations

• Function.Surjective.addActionLeft f hf hsmul = AddAction.mk ⋯ ⋯

theorem Function.Surjective.addActionLeft.proof_2 {R : Type u_3} {S : Type u_2} {M : Type u_1} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S M] (f : R →+ S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) (y₁ : S) (y₂ : S) (b : M) : y₁ + y₂ +ᵥ b = y₁ +ᵥ (y₂ +ᵥ b)

theorem Function.Surjective.addActionLeft.proof_1 {R : Type u_3} {S : Type u_2} {M : Type u_1} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S M] (f : R →+ S) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) (b : M) : 0 +ᵥ b = b

@[reducible, inline]

abbrev Function.Surjective.mulActionLeft {R : Type u_9} {S : Type u_10} {M : Type u_11} [Monoid R] [MulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : MulAction S M

Push forward the action of R on M along a compatible surjective map f : R →* S.

See also Function.Surjective.distribMulActionLeft and Function.Surjective.moduleLeft.

Equations

• Function.Surjective.mulActionLeft f hf hsmul = MulAction.mk ⋯ ⋯

theorem AddAction.compHom.proof_1 {M : Type u_3} {N : Type u_2} (α : Type u_1) [AddMonoid M] [AddAction M α] [AddMonoid N] (g : N →+ M) : ∀ (x : α), 0 +ᵥ x = x

@[reducible, inline]

abbrev AddAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_5) [AddMonoid M] [AddAction M α] [AddMonoid N] (g : N →+ M) : AddAction N α

An additive action of M on α and an additive monoid homomorphism N → M induce an additive action of N on α.

See note [reducible non-instances].

Equations

• AddAction.compHom α g = AddAction.mk ⋯ ⋯

theorem AddAction.compHom.proof_2 {M : Type u_3} {N : Type u_2} (α : Type u_1) [AddMonoid M] [AddAction M α] [AddMonoid N] (g : N →+ M) : ∀ (x x_1 : N) (x_2 : α), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)

@[reducible, inline]

abbrev MulAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_5) [Monoid M] [MulAction M α] [Monoid N] (g : N →* M) : MulAction N α

A multiplicative action of M on α and a monoid homomorphism N → M induce a multiplicative action of N on α.

See note [reducible non-instances].

Equations

• MulAction.compHom α g = MulAction.mk ⋯ ⋯

theorem AddAction.compHom_vadd_def {E : Type u_9} {F : Type u_10} {G : Type u_11} [AddMonoid E] [AddMonoid F] [AddAction F G] (f : E →+ F) (a : E) (x : G) : a +ᵥ x = f a +ᵥ x

theorem MulAction.compHom_smul_def {E : Type u_9} {F : Type u_10} {G : Type u_11} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) : a • x = f a • x

theorem AddMonoidHom.vaddZeroHom.proof_1 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddZeroClass N] [AddAction M N] : 0 +ᵥ 0 = 0

def AddMonoidHom.vaddZeroHom {M : Type u_9} {N : Type u_10} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] : M →+ N

If the additive action of M on N is compatible with addition on N, then fun x ↦ x +ᵥ 0 is an additive monoid homomorphism from M to N.

Equations

• AddMonoidHom.vaddZeroHom = { toFun := fun (x : M) => x +ᵥ 0, map_zero' := ⋯, map_add' := ⋯ }

theorem AddMonoidHom.vaddZeroHom.proof_2 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] (x : M) (y : M) : { toFun := fun (x : M) => x +ᵥ 0, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (x : M) => x +ᵥ 0, map_zero' := ⋯ }.toFun x + { toFun := fun (x : M) => x +ᵥ 0, map_zero' := ⋯ }.toFun y

@[simp]

theorem MonoidHom.smulOneHom_apply {M : Type u_9} {N : Type u_10} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] (x : M) : MonoidHom.smulOneHom x = x • 1

@[simp]

theorem AddMonoidHom.vaddZeroHom_apply {M : Type u_9} {N : Type u_10} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] (x : M) : AddMonoidHom.vaddZeroHom x = x +ᵥ 0

def MonoidHom.smulOneHom {M : Type u_9} {N : Type u_10} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] : M →* N

If the multiplicative action of M on N is compatible with multiplication on N, then fun x ↦ x • 1 is a monoid homomorphism from M to N.

Equations

• MonoidHom.smulOneHom = { toFun := fun (x : M) => x • 1, map_one' := ⋯, map_mul' := ⋯ }

theorem addMonoidHomEquivAddActionIsScalarTower.proof_2 (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] (f : M →+ N) : (fun (x : { _inst : AddAction M N // VAddAssocClass M N N }) => match x with | ⟨val, property⟩ => AddMonoidHom.vaddZeroHom) ((fun (f : M →+ N) => ⟨AddAction.compHom N f, ⋯⟩) f) = f

def addMonoidHomEquivAddActionIsScalarTower (M : Type u_9) (N : Type u_10) [AddMonoid M] [AddMonoid N] : (M →+ N) ≃ { _inst : AddAction M N // VAddAssocClass M N N }

A monoid homomorphism between two additive monoids M and N can be equivalently specified by an additive action of M on N that is compatible with the addition on N.

Equations

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

theorem addMonoidHomEquivAddActionIsScalarTower.proof_3 (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] : ∀ (x : { _inst : AddAction M N // VAddAssocClass M N N }), (fun (f : M →+ N) => ⟨AddAction.compHom N f, ⋯⟩) ((fun (x : { _inst : AddAction M N // VAddAssocClass M N N }) => match x with | ⟨val, property⟩ => AddMonoidHom.vaddZeroHom) x) = x

theorem addMonoidHomEquivAddActionIsScalarTower.proof_1 (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] (f : M →+ N) : VAddAssocClass M N N

def monoidHomEquivMulActionIsScalarTower (M : Type u_9) (N : Type u_10) [Monoid M] [Monoid N] : (M →* N) ≃ { _inst : MulAction M N // IsScalarTower M N N }

A monoid homomorphism between two monoids M and N can be equivalently specified by a multiplicative action of M on N that is compatible with the multiplication on N.

Equations

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

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

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_5) : Monoid (Function.End α)

Equations

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

instance instInhabitedEnd (α : Type u_5) : Inhabited (Function.End α)

Equations

• instInhabitedEnd α = { default := 1 }

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

Equations

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

@[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 : Function.End α) (g : Function.End α) : f * g = f ∘ g

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

def MulAction.toEndHom {M : Type u_1} {α : 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_1} {α : 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