## Stream: Is there code for X?

### Topic: fin (n + m) → fin n ⊕ fin m

#### Eric Wieser (Nov 25 2020 at 12:55):

A naive attempt is:

def fin_split {n m} (f : fin (n + m)) : fin n ⊕ fin m :=
if h : ↑f < n then sum.inl ⟨f, h⟩ else sum.inr (f.sub_nat n (le_of_not_lt h)))


Although this fails because of the difference between fin (n + m) and  fin (m + n), which I haven't yet worked out the right invocation of eq.rec to solve.

#### Reid Barton (Nov 25 2020 at 13:00):

docs#sum_fin_sum_equiv

#### Eric Wieser (Nov 25 2020 at 13:02):

Was not expecting it to be in a different file

#### Eric Wieser (Nov 25 2020 at 13:06):

def sum_split_func {α β γ : Sort*} (f : α ⊕ β → γ) : pprod (α → γ) (β → γ) := by library_search


To un- #xy a bit, I'm trying to define

def finvec_split {n m} {α : Sort*} (f : fin (n + m) → α) : pprod (fin n → α) (fin m → α) := sorry


#### Reid Barton (Nov 25 2020 at 13:08):

In that case you might be interested in #4406

#### Eric Wieser (Nov 25 2020 at 13:20):

To fully un- #xy, I'm trying to implement

$(f \wedge g)(u_1, \dots, u_{m + n}) = \sum_{\sigma \in \operatorname{shuffle}(m, n)} \operatorname{sign}(\sigma) f(u_{\sigma(1)}, \dots, u_{\sigma(m)}) g(u_{\sigma(m+1)}, \dots, u_{\sigma(m+n)})$

which I have little doubt is currently absent from mathlib

#### Kevin Buzzard (Nov 25 2020 at 13:21):

latex debugging output nonexistent :-(

(deleted)

#### Reid Barton (Nov 25 2020 at 13:26):

In that case it might make sense to step back and think about the strategy for proving facts you need about it (associativity?) before getting your hands dirty

#### Reid Barton (Nov 25 2020 at 13:27):

For example, you might want to represent a shuffle by an equiv fin m ⊕ fin n ≃ fin (m + n) which is order-preserving on each of the guys on the left

#### Eric Wieser (Nov 25 2020 at 13:29):

I also wonder whether this generalizes to non-fin types, in the way that docs#perm.sign does

#### Reid Barton (Nov 25 2020 at 13:42):

I think you still need something to fix the overall sign

#### Eric Wieser (Nov 25 2020 at 16:16):

Eric Wieser said:

def sum_split_func {α β γ : Sort*} (f : α ⊕ β → γ) : pprod (α → γ) (β → γ) := ⟨f ∘ sum.inl, f ∘ sum.inr⟩


#### Eric Wieser (Nov 25 2020 at 16:43):

Reid Barton said:

For example, you might want to represent a shuffle by an equiv fin m ⊕ fin n ≃ fin (m + n) which is order-preserving on each of the guys on the left

Which would be {p : fin (m + n) ≃ fin m ⊕ fin r // monotone (p.symm ∘ sum.inr) ∧ monotone (p.symm ∘ sum.inl) } I guess?

#### Adam Topaz (Nov 25 2020 at 16:48):

You can also represent a shuffle by a strictly monotone (hence injective) map fin m \to fin (m+n).

#### Adam Topaz (Nov 25 2020 at 16:49):

But since you want to have easy access to the two inclusions from fin mand fin n, the presentation that Reid mentioned might be better

#### Eric Wieser (Nov 25 2020 at 18:27):

I was able to at least write my definition with

def is_shuffle {m n} (p : fin m ⊕ fin n ≃ fin (m + n)) : Prop := monotone (p ∘ sum.inl) ∧ monotone (p ∘ sum.inr)

instance {m n : ℕ} : decidable_pred (@is_shuffle m n) :=
λ p, by {unfold is_shuffle monotone, apply_instance}

@[derive has_coe_to_fun]
def shuffle (m n) : Type* := {p : fin m ⊕ fin n ≃ fin (m + n) // is_shuffle p }

namespace shuffle
variables {m n : ℕ}

def to_perm (s : shuffle m n) := sum_fin_sum_equiv.symm.trans s.val
instance : has_coe_t (shuffle m n) (equiv.perm \$ fin (m + n)) := ⟨to_perm⟩
instance : fintype (shuffle m n) := subtype.fintype _

end shuffle

def mul_fin {n m} [monoid N] [semimodule ℤ N] (a : alternating_map R M N (fin m)) (b : alternating_map R M N (fin n)) :
alternating_map R M N (fin (m + n)) :=
{ to_fun := λ (v : fin (m + n) → M),
-- definition here
∑ σ : shuffle m n,
(equiv.perm.sign σ.to_perm : ℤ) • (a (v ∘ σ ∘ sum.inl) * b (v ∘ σ ∘ sum.inr)),
map_add' := sorry, map_smul' := sorry, map_eq_args' := sorry }
`

Those first two sorries ought to be trivial but are awkward, and the last one will require some thought.

Last updated: May 07 2021 at 21:10 UTC