Algebraic closures and arithmetic universes

Algebraic closures and arithmetic universes

[David Roberts]

Hi,

There's a question at MathOverflow on the construction of algebraic
closures in constructive mathematics by Joyal. The idea as far as I can
tell is to construct the classifying arithmetic universe for the theory of
the algebraic closure. People might either be interested or have something
to contribute

https://mathoverflow.net/q/277551/4177

I repeat my respectful call for André to release his notes of arithmetic
universes for us all to use, or at the least confirm that Maietti et al
found the same definition  :-)


Best regards,
David


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

Re: Algebraic closures and arithmetic universes

[Steve Vickers]

Dear Andre,

Here's my own understanding of the history of AU definitions. Can you comment on its accuracy?

1. You defined the initial AU, with a concrete construction, as sufficient structure to embody arithmetic. You also showed that the initial AU has an internal initial AU, and used that to establish the Goedel gap between truth (external) and provability (internal).

2. You and others also discussed what the general definition might be. I picked this up from Gavin Wraith in the 1990s. (I had first learned about AUs from Gavin's talk at the 1985 Surrey conference on Categories in Computer Science.) Conceptually, it was "pretopos + free algebra constructions", but the  question was how to get a collection of primitive constructions sufficient to get whatever else was needed. Gavin suggested free categories over directed graphs and free category actions over graph actions.

3. Milly Maietti proposed parametrized list objects, and I am persuaded her axiomatization is good. It is the one we used in our joint paper, and I used in "Sketches for AUs". I believe it provides adequate foundations for my proof with Palmgren of the existence of initial algebras for cartesian theories.

All the best,

Steve.

> On 1 Aug 2017, at 01:26, a1078662@adelaide.edu.au wrote:
> 
> Hi,
> 
> There's a question at MathOverflow on the construction of algebraic
> closures in constructive mathematics by Joyal. The idea as far as I can
> tell is to construct the classifying arithmetic universe for the theory of
> the algebraic closure. People might either be interested or have something
> to contribute
> 
> https://mathoverflow.net/q/277551/4177
> 
> I repeat my respectful call for André to release his notes of arithmetic
> universes for us all to use, or at the least confirm that Maietti et al
> found the same definition  :-)
> 
> 
> Best regards,
> David
> 



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

Re: Re: Algebraic closures and arithmetic universes

[David Roberts]

Hi Steve,

Ah, excellent. I do wonder then, if free parameterised list objects
are finitary (parameterised) W-types and all of the latter exist when
the former exist (in the presence of the other assumptions on the AU),
if existence of W-types is a cleaner assumption for an AU. It may be
like the definition of elementary topos, where terminal object,
pullbacks and power objects suffice, but people sometimes just package
(local) cartesian closedness into the definition (not to speak of
finite colimits) as it is perfectly equivalent.

From a categorical point of view W-types may be ok, though for certain
parsimonious presentations I guess list objects may be smaller to
describe and so desirable for that reason.

To advertise slightly some of my own work that I presented at Topos à
l'IHÉS (or at least some approximation of the following), the
following construction gives an arithmetic pretopos (with finitary
W-types), plus some.

Take a filtered category R that is (classically) well-founded with
terminal object, R may be large. Let E:R^op --> Topos/Set be a diagram
in Grothendieck toposes. Define E*: R --> (Topos/Set)^op --> Set/LEX
where the latter functor sends a topos to the underlying
infinitary-lextensive category and a geometric morphism to its left
exact cocontinuous inverse image functor. I allow for objects of LEX
to be large categories. Then colim E* is an infinitary Heyting
pretopos with subobject classifier and parameterised finitary W-types.
If R is small, this is the limit of the diagram of toposes, but if R
is large then this colimit arises in set theory as "(Easton) class
forcing".

If one starts instead with a base other than set, and even not with
toposes but the underlying pretopos then I imagine one still have a
reasonable structure at the end, minus perhaps the infinitary colimits
and the subobject classifier. One of the points I wasn't sure on is
the classical well-foundedness; I'm not 100% sure I conjecture than
for any "pretame" class forcing (a partial order with top and with
some local smallness conditions) then one has a similar result,
constructing an Easton pretopos. There are conditions one can give
that ensure one has a topos at the end. The pretameness could be
generalised to other sites than partial orders with double negation.

David




