Mathlib.Algebra.Module.Hom

AddMonoidHom.instDistribSMul instance

[AddZeroClass A] [AddCommMonoid B] [DistribSMul M B] : DistribSMul M (A →+ B)

Full source

instance instDistribSMul [AddZeroClass A] [AddCommMonoid B] [DistribSMul M B] :
    DistribSMul M (A →+ B) where
  smul_add _ _ _ := ext fun _ => smul_add _ _ _

Distributive Scalar Multiplication on Additive Monoid Homomorphisms

Informal description

For any additive zero class $A$ and additive commutative monoid $B$ equipped with a distributive scalar multiplication by $M$, the type of additive monoid homomorphisms from $A$ to $B$ inherits a distributive scalar multiplication structure from $M$.

AddMonoidHom.instDistribMulAction instance

: DistribMulAction R (A →+ B)

Full source

instance instDistribMulAction : DistribMulAction R (A →+ B) where
  smul_zero := smul_zero
  smul_add := smul_add
  one_smul _ := ext fun _ => one_smul _ _
  mul_smul _ _ _ := ext fun _ => mul_smul _ _ _

Distributive Multiplicative Action on Additive Monoid Homomorphisms

Informal description

For any additive monoid $A$ and any additive commutative monoid $B$ with a distributive scalar multiplication by $R$, the type of additive monoid homomorphisms $A \to B$ inherits a distributive multiplicative action structure from $R$.

AddMonoidHom.coe_smul theorem

(r : R) (f : A →+ B) : ⇑(r • f) = r • ⇑f

Full source

@[simp] theorem coe_smul (r : R) (f : A →+ B) : ⇑(r • f) = r • ⇑f := rfl

Scalar Multiplication of Additive Monoid Homomorphisms is Pointwise

Informal description

For any scalar $r$ in $R$ and any additive monoid homomorphism $f \colon A \to B$, the underlying function of the scalar multiple $r \cdot f$ is equal to the pointwise scalar multiple of the underlying function of $f$, i.e., $(r \cdot f)(x) = r \cdot f(x)$ for all $x \in A$.

AddMonoidHom.smul_apply theorem

(r : R) (f : A →+ B) (x : A) : (r • f) x = r • f x

Full source

theorem smul_apply (r : R) (f : A →+ B) (x : A) : (r • f) x = r • f x :=
  rfl

Scalar Multiplication Commutes with Evaluation of Additive Monoid Homomorphisms

Informal description

For any scalar $r$ in $R$, any additive monoid homomorphism $f \colon A \to B$, and any element $x \in A$, the evaluation of the scalar multiple $r \cdot f$ at $x$ equals the scalar multiple of the evaluation of $f$ at $x$, i.e., $(r \cdot f)(x) = r \cdot f(x)$.

AddMonoidHom.smulCommClass instance

[SMulCommClass R S B] : SMulCommClass R S (A →+ B)

Full source

instance smulCommClass [SMulCommClass R S B] : SMulCommClass R S (A →+ B) :=
  ⟨fun _ _ _ => ext fun _ => smul_comm _ _ _⟩

Commutativity of Scalar Actions on Additive Monoid Homomorphisms

Informal description

For any additive commutative monoids $A$ and $B$, and any scalar actions of $R$ and $S$ on $B$ that commute with each other, the scalar actions of $R$ and $S$ on the additive monoid homomorphisms from $A$ to $B$ also commute. That is, for any $r \in R$, $s \in S$, and $f \colon A \to B$, we have $r \cdot (s \cdot f) = s \cdot (r \cdot f)$.

AddMonoidHom.isScalarTower instance

[SMul R S] [IsScalarTower R S B] : IsScalarTower R S (A →+ B)

Full source

instance isScalarTower [SMul R S] [IsScalarTower R S B] : IsScalarTower R S (A →+ B) :=
  ⟨fun _ _ _ => ext fun _ => smul_assoc _ _ _⟩

Scalar Multiplication Tower Property for Additive Monoid Homomorphisms

Informal description

