Finsupps 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

def Finsupp.supported {α : Type u_1} (M : Type u_2) (R : Type u_3) [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' := ⋯ }

theorem Finsupp.mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} (p : α →₀ M) : p ∈ supported M R s ↔ ↑p.support ⊆ s

theorem Finsupp.mem_supported' {α : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} (p : α →₀ M) : p ∈ supported M R s ↔ ∀ x ∉ s, p x = 0

theorem Finsupp.mem_supported_support {α : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] (p : α →₀ M) : p ∈ supported M R ↑p.support

theorem Finsupp.single_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {a : α} (b : M) (h : a ∈ s) : single a b ∈ supported M R s

theorem Finsupp.supported_eq_span_single {α : Type u_1} (R : Type u_3) [Semiring R] (s : Set α) : supported R R s = Submodule.span R ((fun (i : α) => single i 1) '' s)

theorem Finsupp.single_mem_span_single {α : Type u_1} (R : Type u_3) [Semiring R] [Nontrivial R] {a : α} {s : Set α} : single a 1 ∈ Submodule.span R ((fun (x : α) => single x 1) '' s) ↔ a ∈ s

theorem Finsupp.span_le_supported_biUnion_support {α : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set (α →₀ M)) : Submodule.span R s ≤ supported M R (⋃ x ∈ s, ↑x.support)

noncomputable def Finsupp.restrictDom {α : Type u_1} (M : Type u_2) (R : Type u_3) [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' := ⋯ } ⋯

@[simp]

theorem Finsupp.restrictDom_apply {α : Type u_1} {M : Type u_2} {R : Type u_3} [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

theorem Finsupp.restrictDom_comp_subtype {α : Type u_1} {M : Type u_2} {R : Type u_3} [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

theorem Finsupp.range_restrictDom {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : (restrictDom M R s).range = ⊤

theorem Finsupp.supported_mono {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set α} (st : s ⊆ t) : supported M R s ≤ supported M R t

@[simp]

theorem Finsupp.supported_empty {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : supported M R ∅ = ⊥

@[simp]

theorem Finsupp.supported_univ {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : supported M R Set.univ = ⊤

theorem Finsupp.supported_iUnion {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {δ : Type u_4} (s : δ → Set α) : supported M R (⋃ (i : δ), s i) = ⨆ (i : δ), supported M R (s i)

theorem Finsupp.supported_union {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Set α) : supported M R (s ∪ t) = supported M R s ⊔ supported M R t

theorem Finsupp.supported_iInter {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} (s : ι → Set α) : supported M R (⋂ (i : ι), s i) = ⨅ (i : ι), supported M R (s i)

theorem Finsupp.supported_inter {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Set α) : supported M R (s ∩ t) = supported M R s ⊓ supported M R t

theorem Finsupp.disjoint_supported_supported {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set α} (h : Disjoint s t) : Disjoint (supported M R s) (supported M R t)

theorem Finsupp.disjoint_supported_supported_iff {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] {s t : Set α} : Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t

theorem Finsupp.codisjoint_supported_supported {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set α} (h : Codisjoint s t) : Codisjoint (supported M R s) (supported M R t)

theorem Finsupp.codisjoint_supported_supported_iff {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] {s t : Set α} : Codisjoint (supported M R s) (supported M R t) ↔ Codisjoint s t

noncomputable def Finsupp.supportedEquivFinsupp {α : Type u_1} {M : Type u_2} {R : Type u_3} [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 ⋯

@[simp]

theorem Finsupp.supportedEquivFinsupp_symm_apply_coe_apply {α : Type u_1} {M : Type u_2} {R : Type u_3} [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

@[simp]

theorem Finsupp.supportedEquivFinsupp_apply_support_val {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (a✝ : ↥(supported M R s)) : ((supportedEquivFinsupp s) a✝).support.val = Multiset.map (fun (x : ↥({x ∈ (↑a✝).support | x ∈ s})) => ⟨↑x, ⋯⟩) (Multiset.filter (fun (x : α) => x ∈ s) (↑a✝).support.val).attach

@[simp]

theorem Finsupp.supportedEquivFinsupp_apply_apply {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (a✝ : ↥(supported M R s)) (a✝¹ : { x : α // x ∈ s }) : ((supportedEquivFinsupp s) a✝) a✝¹ = ↑a✝ ↑a✝¹

@[simp]

theorem Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val {α : Type u_1} {M : Type u_2} {R : Type u_3} [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

@[simp]

theorem Finsupp.supportedEquivFinsupp_symm_apply_coe {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (f : ↑s →₀ M) : ↑((supportedEquivFinsupp s).symm f) = f.extendDomain

@[simp]

theorem Finsupp.supportedEquivFinsupp_symm_single {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (i : ↑s) (a : M) : ↑((supportedEquivFinsupp s).symm (single i a)) = single (↑i) a

theorem Finsupp.supported_comap_lmapDomain {α : Type u_1} (M : Type u_2) (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_4} (f : α → α') (s : Set α') : supported M R (f ⁻¹' s) ≤ Submodule.comap (lmapDomain M R f) (supported M R s)

theorem Finsupp.lmapDomain_supported {α : Type u_1} (M : Type u_2) (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_4} (f : α → α') (s : Set α) : Submodule.map (lmapDomain M R f) (supported M R s) = supported M R (f '' s)

theorem Finsupp.lmapDomain_disjoint_ker {α : Type u_1} (M : Type u_2) (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_4} (f : α → α') {s : Set α} (H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b) : Disjoint (supported M R s) (lmapDomain M R f).ker

noncomputable def Finsupp.congr {α : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_4} (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 Finsupps supported on those sets.

Equations

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