Mathlib.Algebra.Group.Hom.End

AddMonoid.End.instAddMonoidWithOne instance

(M) [AddCommMonoid M] : AddMonoidWithOne (AddMonoid.End M)

Full source

instance instAddMonoidWithOne (M) [AddCommMonoid M] : AddMonoidWithOne (AddMonoid.End M) where
  natCast n := n • (1 : AddMonoid.End M)
  natCast_zero := AddMonoid.nsmul_zero _
  natCast_succ n := AddMonoid.nsmul_succ n 1

Additive Monoid with One Structure on Endomorphism Ring

Informal description

For any additive commutative monoid $M$, the endomorphism ring $\text{End}(M)$ is an additive monoid with one, where the additive structure is given by pointwise addition of endomorphisms and the multiplicative identity is the identity endomorphism.

AddMonoid.End.natCast_apply theorem

[AddCommMonoid M] (n : ℕ) (m : M) : (↑n : AddMonoid.End M) m = n • m

Full source

/-- See also `AddMonoid.End.natCast_def`. -/
@[simp]
lemma natCast_apply [AddCommMonoid M] (n : ℕ) (m : M) : (↑n : AddMonoid.End M) m = n • m := rfl

Natural Number as Endomorphism Acts by Repeated Addition

Informal description

For any additive commutative monoid $M$, a natural number $n$, and an element $m \in M$, the action of the natural number $n$ (viewed as an endomorphism in $\text{End}(M)$) on $m$ is equal to the $n$-fold addition of $m$, i.e., $n \cdot m$.

AddMonoid.End.ofNat_apply theorem

[AddCommMonoid M] (n : ℕ) [n.AtLeastTwo] (m : M) : (ofNat(n) : AddMonoid.End M) m = n • m

Full source

@[simp] lemma ofNat_apply [AddCommMonoid M] (n : ℕ) [n.AtLeastTwo] (m : M) :
    (ofNat(n) : AddMonoid.End M) m = n • m := rfl

Action of Numeric Endomorphism as Repeated Addition for $n \geq 2$

Informal description

For any additive commutative monoid $M$, natural number $n \geq 2$, and element $m \in M$, the action of the natural number $n$ (interpreted as an endomorphism in $\text{End}(M)$ via the `OfNat` instance) on $m$ equals the $n$-fold addition of $m$, i.e., $(n : \text{End}(M))(m) = n \cdot m$.

AddMonoid.End.instSemiring instance

[AddCommMonoid M] : Semiring (AddMonoid.End M)

Full source

instance instSemiring [AddCommMonoid M] : Semiring (AddMonoid.End M) :=
  { AddMonoid.End.instMonoid M,
    AddMonoidHom.instAddCommMonoid,
    AddMonoid.End.instAddMonoidWithOne M with
    zero_mul := fun _ => AddMonoidHom.ext fun _ => rfl,
    mul_zero := fun _ => AddMonoidHom.ext fun _ => AddMonoidHom.map_zero _,
    left_distrib := fun _ _ _ => AddMonoidHom.ext fun _ => AddMonoidHom.map_add _ _ _,
    right_distrib := fun _ _ _ => AddMonoidHom.ext fun _ => rfl }

Semiring Structure on Endomorphism Ring of an Additive Commutative Monoid

Informal description

For any additive commutative monoid $M$, the endomorphism ring $\text{End}(M)$ is a semiring. The additive structure is given by pointwise addition of endomorphisms, the multiplicative structure is given by composition of endomorphisms, and the multiplicative identity is the identity endomorphism.

AddMonoid.End.instRing instance

[AddCommGroup M] : Ring (AddMonoid.End M)

Full source

instance instRing [AddCommGroup M] : Ring (AddMonoid.End M) :=
  { AddMonoid.End.instSemiring, AddMonoid.End.instAddCommGroup with
    intCast := fun z => z • (1 : AddMonoid.End M),
    intCast_ofNat := natCast_zsmul _,
    intCast_negSucc := negSucc_zsmul _ }

Ring Structure on Endomorphism Ring of an Additive Commutative Group

Informal description

For any additive commutative group $M$, the endomorphism ring $\text{End}(M)$ is a ring. The additive structure is given by pointwise addition of endomorphisms, the multiplicative structure is given by composition of endomorphisms, and the multiplicative identity is the identity endomorphism.

AddMonoidHom.mul definition

: R →+ R →+ R

Full source

