Mathlib.LinearAlgebra.Finsupp.Span

Finsupp.ker_lsingle theorem

(a : α) : ker (lsingle a : M →ₗ[R] α →₀ M) = ⊥

Full source

@[simp]
theorem ker_lsingle (a : α) : ker (lsingle a : M →ₗ[R] α →₀ M) = ⊥ :=
  ker_eq_bot_of_injective (single_injective a)

Trivial Kernel of Single-Point Linear Finitely Supported Function

Informal description

For any element $a$ in a type $\alpha$, the kernel of the linear map $\text{lsingle}(a) : M \to_{\text{lin}} (\alpha \to_{\text{f}} M)$, which sends an element $b \in M$ to the finitely supported function that is $b$ at $a$ and zero elsewhere, is trivial. That is, $\ker(\text{lsingle}(a)) = \{0\}$.

Finsupp.lsingle_range_le_ker_lapply theorem

 (s t : Set α) (h : Disjoint s t) :
  ⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M) ≤ ⨅ a ∈ t, ker (lapply a : (α →₀ M) →ₗ[R] M)

Full source

theorem lsingle_range_le_ker_lapply (s t : Set α) (h : Disjoint s t) :
    ⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M) ≤
      ⨅ a ∈ t, ker (lapply a : (α →₀ M) →ₗ[R] M) := by
  refine iSup_le fun a₁ => iSup_le fun h₁ => range_le_iff_comap.2 ?_
  simp only [(ker_comp _ _).symm, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]
  intro b _ a₂ h₂
  have : a₁ ≠ a₂ := fun eq => h.le_bot ⟨h₁, eq.symm ▸ h₂⟩
  exact single_eq_of_ne this

Inclusion of Ranges of Single-Point Functions in Kernels of Evaluations for Disjoint Sets

Informal description

Let $s$ and $t$ be disjoint subsets of a type $\alpha$. For any semiring $R$ and any $R$-module $M$, the supremum of the ranges of the linear maps $\text{lsingle}(a) : M \to \alpha \to_{\text{f}} M$ (which sends $m \in M$ to the finitely supported function that is $m$ at $a$ and zero elsewhere) over all $a \in s$ is less than or equal to the infimum of the kernels of the evaluation maps $\text{lapply}(a) : (\alpha \to_{\text{f}} M) \to M$ (which evaluates a finitely supported function at $a$) over all $a \in t$. In symbols: \[ \bigsqcup_{a \in s} \text{range}(\text{lsingle}(a)) \leq \bigsqcap_{a \in t} \text{ker}(\text{lapply}(a)) \]

Finsupp.iInf_ker_lapply_le_bot theorem

: ⨅ a, ker (lapply a : (α →₀ M) →ₗ[R] M) ≤ ⊥

Full source

theorem iInf_ker_lapply_le_bot : ⨅ a, ker (lapply a : (α →₀ M) →ₗ[R] M) ≤ ⊥ := by
  simp only [SetLike.le_def, mem_iInf, mem_ker, mem_bot, lapply_apply]
  exact fun a h => Finsupp.ext h

Infimum of Evaluation Kernels is Trivial in Finitely Supported Functions

Informal description

For any type $\alpha$ and any module $M$ over a semiring $R$, the infimum of the kernels of the evaluation maps $\operatorname{ker}(\operatorname{lapply}_a)$ for all $a \in \alpha$ is less than or equal to the trivial submodule $\bot$. Here, $\operatorname{lapply}_a$ denotes the linear map from $\alpha \to_{\text{f}} M$ to $M$ that evaluates a finitely supported function at $a$.

Finsupp.iSup_lsingle_range theorem

: ⨆ a, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M) = ⊤

Full source

theorem iSup_lsingle_range : ⨆ a, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M) = ⊤ := by
  refine eq_top_iff.2 <| SetLike.le_def.2 fun f _ => ?_
  rw [← sum_single f]
  exact sum_mem fun a _ => Submodule.mem_iSup_of_mem a ⟨_, rfl⟩

Span of Single-Element Functions is Entire Space of Finitely Supported Functions

Informal description

For any type $\alpha$ and any module $M$ over a semiring $R$, the supremum of the ranges of the linear maps `lsingle a : M →ₗ[R] α →₀ M` for all $a \in \alpha$ is equal to the top submodule of $\alpha \to₀ M$. In other words, the span of all single-element functions is the entire space of finitely supported functions.

Finsupp.disjoint_lsingle_lsingle theorem

 (s t : Set α) (hs : Disjoint s t) :
  Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M))
    (⨆ a ∈ t, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M))

Full source

theorem disjoint_lsingle_lsingle (s t : Set α) (hs : Disjoint s t) :
    Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M))
      (⨆ a ∈ t, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) := by
  refine
    (Disjoint.mono
      (lsingle_range_le_ker_lapply s sᶜ disjoint_compl_right)
      (lsingle_range_le_ker_lapply t tᶜ disjoint_compl_right))
      ?_
  rw [disjoint_iff_inf_le]
  refine le_trans (le_iInf fun i => ?_) iInf_ker_lapply_le_bot
  classical
    by_cases his : i ∈ s
    · by_cases hit : i ∈ t
      · exact (hs.le_bot ⟨his, hit⟩).elim
      exact inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)
    exact inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)

Disjointness of Span of Single-Element Functions for Disjoint Sets

Informal description

