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_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' := ⋯ }

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 ∈ Finsupp.supported M R s ↔ ↑p.support ⊆ s

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 ∈ Finsupp.supported M R s ↔ ∀ x ∉ s, p x = 0

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 ∈ Finsupp.supported M R ↑p.support

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) : 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 ((fun (i : α) => Finsupp.single i 1) '' s)

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] ↥(Finsupp.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_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (l : α →₀ M) [DecidablePred fun (x : α) => x ∈ s] : ↑((Finsupp.restrictDom M R s) l) = Finsupp.filter (fun (x : α) => x ∈ s) l

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] : Finsupp.restrictDom M R s ∘ₗ (Finsupp.supported M R s).subtype = LinearMap.id

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 (Finsupp.restrictDom M R s) = ⊤

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) : 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] [AddCommMonoid M] [Module R M] : Finsupp.supported M R ∅ = ⊥

@[simp]

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

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 α) : 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] [AddCommMonoid M] [Module R M] (s t : Set α) : Finsupp.supported M R (s ∪ t) = Finsupp.supported M R s ⊔ Finsupp.supported M R t

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 α) : 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] [AddCommMonoid M] [Module 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] [AddCommMonoid M] [Module 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] [AddCommMonoid M] [Module R M] [Nontrivial M] {s t : Set α} : Disjoint (Finsupp.supported M R s) (Finsupp.supported M R t) ↔ Disjoint s t

def Finsupp.supportedEquivFinsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) : ↥(Finsupp.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 ⋯

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 α') : Finsupp.supported M R (f ⁻¹' s) ≤ Submodule.comap (Finsupp.lmapDomain M R f) (Finsupp.supported M R s)

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 (Finsupp.lmapDomain M R f) (Finsupp.supported M R s) = Finsupp.supported M R (f '' s)

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 (Finsupp.supported M R s) (LinearMap.ker (Finsupp.lmapDomain M R f))

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) : ↥(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.supportedEquivFinsupp s ≪≫ₗ (Finsupp.domLCongr e ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm)