mathlib documentation

linear_algebra.finsupp

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:

Tags

function with finite support, semimodule, linear algebra

def finsupp.lsingle {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] :
α → (M →ₗ[R] α →₀ M)

Interpret finsupp.single a as a linear map.

Equations
theorem finsupp.lhom_ext {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N] ⦃φ ψ : →₀ M) →ₗ[R] N⦄ :
(∀ (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_4} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N] ⦃φ ψ : →₀ M) →ₗ[R] N⦄ :
(∀ (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_4} [semiring R] [add_comm_monoid M] [semimodule R M] :
α → ((α →₀ M) →ₗ[R] M)

Interpret λ (f : α →₀ M), f a as a linear map.

Equations
def finsupp.lsubtype_domain {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] (s : set α) :

Interpret finsupp.subtype_domain s as a linear map.

Equations
theorem finsupp.lsubtype_domain_apply {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] (s : set α) (f : α →₀ M) :

@[simp]
theorem finsupp.lsingle_apply {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] (a : α) (b : M) :

@[simp]
theorem finsupp.lapply_apply {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] (a : α) (f : α →₀ M) :

@[simp]
theorem finsupp.ker_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] (a : α) :

theorem finsupp.lsingle_range_le_ker_lapply {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule 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} [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_4} [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_4} [semiring R] [add_comm_monoid M] [semimodule R M] (s t : set α) :
disjoint s tdisjoint (⨆ (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} [semiring R] [add_comm_monoid M] [semimodule R M] (s : set M) (a : α) :

def finsupp.supported {α : Type u_1} (M : Type u_2) (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] :
set αsubmodule R →₀ M)

finsupp.supported M R s is the R-submodule of all p : α →₀ M such that p.support ⊆ s.

Equations
theorem finsupp.mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_4) [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_4) [semiring R] [add_comm_monoid M] [semimodule R M] {s : set α} (p : α →₀ M) :
p finsupp.supported M R s ∀ (x : α), x sp x = 0

theorem finsupp.single_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] {s : set α} {a : α} (b : M) :

theorem finsupp.supported_eq_span_single {α : Type u_1} (R : Type u_4) [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_4) [semiring R] [add_comm_monoid M] [semimodule R M] (s : set α) :

Interpret finsupp.filter s as a linear map from α →₀ M to supported M R s.

Equations
@[simp]
theorem finsupp.restrict_dom_apply {α : Type u_1} {M : Type u_2} {R : Type u_4} [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_4} [semiring R] [add_comm_monoid M] [semimodule R M] (s : set α) :

theorem finsupp.range_restrict_dom {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] (s : set α) :

theorem finsupp.supported_mono {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] {s t : set α} :

@[simp]
theorem finsupp.supported_empty {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] :

@[simp]
theorem finsupp.supported_univ {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] :

theorem finsupp.supported_Union {α : Type u_1} {M : Type u_2} {R : Type u_4} [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_4} [semiring R] [add_comm_monoid M] [semimodule R M] (s t : set α) :

theorem finsupp.supported_Inter {α : Type u_1} {M : Type u_2} {R : Type u_4} [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_4} [semiring R] [add_comm_monoid M] [semimodule R M] (s t : set α) :

theorem finsupp.disjoint_supported_supported {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] {s t : set α} :

theorem finsupp.disjoint_supported_supported_iff {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] [nontrivial M] {s t : set α} :

def finsupp.supported_equiv_finsupp {α : Type u_1} {M : Type u_2} {R : Type u_4} [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
def finsupp.lsum {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N] :
(α → (M →ₗ[R] N)) ≃+ ((α →₀ M) →ₗ[R] 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. We define this as an additive equivalence. For a commutative R, this equivalence can be upgraded further to a linear equivalence.

Equations
@[simp]
theorem finsupp.coe_lsum {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N] (f : α → (M →ₗ[R] N)) :
(finsupp.lsum f) = λ (d : α →₀ M), d.sum (λ (i : α), (f i))

theorem finsupp.lsum_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule 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} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N] (f : α → (M →ₗ[R] N)) (i : α) (m : M) :

theorem finsupp.lsum_symm_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N] (f : →₀ M) →ₗ[R] N) (x : α) :

