Pushforward of a finmap

Stream: general

[Notification Bot]

A message was moved here from #general > ℕ ≠ ℤ by Heather Macbeth.

[Eric Wieser]

docs#finsupp.map_domain or docs#finsupp.emb_domain?

[Patrick Johnson]

Feels like this useful function is missing from the library:

def finmap.equiv_finset_fun {α : Type*} {F : α → Type*} :
  finmap F ≃ Σ' (s : finset α), Π (x ∈ s), F x

[Sabrina Jewson]

I tried implementing that but ran into a problem: when transforming the finset α, I have no way to generate the proof that x ∈ s. I think the fundamental issue is that when I use quot.lift, while I am perfectly able to generate a proof that x ∈ l for some inner value l, there doesn’t appear to be a way to convert that to an x ∈ s, because l and s are totally unrelated in the type system.

[Sabrina Jewson]

Here was my code:

def finmap.equiv_finset_fun {α : Type*} {F : α → Type*} [decidable_eq α] :
  finmap F ≃ Σ (s : finset α), Π (x ∈ s), F x
:= {
  to_fun := λ map, {
    fst := map.keys,
    snd := λ x x_mem, option.get (finmap.lookup_is_some.mpr x_mem),
  },
  inv_fun := λ pair, {
    entries := pair.fst.val.map (λ key, ⟨key, pair.snd key sorry⟩),
    --                                                     ^^^^^
    --                                        Have to show that key ∈ pair.fst
    nodupkeys := begin
      sorry
    end
  },
  left_inv := sorry,
  right_inv := sorry,
}

[Kevin Buzzard]

multiset.map wants to eat a map defined on all of the domain so perhaps that's not an appropriate thing to use here in your definition of entries.

[Sabrina Jewson]

I did try also to make my own map that gives an elem ∈ s guarantee, but ran into the same problem pretty much:

def list.map_mem {α : Type u} {β : Type v} : Π l : list α, (Π elem ∈ l, β) → list β
| [] mapper := []
| (head :: tail) mapper := mapper head (list.mem_cons_self head tail)
  :: list.map_mem tail (λ elem mem, mapper elem (list.mem_cons_of_mem head mem))

def multiset.map_mem {α : Type u} {β : Type v}
  (s : multiset α) (mapper : Π (elem ∈ s), β) : multiset β
:= quot.lift_on s (λ l : list α, (l.map_mem mapper : multiset β)) (λ l₁ l₂ p, sorry)
--                                          ^^^^^^
-- Type error here: somehow, I need to convert the mapper that accepts `elem ∈ s` into a mapper that
-- accepts `elem ∈ l`.

[Kevin Buzzard]

This works:

    entries := by classical; exact (finset.image (λ (x : pair.1), (⟨x.1, pair.2 _ x.2⟩ : sigma F)) finset.univ).val,--{ σ : sigma F | ∃ (a : α) (ha : a ∈ pair.1), σ.fst = a ∧ σ.snd == pair.2 a ha},

but it assumes decidable equality on sigma F. Another approach would be to prove that the map from pair.1 (promoted to a type, which is what I'm doing here to avoid the problem you're seeing) to sigma F coming from pair.2 is injective and then you can use finset.map and perhaps get computability back if it's important to you.

[Yaël Dillies]

Sabrina Jewson said:

I tried implementing that but ran into a problem: when transforming the finset α, I have no way to generate the proof that x ∈ s.

Does docs#finset.attach help?

[Sabrina Jewson]

Yaël Dillies said:

Sabrina Jewson said:

I tried implementing that but ran into a problem: when transforming the finset α, I have no way to generate the proof that x ∈ s.

Does docs#finset.attach help?

Through that link I was able to discover docs#multiset.pmap which seems to be basically exactly what I want:

entries := pair.1.val.pmap
  (λ (elem : α) (elem_mem : elem ∈ pair.1.val), ⟨elem, pair.2 elem elem_mem⟩)
  (λ elem, id),

Thanks a lot :D! And thanks Kevin too, that’s a really elegant solution.