# Zulip Chat Archive

## 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):

#### 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):

How about this one?

```
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 :-(

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

(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:

How about this one?

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

That's docs#equiv.sum_arrow_equiv_prod_arrow

#### 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 m`

and `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