Mathlib.LinearAlgebra.Finsupp.Supported

Finsupp.supported definition

(s : Set α) : Submodule R (α →₀ M)

Full source

/-- `Finsupp.supported M R s` is the `R`-submodule of all `p : α →₀ M` such that `p.support ⊆ s`. -/
def supported (s : Set α) : Submodule R (α →₀ M) where
  carrier := { p | ↑p.support ⊆ s }
  add_mem' {p q} hp hq := by
    classical
    refine Subset.trans (Subset.trans (Finset.coe_subset.2 support_add) ?_) (union_subset hp hq)
    rw [Finset.coe_union]
  zero_mem' := by
    simp only [subset_def, Finset.mem_coe, Set.mem_setOf_eq, mem_support_iff, zero_apply]
    intro h ha
    exact (ha rfl).elim
  smul_mem' _ _ hp := Subset.trans (Finset.coe_subset.2 support_smul) hp

Submodule of finitely supported functions with support in $s$

Informal description

For a given set $s \subseteq \alpha$, the submodule `Finsupp.supported M R s` consists of all finitely supported functions $p : \alpha \to_{\text{f}} M$ whose support is contained in $s$. Here, the support of $p$ is the finite set of points where $p$ is nonzero.

Finsupp.mem_supported theorem

{s : Set α} (p : α →₀ M) : p ∈ supported M R s ↔ ↑p.support ⊆ s

Full source

theorem mem_supported {s : Set α} (p : α →₀ M) : p ∈ supported M R sp ∈ supported M R s ↔ ↑p.support ⊆ s :=
  Iff.rfl

Characterization of Finitely Supported Functions in Submodule by Support Condition

Informal description

Let $s$ be a subset of $\alpha$ and $p : \alpha \to_{\text{f}} M$ be a finitely supported function. Then $p$ belongs to the submodule $\text{supported}\, M\, R\, s$ if and only if the support of $p$ (as a set) is contained in $s$.

Finsupp.mem_supported' theorem

{s : Set α} (p : α →₀ M) : p ∈ supported M R s ↔ ∀ x ∉ s, p x = 0

Full source

theorem mem_supported' {s : Set α} (p : α →₀ M) :
    p ∈ supported M R sp ∈ supported M R s ↔ ∀ x ∉ s, p x = 0 := by
  haveI := Classical.decPred fun x : α => x ∈ s; simp [mem_supported, Set.subset_def, not_imp_comm]

Characterization of Finitely Supported Functions on a Subset $s$ via Vanishing Outside $s$

Informal description

Let $s$ be a subset of a type $\alpha$, and let $p : \alpha \to_{\text{f}} M$ be a finitely supported function from $\alpha$ to an additive commutative monoid $M$ with zero. Then $p$ belongs to the submodule of functions supported on $s$ if and only if for every $x \notin s$, the value $p(x) = 0$.

Finsupp.mem_supported_support theorem

(p : α →₀ M) : p ∈ Finsupp.supported M R (p.support : Set α)

Full source

theorem mem_supported_support (p : α →₀ M) : p ∈ Finsupp.supported M R (p.support : Set α) := by
  rw [Finsupp.mem_supported]

Membership of Finitely Supported Function in Submodule of Its Support

Informal description

For any finitely supported function $p \colon \alpha \to_{\text{f}} M$, the function $p$ belongs to the submodule of functions supported on its own support set $\text{supp}(p) \subseteq \alpha$.

Finsupp.single_mem_supported theorem

{s : Set α} {a : α} (b : M) (h : a ∈ s) : single a b ∈ supported M R s

Full source

theorem single_mem_supported {s : Set α} {a : α} (b : M) (h : a ∈ s) :
    singlesingle a b ∈ supported M R s :=
  Set.Subset.trans support_single_subset (Finset.singleton_subset_set_iff.2 h)

Membership of Single Function in Supported Submodule

Informal description

