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

def dfinsupp.lmk {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [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
def dfinsupp.lsingle {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [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
theorem dfinsupp.lhom_ext {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {N : Type u_4} [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.

@[ext]
theorem dfinsupp.lhom_ext' {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {N : Type u_4} [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).

def dfinsupp.lapply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [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
@[simp]
theorem dfinsupp.lmk_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [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) :

@[simp]
theorem dfinsupp.lsingle_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] (i : ι) (x : M i) :

@[simp]
theorem dfinsupp.lapply_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] (i : ι) (f : Π₀ (i : ι), M i) :

@[simp]
theorem dfinsupp.lsum_symm_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {N : Type u_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] [add_comm_monoid N] [semimodule R N] (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) :

def dfinsupp.lsum {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {N : Type u_4} [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) ≃+ ((Π₀ (i : ι), M i) →ₗ[R] N)

The dfinsupp version of finsupp.lsum.

Equations
@[simp]
theorem dfinsupp.lsum_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {N : Type u_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), semimodule R (M i)] [add_comm_monoid N] [semimodule R N] (F : Π (i : ι), M i →ₗ[R] N) :