Operations on Finsupps with an Option domain

Similar to how Finsupp.cons and Finsupp.tail construct an object of type Fin (n + 1) →₀ M from a map Fin n →₀ M and vice versa, we define Finsupp.optionElim and Finsupp.some to construct Option α →₀ M from a map α →₀ M, and vice versa.

As functions, these behave as Option.elim', and as an application of some hence the names.

We prove a variety of API lemmas, see Mathlib/Data/Finsupp/Fin.lean for comparison.

Main declarations

• Finsupp.some: restrict a finitely supported function on Option α to a finitely supported function on α.
• Finsupp.optionElim: extend a finitely supported function on α to a finitely supported function on Option α, provided a default value for none.

Implementation notes

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

noncomputable def Finsupp.some {α : Type u_1} {M : Type u_2} [Zero M] (f : Option α →₀ M) : α →₀ M

Restrict a finitely supported function on Option α to a finitely supported function on α.

Equations

• f.some = Finsupp.comapDomain some f ⋯

@[simp]

theorem Finsupp.some_apply {α : Type u_1} {M : Type u_2} [Zero M] (f : Option α →₀ M) (a : α) : f.some a = f (Option.some a)

@[simp]

theorem Finsupp.some_zero {α : Type u_1} {M : Type u_2} [Zero M] : some 0 = 0

@[simp]

theorem Finsupp.some_add {α : Type u_1} {M : Type u_2} [AddZeroClass M] (f g : Option α →₀ M) : (f + g).some = f.some + g.some

@[simp]

theorem Finsupp.some_single_none {α : Type u_1} {M : Type u_2} [Zero M] (m : M) : (single none m).some = 0

@[simp]

theorem Finsupp.some_single_some {α : Type u_1} {M : Type u_2} [Zero M] (a : α) (m : M) : (single (Option.some a) m).some = single a m

@[simp]

theorem Finsupp.some_embDomain_some {α : Type u_1} {M : Type u_2} [Zero M] (f : α →₀ M) : (embDomain Function.Embedding.some f).some = f

@[simp]

theorem Finsupp.embDomain_some_none {α : Type u_1} {M : Type u_2} [Zero M] (f : α →₀ M) : (embDomain Function.Embedding.some f) none = 0

@[simp]

theorem Finsupp.embDomain_some_some {α : Type u_1} {M : Type u_2} [Zero M] (f : α →₀ M) (x : α) : (embDomain Function.Embedding.some f) (Option.some x) = f x

@[simp]

theorem Finsupp.some_update_none {α : Type u_1} {M : Type u_2} [Zero M] (f : Option α →₀ M) (a : M) : (f.update none a).some = f.some

noncomputable def Finsupp.optionEquiv {α : Type u_1} {M : Type u_2} [Zero M] : (Option α →₀ M) ≃ M × (α →₀ M)

Finsupps from Option are equivalent to pairs of an element and a Finsupp on the original type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.optionEquiv_apply {α : Type u_1} {M : Type u_2} [Zero M] (P : Option α →₀ M) : optionEquiv P = (P none, P.some)

@[simp]

theorem Finsupp.optionEquiv_symm_apply {α : Type u_1} {M : Type u_2} [Zero M] (P : M × (α →₀ M)) : optionEquiv.symm P = (embDomain Function.Embedding.some P.2).update none P.1

noncomputable def Finsupp.optionElim {α : Type u_1} {M : Type u_2} [Zero M] (y : M) (f : α →₀ M) : Option α →₀ M

Extend a finitely supported function on α to a finitely supported function on Option α, provided a default value for none.

Equations

• Finsupp.optionElim y f = Finsupp.optionEquiv.invFun (y, f)

theorem Finsupp.optionElim_apply_none {α : Type u_1} {M : Type u_2} [Zero M] (y : M) (f : α →₀ M) : (optionElim y f) none = y

theorem Finsupp.optionElim_apply_some {α : Type u_1} {M : Type u_2} [Zero M] (y : M) (f : α →₀ M) (x : α) : (optionElim y f) (Option.some x) = f x

@[simp]

theorem Finsupp.optionElim_apply_eq_elim {α : Type u_1} {M : Type u_2} [Zero M] (y : M) (f : α →₀ M) (a : Option α) : (optionElim y f) a = a.elim y ⇑f

theorem Finsupp.optionElim_eq_elim' {α : Type u_1} {M : Type u_2} [Zero M] (y : M) (f : α →₀ M) (a : Option α) : (optionElim y f) a = Option.elim' y (⇑f) a

@[simp]

theorem Finsupp.some_optionElim {α : Type u_1} {M : Type u_2} [Zero M] (y : M) (f : α →₀ M) : (optionElim y f).some = f

@[simp]

theorem Finsupp.optionElim_some {α : Type u_1} {M : Type u_2} [Zero M] (f : Option α →₀ M) : optionElim (f none) f.some = f

@[simp]

theorem Finsupp.optionElim_zero {α : Type u_1} {M : Type u_2} [Zero M] (y : M) : optionElim y 0 = single none y

theorem Finsupp.optionElim_ne_zero_of_left {α : Type u_1} {M : Type u_2} [Zero M] (y : M) (f : α →₀ M) (h : y ≠ 0) : optionElim y f ≠ 0

theorem Finsupp.optionElim_ne_zero_of_right {α : Type u_1} {M : Type u_2} [Zero M] (y : M) (f : α →₀ M) (h : f ≠ 0) : optionElim y f ≠ 0

theorem Finsupp.optionElim_ne_zero_iff {α : Type u_1} {M : Type u_2} [Zero M] (y : M) (f : α →₀ M) : optionElim y f ≠ 0 ↔ f ≠ 0 ∨ y ≠ 0

theorem Finsupp.eq_option_embedding_update_none_iff {α : Type u_1} {M : Type u_2} [Zero M] {n : Option α →₀ M} {m : α →₀ M} {i : M} : n = (embDomain Function.Embedding.some m).update none i ↔ n none = i ∧ n.some = m

theorem Finsupp.prod_option_index {α : Type u_1} {M : Type u_2} {N : Type u_3} [AddZeroClass M] [CommMonoid N] (f : Option α →₀ M) (b : Option α → M → N) (h_zero : ∀ (o : Option α), b o 0 = 1) (h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂) : f.prod b = b none (f none) * f.some.prod fun (a : α) => b (Option.some a)

theorem Finsupp.sum_option_index {α : Type u_1} {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddCommMonoid N] (f : Option α →₀ M) (b : Option α → M → N) (h_zero : ∀ (o : Option α), b o 0 = 0) (h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ + b o m₂) : f.sum b = b none (f none) + f.some.sum fun (a : α) => b (Option.some a)

theorem Finsupp.sum_option_index_smul {α : Type u_1} {M : Type u_2} {R : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (f : Option α →₀ R) (b : Option α → M) : (f.sum fun (o : Option α) (r : R) => r • b o) = f none • b none + f.some.sum fun (a : α) (r : R) => r • b (Option.some a)

@[simp]

theorem Finsupp.optionElim_add {α : Type u_1} {M : Type u_2} [AddZeroClass M] (a b : α →₀ M) (i j : M) : optionElim (i + j) (a + b) = optionElim i a + optionElim j b