For any two disjoint subsets $s$ and $t$ of a type $\alpha$, and for any module $M$ over a semiring $R$, the subspaces generated by the ranges of the linear maps $\text{lsingle}(a) : M \to \alpha \to_{\text{f}} M$ for all $a \in s$ and $a \in t$ are disjoint. Here, $\text{lsingle}(a)$ maps an element $m \in M$ to the finitely supported function that is $m$ at $a$ and zero elsewhere. In symbols: \[ \text{Disjoint}\left(\bigsqcup_{a \in s} \text{range}(\text{lsingle}(a)), \bigsqcup_{a \in t} \text{range}(\text{lsingle}(a))\right) \]

Finsupp.span_single_image theorem

 (s : Set M) (a : α) : Submodule.span R (single a '' s) = (Submodule.span R s).map (lsingle a : M →ₗ[R] α →₀ M)

Full source

theorem span_single_image (s : Set M) (a : α) :
    Submodule.span R (singlesingle a '' s) = (Submodule.span R s).map (lsingle a : M →ₗ[R] α →₀ M) := by
  rw [← span_image]; rfl

Span-Image Commutation for Finitely Supported Single-Element Functions

Informal description

For any subset $s$ of an $R$-module $M$ and any element $a \in \alpha$, the span of the image of $s$ under the finitely supported function $\text{single}(a, \cdot)$ is equal to the image of the span of $s$ under the linear map $\text{lsingle}(a) : M \to \alpha \to_{\text{f}} M$. In symbols: \[ \operatorname{span}_R \left( \text{single}(a, \cdot)(s) \right) = \text{lsingle}(a)(\operatorname{span}_R s). \]

Submodule.exists_finset_of_mem_iSup theorem

{ι : Sort _} (p : ι → Submodule R M) {m : M} (hm : m ∈ ⨆ i, p i) : ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i

Full source

theorem Submodule.exists_finset_of_mem_iSup {ι : Sort _} (p : ι → Submodule R M) {m : M}
    (hm : m ∈ ⨆ i, p i) : ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i := by
  have :=
    CompleteLattice.IsCompactElement.exists_finset_of_le_iSup (Submodule R M)
      (Submodule.singleton_span_isCompactElement m) p
  simp only [Submodule.span_singleton_le_iff_mem] at this
  exact this hm

Finite Approximation Property for Elements in Suprema of Submodules

Informal description

Let $M$ be a module over a ring $R$, and let $\{p_i\}_{i \in \iota}$ be a family of submodules of $M$ indexed by a type $\iota$. For any element $m \in M$ that belongs to the supremum of the submodules $\bigsqcup_{i \in \iota} p_i$, there exists a finite subset $s \subseteq \iota$ such that $m$ belongs to the supremum $\bigsqcup_{i \in s} p_i$.

Submodule.mem_iSup_iff_exists_finset theorem

{ι : Sort _} {p : ι → Submodule R M} {m : M} : (m ∈ ⨆ i, p i) ↔ ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i

Full source

/-- `Submodule.exists_finset_of_mem_iSup` as an `iff` -/
theorem Submodule.mem_iSup_iff_exists_finset {ι : Sort _} {p : ι → Submodule R M} {m : M} :
    (m ∈ ⨆ i, p i) ↔ ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i :=
  ⟨Submodule.exists_finset_of_mem_iSup p, fun ⟨_, hs⟩ =>
    iSup_mono (fun i => (iSup_const_le : _ ≤ p i)) hs⟩

Characterization of Membership in Supremum of Submodules via Finite Approximation

Informal description

Let $M$ be a module over a ring $R$, and let $\{p_i\}_{i \in \iota}$ be a family of submodules of $M$ indexed by a type $\iota$. For any element $m \in M$, we have $m \in \bigsqcup_{i \in \iota} p_i$ if and only if there exists a finite subset $s \subseteq \iota$ such that $m \in \bigsqcup_{i \in s} p_i$.

Submodule.mem_sSup_iff_exists_finset theorem

 {S : Set (Submodule R M)} {m : M} : m ∈ sSup S ↔ ∃ s : Finset (Submodule R M), ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i

Full source

theorem Submodule.mem_sSup_iff_exists_finset {S : Set (Submodule R M)} {m : M} :
    m ∈ sSup Sm ∈ sSup S ↔ ∃ s : Finset (Submodule R M), ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i := by
  rw [sSup_eq_iSup, iSup_subtype', Submodule.mem_iSup_iff_exists_finset]
  refine ⟨fun ⟨s, hs⟩ ↦ ⟨s.map (Function.Embedding.subtype S), ?_, ?_⟩,
          fun ⟨s, hsS, hs⟩ ↦ ⟨s.preimage (↑) Subtype.coe_injective.injOn, ?_⟩⟩
  · simpa using fun x _ ↦ x.property
  · suffices m ∈ ⨆ (i) (hi : i ∈ S) (_ : ⟨i, hi⟩ ∈ s), i by simpa
    rwa [iSup_subtype']
  · have : ⨆ (i) (_ : i ∈ S ∧ i ∈ s), i = ⨆ (i) (_ : i ∈ s), i := by convert rfl; aesop
    simpa only [Finset.mem_preimage, iSup_subtype, iSup_and', this]

Characterization of membership in supremum of submodules via finite approximation

Informal description

Let $M$ be a module over a ring $R$, and let $S$ be a set of submodules of $M$. For any element $m \in M$, we have $m \in \bigvee S$ if and only if there exists a finite subset $s \subseteq S$ such that $m \in \bigvee_{N \in s} N$, where $\bigvee$ denotes the supremum of submodules.

Tags