Newbie question: is this sane?

[David Starner]

I'm trying again to prove stuff in metamath, starting with the
"definition" of a group in Algebra: Chapter 0, by Paolo Aluffi: "A
group is a groupoid with a single object." After pushing through the
category theory section, I've finally put together:

$( <MM> <PROOF_ASST> THEOREM=catisoismnd LOC_AFTER=

hd1:: |- ( ph -> B = ( Base ` C ) )
hd2:: |- ( ph -> .x. = ( comp ` C ) )
hd3:: |- ( ph -> I = ( Iso ` C ) )
hd4:: |- ( ph -> C e. Cat )
hd5:: |- ( ph -> suc (/) ~~ B )
hd6:: |- ( ph -> I = ( Base ` G ) )
hd7:: |- ( ph -> .x. = ( +g ` G ) )
qed:: |- ( ph -> G e. Mnd )

That is, if I understand it right, the isomorphisms of a category with
one object form a monoid. Am I on the right track?

--
Kie ekzistas vivo, ekzistas espero.

[Benoit]

First note that categories as defined in set.mm are small (that is, their morphisms form sets), so there is no size issue to worry about.

I would prove the following statements:

* the set of isomorphisms of a category is a groupoid;

* the set of endomorphisms of a category on a given object is a monoid;

* the set of automorphisms of a category on a given object is a group.

The easiest way to code these is probably to use the restriction of extensible structures, |`s(see df-ress).  Therefore it would look something like:

${

$e |- ( ph -> C e. Cat ) $.

$p |- ( ph -> ( C |`s ( Iso `C ) ) e. Groupoid ) $= ? $.

$e |- ( ph -> X e. ( Base `C ) ) $.

$p |- ( ph -> ( C |`s ( ( End ` C ) ` X ) ) e. Monoid ) $= ? $.

$p |- ( ph -> ( C |`s ( ( Aut `C ) `X ) ) e. Group ) $= ? $.

$}

EDIT: obviously, as you noticed, there is some gymnastic to do to put things in the right "slot", which looks painful...

Benoît

[fl]

They are small but Tarski-Grothendieck's  axiom has been added. that means that you can

always find sets of sufficient size where all the operations you expect in set theory are available:

powerset, union etc. So as I understand it, they are small but you will never notice it.

However it would be interesting to identify where being small matters.

I had tried to add an alternate definition where we could deal with not small categories  

but Norm didn't want it. It is reasonable to keep the system sound but that means there is no

way to understand precisely where smallness occurs precisely in the theory.

--

FL

[Mario Carneiro]

The problem with large categories is that they don't fit in as structures. You have to have a completely separate theory for them, so they aren't really categories at all. And category theorists never stop there anyway. They want to make constructions on top of these categories, talking about "conglomerates" and such, and then you are stuck. I think it is better to just always relativize to some set when doing explicit category theory. In theory, TG is there in case we need ZFC in one of these sets, but in practice (at least in the small amount of category theory done thus far) it hasn't been needed at all, and "weak universes" are mostly sufficient and can be proven to exist in ZFC.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b5e0497b-933a-4553-8c7f-b3e14d63aac6%40googlegroups.com.

[Mario Carneiro]

On Wed, Jan 29, 2020 at 7:57 AM 'fl' via Metamath <meta...@googlegroups.com> wrote:

It is reasonable to keep the system sound but that means there is no

way to understand precisely where smallness occurs precisely in the theory.

Actually, when you are doing relativized category theory, the smallness is quite explicit - the relativizing sets (traditionally called "universes", although I put no particular requirements on them). These sets can be in a containment relationship which indicates that you are in a larger category, and so the smaller one is the "small" category and the larger one is the "large" category, and you can have as many levels of this as you want.

[Benoit]

I agree with FL's and Mario's comments. If one does category theory in a set theoretical framework, then Grothendieck's universes are the way to go.

My initial remark

  "First note that categories as defined in set.mm are small (that is, their morphisms form sets), so there is no size issue to worry about."

was there to mean only that: there is no size issue to worry about.

Benoît