On 3 August 2017 at 17:15, Steve Vickers <s.j.vickers@cs.bham.ac.uk> wrote:
> Dear David,
>
> Any AU should have finitary W-types, at least if "finite" is in the strong
> sense of "isomorphic to an initial segment of N".
>
> Consider f: B -> A in an AU AA, such that f is finite in the slice AA/A. It
> will correspond to a morphism ar: A -> N, which we can think of as an arity
> map.
>
> The elements of the W-type are trees, but an alternative representation is
> as elements of List(A), using reverse Polish notion. This is the key
> insight: that trees can be encoded as lists. After that, the rest is just
> about manipulating lists.
>
> Now think of stack evaluation of reverse Polish expressions. We have a
> function sd: List(A) -> Z, such that sd(as) is the stack depth change after
> evaluating as:
>
>   sd empty = 0
>   sd (as ++ [a]) = sd(as) - ar(a) + 1  (pop ar(a) arguments, push the
> result)
>
> Then the elements of the W-type are those bs such that sd(as) = 1 (just  one
> value at the end), and sd(as') >= 1 for every non-empty prefix as' of as (no
> stack underflow).
>
> All that can be expressed in AUs.
>
> Obviously there's more to be done to show that the object constructed here
> has the right properties for a W-type, but our knowledge of reverse Polish
> notation gives us good grounds for conjecturing that it does. I haven't
> addressed "or rather a parametrized version", but hopefully that will work
> out.
>
> I'm relating this to your formulation as follows. A_n is the fibre of ar
> over n. (Note - in my formulation I haven't assumed that A is finite, or
> that ar is bounded.) Then P(X) is the subobject of A x List(X) comprising
> pairs (a, xs) such that length of xs = ar(a).
>
> Regards,
>
> Steve.
>
>
> On 2 Aug 2017, at 00:31, droberts.65537@gmail.com wrote:
>
> Has anyone considered a version of arithmetic universes admitting all
> finitary W-types? I'm thinking initial algebras for "explicit polynomial"
> endofunctors, like
>
> P(X) = A_0 + A_1 x X + A_2 x X^2 +... +A_n x X^n
>
> or rather parameterised versions, for any given family A_0,...A_n.
>
> Can these more general parameterised W-types be shown to exist from weaker
> considerations?
>
> David
>
>
> On 2 Aug 2017 8:42 AM, "Steve Vickers" <s.j.vickers@cs.bham.ac.uk> wrote:
>
> Dear Andre,
>
> Here's my own understanding of the history of AU definitions. Can you
> comment on its accuracy?
>
> 1. You defined the initial AU, with a concrete construction, as sufficient
> structure to embody arithmetic. You also showed that the initial AU has an
> internal initial AU, and used that to establish the Goedel gap between truth
> (external) and provability (internal).
>
> 2. You and others also discussed what the general definition might be. I
> picked this up from Gavin Wraith in the 1990s. (I had first learned about
> AUs from Gavin's talk at the 1985 Surrey conference on Categories in
> Computer Science.) Conceptually, it was "pretopos + free algebra
> constructions", but the  question was how to get a collection of primitive
> constructions sufficient to get whatever else was needed. Gavin suggested
> free categories over directed graphs and free category actions over graph
> actions.
>
> 3. Milly Maietti proposed parametrized list objects, and I am persuaded her
> axiomatization is good. It is the one we used in our joint paper, and I used
> in "Sketches for AUs". I believe it provides adequate foundations for my
> proof with Palmgren of the existence of initial algebras for cartesian
> theories.
>
> All the best,
>
> Steve.
>
>> On 1 Aug 2017, at 01:26, a1078662@adelaide.edu.au wrote:
>>
>> Hi,
>>
>> There's a question at MathOverflow on the construction of algebraic
>> closures in constructive mathematics by Joyal. The idea as far as I can
>> tell is to construct the classifying arithmetic universe for the theory of
>> the algebraic closure. People might either be interested or have something
>> to contribute
>>
>> https://mathoverflow.net/q/277551/4177
>>
>> I repeat my respectful call for André to release his notes of arithmetic
>> universes for us all to use, or at the least confirm that Maietti et al
>> found the same definition  :-)
>>
>>
>> Best regards,
>> David
>>
>
>
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
>
>



-- 
David Roberts
http://ncatlab.org/nlab/show/David+Roberts


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

Re: Re: Algebraic closures and arithmetic universes

[Steve Vickers]

Dear David,

I'm sure there's scope for optimizing the AU axioms. In my "Sketches for
AUs" I replaced the original list-arithmetic pretopos with a slightly
different formulation that exploits the fact that, in the presence of
list objects, the pretopos has all finite colimits. (This is essentially
because one can form transitive closures of relations and hence get
arbitrary coequalizers.)

However, note that to use finitary W-types as internal structure (the
way I described) you have to express "finitary" internally somehow; and
to use them, or some of them, as external structure, with externally
given A_i etc, you may need infinitely many operations to present the
theory of AUs.

My own feeling when I wrote "Sketches for AUs" was that the ugliest bits
of the presentation were the exactness and stability conditions needed
for a pretopos. (Look at the rules for exactness and stability in
definition 15, for equivalence extensions.) I wondered whether they
could be simplified in the presence of the list objects.

All the best,

Steve.

On 03/08/2017 09:25, droberts.65537@gmail.com wrote:
> Hi Steve,
>
> Ah, excellent. I do wonder then, if free parameterised list objects
> are finitary (parameterised) W-types and all of the latter exist when
> the former exist (in the presence of the other assumptions on the AU),
> if existence of W-types is a cleaner assumption for an AU. It may be
> like the definition of elementary topos, where terminal object,
> pullbacks and power objects suffice, but people sometimes just package
> (local) cartesian closedness into the definition (not to speak of
> finite colimits) as it is perfectly equivalent.
>
> From a categorical point of view W-types may be ok, though for certain
> parsimonious presentations I guess list objects may be smaller to
> describe and so desirable for that reason.
>



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