## Stream: Is there code for X?

### Topic: Disjoint union of fin's

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


#### Scott Morrison (Jul 10 2020 at 00:17):

There is src#sum_fin_sum_equiv

#### Scott Morrison (Jul 10 2020 at 00:18):

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

#### Adam Topaz (Jul 10 2020 at 00:21):

That should be good enough! Thanks!

#### Scott Morrison (Jul 10 2020 at 00:40):

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

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