# 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_setOf_eq_single`: `Finsupp` is generated by all the `single`s
- `Finsupp.addHom_ext`: additive homomorphisms that are equal on each `single` are equal everywhere

source
@[simp]
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} = ⊤
source
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.

source
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 `AddMonoidHom`s 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)`.

source
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)
source
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
source
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
source
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))