Summing over `monoid_hom.range`

Stream: Is there code for X?

[Eric Wieser]

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?

[Eric Wieser]

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

[Eric Wieser]

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?

[Eric Wieser]

#5708 adds the first one under a better name

[Kyle Miller]

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

[Kyle Miller]

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

[Eric Wieser]

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