/-- Multiplication of an element of a (semi)ring is an `AddMonoidHom` in both arguments.

This is a more-strongly bundled version of `AddMonoidHom.mulLeft` and `AddMonoidHom.mulRight`.

Stronger versions of this exists for algebras as `LinearMap.mul`, `NonUnitalAlgHom.mul`
and `Algebra.lmul`.
-/
def AddMonoidHom.mul : R →+ R →+ R where
  toFun := AddMonoidHom.mulLeft
  map_zero' := AddMonoidHom.ext <| zero_mul
  map_add' a b := AddMonoidHom.ext <| add_mul a b

Bundled left multiplication as additive monoid homomorphism

Informal description

The function maps an element $ r $ of a (semi)ring $ R $ to the additive monoid homomorphism $ \text{AddMonoidHom.mulLeft}(r) $, which represents left multiplication by $ r $. This function is itself an additive monoid homomorphism from $ R $ to $ R \to^+ R $. More precisely, for any $ r \in R $, the function $ \text{AddMonoidHom.mul}(r) $ is the additive monoid homomorphism sending $ s \in R $ to $ r \cdot s $, and the map $ r \mapsto \text{AddMonoidHom.mul}(r) $ is an additive monoid homomorphism.

AddMonoidHom.mul_apply theorem

(x y : R) : AddMonoidHom.mul x y = x * y

Full source

theorem AddMonoidHom.mul_apply (x y : R) : AddMonoidHom.mul x y = x * y :=
  rfl

Application of Multiplication Homomorphism Equals Ring Multiplication

Informal description

For any elements $x$ and $y$ in a (semi)ring $R$, the application of the additive monoid homomorphism $\text{AddMonoidHom.mul}(x)$ to $y$ equals the product $x \cdot y$.

AddMonoidHom.coe_mul theorem

: ⇑(AddMonoidHom.mul : R →+ R →+ R) = AddMonoidHom.mulLeft

Full source

@[simp]
theorem AddMonoidHom.coe_mul : ⇑(AddMonoidHom.mul : R →+ R →+ R) = AddMonoidHom.mulLeft :=
  rfl

Underlying Function of Multiplication Homomorphism Equals Left Multiplication

Informal description

The underlying function of the additive monoid homomorphism `AddMonoidHom.mul` from a (semi)ring $R$ to the additive monoid of endomorphisms of $R$ is equal to the left multiplication function `AddMonoidHom.mulLeft`. More precisely, for any $r \in R$, the function `AddMonoidHom.mul(r)` is the additive monoid homomorphism that sends $s \in R$ to $r \cdot s$, and the map $r \mapsto \text{AddMonoidHom.mul}(r)$ is itself an additive monoid homomorphism. The theorem states that the underlying function of this homomorphism coincides with the left multiplication function.

AddMonoidHom.coe_flip_mul theorem

: ⇑(AddMonoidHom.mul : R →+ R →+ R).flip = AddMonoidHom.mulRight

Full source

@[simp]
theorem AddMonoidHom.coe_flip_mul :
    ⇑(AddMonoidHom.mul : R →+ R →+ R).flip = AddMonoidHom.mulRight :=
  rfl

Flipped Multiplication Homomorphism Equals Right Multiplication

Informal description

The underlying function of the flipped additive monoid homomorphism `AddMonoidHom.mul` from a (semi)ring $R$ to the additive monoid of endomorphisms of $R$ is equal to the right multiplication function `AddMonoidHom.mulRight`. More precisely, for any $r \in R$, the function `AddMonoidHom.mul(r)` is the additive monoid homomorphism that sends $s \in R$ to $r \cdot s$, and the map $r \mapsto \text{AddMonoidHom.mul}(r)$ is itself an additive monoid homomorphism. The theorem states that when we flip the arguments of this homomorphism (i.e., consider $s \mapsto r \mapsto r \cdot s$), the resulting function coincides with the right multiplication function.

AddMonoidHom.map_mul_iff theorem

 (f : R →+ S) :
  (∀ x y, f (x * y) = f x * f y) ↔ (AddMonoidHom.mul : R →+ R →+ R).compr₂ f = (AddMonoidHom.mul.comp f).compl₂ f

Full source

