Mathlib.LinearAlgebra.Finsupp.LSum

Finsupp.smul_sum theorem

 [Zero β] [AddCommMonoid M] [DistribSMul R M] {v : α →₀ β} {c : R} {h : α → β → M} :
  c • v.sum h = v.sum fun a b => c • h a b

Full source

theorem smul_sum [Zero β] [AddCommMonoid M] [DistribSMul R M] {v : α →₀ β} {c : R} {h : α → β → M} :
    c • v.sum h = v.sum fun a b => c • h a b :=
  Finset.smul_sum

Scalar Multiplication Commutes with Summation of Finitely Supported Functions

Informal description

Let $R$ be a ring, $M$ be an additive commutative monoid with a distributive scalar multiplication by $R$, and $\beta$ be a type with a zero element. For any finitely supported function $v \colon \alpha \to \beta$, any scalar $c \in R$, and any function $h \colon \alpha \to \beta \to M$, we have the equality: \[ c \cdot \sum_{a \in \alpha} h(a, v(a)) = \sum_{a \in \alpha} c \cdot h(a, v(a)). \]

Finsupp.sum_smul_index_linearMap' theorem

 [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {v : α →₀ M} {c : R}
  {h : α → M →ₗ[R] M₂} : ((c • v).sum fun a => h a) = c • v.sum fun a => h a

Full source

@[simp]
theorem sum_smul_index_linearMap' [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂]
    [Module R M₂] {v : α →₀ M} {c : R} {h : α → M →ₗ[R] M₂} :
    ((c • v).sum fun a => h a) = c • v.sum fun a => h a := by
  rw [Finsupp.sum_smul_index', Finsupp.smul_sum]
  · simp only [map_smul]
  · intro i
    exact (h i).map_zero

Linearity of Summation under Scalar Multiplication for Finitely Supported Functions with Linear Maps

Informal description

Let $R$ be a semiring, $M$ and $M₂$ be additive commutative monoids equipped with $R$-module structures. For any finitely supported function $v \colon \alpha \to_{\text{f}} M$, any scalar $c \in R$, and any family of $R$-linear maps $h_a \colon M \to M₂$ indexed by $a \in \alpha$, we have: \[ \sum_{a \in \alpha} h_a((c \cdot v)(a)) = c \cdot \sum_{a \in \alpha} h_a(v(a)). \]

LinearMap.CompatibleSMul.finsupp_dom instance

[SMulZeroClass R M] [DistribSMul R N] [LinearMap.CompatibleSMul M N R S] : LinearMap.CompatibleSMul (ι →₀ M) N R S

Full source

instance _root_.LinearMap.CompatibleSMul.finsupp_dom [SMulZeroClass R M] [DistribSMul R N]
    [LinearMap.CompatibleSMul M N R S] : LinearMap.CompatibleSMul (ι →₀ M) N R S where
  map_smul f r m := by
    conv_rhs => rw [← sum_single m, map_finsuppSum, smul_sum]
    erw [← sum_single (r • m), sum_mapRange_index single_zero, map_finsuppSum]
    congr; ext i m; exact (f.comp <| lsingle i).map_smul_of_tower r m

Compatible Scalar Multiplication on Finitely Supported Functions with Domain

Informal description

For any type $\iota$ and any $R$-module $M$ with a scalar multiplication action that preserves zero, if $N$ is an $R$-module with a distributive scalar multiplication action and there is a compatible scalar multiplication between $M$ and $N$ over $R$ and $S$, then the space of finitely supported functions $\iota \to_{\text{f}} M$ also has a compatible scalar multiplication with $N$ over $R$ and $S$.

LinearMap.CompatibleSMul.finsupp_cod instance

[SMul R M] [SMulZeroClass R N] [LinearMap.CompatibleSMul M N R S] : LinearMap.CompatibleSMul M (ι →₀ N) R S

Full source

instance _root_.LinearMap.CompatibleSMul.finsupp_cod [SMul R M] [SMulZeroClass R N]
    [LinearMap.CompatibleSMul M N R S] : LinearMap.CompatibleSMul M (ι →₀ N) R S where
  map_smul f r m := by ext i; apply ((lapply i).comp f).map_smul_of_tower

Compatibility of Scalar Multiplication between Modules and Finitely Supported Functions

Informal description

For any type $R$ with a scalar multiplication action on $M$ and a zero-preserving scalar multiplication action on $N$, if the $R$-module structures on $M$ and $N$ are compatible with respect to $S$, then the compatibility also holds between $M$ and the space of finitely supported functions $\iota \to_{\text{f}} N$.

Finsupp.lsum definition

: (α → M →ₗ[R] N) ≃ₗ[S] (α →₀ M) →ₗ[R] N

Full source

/-- Lift a family of linear maps `M →ₗ[R] N` indexed by `x : α` to a linear map from `α →₀ M` to
`N` using `Finsupp.sum`. This is an upgraded version of `Finsupp.liftAddHom`.

See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
-/
def lsum : (α → M →ₗ[R] N) ≃ₗ[S] (α →₀ M) →ₗ[R] N where
  toFun F :=
    { toFun := fun d => d.sum fun i => F i
      map_add' := (liftAddHom (α := α) (M := M) (N := N) fun x => (F x).toAddMonoidHom).map_add
      map_smul' := fun c f => by simp [sum_smul_index', smul_sum] }
  invFun F x := F.comp (lsingle x)
  left_inv F := by
    ext x y
    simp
  right_inv F := by
    ext x y
    simp
  map_add' F G := by
    ext x y
    simp
  map_smul' F G := by
    ext x y
    simp

Linear sum of a family of linear maps

Informal description

Given a semiring $R$, an additive commutative monoid $M$ with a module structure over $R$, and another $R$-module $N$, the linear equivalence $\operatorname{lsum}$ maps a family of linear maps $(f_i \colon M \to N)_{i \in \alpha}$ to a linear map $\sum_{i \in \alpha} f_i \colon \alpha \to_{\text{f}} M \to N$, where $\alpha \to_{\text{f}} M$ denotes the space of finitely supported functions from $\alpha$ to $M$. The map $\sum_{i \in \alpha} f_i$ evaluates a finitely supported function $d \in \alpha \to_{\text{f}} M$ by summing the values $f_i(d(i))$ over the support of $d$.

Finsupp.coe_lsum theorem

(f : α → M →ₗ[R] N) : (lsum S f : (α →₀ M) → N) = fun d => d.sum fun i => f i

Full source

@[simp]
theorem coe_lsum (f : α → M →ₗ[R] N) : (lsum S f : (α →₀ M) → N) = fun d => d.sum fun i => f i :=
  rfl

Linear Sum as Pointwise Summation of Linear Maps

Informal description

For any family of linear maps $f_i \colon M \to N$ indexed by $\alpha$, the linear sum $\operatorname{lsum}_S f$ as a function from $\alpha \to_{\text{f}} M$ to $N$ is given by $\operatorname{lsum}_S f (d) = \sum_{i \in \alpha} f_i(d(i))$ for any finitely supported function $d \in \alpha \to_{\text{f}} M$.

Finsupp.lsum_apply theorem

(f : α → M →ₗ[R] N) (l : α →₀ M) : Finsupp.lsum S f l = l.sum fun b => f b

Full source

theorem lsum_apply (f : α → M →ₗ[R] N) (l : α →₀ M) : Finsupp.lsum S f l = l.sum fun b => f b :=
  rfl

Evaluation of Linear Sum on Finitely Supported Functions

Informal description

Given a semiring $R$, an additive commutative monoid $M$ with an $R$-module structure, and another $R$-module $N$, for any family of linear maps $(f_i \colon M \to N)_{i \in \alpha}$ and any finitely supported function $l \in \alpha \to_{\text{f}} M$, the linear sum $\operatorname{lsum}_S f$ evaluated at $l$ equals the sum $\sum_{b \in \alpha} f_b(l(b))$ over the support of $l$.

Finsupp.lsum_single theorem

(f : α → M →ₗ[R] N) (i : α) (m : M) : Finsupp.lsum S f (Finsupp.single i m) = f i m

Full source

theorem lsum_single (f : α → M →ₗ[R] N) (i : α) (m : M) :
    Finsupp.lsum S f (Finsupp.single i m) = f i m :=
  Finsupp.sum_single_index (f i).map_zero

Linear Sum Evaluated on Single Element: $\operatorname{lsum} f (\operatorname{single}_i m) = f_i(m)$

Informal description

For any family of linear maps $f_i \colon M \to N$ indexed by $\alpha$, any index $i \in \alpha$, and any element $m \in M$, the linear sum $\operatorname{lsum} f$ evaluated at the finitely supported function $\operatorname{single}_i m$ equals $f_i(m)$. In other words, $\operatorname{lsum} f (\operatorname{single}_i m) = f_i(m)$.

Finsupp.lsum_comp_lsingle theorem

(f : α → M →ₗ[R] N) (i : α) : Finsupp.lsum S f ∘ₗ lsingle i = f i

Full source

@[simp] theorem lsum_comp_lsingle (f : α → M →ₗ[R] N) (i : α) :
    Finsupp.lsumFinsupp.lsum S f ∘ₗ lsingle i = f i := by ext; simp

Composition of Linear Sum with Single-Point Embedding Equals Component Map

Informal description

Let $R$ be a semiring, $M$ and $N$ be $R$-modules, and $\alpha$ be a type. For any family of linear maps $f_i \colon M \to N$ indexed by $i \in \alpha$, the composition of the linear sum map $\operatorname{lsum}(f) \colon \alpha \to_{\text{f}} M \to N$ with the linear single-point embedding $\operatorname{lsingle}(i) \colon M \to \alpha \to_{\text{f}} M$ equals $f_i$. That is, $\operatorname{lsum}(f) \circ \operatorname{lsingle}(i) = f_i$.

Finsupp.lsum_symm_apply theorem

(f : (α →₀ M) →ₗ[R] N) (x : α) : (lsum S).symm f x = f.comp (lsingle x)

Full source

theorem lsum_symm_apply (f : (α →₀ M) →ₗ[R] N) (x : α) : (lsum S).symm f x = f.comp (lsingle x) :=
  rfl

Inverse of Linear Sum Map Evaluated at Component: $(\operatorname{lsum})^{-1}(f)(x) = f \circ \operatorname{lsingle}(x)$

Informal description

For any linear map $f \colon \alpha \to_{\text{f}} M \to N$ and any element $x \in \alpha$, the $x$-th component of the inverse of the linear sum map $\operatorname{lsum}$ evaluated at $f$ is equal to the composition of $f$ with the linear single-point embedding $\operatorname{lsingle}(x) \colon M \to \alpha \to_{\text{f}} M$. That is, $(\operatorname{lsum})^{-1}(f)(x) = f \circ \operatorname{lsingle}(x)$.

Finsupp.lift definition

: (X → M) ≃+ ((X →₀ R) →ₗ[R] M)

Full source

/-- A slight rearrangement from `lsum` gives us
the bijection underlying the free-forgetful adjunction for R-modules.
-/
noncomputable def lift : (X → M) ≃+ ((X →₀ R) →ₗ[R] M) :=
  (AddEquiv.arrowCongr (Equiv.refl X) (ringLmapEquivSelf R ℕ M).toAddEquiv.symm).trans
    (lsum _ : _ ≃ₗ[ℕ] _).toAddEquiv

Free-forgetful adjunction equivalence for $R$-modules

Informal description

The equivalence $\operatorname{lift} \colon (X \to M) \simeq^{+} ((X \to_{\text{f}} R) \to_{\text{lin}[R]} M)$ establishes a bijection between functions from $X$ to an $R$-module $M$ and linear maps from finitely supported functions $X \to_{\text{f}} R$ to $M$. This equivalence underlies the free-forgetful adjunction for $R$-modules, where $X \to_{\text{f}} R$ represents the free $R$-module on $X$. For a function $f \colon X \to M$, the corresponding linear map $\operatorname{lift}(f) \colon X \to_{\text{f}} R \to M$ evaluates a finitely supported function $g \in X \to_{\text{f}} R$ by summing the values $r \cdot f(x)$ for each pair $(x, r)$ in the support of $g$. Conversely, the inverse map sends a linear map $F \colon X \to_{\text{f}} R \to M$ to the function $x \mapsto F(\delta_x)$, where $\delta_x$ is the indicator function at $x$ (i.e., $\delta_x(x) = 1$ and $\delta_x(y) = 0$ for $y \neq x$).

Finsupp.lift_symm_apply theorem

(f) (x) : ((lift M R X).symm f) x = f (single x 1)

Full source

@[simp]
theorem lift_symm_apply (f) (x) : ((lift M R X).symm f) x = f (single x 1) :=
  rfl

Inverse Lift Map Evaluates as $f(\delta_x)$ at $x$

Informal description

For any linear map $f \colon (X \to_{\text{f}} R) \to M$ and any element $x \in X$, the inverse of the lift map evaluated at $f$ and $x$ satisfies $(\operatorname{lift}_{M,R,X}^{-1}(f))(x) = f(\delta_x)$, where $\delta_x$ is the finitely supported function that takes the value $1$ at $x$ and $0$ elsewhere.

Finsupp.lift_apply theorem

(f) (g) : ((lift M R X) f) g = g.sum fun x r => r • f x

Full source

@[simp]
theorem lift_apply (f) (g) : ((lift M R X) f) g = g.sum fun x r => r • f x :=
  rfl

Evaluation of Lift Map on Finitely Supported Functions

Informal description

For any function $f \colon X \to M$ and any finitely supported function $g \colon X \to_{\text{f}} R$, the linear map $\operatorname{lift}(f)$ evaluated at $g$ is equal to the sum $\sum_{x \in \text{supp}(g)} r \cdot f(x)$ for each pair $(x, r)$ in the support of $g$, where $\cdot$ denotes the scalar multiplication in $M$.

Finsupp.llift definition

: (X → M) ≃ₗ[S] (X →₀ R) →ₗ[R] M

Full source

/-- Given compatible `S` and `R`-module structures on `M` and a type `X`, the set of functions
`X → M` is `S`-linearly equivalent to the `R`-linear maps from the free `R`-module
on `X` to `M`. -/
noncomputable def llift : (X → M) ≃ₗ[S] (X →₀ R) →ₗ[R] M :=
  { lift M R X with
    map_smul' := by
      intros
      dsimp
      ext
      simp only [coe_comp, Function.comp_apply, lsingle_apply, lift_apply, Pi.smul_apply,
        sum_single_index, zero_smul, one_smul, LinearMap.smul_apply] }

Linear equivalence between functions and linear maps on free modules

Informal description

Given compatible $S$-module and $R$-module structures on $M$ and a type $X$, the set of functions $X \to M$ is $S$-linearly equivalent to the $R$-linear maps from the free $R$-module on $X$ (represented as finitely supported functions $X \to_{\text{f}} R$) to $M$. More precisely, the equivalence $\operatorname{llift} \colon (X \to M) \simeq_{\text{lin}[S]} ((X \to_{\text{f}} R) \to_{\text{lin}[R]} M)$ maps a function $f \colon X \to M$ to the linear map that evaluates a finitely supported function $g \in X \to_{\text{f}} R$ by summing the values $r \cdot f(x)$ for each pair $(x, r)$ in the support of $g$. The inverse map sends a linear map $F \colon X \to_{\text{f}} R \to M$ to the function $x \mapsto F(\delta_x)$, where $\delta_x$ is the indicator function at $x$.

Finsupp.llift_apply theorem

(f : X → M) (x : X →₀ R) : llift M R S X f x = lift M R X f x

Full source

@[simp]
theorem llift_apply (f : X → M) (x : X →₀ R) : llift M R S X f x = lift M R X f x :=
  rfl

Equality of Linear Lift and Additive Lift Evaluations

Informal description

For any function $f \colon X \to M$ and any finitely supported function $x \colon X \to_{\text{f}} R$, the linear map $\operatorname{llift}(f)$ evaluated at $x$ equals the evaluation of $\operatorname{lift}(f)$ at $x$, i.e., $\operatorname{llift}(f)(x) = \operatorname{lift}(f)(x)$.

Finsupp.llift_symm_apply theorem

(f : (X →₀ R) →ₗ[R] M) (x : X) : (llift M R S X).symm f x = f (single x 1)

Full source

@[simp]
theorem llift_symm_apply (f : (X →₀ R) →ₗ[R] M) (x : X) :
    (llift M R S X).symm f x = f (single x 1) :=
  rfl

Inverse of Linear Lift Evaluates at Indicator Function

Informal description

For any $R$-linear map $f \colon (X \to_{\text{f}} R) \to M$ and any element $x \in X$, the inverse of the linear equivalence $\operatorname{llift}$ evaluated at $f$ and $x$ satisfies $(\operatorname{llift}^{-1} f)(x) = f(\delta_x)$, where $\delta_x$ is the finitely supported function that takes the value $1$ at $x$ and $0$ elsewhere.

Finsupp.domLCongr definition

{α₁ α₂ : Type*} (e : α₁ ≃ α₂) : (α₁ →₀ M) ≃ₗ[R] α₂ →₀ M

Full source

/-- An equivalence of domains induces a linear equivalence of finitely supported functions.

This is `Finsupp.domCongr` as a `LinearEquiv`.
See also `LinearMap.funCongrLeft` for the case of arbitrary functions. -/
protected def domLCongr {α₁ α₂ : Type*} (e : α₁ ≃ α₂) : (α₁ →₀ M) ≃ₗ[R] α₂ →₀ M :=
  (Finsupp.domCongr e : (α₁ →₀ M) ≃+ (α₂ →₀ M)).toLinearEquiv <| by
    simpa only [equivMapDomain_eq_mapDomain, domCongr_apply] using (lmapDomain M R e).map_smul

Linear equivalence of finitely supported functions under domain equivalence

Informal description

Given a semiring $R$, an $R$-module $M$, and an equivalence $e : \alpha_1 \simeq \alpha_2$ between types $\alpha_1$ and $\alpha_2$, the function `Finsupp.domLCongr e` is a linear equivalence between the $R$-modules of finitely supported functions $\alpha_1 \to_0 M$ and $\alpha_2 \to_0 M$. It maps a finitely supported function $f : \alpha_1 \to_0 M$ to the function $\alpha_2 \to_0 M$ defined by $b \mapsto f(e^{-1}(b))$, and its inverse maps $g : \alpha_2 \to_0 M$ to $\alpha_1 \to_0 M$ defined by $a \mapsto g(e(a))$. This equivalence preserves both the additive and $R$-module structures.

Finsupp.domLCongr_apply theorem

 {α₁ : Type*} {α₂ : Type*} (e : α₁ ≃ α₂) (v : α₁ →₀ M) : (Finsupp.domLCongr e : _ ≃ₗ[R] _) v = Finsupp.domCongr e v

Full source

@[simp]
theorem domLCongr_apply {α₁ : Type*} {α₂ : Type*} (e : α₁ ≃ α₂) (v : α₁ →₀ M) :
    (Finsupp.domLCongr e : _ ≃ₗ[R] _) v = Finsupp.domCongr e v :=
  rfl

Action of Linear Equivalence on Finitely Supported Functions via Domain Equivalence

Informal description

Given a semiring $R$, an $R$-module $M$, and an equivalence $e : \alpha_1 \simeq \alpha_2$ between types $\alpha_1$ and $\alpha_2$, the linear equivalence $\text{Finsupp.domLCongr}\, e$ maps a finitely supported function $v : \alpha_1 \to_0 M$ to the finitely supported function $\alpha_2 \to_0 M$ defined by $b \mapsto v(e^{-1}(b))$. This is equal to the additive equivalence $\text{Finsupp.domCongr}\, e$ applied to $v$.

Finsupp.domLCongr_refl theorem

: Finsupp.domLCongr (Equiv.refl α) = LinearEquiv.refl R (α →₀ M)

Full source

@[simp]
theorem domLCongr_refl : Finsupp.domLCongr (Equiv.refl α) = LinearEquiv.refl R (α →₀ M) :=
  LinearEquiv.ext fun _ => equivMapDomain_refl _

Identity Equivalence Yields Identity Linear Equivalence for Finitely Supported Functions

Informal description

Given a semiring $R$ and an $R$-module $M$, the linear equivalence `Finsupp.domLCongr` applied to the identity equivalence $\text{Equiv.refl}(\alpha)$ is equal to the identity linear equivalence on the $R$-module of finitely supported functions $\alpha \to_{\text{f}} M$.

Finsupp.domLCongr_trans theorem

 {α₁ α₂ α₃ : Type*} (f : α₁ ≃ α₂) (f₂ : α₂ ≃ α₃) :
  (Finsupp.domLCongr f).trans (Finsupp.domLCongr f₂) = (Finsupp.domLCongr (f.trans f₂) : (_ →₀ M) ≃ₗ[R] _)

Full source

theorem domLCongr_trans {α₁ α₂ α₃ : Type*} (f : α₁ ≃ α₂) (f₂ : α₂ ≃ α₃) :
    (Finsupp.domLCongr f).trans (Finsupp.domLCongr f₂) =
      (Finsupp.domLCongr (f.trans f₂) : (_ →₀ M) ≃ₗ[R] _) :=
  LinearEquiv.ext fun _ => (equivMapDomain_trans _ _ _).symm

Composition of Linear Equivalences for Finitely Supported Functions under Domain Equivalences

Informal description

Given a semiring $R$, an $R$-module $M$, and equivalences $f \colon \alpha_1 \simeq \alpha_2$ and $f_2 \colon \alpha_2 \simeq \alpha_3$, the composition of the linear equivalences $\text{Finsupp.domLCongr}\,f$ and $\text{Finsupp.domLCongr}\,f_2$ is equal to the linear equivalence $\text{Finsupp.domLCongr}\,(f \circ f_2)$ between the $R$-modules of finitely supported functions $\alpha_1 \to_{\text{f}} M$ and $\alpha_3 \to_{\text{f}} M$.

Finsupp.domLCongr_symm theorem

 {α₁ α₂ : Type*} (f : α₁ ≃ α₂) : ((Finsupp.domLCongr f).symm : (_ →₀ M) ≃ₗ[R] _) = Finsupp.domLCongr f.symm

Full source

@[simp]
theorem domLCongr_symm {α₁ α₂ : Type*} (f : α₁ ≃ α₂) :
    ((Finsupp.domLCongr f).symm : (_ →₀ M) ≃ₗ[R] _) = Finsupp.domLCongr f.symm :=
  LinearEquiv.ext fun _ => rfl

Inverse of Linear Equivalence on Finitely Supported Functions Induced by Domain Equivalence

Informal description

Given a semiring $R$, an $R$-module $M$, and an equivalence $f : \alpha_1 \simeq \alpha_2$ between types $\alpha_1$ and $\alpha_2$, the inverse of the linear equivalence `Finsupp.domLCongr f` is equal to the linear equivalence `Finsupp.domLCongr f.symm`. That is, the inverse of the linear equivalence induced by $f$ on the spaces of finitely supported functions is the linear equivalence induced by the inverse of $f$.

Finsupp.domLCongr_single theorem

 {α₁ : Type*} {α₂ : Type*} (e : α₁ ≃ α₂) (i : α₁) (m : M) :
  (Finsupp.domLCongr e : _ ≃ₗ[R] _) (Finsupp.single i m) = Finsupp.single (e i) m

Full source

theorem domLCongr_single {α₁ : Type*} {α₂ : Type*} (e : α₁ ≃ α₂) (i : α₁) (m : M) :
    (Finsupp.domLCongr e : _ ≃ₗ[R] _) (Finsupp.single i m) = Finsupp.single (e i) m := by
  simp

Linear Equivalence Preserves Single Functions: $(\text{domLCongr } e)(\text{single } i \, m) = \text{single } (e(i)) \, m$

Informal description

Given a semiring $R$, an $R$-module $M$, and an equivalence $e \colon \alpha_1 \simeq \alpha_2$ between types $\alpha_1$ and $\alpha_2$, the linear equivalence $\text{domLCongr } e$ maps the finitely supported function $\text{single } i \, m$ (which is the function that takes value $m$ at $i$ and zero elsewhere) to the finitely supported function $\text{single } (e(i)) \, m$ (which takes value $m$ at $e(i)$ and zero elsewhere). In other words, $(\text{domLCongr } e)(\text{single } i \, m) = \text{single } (e(i)) \, m$.

Finsupp.lcongr definition

{ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) : (ι →₀ M) ≃ₗ[R] κ →₀ N

Full source

/-- An equivalence of domain and a linear equivalence of codomain induce a linear equivalence of the
corresponding finitely supported functions. -/
def lcongr {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) : (ι →₀ M) ≃ₗ[R] κ →₀ N :=
  (Finsupp.domLCongr e₁).trans (mapRange.linearEquiv e₂)

Linear equivalence of finitely supported functions under domain and codomain equivalences

Informal description

Given a semiring $R$, $R$-modules $M$ and $N$, an equivalence $e_1 : \iota \simeq \kappa$ between index types, and a linear equivalence $e_2 : M \simeq_{\text{lin}[R]} N$, the linear equivalence $\text{Finsupp.lcongr } e_1 e_2$ maps a finitely supported function $f : \iota \to_{\text{f}} M$ to the finitely supported function $\kappa \to_{\text{f}} N$ defined by $k \mapsto e_2(f(e_1^{-1}(k)))$. This is constructed by first applying the domain equivalence $e_1$ (via $\text{domLCongr}$) and then the codomain linear equivalence $e_2$ (via $\text{mapRange.linearEquiv}$).

Finsupp.lcongr_single theorem

 {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (i : ι) (m : M) :
  lcongr e₁ e₂ (Finsupp.single i m) = Finsupp.single (e₁ i) (e₂ m)

Full source

@[simp]
theorem lcongr_single {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (i : ι) (m : M) :
    lcongr e₁ e₂ (Finsupp.single i m) = Finsupp.single (e₁ i) (e₂ m) := by simp [lcongr]

Linear Equivalence Preserves Single Functions: $\text{lcongr}\, e_1\, e_2\, (\text{single}\, i\, m) = \text{single}\, (e_1(i))\, (e_2(m))$

Informal description

Given a semiring $R$, $R$-modules $M$ and $N$, an equivalence $e_1 \colon \iota \simeq \kappa$ between index types, and a linear equivalence $e_2 \colon M \simeq_{\text{lin}[R]} N$, the linear equivalence $\text{lcongr}\, e_1\, e_2$ maps the finitely supported function $\text{single}\, i\, m$ (which takes value $m$ at $i$ and zero elsewhere) to the finitely supported function $\text{single}\, (e_1(i))\, (e_2(m))$ (which takes value $e_2(m)$ at $e_1(i)$ and zero elsewhere). In other words: $$\text{lcongr}\, e_1\, e_2\, (\text{single}\, i\, m) = \text{single}\, (e_1(i))\, (e_2(m)).$$

Finsupp.lcongr_apply_apply theorem

 {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (f : ι →₀ M) (k : κ) : lcongr e₁ e₂ f k = e₂ (f (e₁.symm k))

Full source

@[simp]
theorem lcongr_apply_apply {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (f : ι →₀ M) (k : κ) :
    lcongr e₁ e₂ f k = e₂ (f (e₁.symm k)) :=
  rfl

Evaluation of Linear Equivalence on Finitely Supported Functions

Informal description

Given a semiring $R$, $R$-modules $M$ and $N$, an equivalence $e_1 : \iota \simeq \kappa$ between index types, and a linear equivalence $e_2 : M \simeq_{\text{lin}[R]} N$, the evaluation of the linear equivalence $\text{Finsupp.lcongr } e_1 e_2$ at a finitely supported function $f : \iota \to_{\text{f}} M$ and a point $k \in \kappa$ is given by $(e_1 e_2 f)(k) = e_2(f(e_1^{-1}(k)))$.

Finsupp.lcongr_symm_single theorem

 {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) :
  (lcongr e₁ e₂).symm (Finsupp.single k n) = Finsupp.single (e₁.symm k) (e₂.symm n)

Full source

theorem lcongr_symm_single {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) :
    (lcongr e₁ e₂).symm (Finsupp.single k n) = Finsupp.single (e₁.symm k) (e₂.symm n) := by
  apply_fun (lcongr e₁ e₂ : (ι →₀ M) → (κ →₀ N)) using (lcongr e₁ e₂).injective
  simp

Inverse Linear Equivalence Preserves Single Functions: $(\text{lcongr}\, e_1\, e_2)^{-1} (\text{single}\, k\, n) = \text{single}\, (e_1^{-1}(k))\, (e_2^{-1}(n))$

Informal description

Given a semiring $R$, $R$-modules $M$ and $N$, an equivalence $e_1 \colon \iota \simeq \kappa$ between index types, and a linear equivalence $e_2 \colon M \simeq_{\text{lin}[R]} N$, the inverse of the linear equivalence $\text{lcongr}\, e_1\, e_2$ maps the finitely supported function $\text{single}\, k\, n$ (which takes value $n$ at $k$ and zero elsewhere) to the finitely supported function $\text{single}\, (e_1^{-1}(k))\, (e_2^{-1}(n))$ (which takes value $e_2^{-1}(n)$ at $e_1^{-1}(k)$ and zero elsewhere). In other words: $$(\text{lcongr}\, e_1\, e_2)^{-1} (\text{single}\, k\, n) = \text{single}\, (e_1^{-1}(k))\, (e_2^{-1}(n)).$$

Finsupp.lcongr_symm theorem

{ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) : (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm

Full source

@[simp]
theorem lcongr_symm {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) :
    (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm := by
  ext
  rfl

Inverse of Linear Equivalence of Finitely Supported Functions

Informal description

Given a semiring $R$, $R$-modules $M$ and $N$, an equivalence $e_1 : \iota \simeq \kappa$ between index types, and a linear equivalence $e_2 : M \simeq_{\text{lin}[R]} N$, the inverse of the linear equivalence $\text{Finsupp.lcongr } e_1 e_2$ is equal to the linear equivalence $\text{Finsupp.lcongr } e_1^{-1} e_2^{-1}$.

Submodule.finsuppSum_mem theorem

 {ι β : Type*} [Zero β] (S : Submodule R M) (f : ι →₀ β) (g : ι → β → M) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) :
  f.sum g ∈ S

Full source

protected theorem Submodule.finsuppSum_mem {ι β : Type*} [Zero β] (S : Submodule R M) (f : ι →₀ β)
    (g : ι → β → M) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S :=
  AddSubmonoidClass.finsuppSum_mem S f g h

Submodule Membership of Finsupp Sum

Informal description

Let $R$ be a ring and $M$ an $R$-module. For any submodule $S$ of $M$, any finitely supported function $f : \iota \to \beta$ (where $\beta$ has a zero element), and any function $g : \iota \to \beta \to M$, if for every $c \in \iota$ with $f(c) \neq 0$ we have $g(c)(f(c)) \in S$, then the sum $\sum_{c \in \iota} g(c)(f(c))$ belongs to $S$.

LinearMap.splittingOfFinsuppSurjective definition

(f : M →ₗ[R] α →₀ R) (s : Surjective f) : (α →₀ R) →ₗ[R] M

Full source

/-- A surjective linear map to finitely supported functions has a splitting. -/
def splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f) : (α →₀ R) →ₗ[R] M :=
  Finsupp.lift _ _ _ fun x : α => (s (Finsupp.single x 1)).choose

Splitting of a surjective linear map to finitely supported functions

Informal description

Given a surjective linear map $ f : M \to_{\text{lin}[R]} (\alpha \to_{\text{f}} R) $ from an $ R $-module $ M $ to the space of finitely supported functions $ \alpha \to_{\text{f}} R $, there exists a linear map $ g : (\alpha \to_{\text{f}} R) \to_{\text{lin}[R]} M $ such that $ f \circ g $ is the identity map on $ \alpha \to_{\text{f}} R $. The map $ g $ is constructed by lifting the function that assigns to each $ x \in \alpha $ an arbitrary preimage of the indicator function $ \text{single } x \text{ } 1 $ under $ f $.

LinearMap.splittingOfFinsuppSurjective_splits theorem

(f : M →ₗ[R] α →₀ R) (s : Surjective f) : f.comp (splittingOfFinsuppSurjective f s) = LinearMap.id

Full source

theorem splittingOfFinsuppSurjective_splits (f : M →ₗ[R] α →₀ R) (s : Surjective f) :
    f.comp (splittingOfFinsuppSurjective f s) = LinearMap.id := by
  ext x
  dsimp [splittingOfFinsuppSurjective]
  congr
  rw [sum_single_index, one_smul]
  · exact (s (Finsupp.single x 1)).choose_spec
  · rw [zero_smul]

Splitting of Surjective Linear Map to Finitely Supported Functions is a Right Inverse

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\alpha$ a type. Given a surjective $R$-linear map $f \colon M \to \alpha \to_{\text{f}} R$ (where $\alpha \to_{\text{f}} R$ denotes the space of finitely supported functions from $\alpha$ to $R$), the composition of $f$ with its splitting map $\text{splittingOfFinsuppSurjective}\, f\, s$ equals the identity map on $\alpha \to_{\text{f}} R$. In other words, $f \circ g = \text{id}$, where $g = \text{splittingOfFinsuppSurjective}\, f\, s$.

LinearMap.leftInverse_splittingOfFinsuppSurjective theorem

(f : M →ₗ[R] α →₀ R) (s : Surjective f) : LeftInverse f (splittingOfFinsuppSurjective f s)

Full source

theorem leftInverse_splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f) :
    LeftInverse f (splittingOfFinsuppSurjective f s) := fun g =>
  LinearMap.congr_fun (splittingOfFinsuppSurjective_splits f s) g

Splitting Map is a Right Inverse of Surjective Linear Map to Finitely Supported Functions

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\alpha$ a type. Given a surjective $R$-linear map $f \colon M \to \alpha \to_{\text{f}} R$ (where $\alpha \to_{\text{f}} R$ denotes the space of finitely supported functions from $\alpha$ to $R$), the splitting map $g = \text{splittingOfFinsuppSurjective}\, f\, s$ satisfies $f \circ g = \text{id}$. That is, $f$ is a left inverse of $g$.

LinearMap.splittingOfFinsuppSurjective_injective theorem

(f : M →ₗ[R] α →₀ R) (s : Surjective f) : Injective (splittingOfFinsuppSurjective f s)

Full source

theorem splittingOfFinsuppSurjective_injective (f : M →ₗ[R] α →₀ R) (s : Surjective f) :
    Injective (splittingOfFinsuppSurjective f s) :=
  (leftInverse_splittingOfFinsuppSurjective f s).injective

Injectivity of the Splitting Map for Surjective Linear Maps to Finitely Supported Functions

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\alpha$ a type. Given a surjective $R$-linear map $f \colon M \to \alpha \to_{\text{f}} R$ (where $\alpha \to_{\text{f}} R$ denotes the space of finitely supported functions from $\alpha$ to $R$), the splitting map $g = \text{splittingOfFinsuppSurjective}\, f\, s$ is injective.

LinearMap.coe_finsupp_sum theorem

(t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) : ⇑(t.sum g) = t.sum fun i d => g i d

Full source

theorem coe_finsupp_sum (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) :
    ⇑(t.sum g) = t.sum fun i d => g i d := rfl

Coefficient-wise Sum of Linear Maps Equals Pointwise Sum

Informal description

For a finitely supported function $t : \iota \to \gamma$ and a family of linear maps $g_i : \gamma \to (M \to_{σ₁₂} M₂)$ indexed by $\iota$, the underlying function of the sum $\sum_{i \in \iota} g_i(t(i))$ is equal to the pointwise sum $\sum_{i \in \iota} (g_i(t(i)))$.

LinearMap.finsupp_sum_apply theorem

(t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) (b : M) : (t.sum g) b = t.sum fun i d => g i d b

Full source

@[simp]
theorem finsupp_sum_apply (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) (b : M) :
    (t.sum g) b = t.sum fun i d => g i d b :=
  sum_apply _ _ _

Evaluation of Sum of Linear Maps Equals Sum of Evaluations

Informal description

For any finitely supported function $t \colon \iota \to \gamma$, any family of linear maps $g_i \colon \gamma \to (M \to_{σ₁₂} M₂)$ indexed by $\iota$, and any element $b \in M$, the evaluation of the sum $\sum_{i \in \iota} g_i(t(i))$ at $b$ is equal to the sum $\sum_{i \in \iota} (g_i(t(i)))(b)$.

Submodule.mulLeftMap definition

{M : Submodule R S} (N : Submodule R S) {ι : Type*} (m : ι → M) : (ι →₀ N) →ₗ[R] S

Full source

/-- If `M` and `N` are submodules of an `R`-algebra `S`, `m : ι → M` is a family of elements, then
there is an `R`-linear map from `ι →₀ N` to `S` which maps `{ n_i }` to the sum of `m_i * n_i`.
This is used in the definition of linearly disjointness. -/
def mulLeftMap {M : Submodule R S} (N : Submodule R S) {ι : Type*} (m : ι → M) :
    (ι →₀ N) →ₗ[R] S := Finsupp.lsum R fun i ↦ (m i).1 • N.subtype

Linear map induced by left multiplication in submodules

Informal description

Given a commutative ring $R$, an $R$-algebra $S$, and two submodules $M$ and $N$ of $S$, for any family of elements $m_i \in M$ indexed by $\iota$, there exists an $R$-linear map from the space of finitely supported functions $\iota \to_{\text{f}} N$ to $S$. This map sends a finitely supported function $n \colon \iota \to N$ to the sum $\sum_{i \in \iota} m_i \cdot n_i$, where $n_i$ is the value of $n$ at $i$ (considered as an element of $S$ via the submodule inclusion).

Submodule.mulLeftMap_apply theorem

 {M N : Submodule R S} {ι : Type*} (m : ι → M) (n : ι →₀ N) :
  mulLeftMap N m n = Finsupp.sum n fun (i : ι) (n : N) ↦ (m i).1 * n.1

Full source

theorem mulLeftMap_apply {M N : Submodule R S} {ι : Type*} (m : ι → M) (n : ι →₀ N) :
    mulLeftMap N m n = Finsupp.sum n fun (i : ι) (n : N) ↦ (m i).1 * n.1 := rfl

Evaluation of Left Multiplication Map on Finitely Supported Functions

Informal description

Let $R$ be a commutative ring and $S$ an $R$-algebra. Given submodules $M, N \subseteq S$ and a family of elements $m_i \in M$ indexed by $i \in \iota$, the linear map $\text{mulLeftMap}_N m$ evaluated at a finitely supported function $n \colon \iota \to_{\text{f}} N$ is equal to the sum $\sum_{i \in \iota} m_i \cdot n_i$, where $n_i$ is the value of $n$ at $i$ (considered as an element of $S$ via the submodule inclusion).

Submodule.mulLeftMap_apply_single theorem

 {M N : Submodule R S} {ι : Type*} (m : ι → M) (i : ι) (n : N) : mulLeftMap N m (Finsupp.single i n) = (m i).1 * n.1

Full source

@[simp]
theorem mulLeftMap_apply_single {M N : Submodule R S} {ι : Type*} (m : ι → M) (i : ι) (n : N) :
    mulLeftMap N m (Finsupp.single i n) = (m i).1 * n.1 := by
  simp [mulLeftMap]

Evaluation of Left Multiplication Map on Single Element

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra, and $M, N$ submodules of $S$. For any family of elements $(m_i)_{i \in \iota}$ in $M$ and any element $n \in N$, the linear map $\text{mulLeftMap}_N (m_i)_{i \in \iota}$ applied to the finitely supported function $\text{single}_i n$ (which is $n$ at index $i$ and zero elsewhere) equals the product $m_i \cdot n$ in $S$.

Submodule.mulRightMap definition

(M : Submodule R S) {N : Submodule R S} {ι : Type*} (n : ι → N) : (ι →₀ M) →ₗ[R] S

Full source

/-- If `M` and `N` are submodules of an `R`-algebra `S`, `n : ι → N` is a family of elements, then
there is an `R`-linear map from `ι →₀ M` to `S` which maps `{ m_i }` to the sum of `m_i * n_i`.
This is used in the definition of linearly disjointness. -/
def mulRightMap (M : Submodule R S) {N : Submodule R S} {ι : Type*} (n : ι → N) :
    (ι →₀ M) →ₗ[R] S := Finsupp.lsum R fun i ↦ MulOpposite.op (n i).1 • M.subtype

Right multiplication map for submodules

Informal description

Given an $R$-algebra $S$ and submodules $M, N \subseteq S$, for any family of elements $n_i \in N$ indexed by $i \in \iota$, there is an $R$-linear map from the space of finitely supported functions $\iota \to_{\text{f}} M$ to $S$ that sends a function $m \colon \iota \to_{\text{f}} M$ to the sum $\sum_{i \in \iota} m_i \cdot n_i$. This map is constructed using the linear sum operation on the family of scalar multiplications by the elements $n_i$.

Submodule.mulRightMap_apply theorem

 {M N : Submodule R S} {ι : Type*} (n : ι → N) (m : ι →₀ M) :
  mulRightMap M n m = Finsupp.sum m fun (i : ι) (m : M) ↦ m.1 * (n i).1

Full source

theorem mulRightMap_apply {M N : Submodule R S} {ι : Type*} (n : ι → N) (m : ι →₀ M) :
    mulRightMap M n m = Finsupp.sum m fun (i : ι) (m : M) ↦ m.1 * (n i).1 := rfl

Evaluation of Right Multiplication Map on Finitely Supported Functions

Informal description

Let $R$ be a semiring and $S$ an $R$-algebra with submodules $M, N \subseteq S$. For any family of elements $(n_i)_{i \in \iota}$ in $N$ and any finitely supported function $m \colon \iota \to_{\text{f}} M$, the right multiplication map satisfies: \[ \text{mulRightMap}_M\, n\, m = \sum_{i \in \iota} m_i \cdot n_i \] where $m_i$ denotes the value of $m$ at $i$ and the sum is taken over the finite support of $m$.

Submodule.mulRightMap_apply_single theorem

 {M N : Submodule R S} {ι : Type*} (n : ι → N) (i : ι) (m : M) : mulRightMap M n (Finsupp.single i m) = m.1 * (n i).1

Full source

@[simp]
theorem mulRightMap_apply_single {M N : Submodule R S} {ι : Type*} (n : ι → N) (i : ι) (m : M) :
    mulRightMap M n (Finsupp.single i m) = m.1 * (n i).1 := by
  simp [mulRightMap]

Evaluation of Right Multiplication Map on Single Element

Informal description

Let $R$ be a semiring, $S$ an $R$-algebra, and $M, N$ submodules of $S$. For any family of elements $(n_i)_{i \in \iota}$ in $N$ and any element $m \in M$, the right multiplication map evaluated at the finitely supported function $\text{single}_i(m)$ (which is $m$ at index $i$ and zero elsewhere) equals $m \cdot n_i$.

Submodule.mulLeftMap_eq_mulRightMap_of_commute theorem

 [SMulCommClass R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type*} (m : ι → M)
  (hc : ∀ (i : ι) (n : N), Commute (m i).1 n.1) : mulLeftMap N m = mulRightMap N m

Full source

theorem mulLeftMap_eq_mulRightMap_of_commute [SMulCommClass R S S]
    {M : Submodule R S} (N : Submodule R S) {ι : Type*} (m : ι → M)
    (hc : ∀ (i : ι) (n : N), Commute (m i).1 n.1) : mulLeftMap N m = mulRightMap N m := by
  ext i n; simp [(hc i n).eq]

Equality of Left and Right Multiplication Maps under Commutativity Condition

Informal description

Let $R$ be a semiring and $S$ an $R$-algebra. Given submodules $M, N \subseteq S$ and a family of elements $(m_i)_{i \in \iota}$ in $M$, suppose that for every $i \in \iota$ and every $n \in N$, the elements $m_i$ and $n$ commute in $S$ (i.e., $m_i \cdot n = n \cdot m_i$). Then the left multiplication map $\text{mulLeftMap}_N (m_i)_{i \in \iota}$ equals the right multiplication map $\text{mulRightMap}_N (m_i)_{i \in \iota}$ as linear maps from $\iota \to_{\text{f}} N$ to $S$.

Submodule.mulLeftMap_eq_mulRightMap theorem

 {S : Type*} [CommSemiring S] [Module R S] [SMulCommClass R R S] [SMulCommClass R S S] [IsScalarTower R S S]
  {M : Submodule R S} (N : Submodule R S) {ι : Type*} (m : ι → M) : mulLeftMap N m = mulRightMap N m

Full source

theorem mulLeftMap_eq_mulRightMap {S : Type*} [CommSemiring S] [Module R S] [SMulCommClass R R S]
    [SMulCommClass R S S] [IsScalarTower R S S] {M : Submodule R S} (N : Submodule R S)
    {ι : Type*} (m : ι → M) : mulLeftMap N m = mulRightMap N m :=
  mulLeftMap_eq_mulRightMap_of_commute N m fun _ _ ↦ mul_comm _ _

Equality of Left and Right Multiplication Maps in Commutative Semiring Modules

Informal description

Let $R$ be a semiring and $S$ a commutative semiring equipped with an $R$-module structure. Suppose that: 1. The actions of $R$ on $S$ and of $S$ on itself commute (i.e., $[R, S] = 0$ and $[S, S] = 0$), and 2. $S$ is a scalar tower over $R$. Then for any submodules $M, N \subseteq S$ and any family of elements $(m_i)_{i \in \iota}$ in $M$, the left multiplication map $\text{mulLeftMap}_N (m_i)_{i \in \iota}$ equals the right multiplication map $\text{mulRightMap}_N (m_i)_{i \in \iota}$ as $R$-linear maps from $\iota \to_{\text{f}} N$ to $S$.

Mathlib.LinearAlgebra.Finsupp.LSum

Main definitions

Tags