Finitely supported functions on exactly one point

This file contains definitions and basic results on defining/updating/removing Finsupps using one point of the domain.

Main declarations

• Finsupp.single: The Finsupp which is nonzero in exactly one point.
• Finsupp.update: Changes one value of a Finsupp.
• Finsupp.erase: Replaces one value of a Finsupp by 0.

Implementation notes

This file is a noncomputable theory and uses classical logic throughout.

Declarations about single

def Finsupp.single {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (b : M) : α →₀ M

single a b is the finitely supported function with value b at a and zero otherwise.

Equations

• Finsupp.single a b = { support := if b = 0 then ∅ else {a}, toFun := Pi.single a b, mem_support_toFun := ⋯ }

theorem Finsupp.single_apply {α : Type u_1} {M : Type u_5} [Zero M] {a a' : α} {b : M} [Decidable (a = a')] : (single a b) a' = if a = a' then b else 0

theorem Finsupp.single_apply_left {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α → β} (hf : Function.Injective f) (x z : α) (y : M) : (single (f x) y) (f z) = (single x y) z

theorem Finsupp.single_eq_set_indicator {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} : ⇑(single a b) = {a}.indicator fun (x : α) => b

@[simp]

theorem Finsupp.single_eq_same {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} : (single a b) a = b

@[simp]

theorem Finsupp.single_eq_of_ne {α : Type u_1} {M : Type u_5} [Zero M] {a a' : α} {b : M} (h : a ≠ a') : (single a b) a' = 0

theorem Finsupp.single_eq_update {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] (a : α) (b : M) : ⇑(single a b) = Function.update 0 a b

theorem Finsupp.single_eq_pi_single {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] (a : α) (b : M) : ⇑(single a b) = Pi.single a b

@[simp]

theorem Finsupp.single_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) : single a 0 = 0

theorem Finsupp.single_of_single_apply {α : Type u_1} {M : Type u_5} [Zero M] (a a' : α) (b : M) : single a ((single a' b) a) = (single a' (single a' b)) a

theorem Finsupp.support_single_ne_zero {α : Type u_1} {M : Type u_5} [Zero M] {b : M} (a : α) (hb : b ≠ 0) : (single a b).support = {a}

theorem Finsupp.support_single_subset {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} : (single a b).support ⊆ {a}

theorem Finsupp.single_apply_mem {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} (x : α) : (single a b) x ∈ {0, b}

theorem Finsupp.range_single_subset {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} : Set.range ⇑(single a b) ⊆ {0, b}

theorem Finsupp.single_injective {α : Type u_1} {M : Type u_5} [Zero M] (a : α) : Function.Injective (single a)

Finsupp.single a b is injective in b. For the statement that it is injective in a, see Finsupp.single_left_injective

theorem Finsupp.single_apply_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {a x : α} {b : M} : (single a b) x = 0 ↔ x = a → b = 0

theorem Finsupp.single_apply_ne_zero {α : Type u_1} {M : Type u_5} [Zero M] {a x : α} {b : M} : (single a b) x ≠ 0 ↔ x = a ∧ b ≠ 0

theorem Finsupp.mem_support_single {α : Type u_1} {M : Type u_5} [Zero M] (a a' : α) (b : M) : a ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0

theorem Finsupp.eq_single_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} {b : M} : f = single a b ↔ f.support ⊆ {a} ∧ f a = b

theorem Finsupp.single_eq_single_iff {α : Type u_1} {M : Type u_5} [Zero M] (a₁ a₂ : α) (b₁ b₂ : M) : single a₁ b₁ = single a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

theorem Finsupp.single_left_injective {α : Type u_1} {M : Type u_5} [Zero M] {b : M} (h : b ≠ 0) : Function.Injective fun (a : α) => single a b

Finsupp.single a b is injective in a. For the statement that it is injective in b, see Finsupp.single_injective

