mathlib documentation

linear_algebra.dfinsupp

Properties of the semimodule Π₀ i, M i #

Given an indexed collection of R-semimodules M i, the R-semimodule structure on Π₀ i, M i is defined in data.dfinsupp.

In this file we define linear_map versions of various maps:

Implementation notes #

This file should try to mirror linear_algebra.finsupp where possible. The API of finsupp is much more developed, but many lemmas in that file should be eligible to copy over.

Tags #

function with finite support, semimodule, linear algebra

source
def dfinsupp.lmk {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] (s : finset ι) :
(Π (i : ↥↑s), M ↑i) →ₗ[R] Π₀ (i : ι), M i

dfinsupp.mk as a linear_map.

Equations
source
def dfinsupp.lsingle {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] (i : ι) :
M i →ₗ[R] Π₀ (i : ι), M i

dfinsupp.single as a linear_map

Equations
source
theorem dfinsupp.lhom_ext {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] [add_comm_monoid N] [semimodule R N] ⦃φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ (h : ∀ (i : ι) (x : M i), ⇑φ (dfinsupp.single i x) = ⇑ψ (dfinsupp.single i x)) :
φ = ψ

Two R-linear maps from Π₀ i, M i which agree on each single i x agree everywhere.

source
@[ext]
theorem dfinsupp.lhom_ext' {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] [add_comm_monoid N] [semimodule R N] ⦃φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ (h : ∀ (i : ι), φ.comp (dfinsupp.lsingle i) = ψ.comp (dfinsupp.lsingle i)) :
φ = ψ

Two R-linear maps from Π₀ i, M i which agree on each single i x agree everywhere.

See note [partially-applied ext lemmas]. After apply this lemma, if M = R then it suffices to verify φ (single a 1) = ψ (single a 1).

source
def dfinsupp.lapply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] (i : ι) :
(Π₀ (i : ι), M i) →ₗ[R] M i

Interpret λ (f : Π₀ i, M i), f i as a linear map.

Equations
source
@[simp]
theorem dfinsupp.lmk_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] (s : finset ι) (x : Π (i : ↥↑s), (λ (i : ι), M i) ↑i) :
⇑(dfinsupp.lmk s) x = dfinsupp.mk s x
source
@[simp]
theorem dfinsupp.lsingle_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] (i : ι) (x : M i) :
⇑(dfinsupp.lsingle i) x = dfinsupp.single i x
source
@[simp]
theorem dfinsupp.lapply_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] (i : ι) (f : Π₀ (i : ι), M i) :
⇑(dfinsupp.lapply i) f = ⇑f i
source
@[instance]
def dfinsupp.add_comm_monoid_of_linear_map {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] [add_comm_monoid N] [semimodule R N] :
add_comm_monoid (Π₀ (i : ι), M i →ₗ[R] N)

Typeclass inference can't find dfinsupp.add_comm_monoid without help for this case. This instance allows it to be found where it is needed on the LHS of the colon in dfinsupp.semimodule_of_linear_map.

Equations
source
@[instance]
def dfinsupp.semimodule_of_linear_map {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : ι → Type u_4} {N : Type u_5} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] [add_comm_monoid N] [semimodule R N] [semiring S] [semimodule S N] [smul_comm_class R S N] :
semimodule S (Π₀ (i : ι), M i →ₗ[R] N)

Typeclass inference can't find dfinsupp.semimodule without help for this case. This is needed to define dfinsupp.lsum below.

The cause seems to be an inability to unify the Π i, add_comm_monoid (M i →ₗ[R] N) instance that we have with the Π i, has_zero (M i →ₗ[R] N) instance which appears as a parameter to the dfinsupp type.

Equations
source
@[simp]
theorem dfinsupp.lsum_symm_apply {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] [add_comm_monoid N] [semimodule R N] [semiring S] [semimodule S N] [smul_comm_class R S N] (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) :
⇑((dfinsupp.lsum S).symm) F i = F.comp (dfinsupp.lsingle i)
source
def dfinsupp.lsum {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] [add_comm_monoid N] [semimodule R N] [semiring S] [semimodule S N] [smul_comm_class R S N] :
(Π (i : ι), M i →ₗ[R] N) ≃ₗ[S] (Π₀ (i : ι), M i) →ₗ[R] N

The dfinsupp version of finsupp.lsum.

See note [bundled maps over different rings] for why separate R and S semirings are used.

Equations
source
@[simp]
theorem dfinsupp.lsum_apply {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] [add_comm_monoid N] [semimodule R N] [semiring S] [semimodule S N] [smul_comm_class R S N] (F : Π (i : ι), M i →ₗ[R] N) :
⇑(dfinsupp.lsum S) F = {to_fun := ⇑(dfinsupp.sum_add_hom (λ (i : ι), (F i).to_add_monoid_hom)), map_add' := _, map_smul' := _}