Group actions and (endo)morphisms

@[reducible, inline]

abbrev Function.Surjective.distribMulActionLeft {R : Type u_7} {S : Type u_8} {M : Type u_9} [Monoid R] [AddMonoid M] [DistribMulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : DistribMulAction S M

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

See also Function.Surjective.mulActionLeft and Function.Surjective.moduleLeft.

Equations

• Function.Surjective.distribMulActionLeft f hf hsmul = DistribMulAction.mk ⋯ ⋯

@[reducible, inline]

abbrev DistribMulAction.compHom {M : Type u_1} {N : Type u_2} (A : Type u_3) [AddMonoid A] [Monoid M] [DistribMulAction M A] [Monoid N] (f : N →* M) : DistribMulAction N A

Compose a DistribMulAction with a MonoidHom, with action f r' • m. See note [reducible non-instances].

Equations

• DistribMulAction.compHom A f = DistribMulAction.mk ⋯ ⋯

@[reducible, inline]

abbrev MulDistribMulAction.compHom {M : Type u_1} {N : Type u_2} (A : Type u_3) [Monoid A] [Monoid M] [MulDistribMulAction M A] [Monoid N] (f : N →* M) : MulDistribMulAction N A

Compose a MulDistribMulAction with a MonoidHom, with action f r' • m. See note [reducible non-instances].

Equations

• MulDistribMulAction.compHom A f = MulDistribMulAction.mk ⋯ ⋯

instance AddMonoid.End.applyDistribMulAction {α : Type u_5} [AddMonoid α] : DistribMulAction (AddMonoid.End α) α

The tautological action by AddMonoid.End α on α.

This generalizes Function.End.applyMulAction.

Equations

• AddMonoid.End.applyDistribMulAction = DistribMulAction.mk ⋯ ⋯

@[simp]

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

instance AddMonoid.End.applyFaithfulSMul {α : Type u_5} [AddMonoid α] : FaithfulSMul (AddMonoid.End α) α

AddMonoid.End.applyDistribMulAction is faithful.

Equations

• ⋯ = ⋯

def DistribMulAction.toAddEquiv₀ {α : Type u_7} (β : Type u_8) [GroupWithZero α] [AddMonoid β] [DistribMulAction α β] (x : α) (hx : x ≠ 0) : β ≃+ β

Each non-zero element of a GroupWithZero defines an additive monoid isomorphism of an AddMonoid on which it acts distributively. This is a stronger version of DistribMulAction.toAddMonoidHom.

Equations

• DistribMulAction.toAddEquiv₀ β x hx = { toFun := (↑(DistribMulAction.toAddMonoidHom β x)).toFun, invFun := fun (b : β) => x⁻¹ • b, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem MulDistribMulAction.toMonoidEnd_apply (M : Type u_1) (A : Type u_3) [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) : (MulDistribMulAction.toMonoidEnd M A) r = MulDistribMulAction.toMonoidHom A r

def MulDistribMulAction.toMonoidEnd (M : Type u_1) (A : Type u_3) [Monoid M] [Monoid A] [MulDistribMulAction M A] : M →* Monoid.End A

Each element of the monoid defines a monoid homomorphism.

Equations

• MulDistribMulAction.toMonoidEnd M A = { toFun := MulDistribMulAction.toMonoidHom A, map_one' := ⋯, map_mul' := ⋯ }