theorem Finsupp.single_left_inj {α : Type u_1} {M : Type u_5} [Zero M] {a a' : α} {b : M} (h : b ≠ 0) : single a b = single a' b ↔ a = a'

theorem Finsupp.apply_surjective {α : Type u_1} {M : Type u_5} [Zero M] (a : α) : Function.Surjective fun (f : α →₀ M) => f a

theorem Finsupp.support_single_ne_bot {α : Type u_1} {M : Type u_5} [Zero M] {b : M} (i : α) (h : b ≠ 0) : (single i b).support ≠ ⊥

theorem Finsupp.support_single_disjoint {α : Type u_1} {M : Type u_5} [Zero M] {b b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} : Disjoint (single i b).support (single j b').support ↔ i ≠ j

@[simp]

theorem Finsupp.single_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} : single a b = 0 ↔ b = 0

theorem Finsupp.single_ne_zero {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} : single a b ≠ 0 ↔ b ≠ 0

theorem Finsupp.single_swap {α : Type u_1} {M : Type u_5} [Zero M] (a₁ a₂ : α) (b : M) : (single a₁ b) a₂ = (single a₂ b) a₁

instance Finsupp.instNontrivial {α : Type u_1} {M : Type u_5} [Zero M] [Nonempty α] [Nontrivial M] : Nontrivial (α →₀ M)

theorem Finsupp.unique_single {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] (x : α →₀ M) : x = single default (x default)

@[simp]

theorem Finsupp.unique_single_eq_iff {α : Type u_1} {M : Type u_5} [Zero M] {a a' : α} {b : M} [Unique α] {b' : M} : single a b = single a' b' ↔ b = b'

theorem Finsupp.apply_single' {α : Type u_1} {N : Type u_7} {P : Type u_8} [Zero N] [Zero P] (e : N → P) (he : e 0 = 0) (a : α) (n : N) (b : α) : e ((single a n) b) = (single a (e n)) b

theorem Finsupp.apply_single {α : Type u_1} {N : Type u_7} {P : Type u_8} [Zero N] [Zero P] {F : Type u_13} [FunLike F N P] [ZeroHomClass F N P] (e : F) (a : α) (n : N) (b : α) : e ((single a n) b) = (single a (e n)) b

theorem Finsupp.support_eq_singleton {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} : f.support = {a} ↔ f a ≠ 0 ∧ f = single a (f a)

theorem Finsupp.support_eq_singleton' {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} : f.support = {a} ↔ ∃ (b : M), b ≠ 0 ∧ f = single a b

theorem Finsupp.card_support_eq_one {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} : f.support.card = 1 ↔ ∃ (a : α), f a ≠ 0 ∧ f = single a (f a)

theorem Finsupp.card_support_eq_one' {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} : f.support.card = 1 ↔ ∃ (a : α) (b : M), b ≠ 0 ∧ f = single a b

theorem Finsupp.support_subset_singleton {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} : f.support ⊆ {a} ↔ f = single a (f a)

theorem Finsupp.support_subset_singleton' {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} : f.support ⊆ {a} ↔ ∃ (b : M), f = single a b

theorem Finsupp.card_support_le_one {α : Type u_1} {M : Type u_5} [Zero M] [Nonempty α] {f : α →₀ M} : f.support.card ≤ 1 ↔ ∃ (a : α), f = single a (f a)

theorem Finsupp.card_support_le_one' {α : Type u_1} {M : Type u_5} [Zero M] [Nonempty α] {f : α →₀ M} : f.support.card ≤ 1 ↔ ∃ (a : α) (b : M), f = single a b

@[simp]

theorem Finsupp.equivFunOnFinite_single {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] [Finite α] (x : α) (m : M) : equivFunOnFinite (single x m) = Pi.single x m

@[simp]

theorem Finsupp.equivFunOnFinite_symm_single {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] [Finite α] (x : α) (m : M) : equivFunOnFinite.symm (Pi.single x m) = single x m

Declarations about update

def Finsupp.update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) : α →₀ M

Replace the value of a α →₀ M at a given point a : α by a given value b : M. If b = 0, this amounts to removing a from the Finsupp.support. Otherwise, if a was not in the Finsupp.support, it is added to it.

This is the finitely-supported version of Function.update.

Equations

• f.update a b = { support := if b = 0 then f.support.erase a else insert a f.support, toFun := Function.update (⇑f) a b, mem_support_toFun := ⋯ }

@[simp]

theorem Finsupp.coe_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) [DecidableEq α] : ⇑(f.update a b) = Function.update (⇑f) a b

@[simp]

theorem Finsupp.update_self {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) : f.update a (f a) = f

@[simp]

theorem Finsupp.zero_update {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (b : M) : update 0 a b = single a b

theorem Finsupp.support_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) [DecidableEq α] [DecidableEq M] : (f.update a b).support = if b = 0 then f.support.erase a else insert a f.support

@[simp]

