Zulip Chat Archive

Stream: Is there code for X?

Topic: Disjoint union of fin's


view this post on Zulip Adam Topaz (Jul 09 2020 at 23:37):

Hi everyone. I'm looking for the statement that fin (a + b) is the disjoint union of fin a and fin b, in terms of the universal property of the disjoint union. Specifically, I'm looking for the following definitions and theorems, and I hope mathlib has something similar which I can use:

def inl {a b : } : fin a  fin (a + b) := λ x, x.1, by {cases x, linarith}

def inr {a b : } : fin b  fin (a + b) := λ x, a + x.1, by {cases x, linarith}

def sum {a b : } {T : Type*} (f : fin a  T) (g : fin b  T) : fin (a + b)  T :=
  λ x, if h : x.1 < a then f x.1,h else g x.1 - a, (nat.sub_lt_left_iff_lt_add $ not_lt.mp h).mpr x.2

theorem suml {a b : } {T : Type*} (f : fin a  T) (g : fin b  T) :
  (sum f g)  inl = f := sorry

theorem sumr {a b : } {T : Type*} (f : fin a  T) (g : fin b  T) :
  (sum f g)  inr = g := sorry

theorem sum_unique {a b : } {T : Type*} (f : fin a  T) (g : fin b  T) (h : fin (a + b)  T):
  h  inl = f  h  inr = g  h = sum f g := sorry

view this post on Zulip Scott Morrison (Jul 10 2020 at 00:17):

There is src#sum_fin_sum_equiv

view this post on Zulip Scott Morrison (Jul 10 2020 at 00:18):

Which has an equivalence, although no lemmas saying what the equivalence actually does. :-(

view this post on Zulip Adam Topaz (Jul 10 2020 at 00:21):

That should be good enough! Thanks!

view this post on Zulip Scott Morrison (Jul 10 2020 at 00:40):

If you feel like PRing some extra material around that definition, that would be great. :-)

view this post on Zulip Adam Topaz (Jul 10 2020 at 00:42):

Sure, i could do that. Is there no theorem which proves the universal property of sum/product assuming an equivalence with a sum/product?


Last updated: May 07 2021 at 23:11 UTC