For any additive monoids $A$ and $B$, if $B$ has a scalar multiplication tower structure with scalars $R$ and $S$ (i.e., $R$ acts on $S$ and $S$ acts on $B$ in a compatible way), then the space of additive monoid homomorphisms $A \to B$ also forms a scalar multiplication tower with the same scalars $R$ and $S$. More precisely, for any $r \in R$, $s \in S$, and $f \in (A \to+ B)$, the scalar multiplications satisfy $(r \cdot s) \cdot f = r \cdot (s \cdot f)$.

AddMonoidHom.isCentralScalar instance

[DistribMulAction Rᵐᵒᵖ B] [IsCentralScalar R B] : IsCentralScalar R (A →+ B)

Full source

instance isCentralScalar [DistribMulAction Rᵐᵒᵖ B] [IsCentralScalar R B] :
    IsCentralScalar R (A →+ B) :=
  ⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

Central Scalar Action on Additive Monoid Homomorphisms

Informal description

For any additive monoids $A$ and $B$, if $B$ has a right scalar action by the multiplicative opposite $R^\text{op}$ and the scalar actions of $R$ and $R^\text{op}$ on $B$ are central (i.e., they coincide), then the space of additive monoid homomorphisms $A \to B$ also has a central scalar action by $R$.

AddMonoidHom.instModule instance

[Semiring R] [AddMonoid A] [AddCommMonoid B] [Module R B] : Module R (A →+ B)

Full source

instance instModule [Semiring R] [AddMonoid A] [AddCommMonoid B] [Module R B] : Module R (A →+ B) :=
  { add_smul := fun _ _ _=> ext fun _ => add_smul _ _ _
    zero_smul := fun _ => ext fun _ => zero_smul _ _ }

Module Structure on Additive Monoid Homomorphisms

Informal description

For any semiring $R$, additive monoid $A$, and additive commutative monoid $B$ equipped with a module structure over $R$, the space of additive monoid homomorphisms from $A$ to $B$ forms a module over $R$. The module structure is defined pointwise: for any $f, g \in (A \to+ B)$, $r \in R$, and $a \in A$, we have: 1. $(f + g)(a) = f(a) + g(a)$ (pointwise addition) 2. $(r \cdot f)(a) = r \cdot f(a)$ (pointwise scalar multiplication)

AddMonoidHom.instDomMulActModule instance

{S M M₂ : Type*} [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module S M] : Module Sᵈᵐᵃ (M →+ M₂)

Full source

instance instDomMulActModule
    {S M M₂ : Type*} [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module S M] :
    Module Sᵈᵐᵃ (M →+ M₂) where
  add_smul s s' f := AddMonoidHom.ext fun m ↦ by
    simp_rw [AddMonoidHom.add_apply, DomMulAct.smul_addMonoidHom_apply, ← map_add, ← add_smul]; rfl
  zero_smul _ := AddMonoidHom.ext fun _ ↦ by
    rw [DomMulAct.smul_addMonoidHom_apply]
    -- TODO there should be a simp lemma for `DomMulAct.mk.symm 0`
    simp [DomMulAct.mk, MulOpposite.opEquiv]

Module Structure on Additive Monoid Homomorphisms via Domain Multiplication Action

Informal description

For any semiring $S$ and additive commutative monoids $M$ and $M₂$ where $M$ is a module over $S$, the domain multiplication action type $S^\text{dma}$ has a module structure on the space of additive monoid homomorphisms $M \to M₂$. This module structure is defined by $(c \cdot f)(a) = f(c \cdot a)$ for $c \in S^\text{dma}$, $f \in M \to M₂$, and $a \in M$.

AddMonoid.End.instDistribSMul instance

[DistribSMul M A] : DistribSMul M (AddMonoid.End A)

Full source

instance instDistribSMul [DistribSMul M A] : DistribSMul M (AddMonoid.End A) :=
  AddMonoidHom.instDistribSMul

Distributive Scalar Multiplication on Endomorphisms

Informal description

For any additive monoid $A$ with a distributive scalar multiplication by $M$, the endomorphism monoid $\text{End}(A)$ inherits a distributive scalar multiplication structure from $M$.

AddMonoid.End.instDistribMulAction instance