For any set $s \subseteq \alpha$, element $a \in s$, and element $b \in M$, the finitely supported function $\text{single } a b$ (which takes value $b$ at $a$ and zero elsewhere) belongs to the submodule of finitely supported functions with support contained in $s$.

Finsupp.supported_eq_span_single theorem

(s : Set α) : supported R R s = span R ((fun i => single i 1) '' s)

Full source

theorem supported_eq_span_single (s : Set α) :
    supported R R s = span R ((fun i => single i 1) '' s) := by
  refine (span_eq_of_le _ ?_ (SetLike.le_def.2 fun l hl => ?_)).symm
  · rintro _ ⟨_, hp, rfl⟩
    exact single_mem_supported R 1 hp
  · rw [← l.sum_single]
    refine sum_mem fun i il => ?_
    rw [show single i (l i) = l i • single i 1 by simp [span]]
    exact smul_mem _ (l i) (subset_span (mem_image_of_mem _ (hl il)))

Span Characterization of Supported Functions: $\operatorname{supported}_R R s = \operatorname{span}_R \{\operatorname{single}_i 1 \mid i \in s\}$

Informal description

For any set $s \subseteq \alpha$, the submodule of finitely supported functions $\operatorname{supported}_R R s$ (consisting of functions with support contained in $s$) is equal to the $R$-linear span of the image of $s$ under the map $i \mapsto \operatorname{single}_i 1$, where $\operatorname{single}_i 1$ denotes the function that is $1$ at $i$ and $0$ elsewhere.

Finsupp.span_le_supported_biUnion_support theorem

(s : Set (α →₀ M)) : span R s ≤ supported M R (⋃ x ∈ s, x.support)

Full source

theorem span_le_supported_biUnion_support (s : Set (α →₀ M)) :
    span R s ≤ supported M R (⋃ x ∈ s, x.support) :=
  span_le.mpr fun _ h ↦ subset_biUnion_of_mem h (u := (·.support.toSet))

Span containment in supported functions of union of supports

Informal description

For any set $s$ of finitely supported functions from $\alpha$ to $M$, the $R$-linear span of $s$ is contained in the submodule of functions supported on the union of the supports of all functions in $s$. That is, $$\operatorname{span}_R s \leq \operatorname{supported}_R M \left( \bigcup_{x \in s} \operatorname{supp}(x) \right)$$ where $\operatorname{supp}(x)$ denotes the support of the function $x$.

Finsupp.restrictDom definition

(s : Set α) [DecidablePred (· ∈ s)] : (α →₀ M) →ₗ[R] supported M R s

Full source

