DirectSum.of

Stream: Is there code for X?

[Madison Crim]

I have a finite direct sum of a direct product and I'm trying to show I can reconstruct it's elements from the DirectSum.of construction. Can someone please help?

import Mathlib

open DirectSum

example {ι' : Type*} {ι : Type*} {N : ι → ι' → Type*}
  [inst : (i : ι) → (i' : ι') → AddCommGroup (N i i')]
  [inst_1 : Fintype ι'] [inst_2 : DecidableEq ι']
  (nm : ⨁ (i' : ι'), (i : ι) → N i i') (j : ι')  (i : ι) :
  (∑ x : ι', (of (fun i' ↦ N i i') x) (nm x i)) j = nm j i :=
sorry

[Andrew Yang]

The key is probably docs#DirectSum.sum_univ_of. But the goal seems very strange to me. In particular nm is of type $\bigoplus_{i'} \prod_{i} N_{i, i'}$ and not $\bigoplus_{i', i} N_{i, i'}$

Solution

example {ι' : Type*} {ι : Type*} {N : ι → ι' → Type*}
  [inst : (i : ι) → (i' : ι') → AddCommGroup (N i i')]
  [inst_1 : Fintype ι'] [inst_2 : DecidableEq ι']
  (nm : ⨁ (i' : ι'), (i : ι) → N i i') (j : ι')  (i : ι) :
  (∑ x : ι', (of (fun i' ↦ N i i') x) (nm x i)) j = nm j i := by
  conv_rhs => rw [← DirectSum.sum_univ_of nm]
  rw [DFinsupp.finset_sum_apply, DFinsupp.finset_sum_apply, Finset.sum_apply]
  congr with k
  by_cases h : k = j
  · subst h; simp
  · simp [of_eq_of_ne _ _ _ h]