Mathlib.Algebra.Module.End

AddMonoid.End.natCast_def theorem

(n : ℕ) : (↑n : AddMonoid.End M) = DistribMulAction.toAddMonoidEnd ℕ M n

Full source

theorem AddMonoid.End.natCast_def (n : ℕ) :
    (↑n : AddMonoid.End M) = DistribMulAction.toAddMonoidEnd ℕ M n :=
  rfl

Natural Number Cast as Scalar Multiplication Endomorphism

Informal description

For any natural number $n$ and any additive commutative monoid $M$, the canonical map from $\mathbb{N}$ to the endomorphism ring $\text{End}(M)$ sends $n$ to the endomorphism given by scalar multiplication by $n$, i.e., $\uparrow n = (n \cdot -) \in \text{End}(M)$.

Module.toAddMonoidEnd definition

: R →+* AddMonoid.End M

Full source

/-- `(•)` as an `AddMonoidHom`.

This is a stronger version of `DistribMulAction.toAddMonoidEnd` -/
@[simps! apply_apply]
def Module.toAddMonoidEnd : R →+* AddMonoid.End M :=
  { DistribMulAction.toAddMonoidEnd R M with
    map_zero' := AddMonoidHom.ext fun r => by simp
    map_add' x y :=
      AddMonoidHom.ext fun r => by simp [(AddMonoidHom.add_apply), add_smul] }

Scalar multiplication as an endomorphism ring homomorphism

Informal description

The scalar multiplication operation `(•)` as a monoid homomorphism from the semiring `R` to the endomorphism ring of the additive commutative monoid `M`. This homomorphism maps each scalar `r ∈ R` to the endomorphism `(r • -) : M → M`.

smulAddHom definition

: R →+ M →+ M

Full source

/-- A convenience alias for `Module.toAddMonoidEnd` as an `AddMonoidHom`, usually to allow the
use of `AddMonoidHom.flip`. -/
def smulAddHom : R →+ M →+ M :=
  (Module.toAddMonoidEnd R M).toAddMonoidHom

Scalar multiplication as additive monoid homomorphism

Informal description

The additive monoid homomorphism version of the scalar multiplication operation, mapping each scalar $r \in R$ to the additive monoid endomorphism $(r \cdot -) : M \to M$. This is a bundled version of the map that sends $r$ to the function $x \mapsto r \cdot x$.

smulAddHom_apply theorem

: smulAddHom R M r x = r • x

Full source

@[simp]
theorem smulAddHom_apply : smulAddHom R M r x = r • x :=
  rfl

Scalar Multiplication Homomorphism Application: $\text{smulAddHom}(r)(x) = r \cdot x$

Informal description

For a scalar $r$ in a ring $R$ and an element $x$ in an $R$-module $M$, the application of the scalar multiplication homomorphism $\text{smulAddHom}$ satisfies $\text{smulAddHom}(r)(x) = r \cdot x$.

IsAddUnit.smul_left theorem

[Monoid S] [DistribMulAction S M] (hx : IsAddUnit x) (s : S) : IsAddUnit (s • x)

Full source

lemma IsAddUnit.smul_left [Monoid S] [DistribMulAction S M] (hx : IsAddUnit x) (s : S) :
    IsAddUnit (s • x) :=
  hx.map (DistribMulAction.toAddMonoidHom M s)

Scalar Multiplication Preserves Additive Units (Left Version)

Informal description

Let $S$ be a monoid acting distributively on an additive commutative monoid $M$. If $x \in M$ is an additive unit (i.e., has an additive inverse), then for any $s \in S$, the scalar multiple $s \cdot x$ is also an additive unit.

IsAddUnit.smul_right theorem

(hr : IsAddUnit r) : IsAddUnit (r • x)

Full source

lemma IsAddUnit.smul_right (hr : IsAddUnit r) : IsAddUnit (r • x) :=
  hr.map (AddMonoidHom.flip (smulAddHom R M) x)

Scalar Multiplication Preserves Additive Units

Informal description

If $r$ is an additive unit (i.e., has an additive inverse), then the scalar multiplication $r \cdot x$ is also an additive unit for any $x$ in the module $M$.

AddMonoid.End.intCast_def theorem

(z : ℤ) : (↑z : AddMonoid.End M) = DistribMulAction.toAddMonoidEnd ℤ M z

Full source

theorem AddMonoid.End.intCast_def (z : ℤ) :
    (↑z : AddMonoid.End M) = DistribMulAction.toAddMonoidEnd ℤ M z :=
  rfl

Integer Scalar Multiplication as Module Endomorphism

Informal description

For any integer $z \in \mathbb{Z}$ and any additive commutative group $M$, the canonical integer scalar multiplication endomorphism $\uparrow z \in \text{End}(M)$ is equal to the monoid homomorphism induced by the $\mathbb{Z}$-module structure on $M$, i.e., $\uparrow z = \text{DistribMulAction.toAddMonoidEnd}_{\mathbb{Z}}(M)(z)$.

