Group actions and (endo)morphisms

@[reducible, inline]

abbrev Function.Surjective.distribMulActionLeft {R : Type u_6} {S : Type u_7} {M : Type u_8} [Monoid R] [AddMonoid M] [DistribMulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : 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 = { toSMul := (Function.Surjective.distribSMulLeft (⇑f) hf hsmul).toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

@[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 = { toSMul := (DistribSMul.compFun A ⇑f).toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

@[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 = { toMulAction := MulAction.compHom A f, smul_one := ⋯, smul_mul := ⋯ }

@[instance_reducible]

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

The tautological action by AddMonoid.End α on α.

This generalizes Function.End.applyMulAction.

Equations

• AddMonoid.End.applyDistribMulAction = { smul := fun (x1 : AddMonoid.End α) (x2 : α) => x1 x2, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

@[simp]

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

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

AddMonoid.End.applyDistribMulAction is faithful.

def DistribMulAction.toAddEquiv₀ {α : Type u_6} (β : Type u_7) [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 DistribSMul.toAddMonoidHom.

Equations

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