def
finsupp.lsingle
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M] :
Equations
- finsupp.lsingle a = {to_fun := finsupp.single a, map_add' := _, map_smul' := _}
def
finsupp.lsubtype_domain
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(s : set α) :
Equations
- finsupp.lsubtype_domain s = {to_fun := finsupp.subtype_domain (λ (x : α), x ∈ s), map_add' := _, map_smul' := _}
theorem
finsupp.lsubtype_domain_apply
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(s : set α)
(f : α →₀ M) :
⇑(finsupp.lsubtype_domain s) f = finsupp.subtype_domain (λ (x : α), x ∈ s) f
@[simp]
theorem
finsupp.lsingle_apply
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(a : α)
(b : M) :
⇑(finsupp.lsingle a) b = finsupp.single a b
@[simp]
theorem
finsupp.lapply_apply
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(a : α)
(f : α →₀ M) :
⇑(finsupp.lapply a) f = ⇑f a
@[simp]
theorem
finsupp.ker_lsingle
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(a : α) :
(finsupp.lsingle a).ker = ⊥
theorem
finsupp.lsingle_range_le_ker_lapply
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(s t : set α) :
disjoint s t → ((⨆ (a : α) (H : a ∈ s), (finsupp.lsingle a).range) ≤ ⨅ (a : α) (H : a ∈ t), (finsupp.lapply a).ker)
theorem
finsupp.infi_ker_lapply_le_bot
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M] :
(⨅ (a : α), (finsupp.lapply a).ker) ≤ ⊥
theorem
finsupp.supr_lsingle_range
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M] :
(⨆ (a : α), (finsupp.lsingle a).range) = ⊤
theorem
finsupp.disjoint_lsingle_lsingle
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(s t : set α) :
disjoint s t → disjoint (⨆ (a : α) (H : a ∈ s), (finsupp.lsingle a).range) (⨆ (a : α) (H : a ∈ t), (finsupp.lsingle a).range)
theorem
finsupp.span_single_image
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(s : set M)
(a : α) :
submodule.span R (finsupp.single a '' s) = submodule.map (finsupp.lsingle a) (submodule.span R s)
theorem
finsupp.mem_supported
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{s : set α}
(p : α →₀ M) :
theorem
finsupp.mem_supported'
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{s : set α}
(p : α →₀ M) :
theorem
finsupp.single_mem_supported
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{s : set α}
{a : α}
(b : M) :
a ∈ s → finsupp.single a b ∈ finsupp.supported M R s
theorem
finsupp.supported_eq_span_single
{α : Type u_1}
(R : Type u_4)
[ring R]
(s : set α) :
finsupp.supported R R s = submodule.span R ((λ (i : α), finsupp.single i 1) '' s)
def
finsupp.restrict_dom
{α : Type u_1}
(M : Type u_2)
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
(s : set α) :
(α →₀ M) →ₗ[R] ↥(finsupp.supported M R s)
Equations
- finsupp.restrict_dom M R s = linear_map.cod_restrict (finsupp.supported M R s) {to_fun := finsupp.filter (λ (_x : α), _x ∈ s), map_add' := _, map_smul' := _} _
@[simp]
theorem
finsupp.restrict_dom_apply
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(s : set α)
(l : α →₀ M) :
↑(⇑(finsupp.restrict_dom M R s) l) = finsupp.filter (λ (_x : α), _x ∈ s) l
theorem
finsupp.restrict_dom_comp_subtype
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(s : set α) :
(finsupp.restrict_dom M R s).comp (finsupp.supported M R s).subtype = linear_map.id
theorem
finsupp.range_restrict_dom
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(s : set α) :
(finsupp.restrict_dom M R s).range = ⊤
theorem
finsupp.supported_mono
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
{s t : set α} :
s ⊆ t → finsupp.supported M R s ≤ finsupp.supported M R t
@[simp]
theorem
finsupp.supported_empty
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M] :
finsupp.supported M R ∅ = ⊥
@[simp]
theorem
finsupp.supported_univ
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M] :
finsupp.supported M R set.univ = ⊤
theorem
finsupp.supported_Union
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
{δ : Type u_3}
(s : δ → set α) :
finsupp.supported M R (⋃ (i : δ), s i) = ⨆ (i : δ), finsupp.supported M R (s i)
theorem
finsupp.supported_union
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(s t : set α) :
finsupp.supported M R (s ∪ t) = finsupp.supported M R s ⊔ finsupp.supported M R t
theorem
finsupp.supported_Inter
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
{ι : Type u_3}
(s : ι → set α) :
finsupp.supported M R (⋂ (i : ι), s i) = ⨅ (i : ι), finsupp.supported M R (s i)
def
finsupp.supported_equiv_finsupp
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
(s : set α) :
Equations
- finsupp.supported_equiv_finsupp s = let F : ↥(finsupp.supported M R s) ≃ (↥s →₀ M) := finsupp.restrict_support_equiv s M in F.to_linear_equiv _
def
finsupp.lsum
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N] :
finsupp.sum as a linear map.
@[simp]
theorem
finsupp.coe_lsum
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : α → (M →ₗ[R] N)) :
theorem
finsupp.lsum_apply
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : α → (M →ₗ[R] N))
(l : α →₀ M) :
⇑(finsupp.lsum f) l = l.sum (λ (b : α), ⇑(f b))
theorem
finsupp.lsum_single
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : α → (M →ₗ[R] N))
(i : α)
(m : M) :
⇑(finsupp.lsum f) (finsupp.single i m) = ⇑(f i) m
def
finsupp.lmap_domain
{α : Type u_1}
(M : Type u_2)
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{α' : Type u_5} :
Equations
- finsupp.lmap_domain M R f = {to_fun := finsupp.map_domain f, map_add' := _, map_smul' := _}
@[simp]
theorem
finsupp.lmap_domain_apply
{α : Type u_1}
(M : Type u_2)
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{α' : Type u_5}
(f : α → α')
(l : α →₀ M) :
⇑(finsupp.lmap_domain M R f) l = finsupp.map_domain f l
@[simp]
theorem
finsupp.lmap_domain_id
{α : Type u_1}
(M : Type u_2)
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M] :
theorem
finsupp.lmap_domain_comp
{α : Type u_1}
(M : Type u_2)
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{α' : Type u_5}
{α'' : Type u_6}
(f : α → α')
(g : α' → α'') :
finsupp.lmap_domain M R (g ∘ f) = (finsupp.lmap_domain M R g).comp (finsupp.lmap_domain M R f)
theorem
finsupp.supported_comap_lmap_domain
{α : Type u_1}
(M : Type u_2)
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{α' : Type u_5}
(f : α → α')
(s : set α') :
finsupp.supported M R (f ⁻¹' s) ≤ submodule.comap (finsupp.lmap_domain M R f) (finsupp.supported M R s)
theorem
finsupp.lmap_domain_supported
{α : Type u_1}
(M : Type u_2)
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{α' : Type u_5}
[nonempty α]
(f : α → α')
(s : set α) :
submodule.map (finsupp.lmap_domain M R f) (finsupp.supported M R s) = finsupp.supported M R (f '' s)
theorem
finsupp.lmap_domain_disjoint_ker
{α : Type u_1}
(M : Type u_2)
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{α' : Type u_5}
(f : α → α')
{s : set α} :
(∀ (a b : α), a ∈ s → b ∈ s → f a = f b → a = b) → disjoint (finsupp.supported M R s) (finsupp.lmap_domain M R f).ker
def
finsupp.total
(α : Type u_1)
(M : Type u_2)
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M] :
Interprets (l : α →₀ R) as linear combination of the elements in the family (v : α → M) and evaluates this linear combination.
Equations
- finsupp.total α M R v = finsupp.lsum (λ (i : α), linear_map.id.smul_right (v i))
theorem
finsupp.total_apply
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{v : α → M}
(l : α →₀ R) :
⇑(finsupp.total α M R v) l = l.sum (λ (i : α) (a : R), a • v i)
@[simp]
theorem
finsupp.total_single
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{v : α → M}
(c : R)
(a : α) :
⇑(finsupp.total α M R v) (finsupp.single a c) = c • v a
theorem
finsupp.total_range
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{v : α → M} :
function.surjective v → (finsupp.total α M R v).range = ⊤
theorem
finsupp.range_total
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{v : α → M} :
(finsupp.total α M R v).range = submodule.span R (set.range v)
theorem
finsupp.lmap_domain_total
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{α' : Type u_5}
{M' : Type u_6}
[add_comm_group M']
[module R M']
{v : α → M}
{v' : α' → M'}
(f : α → α')
(g : M →ₗ[R] M') :
(∀ (i : α), ⇑g (v i) = v' (f i)) → (finsupp.total α' M' R v').comp (finsupp.lmap_domain R R f) = g.comp (finsupp.total α M R v)
theorem
finsupp.total_emb_domain
{α : Type u_1}
(R : Type u_4)
[ring R]
{α' : Type u_5}
{M' : Type u_6}
[add_comm_group M']
[module R M']
{v' : α' → M'}
(f : α ↪ α')
(l : α →₀ R) :
⇑(finsupp.total α' M' R v') (finsupp.emb_domain f l) = ⇑(finsupp.total α M' R (v' ∘ ⇑f)) l
theorem
finsupp.total_map_domain
{α : Type u_1}
(R : Type u_4)
[ring R]
{α' : Type u_5}
{M' : Type u_6}
[add_comm_group M']
[module R M']
{v' : α' → M'}
(f : α → α')
(hf : function.injective f)
(l : α →₀ R) :
⇑(finsupp.total α' M' R v') (finsupp.map_domain f l) = ⇑(finsupp.total α M' R (v' ∘ f)) l
theorem
finsupp.span_eq_map_total
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{v : α → M}
(s : set α) :
submodule.span R (v '' s) = submodule.map (finsupp.total α M R v) (finsupp.supported R R s)
theorem
finsupp.mem_span_iff_total
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{v : α → M}
{s : set α}
{x : M} :
x ∈ submodule.span R (v '' s) ↔ ∃ (l : α →₀ R) (H : l ∈ finsupp.supported R R s), ⇑(finsupp.total α M R v) l = x
def
finsupp.total_on
(α : Type u_1)
(M : Type u_2)
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
(v : α → M)
(s : set α) :
↥(finsupp.supported R R s) →ₗ[R] ↥(submodule.span R (v '' s))
Equations
- finsupp.total_on α M R v s = linear_map.cod_restrict (submodule.span R (v '' s)) ((finsupp.total α M R v).comp (finsupp.supported R R s).subtype) _
theorem
finsupp.total_on_range
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{v : α → M}
(s : set α) :
(finsupp.total_on α M R v s).range = ⊤
theorem
finsupp.total_comp
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{α' : Type u_5}
{v : α → M}
(f : α' → α) :
finsupp.total α' M R (v ∘ f) = (finsupp.total α M R v).comp (finsupp.lmap_domain R R f)
theorem
finsupp.total_comap_domain
{α : Type u_1}
{M : Type u_2}
(R : Type u_4)
[ring R]
[add_comm_group M]
[module R M]
{α' : Type u_5}
{v : α → M}
(f : α → α')
(l : α' →₀ R)
(hf : set.inj_on f (f ⁻¹' ↑(l.support))) :
⇑(finsupp.total α M R v) (finsupp.comap_domain f l hf) = (l.support.preimage f hf).sum (λ (i : α), ⇑l (f i) • v i)
def
finsupp.dom_lcongr
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
{α₁ : Type u_1}
{α₂ : Type u_3} :
An equivalence of domains induces a linear equivalence of finitely supported functions.
Equations
@[simp]
theorem
finsupp.dom_lcongr_single
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
{α₁ : Type u_1}
{α₂ : Type u_3}
(e : α₁ ≃ α₂)
(i : α₁)
(m : M) :
⇑(finsupp.dom_lcongr e) (finsupp.single i m) = finsupp.single (⇑e i) m
def
finsupp.congr
{α : Type u_1}
{M : Type u_2}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
{α' : Type u_3}
(s : set α)
(t : set α') :
↥s ≃ ↥t → (↥(finsupp.supported M R s) ≃ₗ[R] ↥(finsupp.supported M R t))
Equations
- finsupp.congr s t e = (finsupp.supported_equiv_finsupp s).trans ((finsupp.dom_lcongr e).trans (finsupp.supported_equiv_finsupp t).symm)
def
finsupp.lcongr
{M : Type u_2}
{N : Type u_3}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
{ι : Type u_1}
{κ : Type u_5} :
An equivalence of domain and a linear equivalence of codomain induce a linear equivalence of the corresponding finitely supported functions.
Equations
- finsupp.lcongr e₁ e₂ = (finsupp.dom_lcongr e₁).trans {to_fun := finsupp.map_range ⇑e₂ _, map_add' := _, map_smul' := _, inv_fun := finsupp.map_range ⇑(e₂.symm) _, left_inv := _, right_inv := _}
@[simp]
theorem
finsupp.lcongr_single
{M : Type u_2}
{N : Type u_3}
{R : Type u_4}
[ring R]
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
{ι : Type u_1}
{κ : Type u_5}
(e₁ : ι ≃ κ)
(e₂ : M ≃ₗ[R] N)
(i : ι)
(m : M) :
⇑(finsupp.lcongr e₁ e₂) (finsupp.single i m) = finsupp.single (⇑e₁ i) (⇑e₂ m)
theorem
linear_map.map_finsupp_total
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[ring R]
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(f : M →ₗ[R] N)
{ι : Type u_4}
{g : ι → M}
(l : ι →₀ R) :
⇑f (⇑(finsupp.total ι M R g) l) = ⇑(finsupp.total ι N R (⇑f ∘ g)) l
theorem
submodule.exists_finset_of_mem_supr
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{ι : Type u_3}
(p : ι → submodule R M)
{m : M} :