Modifying skew monoid algebra at exactly one point

This file contains basic results on updating/erasing an element of a skew monoid algebra using one point of the domain.

noncomputable def SkewMonoidAlgebra.erase {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) : SkewMonoidAlgebra M α →+ SkewMonoidAlgebra M α

Given an element f of a skew monoid algebra, erase a f is an element with the same coefficients as f except at a where the coefficient is 0. If a is not in the support of f then erase a f = f.

Equations

• SkewMonoidAlgebra.erase a = { toFun := fun (f : SkewMonoidAlgebra M α) => { coeff := Finsupp.erase a f.coeff }, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem SkewMonoidAlgebra.coeff_erase_apply {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α) : ((erase a) f).coeff = Finsupp.erase a f.coeff

@[deprecated SkewMonoidAlgebra.coeff_erase_apply (since := "2026-07-04")]

theorem SkewMonoidAlgebra.erase_apply_toFinsupp {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α) : ((erase a) f).coeff = Finsupp.erase a f.coeff

Alias of SkewMonoidAlgebra.coeff_erase_apply.

@[simp]

theorem SkewMonoidAlgebra.support_erase {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α) [DecidableEq α] : ((erase a) f).support = f.support.erase a

@[deprecated Finsupp.erase_same (since := "2026-07-04")]

theorem SkewMonoidAlgebra.coeff_erase_same {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α) : ((erase a) f).coeff a = 0

@[deprecated Finsupp.erase_ne (since := "2026-07-04")]

theorem SkewMonoidAlgebra.coeff_erase_ne {M : Type u_4} {α : Type u_5} [AddCommMonoid M] {a a' : α} (f : SkewMonoidAlgebra M α) (h : a' ≠ a) : ((erase a) f).coeff a' = f.coeff a'

@[simp]

theorem SkewMonoidAlgebra.erase_single {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) (b : M) : (erase a) (single a b) = 0

theorem SkewMonoidAlgebra.single_add_erase {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α) : single a (f.coeff a) + (erase a) f = f

theorem SkewMonoidAlgebra.induction {M : Type u_4} {α : Type u_5} [AddCommMonoid M] {p : SkewMonoidAlgebra M α → Prop} (f : SkewMonoidAlgebra M α) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)) : p f

noncomputable def SkewMonoidAlgebra.update {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M) : SkewMonoidAlgebra M α

Replace the coefficient of an element f of a skew monoid algebra at a given point a : α by a given value b : M. If b = 0, this amounts to removing a from the support of f. Otherwise, if a was not in the support of f, it is added to it.

Equations

• f.update a b = { coeff := f.coeff.update a b }

@[simp]

theorem SkewMonoidAlgebra.coeff_update {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M) : (f.update a b).coeff = f.coeff.update a b

@[deprecated SkewMonoidAlgebra.coeff_update (since := "2026-07-04")]

theorem SkewMonoidAlgebra.update_toFinsupp {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M) : (f.update a b).coeff = f.coeff.update a b

Alias of SkewMonoidAlgebra.coeff_update.

@[simp]

theorem SkewMonoidAlgebra.update_self {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) : f.update a (f.coeff a) = f

@[simp]

theorem SkewMonoidAlgebra.zero_update {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) (b : M) : update 0 a b = single a b

theorem SkewMonoidAlgebra.support_update {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra 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

@[deprecated Finsupp.update_apply (since := "2026-07-04")]

theorem SkewMonoidAlgebra.coeff_update_apply {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a a' : α) (b : M) [DecidableEq α] : (f.update a b).coeff a' = if a' = a then b else f.coeff a'

@[deprecated Finsupp.update_apply (since := "2026-07-04")]

theorem SkewMonoidAlgebra.coeff_update_same {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M) : (f.update a b).coeff a = b

@[deprecated Finsupp.update_apply (since := "2026-07-04")]

theorem SkewMonoidAlgebra.coeff_update_ne {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) {a a' : α} (b : M) (h : a' ≠ a) : (f.update a b).coeff a' = f.coeff a'

theorem SkewMonoidAlgebra.update_eq_erase_add_single {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M) : f.update a b = (erase a) f + single a b

@[simp]

theorem SkewMonoidAlgebra.update_zero_eq_erase {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) : f.update a 0 = (erase a) f