doc-next-gen

Mathlib.LinearAlgebra.Finsupp.Defs

Module docstring

{"# Properties of the module α →₀ M

Given an R-module M, the R-module structure on α →₀ M is defined in Data.Finsupp.Basic.

In this file we define LinearMap versions of various maps:

  • Finsupp.lsingle a : M →ₗ[R] ι →₀ M: Finsupp.single a as a linear map;
  • Finsupp.lapply a : (ι →₀ M) →ₗ[R] M: the map fun f ↦ f a as a linear map;
  • Finsupp.lsubtypeDomain (s : Set α) : (α →₀ M) →ₗ[R] (s →₀ M): restriction to a subtype as a linear map;
  • Finsupp.restrictDom: Finsupp.filter as a linear map to Finsupp.supported s;
  • Finsupp.lmapDomain: a linear map version of Finsupp.mapDomain;

Tags

function with finite support, module, linear algebra "}

Finsupp.linearEquivFunOnFinite definition
: (α →₀ M) ≃ₗ[R] α → M
Full source 
/-- Given `Finite α`, `linearEquivFunOnFinite R` is the natural `R`-linear equivalence between
`α →₀ β` and `α → β`. -/
@[simps apply]
noncomputable def linearEquivFunOnFinite : (α →₀ M) ≃ₗ[R] α → M :=
  { equivFunOnFinite with
    toFun := (⇑)
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }
Linear equivalence between finitely supported functions and all functions on a finite type
Informal description
Given a finite type $\alpha$, a semiring $R$, and an $R$-module $M$, the natural $R$-linear equivalence between the space of finitely supported functions $\alpha \to_{\text{f}} M$ and the space of all functions $\alpha \to M$. This equivalence maps a finitely supported function to its underlying function, and its inverse constructs a finitely supported function from any function (which is automatically finitely supported when $\alpha$ is finite). The equivalence preserves addition and scalar multiplication.
Finsupp.linearEquivFunOnFinite_single theorem
[DecidableEq α] (x : α) (m : M) : (linearEquivFunOnFinite R M α) (single x m) = Pi.single x m
Full source 
@[simp]
theorem linearEquivFunOnFinite_single [DecidableEq α] (x : α) (m : M) :
    (linearEquivFunOnFinite R M α) (single x m) = Pi.single x m :=
  equivFunOnFinite_single x m
Linear equivalence maps single finitely supported function to pointwise single function
Informal description
Let $\alpha$ be a finite type with decidable equality, $R$ a semiring, and $M$ an $R$-module. For any $x \in \alpha$ and $m \in M$, the linear equivalence $\text{linearEquivFunOnFinite}$ maps the finitely supported function $\text{single}\ x\ m$ to the pointwise function $\text{Pi.single}\ x\ m$.
Finsupp.linearEquivFunOnFinite_symm_single theorem
[DecidableEq α] (x : α) (m : M) : (linearEquivFunOnFinite R M α).symm (Pi.single x m) = single x m
Full source 
@[simp]
theorem linearEquivFunOnFinite_symm_single [DecidableEq α] (x : α) (m : M) :
    (linearEquivFunOnFinite R M α).symm (Pi.single x m) = single x m :=
  equivFunOnFinite_symm_single x m
Inverse Linear Equivalence Maps Pointwise Single to Finsupp Single
Informal description
Let $\alpha$ be a finite type with decidable equality, $R$ a semiring, and $M$ an $R$-module. For any $x \in \alpha$ and $m \in M$, the inverse of the linear equivalence $\text{linearEquivFunOnFinite}$ maps the pointwise single function $\text{Pi.single}\,x\,m$ to the finitely supported function $\text{single}\,x\,m$.
Finsupp.linearEquivFunOnFinite_symm_coe theorem
(f : α →₀ M) : (linearEquivFunOnFinite R M α).symm f = f
Full source 
@[simp]
theorem linearEquivFunOnFinite_symm_coe (f : α →₀ M) : (linearEquivFunOnFinite R M α).symm f = f :=
  (linearEquivFunOnFinite R M α).symm_apply_apply f
Inverse of Linear Equivalence Preserves Finitely Supported Functions
Informal description
For any finitely supported function $f \colon \alpha \to_{\text{f}} M$, the inverse of the linear equivalence `linearEquivFunOnFinite` evaluated at $f$ is equal to $f$ itself. That is, $(\text{linearEquivFunOnFinite}\, R\, M\, \alpha)^{-1}(f) = f$.
Finsupp.lsingle definition
(a : α) : M →ₗ[R] α →₀ M
Full source 
/-- Interpret `Finsupp.single a` as a linear map. -/
def lsingle (a : α) : M →ₗ[R] α →₀ M :=
  { Finsupp.singleAddHom a with map_smul' := fun _ _ => (smul_single _ _ _).symm }
Linear single-point embedding of finitely supported functions
Informal description
For a fixed element $a \in \alpha$, the linear map $\operatorname{lsingle}(a) \colon M \to \alpha \to_{\text{f}} M$ sends each $m \in M$ to the finitely supported function that takes the value $m$ at $a$ and zero elsewhere. This map is linear with respect to the module structures on $M$ and $\alpha \to_{\text{f}} M$.
Finsupp.lhom_ext theorem
⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a b, φ (single a b) = ψ (single a b)) : φ = ψ
Full source 
/-- Two `R`-linear maps from `Finsupp X M` which agree on each `single x y` agree everywhere. -/
theorem lhom_ext ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a b, φ (single a b) = ψ (single a b)) : φ = ψ :=
  LinearMap.toAddMonoidHom_injective <| addHom_ext h
