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
noncomputable 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
    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
    @[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
    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
    @[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
    @[simp]
    theorem Finsupp.embSigma_zero {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} :
    embSigma 0 = 0
    source
    @[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
    theorem Finsupp.embSigma_injective {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} :
    Function.Injective embSigma
    source
    @[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
    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
    @[simp]
    theorem Finsupp.embSigma_single {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [Zero M] {k : κ} (i : ι k) (m : M) :
    (single i m).embSigma = single ⟨k, i⟩ m
    source
    @[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
    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.