def finsupp.lmap_domain {α : Type u_1} (M : Type u_2) (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] {α' : Type u_5} :
(α → α')((α →₀ M) →ₗ[R] α' →₀ M)

Interpret finsupp.lmap_domain as a linear map.

Equations
@[simp]
theorem finsupp.lmap_domain_apply {α : Type u_1} (M : Type u_2) (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] {α' : Type u_5} (f : α → α') (l : α →₀ M) :

@[simp]
theorem finsupp.lmap_domain_id {α : Type u_1} (M : Type u_2) (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] :

theorem finsupp.lmap_domain_comp {α : Type u_1} (M : Type u_2) (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] {α' : Type u_5} {α'' : Type u_6} (f : α → α') (g : α' → α'') :

theorem finsupp.supported_comap_lmap_domain {α : Type u_1} (M : Type u_2) (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] {α' : Type u_5} (f : α → α') (s : set α') :

theorem finsupp.lmap_domain_supported {α : Type u_1} (M : Type u_2) (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] {α' : Type u_5} [nonempty α] (f : α → α') (s : set α) :

theorem finsupp.lmap_domain_disjoint_ker {α : Type u_1} (M : Type u_2) (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] {α' : Type u_5} (f : α → α') {s : set α} :
(∀ (a b : α), a sb sf a = f ba = 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) [semiring R] [add_comm_monoid M] [semimodule R M] :
(α → M)((α →₀ R) →ₗ[R] M)

Interprets (l : α →₀ R) as linear combination of the elements in the family (v : α → M) and evaluates this linear combination.

Equations
theorem finsupp.total_apply {α : Type u_1} {M : Type u_2} (R : Type u_4) [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_4) [semiring R] [add_comm_monoid M] [semimodule R M] {v : α → M} {l : α →₀ R} {s : finset α} :
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_4) [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_4) [semiring R] [add_comm_monoid M] [semimodule R M] [unique α] (l : α →₀ R) (v : α → M) :
(finsupp.total α M R v) l = l (default α) v (default α)

theorem finsupp.total_range {α : Type u_1} {M : Type u_2} (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] {v : α → M} :

theorem finsupp.range_total {α : Type u_1} {M : Type u_2} (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] {v : α → M} :

theorem finsupp.lmap_domain_total {α : Type u_1} {M : Type u_2} (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] {α' : Type u_5} {M' : Type u_6} [add_comm_monoid M'] [semimodule 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) [semiring R] {α' : Type u_5} {M' : Type u_6} [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_4) [semiring R] {α' : Type u_5} {M' : Type u_6} [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_4) [semiring R] [add_comm_monoid M] [semimodule R M] {v : α → M} (s : set α) :

theorem finsupp.mem_span_iff_total {α : Type u_1} {M : Type u_2} (R : Type u_4) [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_4) [semiring R] [add_comm_monoid M] [semimodule R M] (v : α → M) (s : set α) :

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
theorem finsupp.total_on_range {α : Type u_1} {M : Type u_2} (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule R M] {v : α → M} (s : set α) :

theorem finsupp.total_comp {α : Type u_1} {M : Type u_2} (R : Type u_4) [semiring R] [add_comm_monoid M] [semimodule 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) [semiring R] [add_comm_monoid M] [semimodule 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) = ∑ (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_4) [semiring R] [add_comm_monoid M] [semimodule R M] {s : finset α} {f : α → R} (g : α → M) (hf : ∀ (a : α), f a 0a 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_4} [semiring R] [add_comm_monoid M] [semimodule R M] {α₁ : Type u_1} {α₂ : Type u_3} :
α₁ α₂((α₁ →₀ M) ≃ₗ[R] α₂ →₀ M)

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} [semiring R] [add_comm_monoid M] [semimodule R M] {α₁ : Type u_1} {α₂ : Type u_3} (e : α₁ α₂) (i : α₁) (m : M) :

def finsupp.congr {α : Type u_1} {M : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] {α' : Type u_3} (s : set α) (t : set α') :

An equivalence of sets induces a linear equivalence of finsupps supported on those sets.

Equations
def finsupp.lcongr {M : Type u_2} {N : Type u_3} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N] {ι : Type u_1} {κ : Type u_5} :
ι κ(M ≃ₗ[R] N)((ι →₀ M) ≃ₗ[R] κ →₀ N)

An equivalence of domain and a linear equivalence of codomain induce a linear equivalence of the corresponding finitely supported functions.

Equations
@[simp]
theorem finsupp.lcongr_single {M : Type u_2} {N : Type u_3} {R : Type u_4} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule 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} [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} :
(m ⨆ (i : ι), p i)(∃ (s : finset ι), m ⨆ (i : ι) (H : i s), 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} :
x submodule.span R s ∃ (f : M → R), ∑ (i : M) in s, f i i = x