Defining Finmaps via Finsets

Stream: Is there code for X?

[Bernhard Reinke]

I want to use Finmaps together with Finsets. I think I want to have a function of the following type:

def helper {α β γ} (g : α -> β) (f : ∀ b : α, γ (g b)) (h_g : Function.Injective g) (s : Finset α)
: Finmap γ

So I have an injective function g : α -> β and some dependent function (f : ∀ b : α, γ (g b)), and I want to use both functions together to define a Finmap that has keys equal to the image of s under g. Is there an easy way to get something like this? The thing that is a little bit tricky is that the way that Finset and Finmap are defined doesn't commute: Finset is a subset of a quotient of lists, whereas Finmap is a quotient of subsets of lists.

[Bernhard Reinke]

In my application, γ is a constant type family, so f : α -> γwould be also fine. I think there is no specialized version for nondependent Finmaps, so I tried to write down the correct general type

[Bernhard Reinke]

I am trying to write something myself, but I got stuck, see here my key issue

[Matt Diamond]

What determines the values of the map? Is the idea that the Finmap has keys equal to g a and values equal to f a for every a in s?

Constructing a Finmap requires assembling a Multiset of the keys & values and then proving there are no duplicate keys. Are you having trouble with constructing the Multiset from your original Finset, or proving nodupKeys?

[Bernhard Reinke]

Ah, I think my problem was that I tried to go via AList and got lost in some Quotient issues.

[Bernhard Reinke]

A direct definition works nicely:

def helper {α β γ} (g : α -> β) (f : ∀ b : α, γ (g b)) (h_g : Function.Injective g) (s : Finset α)
: Finmap γ where
  entries := Multiset.map (fun a => ⟨g a, f a⟩) s.1
  nodupKeys := by
    rw [← Multiset.nodup_keys]
    unfold Multiset.keys
    simp only [Multiset.map_map, Function.comp_apply]
    rw [Multiset.nodup_map_iff_of_injective]
    exact s.2
    exact h_g

What would be a standard name for this?

[Bernhard Reinke]

Hm, actually I also need an inj_on variant of this :)