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:Finsuppis generated by all thesinglesFinsupp.addHom_ext: additive homomorphisms that are equal on eachsingleare equal everywhere
@[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 = Finsupp.single a b} = ⊤
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 (Finsupp.single x y) = g (Finsupp.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 (Finsupp.singleAddHom x) = g.comp (Finsupp.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.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 (Finsupp.single x y)) = g (Multiplicative.ofAdd (Finsupp.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 (Finsupp.singleAddHom x)) = g.comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)))
:
f = g