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 : ι), φ.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_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 : ι) :
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
@[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 : ι), 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) :

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) (g : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
(dfinsupp.map_range.linear_map f) g = dfinsupp.map_range (λ (i : ι) (x : β₁ i), (f i) x) _ g
@[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) (g : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
(dfinsupp.map_range.linear_equiv e) g = dfinsupp.map_range (λ (i : ι) (x : β₁ i), (e i) x) _ g
@[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) :