/-- An `AddMonoidHom` preserves multiplication if pre- and post- composition with
`AddMonoidHom.mul` are equivalent. By converting the statement into an equality of
`AddMonoidHom`s, this lemma allows various specialized `ext` lemmas about `→+` to then be applied.
-/
theorem AddMonoidHom.map_mul_iff (f : R →+ S) :
    (∀ x y, f (x * y) = f x * f y) ↔
      (AddMonoidHom.mul : R →+ R →+ R).compr₂ f = (AddMonoidHom.mul.comp f).compl₂ f :=
  Iff.symm AddMonoidHom.ext_iff₂

Characterization of Multiplicative Preserving Additive Monoid Homomorphisms via Commuting Diagram

Informal description

Let $R$ and $S$ be semirings and $f : R \to^+ S$ be an additive monoid homomorphism. Then $f$ preserves multiplication (i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in R$) if and only if the following diagram commutes: \[ \text{AddMonoidHom.mul} \circ f = f \circ \text{AddMonoidHom.mul} \] where $\text{AddMonoidHom.mul} : R \to^+ R \to^+ R$ is the bundled left multiplication homomorphism, and the equality is interpreted as an equality of additive monoid homomorphisms.

AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute theorem

{a : R} : mulLeft a = mulRight a ↔ ∀ b, Commute a b

Full source

lemma AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute {a : R} :
    mulLeftmulLeft a = mulRight a ↔ ∀ b, Commute a b :=
  DFunLike.ext_iff

Equality of Left and Right Multiplication Homomorphisms Characterizes Central Elements

Informal description

For any element $a$ in a (semi)ring $R$, the left multiplication homomorphism $\text{mulLeft}(a)$ equals the right multiplication homomorphism $\text{mulRight}(a)$ if and only if $a$ commutes with every element $b \in R$.

AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute theorem

{b : R} : mulRight b = mulLeft b ↔ ∀ a, Commute a b

Full source

lemma AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute {b : R} :
    mulRightmulRight b = mulLeft b ↔ ∀ a, Commute a b :=
  DFunLike.ext_iff

Equality of Right and Left Multiplication Maps via Commutativity

Informal description

For any element $b$ in a semiring $R$, the right multiplication map by $b$ equals the left multiplication map by $b$ if and only if $a$ commutes with $b$ for all $a \in R$.

AddMonoid.End.mulLeft definition

: R →+ AddMonoid.End R

Full source

/-- The left multiplication map: `(a, b) ↦ a * b`. See also `AddMonoidHom.mulLeft`. -/
@[simps!]
def AddMonoid.End.mulLeft : R →+ AddMonoid.End R :=
  AddMonoidHom.mul

Left multiplication as an additive monoid homomorphism

Informal description

The left multiplication map is an additive monoid homomorphism from a (semi)ring $ R $ to the endomorphism ring of its additive monoid, $ \text{End}(R) $. For each $ r \in R $, it sends $ r $ to the endomorphism $ \text{End.mulLeft}(r) $ defined by $ x \mapsto r \cdot x $. More precisely, the map $ r \mapsto (x \mapsto r \cdot x) $ is an additive monoid homomorphism from $ R $ to $ \text{End}(R) $.

AddMonoid.End.mulRight definition

: R →+ AddMonoid.End R

Full source

/-- The right multiplication map: `(a, b) ↦ b * a`. See also `AddMonoidHom.mulRight`. -/
@[simps!]
def AddMonoid.End.mulRight : R →+ AddMonoid.End R :=
  (AddMonoidHom.mul : R →+ AddMonoid.End R).flip

Right multiplication as an additive monoid homomorphism

Informal description

The right multiplication map is an additive monoid homomorphism from a (semi)ring $ R $ to the endomorphism ring of its additive monoid, $ \text{AddMonoid.End}(R) $. For each $ r \in R $, it sends $ r $ to the endomorphism $ \text{AddMonoid.End.mulRight}(r) $ defined by $ x \mapsto x \cdot r $.

AddMonoid.End.mulRight_eq_mulLeft theorem

: mulRight = (mulLeft : R →+ AddMonoid.End R)

Full source

lemma mulRight_eq_mulLeft : mulRight = (mulLeft : R →+ AddMonoid.End R) :=
  AddMonoidHom.ext fun _ =>
    Eq.symm <| AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute.2 (.all _)

Equality of Left and Right Multiplication Homomorphisms in Endomorphism Ring

Informal description

The right multiplication homomorphism $\text{mulRight}$ from a (semi)ring $R$ to its endomorphism ring $\text{AddMonoid.End}(R)$ is equal to the left multiplication homomorphism $\text{mulLeft}$.