Documentation

TauCeti.LinearAlgebra.Finsupp.Supported

Filtering finitely supported functions supported on a set #

Keeping the values of a finitely supported function f at the points satisfying a predicate p (Finsupp.filter p f) sends functions supported on s to functions supported on t, as soon as every point of s satisfying p lies in t. This file packages this operation as a linear map between the submodules Finsupp.supported M R s and Finsupp.supported M R t; Mathlib's Finsupp.restrictDom is the case of the predicate (· ∈ t) on the whole space.

A linear map from a finitely generated module into α →₀ M takes values in the functions supported on one finite set (LinearMap.exists_finset_support_subset).

A finitely generated submodule of ℕ →₀ M consists of functions supported on an initial segment {i | i < n}, since its finitely many generators have finite supports.

Main definitions #

Main results #

source
noncomputable def TauCeti.Finsupp.filterSupported {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set α} (p : α → Prop) [DecidablePred p] (h : ∀ a ∈ s, p a → a ∈ t) :
↥(Finsupp.supported M R s) →ₗ[R] ↥(Finsupp.supported M R t)

Finsupp.filter p as a linear map from the functions supported on s to the functions supported on t, where every point of s satisfying p lies in t.

Instances For
    source
    @[simp]
    theorem TauCeti.Finsupp.filterSupported_apply {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set α} (p : α → Prop) [DecidablePred p] (h : ∀ a ∈ s, p a → a ∈ t) (f : ↥(Finsupp.supported M R s)) :
    ↑((filterSupported p h) f) = Finsupp.filter p ↑f

    TauCeti.Finsupp.filterSupported p h filters the underlying finitely supported function.

    source
    theorem TauCeti.Finsupp.filterSupported_comp_inclusion {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s s' t : Set α} (p : α → Prop) [DecidablePred p] (hs : s ⊆ s') (h : ∀ a ∈ s', p a → a ∈ t) :
    filterSupported p h ∘ₗ Submodule.inclusion ⋯ = filterSupported p ⋯

    Filtering a function supported on s after viewing it as supported on a larger set s' is filtering it directly.

    source
    theorem TauCeti.Finsupp.inclusion_comp_filterSupported {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s t t' : Set α} (p : α → Prop) [DecidablePred p] (h : ∀ a ∈ s, p a → a ∈ t) (ht : t ⊆ t') :
    Submodule.inclusion ⋯ ∘ₗ filterSupported p h = filterSupported p ⋯

    Viewing the filter of a function as supported on a larger set t' is filtering it with target t' directly.

    source
    theorem LinearMap.exists_finset_support_subset {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module.Finite R N] (f : N →ₗ[R] α →₀ M) :
    ∃ (T : Finset α), ∀ (y : N), (f y).support ⊆ T

    A finitely generated module maps into finitely many coordinates: the values of a linear map from a finitely generated module into α →₀ M are all supported on one finite set, the union of the supports of the images of finitely many generators (Mathlib's Finsupp.span_le_supported_biUnion_support).

    source
    theorem Submodule.FG.exists_le_supported_Iio {M : Type u_1} {R : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {V : Submodule R (ℕ →₀ M)} (hV : V.FG) :
    ∃ (n : ℕ), V ≤ Finsupp.supported M R (Set.Iio n)

    A finitely generated submodule of ℕ →₀ M consists of functions vanishing from some coordinate on.

    source
    theorem Finsupp.sub_single_mem_supported {α : Type u_1} {M : Type u_3} (R : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] {s : Set α} (v : α →₀ M) (k : α) (hv : ∀ j ∈ v.support, j ∈ s ∨ j = k) :
    v - single k (v k) ∈ supported M R s

    Removing the value at an exceptional coordinate k leaves a function supported on s, if every other point of the support lies in s.

    source
    theorem Finsupp.map_mem_supported_of_forall_single_mem {α : Type u_1} {β : Type u_2} {M : Type u_3} {N : Type u_4} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {s : Set α} {t : Set β} (f : (α →₀ M) →ₗ[R] β →₀ N) (hf : ∀ j ∈ s, ∀ (x : M), f (single j x) ∈ supported N R t) {v : α →₀ M} (hv : v ∈ supported M R s) :
    f v ∈ supported N R t

    A linear map sending every basis vector single j x with j ∈ s into supported N R t maps supported M R s into supported N R t.