# `Finsupp`s supported on a given submodule #

- `Finsupp.restrictDom`: `Finsupp.filter` as a linear map to `Finsupp.supported s`; `Finsupp.supported R R s` and codomain `Submodule.span R (v '' s)`;
- `Finsupp.supportedEquivFinsupp`: a linear equivalence between the functions `α →₀ M` supported on `s` and the functions `s →₀ M`;
- `Finsupp.domLCongr`: a `LinearEquiv` version of `Finsupp.domCongr`;
- `Finsupp.congr`: if the sets `s` and `t` are equivalent, then `supported M R s` is equivalent to `supported M R t`;

## Tags #

function with finite support, module, linear algebra

source
def Finsupp.supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) :
Submodule R (α →₀ M)

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

Equations

- Finsupp.supported M R s = { carrier := {p : α →₀ M | ↑p.support ⊆ s}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source
theorem Finsupp.mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} (p : α →₀ M) :
p ∈ supported M R s ↔ ↑p.support ⊆ s
source
theorem Finsupp.mem_supported' {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} (p : α →₀ M) :
p ∈ supported M R s ↔ ∀ x ∉ s, p x = 0
source
theorem Finsupp.mem_supported_support {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (p : α →₀ M) :
p ∈ supported M R ↑p.support
source
theorem Finsupp.single_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {a : α} (b : M) (h : a ∈ s) :
single a b ∈ supported M R s
source
theorem Finsupp.supported_eq_span_single {α : Type u_1} (R : Type u_5) [Semiring R] (s : Set α) :
supported R R s = Submodule.span R ((fun (i : α) => single i 1) '' s)
source
theorem Finsupp.span_le_supported_biUnion_support {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set (α →₀ M)) :
Submodule.span R s ≤ supported M R (⋃ x ∈ s, ↑x.support)
source
def Finsupp.restrictDom {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] :
(α →₀ M) →ₗ[R] ↥(supported M R s)

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

Equations

- Finsupp.restrictDom M R s = LinearMap.codRestrict (Finsupp.supported M R s) { toFun := Finsupp.filter fun (x : α) => x ∈ s, map_add' := ⋯, map_smul' := ⋯ } ⋯

Instances For

source
@[simp]
theorem Finsupp.restrictDom_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (l : α →₀ M) [DecidablePred fun (x : α) => x ∈ s] :
↑((restrictDom M R s) l) = filter (fun (x : α) => x ∈ s) l
source
theorem Finsupp.restrictDom_comp_subtype {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] :
restrictDom M R s ∘ₗ (supported M R s).subtype = LinearMap.id
source
theorem Finsupp.range_restrictDom {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] :
LinearMap.range (restrictDom M R s) = ⊤
source
theorem Finsupp.supported_mono {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set α} (st : s ⊆ t) :
supported M R s ≤ supported M R t
source
@[simp]
theorem Finsupp.supported_empty {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
supported M R ∅ = ⊥
source
@[simp]
theorem Finsupp.supported_univ {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
supported M R Set.univ = ⊤
source
theorem Finsupp.supported_iUnion {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {δ : Type u_7} (s : δ → Set α) :
supported M R (⋃ (i : δ), s i) = ⨆ (i : δ), supported M R (s i)
source
theorem Finsupp.supported_union {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Set α) :
supported M R (s ∪ t) = supported M R s ⊔ supported M R t
source
theorem Finsupp.supported_iInter {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_7} (s : ι → Set α) :
supported M R (⋂ (i : ι), s i) = ⨅ (i : ι), supported M R (s i)
source
theorem Finsupp.supported_inter {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Set α) :
supported M R (s ∩ t) = supported M R s ⊓ supported M R t
source
theorem Finsupp.disjoint_supported_supported {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set α} (h : Disjoint s t) :
Disjoint (supported M R s) (supported M R t)
source
theorem Finsupp.disjoint_supported_supported_iff {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] {s t : Set α} :
Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t
source
theorem Finsupp.codisjoint_supported_supported {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set α} (h : Codisjoint s t) :
Codisjoint (supported M R s) (supported M R t)
source
theorem Finsupp.codisjoint_supported_supported_iff {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] {s t : Set α} :
Codisjoint (supported M R s) (supported M R t) ↔ Codisjoint s t
source
def Finsupp.supportedEquivFinsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) :
↥(supported M R s) ≃ₗ[R] ↑s →₀ M

Interpret `Finsupp.restrictSupportEquiv` as a linear equivalence between `supported M R s` and `s →₀ M`.

Equations

- Finsupp.supportedEquivFinsupp s = (Finsupp.restrictSupportEquiv s M).toLinearEquiv ⋯

Instances For

source
@[simp]
theorem Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (a✝ : ↑s →₀ M) :
(↑((supportedEquivFinsupp s).symm a✝)).support.val = Multiset.map Subtype.val a✝.support.val
source
@[simp]
theorem Finsupp.supportedEquivFinsupp_apply_support_val {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (a✝ : ↥(supported M R s)) :
((supportedEquivFinsupp s) a✝).support.val = Multiset.map (fun (x : { x : α // x ∈ {x ∈ (↑a✝).support | x ∈ s} }) => ⟨↑x, ⋯⟩) (Multiset.filter (fun (x : α) => x ∈ s) (↑a✝).support.val).attach
source
@[simp]
theorem Finsupp.supportedEquivFinsupp_symm_apply_coe_toFun {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (a✝ : ↑s →₀ M) (a : α) :
↑((supportedEquivFinsupp s).symm a✝) a = if h : a ∈ s then a✝ ⟨a, h⟩ else 0
source
@[simp]
theorem Finsupp.supportedEquivFinsupp_apply_toFun {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (a✝ : ↥(supported M R s)) (a✝¹ : { x : α // x ∈ s }) :
((supportedEquivFinsupp s) a✝) a✝¹ = ↑a✝ ↑a✝¹
source
@[simp]
theorem Finsupp.supportedEquivFinsupp_symm_apply_coe {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (f : ↑s →₀ M) :
↑((supportedEquivFinsupp s).symm f) = f.extendDomain
source
@[simp]
theorem Finsupp.supportedEquivFinsupp_symm_single {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (i : ↑s) (a : M) :
↑((supportedEquivFinsupp s).symm (single i a)) = single (↑i) a
source
theorem Finsupp.supported_comap_lmapDomain {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : α → α') (s : Set α') :
supported M R (f ⁻¹' s) ≤ Submodule.comap (lmapDomain M R f) (supported M R s)
source
theorem Finsupp.lmapDomain_supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : α → α') (s : Set α) :
Submodule.map (lmapDomain M R f) (supported M R s) = supported M R (f '' s)
source
theorem Finsupp.lmapDomain_disjoint_ker {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : α → α') {s : Set α} (H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b) :
Disjoint (supported M R s) (LinearMap.ker (lmapDomain M R f))
source
noncomputable def Finsupp.congr {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (s : Set α) (t : Set α') (e : ↑s ≃ ↑t) :
↥(supported M R s) ≃ₗ[R] ↥(supported M R t)

An equivalence of sets induces a linear equivalence of `Finsupp`s supported on those sets.

Equations

- Finsupp.congr s t e = Finsupp.supportedEquivFinsupp s ≪≫ₗ (Finsupp.domLCongr e ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm)

Instances For