mathlib documentation

linear_algebra.dfinsupp

Properties of the module Π₀ i, M i #

Given an indexed collection of R-modules M i, the R-module 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, module, linear algebra

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 : ι), module 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_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module 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_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] [add_comm_monoid N] [module 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_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] [add_comm_monoid N] [module R N] ⦃φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ (h : ∀ (i : ι), φ ∘ₗ dfinsupp.lsingle i = ψ ∘ₗ 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_4} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module 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_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module 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_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] (i : ι) (x : M i) :
@[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 : ι), module R (M i)] (i : ι) (f : Π₀ (i : ι), M i) :
@[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 : ι), module R (M i)] [add_comm_monoid N] [module 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.module_of_linear_map.

Equations
@[instance]
def dfinsupp.module_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 : ι), module R (M i)] [add_comm_monoid N] [module R N] [semiring S] [module S N] [smul_comm_class R S N] :
module S (Π₀ (i : ι), M i →ₗ[R] N)

Typeclass inference can't find dfinsupp.module 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
@[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 : ι), module R (M i)] [add_comm_monoid N] [module R N] [semiring S] [module S N] [smul_comm_class R S N] (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) :
@[simp]
theorem dfinsupp.lsum_apply_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 : ι), module R (M i)] [add_comm_monoid N] [module R N] [semiring S] [module S N] [smul_comm_class R S N] (F : Π (i : ι), M i →ₗ[R] N) (ᾰ : Π₀ (i : ι), (λ (i : ι), M i) i) :
((dfinsupp.lsum S) F) = (dfinsupp.sum_add_hom (λ (i : ι), (F i).to_add_monoid_hom))
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 : ι), module R (M i)] [add_comm_monoid N] [module R N] [semiring S] [module 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

Bundled versions of dfinsupp.map_range #

The names should match the equivalent bundled finsupp.map_range definitions.

theorem dfinsupp.map_range_smul {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (f : Π (i : ι), β₁ iβ₂ i) (hf : ∀ (i : ι), f i 0 = 0) (r : R) (hf' : ∀ (i : ι) (x : β₁ i), f i (r x) = r f i x) (g : Π₀ (i : ι), β₁ i) :
def dfinsupp.map_range.linear_map {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (f : Π (i : ι), β₁ i →ₗ[R] β₂ i) :
(Π₀ (i : ι), β₁ i) →ₗ[R] Π₀ (i : ι), β₂ i

dfinsupp.map_range as an linear_map.

Equations
@[simp]
theorem dfinsupp.map_range.linear_map_apply {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (f : Π (i : ι), β₁ i →ₗ[R] β₂ i) (ᾰ : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
(dfinsupp.map_range.linear_map f) = dfinsupp.map_range (λ (i : ι) (x : β₁ i), (f i) x) _
@[simp]
theorem dfinsupp.map_range.linear_map_id {ι : Type u_1} {R : Type u_2} [semiring R] {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₂ i)] :
theorem dfinsupp.map_range.linear_map_comp {ι : Type u_1} {R : Type u_2} [semiring R] {β : ι → Type u_6} {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (f : Π (i : ι), β₁ i →ₗ[R] β₂ i) (f₂ : Π (i : ι), β i →ₗ[R] β₁ i) :
def dfinsupp.map_range.linear_equiv {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (e : Π (i : ι), β₁ i ≃ₗ[R] β₂ i) :
(Π₀ (i : ι), β₁ i) ≃ₗ[R] Π₀ (i : ι), β₂ i

dfinsupp.map_range.linear_map as an linear_equiv.

Equations
@[simp]
theorem dfinsupp.map_range.linear_equiv_apply {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (e : Π (i : ι), β₁ i ≃ₗ[R] β₂ i) (ᾰ : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
(dfinsupp.map_range.linear_equiv e) = dfinsupp.map_range (λ (i : ι) (x : β₁ i), (e i) x) _
@[simp]
theorem dfinsupp.map_range.linear_equiv_refl {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), module R (β₁ i)] :
dfinsupp.map_range.linear_equiv (λ (i : ι), linear_equiv.refl R (β₁ i)) = linear_equiv.refl R (Π₀ (i : ι), β₁ i)
theorem dfinsupp.map_range.linear_equiv_trans {ι : Type u_1} {R : Type u_2} [semiring R] {β : ι → Type u_6} {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (f : Π (i : ι), β i ≃ₗ[R] β₁ i) (f₂ : Π (i : ι), β₁ i ≃ₗ[R] β₂ i) :
@[simp]
theorem dfinsupp.map_range.linear_equiv_symm {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (e : Π (i : ι), β₁ i ≃ₗ[R] β₂ i) :
def dfinsupp.basis {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] {η : ι → Type u_3} (b : Π (i : ι), basis (η i) R (M i)) :
basis (Σ (i : ι), η i) R (Π₀ (i : ι), M i)

The direct sum of free modules is free.

Note that while this is stated for dfinsupp not direct_sum, the types are defeq.

Equations
theorem submodule.dfinsupp_sum_mem {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] {β : ι → Type u_3} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (S : submodule R N) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i → N) (h : ∀ (c : ι), f c 0g c (f c) S) :
f.sum g S
theorem submodule.dfinsupp_sum_add_hom_mem {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] {β : ι → Type u_3} [Π (i : ι), add_zero_class (β i)] (S : submodule R N) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i →+ N) (h : ∀ (c : ι), f c 0(g c) (f c) S) :
theorem submodule.supr_eq_range_dfinsupp_lsum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] (p : ι → submodule R N) :
supr p = ((dfinsupp.lsum ) (λ (i : ι), (p i).subtype)).range

The supremum of a family of submodules is equal to the range of dfinsupp.lsum; that is every element in the supr can be produced from taking a finite number of non-zero elements of p i, coercing them to N, and summing them.

theorem submodule.mem_supr_iff_exists_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] (p : ι → submodule R N) (x : N) :
x supr p ∃ (f : Π₀ (i : ι), (p i)), ((dfinsupp.lsum ) (λ (i : ι), (p i).subtype)) f = x
theorem submodule.mem_supr_iff_exists_dfinsupp' {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] (p : ι → submodule R N) [Π (i : ι) (x : (p i)), decidable (x 0)] (x : N) :
x supr p ∃ (f : Π₀ (i : ι), (p i)), f.sum (λ (i : ι) (xi : (p i)), xi) = x

A variant of submodule.mem_supr_iff_exists_dfinsupp with the RHS fully unfolded.