Zulip Chat Archive

Stream: new members

Topic: Describe coproducts in Sets


Noah Anderson (Mar 26 2025 at 07:06):

How can I say that "disjoint union" is coproduct in the category of Sets?
(or the coproduct in the category of Sets is disjoint union

Noah Anderson (Mar 26 2025 at 07:11):

Do we have "category of sets" in mathlib? and is it possible to prove such thinig via simply verifying its universal property etc.?

Noah Anderson (Mar 26 2025 at 07:54):

Should it be something like this?

/-
Describe coproducts in Sets.
-/

open CategoryTheory Limits

universe u

structure Sets : Type (u + 1) where
  (carrier : Type u)
  [str : Set carrier]

structure Sets.Hom (A B : Sets.{u}) where
  private mk ::
  hom' : A.str  B.str

instance : Category Sets.{u} where
  Hom X Y := Sets.Hom X Y
  id X := id
  comp f g := g.hom'.comp f.hom'

variable (X Y : Sets.{u})

abbrev Z : Sets.{u} := {
  carrier := X.carrier  Y.carrier
  str := Set.univ
}

example (X Y : Sets) : HasBinaryCoproduct X Y := by
  sorry

Aaron Liu (Mar 26 2025 at 08:43):

In mathlib we have the category of types

Aaron Liu (Mar 26 2025 at 08:44):

This looks like it should be an equivalent category

Aaron Liu (Mar 26 2025 at 08:45):

But your coproduct is wrong

Johan Commelin (Mar 26 2025 at 08:48):

@Noah Anderson You can just work with Type u directly. Your current Sets has objects of the form strcarrier\text{str} \subseteq \text{carrier}, but then you ignore the carrier when defining homs.

Kevin Buzzard (Mar 26 2025 at 13:31):

Lean uses type theory not set theory, and the type plays the role of a set here.

Noah Anderson (Mar 27 2025 at 01:44):

I see... so it would be CategoryTheory.Limits.Types.binaryCoproductIso I imagine, thanks!


Last updated: May 02 2025 at 03:31 UTC