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

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

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

(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

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 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: Dec 20 2023 at 11:08 UTC