projective algebras

projective algebras

[Andrei Popescu]

Dear Categorists,

Some time ago, I have posed you a question about the characterization of
projective algebras in the category of all algebras of a given signature.
Since some of you appeard interested in the subject, I allow myself to
send you, in a slightly detailed manner, the answer that I have found.

Projective algebras coincide with free algebras in the following cases:

I. Any class (i.e. complete subcategory) of algebras that is closed to
taking subobjects and for which free algebras exist and have a certain
property (namely that there are no infinite chains of elements such that
each one is obtained by applying an operation to an n-uple that includes
the predecesor in the chain).

In particular,

II. Suppose X is a countably infinite set. Any quasivariety K of algebras
for which the kernel of the unique morphism extending X from the term
algebra to the algebra freely generated in K by X has finite congruence
classes.

In particular,

III. - The category of all algebras (of a given signature);

    - The category of [commutative] semigroups;

   - The category of [commutative] (non-unital and non-anihilating) semirings.

Best regards,

    Andrei

Re: projective algebras

[Mamuka Jibladze]

Here is some more information on the question of Andrei Popescu. In the
paper "Projectives are free for nilpotent algebraic theories" by T.
Pirashvili (pages 589-599 in: Algebraic $K$-theory and its applications.
Proceedings of the workshop and symposium, ICTP, Trieste, Italy, September
1-19, 1997. World Scientific, Singapore (1999)) it is shown that if
projectives are free in the category of internal abelian groups of a
sufficiently nice (e. g. Maltsev) variety, then the same holds for the
category of all nilpotent (in the sense of commutator calculus) algebras in
that variety. This is derived from the fact that one can lift splittings of
idempotents along a linear extension of algebraic theories.

Mamuka

> Dear Categorists,
>
> Some time ago, I have posed you a question about the characterization of
> projective algebras in the category of all algebras of a given signature.
> Since some of you appeard interested in the subject, I allow myself to
> send you, in a slightly detailed manner, the answer that I have found.
>
> Projective algebras coincide with free algebras in the following cases:
>
> I. Any class (i.e. complete subcategory) of algebras that is closed to
> taking subobjects and for which free algebras exist and have a certain
> property (namely that there are no infinite chains of elements such that
> each one is obtained by applying an operation to an n-uple that includes
> the predecesor in the chain).
>
> In particular,
>
> II. Suppose X is a countably infinite set. Any quasivariety K of algebras
> for which the kernel of the unique morphism extending X from the term
> algebra to the algebra freely generated in K by X has finite congruence
> classes.
>
> In particular,
>
> III. - The category of all algebras (of a given signature);
>
>     - The category of [commutative] semigroups;
>
>    - The category of [commutative] (non-unital and non-anihilating)
semirings.
>
> Best regards,
>
>     Andrei

Inductive datatypes in toposes

[Lutz Schroeder]

Dear categorists,

is there a good reference for the construction of inductive datatypes
(lists, trees etc.) in a topos with nno (assuming that my guess that
such a construction is indeed possible is correct)?

Thanks a lot,

Lutz Schröder


-- 
-----------------------------------------------------------------------------
Lutz Schroeder                  Phone +49-421-218-4683
Dept. of Computer Science       Fax +49-421-218-3054
University of Bremen            lschrode@informatik.uni-bremen.de
P.O.Box 330440, D-28334 Bremen
http://www.informatik.uni-bremen.de/~lschrode
-----------------------------------------------------------------------------

Re: Inductive datatypes in toposes

[Luigi Santocanale]

Lutz Schroeder a écrit :
> 
> Dear categorists,
> 
> is there a good reference for the construction of inductive datatypes
> (lists, trees etc.) in a topos with nno (assuming that my guess that
> such a construction is indeed possible is correct)?

Here are those I know:
\x1f
@incollection {MR81f:18019,
    AUTHOR = {Johnstone, Peter T. and Wraith, Gavin C.},
     TITLE = {Algebraic theories in toposes},
 BOOKTITLE = {Indexed categories and their applications},
    SERIES = {Lecture Notes in Math.},
    VOLUME = {661},
     PAGES = {141--242},
 PUBLISHER = {Springer},
   ADDRESS = {Berlin},
      YEAR = {1978},
   MRCLASS = {18B25 (18C10)},
  MRNUMBER = {81f:18019},
}

