Documentation

Mathlib.Data.Finsupp.Sigma

Embedding a finitely supported function into a sigma type summand #

This file provides Finsupp.embSigma, which embeds a finitely supported function ι k →₀ M into the corresponding summand of (Σ k, ι k) →₀ M.

Main declarations #

Implementation notes #

This is a special case of Finsupp.embDomain using Function.Embedding.sigmaMk.

source
🔸 coverage
def Finsupp.embSigma {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} (f : ι k →₀ M) :
(k : κ) × ι k →₀ M

Embed a finitely supported function f : ι k →₀ M into the k-th summand of the sigma type (Σ k, ι k) →₀ M.

This is Finsupp.embDomain specialized to Function.Embedding.sigmaMk k.

Equations
    Instances For
      source
      📐 coverage
      theorem Finsupp.embSigma_apply {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] [DecidableEq κ] {k : κ} (f : ι k →₀ M) (i : (k : κ) × ι k) :
      f.embSigma i = if h : i.fst = k then f (h ▸ i.snd) else 0
      source
      📐 coverage
      @[simp]
      theorem Finsupp.embSigma_apply_self {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} (f : ι k →₀ M) (i : ι k) :
      f.embSigma ⟨k, i⟩ = f i
      source
      📐 coverage
      theorem Finsupp.embSigma_apply_of_ne {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k k' : κ} (f : ι k →₀ M) (hk : k' ≠ k) (i : ι k') :
      f.embSigma ⟨k', i⟩ = 0

      Values of embSigma f at indices outside the k-th summand are zero.

      source
      📐 coverage
      @[simp]
      theorem Finsupp.support_embSigma {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} (f : ι k →₀ M) :
      f.embSigma.support = Finset.map (Function.Embedding.sigmaMk k) f.support
      source
      📐 coverage
      @[simp]
      theorem Finsupp.embSigma_zero {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} :
      embSigma 0 = 0
      source
      📐 coverage
      @[simp]
      theorem Finsupp.embSigma_eq_zero {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} {f : ι k →₀ M} :
      f.embSigma = 0 ↔ f = 0
      source
      📐 coverage
      theorem Finsupp.embSigma_injective {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} :
      Function.Injective embSigma
      source
      📐 coverage
      @[simp]
      theorem Finsupp.embSigma_inj {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} {f g : ι k →₀ M} :
      f.embSigma = g.embSigma ↔ f = g
      source
      📐 coverage
      theorem Finsupp.embSigma_add {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [AddMonoid M] {k : κ} (f g : ι k →₀ M) :
      (f + g).embSigma = f.embSigma + g.embSigma
      source
      📐 coverage
      @[simp]
      theorem Finsupp.embSigma_single {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} (i : ι k) (m : M) :
      (fun₀ | i => m).embSigma = fun₀ | ⟨k, i⟩ => m
      source
      📐 coverage
      @[simp]
      theorem Finsupp.split_embSigma_self {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} (f : ι k →₀ M) :
      f.embSigma.split k = f

      embSigma is a left inverse to split at the same index.

      source
      📐 coverage
      theorem Finsupp.split_embSigma_of_ne {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k k' : κ} (f : ι k →₀ M) (hk : k' ≠ k) :
      f.embSigma.split k' = 0

      split returns zero at indices different from where embSigma embeds.