: DistribMulAction R (AddMonoid.End A)

Full source

instance instDistribMulAction : DistribMulAction R (AddMonoid.End A) :=
  AddMonoidHom.instDistribMulAction

Distributive Multiplicative Action on Endomorphism Ring

Informal description

For any additive commutative monoid $A$ and any monoid $R$ with a distributive multiplicative action on $A$, the endomorphism ring $\text{End}(A)$ inherits a distributive multiplicative action structure from $R$.

AddMonoid.End.coe_smul theorem

(r : R) (f : AddMonoid.End A) : ⇑(r • f) = r • ⇑f

Full source

@[simp] theorem coe_smul (r : R) (f : AddMonoid.End A) : ⇑(r • f) = r • ⇑f := rfl

Scalar Multiplication of Endomorphisms is Pointwise

Informal description

For any scalar $r$ in $R$ and any endomorphism $f$ of an additive commutative monoid $A$, the underlying function of the scalar multiple $r \cdot f$ is equal to the pointwise scalar multiplication of $r$ with the underlying function of $f$, i.e., $(r \cdot f)(x) = r \cdot f(x)$ for all $x \in A$.

AddMonoid.End.smul_apply theorem

(r : R) (f : AddMonoid.End A) (x : A) : (r • f) x = r • f x

Full source

theorem smul_apply (r : R) (f : AddMonoid.End A) (x : A) : (r • f) x = r • f x :=
  rfl

Scalar Multiplication Action on Endomorphism: $(r \cdot f)(x) = r \cdot f(x)$

Informal description

For any scalar $r$ in $R$, any endomorphism $f$ of an additive monoid $A$, and any element $x$ in $A$, the action of the scalar multiple $r \cdot f$ on $x$ is equal to the scalar multiple $r$ acting on the result of $f$ applied to $x$, i.e., $(r \cdot f)(x) = r \cdot f(x)$.

AddMonoid.End.smulCommClass instance

[SMulCommClass R S A] : SMulCommClass R S (AddMonoid.End A)

Full source

instance smulCommClass [SMulCommClass R S A] : SMulCommClass R S (AddMonoid.End A) :=
  AddMonoidHom.smulCommClass

Commutativity of Scalar Actions on Endomorphisms

Informal description

For any additive monoid $A$ with commuting scalar actions of $R$ and $S$ on $A$, the scalar actions of $R$ and $S$ on the endomorphism monoid $\text{End}(A)$ also commute. That is, for any $r \in R$, $s \in S$, and $f \in \text{End}(A)$, we have $r \cdot (s \cdot f) = s \cdot (r \cdot f)$.

AddMonoid.End.isScalarTower instance

[SMul R S] [IsScalarTower R S A] : IsScalarTower R S (AddMonoid.End A)

Full source

instance isScalarTower [SMul R S] [IsScalarTower R S A] : IsScalarTower R S (AddMonoid.End A) :=
  AddMonoidHom.isScalarTower

Scalar Multiplication Tower Property for Endomorphisms

Informal description

For any additive monoid $A$ with a scalar multiplication tower structure involving scalars $R$ and $S$ (i.e., $R$ acts on $S$ and $S$ acts on $A$ in a compatible way), the endomorphism monoid $\text{End}(A)$ also forms a scalar multiplication tower with the same scalars $R$ and $S$. More precisely, for any $r \in R$, $s \in S$, and $f \in \text{End}(A)$, the scalar multiplications satisfy $(r \cdot s) \cdot f = r \cdot (s \cdot f)$.

AddMonoid.End.isCentralScalar instance

[DistribMulAction Rᵐᵒᵖ A] [IsCentralScalar R A] : IsCentralScalar R (AddMonoid.End A)

Full source

instance isCentralScalar [DistribMulAction Rᵐᵒᵖ A] [IsCentralScalar R A] :
    IsCentralScalar R (AddMonoid.End A) :=
  AddMonoidHom.isCentralScalar

Central Scalar Action on Endomorphisms of Additive Monoids

Informal description

