Mathlib.Data.Finsupp.Ext

Module docstring

{"# 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 singles
Finsupp.addHom_ext: additive homomorphisms that are equal on each single are equal everywhere "}

Finsupp.add_closure_setOf_eq_single theorem

: AddSubmonoid.closure {f : α →₀ M | ∃ a b, f = single a b} = ⊤

Full source

@[simp]
theorem add_closure_setOf_eq_single :
    AddSubmonoid.closure { f : α →₀ M | ∃ a b, f = single a b } = ⊤ :=
  top_unique fun x _hx =>
    Finsupp.induction x (AddSubmonoid.zero_mem _) fun a b _f _ha _hb hf =>
      AddSubmonoid.add_mem _ (AddSubmonoid.subset_closure <| ⟨a, b, rfl⟩) hf

Generation of Finitely Supported Functions by Single Functions

Informal description

The additive submonoid generated by the set of all finitely supported functions of the form `single a b` (where `a : α` and `b : M`) is equal to the entire space of finitely supported functions `α →₀ M`.

Finsupp.addHom_ext theorem

[AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄ (H : ∀ x y, f (single x y) = g (single x y)) : f = g

Full source

/-- If two additive homomorphisms from `α →₀ M` are equal on each `single a b`,
then they are equal. -/
theorem addHom_ext [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄
    (H : ∀ x y, f (single x y) = g (single x y)) : f = g := by
  refine AddMonoidHom.eq_of_eqOn_denseM add_closure_setOf_eq_single ?_
  rintro _ ⟨x, y, rfl⟩
  apply H

Extensionality of Additive Homomorphisms on Finitely Supported Functions

Informal description

Let $N$ be an add-zero class, and let $f, g \colon (\alpha \to_{\text{f}} M) \to^+ N$ be two additive homomorphisms from the space of finitely supported functions $\alpha \to_{\text{f}} M$ to $N$. If $f$ and $g$ agree on all functions of the form $\text{single}(x, y)$ for $x \in \alpha$ and $y \in M$, then $f = g$.

Finsupp.addHom_ext' theorem

 [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄ (H : ∀ x, f.comp (singleAddHom x) = g.comp (singleAddHom x)) : f = g

Full source

/-- 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)`. -/
@[ext high]
theorem addHom_ext' [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄
    (H : ∀ x, f.comp (singleAddHom x) = g.comp (singleAddHom x)) : f = g :=
  addHom_ext fun x => DFunLike.congr_fun (H x)

Extensionality of Additive Homomorphisms via Composition with Single Functions

Informal description

Let $N$ be an add-zero class, and let $f, g \colon (\alpha \to_{\text{f}} M) \to^+ N$ be two additive homomorphisms from the space of finitely supported functions $\alpha \to_{\text{f}} M$ to $N$. If for every $x \in \alpha$, the compositions $f \circ \text{singleAddHom}(x)$ and $g \circ \text{singleAddHom}(x)$ are equal, then $f = g$.

Finsupp.mulHom_ext theorem

 [MulOneClass N] ⦃f g : Multiplicative (α →₀ M) →* N⦄
  (H : ∀ x y, f (Multiplicative.ofAdd <| single x y) = g (Multiplicative.ofAdd <| single x y)) : f = g

Full source

theorem mulHom_ext [MulOneClass N] ⦃f g : MultiplicativeMultiplicative (α →₀ M) →* N⦄
    (H : ∀ x y, f (Multiplicative.ofAdd <| single x y) = g (Multiplicative.ofAdd <| single x y)) :
    f = g :=
  MonoidHom.ext <|
    DFunLike.congr_fun <| by
      have := @addHom_ext α M (Additive N) _ _
        (MonoidHom.toAdditive'' f) (MonoidHom.toAdditive'' g) H
      ext
      rw [DFunLike.ext_iff] at this
      apply this

Extensionality of Multiplicative Homomorphisms on Finitely Supported Functions

Informal description

Let $N$ be a multiplicative monoid, and let $f, g \colon \text{Multiplicative}(\alpha \to_{\text{f}} M) \to^* N$ be two multiplicative homomorphisms from the multiplicative version of the space of finitely supported functions $\alpha \to_{\text{f}} M$ to $N$. If $f$ and $g$ agree on all elements of the form $\text{Multiplicative.ofAdd}(\text{single}(x, y))$ for $x \in \alpha$ and $y \in M$, then $f = g$.

Finsupp.mulHom_ext' theorem

 [MulOneClass N] {f g : Multiplicative (α →₀ M) →* N}
  (H :
    ∀ x,
      f.comp (AddMonoidHom.toMultiplicative (singleAddHom x)) =
        g.comp (AddMonoidHom.toMultiplicative (singleAddHom x))) :
  f = g

Full source

@[ext]
theorem mulHom_ext' [MulOneClass N] {f g : MultiplicativeMultiplicative (α →₀ M) →* N}
    (H : ∀ x, f.comp (AddMonoidHom.toMultiplicative (singleAddHom x)) =
              g.comp (AddMonoidHom.toMultiplicative (singleAddHom x))) :
    f = g :=
  mulHom_ext fun x => DFunLike.congr_fun (H x)

Extensionality of Multiplicative Homomorphisms via Single Function Compositions

Informal description

Let $N$ be a multiplicative monoid, and let $f, g \colon \text{Multiplicative}(\alpha \to_{\text{f}} M) \to^* N$ be two multiplicative homomorphisms. If for every $x \in \alpha$, the compositions of $f$ and $g$ with the multiplicative version of the single function homomorphism $\text{singleAddHom}(x)$ are equal, then $f = g$.