Int.cast_smul_eq_zsmul theorem

(n : ℤ) (b : M) : (n : R) • b = n • b

Full source

/-- `zsmul` is equal to any other module structure via a cast. -/
@[norm_cast]
lemma Int.cast_smul_eq_zsmul (n : ℤ) (b : M) : (n : R) • b = n • b :=
  have : ((smulAddHom R M).flip b).comp (Int.castAddHom R) = (smulAddHom ℤ M).flip b := by
    apply AddMonoidHom.ext_int
    simp
  DFunLike.congr_fun this n

Equality of Cast Integer Scalar Multiplication and $\mathbb{Z}$-module Scalar Multiplication

Informal description

For any integer $n \in \mathbb{Z}$ and any element $b$ in an additive commutative group $M$ with a $\mathbb{Z}$-module structure, the scalar multiplication $(n : R) \cdot b$ (where $n$ is cast to $R$) is equal to the integer scalar multiplication $n \cdot b$ defined by the $\mathbb{Z}$-module structure.

int_smul_eq_zsmul theorem

(h : Module ℤ M) (n : ℤ) (x : M) : @SMul.smul ℤ M h.toSMul n x = n • x

Full source

/-- Convert back any exotic `ℤ`-smul to the canonical instance. This should not be needed since in
mathlib all `AddCommGroup`s should normally have exactly one `ℤ`-module structure by design. -/
theorem int_smul_eq_zsmul (h : Module ℤ M) (n : ℤ) (x : M) : @SMul.smul ℤ M h.toSMul n x = n • x :=
  Int.cast_smul_eq_zsmul ..

Equality of Scalar Multiplications in $\mathbb{Z}$-module Structures

Informal description

For any $\mathbb{Z}$-module structure $h$ on an additive commutative group $M$, any integer $n \in \mathbb{Z}$, and any element $x \in M$, the scalar multiplication $n \cdot x$ defined by $h$ is equal to the integer scalar multiplication $n \cdot x$ defined by the canonical $\mathbb{Z}$-module structure on $M$.

AddCommGroup.uniqueIntModule definition

: Unique (Module ℤ M)

Full source

/-- All `ℤ`-module structures are equal. Not an instance since in mathlib all `AddCommGroup`
should normally have exactly one `ℤ`-module structure by design. -/
def AddCommGroup.uniqueIntModule : Unique (Module ℤ M) where
  default := by infer_instance
  uniq P := (Module.ext' P _) fun n => by convert int_smul_eq_zsmul P n

Uniqueness of $\mathbb{Z}$-module structure on additive commutative groups

Informal description

For any additive commutative group $M$, there is a unique $\mathbb{Z}$-module structure on $M$, where the scalar multiplication is given by the group's addition structure.

map_intCast_smul theorem

 [AddCommGroup M] [AddCommGroup M₂] {F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R S : Type*)
  [Ring R] [Ring S] [Module R M] [Module S M₂] (x : ℤ) (a : M) : f ((x : R) • a) = (x : S) • f a

Full source

theorem map_intCast_smul [AddCommGroup M] [AddCommGroup M₂] {F : Type*} [FunLike F M M₂]
    [AddMonoidHomClass F M M₂] (f : F) (R S : Type*) [Ring R] [Ring S] [Module R M] [Module S M₂]
    (x : ℤ) (a : M) :
    f ((x : R) • a) = (x : S) • f a := by simp only [Int.cast_smul_eq_zsmul, map_zsmul]

Compatibility of Integer Scalar Multiplication with Additive Monoid Homomorphisms

Informal description

Let $M$ and $M₂$ be additive commutative groups, and let $F$ be a type of functions from $M$ to $M₂$ that are additive monoid homomorphisms. Given rings $R$ and $S$ with module structures on $M$ and $M₂$ respectively, for any integer $x \in \mathbb{Z}$ and any element $a \in M$, we have: \[ f((x : R) \cdot a) = (x : S) \cdot f(a) \] where $(x : R)$ denotes the canonical ring homomorphism from $\mathbb{Z}$ to $R$, and similarly for $(x : S)$.

AddCommGroup.intIsScalarTower instance

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

Full source

instance AddCommGroup.intIsScalarTower {R : Type u} {M : Type v} [Ring R] [AddCommGroup M]
    [Module R M] : IsScalarTower ℤ R M where
  smul_assoc n x y := ((smulAddHom R M).flip y).map_zsmul x n

Integer Scalar Multiplication Tower Property for Modules

Informal description

For any ring $R$ and additive commutative group $M$ equipped with an $R$-module structure, the scalar multiplication by integers on $M$ forms a scalar tower with the $R$-module structure. That is, for any integer $n \in \mathbb{Z}$, ring element $r \in R$, and module element $x \in M$, we have $n \cdot (r \cdot x) = (n \cdot r) \cdot x = r \cdot (n \cdot x)$.