Mathlib.Data.Finsupp.SMulWithZero

Module docstring

{"# Scalar multiplication on Finsupp

This file defines the pointwise scalar multiplication on Finsupp, assuming it preserves zero.

Main declarations

Finsupp.smulZeroClass: if the action of R on M preserves 0, then it acts on α →₀ M

Implementation notes

This file is intermediate between Finsupp.Defs and Finsupp.Module in that it covers scalar multiplication but does not rely on the definition of Module. Scalar multiplication is needed to supply the nsmul (and zsmul) fields of (semi)ring structures which are fundamental for e.g. Polynomial, so we want to keep the imports required for the Finsupp.smulZeroClass instance reasonably light.

This file is a noncomputable theory and uses classical logic throughout. ","Throughout this section, some Monoid and Semiring arguments are specified with {} instead of []. See note [implicit instance arguments]. "}

Finsupp.smulZeroClass instance

[Zero M] [SMulZeroClass R M] : SMulZeroClass R (α →₀ M)

Full source

instance smulZeroClass [Zero M] [SMulZeroClass R M] : SMulZeroClass R (α →₀ M) where
  smul a v := v.mapRange (a • ·) (smul_zero _)
  smul_zero a := by
    ext
    apply smul_zero

Pointwise Scalar Multiplication on Finitely Supported Functions Preserving Zero

Informal description

For any type $R$ with a scalar multiplication action on $M$ that preserves zero (i.e., $r \cdot 0 = 0$ for all $r \in R$), the type of finitely supported functions $\alpha \to₀ M$ inherits a scalar multiplication action from $R$ that also preserves zero. This action is defined pointwise: $(r \cdot f)(a) = r \cdot f(a)$ for any $f \in \alpha \to₀ M$ and $a \in \alpha$.

Finsupp.coe_smul theorem

[Zero M] [SMulZeroClass R M] (b : R) (v : α →₀ M) : ⇑(b • v) = b • ⇑v

Full source

@[simp, norm_cast]
theorem coe_smul [Zero M] [SMulZeroClass R M] (b : R) (v : α →₀ M) : ⇑(b • v) = b • ⇑v :=
  rfl

Pointwise Scalar Multiplication on Finitely Supported Functions

Informal description

For any type $R$ with a scalar multiplication action on $M$ that preserves zero, and for any finitely supported function $v : \alpha \to₀ M$, the underlying function of the scalar multiple $b \cdot v$ is equal to the pointwise scalar multiple of $b$ with the underlying function of $v$, i.e., $(b \cdot v)(a) = b \cdot v(a)$ for all $a \in \alpha$.

Finsupp.smul_apply theorem

[Zero M] [SMulZeroClass R M] (b : R) (v : α →₀ M) (a : α) : (b • v) a = b • v a

Full source

theorem smul_apply [Zero M] [SMulZeroClass R M] (b : R) (v : α →₀ M) (a : α) :
    (b • v) a = b • v a :=
  rfl

Pointwise Scalar Multiplication Formula for Finitely Supported Functions

Informal description

For a scalar multiplication action of $R$ on $M$ that preserves zero (i.e., $r \cdot 0 = 0$ for all $r \in R$), and for any finitely supported function $v \colon \alpha \to₀ M$, scalar $b \in R$, and element $a \in \alpha$, the evaluation of the scalar multiple $b \cdot v$ at $a$ equals the scalar multiple of the evaluation of $v$ at $a$, i.e., $(b \cdot v)(a) = b \cdot v(a)$.

Finsupp.instSMulWithZero instance

[Zero R] [Zero M] [SMulWithZero R M] : SMulWithZero R (α →₀ M)

Full source

instance instSMulWithZero [Zero R] [Zero M] [SMulWithZero R M] : SMulWithZero R (α →₀ M) where
  zero_smul f := by ext i; exact zero_smul _ _

Scalar Multiplication on Finitely Supported Functions Preserving Zero

Informal description

For any types $R$ and $M$ with zero elements, if $M$ has a scalar multiplication action by $R$ that preserves zero (i.e., $r \cdot 0_M = 0_M$ for all $r \in R$), then the type of finitely supported functions $\alpha \to₀ M$ inherits a scalar multiplication action by $R$ that also preserves zero. This action is defined pointwise: $(r \cdot f)(a) = r \cdot (f(a))$ for any $f \in \alpha \to₀ M$ and $a \in \alpha$.

Finsupp.distribSMul instance

[AddZeroClass M] [DistribSMul R M] : DistribSMul R (α →₀ M)

Full source

instance distribSMul [AddZeroClass M] [DistribSMul R M] : DistribSMul R (α →₀ M) where
  smul := (· • ·)
  smul_add _ _ _ := ext fun _ => smul_add _ _ _
  smul_zero _ := ext fun _ => smul_zero _

Distributive Scalar Multiplication on Finitely Supported Functions

Informal description

For any type $M$ with an additive zero class structure and a distributive scalar multiplication action by $R$ (i.e., $r \cdot (m_1 + m_2) = r \cdot m_1 + r \cdot m_2$ for all $r \in R$ and $m_1, m_2 \in M$), the type of finitely supported functions $\alpha \to_{\text{f}} M$ inherits a distributive scalar multiplication action from $R$. This action is defined pointwise: $(r \cdot f)(a) = r \cdot f(a)$ for any $f \in \alpha \to_{\text{f}} M$ and $a \in \alpha$.

Finsupp.isScalarTower instance

[Zero M] [SMulZeroClass R M] [SMulZeroClass S M] [SMul R S] [IsScalarTower R S M] : IsScalarTower R S (α →₀ M)

Full source

instance isScalarTower [Zero M] [SMulZeroClass R M] [SMulZeroClass S M] [SMul R S]
  [IsScalarTower R S M] : IsScalarTower R S (α →₀ M) where
  smul_assoc _ _ _ := ext fun _ => smul_assoc _ _ _

Scalar Tower Structure on Finitely Supported Functions

Informal description

For any type $M$ with a zero element and scalar multiplication actions from types $R$ and $S$ that preserve zero, if $R$ and $S$ form a scalar tower (i.e., $(r \cdot s) \cdot m = r \cdot (s \cdot m)$ for all $r \in R$, $s \in S$, $m \in M$), then the type of finitely supported functions $\alpha \to₀ M$ also forms a scalar tower with respect to the pointwise scalar multiplication.

Finsupp.smulCommClass instance

[Zero M] [SMulZeroClass R M] [SMulZeroClass S M] [SMulCommClass R S M] : SMulCommClass R S (α →₀ M)

Full source

instance smulCommClass [Zero M] [SMulZeroClass R M] [SMulZeroClass S M] [SMulCommClass R S M] :
  SMulCommClass R S (α →₀ M) where
  smul_comm _ _ _ := ext fun _ => smul_comm _ _ _

Commutativity of Scalar Multiplication on Finitely Supported Functions

Informal description

For any type $R$ and $S$ with scalar multiplication actions on $M$ that preserve zero (i.e., $r \cdot 0 = 0$ for all $r \in R$ and $s \cdot 0 = 0$ for all $s \in S$), if the actions of $R$ and $S$ on $M$ commute (i.e., $r \cdot (s \cdot m) = s \cdot (r \cdot m)$ for all $r \in R$, $s \in S$, and $m \in M$), then the pointwise scalar multiplication actions of $R$ and $S$ on the finitely supported functions $\alpha \to₀ M$ also commute.

Finsupp.isCentralScalar instance

[Zero M] [SMulZeroClass R M] [SMulZeroClass Rᵐᵒᵖ M] [IsCentralScalar R M] : IsCentralScalar R (α →₀ M)

Full source

instance isCentralScalar [Zero M] [SMulZeroClass R M] [SMulZeroClass Rᵐᵒᵖ M] [IsCentralScalar R M] :
  IsCentralScalar R (α →₀ M) where
  op_smul_eq_smul _ _ := ext fun _ => op_smul_eq_smul _ _

Pointwise Scalar Multiplication on Finitely Supported Functions Preserving Zero

Informal description

For any type $R$ with a scalar multiplication action on $M$ that preserves zero, and any type $\alpha$, the space of finitely supported functions $\alpha \to_{\text{f}} M$ (denoted $\alpha \to₀ M$) inherits a scalar multiplication action from $R$ that also preserves zero. This action is defined pointwise: $(r \cdot f)(a) = r \cdot f(a)$ for any $f \in \alpha \to₀ M$ and $a \in \alpha$.

Finsupp.support_smul theorem

[Zero M] [SMulZeroClass R M] {b : R} {g : α →₀ M} : (b • g).support ⊆ g.support

Full source

theorem support_smul [Zero M] [SMulZeroClass R M] {b : R} {g : α →₀ M} :
    (b • g).support ⊆ g.support := fun a => by
  simp only [smul_apply, mem_support_iff, Ne]
  exact mt fun h => h.symm ▸ smul_zero _

Support of Scalar Multiple is Subset of Original Support in Finitely Supported Functions

Informal description

Let $R$ be a type with a scalar multiplication action on $M$ that preserves zero (i.e., $r \cdot 0 = 0$ for all $r \in R$), and let $g : \alpha \to₀ M$ be a finitely supported function from $\alpha$ to $M$. For any $b \in R$, the support of the scalar multiple $b \cdot g$ is a subset of the support of $g$.

Finsupp.smul_single theorem

[Zero M] [SMulZeroClass R M] (c : R) (a : α) (b : M) : c • Finsupp.single a b = Finsupp.single a (c • b)

Full source

@[simp]
theorem smul_single [Zero M] [SMulZeroClass R M] (c : R) (a : α) (b : M) :
    c • Finsupp.single a b = Finsupp.single a (c • b) :=
  mapRange_single

Scalar Multiplication Commutes with Single-Point Function: $c \cdot (\text{single}\, a\, b) = \text{single}\, a\, (c \cdot b)$

Informal description

Let $R$ be a type with a scalar multiplication action on $M$ that preserves zero (i.e., $r \cdot 0 = 0$ for all $r \in R$). For any scalar $c \in R$, any element $a \in \alpha$, and any value $b \in M$, the scalar multiple $c \cdot (\text{single}\, a\, b)$ is equal to the single-point finitely supported function $\text{single}\, a\, (c \cdot b)$. In mathematical notation: $$c \cdot (\text{single}\, a\, b) = \text{single}\, a\, (c \cdot b).$$

Finsupp.mapRange_smul theorem

 [Zero M] [SMulZeroClass R M] [Zero N] [SMulZeroClass R N] {f : M → N} {hf : f 0 = 0} (c : R) (v : α →₀ M)
  (hsmul : ∀ x, f (c • x) = c • f x) : mapRange f hf (c • v) = c • mapRange f hf v

Full source

theorem mapRange_smul [Zero M] [SMulZeroClass R M] [Zero N]
    [SMulZeroClass R N] {f : M → N} {hf : f 0 = 0} (c : R) (v : α →₀ M)
    (hsmul : ∀ x, f (c • x) = c • f x) : mapRange f hf (c • v) = c • mapRange f hf v := by
  ext
  simp [hsmul]

Scalar Multiplication Commutes with Composition of Finitely Supported Functions

Informal description

Let $M$ and $N$ be types with zero elements, and let $R$ be a type with a scalar multiplication action on both $M$ and $N$ that preserves zero. Given a function $f \colon M \to N$ such that $f(0) = 0$, a scalar $c \in R$, and a finitely supported function $v \colon \alpha \to_{\text{f}} M$, if $f$ commutes with scalar multiplication (i.e., $f(c \cdot x) = c \cdot f(x)$ for all $x \in M$), then the composition of $f$ with the scalar multiple $c \cdot v$ equals the scalar multiple of the composition of $f$ with $v$. In other words, $f \circ (c \cdot v) = c \cdot (f \circ v)$ as finitely supported functions from $\alpha$ to $N$.