theorem Finsupp.support_update_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) [DecidableEq α] : (f.update a 0).support = f.support.erase a

theorem Finsupp.support_update_ne_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) {b : M} [DecidableEq α] (h : b ≠ 0) : (f.update a b).support = insert a f.support

theorem Finsupp.support_update_subset {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) {b : M} [DecidableEq α] : (f.update a b).support ⊆ insert a f.support

theorem Finsupp.update_comm {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) {a₁ a₂ : α} (h : a₁ ≠ a₂) (m₁ m₂ : M) : (f.update a₁ m₁).update a₂ m₂ = (f.update a₂ m₂).update a₁ m₁

@[simp]

theorem Finsupp.update_idem {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b c : M) : (f.update a b).update a c = f.update a c

Declarations about erase

def Finsupp.erase {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (f : α →₀ M) : α →₀ M

erase a f is the finitely supported function equal to f except at a where it is equal to 0. If a is not in the support of f then erase a f = f.

Equations

• Finsupp.erase a f = { support := f.support.erase a, toFun := fun (a' : α) => if a' = a then 0 else f a', mem_support_toFun := ⋯ }

@[simp]

theorem Finsupp.support_erase {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] {a : α} {f : α →₀ M} : (erase a f).support = f.support.erase a

@[simp]

theorem Finsupp.erase_same {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {f : α →₀ M} : (erase a f) a = 0

@[simp]

theorem Finsupp.erase_ne {α : Type u_1} {M : Type u_5} [Zero M] {a a' : α} {f : α →₀ M} (h : a' ≠ a) : (erase a f) a' = f a'

theorem Finsupp.erase_apply {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] {a a' : α} {f : α →₀ M} : (erase a f) a' = if a' = a then 0 else f a'

@[simp]

theorem Finsupp.erase_single {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} : erase a (single a b) = 0

theorem Finsupp.erase_single_ne {α : Type u_1} {M : Type u_5} [Zero M] {a a' : α} {b : M} (h : a ≠ a') : erase a (single a' b) = single a' b

@[simp]

theorem Finsupp.erase_of_notMem_support {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} (haf : a ∉ f.support) : erase a f = f

@[deprecated Finsupp.erase_of_notMem_support (since := "2025-05-23")]

theorem Finsupp.erase_of_not_mem_support {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} (haf : a ∉ f.support) : erase a f = f

Alias of Finsupp.erase_of_notMem_support.

theorem Finsupp.erase_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) : erase a 0 = 0

theorem Finsupp.erase_eq_update_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) : erase a f = f.update a 0

theorem Finsupp.erase_update_of_ne {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) {a a' : α} (ha : a ≠ a') (b : M) : erase a (f.update a' b) = (erase a f).update a' b

theorem Finsupp.erase_idem {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) : erase a (erase a f) = erase a f

@[simp]

theorem Finsupp.update_erase_eq_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) : (erase a f).update a b = f.update a b

@[simp]

theorem Finsupp.erase_update_eq_erase {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) : erase a (f.update a b) = erase a f

Declarations about mapRange

@[simp]

theorem Finsupp.mapRange_single {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : M → N} {hf : f 0 = 0} {a : α} {b : M} : mapRange f hf (single a b) = single a (f b)

Declarations about embDomain

theorem Finsupp.single_of_embDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (l : α →₀ M) (f : α ↪ β) (a : β) (b : M) (hb : b ≠ 0) (h : embDomain f l = single a b) : ∃ (x : α), l = single x b ∧ f x = a

@[simp]

theorem Finsupp.embDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) (a : α) (m : M) : embDomain f (single a m) = single (f a) m

Declarations about zipWith

@[simp]

theorem Finsupp.zipWith_single_single {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : M → N → P) (hf : f 0 0 = 0) (a : α) (m : M) (n : N) : zipWith f hf (single a m) (single a n) = single a (f m n)

Additive monoid structure on α →₀ M

@[simp]

theorem Finsupp.single_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (b₁ b₂ : M) : single a (b₁ + b₂) = single a b₁ + single a b₂

theorem Finsupp.support_single_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] {a : α} {b : M} {f : α →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) : (single a b + f).support = Finset.cons a f.support ha

theorem Finsupp.support_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] {a : α} {b : M} {f : α →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) : (f + single a b).support = Finset.cons a f.support ha

theorem AddEquiv.finsuppUnique_symm {M : Type u_13} [AddZeroClass M] (d : M) : finsuppUnique.symm d = Finsupp.single () d

def Finsupp.singleAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) : M →+ α →₀ M

