fin (n + m) → fin n ⊕ fin m

Stream: Is there code for X?

[Eric Wieser]

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]

docs#sum_fin_sum_equiv

[Eric Wieser]

Was not expecting it to be in a different file

[Eric Wieser]

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]

In that case you might be interested in #4406

[Eric Wieser]

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]

latex debugging output nonexistent :-(

[Reid Barton]

(deleted)

[Reid Barton]

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]

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]

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

[Reid Barton]

I think you still need something to fix the overall sign

[Eric Wieser]

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]

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]

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

[Adam Topaz]

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]

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.