Properties of the semimodule α →₀ M #
Given an R-semimodule M, the R-semimodule structure on α →₀ M is defined in
data.finsupp.basic.
In this file we define finsupp.supported s to be the set {f : α →₀ M | f.support ⊆ s}
interpreted as a submodule of α →₀ M. We also define linear_map versions of various maps:
-
finsupp.lsingle a : M →ₗ[R] ι →₀ M:finsupp.single aas a linear map; -
finsupp.lapply a : (ι →₀ M) →ₗ[R] M: the mapλ f, f aas a linear map; -
finsupp.lsubtype_domain (s : set α) : (α →₀ M) →ₗ[R] (s →₀ M): restriction to a subtype as a linear map; -
finsupp.restrict_dom:finsupp.filteras a linear map tofinsupp.supported s; -
finsupp.lsum:finsupp.sumorfinsupp.lift_add_homas alinear_map; -
finsupp.total α M R (v : ι → M): sendsl : ι → Rto the linear combination ofv iwith coefficientsl i; -
finsupp.total_on: a restricted version offinsupp.totalwith domainfinsupp.supported R R sand codomainsubmodule.span R (v '' s); -
finsupp.supported_equiv_finsupp: a linear equivalence between the functionsα →₀ Msupported onsand the functionss →₀ M; -
finsupp.lmap_domain: a linear map version offinsupp.map_domain; -
finsupp.dom_lcongr: alinear_equivversion offinsupp.dom_congr; -
finsupp.congr: if the setssandtare equivalent, thensupported M R sis equivalent tosupported M R t; -
finsupp.lcongr: alinear_equivalence betweenα →₀ Mandβ →₀ Nconstructed usinge : α ≃ βande' : M ≃ₗ[R] N.
Tags #
function with finite support, semimodule, linear algebra
def
finsupp.lsingle
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(a : α) :
Interpret finsupp.single a as a linear map.
Equations
- finsupp.lsingle a = {to_fun := (finsupp.single_add_hom a).to_fun, map_add' := _, map_smul' := _}
theorem
finsupp.lhom_ext
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
⦃φ ψ : (α →₀ M) →ₗ[R] N⦄
(h : ∀ (a : α) (b : M), ⇑φ (finsupp.single a b) = ⇑ψ (finsupp.single a b)) :
φ = ψ
Two R-linear maps from finsupp X M which agree on each single x y agree everywhere.
@[ext]
theorem
finsupp.lhom_ext'
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
⦃φ ψ : (α →₀ M) →ₗ[R] N⦄
(h : ∀ (a : α), φ.comp (finsupp.lsingle a) = ψ.comp (finsupp.lsingle a)) :
φ = ψ
Two R-linear maps from finsupp X M which agree on each single x y agree everywhere.
We formulate this fact using equality of linear maps φ.comp (lsingle a) and ψ.comp (lsingle a)
so that the ext tactic can apply a type-specific extensionality lemma to prove equality of these
maps. E.g., if M = R, then it suffices to verify φ (single a 1) = ψ (single a 1).
def
finsupp.lapply
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(a : α) :
Interpret λ (f : α →₀ M), f a as a linear map.
Equations
- finsupp.lapply a = {to_fun := (finsupp.apply_add_hom a).to_fun, map_add' := _, map_smul' := _}
def
finsupp.lsubtype_domain
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(s : set α) :
Interpret finsupp.subtype_domain s as a linear map.
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_5}
[semiring R]
[add_comm_monoid M]
[semimodule 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(a : α) :
(finsupp.lsingle a).ker = ⊥
theorem
finsupp.lsingle_range_le_ker_lapply
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(s t : set α)
(h : 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
(⨅ (a : α), (finsupp.lapply a).ker) ≤ ⊥
theorem
finsupp.supr_lsingle_range
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
(⨆ (a : α), (finsupp.lsingle a).range) = ⊤
theorem
finsupp.disjoint_lsingle_lsingle
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(s t : set α)
(hs : 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(s : set M)
(a : α) :
submodule.span R (finsupp.single a '' s) = submodule.map (finsupp.lsingle a) (submodule.span R s)
def
finsupp.supported
{α : Type u_1}
(M : Type u_2)
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(s : set α) :
finsupp.supported M R s is the R-submodule of all p : α →₀ M such that p.support ⊆ s.
theorem
finsupp.mem_supported
{α : Type u_1}
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s : set α}
(p : α →₀ M) :
theorem
finsupp.mem_supported'
{α : Type u_1}
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s : set α}
(p : α →₀ M) :
theorem
finsupp.single_mem_supported
{α : Type u_1}
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s : set α}
{a : α}
(b : M)
(h : a ∈ s) :
finsupp.single a b ∈ finsupp.supported M R s
theorem
finsupp.supported_eq_span_single
{α : Type u_1}
(R : Type u_5)
[semiring 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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(s : set α) :
(α →₀ M) →ₗ[R] ↥(finsupp.supported M R s)
Interpret finsupp.filter s as a linear map from α →₀ M to 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s t : set α}
(st : 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
finsupp.supported M R ∅ = ⊥
@[simp]
theorem
finsupp.supported_univ
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
finsupp.supported M R set.univ = ⊤
theorem
finsupp.supported_Union
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{ι : Type u_3}
(s : ι → set α) :
finsupp.supported M R (⋂ (i : ι), s i) = ⨅ (i : ι), finsupp.supported M R (s i)
theorem
finsupp.supported_inter
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(s t : set α) :
finsupp.supported M R (s ∩ t) = finsupp.supported M R s ⊓ finsupp.supported M R t
theorem
finsupp.disjoint_supported_supported
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s t : set α}
(h : disjoint s t) :
disjoint (finsupp.supported M R s) (finsupp.supported M R t)
theorem
finsupp.disjoint_supported_supported_iff
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[nontrivial M]
{s t : set α} :
disjoint (finsupp.supported M R s) (finsupp.supported M R t) ↔ disjoint s t
def
finsupp.supported_equiv_finsupp
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(s : set α) :
Interpret finsupp.restrict_support_equiv as a linear equivalence between
supported M R s and s →₀ M.
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_5}
(S : Type u_6)
[semiring R]
[semiring S]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
[semimodule S N]
[smul_comm_class R S N] :
Lift a family of linear maps M →ₗ[R] N indexed by x : α to a linear map from α →₀ M to
N using finsupp.sum. This is an upgraded version of finsupp.lift_add_hom.
See note [bundled maps over different rings] for why separate R and S semirings are used.
@[simp]
theorem
finsupp.coe_lsum
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
(S : Type u_6)
[semiring R]
[semiring S]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
[semimodule S N]
[smul_comm_class R S N]
(f : α → (M →ₗ[R] N)) :
theorem
finsupp.lsum_apply
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
(S : Type u_6)
[semiring R]
[semiring S]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
[semimodule S N]
[smul_comm_class R S N]
(f : α → (M →ₗ[R] N))
(l : α →₀ M) :
theorem
finsupp.lsum_single
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
(S : Type u_6)
[semiring R]
[semiring S]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
[semimodule S N]
[smul_comm_class R S N]
(f : α → (M →ₗ[R] N))
(i : α)
(m : M) :
⇑(⇑(finsupp.lsum S) f) (finsupp.single i m) = ⇑(f i) m
theorem
finsupp.lsum_symm_apply
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
(S : Type u_6)
[semiring R]
[semiring S]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
[semimodule S N]
[smul_comm_class R S N]
(f : (α →₀ M) →ₗ[R] N)
(x : α) :
⇑((finsupp.lsum S).symm) f x = f.comp (finsupp.lsingle x)
def
finsupp.lift
(M : Type u_2)
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(X : Type u_7) :
A slight rearrangement from lsum gives us
the bijection underlying the free-forgetful adjunction for R-modules.
Equations
- finsupp.lift M R X = (add_equiv.arrow_congr (equiv.refl X) (linear_map.ring_lmap_equiv_self R M ℕ).to_add_equiv.symm).trans (finsupp.lsum ℕ).to_add_equiv
@[simp]
theorem
finsupp.lift_symm_apply
(M : Type u_2)
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(X : Type u_7)
(f : (X →₀ R) →ₗ[R] M)
(x : X) :
⇑((finsupp.lift M R X).symm) f x = ⇑f (finsupp.single x 1)
@[simp]
theorem
finsupp.lift_apply
(M : Type u_2)
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(X : Type u_7)
(f : X → M)
(g : X →₀ R) :
def
finsupp.lmap_domain
{α : Type u_1}
(M : Type u_2)
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α' : Type u_7}
(f : α → α') :
Interpret finsupp.map_domain as a linear map.
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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α' : Type u_7}
(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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
theorem
finsupp.lmap_domain_comp
{α : Type u_1}
(M : Type u_2)
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α' : Type u_7}
{α'' : Type u_8}
(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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α' : Type u_7}
(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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α' : Type u_7}
[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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α' : Type u_7}
(f : α → α')
{s : set α}
(H : ∀ (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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(v : α → 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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{v : α → M}
(l : α →₀ R) :
⇑(finsupp.total α M R v) l = l.sum (λ (i : α) (a : R), a • v i)
theorem
finsupp.total_apply_of_mem_supported
{α : Type u_1}
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{v : α → M}
{l : α →₀ R}
{s : finset α}
(hs : l ∈ finsupp.supported R R ↑s) :
⇑(finsupp.total α M R v) l = ∑ (i : α) in s, ⇑l i • v i
@[simp]
theorem
finsupp.total_single
{α : Type u_1}
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{v : α → M}
(c : R)
(a : α) :
⇑(finsupp.total α M R v) (finsupp.single a c) = c • v a
theorem
finsupp.total_unique
{α : Type u_1}
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[unique α]
(l : α →₀ R)
(v : α → M) :
theorem
finsupp.total_range
{α : Type u_1}
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{v : α → M}
(h : function.surjective v) :
(finsupp.total α M R v).range = ⊤
theorem
finsupp.range_total
{α : Type u_1}
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule 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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α' : Type u_7}
{M' : Type u_8}
[add_comm_monoid M']
[semimodule R M']
{v : α → M}
{v' : α' → M'}
(f : α → α')
(g : M →ₗ[R] M')
(h : ∀ (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_5)
[semiring R]
{α' : Type u_7}
{M' : Type u_8}
[add_comm_monoid M']
[semimodule 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_5)
[semiring R]
{α' : Type u_7}
{M' : Type u_8}
[add_comm_monoid M']
[semimodule 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_5)
[semiring R]
[add_comm_monoid M]
[semimodule 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_5)
[semiring R]
[add_comm_monoid M]
[semimodule 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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(v : α → M)
(s : set α) :
↥(finsupp.supported R R s) →ₗ[R] ↥(submodule.span R (v '' s))
finsupp.total_on M v s interprets p : α →₀ R as a linear combination of a
subset of the vectors in v, mapping it to the span of those vectors.
The subset is indicated by a set s : set α of indices.
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_5)
[semiring R]
[add_comm_monoid M]
[semimodule 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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α' : Type u_7}
{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_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α' : Type u_7}
{v : α → M}
(f : α → α')
(l : α' →₀ R)
(hf : set.inj_on f (f ⁻¹' ↑(l.support))) :
⇑(finsupp.total α M R v) (finsupp.comap_domain f l hf) = ∑ (i : α) in l.support.preimage f hf, ⇑l (f i) • v i
theorem
finsupp.total_on_finset
{α : Type u_1}
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s : finset α}
{f : α → R}
(g : α → M)
(hf : ∀ (a : α), f a ≠ 0 → a ∈ s) :
⇑(finsupp.total α M R g) (finsupp.on_finset s f hf) = ∑ (x : α) in s, f x • g x
def
finsupp.dom_lcongr
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α₁ : Type u_1}
{α₂ : Type u_3}
(e : α₁ ≃ α₂) :
An equivalence of domains induces a linear equivalence of finitely supported functions.
This is finsupp.dom_congr as a linear_equiv.
Equations
@[simp]
theorem
finsupp.dom_lcongr_refl
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
finsupp.dom_lcongr (equiv.refl α) = linear_equiv.refl R (α →₀ M)
theorem
finsupp.dom_lcongr_trans
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α₁ : Type u_1}
{α₂ : Type u_3}
{α₃ : Type u_4}
(f : α₁ ≃ α₂)
(f₂ : α₂ ≃ α₃) :
(finsupp.dom_lcongr f).trans (finsupp.dom_lcongr f₂) = finsupp.dom_lcongr (f.trans f₂)
@[simp]
theorem
finsupp.dom_lcongr_symm
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α₁ : Type u_1}
{α₂ : Type u_3}
(f : α₁ ≃ α₂) :
@[simp]
theorem
finsupp.dom_lcongr_single
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule 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_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α' : Type u_3}
(s : set α)
(t : set α')
(e : ↥s ≃ ↥t) :
↥(finsupp.supported M R s) ≃ₗ[R] ↥(finsupp.supported M R t)
An equivalence of sets induces a linear equivalence of finsupps supported on those sets.
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.map_range.linear_map
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
(f : M →ₗ[R] N) :
finsupp.map_range as a linear_map.
Equations
- finsupp.map_range.linear_map f = {to_fun := finsupp.map_range ⇑f _, map_add' := _, map_smul' := _}
@[simp]
theorem
finsupp.map_range.linear_map_apply
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
(f : M →ₗ[R] N)
(g : α →₀ M) :
⇑(finsupp.map_range.linear_map f) g = finsupp.map_range ⇑f _ g
@[simp]
theorem
finsupp.map_range.linear_map_id
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
theorem
finsupp.map_range.linear_map_comp
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
[add_comm_monoid P]
[semimodule R P]
(f : N →ₗ[R] P)
(f₂ : M →ₗ[R] N) :
def
finsupp.map_range.linear_equiv
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
(e : M ≃ₗ[R] N) :
finsupp.map_range as a linear_equiv.
Equations
- finsupp.map_range.linear_equiv e = {to_fun := finsupp.map_range ⇑e _, map_add' := _, map_smul' := _, inv_fun := finsupp.map_range ⇑(e.symm) _, left_inv := _, right_inv := _}
@[simp]
theorem
finsupp.map_range.linear_equiv_apply
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
(e : M ≃ₗ[R] N)
(g : α →₀ M) :
⇑(finsupp.map_range.linear_equiv e) g = finsupp.map_range ⇑e _ g
@[simp]
theorem
finsupp.map_range.linear_equiv_refl
{α : Type u_1}
{M : Type u_2}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
finsupp.map_range.linear_equiv (linear_equiv.refl R M) = linear_equiv.refl R (α →₀ M)
theorem
finsupp.map_range.linear_equiv_trans
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
[add_comm_monoid P]
[semimodule R P]
(f : M ≃ₗ[R] N)
(f₂ : N ≃ₗ[R] P) :
@[simp]
theorem
finsupp.map_range.linear_equiv_symm
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
(f : M ≃ₗ[R] N) :
def
finsupp.lcongr
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
{ι : Type u_1}
{κ : Type u_4}
(e₁ : ι ≃ κ)
(e₂ : M ≃ₗ[R] N) :
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 (finsupp.map_range.linear_equiv e₂)
@[simp]
theorem
finsupp.lcongr_single
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
{ι : Type u_1}
{κ : Type u_4}
(e₁ : ι ≃ κ)
(e₂ : M ≃ₗ[R] N)
(i : ι)
(m : M) :
⇑(finsupp.lcongr e₁ e₂) (finsupp.single i m) = finsupp.single (⇑e₁ i) (⇑e₂ m)
@[simp]
theorem
finsupp.lcongr_apply_apply
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
{ι : Type u_1}
{κ : Type u_4}
(e₁ : ι ≃ κ)
(e₂ : M ≃ₗ[R] N)
(f : ι →₀ M)
(k : κ) :
theorem
finsupp.lcongr_symm_single
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
{ι : Type u_1}
{κ : Type u_4}
(e₁ : ι ≃ κ)
(e₂ : M ≃ₗ[R] N)
(k : κ)
(n : N) :
⇑((finsupp.lcongr e₁ e₂).symm) (finsupp.single k n) = finsupp.single (⇑(e₁.symm) k) (⇑(e₂.symm) n)
@[simp]
theorem
finsupp.lcongr_symm
{M : Type u_2}
{N : Type u_3}
{R : Type u_5}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule R N]
{ι : Type u_1}
{κ : Type u_4}
(e₁ : ι ≃ κ)
(e₂ : M ≃ₗ[R] N) :
(finsupp.lcongr e₁ e₂).symm = finsupp.lcongr e₁.symm e₂.symm
def
finsupp.sum_finsupp_lequiv_prod_finsupp
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α : Type u_1}
{β : Type u_3} :
The linear equivalence between (α ⊕ β) →₀ M and (α →₀ M) × (β →₀ M).
This is the linear_equiv version of finsupp.sum_finsupp_equiv_prod_finsupp.
Equations
@[simp]
theorem
finsupp.sum_finsupp_lequiv_prod_finsupp_apply
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α : Type u_1}
{β : Type u_3}
(ᾰ : α ⊕ β →₀ M) :
@[simp]
theorem
finsupp.sum_finsupp_lequiv_prod_finsupp_symm_apply
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α : Type u_1}
{β : Type u_3}
(ᾰ : (α →₀ M) × (β →₀ M)) :
theorem
finsupp.fst_sum_finsupp_lequiv_prod_finsupp
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α : Type u_1}
{β : Type u_3}
(f : α ⊕ β →₀ M)
(x : α) :
theorem
finsupp.snd_sum_finsupp_lequiv_prod_finsupp
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α : Type u_1}
{β : Type u_3}
(f : α ⊕ β →₀ M)
(y : β) :
theorem
finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inl
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α : Type u_1}
{β : Type u_3}
(fg : (α →₀ M) × (β →₀ M))
(x : α) :
theorem
finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inr
{M : Type u_2}
(R : Type u_5)
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{α : Type u_1}
{β : Type u_3}
(fg : (α →₀ M) × (β →₀ M))
(y : β) :
theorem
linear_map.map_finsupp_total
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
[add_comm_monoid N]
[semimodule 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}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{ι : Type u_3}
(p : ι → submodule R M)
{m : M}
(hm : m ∈ ⨆ (i : ι), p i) :
theorem
mem_span_finset
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{s : finset M}
{x : M} :
theorem
mem_span_set
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
{m : M}
{s : set M} :
An element m ∈ M is contained in the R-submodule spanned by a set s ⊆ M, if and only if
m can be written as a finite R-linear combination of elements of s.
The implementation uses finsupp.sum.