Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 25 2020 at 13:00):

docs#sum_fin_sum_equiv

view this post on Zulip Eric Wieser (Nov 25 2020 at 13:02):

Was not expecting it to be in a different file

view this post on Zulip 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`

view this post on Zulip Reid Barton (Nov 25 2020 at 13:08):

In that case you might be interested in #4406

view this post on Zulip Eric Wieser (Nov 25 2020 at 13:20):

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

(fg)(u1,,um+n)=σshuffle(m,n)sign(σ)f(uσ(1),,uσ(m))g(uσ(m+1),,uσ(m+n))(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

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 13:21):

latex debugging output nonexistent :-(

view this post on Zulip Reid Barton (Nov 25 2020 at 13:21):

(deleted)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 25 2020 at 13:42):

I think you still need something to fix the overall sign

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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