finsupp.pi

Stream: Is there code for X?

[Yaël Dillies]

Do we have anything close to a finset.pi-like definition for finsupp? Here's how far I got

import data.finsupp.basic

open finset
open_locale pointwise

variables {ι α : Type*}

namespace finsupp
variables [decidable_eq ι] [has_zero α]

/-- Given a finitely supported function `f : ι →₀ finset α`, one can define the finset
`f.pi` of all finitely supported functions whose value at `i` is in `f i` for all `i`. -/
def pi (f : ι →₀ finset α) : finset (ι →₀ α) :=
begin
  refine (f.support.pi (λ i, f i)).preimage (λ g i _, g i) (λ a ha b hb h, _),
  rw [set.mem_preimage, mem_coe, mem_pi] at ha hb,
  ext i,
  by_cases hi : i ∈ f.support,
  { convert _root_.congr_fun (_root_.congr_fun h i) hi },
  {

  }
end

end finsupp

[Kevin Buzzard]

Wait a second -- if iota is infinite then for some i you have f i = empty (assuming 0=bot) so the set you're considering is also empty. Is that what you mean?

[Yaël Dillies]

Yes

[Yaël Dillies]

Wait, no, you're misunderstanding docs#finset.has_zero.

[Yaël Dillies]

0 : finset α is not the empty set, but {0}. By what seems to me like a lucky coincidence, linear algebra forced upon us a definition of 0 : finset α which is precisely the one I want in this seemingly unrelated context.

[Eric Wieser]

I think that should be called finset.finsupp not finsupp.pi

[Eric Wieser]

Because what you're doing is replacing the A → B (pi) in finset.pi with A →₀ B (finsupp)

[Yaël Dillies]

But... dot notation

[Eric Wieser]

You could rename finset.pi to pi.finset to keep dot notation as finsupp.finset

[Yaël Dillies]

Anyway, the sorried goal is false. Do you have any idea how to fix this?

[Eric Wieser]

I see no sorry ;)

[Yaël Dillies]

Okay, I have excused myself now.

[Eric Wieser]

Can you add the statement of mem_pi that you want? x ∈ finsupp.pi f ↔ _

[Yaël Dillies]

This is what I want

@[simp] lemma mem_pi {f : ι →₀ finset α} {g : ι →₀ α} : g ∈ f.pi ↔ ∀ i, g i ∈ f i :=

I'm thinking I need finsupp.extend, which apparently doesn't exist?

[Yaël Dillies]

Ahah! finsupp.map_domain is what I want.

[Yaël Dillies]

Sorry, it's me again. I'm still stuck at the same place, but this time with a slightly different definition.

vimport data.finsupp.basic

variables {ι α : Type*}

namespace finset
variables [decidable_eq ι] [decidable_eq α] [has_zero α]

def finsupp (s : finset ι) (t : ι → finset α) : finset (ι →₀ α) :=
(s.pi t).map sorry

@[simp] lemma mem_finsupp {s : finset ι} {t : ι → finset α} {f : ι →₀ α} :
  f ∈ s.finsupp t ↔ ∀ i ∈ s, f i ∈ t i :=
sorry

end finset

[Yaël Dillies]

I need the injection (Π (a : ι), a ∈ s → α) ↪ ι →₀ α which adds zeroes outside of s.

[Eric Wieser]

Isn't that docs#finsupp.on_finset?

[Yaël Dillies]

Yeah, that's what I'm figuring out now. I'm working through it.

[Yaël Dillies]

However, it's not quite bundled in the way I want. Do you mind if I refactor finsupp.on_finset to be

def on_finset (s : finset α) (f : ∀ a ∈ s, M) : α →₀ M :=

[Eric Wieser]

Is docs#dfinsupp.mk more similar?

[Yaël Dillies]

Yeah

[Yaël Dillies]

Should I just define finsupp.mk, then? I don't really know much this bit of the library, so it's hard to judge.

[Eric Wieser]

docs#finsupp.mk already exists and is a constructor!

[Yaël Dillies]

Ah of course! How should I name it then?

[Eric Wieser]

I think maybe extend is a good name after all

[Eric Wieser]

Is docs#function.extend similar?

[Eric Wieser]

No...

[Eric Wieser]

docs#set.indicator?

[Yaël Dillies]

Why not finsupp.indicator after all.