Extensionality of Linear Maps on Finitely Supported Functions via Single Functions
Informal description
Let $R$ be a semiring, $M$ an $R$-module, and $N$ an $R$-module. For any two $R$-linear maps $\varphi, \psi \colon (\alpha \to_{\text{f}} M) \to N$, if $\varphi$ and $\psi$ agree on all functions of the form $\text{single}(a, b)$ for $a \in \alpha$ and $b \in M$, then $\varphi = \psi$.
Finsupp.lhom_ext' theorem
⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a, φ.comp (lsingle a) = ψ.comp (lsingle a)) : φ = ψ
Full source 
/-- Two `R`-linear maps from `Finsupp X M` which agree on each `single x y` agree everywhere.

We formulate this fact using equality of linear maps `φ.comp (lsingle a)` and `ψ.comp (lsingle a)`
so that the `ext` tactic can apply a type-specific extensionality lemma to prove equality of these
maps. E.g., if `M = R`, then it suffices to verify `φ (single a 1) = ψ (single a 1)`. -/
-- Porting note: The priority should be higher than `LinearMap.ext`.
@[ext high]
theorem lhom_ext' ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a, φ.comp (lsingle a) = ψ.comp (lsingle a)) :
    φ = ψ :=
  lhom_ext fun a => LinearMap.congr_fun (h a)
