Instances on spaces of monoid and group morphisms

This file does two things involving AddMonoid.End and Ring. They are separate, and if someone would like to split this file in two that may be helpful.

• We provide the Ring structure on AddMonoid.End.
• Results about AddMonoid.End R when R is a ring.

instance AddMonoid.End.instAddMonoidWithOne (M : Type u_1) [AddCommMonoid M] : AddMonoidWithOne (AddMonoid.End M)

Equations

• AddMonoid.End.instAddMonoidWithOne M = AddMonoidWithOne.mk ⋯ ⋯

@[simp]

theorem AddMonoid.End.natCast_apply {M : Type uM} [AddCommMonoid M] (n : ℕ) (m : M) : ↑n m = n • m

See also AddMonoid.End.natCast_def.

@[simp]

theorem AddMonoid.End.ofNat_apply {M : Type uM} [AddCommMonoid M] (n : ℕ) [n.AtLeastTwo] (m : M) : (OfNat.ofNat n) m = n • m

instance AddMonoid.End.instSemiring {M : Type uM} [AddCommMonoid M] : Semiring (AddMonoid.End M)

Equations

• AddMonoid.End.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

instance AddMonoid.End.instRing {M : Type uM} [AddCommGroup M] : Ring (AddMonoid.End M)

Equations

• AddMonoid.End.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

Miscellaneous definitions

This file used to import Algebra.GroupPower.Basic, hence it was not possible to import it in some of the lower-level files like Algebra.Ring.Basic. The following lemmas should be rehomed now that Algebra.GroupPower.Basic was deleted.

def AddMonoidHom.mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ R →+ R

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.

Equations

• AddMonoidHom.mul = { toFun := AddMonoidHom.mulLeft, map_zero' := ⋯, map_add' := ⋯ }

theorem AddMonoidHom.mul_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : R) (y : R) : (AddMonoidHom.mul x) y = x * y

@[simp]

theorem AddMonoidHom.coe_mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : ⇑AddMonoidHom.mul = AddMonoidHom.mulLeft

@[simp]

theorem AddMonoidHom.coe_flip_mul {R : Type u_1} [NonUnitalNonAssocSemiring R] : ⇑AddMonoidHom.mul.flip = AddMonoidHom.mulRight

theorem AddMonoidHom.map_mul_iff {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →+ S) : (∀ (x y : R), f (x * y) = f x * f y) ↔ AddMonoidHom.mul.compr₂ f = (AddMonoidHom.mul.comp f).compl₂ f

An AddMonoidHom preserves multiplication if pre- and post- composition with AddMonoidHom.mul are equivalent. By converting the statement into an equality of AddMonoidHoms, this lemma allows various specialized ext lemmas about →+ to then be applied.

theorem AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute {R : Type u_1} [NonUnitalNonAssocSemiring R] {a : R} : AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ↔ ∀ (b : R), Commute a b

theorem AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute {R : Type u_1} [NonUnitalNonAssocSemiring R] {b : R} : AddMonoidHom.mulRight b = AddMonoidHom.mulLeft b ↔ ∀ (a : R), Commute a b

def AddMonoid.End.mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ AddMonoid.End R

The left multiplication map: (a, b) ↦ a * b. See also AddMonoidHom.mulLeft.

Equations

• AddMonoid.End.mulLeft = AddMonoidHom.mul

@[simp]

theorem AddMonoid.End.mulLeft_apply_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (r : R) : ∀ (x : R), (AddMonoid.End.mulLeft r) x = r * x

def AddMonoid.End.mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] : R →+ AddMonoid.End R

The right multiplication map: (a, b) ↦ b * a. See also AddMonoidHom.mulRight.

Equations

• AddMonoid.End.mulRight = AddMonoidHom.mul.flip

@[simp]

theorem AddMonoid.End.mulRight_apply_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (y : R) (x : R) : (AddMonoid.End.mulRight y) x = x * y

theorem AddMonoid.End.mulRight_eq_mulLeft {R : Type u_1} [NonUnitalNonAssocCommSemiring R] : AddMonoid.End.mulRight = AddMonoid.End.mulLeft