Documentation

Mathlib.Algebra.SkewMonoidAlgebra.Single

Modifying skew monoid algebra at exactly one point #

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

source
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
Instances For
    source
    @[simp]
    theorem SkewMonoidAlgebra.erase_apply_toFinsupp {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α) :
    ((erase a) f).toFinsupp = Finsupp.erase a f.toFinsupp
    source
    @[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
    source
    @[simp]
    theorem SkewMonoidAlgebra.coeff_erase_same {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α) :
    ((erase a) f).coeff a = 0
    source
    @[simp]
    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'
    source
    @[simp]
    theorem SkewMonoidAlgebra.erase_single {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) (b : M) :
    (erase a) (single a b) = 0
    source
    theorem SkewMonoidAlgebra.coeff_erase_apply {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a a' : α) (f : SkewMonoidAlgebra M α) [DecidableEq α] :
    ((erase a) f).coeff a' = if a' = a then 0 else f.coeff a'
    source
    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
    source
    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
    source
    def SkewMonoidAlgebra.update {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M) :
    SkewMonoidAlgebra M α

    Replace the coefficent 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
    Instances For
      source
      @[simp]
      theorem SkewMonoidAlgebra.update_toFinsupp {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M) :
      (f.update a b).toFinsupp = f.toFinsupp.update a b
      source
      @[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
      source
      @[simp]
      theorem SkewMonoidAlgebra.zero_update {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (a : α) (b : M) :
      update 0 a b = single a b
      source
      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
      source
      theorem SkewMonoidAlgebra.coeff_update {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M) [DecidableEq α] :
      (f.update a b).coeff = Function.update f.coeff a b
      source
      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'
      source
      @[simp]
      theorem SkewMonoidAlgebra.coeff_update_same {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M) [DecidableEq α] :
      (f.update a b).coeff a = b
      source
      @[simp]
      theorem SkewMonoidAlgebra.coeff_update_ne {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) {a a' : α} (b : M) [DecidableEq α] (h : a' ≠ a) :
      (f.update a b).coeff a' = f.coeff a'
      source
      theorem SkewMonoidAlgebra.update_eq_erase_add_single {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M) [DecidableEq α] :
      f.update a b = (erase a) f + single a b
      source
      @[simp]
      theorem SkewMonoidAlgebra.update_zero_eq_erase {M : Type u_4} {α : Type u_5} [AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) [DecidableEq α] :
      f.update a 0 = (erase a) f