# About Michael Barr immersion theorem for regular categories, and pretopos

In the article of M. Barr "Representation of Categories" J. Pure Appl. Algebra, 41 (1986), 113–137 link: ftp://ftp.math.mcgill.ca/pub/barr/pdffiles/represen.pdf

M. Barr shows a classical (but hard) theorem :

"every regular category had a full, regular embedding into a category of set-valued functors".

Anyway I think that in that article there are some mistakes, or he takes for granted things that I do not know or I haven't seen in the literature.

Then I had some difficulties in reassembling the demonstration of the fundamental theorem and other questions that I asked myself while reading.

M. Barr starts from a small category $C$, and lets $FL(C)$ be the full sub category of copreshaves category $C^<:=Cat[C , Set]$ formed by the functors that preserve finite limits.
Then we have the Yoneda immersion $h^-: C^{op} \to FL(C)$ and the dual is a immersion $Y: C \to \widetilde{C}$ by $\widetilde{C}:=FL(C)^{op}$.

Then Barr proves that if $C$ is regular then also $\widetilde{C}$ is regular (in the proof one needs the observation that the Yoneda functor $h^-$ sends a (reg.Epi, Mono) factorization to an (Epi, reg.Mono) one, easy to prove). And this is ok for me.

Then Barr gives a proof (not clear I think) that if $C$ is a pretopos then also $\widetilde{C}$ is pretopos.

For what I know (Sketches of an Elephant, Peter T. Johnstone, Vol 1, part 1.4.7):

A pretopos is a coherent effective categories by disjoint finite coproducts.

And a coherent category is a regular one, by unions that are preservated by pullback's. Effective means that any equivalence realtion is a ker-pair of some morphism (I guess).

Among other difficulties, there is that the completeness of $FL(C)$ follows from being a reflective subcategory of $C^<$ (a hard theorem) and then the immersion $FL(C) \subset C^<$ dosen't preserve colimits (it creates limits of course).

I ask simply: If $C$ is coherent (resp. effective, a pretopos), how I can prove that $\widetilde{C}$ is coherent (resp. effective, a pretopos)?

-
I've made some (I hope) purely typographical changes. If I have changed the meaning of anything you wrote, I sincerely apologize, and you should feel free to roll back the edits. (I was unsure how to fix "A pretopos is a coherent effective categories by disjoint finite coproducts.", which doesn't parse for me, and I felt that any best guess would too likely change the content of (or introduce errors) to the post.) –  Theo Johnson-Freyd Dec 20 '10 at 3:22
I fixed a small TeX-typo that was throwing out the markdown –  David Roberts Dec 20 '10 at 6:27
And another, after Buschi's latest edit. I'm doing this because it was cutting out half of a sentence, making the idea hard to grasp. –  David Roberts Dec 20 '10 at 8:21
I'm in way of solution. No so hard as I guessed in first time, (fog is vanishing). Of course dont seem honest reply to a mine question. But if someone is intesting I can post (or Emailing) a "more detalied" proofs and explanation about BArr article. The result of Barr article is a important goal in category theory tools, and generally the proofs are very long and hard. Thank you for your interset and patience, I'm sorry for my poor English . PS. someone understand Italian too? –  Buschi Sergio Dec 21 '10 at 14:31