Mathlib.Data.DFinsupp.Ext

Module docstring

{"# Extensionality principles for DFinsupp

Main results

DFinsupp.addHom_ext, DFinsupp.addHom_ext': if two additive homomorphisms from Π₀ i, β i are equal on each single a b, then they are equal. "}

DFinsupp.add_closure_iUnion_range_single theorem

: AddSubmonoid.closure (⋃ i : ι, Set.range (single i : β i → Π₀ i, β i)) = ⊤

Full source

@[simp]
theorem add_closure_iUnion_range_single :
    AddSubmonoid.closure (⋃ i : ι, Set.range (single i : β i → Π₀ i, β i)) = ⊤ :=
  top_unique fun x _ => by
    apply DFinsupp.induction x
    · exact AddSubmonoid.zero_mem _
    exact fun a b f _ _ hf =>
      AddSubmonoid.add_mem _
        (AddSubmonoid.subset_closure <| Set.mem_iUnion.2 ⟨a, Set.mem_range_self _⟩) hf

Additive Generation by Single Functions in Dependent Functions with Finite Support

Informal description

The additive submonoid generated by the union of the ranges of the single functions `single i : β i → Π₀ i, β i` for all indices `i` is equal to the entire space of dependent functions with finite support. In other words, every function in `Π₀ i, β i` can be expressed as a finite sum of single functions `single i b` for various indices `i` and elements `b ∈ β i`.

DFinsupp.addHom_ext theorem

 {γ : Type w} [AddZeroClass γ] ⦃f g : (Π₀ i, β i) →+ γ⦄ (H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)) :
  f = g

Full source

/-- If two additive homomorphisms from `Π₀ i, β i` are equal on each `single a b`, then
they are equal. -/
theorem addHom_ext {γ : Type w} [AddZeroClass γ] ⦃f g : (Π₀ i, β i) →+ γ⦄
    (H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)) : f = g := by
  refine AddMonoidHom.eq_of_eqOn_denseM add_closure_iUnion_range_single fun f hf => ?_
  simp only [Set.mem_iUnion, Set.mem_range] at hf
  rcases hf with ⟨x, y, rfl⟩
  apply H

Extensionality of Additive Homomorphisms on Dependent Functions with Finite Support

Informal description

Let $\gamma$ be an additive zero class, and let $f, g \colon (\Pi_{i} \beta_i) \to^+ \gamma$ be two additive homomorphisms from the dependent functions with finite support to $\gamma$. If for every index $i$ and every element $y \in \beta_i$, the equality $f(\text{single}_i(y)) = g(\text{single}_i(y))$ holds, then $f = g$. Here, $\text{single}_i(y)$ denotes the dependent function that maps $i$ to $y$ and all other indices to $0$.

DFinsupp.addHom_ext' theorem

 {γ : Type w} [AddZeroClass γ] ⦃f g : (Π₀ i, β i) →+ γ⦄
  (H : ∀ x, f.comp (singleAddHom β x) = g.comp (singleAddHom β x)) : f = g

Full source

/-- If two additive homomorphisms from `Π₀ i, β i` are equal on each `single a b`, then
they are equal.

See note [partially-applied ext lemmas]. -/
@[ext]
theorem addHom_ext' {γ : Type w} [AddZeroClass γ] ⦃f g : (Π₀ i, β i) →+ γ⦄
    (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 $\gamma$ be an additive zero class, and let $f, g \colon (\Pi_{i} \beta_i) \to^+ \gamma$ be two additive homomorphisms from the dependent functions with finite support to $\gamma$. If for every index $i$, the compositions $f \circ \text{singleAddHom}_i$ and $g \circ \text{singleAddHom}_i$ are equal, then $f = g$. Here, $\text{singleAddHom}_i \colon \beta_i \to^+ \Pi_{i} \beta_i$ is the additive homomorphism that maps $b \in \beta_i$ to the function $\text{single}_i(b)$ which is zero everywhere except at index $i$ where it takes the value $b$.