category of sets

Stream: Is there code for X?

[Utensil Song]

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

[Utensil Song]

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.

[Markus Himmel]

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

[Scott Morrison]

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

[Markus Himmel]

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?

[Utensil Song]

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.

[Scott Morrison]

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).

[Scott Morrison]

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).

[Adam Topaz]

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.

[Utensil Song]

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).

[Kenny Lau]

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

[Utensil Song]

has_limits_of_complete_lattice ?

[Kenny Lau]

that’s saying it has all limits right

[Kenny Lau]

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

[Kenny Lau]

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

[Utensil Song]

preorder.small_category (set X)

[Adam Topaz]

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.