Zulip Chat Archive

Stream: Is there code for X?

Topic: sum_sum_elim for fintypes


view this post on Zulip Oliver Nash (Jul 04 2020 at 16:11):

I'd like to use the fintype-flavour version of the result finset.sum_sum_elim and can't seem to find it. Does it already exist?

view this post on Zulip Oliver Nash (Jul 04 2020 at 16:11):

More precisely, what I would like is hidden.sum_sum_elim:

namespace hidden

open_locale classical
open_locale big_operators

lemma sum_sum_elim
  {l m A : Type*} [fintype l] [fintype m] [add_comm_monoid A] (f : l  A) (g : m  A) :
   i, sum.elim f g i = ( i, f i) + ( i, g i) :=
begin
  have : @finset.univ (l  m) _ = finset.image sum.inl finset.univ  finset.image sum.inr finset.univ :=
    by { ext a, rcases a; simp, },
  by rw [finset.sum_sum_elim, this],
end

end hidden

view this post on Zulip Jalex Stark (Jul 04 2020 at 16:13):

i thought the point of proving things for finsets is that you can apply them to fintypes and lean will insert the coercion to univ for you

view this post on Zulip Oliver Nash (Jul 04 2020 at 16:14):

Oh I see, that lines up with my surprise at not finding anything for fintypes. Thank you I'll try to proceed along these lines.

view this post on Zulip Oliver Nash (Jul 04 2020 at 16:18):

I wonder if something like the following is missing:

@[simp] lemma finset.univ_sum_union {l m : Type*} [fintype l] [fintype m] :
  @finset.univ (l  m) _ = finset.image sum.inl finset.univ  finset.image sum.inr finset.univ :=
by { ext a, rcases a; simp, }

since we then have:

example {l m : Type*} [fintype l] [fintype m] (f : l  R) (g : m  R) :
   i, sum.elim f g i = ( i, f i) + ( i, g i) :=
by simp

view this post on Zulip Oliver Nash (Jul 04 2020 at 16:34):

(P.S. I love this newish notation for big_operators.)

view this post on Zulip Johan Commelin (Jul 04 2020 at 16:37):

You're welcome :wink:

view this post on Zulip Jalex Stark (Jul 04 2020 at 16:48):

your finset.univ_sum_union looks good to me

view this post on Zulip Jalex Stark (Jul 04 2020 at 16:51):

i'm not sure what file finset.univ_sum_union goes in, but putting that somewhere and sum_sum_elim in big_operators sounds like a fine PR

view this post on Zulip Oliver Nash (Jul 04 2020 at 17:06):

Great. I’ll either include it with some other changes or else make a mini-PR along the lines you suggest.

view this post on Zulip Chris Hughes (Jul 04 2020 at 18:32):

To make this consistent in style with things like sum_sigma and sum_product it would make sense to define the function taking a finset X and a finset Y and returns the disjoint union as a finset (X \oplus Y)

view this post on Zulip Chris Hughes (Jul 04 2020 at 18:42):

This would provide a nicer way to manipulate sums than using sum_union and providing a disjointness proof.

view this post on Zulip Scott Morrison (Jul 05 2020 at 00:18):

I'm not sure that should be a simp lemma.

view this post on Zulip Oliver Nash (Jul 05 2020 at 16:59):

Scott Morrison said:

I'm not sure that should be a simp lemma.

I agree: if anything, it should simplify in the other direction: the disjoint union of two finset.univs is a single finset.univ!

view this post on Zulip Oliver Nash (Jul 05 2020 at 17:01):

I was just looking to pick up this thread again and I discovered that what I was looking for yesterday in fact _does_ exist. It's called fintype.sum_sum_type.

view this post on Zulip Oliver Nash (Jul 05 2020 at 17:07):

I had just started down the road (which I like) that @Chris Hughes had sketched out, which I interpreted as something like:

variables {α γ : Type*}

def disjoint_union (s : finset α) (t : finset γ) : finset (α  γ) :=
s.image sum.inl  t.image sum.inr

def finset.sum_proj_l (s : finset (α  γ)) : (finset α) := sorry

def finset.sum_proj_r (s : finset (α  γ)) : (finset γ) := sorry

lemma finset.proj_l_disjoint_union (s : finset α) (t : finset γ) :
  s = (disjoint_union s t).sum_proj_l := sorry

lemma finset.proj_r_disjoint_union (s : finset α) (t : finset γ) :
  t = (disjoint_union s t).sum_proj_r := sorry

lemma finset.disjoint_union_proj_lr (s : finset (α  γ)) :
  s = disjoint_union s.sum_proj_l s.sum_proj_r := sorry

def finset.sum_equiv' : finset (α  γ)  (finset α) × (finset γ) := sorry

-- The lemma I originally wanted, so that I could use `finset.sum_sum_elim`:
@[simp] lemma finset.disjoint_union_univ {l m : Type*} [fintype l] [fintype m] :
  disjoint_union finset.univ finset.univ = @finset.univ (l  m) _ :=
by { ext a, rcases a; simp [disjoint_union], }

but having found fintype.sum_sum_type I'm going to park all this, even if the existence of fintype.sum_sum_type does seem a bit inconsistent with the philosophy outlined by @Jalex Stark


Last updated: May 07 2021 at 21:10 UTC