@article {MR48:8597,
    AUTHOR = {Lesaffre, Brigitte},
     TITLE = {Structures alg\'ebriques dans les topos \'el\'ementaires},
   JOURNAL = {C. R. Acad. Sci. Paris S\'er. A-B},
    VOLUME = {277},
      YEAR = {1973},
     PAGES = {A663--A666},
   MRCLASS = {18C10 (02H10)},
  MRNUMBER = {48 \#8597},
MRREVIEWER = {Andreas Blass},
}

For a subtopos structure:

@incollection {MR95h:68133,
    AUTHOR = {Jay, C. Barry and Cockett, J. R. B.},
     TITLE = {Shapely types and shape polymorphism},
 BOOKTITLE = {Programming languages and systems---ESOP '94 (Edinburgh,
              1994)},
    SERIES = {Lecture Notes in Comput. Sci.},
    VOLUME = {788},
     PAGES = {302--316},
 PUBLISHER = {Springer},
   ADDRESS = {Berlin},
      YEAR = {1994},
   MRCLASS = {68Q65 (68N15)},
  MRNUMBER = {95h:68133},
}

Best,

	Luigi

-- 
Luigi Santocanale
http://www.labri.fr/~santocan/

Re: Inductive datatypes in toposes

[Thomas Streicher]

concerning the question

> is there a good reference for the construction of inductive datatypes
> (lists, trees etc.) in a topos with nno (assuming that my guess that
> such a construction is indeed possible is correct)?

The situation appears to me as follows.
I those toposes where IZF (intuitionistic Zermelo Fraenkel set theory) is
available (as e.g. Grothendieck and realizability toposes) business is as
usual for functors preserving \omega-colimits: you simply construct mu(F) as
colim_{n \in \omega} F^n(0). Notice, however, that there is a tacit appeal
to the axiom of replacement when constructing the family (F^n(0))_{n\in\omega}.
In general there is no reason why this family should exist. Of course, for the
above mentioned examples like lists, trees etc. you can construct such
inductive data types because both List(A) and Tree(A) appear as inductively
defined subsets of P(\tilde{A}^N) where \tilde{A} is the partial map
classifier. The reason is that trees and lists over A can be coded as partial
maps from N to A.
The point is that toposes (due to their impredicative nature) support inductive
definitions of predicates on a type A given in advance. However, they don't
support construction of inductively defined types as one cannot define
sufficiently many families of types.
It is not clear to me to which extent one can characterise those inductive
types that can be reduced to inductively defined predicates in HAH.
However, one knows that assuming W-types (`a la Martin-Loef) one can reduce
most inductive types to W-types in extensional type theory. As far as I
understand that's the reason why Moerdijk and Palmgren introduced lccc's with
W-types as sort of ``predicative toposes''.

Thomas

Re: Inductive datatypes in toposes

[Alex Simpson]

Lutz Schroeder asked:

> > is there a good reference for the construction of inductive
> datatypes
> > (lists, trees etc.) in a topos with nno (assuming that my guess that
> > such a construction is indeed possible is correct)?

Thomas Streicher replied:

> It is not clear to me to which extent one can characterise those
> inductive
> types that can be reduced to inductively defined predicates in HAH.
> However, one knows that assuming W-types (`a la Martin-Loef) one can
> reduce
> most inductive types to W-types in extensional type theory. As far as
> I
> understand that's the reason why Moerdijk and Palmgren introduced lccc's
> with
> W-types as sort of ``predicative toposes''.

Just to point out that "assuming W-types" here is no extra assumption.
Moerdijk and Palmgren observe that every elementary topos with nno
has W-types. This observation more than answers Schroeder's
original question affirmatively. See Moerdijk and Palmgren,
"Well-founded trees in categories", APAL 104, 2000, for the
observation. I'm not sure whether they include the details (I
don't have the paper to hand), but it's not a hard exercise.

Alex Simpson

Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh
Email: Alex.Simpson@ed.ac.uk           Tel: +44 (0)131 650 5113
Web: http://www.dcs.ed.ac.uk/home/als  Fax: +44 (0)131 667 7209