/-- Interpret `Finsupp.filter s` as a linear map from `α →₀ M` to `supported M R s`. -/
def restrictDom (s : Set α) [DecidablePred (· ∈ s)] : (α →₀ M) →ₗ[R] supported M R s :=
  LinearMap.codRestrict _
    { toFun := filter (· ∈ s)
      map_add' := fun _ _ => filter_add
      map_smul' := fun _ _ => filter_smul } fun l =>
    (mem_supported' _ _).2 fun _ => filter_apply_neg (· ∈ s) l

Restriction of finitely supported functions to a submodule supported on a set

Informal description

For a given set $s \subseteq \alpha$ with decidable membership, the linear map $\text{restrictDom}_{M,R,s} : (\alpha \to_{\text{f}} M) \to \text{supported } M R s$ restricts a finitely supported function to its values on $s$, where $\text{supported } M R s$ is the submodule of finitely supported functions with support contained in $s$. More precisely, for any $f \in \alpha \to_{\text{f}} M$, the map $\text{restrictDom}_{M,R,s}(f)$ is equal to $f$ on $s$ and zero elsewhere.

Finsupp.restrictDom_apply theorem

 (s : Set α) (l : α →₀ M) [DecidablePred (· ∈ s)] : (restrictDom M R s l : α →₀ M) = Finsupp.filter (· ∈ s) l

Full source

@[simp]
theorem restrictDom_apply (s : Set α) (l : α →₀ M) [DecidablePred (· ∈ s)] :
    (restrictDom M R s l : α →₀ M) = Finsupp.filter (· ∈ s) l := rfl

Restriction of Finitely Supported Function to Submodule Equals Filtered Function

Informal description

For any set $s \subseteq \alpha$ with decidable membership and any finitely supported function $l : \alpha \to_{\text{f}} M$, the restriction of $l$ to the submodule of functions supported on $s$ is equal to the filtered function that coincides with $l$ on $s$ and is zero elsewhere. That is, $$(\text{restrictDom}_{M,R,s}\, l : \alpha \to_{\text{f}} M) = \text{filter}\, (\cdot \in s)\, l.$$

Finsupp.restrictDom_comp_subtype theorem

(s : Set α) [DecidablePred (· ∈ s)] : (restrictDom M R s).comp (Submodule.subtype _) = LinearMap.id

Full source

theorem restrictDom_comp_subtype (s : Set α) [DecidablePred (· ∈ s)] :
    (restrictDom M R s).comp (Submodule.subtype _) = LinearMap.id := by
  ext l a
  by_cases h : a ∈ s
  · simp [h]
  simpa [h] using ((mem_supported' R l.1).1 l.2 a h).symm

Restriction-Inclusion Composition Yields Identity on Supported Functions

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\alpha$ a type. For any subset $s \subseteq \alpha$ with decidable membership, the composition of the linear map $\text{restrictDom}_{M,R,s} \colon (\alpha \to_{\text{f}} M) \to \text{supported } M R s$ (which restricts a finitely supported function to $s$) with the canonical inclusion $\text{supported } M R s \hookrightarrow (\alpha \to_{\text{f}} M)$ is equal to the identity linear map on $\text{supported } M R s$.

Finsupp.range_restrictDom theorem

(s : Set α) [DecidablePred (· ∈ s)] : LinearMap.range (restrictDom M R s) = ⊤

Full source

theorem range_restrictDom (s : Set α) [DecidablePred (· ∈ s)] :
    LinearMap.range (restrictDom M R s) = ⊤ :=
  range_eq_top.2 <|
    Function.RightInverse.surjective <| LinearMap.congr_fun (restrictDom_comp_subtype s)

Surjectivity of Restriction Map to Finitely Supported Functions on a Set

Informal description

For any set $s \subseteq \alpha$ with decidable membership, the range of the linear map $\text{restrictDom}_{M,R,s} \colon (\alpha \to_{\text{f}} M) \to \text{supported } M R s$ is equal to the entire codomain $\text{supported } M R s$. In other words, the restriction map is surjective onto the submodule of finitely supported functions with support contained in $s$.

Finsupp.supported_mono theorem

{s t : Set α} (st : s ⊆ t) : supported M R s ≤ supported M R t

Full source

theorem supported_mono {s t : Set α} (st : s ⊆ t) : supported M R s ≤ supported M R t := fun _ h =>
  Set.Subset.trans h st

Monotonicity of Finitely Supported Functions Submodule with Respect to Support Inclusion

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, if $s$ is a subset of $t$, then the submodule of finitely supported functions with support contained in $s$ is a submodule of the submodule of finitely supported functions with support contained in $t$.

Finsupp.supported_empty theorem

: supported M R (∅ : Set α) = ⊥

Full source

@[simp]
theorem supported_empty : supported M R (∅ : Set α) = ⊥ :=
  eq_bot_iff.2 fun l h => (Submodule.mem_bot R).2 <| by ext; simp_all [mem_supported']

Triviality of Finitely Supported Functions with Empty Support

Informal description

For any type $\alpha$, semiring $R$, and additive commutative monoid $M$, the submodule of finitely supported functions $\alpha \to_{\text{f}} M$ with support contained in the empty set is equal to the trivial submodule $\bot$.

Finsupp.supported_univ theorem

: supported M R (Set.univ : Set α) = ⊤

Full source

@[simp]
theorem supported_univ : supported M R (Set.univ : Set α) = ⊤ :=
  eq_top_iff.2 fun _ _ => Set.subset_univ _

The supported submodule on the universal set is the entire space of finitely supported functions

Informal description

For any type $\alpha$, semiring $R$, and additive commutative monoid $M$ with an $R$-module structure, the submodule of finitely supported functions $\alpha \to_{\text{f}} M$ with support contained in the universal set $\text{univ}$ is equal to the entire space of finitely supported functions, i.e., $\text{supported}_M^R(\text{univ}) = \top$.

Finsupp.supported_iUnion theorem

{δ : Type*} (s : δ → Set α) : supported M R (⋃ i, s i) = ⨆ i, supported M R (s i)

Full source

theorem supported_iUnion {δ : Type*} (s : δ → Set α) :
    supported M R (⋃ i, s i) = ⨆ i, supported M R (s i) := by
  refine le_antisymm ?_ (iSup_le fun i => supported_mono <| Set.subset_iUnion _ _)
  haveI := Classical.decPred fun x => x ∈ ⋃ i, s i
  suffices
    LinearMap.range ((Submodule.subtype _).comp (restrictDom M R (⋃ i, s i))) ≤
      ⨆ i, supported M R (s i) by
    rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this
  rw [range_le_iff_comap, eq_top_iff]
  rintro l ⟨⟩
  induction l using Finsupp.induction with
  | zero => exact zero_mem _
  | single_add x a l _ _ ih =>
    refine add_mem ?_ ih
    by_cases h : ∃ i, x ∈ s i
    · simp only [mem_comap, coe_comp, coe_subtype, Function.comp_apply, restrictDom_apply,
        mem_iUnion, h, filter_single_of_pos]
      obtain ⟨i, hi⟩ := h
      exact le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi)
    · simp [h]

Union of Supports Equals Supremum of Supported Submodules

Informal description

For any indexed family of sets $s : \delta \to \text{Set } \alpha$, the submodule of finitely supported functions with support in the union $\bigcup_i s_i$ is equal to the supremum of the submodules of finitely supported functions with support in each $s_i$. That is, \[ \text{supported}_R M \left( \bigcup_i s_i \right) = \bigsqcup_i \text{supported}_R M (s_i). \]

Finsupp.supported_union theorem

(s t : Set α) : supported M R (s ∪ t) = supported M R s ⊔ supported M R t

Full source

theorem supported_union (s t : Set α) :
    supported M R (s ∪ t) = supportedsupported M R s ⊔ supported M R t := by
  rw [Set.union_eq_iUnion, supported_iUnion, iSup_bool_eq, cond_true, cond_false]

Union of Supports Equals Join of Supported Submodules

Informal description

For any two subsets $s$ and $t$ of a type $\alpha$, the submodule of finitely supported functions from $\alpha$ to $M$ with support contained in $s \cup t$ is equal to the supremum (join) of the submodules of finitely supported functions with support contained in $s$ and $t$ respectively. That is, \[ \text{supported}_R M (s \cup t) = \text{supported}_R M s \sqcup \text{supported}_R M t. \]

Finsupp.supported_iInter theorem

{ι : Type*} (s : ι → Set α) : supported M R (⋂ i, s i) = ⨅ i, supported M R (s i)

Full source

theorem supported_iInter {ι : Type*} (s : ι → Set α) :
    supported M R (⋂ i, s i) = ⨅ i, supported M R (s i) :=
  Submodule.ext fun x => by simp [mem_supported, subset_iInter_iff]

Intersection of Supports Equals Infimum of Supported Submodules

Informal description

For any indexed family of sets $s : \iota \to \text{Set } \alpha$, the submodule of finitely supported functions with support in the intersection $\bigcap_i s_i$ is equal to the infimum of the submodules of finitely supported functions with support in each $s_i$. That is, \[ \text{supported}_R M \left( \bigcap_i s_i \right) = \bigsqcap_i \text{supported}_R M (s_i). \]

Finsupp.supported_inter theorem

(s t : Set α) : supported M R (s ∩ t) = supported M R s ⊓ supported M R t

Full source

theorem supported_inter (s t : Set α) :
    supported M R (s ∩ t) = supportedsupported M R s ⊓ supported M R t := by
  rw [Set.inter_eq_iInter, supported_iInter, iInf_bool_eq]; rfl

Intersection of Supports Equals Meet of Supported Submodules

Informal description

For any two subsets $s$ and $t$ of a type $\alpha$, the submodule of finitely supported functions from $\alpha$ to $M$ with support contained in $s \cap t$ is equal to the infimum (meet) of the submodules of finitely supported functions with support contained in $s$ and $t$ respectively. That is, \[ \text{supported}_R M (s \cap t) = \text{supported}_R M s \sqcap \text{supported}_R M t. \]

Finsupp.disjoint_supported_supported theorem

{s t : Set α} (h : Disjoint s t) : Disjoint (supported M R s) (supported M R t)

Full source

theorem disjoint_supported_supported {s t : Set α} (h : Disjoint s t) :
    Disjoint (supported M R s) (supported M R t) :=
  disjoint_iff.2 <| by rw [← supported_inter, disjoint_iff_inter_eq_empty.1 h, supported_empty]

Disjointness of Supported Submodules for Disjoint Sets

Informal description

For any two disjoint subsets $s$ and $t$ of a type $\alpha$, the submodules of finitely supported functions from $\alpha$ to $M$ with supports contained in $s$ and $t$ respectively are also disjoint. That is, if $s \cap t = \emptyset$, then $\text{supported}_R M s \sqcap \text{supported}_R M t = \bot$.

Finsupp.disjoint_supported_supported_iff theorem

[Nontrivial M] {s t : Set α} : Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t

Full source

theorem disjoint_supported_supported_iff [Nontrivial M] {s t : Set α} :
    DisjointDisjoint (supported M R s) (supported M R t) ↔ Disjoint s t := by
  refine ⟨fun h => Set.disjoint_left.mpr fun x hx1 hx2 => ?_, disjoint_supported_supported⟩
  rcases exists_ne (0 : M) with ⟨y, hy⟩
  have := h.le_bot ⟨single_mem_supported R y hx1, single_mem_supported R y hx2⟩
  rw [mem_bot, single_eq_zero] at this
  exact hy this

Disjointness Criterion for Supported Submodules: $\text{supported}_R M s \sqcap \text{supported}_R M t = \bot \leftrightarrow s \cap t = \emptyset$

Informal description

For a nontrivial module $M$ over a semiring $R$ and subsets $s, t$ of a type $\alpha$, the submodules of finitely supported functions with supports contained in $s$ and $t$ are disjoint if and only if the sets $s$ and $t$ themselves are disjoint. In symbols: \[ \text{supported}_R M s \sqcap \text{supported}_R M t = \bot \leftrightarrow s \cap t = \emptyset. \]

Finsupp.supportedEquivFinsupp definition

(s : Set α) : supported M R s ≃ₗ[R] s →₀ M

Full source

/-- Interpret `Finsupp.restrictSupportEquiv` as a linear equivalence between
`supported M R s` and `s →₀ M`. -/
@[simps!] def supportedEquivFinsupp (s : Set α) : supportedsupported M R s ≃ₗ[R] s →₀ M := by
  let F : supportedsupported M R s ≃ (s →₀ M) := restrictSupportEquiv s M
  refine F.toLinearEquiv ?_
  have :
    (F : supported M R s → ↥s →₀ M) =
      (lsubtypeDomain s : (α →₀ M) →ₗ[R] s →₀ M).comp (Submodule.subtype (supported M R s)) :=
    rfl
  rw [this]
  exact LinearMap.isLinear _

Linear equivalence between finitely supported functions with restricted support and functions on the subset

Informal description

Given a semiring $R$, an additive commutative monoid $M$ with an $R$-module structure, and a subset $s$ of a type $\alpha$, the linear equivalence $\mathrm{supportedEquivFinsupp}\, s$ establishes an isomorphism between: 1. The submodule of finitely supported functions $f \colon \alpha \to_{\text{f}} M$ with support contained in $s$ 2. The space of finitely supported functions $s \to_{\text{f}} M$ This equivalence is the linear version of $\mathrm{restrictSupportEquiv}$, where the forward direction restricts a function to $s$ and the inverse direction extends a function from $s$ to $\alpha$ by setting it to zero outside $s$.

Finsupp.supportedEquivFinsupp_symm_apply_coe theorem

(s : Set α) [DecidablePred (· ∈ s)] (f : s →₀ M) : (supportedEquivFinsupp (R := R) s).symm f = f.extendDomain

Full source

@[simp] theorem supportedEquivFinsupp_symm_apply_coe (s : Set α) [DecidablePred (· ∈ s)]
    (f : s →₀ M) : (supportedEquivFinsupp (R := R) s).symm f = f.extendDomain := by
  convert restrictSupportEquiv_symm_apply_coe ..

Inverse of Supported Equivalence is Extension by Zero

Informal description

For any subset $s$ of a type $\alpha$ and any finitely supported function $f \colon s \to_{\text{f}} M$, the inverse of the linear equivalence $\mathrm{supportedEquivFinsupp}\, s$ applied to $f$ is equal to the extension of $f$ to $\alpha$ by zero outside $s$. In symbols: \[ (\mathrm{supportedEquivFinsupp}\, s)^{-1}(f) = f.\mathrm{extendDomain}. \]

Finsupp.supported_comap_lmapDomain theorem

(f : α → α') (s : Set α') : supported M R (f ⁻¹' s) ≤ (supported M R s).comap (lmapDomain M R f)

Full source

theorem supported_comap_lmapDomain (f : α → α') (s : Set α') :
    supported M R (f ⁻¹' s) ≤ (supported M R s).comap (lmapDomain M R f) := by
  classical
  intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)
  show ↑(mapDomain f l).support ⊆ s
  rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
  exact Set.Subset.trans mapDomain_support hl

Inclusion of Supported Submodules under Preimage and Linear Map

Informal description

For any function $f \colon \alpha \to \alpha'$ and subset $s \subseteq \alpha'$, the submodule of finitely supported functions with support contained in the preimage $f^{-1}(s)$ is contained in the preimage of the submodule of finitely supported functions with support in $s$ under the linear map induced by $f$. In symbols: \[ \text{supported}\, M\, R\, (f^{-1}(s)) \leq (\text{supported}\, M\, R\, s).\text{comap}\, (\text{lmapDomain}\, M\, R\, f). \]

Finsupp.lmapDomain_supported theorem

(f : α → α') (s : Set α) : (supported M R s).map (lmapDomain M R f) = supported M R (f '' s)

Full source

theorem lmapDomain_supported (f : α → α') (s : Set α) :
    (supported M R s).map (lmapDomain M R f) = supported M R (f '' s) := by
  classical
  cases isEmpty_or_nonempty α
  · simp [s.eq_empty_of_isEmpty]
  refine
    le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_
  intro l hl
  refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
  · rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩
    exact Function.invFunOn_mem (by simpa using hl hc)
  · rw [← LinearMap.comp_apply, ← lmapDomain_comp]
    refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
    exact Function.invFunOn_eq (by simpa using hl hc)

Image of Supported Submodule under Linear Domain Mapping Equals Supported Submodule of Image

Informal description

For any function $f \colon \alpha \to \alpha'$ and subset $s \subseteq \alpha$, the image of the submodule of finitely supported functions with support in $s$ under the linear map induced by $f$ is equal to the submodule of finitely supported functions with support in the image $f(s)$. In symbols: \[ \text{map}\, (\text{lmapDomain}\, M\, R\, f)\, (\text{supported}\, M\, R\, s) = \text{supported}\, M\, R\, (f(s)). \]

Finsupp.lmapDomain_disjoint_ker theorem

 (f : α → α') {s : Set α} (H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b) :
  Disjoint (supported M R s) (ker (lmapDomain M R f))

Full source

theorem lmapDomain_disjoint_ker (f : α → α') {s : Set α}
    (H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b) :
    Disjoint (supported M R s) (ker (lmapDomain M R f)) := by
  rw [disjoint_iff_inf_le]
  rintro l ⟨h₁, h₂⟩
  rw [SetLike.mem_coe, mem_ker, lmapDomain_apply, mapDomain] at h₂
  simp only [mem_bot]; ext x
  haveI := Classical.decPred fun x => x ∈ s
  by_cases xs : x ∈ s
  · have : Finsupp.sum l (fun a => Finsupp.single (f a)) (f x) = 0 := by
      rw [h₂]
      rfl
    rw [Finsupp.sum_apply, Finsupp.sum_eq_single x, single_eq_same] at this
    · simpa
    · intro y hy xy
      simp only [SetLike.mem_coe, mem_supported, subset_def, Finset.mem_coe, mem_support_iff] at h₁
      simp [mt (H _ (h₁ _ hy) _ xs) xy]
    · simp +contextual
  · by_contra h
    exact xs (h₁ <| Finsupp.mem_support_iff.2 h)

Disjointness of Supported Submodule and Kernel under Injective Domain Mapping

Informal description

Let $f \colon \alpha \to \alpha'$ be a function and $s \subseteq \alpha$ a subset such that $f$ is injective on $s$ (i.e., for any $a, b \in s$, if $f(a) = f(b)$ then $a = b$). Then the submodule of finitely supported functions with support in $s$ is disjoint from the kernel of the linear map induced by $f$ on the space of finitely supported functions $\alpha \to_{\text{f}} M$.

Finsupp.congr definition

{α' : Type*} (s : Set α) (t : Set α') (e : s ≃ t) : supported M R s ≃ₗ[R] supported M R t

Full source

/-- An equivalence of sets induces a linear equivalence of `Finsupp`s supported on those sets. -/
noncomputable def congr {α' : Type*} (s : Set α) (t : Set α') (e : s ≃ t) :
    supportedsupported M R s ≃ₗ[R] supported M R t := by
  haveI := Classical.decPred fun x => x ∈ s
  haveI := Classical.decPred fun x => x ∈ t
  exact Finsupp.supportedEquivFinsuppFinsupp.supportedEquivFinsupp s ≪≫ₗ
    (Finsupp.domLCongr e ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm)

Linear equivalence of supported finitely supported functions under set equivalence

Informal description

Given a semiring $R$, an additive commutative monoid $M$ with an $R$-module structure, and two sets $s \subseteq \alpha$ and $t \subseteq \alpha'$ that are equivalent via a bijection $e: s \simeq t$, there exists a linear equivalence between: 1. The submodule of finitely supported functions $\alpha \to_{\text{f}} M$ with support contained in $s$ 2. The submodule of finitely supported functions $\alpha' \to_{\text{f}} M$ with support contained in $t$ This equivalence is constructed by composing: - The linear equivalence between $s$-supported functions and functions $s \to_{\text{f}} M$ - The linear equivalence induced by $e$ between function spaces $s \to_{\text{f}} M$ and $t \to_{\text{f}} M$ - The inverse of the linear equivalence between $t$-supported functions and functions $t \to_{\text{f}} M$

Tags