Finsupp.single as an AddMonoidHom.

See Finsupp.lsingle in Mathlib/LinearAlgebra/Finsupp/Defs.lean for the stronger version as a linear map.

Equations

• Finsupp.singleAddHom a = { toFun := Finsupp.single a, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.singleAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (b : M) : (singleAddHom a) b = single a b

theorem Finsupp.update_eq_single_add_erase {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) : f.update a b = single a b + erase a f

theorem Finsupp.update_eq_erase_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) : f.update a b = erase a f + single a b

theorem Finsupp.single_add_erase {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) : single a (f a) + erase a f = f

theorem Finsupp.erase_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) : erase a f + single a (f a) = f

@[simp]

theorem Finsupp.erase_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f f' : α →₀ M) : erase a (f + f') = erase a f + erase a f'

def Finsupp.eraseAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) : (α →₀ M) →+ α →₀ M

Finsupp.erase as an AddMonoidHom.

Equations

• Finsupp.eraseAddHom a = { toFun := Finsupp.erase a, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.eraseAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) : (eraseAddHom a) f = erase a f

theorem Finsupp.induction {α : Type u_1} {M : Type u_5} [AddZeroClass M] {motive : (α →₀ M) → Prop} (f : α →₀ M) (zero : motive 0) (single_add : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)) : motive f

theorem Finsupp.induction₂ {α : Type u_1} {M : Type u_5} [AddZeroClass M] {motive : (α →₀ M) → Prop} (f : α →₀ M) (zero : motive 0) (add_single : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)) : motive f

theorem Finsupp.induction_linear {α : Type u_1} {M : Type u_5} [AddZeroClass M] {motive : (α →₀ M) → Prop} (f : α →₀ M) (zero : motive 0) (add : ∀ (f g : α →₀ M), motive f → motive g → motive (f + g)) (single : ∀ (a : α) (b : M), motive (single a b)) : motive f

theorem Finsupp.induction_on_max {α : Type u_1} {M : Type u_5} [AddZeroClass M] [LinearOrder α] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (single a b + f)) : p f

A finitely supported function can be built by adding up single a b for increasing a.

The theorem induction_on_max₂ swaps the argument order in the sum.

theorem Finsupp.induction_on_min {α : Type u_1} {M : Type u_5} [AddZeroClass M] [LinearOrder α] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (single a b + f)) : p f

A finitely supported function can be built by adding up single a b for decreasing a.

The theorem induction_on_min₂ swaps the argument order in the sum.

theorem Finsupp.induction_on_max₂ {α : Type u_1} {M : Type u_5} [AddZeroClass M] [LinearOrder α] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)) : p f

A finitely supported function can be built by adding up single a b for increasing a.

The theorem induction_on_max swaps the argument order in the sum.

theorem Finsupp.induction_on_min₂ {α : Type u_1} {M : Type u_5} [AddZeroClass M] [LinearOrder α] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (f + single a b)) : p f

A finitely supported function can be built by adding up single a b for decreasing a.

The theorem induction_on_min swaps the argument order in the sum.

theorem Finsupp.single_add_single_eq_single_add_single {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {k l m n : α} {u v : M} (hu : u ≠ 0) (hv : v ≠ 0) : single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

theorem Finsupp.erase_eq_sub_single {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) (a : α) : erase a f = f - single a (f a)

theorem Finsupp.update_eq_sub_add_single {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) (a : α) (b : G) : f.update a b = f - single a (f a) + single a b

@[simp]

theorem Finsupp.single_neg {α : Type u_1} {G : Type u_9} [AddGroup G] (a : α) (b : G) : single a (-b) = -single a b

@[simp]

theorem Finsupp.single_sub {α : Type u_1} {G : Type u_9} [AddGroup G] (a : α) (b₁ b₂ : G) : single a (b₁ - b₂) = single a b₁ - single a b₂

@[simp]

theorem Finsupp.erase_neg {α : Type u_1} {G : Type u_9} [AddGroup G] (a : α) (f : α →₀ G) : erase a (-f) = -erase a f

@[simp]

theorem Finsupp.erase_sub {α : Type u_1} {G : Type u_9} [AddGroup G] (a : α) (f₁ f₂ : α →₀ G) : erase a (f₁ - f₂) = erase a f₁ - erase a f₂