Mathlib.Algebra.GroupWithZero.Action.End

Function.Surjective.distribMulActionLeft abbrev

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

Full source

/-- 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`.
-/
abbrev Function.Surjective.distribMulActionLeft {R S M : Type*} [Monoid R] [AddMonoid M]
    [DistribMulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Function.Surjective f)
    (hsmul : ∀ (c) (x : M), f c • x = c • x) : DistribMulAction S M :=
  { hf.distribSMulLeft f hsmul, hf.mulActionLeft f hsmul with }

Pushforward of Distributive Multiplicative Action Along Surjective Homomorphism

Informal description

Let $R$ and $S$ be monoids, and $M$ be an additive monoid with a distributive multiplicative action of $R$ (i.e., $[DistribMulAction R M]$). Given a surjective monoid homomorphism $f \colon R \to S$ and a scalar multiplication operation $\bullet \colon S \times M \to M$ such that for all $c \in R$ and $x \in M$, we have $f(c) \bullet x = c \bullet x$, then $M$ inherits a distributive multiplicative action of $S$ via $f$.

DistribMulAction.compHom abbrev

[Monoid N] (f : N →* M) : DistribMulAction N A

Full source

/-- Compose a `DistribMulAction` with a `MonoidHom`, with action `f r' • m`.
See note [reducible non-instances]. -/
abbrev DistribMulAction.compHom [Monoid N] (f : N →* M) : DistribMulAction N A :=
  { DistribSMul.compFun A f, MulAction.compHom A f with }

Induced Distributive Multiplicative Action via Monoid Homomorphism

Informal description

Given a monoid $N$ and a monoid homomorphism $f \colon N \to M$, the distributive multiplicative action of $M$ on an additive monoid $A$ induces a distributive multiplicative action of $N$ on $A$ via composition with $f$. Specifically, for $n \in N$ and $a \in A$, the action is defined by $n \bullet a = f(n) \bullet a$.

MulDistribMulAction.compHom abbrev

[Monoid N] (f : N →* M) : MulDistribMulAction N A

Full source

/-- Compose a `MulDistribMulAction` with a `MonoidHom`, with action `f r' • m`.
See note [reducible non-instances]. -/
abbrev MulDistribMulAction.compHom [Monoid N] (f : N →* M) : MulDistribMulAction N A :=
  { MulAction.compHom A f with
    smul_one := fun x => smul_one (f x),
    smul_mul := fun x => smul_mul' (f x) }

Induced Multiplicative Distributive Action via Monoid Homomorphism

Informal description

Given monoids $M$ and $N$, and a monoid homomorphism $f \colon N \to M$, the composition of a multiplicative distributive action of $M$ on $A$ with $f$ yields a multiplicative distributive action of $N$ on $A$, where the action is defined by $n \bullet a = f(n) \bullet a$ for $n \in N$ and $a \in A$.

AddMonoid.End.applyDistribMulAction instance

[AddMonoid α] : DistribMulAction (AddMonoid.End α) α

Full source

/-- The tautological action by `AddMonoid.End α` on `α`.

This generalizes `Function.End.applyMulAction`. -/
instance AddMonoid.End.applyDistribMulAction [AddMonoid α] :
    DistribMulAction (AddMonoid.End α) α where
  smul := (· <| ·)
  smul_zero := AddMonoidHom.map_zero
  smul_add := AddMonoidHom.map_add
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Distributive Action of Additive Endomorphisms via Application

Informal description

For any additive monoid $\alpha$, the monoid of additive endomorphisms $\text{AddMonoid.End}(\alpha)$ acts distributively on $\alpha$ via function application. Specifically, for any endomorphism $f \in \text{AddMonoid.End}(\alpha)$ and element $a \in \alpha$, the action is defined by $f \bullet a = f(a)$.

AddMonoid.End.smul_def theorem

[AddMonoid α] (f : AddMonoid.End α) (a : α) : f • a = f a

Full source

@[simp]
theorem AddMonoid.End.smul_def [AddMonoid α] (f : AddMonoid.End α) (a : α) : f • a = f a :=
  rfl

Scalar multiplication by additive endomorphisms coincides with function application

Informal description

For any additive monoid $\alpha$, given an additive endomorphism $f \in \text{AddMonoid.End}(\alpha)$ and an element $a \in \alpha$, the scalar multiplication action of $f$ on $a$ is equal to the application of $f$ to $a$, i.e., $f \bullet a = f(a)$.

AddMonoid.End.applyFaithfulSMul instance

[AddMonoid α] : FaithfulSMul (AddMonoid.End α) α

Full source

/-- `AddMonoid.End.applyDistribMulAction` is faithful. -/
instance AddMonoid.End.applyFaithfulSMul [AddMonoid α] :
    FaithfulSMul (AddMonoid.End α) α :=
  ⟨fun {_ _ h} => AddMonoidHom.ext h⟩

Faithfulness of the Action of Additive Endomorphisms via Application

Informal description

For any additive monoid $\alpha$, the scalar multiplication action of the monoid of additive endomorphisms $\text{End}(\alpha)$ on $\alpha$ via function application is faithful. That is, distinct endomorphisms act differently on $\alpha$.

DistribMulAction.toAddEquiv₀ definition

 {α : Type*} (β : Type*) [GroupWithZero α] [AddMonoid β] [DistribMulAction α β] (x : α) (hx : x ≠ 0) : β ≃+ β

Full source

/-- 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`. -/
def DistribMulAction.toAddEquiv₀ {α : Type*} (β : Type*) [GroupWithZero α] [AddMonoid β]
    [DistribMulAction α β] (x : α) (hx : x ≠ 0) : β ≃+ β :=
  { DistribMulAction.toAddMonoidHom β x with
    invFun := fun b ↦ x⁻¹ • b
    left_inv := fun b ↦ inv_smul_smul₀ hx b
    right_inv := fun b ↦ smul_inv_smul₀ hx b }

Additive monoid isomorphism induced by a nonzero element of a group with zero

Informal description

Given a group with zero $\alpha$, an additive monoid $\beta$, and a distributive multiplicative action of $\alpha$ on $\beta$, each nonzero element $x \in \alpha$ defines an additive monoid isomorphism (additive equivalence) from $\beta$ to itself. The isomorphism maps each $b \in \beta$ to $x \cdot b$, and its inverse maps $b$ to $x^{-1} \cdot b$.