Extensionality for maps on Finsupp

This file contains some extensionality principles for maps on Finsupp. These have been moved to their own file to avoid depending on submonoids when defining Finsupp.

Main results

• Finsupp.add_closure_setOfPred_eq_single: Finsupp is generated by all the singles
• Finsupp.addHom_ext: additive homomorphisms that are equal on each single are equal everywhere

@[simp]

theorem Finsupp.add_closure_setOfPred_eq_single {α : Type u_1} {M : Type u_2} [AddZeroClass M] : AddSubmonoid.closure {f : α →₀ M | ∃ (a : α) (b : M), f = single a b} = ⊤

@[deprecated Finsupp.add_closure_setOfPred_eq_single (since := "2026-07-09")]

theorem Finsupp.add_closure_setOf_eq_single {α : Type u_1} {M : Type u_2} [AddZeroClass M] : AddSubmonoid.closure {f : α →₀ M | ∃ (a : α) (b : M), f = single a b} = ⊤

Alias of Finsupp.add_closure_setOfPred_eq_single.

theorem Finsupp.addHom_ext {α : Type u_1} {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄ (H : ∀ (x : α) (y : M), f (single x y) = g (single x y)) : f = g

If two additive homomorphisms from α →₀ M are equal on each single a b, then they are equal.

theorem Finsupp.addHom_ext' {α : Type u_1} {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄ (H : ∀ (x : α), f.comp (singleAddHom x) = g.comp (singleAddHom x)) : f = g

If two additive homomorphisms from α →₀ M are equal on each single a b, then they are equal.

We formulate this using equality of AddMonoidHoms so that ext tactic can apply a type-specific extensionality lemma after this one. E.g., if the fiber M is ℕ or ℤ, then it suffices to verify f (single a 1) = g (single a 1).

theorem Finsupp.addHom_ext'_iff {α : Type u_1} {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] {f g : (α →₀ M) →+ N} : f = g ↔ ∀ (x : α), f.comp (singleAddHom x) = g.comp (singleAddHom x)

theorem Finsupp.mulHom_ext {α : Type u_1} {M : Type u_2} {N : Type u_3} [AddZeroClass M] [MulOneClass N] ⦃f g : Multiplicative (α →₀ M) →* N⦄ (H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))) : f = g

theorem Finsupp.mulHom_ext' {α : Type u_1} {M : Type u_2} {N : Type u_3} [AddZeroClass M] [MulOneClass N] {f g : Multiplicative (α →₀ M) →* N} (H : ∀ (x : α), f.comp (AddMonoidHom.toMultiplicative (singleAddHom x)) = g.comp (AddMonoidHom.toMultiplicative (singleAddHom x))) : f = g

theorem Finsupp.mulHom_ext'_iff {α : Type u_1} {M : Type u_2} {N : Type u_3} [AddZeroClass M] [MulOneClass N] {f g : Multiplicative (α →₀ M) →* N} : f = g ↔ ∀ (x : α), f.comp (AddMonoidHom.toMultiplicative (singleAddHom x)) = g.comp (AddMonoidHom.toMultiplicative (singleAddHom x))