well powered categories, categorically?

well powered categories, categorically?

[Paul Taylor]

Is there some genuinely categorical account of the notion of

             WELL POWERED CATEGORY

that would rid this topic of what I have taken to calling
"hocus pocus" foundations?

That is, I do not want to be told that a well powered category
has a "set" of isomorphism classes of subobjects of each object.

(I have just done a web search for this phrase but, despite the
occurrence of several names for which I have a lot of respect,
I could not find anything along the lines I have in mind.)

Suppose we are using some elementary topos E as our usual
mathematical workbench, so objects of E are called "sets".
We can set up the notions of poset, dcpo, lattice, complete
lattice and whatever in E in the usual way.

To talk about some category C being "well powered", I want:

- I don't care about "collecting" all the objects of C,
    so it doesn't need to be an internal category in E.

- I would like the homs of C to be objects of E, so it is
    an E-enriched category.

- Each object of C has a "set" (E-object) of isomorphism
    classes of monos into it, and

- C might as well have pullbacks of monos (inverse images),
    so this is a contravariant functor

       Sub  :   C^op  ------>  Poset_E

- Now I want to so some ordinary categorical constructions
    in C using diagrams, with such things as pullbacks,
    colimits of diagrams indexed by E-objects, maybe function
    types.

- Suppose that all of the objects that occur in my
    construction have monos into a handful of particular
    C-objects X_1, ..., X_k

- Then I want to INTERNALISE the construction using
    endofunctions of
           Sub (X_1 x ... x X_k)
    or something like that.

- I use some logic and constructions in the elementary topos
    E to do something or other with this internalisation.

- Then I want to EXTERNALISE this to give some diagrammatic
    construction in the category.

- A particular application of this would be to PARTIAL
    MAPS, so maybe some of the work of Pino Rosolini,
    Robin Cockett and others might form part of this theory.


For example, let C just be the topos E.   We know how to
internalise ("classify") subobjects - using the subobject
classifier Omega.

Simple constructions like intersection and union of
subobjects in E can be internalised as the meet and join
on Omega.  So we can show that it is a Heyting algebra.

Doing this is an exercise that many of us will have done
as graduate students.  It's straightforward, once you get
the idea, but a bit tedious after a while.

So what I'm looking for is the universal property that
says how to internalise and externalise, ie translate
between categorical diagram constructions in the category C
and endofunctions of the Sub(X) objects in E.

I will write about the subject for which I need this in
another posting.

Any ideas?

Paul Taylor.



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: well powered categories, categorically?

[Peter LeFanu Lumsdaine]

Perhaps this is one of the accounts you found unsatisfactory, but what
about the approach using indexed categories, as set out in e.g. Section
B1.3 of the Elephant, and (partially) summarised at
https://ncatlab.org/nlab/show/indexed+category ?

Your category C would be given as an indexed category over the base E; this
allows talking about families of objects of C indexed by objects of E, and
more generally, diagrams in E indexed by internal categories in C.  There
are standard definitions (given in the Elephant) for an indexed category to
*locally small* (generalising the enrichment you ask for), and
*well-powered*, which seems sufficient for all or most of what you ask for
below?

(Of course, all this can be set up in terms of fibrations instead of
indexed categories, according to taste.)

Best,
–Peter

On Thu, Dec 5, 2019 at 3:29 PM Paul Taylor <cats@paultaylor.eu> wrote:

> Is there some genuinely categorical account of the notion of
>
>              WELL POWERED CATEGORY
>
> that would rid this topic of what I have taken to calling
> "hocus pocus" foundations?
>
> That is, I do not want to be told that a well powered category
> has a "set" of isomorphism classes of subobjects of each object.
>
> (I have just done a web search for this phrase but, despite the
> occurrence of several names for which I have a lot of respect,
> I could not find anything along the lines I have in mind.)
>
> Suppose we are using some elementary topos E as our usual
> mathematical workbench, so objects of E are called "sets".
> We can set up the notions of poset, dcpo, lattice, complete
> lattice and whatever in E in the usual way.
>
> To talk about some category C being "well powered", I want:
>
> - I don't care about "collecting" all the objects of C,
>     so it doesn't need to be an internal category in E.
>
> - I would like the homs of C to be objects of E, so it is
>     an E-enriched category.
>
> - Each object of C has a "set" (E-object) of isomorphism
>     classes of monos into it, and
>
> - C might as well have pullbacks of monos (inverse images),
>     so this is a contravariant functor
>
>        Sub  :   C^op  ------>  Poset_E
>
> - Now I want to so some ordinary categorical constructions
>     in C using diagrams, with such things as pullbacks,
>     colimits of diagrams indexed by E-objects, maybe function
>     types.
>
> - Suppose that all of the objects that occur in my
>     construction have monos into a handful of particular
>     C-objects X_1, ..., X_k
>
> - Then I want to INTERNALISE the construction using
>     endofunctions of
>            Sub (X_1 x ... x X_k)
>     or something like that.
>
> - I use some logic and constructions in the elementary topos
>     E to do something or other with this internalisation.
>
> - Then I want to EXTERNALISE this to give some diagrammatic
>     construction in the category.
>
> - A particular application of this would be to PARTIAL
>     MAPS, so maybe some of the work of Pino Rosolini,
>     Robin Cockett and others might form part of this theory.
>
>
> For example, let C just be the topos E.   We know how to
> internalise ("classify") subobjects - using the subobject
> classifier Omega.
>
> Simple constructions like intersection and union of
> subobjects in E can be internalised as the meet and join
> on Omega.  So we can show that it is a Heyting algebra.
>
> Doing this is an exercise that many of us will have done
> as graduate students.  It's straightforward, once you get
> the idea, but a bit tedious after a while.
>
> So what I'm looking for is the universal property that
> says how to internalise and externalise, ie translate
> between categorical diagram constructions in the category C
> and endofunctions of the Sub(X) objects in E.
>
> I will write about the subject for which I need this in
> another posting.
>
> Any ideas?
>
> Paul Taylor.
>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: well powered categories, categorically?

[Ross Street]

On 5 Dec 2019, at 7:38 AM, Paul Taylor <cats@PaulTaylor.EU<mailto:cats@paultaylor.eu>> wrote:

- I would like the homs of C to be objects of E, so it is
an E-enriched category.

Dear Paul

If, rather than C E-enriched, you give meaning to E-indexed families of C objects
by taking C to be a category (parametrized) over E, then what I think you want is
in the works of B\'enabou, Par\'e-Schumacher [SLNM 661], and Section 2 of

32. (with D. Schumacher) Some parametrized categorical concepts,
Communications in Algebra 16(1988) 2313--2347

where you will find precise references to other works.

For example, let C just be the topos E. We know how to
internalise ("classify") subobjects - using the subobject
classifier Omega.

Taking C to be the the arrow category of E, over E via the codomain functor,
wellpowered is about the existence of a subobject classifier in E.

All the best,
Ross


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]