Module structure and endomorphisms

In this file, we define Module.toAddMonoidEnd, which is (•) as a monoid homomorphism. We use this to prove some results on scalar multiplication by integers.

theorem AddMonoid.End.natCast_def {M : Type u_3} [AddCommMonoid M] (n : ℕ) : ↑n = (DistribMulAction.toAddMonoidEnd ℕ M) n

def Module.toAddMonoidEnd (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] : R →+* AddMonoid.End M

(•) as an AddMonoidHom.

This is a stronger version of DistribMulAction.toAddMonoidEnd

Equations

• Module.toAddMonoidEnd R M = { toMonoidHom := DistribMulAction.toAddMonoidEnd R M, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Module.toAddMonoidEnd_apply_apply (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] (x : R) (x✝ : M) : ((toAddMonoidEnd R M) x) x✝ = x • x✝

def smulAddHom (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] : R →+ M →+ M

A convenience alias for Module.toAddMonoidEnd as an AddMonoidHom, usually to allow the use of AddMonoidHom.flip.

Equations

• smulAddHom R M = (Module.toAddMonoidEnd R M).toAddMonoidHom

@[simp]

theorem smulAddHom_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (r : R) (x : M) : ((smulAddHom R M) r) x = r • x

theorem IsAddUnit.smul_left {S : Type u_2} {M : Type u_3} [AddCommMonoid M] {x : M} [Monoid S] [DistribMulAction S M] (hx : IsAddUnit x) (s : S) : IsAddUnit (s • x)

theorem IsAddUnit.smul_right {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} (x : M) (hr : IsAddUnit r) : IsAddUnit (r • x)

theorem AddMonoid.End.intCast_def (M : Type u_3) [AddCommGroup M] (z : ℤ) : ↑z = (DistribMulAction.toAddMonoidEnd ℤ M) z

theorem Int.cast_smul_eq_zsmul (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (n : ℤ) (b : M) : ↑n • b = n • b

zsmul is equal to any other module structure via a cast.

theorem int_smul_eq_zsmul {M : Type u_3} [AddCommGroup M] (h : Module ℤ M) (n : ℤ) (x : M) : SMul.smul n x = n • x

Convert back any exotic ℤ-smul to the canonical instance. This should not be needed since in mathlib all AddCommGroups should normally have exactly one ℤ-module structure by design.

def AddCommGroup.uniqueIntModule {M : Type u_3} [AddCommGroup M] : Unique (Module ℤ M)

All ℤ-module structures are equal. Not an instance since in mathlib all AddCommGroup should normally have exactly one ℤ-module structure by design.

Equations

• AddCommGroup.uniqueIntModule = { default := inferInstance, uniq := ⋯ }

theorem map_intCast_smul {M : Type u_3} {M₂ : Type u_4} [AddCommGroup M] [AddCommGroup M₂] {F : Type u_5} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7) [Ring R] [Ring S] [Module R M] [Module S M₂] (x : ℤ) (a : M) : f (↑x • a) = ↑x • f a

instance AddCommGroup.intIsScalarTower {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] : IsScalarTower ℤ R M