Zulip Chat Archive

Stream: Is there code for X?

Topic: Summing over `monoid_hom.range`


view this post on Zulip Eric Wieser (Jan 08 2021 at 15:34):

I managed to stumble into this proof, but if feels super awkward for something so obvious:

@[to_additive]
lemma finset.prod_filter_univ_exists_eq {α β γ : Type*}
  [fintype α] [fintype β] [comm_monoid γ]
  (f : α  β) (h : function.injective f) {_ : decidable_pred (λ (b : β),  a, f a = b)} (g : β  γ) :
   x in finset.filter (λ (b : β),  a, f a = b) finset.univ, g x =  a, g (f a) :=
begin
  rw finset.prod_subtype (λ x, show x  _   a, x = f a, from _),
  rotate, apply_instance, { simp only [finset.mem_filter, finset.mem_univ, true_and] },
  symmetry,
  apply finset.prod_bij
    (λ a ha, (⟨f a, a, rfl : {x //  (a : α), x = f a}))
    (λ a ha, finset.mem_univ _)
    (λ a ha, _)
    (λ a₁ a₂ ha₁ ha₂ heq, h (subtype.ext_iff.mp heq))
    (λ b hb, let a, hb := b.prop in a, finset.mem_univ _, subtype.ext (by convert hb)⟩),
  refl,
end

lemma finset.sum_filter_univ_mem_monoid_hom_range {α β γ : Type*}
  [fintype α] [fintype β]
    [group α] [group β] [add_comm_monoid γ]
  (f : α →* β) (h : function.injective f) {_ : decidable_pred (λ (b : β), b  f.range)} (g : β  γ) :
   x in finset.filter (λ (b : β), b  f.range) finset.univ, g x =  a, g (f a) :=
begin
  exact finset.sum_filter_univ_exists_eq f h g,
end

Am I missing some lemmas that do most of the lifting for me?

view this post on Zulip Eric Wieser (Jan 08 2021 at 15:35):

Part of the problem seems to be the lack of a finset version of set.range (docs#finset.range is something completely different)

view this post on Zulip Eric Wieser (Jan 08 2021 at 16:37):

Aha!

lemma finset.filter_mem_range_univ {α β : Type*}
  [fintype α] [fintype β] [decidable_eq β]
  (f : α  β) {_ : decidable_pred (λ (b : β), b  set.range f)} :
  finset.filter (λ (b : β), b  set.range f) finset.univ = finset.image f finset.univ :=
by { ext, simp }

@[to_additive]
lemma finset.prod_filter_univ_exists_eq {α β γ : Type*}
  [fintype α] [fintype β] [comm_monoid γ]
  (f : α  β) (h : function.injective f) {_ : decidable_pred (λ (b : β),  a, f a = b)} (g : β  γ) :
   x in finset.filter (λ (b : β),  a, f a = b) finset.univ, g x =  a, g (f a) :=
begin
  classical,
  rw finset.prod_image (λ x _ y _ (z : f x = f y), h z),
  refine finset.prod_congr (finset.filter_mem_range_univ f) (λ _ _, rfl),
end

Are these names sensible enough for inclusion in mathlib?

view this post on Zulip Eric Wieser (Jan 12 2021 at 12:37):

#5708 adds the first one under a better name

view this post on Zulip Kyle Miller (Jan 12 2021 at 20:14):

I usually use finset.univ.image f. Your very first lemma ends up basically being finset.prod_image in algebra.big_operators.basic:

lemma finset.prod_filter_univ_exists_eq {α β γ : Type*}
  [fintype α] [fintype β] [comm_monoid γ]
  (f : α  β) (h : function.injective f) {_ : decidable_pred (λ (b : β),  a, f a = b)} (g : β  γ) :
   x in finset.univ.filter (λ (b : β),  a, f a = b), g x =  a, g (f a) :=
begin
  haveI : decidable_eq β := by { classical, apply_instance },
  have him : finset.univ.filter (λ (b : β),  a, f a = b) = finset.univ.image f,
  { ext, simp, },
  rw him,
  apply finset.prod_image,
  simp,
  apply h,
end

view this post on Zulip Kyle Miller (Jan 12 2021 at 20:16):

Oh, missed that that was from Jan 8 (and I appear to have only read the first message).

view this post on Zulip Eric Wieser (Jan 12 2021 at 20:21):

Right, your him is roughly the lemma I PR'd


Last updated: May 07 2021 at 22:14 UTC