Extensionality of Linear Maps on Finitely Supported Functions via Composition with Single Embeddings
Informal description
Let $R$ be a semiring, $M$ an $R$-module, and $N$ an $R$-module. For any two $R$-linear maps $\varphi, \psi \colon (\alpha \to_{\text{f}} M) \to N$, if for every $a \in \alpha$ the compositions $\varphi \circ \operatorname{lsingle}(a)$ and $\psi \circ \operatorname{lsingle}(a)$ are equal as linear maps from $M$ to $N$, then $\varphi = \psi$.
Finsupp.lapply definition
(a : α) : (α →₀ M) →ₗ[R] M
Full source 
/-- Interpret `fun f : α →₀ M ↦ f a` as a linear map. -/
def lapply (a : α) : (α →₀ M) →ₗ[R] M :=
  { Finsupp.applyAddHom a with map_smul' := fun _ _ => rfl }
Linear evaluation map at a point
Informal description
For a fixed element $a \in \alpha$, the evaluation map that sends a finitely supported function $f \colon \alpha \to M$ to its value $f(a) \in M$ is a linear map from the module of finitely supported functions $\alpha \to_{\text{f}} M$ to $M$.
Finsupp.instFaithfulSMulOfNonempty instance
[Nonempty α] [FaithfulSMul R M] : FaithfulSMul R (α →₀ M)
Full source 
instance [Nonempty α] [FaithfulSMul R M] : FaithfulSMul R (α →₀ M) :=
  .of_injective (Finsupp.lsingle <| Classical.arbitrary _) (Finsupp.single_injective _)
Faithfulness of Pointwise Scalar Multiplication on Finitely Supported Functions
Informal description
For any nonempty type $\alpha$ and any faithful scalar multiplication action of $R$ on $M$, the pointwise scalar multiplication action of $R$ on the space of finitely supported functions $\alpha \to_{\text{f}} M$ is also faithful. That is, if two scalar multiplications $r_1 \cdot f$ and $r_2 \cdot f$ are equal for all $f \in \alpha \to_{\text{f}} M$, then $r_1 = r_2$.
Finsupp.lsubtypeDomain definition
: (α →₀ M) →ₗ[R] s →₀ M
Full source 
/-- Interpret `Finsupp.subtypeDomain s` as a linear map. -/
def lsubtypeDomain : (α →₀ M) →ₗ[R] s →₀ M where
  toFun := subtypeDomain fun x => x ∈ s
  map_add' _ _ := subtypeDomain_add
  map_smul' _ _ := ext fun _ => rfl
Linear restriction map to a subset for finitely supported functions
Informal description
The linear map that restricts a finitely supported function \( f : \alpha \to_{\text{f}} M \) to the subset \( s \subseteq \alpha \), yielding a finitely supported function \( s \to_{\text{f}} M \). More precisely, for any \( f \), the function \( \text{lsubtypeDomain}\, s\, f \) is the restriction of \( f \) to \( s \), i.e., it maps each \( x \in s \) to \( f(x) \).
Finsupp.lsubtypeDomain_apply theorem
(f : α →₀ M) : (lsubtypeDomain s : (α →₀ M) →ₗ[R] s →₀ M) f = subtypeDomain (fun x => x ∈ s) f
Full source 
theorem lsubtypeDomain_apply (f : α →₀ M) :
    (lsubtypeDomain s : (α →₀ M) →ₗ[R] s →₀ M) f = subtypeDomain (fun x => x ∈ s) f :=
  rfl
Linear Restriction Map Evaluates to Subtype Restriction
Informal description
For any finitely supported function $f \colon \alpha \to_{\text{f}} M$, the linear restriction map $\mathrm{lsubtypeDomain}\, s$ applied to $f$ is equal to the restriction of $f$ to the subset $s \subseteq \alpha$, i.e., \[ \mathrm{lsubtypeDomain}\, s\, f = \mathrm{subtypeDomain}\, (\lambda x, x \in s)\, f. \]
Finsupp.lsingle_apply theorem
(a : α) (b : M) : (lsingle a : M →ₗ[R] α →₀ M) b = single a b
Full source 
@[simp]
theorem lsingle_apply (a : α) (b : M) : (lsingle a : M →ₗ[R] α →₀ M) b = single a b :=
  rfl
$\operatorname{lsingle}(a)(b) = \operatorname{single}(a, b)$
Informal description
For any element $a \in \alpha$ and any element $b \in M$, the linear map $\operatorname{lsingle}(a) \colon M \to \alpha \to_{\text{f}} M$ applied to $b$ yields the finitely supported function $\operatorname{single}(a, b) \colon \alpha \to_{\text{f}} M$ that takes the value $b$ at $a$ and zero elsewhere. In other words, $(\operatorname{lsingle}(a))(b) = \operatorname{single}(a, b)$.
Finsupp.lapply_apply theorem
(a : α) (f : α →₀ M) : (lapply a : (α →₀ M) →ₗ[R] M) f = f a
Full source 
@[simp]
theorem lapply_apply (a : α) (f : α →₀ M) : (lapply a : (α →₀ M) →ₗ[R] M) f = f a :=
  rfl
Evaluation of Linear Map on Finitely Supported Functions: $\operatorname{lapply}_a(f) = f(a)$
Informal description
For any element $a \in \alpha$ and any finitely supported function $f \colon \alpha \to M$, the linear evaluation map $\operatorname{lapply}_a$ satisfies $\operatorname{lapply}_a(f) = f(a)$.
Finsupp.lapply_comp_lsingle_same theorem
(a : α) : lapply a ∘ₗ lsingle a = (.id : M →ₗ[R] M)
Full source 
@[simp]
theorem lapply_comp_lsingle_same (a : α) : lapplylapply a ∘ₗ lsingle a = (.id : M →ₗ[R] M) := by ext; simp
Composition of Evaluation and Single-Point Embedding Yields Identity
Informal description
For any element $a \in \alpha$, the composition of the linear evaluation map $\operatorname{lapply}(a) \colon (\alpha \to_{\text{f}} M) \to M$ with the linear single-point embedding $\operatorname{lsingle}(a) \colon M \to (\alpha \to_{\text{f}} M)$ equals the identity linear map on $M$.
Finsupp.lapply_comp_lsingle_of_ne theorem
(a a' : α) (h : a ≠ a') : lapply a ∘ₗ lsingle a' = (0 : M →ₗ[R] M)
Full source 
@[simp]
theorem lapply_comp_lsingle_of_ne (a a' : α) (h : a ≠ a') :
    lapplylapply a ∘ₗ lsingle a' = (0 : M →ₗ[R] M) := by ext; simp [h.symm]
Composition of Evaluation and Single-Point Embedding is Zero for Distinct Points
Informal description
For any distinct elements $a$ and $a'$ in a type $\alpha$, the composition of the linear evaluation map $\operatorname{lapply}(a) \colon (\alpha \to_{\text{f}} M) \to M$ with the linear single-point embedding $\operatorname{lsingle}(a') \colon M \to (\alpha \to_{\text{f}} M)$ is the zero linear map from $M$ to $M$.
Finsupp.lmapDomain definition
(f : α → α') : (α →₀ M) →ₗ[R] α' →₀ M
Full source 
/-- Interpret `Finsupp.mapDomain` as a linear map. -/
def lmapDomain (f : α → α') : (α →₀ M) →ₗ[R] α' →₀ M where
  toFun := mapDomain f
  map_add' _ _ := mapDomain_add
  map_smul' := mapDomain_smul
Linear map induced by domain mapping on finitely supported functions
Informal description
Given a function $f \colon \alpha \to \alpha'$, the linear map `lmapDomain M R f` from the module of finitely supported functions $\alpha \to_{\text{f}} M$ to the module $\alpha' \to_{\text{f}} M$ is defined by applying `mapDomain f` to each function. This map is linear, meaning it preserves addition and scalar multiplication: - For any $v_1, v_2 \in \alpha \to_{\text{f}} M$, we have $\text{lmapDomain}\, f (v_1 + v_2) = \text{lmapDomain}\, f\, v_1 + \text{lmapDomain}\, f\, v_2$. - For any $r \in R$ and $v \in \alpha \to_{\text{f}} M$, we have $\text{lmapDomain}\, f (r \cdot v) = r \cdot \text{lmapDomain}\, f\, v$.
Finsupp.lmapDomain_apply theorem
(f : α → α') (l : α →₀ M) : (lmapDomain M R f : (α →₀ M) →ₗ[R] α' →₀ M) l = mapDomain f l
Full source 
@[simp]
theorem lmapDomain_apply (f : α → α') (l : α →₀ M) :
    (lmapDomain M R f : (α →₀ M) →ₗ[R] α' →₀ M) l = mapDomain f l :=
  rfl
Action of Linear Domain Mapping on Finitely Supported Functions
Informal description
For any function $f \colon \alpha \to \alpha'$ and any finitely supported function $l \colon \alpha \to_{\text{f}} M$, the linear map $\operatorname{lmapDomain}_{M,R}(f)$ applied to $l$ equals the finitely supported function obtained by mapping the domain of $l$ via $f$, i.e., \[ \operatorname{lmapDomain}_{M,R}(f)(l) = \operatorname{mapDomain}(f)(l). \]
Finsupp.lmapDomain_id theorem
: (lmapDomain M R _root_.id : (α →₀ M) →ₗ[R] α →₀ M) = LinearMap.id
Full source 
@[simp]
theorem lmapDomain_id : (lmapDomain M R _root_.id : (α →₀ M) →ₗ[R] α →₀ M) = LinearMap.id :=
  LinearMap.ext fun _ => mapDomain_id
Identity Domain Mapping Yields Identity Linear Map on Finitely Supported Functions
Informal description
The linear map `lmapDomain M R id` induced by the identity function on the domain $\alpha$ is equal to the identity linear map on the module of finitely supported functions $\alpha \to_{\text{f}} M$.
Finsupp.lmapDomain_comp theorem
(f : α → α') (g : α' → α'') : lmapDomain M R (g ∘ f) = (lmapDomain M R g).comp (lmapDomain M R f)
Full source 
theorem lmapDomain_comp (f : α → α') (g : α' → α'') :
    lmapDomain M R (g ∘ f) = (lmapDomain M R g).comp (lmapDomain M R f) :=
  LinearMap.ext fun _ => mapDomain_comp
Composition of Linear Maps Induced by Domain Mapping on Finitely Supported Functions
Informal description
Let $f \colon \alpha \to \alpha'$ and $g \colon \alpha' \to \alpha''$ be functions. Then the linear map induced by the composition $g \circ f$ on finitely supported functions is equal to the composition of the linear maps induced by $g$ and $f$ respectively. That is, \[ \text{lmapDomain}\, M\, R\, (g \circ f) = (\text{lmapDomain}\, M\, R\, g) \circ (\text{lmapDomain}\, M\, R\, f). \]
Finsupp.lcomapDomain definition
(f : α → β) (hf : Function.Injective f) : (β →₀ M) →ₗ[R] α →₀ M
Full source 
/-- Given `f : α → β` and a proof `hf` that `f` is injective, `lcomapDomain f hf` is the linear map
sending `l : β →₀ M` to the finitely supported function from `α` to `M` given by composing
`l` with `f`.

This is the linear version of `Finsupp.comapDomain`. -/
@[simps]
def lcomapDomain (f : α → β) (hf : Function.Injective f) : (β →₀ M) →ₗ[R] α →₀ M where
  toFun l := Finsupp.comapDomain f l hf.injOn
  map_add' x y := by ext; simp
  map_smul' c x := by ext; simp
Linear preimage composition of finitely supported functions
Informal description
Given an injective function $f : \alpha \to \beta$, the linear map `lcomapDomain f hf` sends a finitely supported function $l : \beta \to M$ to the finitely supported function $\alpha \to M$ obtained by composing $l$ with $f$. Here, $M$ is an $R$-module and $hf$ is a proof that $f$ is injective.
Finsupp.mapRange.linearMap definition
(f : M →ₗ[R] N) : (α →₀ M) →ₗ[R] α →₀ N
Full source 
/-- `Finsupp.mapRange` as a `LinearMap`. -/
@[simps apply]
def mapRange.linearMap (f : M →ₗ[R] N) : (α →₀ M) →ₗ[R] α →₀ N :=
  { mapRange.addMonoidHom f.toAddMonoidHom with
    toFun := (mapRange f f.map_zero : (α →₀ M) → α →₀ N)
    map_smul' := fun c v => mapRange_smul c v (f.map_smul c) }
Linear map of finitely supported functions via range mapping
Informal description
Given a linear map \( f \colon M \to N \) between \( R \)-modules, the linear map `Finsupp.mapRange.linearMap f` sends a finitely supported function \( g \colon \alpha \to_{\text{f}} M \) to the finitely supported function \( f \circ g \colon \alpha \to_{\text{f}} N \). This operation preserves the linear structure, meaning it respects addition and scalar multiplication.
Finsupp.mapRange.linearMap_id theorem
: mapRange.linearMap LinearMap.id = (LinearMap.id : (α →₀ M) →ₗ[R] _)
Full source 
@[simp]
theorem mapRange.linearMap_id :
    mapRange.linearMap LinearMap.id = (LinearMap.id : (α →₀ M) →ₗ[R] _) :=
  LinearMap.ext mapRange_id
Identity Linear Map Preserves Finitely Supported Functions
Informal description
The linear map obtained by applying the identity linear map `LinearMap.id : M →ₗ[R] M` to the range of a finitely supported function `α →₀ M` is equal to the identity linear map on `α →₀ M`.
Finsupp.mapRange.linearMap_comp theorem
(f : N →ₗ[R] P) (f₂ : M →ₗ[R] N) : (mapRange.linearMap (f.comp f₂) : (α →₀ _) →ₗ[R] _) = (mapRange.linearMap f).comp (mapRange.linearMap f₂)
Full source 
theorem mapRange.linearMap_comp (f : N →ₗ[R] P) (f₂ : M →ₗ[R] N) :
    (mapRange.linearMap (f.comp f₂) : (α →₀ _) →ₗ[R] _) =
      (mapRange.linearMap f).comp (mapRange.linearMap f₂) :=
  LinearMap.ext <| mapRange_comp f f.map_zero f₂ f₂.map_zero (comp f f₂).map_zero
Composition of Linear Maps on Finitely Supported Functions
Informal description
Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given linear maps $f \colon N \to P$ and $f_2 \colon M \to N$, the composition of the induced linear maps on finitely supported functions satisfies $$ \text{mapRange.linearMap}(f \circ f_2) = \text{mapRange.linearMap}(f) \circ \text{mapRange.linearMap}(f_2). $$ Here, $\text{mapRange.linearMap}(f)$ denotes the linear map from $\alpha \to_{\text{f}} M$ to $\alpha \to_{\text{f}} N$ induced by applying $f$ pointwise.
Finsupp.mapRange.linearMap_toAddMonoidHom theorem
(f : M →ₗ[R] N) : (mapRange.linearMap f).toAddMonoidHom = (mapRange.addMonoidHom f.toAddMonoidHom : (α →₀ M) →+ _)
Full source 
@[simp]
theorem mapRange.linearMap_toAddMonoidHom (f : M →ₗ[R] N) :
    (mapRange.linearMap f).toAddMonoidHom =
      (mapRange.addMonoidHom f.toAddMonoidHom : (α →₀ M) →+ _) :=
  AddMonoidHom.ext fun _ => rfl
Equality of Underlying Additive Monoid Homomorphisms for Linear Maps on Finitely Supported Functions
Informal description
For any linear map $f \colon M \to N$ between $R$-modules, the underlying additive monoid homomorphism of the linear map `Finsupp.mapRange.linearMap f` is equal to the additive monoid homomorphism `Finsupp.mapRange.addMonoidHom f.toAddMonoidHom` from $\alpha \to_{\text{f}} M$ to $\alpha \to_{\text{f}} N$.
Finsupp.mapRange.linearEquiv definition
(e : M ≃ₗ[R] N) : (α →₀ M) ≃ₗ[R] α →₀ N
Full source 
/-- `Finsupp.mapRange` as a `LinearEquiv`. -/
@[simps apply]
def mapRange.linearEquiv (e : M ≃ₗ[R] N) : (α →₀ M) ≃ₗ[R] α →₀ N :=
  { mapRange.linearMap e.toLinearMap,
    mapRange.addEquiv e.toAddEquiv with
    toFun := mapRange e e.map_zero
    invFun := mapRange e.symm e.symm.map_zero }
Linear equivalence of finitely supported functions via range mapping
Informal description
Given a linear equivalence \( e : M \simeq_{\text{lin}[R]} N \) between \( R \)-modules \( M \) and \( N \), the linear equivalence `Finsupp.mapRange.linearEquiv e` maps a finitely supported function \( g : \alpha \to_{\text{f}} M \) to the finitely supported function \( e \circ g : \alpha \to_{\text{f}} N \). Its inverse maps \( h : \alpha \to_{\text{f}} N \) to \( e^{-1} \circ h : \alpha \to_{\text{f}} M \). This construction preserves the linear structure, respecting addition and scalar multiplication.
Finsupp.mapRange.linearEquiv_refl theorem
: mapRange.linearEquiv (LinearEquiv.refl R M) = LinearEquiv.refl R (α →₀ M)
Full source 
@[simp]
theorem mapRange.linearEquiv_refl :
    mapRange.linearEquiv (LinearEquiv.refl R M) = LinearEquiv.refl R (α →₀ M) :=
  LinearEquiv.ext mapRange_id
Identity Linear Equivalence Preserves Finitely Supported Functions
Informal description
The linear equivalence obtained by applying the identity linear equivalence $\mathrm{id} \colon M \simeq_{\text{lin}[R]} M$ to the range of finitely supported functions is equal to the identity linear equivalence on the space of finitely supported functions $\alpha \to_{\text{f}} M$, i.e., \[ \operatorname{mapRange.linearEquiv}(\mathrm{id}_{M}) = \mathrm{id}_{\alpha \to_{\text{f}} M}. \]
Finsupp.mapRange.linearEquiv_trans theorem
(f : M ≃ₗ[R] N) (f₂ : N ≃ₗ[R] P) : (mapRange.linearEquiv (f.trans f₂) : (α →₀ _) ≃ₗ[R] _) = (mapRange.linearEquiv f).trans (mapRange.linearEquiv f₂)
Full source 
theorem mapRange.linearEquiv_trans (f : M ≃ₗ[R] N) (f₂ : N ≃ₗ[R] P) :
    (mapRange.linearEquiv (f.trans f₂) : (α →₀ _) ≃ₗ[R] _) =
      (mapRange.linearEquiv f).trans (mapRange.linearEquiv f₂) :=
  LinearEquiv.ext <| mapRange_comp f₂ f₂.map_zero f f.map_zero (f.trans f₂).map_zero
Composition of Linear Equivalences on Finitely Supported Functions
Informal description
Given linear equivalences $f \colon M \simeq_{\text{lin}[R]} N$ and $f₂ \colon N \simeq_{\text{lin}[R]} P$ between $R$-modules, the linear equivalence obtained by mapping the range of finitely supported functions through the composition $f \circ f₂$ is equal to the composition of the linear equivalences obtained by mapping the range through $f$ and then through $f₂$. That is, \[ \operatorname{mapRange.linearEquiv}(f \circ f₂) = \operatorname{mapRange.linearEquiv}(f) \circ \operatorname{mapRange.linearEquiv}(f₂). \]
Finsupp.mapRange.linearEquiv_symm theorem
(f : M ≃ₗ[R] N) : ((mapRange.linearEquiv f).symm : (α →₀ _) ≃ₗ[R] _) = mapRange.linearEquiv f.symm
Full source 
@[simp]
theorem mapRange.linearEquiv_symm (f : M ≃ₗ[R] N) :
    ((mapRange.linearEquiv f).symm : (α →₀ _) ≃ₗ[R] _) = mapRange.linearEquiv f.symm :=
  LinearEquiv.ext fun _x => rfl
Inverse of Range-Mapped Linear Equivalence of Finitely Supported Functions
Informal description
Given a linear equivalence $f \colon M \simeq_{\text{lin}[R]} N$ between $R$-modules $M$ and $N$, the inverse of the linear equivalence $\operatorname{mapRange.linearEquiv}(f) \colon (\alpha \to_{\text{f}} M) \simeq_{\text{lin}[R]} (\alpha \to_{\text{f}} N)$ is equal to the linear equivalence obtained by applying $f^{-1}$ to the range, i.e., \[ \big(\operatorname{mapRange.linearEquiv}(f)\big)^{-1} = \operatorname{mapRange.linearEquiv}(f^{-1}). \]
Finsupp.mapRange.linearEquiv_toAddEquiv theorem
(f : M ≃ₗ[R] N) : (mapRange.linearEquiv f).toAddEquiv = (mapRange.addEquiv f.toAddEquiv : (α →₀ M) ≃+ _)
Full source 
@[simp 1500]
theorem mapRange.linearEquiv_toAddEquiv (f : M ≃ₗ[R] N) :
    (mapRange.linearEquiv f).toAddEquiv = (mapRange.addEquiv f.toAddEquiv : (α →₀ M) ≃+ _) :=
  AddEquiv.ext fun _ => rfl
Additive Equivalence Underlying Linear Equivalence of Finitely Supported Functions
Informal description
Given a linear equivalence $f : M \simeq_{\text{lin}[R]} N$ between $R$-modules $M$ and $N$, the underlying additive equivalence of the linear equivalence `mapRange.linearEquiv f` is equal to the additive equivalence `mapRange.addEquiv f.toAddEquiv` between the spaces of finitely supported functions $\alpha \to_{\text{f}} M$ and $\alpha \to_{\text{f}} N$.
Finsupp.mapRange.linearEquiv_toLinearMap theorem
(f : M ≃ₗ[R] N) : (mapRange.linearEquiv f).toLinearMap = (mapRange.linearMap f.toLinearMap : (α →₀ M) →ₗ[R] _)
Full source 
@[simp]
theorem mapRange.linearEquiv_toLinearMap (f : M ≃ₗ[R] N) :
    (mapRange.linearEquiv f).toLinearMap = (mapRange.linearMap f.toLinearMap : (α →₀ M) →ₗ[R] _) :=
  LinearMap.ext fun _ => rfl
Underlying Linear Map of Range-Mapping Linear Equivalence
Informal description
Given a linear equivalence $f \colon M \simeq_{\text{lin}[R]} N$ between $R$-modules $M$ and $N$, the underlying linear map of the linear equivalence $\text{mapRange.linearEquiv}\, f$ is equal to the linear map $\text{mapRange.linearMap}\, f.\text{toLinearMap}$ from $\alpha \to_{\text{f}} M$ to $\alpha \to_{\text{f}} N$.
Finsupp.finsuppProdLEquiv definition
{α β : Type*} (R : Type*) {M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] : (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M
Full source 
/-- The linear equivalence between `α × β →₀ M` and `α →₀ β →₀ M`.

This is the `LinearEquiv` version of `Finsupp.finsuppProdEquiv`. -/
noncomputable def finsuppProdLEquiv {α β : Type*} (R : Type*) {M : Type*} [Semiring R]
    [AddCommMonoid M] [Module R M] : (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M :=
  { finsuppProdEquiv with
    map_add' := fun f g => by
      ext
      simp [finsuppProdEquiv, curry_apply]
    map_smul' := fun c f => by
      ext
      simp [finsuppProdEquiv, curry_apply] }
Linear equivalence between finitely supported functions on a product and curried finitely supported functions
Informal description
The linear equivalence `finsuppProdLEquiv` between the space of finitely supported functions $\alpha \times \beta \to_{\text{f}} M$ and the space of finitely supported functions $\alpha \to_{\text{f}} (\beta \to_{\text{f}} M)$. This is the linear version of the equivalence `finsuppProdEquiv`, where the equivalence is given by currying and uncurrying operations that preserve addition and scalar multiplication. Specifically: - For any $f \in \alpha \times \beta \to_{\text{f}} M$ and $(x, y) \in \alpha \times \beta$, the image under the equivalence is given by $(finsuppProdLEquiv\, R\, f)\, x\, y = f(x, y)$. - For any $f \in \alpha \to_{\text{f}} (\beta \to_{\text{f}} M)$ and $(x, y) \in \alpha \times \beta$, the preimage under the equivalence is given by $(finsuppProdLEquiv\, R)^{-1}\, f\, (x, y) = f\, x\, y$. Here, $R$ is a semiring, $M$ is an additive commutative monoid equipped with an $R$-module structure, and $\alpha, \beta$ are arbitrary types.
Finsupp.finsuppProdLEquiv_apply theorem
{α β R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] (f : α × β →₀ M) (x y) : finsuppProdLEquiv R f x y = f (x, y)
Full source 
@[simp]
theorem finsuppProdLEquiv_apply {α β R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
    (f : α × βα × β →₀ M) (x y) : finsuppProdLEquiv R f x y = f (x, y) := by
  rw [finsuppProdLEquiv, LinearEquiv.coe_mk, finsuppProdEquiv, Finsupp.curry_apply]
Evaluation of Linear Currying Equivalence: $(\text{finsuppProdLEquiv}\, R\, f)(x)(y) = f(x, y)$
Informal description
For any types $\alpha$ and $\beta$, semiring $R$, and $R$-module $M$, the linear equivalence $\text{finsuppProdLEquiv}\, R$ between finitely supported functions $\alpha \times \beta \to_{\text{f}} M$ and finitely supported functions $\alpha \to_{\text{f}} (\beta \to_{\text{f}} M)$ satisfies $(\text{finsuppProdLEquiv}\, R\, f)(x)(y) = f(x, y)$ for all $f \in \alpha \times \beta \to_{\text{f}} M$, $x \in \alpha$, and $y \in \beta$.
Finsupp.finsuppProdLEquiv_symm_apply theorem
{α β R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] (f : α →₀ β →₀ M) (xy) : (finsuppProdLEquiv R).symm f xy = f xy.1 xy.2
Full source 
@[simp]
theorem finsuppProdLEquiv_symm_apply {α β R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
    (f : α →₀ β →₀ M) (xy) : (finsuppProdLEquiv R).symm f xy = f xy.1 xy.2 := by
  conv_rhs =>
    rw [← (finsuppProdLEquiv R).apply_symm_apply f, finsuppProdLEquiv_apply]
Evaluation of Inverse Linear Currying Equivalence: $(\text{finsuppProdLEquiv}\, R)^{-1}\, f\, (x, y) = f\, x\, y$
Informal description
For any types $\alpha$ and $\beta$, semiring $R$, and $R$-module $M$, the inverse of the linear equivalence $\text{finsuppProdLEquiv}\, R$ satisfies $(\text{finsuppProdLEquiv}\, R)^{-1}\, f\, (x, y) = f\, x\, y$ for all $f \in \alpha \to_{\text{f}} (\beta \to_{\text{f}} M)$ and $(x, y) \in \alpha \times \beta$.
Module.subsingletonEquiv definition
(R M ι : Type*) [Semiring R] [Subsingleton R] [AddCommMonoid M] [Module R M] : M ≃ₗ[R] ι →₀ R
Full source 
/-- If `Subsingleton R`, then `M ≃ₗ[R] ι →₀ R` for any type `ι`. -/
@[simps]
def Module.subsingletonEquiv (R M ι : Type*) [Semiring R] [Subsingleton R] [AddCommMonoid M]
    [Module R M] : M ≃ₗ[R] ι →₀ R where
  toFun _ := 0
  invFun _ := 0
  left_inv m := by
    letI := Module.subsingleton R M
    simp only [eq_iff_true_of_subsingleton]
  right_inv f := by simp only [eq_iff_true_of_subsingleton]
  map_add' _ _ := (add_zero 0).symm
  map_smul' r _ := (smul_zero r).symm
Subsingleton Module Equivalence to Finitely Supported Functions
Informal description
When $R$ is a subsingleton semiring (i.e., all elements of $R$ are equal), there is a linear equivalence between any $R$-module $M$ and the space of finitely supported functions $\iota \to_{\text{f}} R$ for any type $\iota$. Specifically, both the forward and backward maps send every element to the zero function or zero element, respectively, and all relevant properties hold trivially due to the subsingleton condition.