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