finsupp from input/output pairs

Stream: Is there code for X?

[Violeta Hernández]

Do we happen to have code for the obvious map from list (α × β) to α →₀ β? I need it in a certain cardinality proof

[Violeta Hernández]

(yeah, I'm aware that there's subtleties with duplicate entries and such, I just want a surjective function like this)

[Violeta Hernández]

Actually, now that I recall, I actually want to use this exact same function elsewhere in the code

[Kevin Buzzard]

What is the obvious map?? What does it take [(a,b1),(a,b2)] to? What does it take [(a,0),(a,b)] to?

[Violeta Hernández]

I really just need any implementation of this concept that's surjective for my proof to work

[Violeta Hernández]

The obvious (?) implementation would be

noncomputable def finsupp_of_pairs : list (α × M) → α →₀ M
| []       := 0
| (c :: l) := (finsupp_of_pairs l).update c.1 c.2

which would give answers b1 and 0 to your questions, though of course it could be defined differently

[Kevin Buzzard]

There's what looks to me like an obvious injective map from the finsupp to finset (alpha x beta) which might be more natural. And then there's a surjection from list to finset and you can split the injection.

[Violeta Hernández]

Oh you're right

[Violeta Hernández]

The injection probably suits me better

[Violeta Hernández]

Guess this was just an #xy

[Violeta Hernández]

I guess I now have to change the question

[Violeta Hernández]

Is there code to get the "graph" of a finsupp as a finset?

[Violeta Hernández]

Or however you'd call the finset of input and output pairs

[Yakov Pechersky]

variables {α β : Type*} [has_zero β] (f : α →₀ β)

def graph [decidable_eq (α × β)] : finset (α × β) :=
f.support.image (λ a, (a, f a))

[Violeta Hernández]

It's certainly easy enough to code

[Violeta Hernández]

We can ditch decidable equality, actually

def graph (f : α →₀ M) : finset (α × M) :=
f.support.map ⟨λ a, prod.mk a (f a), λ x y h, (prod.mk.inj h).1⟩

[Yakov Pechersky]

Better:

variables {α β : Type*} [has_zero β] (f : α →₀ β)

def prod.graph (f : α → β) : α ↪ (α × β) :=
{ to_fun := λ a, (a, f a),
  inj' := λ _ _, by simp {contextual := tt} }

@[simp] lemma prod.graph_apply (f : α → β) (a : α) : prod.graph f a = (a, f a) := rfl

def graph : finset (α × β) :=
f.support.map (prod.graph f)

[Yakov Pechersky]

Ah, you just did that too.

[Violeta Hernández]

#15196

[Eric Wieser]

Is there a link to docs#linear_pmap.graph or linear_map.graph here?

[Eric Wieser]

Violeta, did you mean to link to one of your own PRs instead of that one?

[Violeta Hernández]

Oops, off by one error