Zulip Chat Archive

Stream: Is there code for X?

Topic: category of sets


view this post on Zulip Utensil Song (Aug 15 2020 at 12:36):

It seems that there're no category of sets in mathlib?

I've made a #mwe (with a random proof as POC) but don't know if it's idiomatic or correct:

import init.function
import category_theory.category
import category_theory.full_subcategory
import algebra.category.Group

universes u v

open category_theory

variables (X : Type u)

instance Set.category : category (set X) :=
{ hom  := λ A B, A  B,
  id   := λ S s, s,
  comp :=  λ _ _ _ f g, g  f }

lemma Set.injective_of_mono {A B : set X} (f : A  B) [mono f] : function.injective f :=
begin
  assume a₁ a₂ h,
  let α₁ : A  A := λ _, a₁,
  let α₂ : A  A := λ _, a₂,
  let hom_α₁ := as_hom α₁,
  let hom_α₂ := as_hom α₂,
  have t0 : hom_α₁  f = hom_α₂  f :=
  begin
    ext x',
    cases x',
    cases a₁,
    cases a₂,
    dsimp at *,
    solve_by_elim,
  end,
  have t1 : hom_α₁ = hom_α₂ := (cancel_mono f).mp t0,
  have t2 : α₁ = α₂ := by assumption,
  have t3 : α₁ a₁ = α₂ a₁ := by rw t2,
  have t4 : α₁ a₁ = a₁ := rfl,
  have t5 : α₂ a₁ = a₂ := rfl,
  assumption,
end

view this post on Zulip Utensil Song (Aug 15 2020 at 12:38):

I noticed docs#category_theory.bundled and docs#category_theory.induced_category and this topic but don't know how to apply them to a non-class set.

view this post on Zulip Markus Himmel (Aug 15 2020 at 12:39):

What mathematicians would call the category of sets is called the category of types in mathlib: docs#category_theory.types

view this post on Zulip Scott Morrison (Aug 15 2020 at 12:39):

I guess no one has noticed a use for it so far. (Of course we use the category of types a lot.)

view this post on Zulip Markus Himmel (Aug 15 2020 at 12:40):

Are you looking for the category of sets as in your wikipedia link or for the category of sets of a type X as in your code sample?

view this post on Zulip Utensil Song (Aug 15 2020 at 12:44):

Markus Himmel said:

Are you looking for the category of sets as in your wikipedia link or for the category of sets of a type X as in your code sample?

The code example is born out of the difficulty of expressing the "the category of sets " properly, I think.

view this post on Zulip Scott Morrison (Aug 15 2020 at 12:44):

But @Utensil Song, I think the point is that as we're using different foundations, the category of sets is not particularly interesting or useful, and everywhere that conventional mathematics uses their "category of sets" (in set theory), we want to use the "category of types" (in type theory).

view this post on Zulip Scott Morrison (Aug 15 2020 at 12:45):

The category of sets (in type theory) (i.e. the thing you just defined) is not the same thing as the category of sets (in set theory).

view this post on Zulip Adam Topaz (Aug 15 2020 at 12:47):

Perhaps worth mentioning: the category of subsets of X, as defined in the code above, can be constructed as a full subcategory of the category of types. Full subcategories exists already in mathlib, if you really need this.

view this post on Zulip Utensil Song (Aug 15 2020 at 12:57):

Scott Morrison said:

But Utensil Song, I think the point is that as we're using different foundations, the category of sets is not particularly interesting or useful, and everywhere that conventional mathematics uses their "category of sets" (in set theory), we want to use the "category of types" (in type theory).

Thanks for the clarification, now I realized it. I was having trouble treating types as sets and sets as subsets lately due to some discussions on Zulip.

Thanks for the pointers to docs#category_theory.types and docs#category_theory.​full_subcategory , they seem to be what I'm looking for (fail to recognize them previously).

view this post on Zulip Kenny Lau (Aug 15 2020 at 12:58):

we do have a category structure on set X owing to its complete lattice structure

view this post on Zulip Utensil Song (Aug 15 2020 at 13:02):

has_limits_of_complete_lattice ?

view this post on Zulip Kenny Lau (Aug 15 2020 at 13:02):

that’s saying it has all limits right

view this post on Zulip Kenny Lau (Aug 15 2020 at 13:03):

you can try #check (by apply_instance : category (set X)) if you want to find the name

view this post on Zulip Kenny Lau (Aug 15 2020 at 13:03):

ofc with variable (X : Type*) on the previous line

view this post on Zulip Utensil Song (Aug 15 2020 at 13:09):

preorder.small_category (set X)

view this post on Zulip Adam Topaz (Aug 15 2020 at 13:19):

Note that the preorder category structure on set X is different from what was defined above. The limits in this are essentially just Inf and colimits essentially just Sup.


Last updated: May 16 2021 at 05:21 UTC