For any additive monoid $A$ with a distributive multiplicative action by $R$ and its opposite $R^\text{op}$, if the actions of $R$ and $R^\text{op}$ on $A$ are central (i.e., they coincide), then the endomorphism monoid $\text{End}(A)$ also has a central scalar action by $R$.

AddMonoid.End.instModule instance

[Semiring R] [AddCommMonoid A] [Module R A] : Module R (AddMonoid.End A)

Full source

instance instModule [Semiring R] [AddCommMonoid A] [Module R A] : Module R (AddMonoid.End A) :=
  AddMonoidHom.instModule

Module Structure on Endomorphisms of a Module

Informal description

For any semiring $R$ and additive commutative monoid $A$ equipped with a module structure over $R$, the space of additive monoid endomorphisms $\text{End}(A)$ forms a module over $R$ with pointwise scalar multiplication.

AddMonoid.End.applyModule instance

[AddCommMonoid A] : Module (AddMonoid.End A) A

Full source

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

This generalizes `AddMonoid.End.applyDistribMulAction`. -/
instance applyModule [AddCommMonoid A] : Module (AddMonoid.End A) A where
  add_smul _ _ _ := rfl
  zero_smul _ := rfl

Module Structure on Additive Commutative Monoid via Endomorphism Action

Informal description

For any additive commutative monoid $A$, the tautological action of the endomorphism ring $\text{End}(A)$ on $A$ gives $A$ the structure of a module over $\text{End}(A)$. This action is defined by function application, where an endomorphism $f \in \text{End}(A)$ acts on an element $a \in A$ as $f(a)$.

AddMonoidHom.smulLeft definition

[Monoid M] [AddMonoid A] [DistribMulAction M A] (c : M) : A →+ A

Full source

/-- Scalar multiplication on the left as an additive monoid homomorphism. -/
@[simps! -fullyApplied]
protected def smulLeft [Monoid M] [AddMonoid A] [DistribMulAction M A] (c : M) : A →+ A :=
  DistribMulAction.toAddMonoidHom _ c

Left scalar multiplication as an additive monoid homomorphism

Informal description

Given a monoid $M$ acting distributively on an additive monoid $A$, the function $\text{smulLeft}(c) : A \to A$ defined by $a \mapsto c \cdot a$ is an additive monoid homomorphism for any fixed $c \in M$.

AddMonoidHom.smul definition

[Semiring R] [AddCommMonoid M] [Module R M] : R →+ M →+ M

Full source

/-- Scalar multiplication as a biadditive monoid homomorphism. We need `M` to be commutative
to have addition on `M →+ M`. -/
protected def smul [Semiring R] [AddCommMonoid M] [Module R M] : R →+ M →+ M :=
  (Module.toAddMonoidEnd R M).toAddMonoidHom

Scalar multiplication as an additive monoid homomorphism

Informal description

Given a semiring $R$ and an $R$-module $M$ (where $M$ is an additive commutative monoid), the scalar multiplication operation can be viewed as an additive monoid homomorphism from $R$ to the additive monoid of additive endomorphisms of $M$. More precisely, this is the additive monoid homomorphism version of the canonical map that sends each scalar $r \in R$ to the endomorphism $m \mapsto r \bullet m$ (where $\bullet$ denotes the module scalar multiplication).

AddMonoidHom.coe_smul' theorem

[Semiring R] [AddCommMonoid M] [Module R M] : ⇑(.smul : R →+ M →+ M) = AddMonoidHom.smulLeft

Full source

@[simp] theorem coe_smul' [Semiring R] [AddCommMonoid M] [Module R M] :
    ⇑(.smul : R →+ M →+ M) = AddMonoidHom.smulLeft := rfl

Coefficient Function of Scalar Multiplication Homomorphism Equals Left Scalar Multiplication

Informal description

For a semiring $R$ and an $R$-module $M$ (where $M$ is an additive commutative monoid), the underlying function of the additive monoid homomorphism $\text{smul} : R \to (M \to+ M)$ (which represents scalar multiplication) is equal to the function $\text{smulLeft}$ that maps each scalar $r \in R$ to the additive endomorphism $m \mapsto r \bullet m$.