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:
-
dfinsupp.lsingle a : M →ₗ[R] Π₀ i, M i:dfinsupp.single aas a linear map; -
dfinsupp.lmk s : (Π i : (↑s : set ι), M i) →ₗ[R] Π₀ i, M i:dfinsupp.single aas a linear map; -
dfinsupp.lapply i : (Π₀ i, M i) →ₗ[R] M: the mapλ f, f ias a linear map; -
dfinsupp.lsum:dfinsupp.sumordfinsupp.lift_add_homas alinear_map;
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 ι) :
dfinsupp.mk as a linear_map.
Equations
- dfinsupp.lmk s = {to_fun := dfinsupp.mk s, map_add' := _, map_smul' := _}
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 : ι) :
dfinsupp.single as a linear_map
Equations
- dfinsupp.lsingle i = {to_fun := dfinsupp.single i, map_add' := _, map_smul' := _}
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 : ι) :
Interpret λ (f : Π₀ i, M i), f i as a linear map.
@[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) :
⇑(dfinsupp.lmk s) x = dfinsupp.mk s x
@[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) :
⇑(dfinsupp.lsingle i) x = dfinsupp.single i x
@[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) :
⇑(dfinsupp.lapply i) f = ⇑f 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.
@[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] :
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 : ι) :
⇑((dfinsupp.lsum S).symm) F i = F ∘ₗ dfinsupp.lsingle 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] :
The dfinsupp version of finsupp.lsum.
See note [bundled maps over different rings] for why separate R and S semirings are used.
Equations
- dfinsupp.lsum S = {to_fun := λ (F : Π (i : ι), M i →ₗ[R] N), {to_fun := ⇑(dfinsupp.sum_add_hom (λ (i : ι), (F i).to_add_monoid_hom)), map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _, inv_fun := λ (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι), F ∘ₗ dfinsupp.lsingle i, left_inv := _, right_inv := _}
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) :
dfinsupp.map_range f hf (r • g) = r • dfinsupp.map_range f hf g
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) :
dfinsupp.map_range as an linear_map.
Equations
- dfinsupp.map_range.linear_map f = {to_fun := dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(f i) x) _, map_add' := _, map_smul' := _}
@[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)] :
dfinsupp.map_range.linear_map (λ (i : ι), linear_map.id) = linear_map.id
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) :
dfinsupp.map_range.linear_map (λ (i : ι), f i ∘ₗ f₂ i) = dfinsupp.map_range.linear_map f ∘ₗ dfinsupp.map_range.linear_map f₂
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) :
dfinsupp.map_range.linear_map as an linear_equiv.
Equations
- dfinsupp.map_range.linear_equiv e = {to_fun := dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(e i) x) _, map_add' := _, map_smul' := _, inv_fun := dfinsupp.map_range (λ (i : ι) (x : β₂ i), ⇑((e i).symm) x) _, left_inv := _, right_inv := _}
@[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) :
dfinsupp.map_range.linear_equiv (λ (i : ι), f i ≪≫ₗ f₂ i) = dfinsupp.map_range.linear_equiv f ≪≫ₗ dfinsupp.map_range.linear_equiv f₂
@[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) :
(dfinsupp.map_range.linear_equiv e).symm = dfinsupp.map_range.linear_equiv (λ (i : ι), (e i).symm)
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
- dfinsupp.basis b = {repr := dfinsupp.map_range.linear_equiv (λ (i : ι), (b i).repr) ≪≫ₗ (sigma_finsupp_lequiv_dfinsupp R).symm}
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 ≠ 0 → g c (⇑f c) ∈ 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) :
⇑(dfinsupp.sum_add_hom g) f ∈ 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) :
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) :
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) :
A variant of submodule.mem_supr_iff_exists_dfinsupp with the RHS fully unfolded.