BRICS RS-94-37 J. van Oosten: Fibrations and Calculi of Fractions

BRICS

Basic Research in Computer Science

Fibrations and Calculi of Fractions

Jaap van Oosten

BRICS Report Series RS-94-37 ISSN 0909-0878 November 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

Fibrations and Calculi of Fractions

Jaap van Oosten

BRICS^{∗}

Department of Computer Science, University of Aarhus Denmark

Abstract

Given a fibration E → B and a class Σ of arrows of B, one can construct the free fibration (on E over B such that all reindexing functors over elements of Σ are equivalences.

In this work I give an explicit construction of this, and study its properties. For example, the construction preserves the property of being fibrewise discrete, and it commutes up to equivalence with fibrewise exact completions. I show that mathematically interesting situations are examples of this construction. In particular, subtoposes of the effective topos are treated.

Introduction. In the conference in Tours, July 1994, Jean Bénabou ([B2]) presented an alternative treatment of the calculus of fractions of [GZ](see section 1). One of his results was:

Theorem 0.1 (Bénabou) Let [figure: E; p; B] be a fibration and Σ ⊂ B a class of arrows

admitting a calculus of right fractions. Then the class S of arrows in E which are cartesian over elements of Σ also admits a calculus of right fractions. There is a map of fibrations

[figure: E; p; P_{S}; E[S^{−1}]; B; P_{Σ}; B[Σ^{−1}]]

if and only if all the reindexing functors σ^{∗} for σ ∈ Σ are equivalences. Moreover, in this case the diagram shown is a pullback.

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation

By “a map of fibrations” is meant a commutative square of categories as in the theorem, where the vertical arrows are fibrations and the top horizontal arrow is a cartesian functor.

This paper is about some constructions relating to this: I study the free

fibration (on [figure: E; p; B]) such that there is a map of fibrations from [figure: E; p; B] to it, which

inverts all the arrows in Σ on the base level, and consequently the free fibration

on [figure: E; p; B] over B with the property that all reindexing functors over arrows in Σ are

equivalences (by theorem 0.1, these problems are equivalent).

It should be noted that this is the construction of a special kind of colimit in the 2-category of fibrations (see [PTJ] and [H]; this is the category with fibrations as objects, maps of fibrations as 1-cells and vertical natural transformations as 2-cells), namely a bi-coinverter (the author thanks John Power for this piece of terminology). In a 2-category, a bi-coinverter for a diagram of two parallel 1-cells with codomain A and a 2-cell between them, is the universal 1-cell departing from A making the 2-cell invertible. Any class of arrows Σ of a given category B can be seen as a natural transformation between the functors dom and cod from the discrete category on Σ to B, and in the fibrational references given above it is explained how every such 2-cell (in Cat) lifts to a 2-cell between two maps of

fibrations, if B is the base of a fibration [figure: E; p; B]. The bi-coinverter of this 2-cell is

exactly the mentioned construction.

I show that some mathematically interesting situations are examples of this construction: filter-quotient toposes over germs of topological spaces, and some subtoposes of the effective topos Eff. There is also some material on preservation of coproducts.

1 Preliminaries

In this section I recall some definition and basic facts.

Given a category C, a class of arrows Σ ⊂ C is said to admit a calculus of right fractions ([GZ]) if the following conditions hold:

1. Σ contains all identities and is closed under composition;

2. Every diagram [figure: W; s; X; f; Y] with s ∈ Σ can be completed to a commutative square

[figure: V; t; f′; W; s; X; f; Y]

with t ∈ Σ;

3. Whenever tf = tg for some parallel pair f, g and t ∈ Σ, there is s ∈ Σ with fs = gs

In [GZ] it is shown that there is a category C[Σ^{−1}] and an arrow P_{Σ} : C → C[Σ^{−1}] which is universal among functors with domain C inverting all arrows in Σ (i.e. functors F such that F (s) is an isomorphism for all s ∈ Σ), and in case Σ admits a calculus of right fractions, this functor has a very constructive look: the category C[Σ^{−1}] has the same objects as C, and morphisms A → B are equivalence classes of spans [figure: A; V; s; f; B] with s ∈ Σ, where two such spans (s, f) and (t, g) are equivalent if and only if there is a commutative diagram:

[figure: V; s; f; X; Z; a; b; Y; W; t; g]

with sa = tb ∈ Σ. The functor P_{Σ} sends f : A → B to the equivalence class of the span (id, f).

[GZ] note the following facts: if C has finite limits, then C[Σ^{−1}] also has finite limits and P_{Σ} preserves them; given a parallel pair of arrows f, g in C, P_{Σ}(f) = P_{Σ}(g) if and only if there is t ∈ Σ with ft = gt, and P_{Σ}(f) is an isomorphism if and only if f fits into a diagram

[figure: t; g; h; s; f]

with s, t ∈ Σ. One calls the set of f such that P_{Σ}(f) is an isomorphism the saturation of Σ and says that Σ is saturated if it is equal to its own saturation. It is easy to prove, using the above characterization of elements in the saturation of Σ, that if Σ admits a calculus of right fractions, then so does its saturation, and so, in as much one only is interested in C[Σ^{−1}], one may as well assume that Σ is saturated. In case C has pullbacks, this will mean that Σ is a pullback congruence([B1]), that is: a class of arrows which contains all isomorphisms, is stable under pullback and such that for composable f, g, if two of f, g, fg are in the class then so is the third.

2 Construction

Theorem 2.1 Let [figure: E; p; B] be a fibration, and suppose Σ ⊆ B is a collection of arrows

of B which admits a calculus of right fractions. There is a fibration [figure: G; q; B[Σ^{−1}]] ,

together with a map of fibrations

[figure: E; i; p; G; q; B; P_{Σ}; B[Σ^{−1}]]

with the universal property that any map of fibrations

[figure: E; p; f; H; r; B; g; C]

such that g inverts all the arrows from Σ, has a factorization through [figure: G; q; B[Σ^{−1}]] ,

which factorization is unique up to isomorphism. Moreover, if [figure: E; p; B] is left exact,

then [figure: G; q; B[Σ^{−1}]] is too.

Proof. Without loss of generality, we may assume that Σ is saturated, i.e. Σ = P_{Σ}^{−1}(iso). It is not hard to check that the class of those arrows in E which are cartesian over maps in Σ admits a calculus of right fractions; let’s call this class S.

The objects of G are equivalence classes of pairs (σ, A) where A is an object of E and σ is an arrow in Σ with domain p(A). (σ, A) is equivalent to (τ, B) if the codomains of σ and τ coincide, and there is a commutative square

[figure: A; σ; X; Z; ϕ; ψ; B; τ] (This “diagram”, containing data from different categories, means that σp(ϕ) = τp(ψ). Whenever such a diagram is used, the dashed arrow is in the base category) with σ and τ are in Σ, and ϕ, ψ are cartesian, and the composite σp(ϕ) = τp(ψ) is in Σ. The reader will have no trouble verifying that this is an equivalence relation.

A morphism of G is an equivalence class of triples ⟨(σ, A), (ϕ, f), (τ, B)⟩ where (σ, A) and (τ, B) represent objects of G and [figure: A; V; ϕ; f; B] is a span with ϕ ∈ S. Two such triples ⟨(σ, A), (ϕ, f), (τ, B)⟩, ⟨(σ′, A′), (ϕ′, f′), (τ′, B′)⟩ are equivalent if there is a commutative diagram

[figure: A; σ; V; ϕ; f; B; τ; X; L; ζ; g; η; K; u; v; Y; A′; σ′; V′; f′; ϕ′; B′; τ′]

with ϕζ ∈ S and u, v ∈ S. Let us check that this relation is an equivalence relation. Obviously, it is symmetric and reflexive. As to transitivity, suppose we are given

[figure: A; σ; V; ϕ; f; B; τ; L; ζ; η; g; K; u; v; X; A′; σ′; V′; ϕ′; f′; B′; τ′; Y; L′; ζ′; η′; g′; K′; u′; v′; A′′; σ′′; V′′; ϕ′′; f′′; B′′; τ′′]

First construct squares [figure: L′′; β; α; L; η; L′; ζ′; V′] and [figure: K′′; b; a; K; v; K′; u′; B′] with all arrows in S and

then [figure: U; a′; h; K′′; a; L′′; gα; K] and [figure: U′; b′; h′; K′′; b; L′′; g′β; K′] with a′, b′ ∈ S and finally [figure: U′′; a′′; b′′; U; a′; U′; b′; L′′]

with a′′, b′′ ∈ S. Now vahb′′ = vgαa′b′′ = vgαb′a′′ = f′ηαb′a′′ = f′ζ′βb′a′′ = u′g′βb′a′′ = u′bh′a′′ = vah′a′′. Since va ∈ S we may, if necessary prefixing with an element from S, assume h′a′′ = hb′′. Then the diagram

[figure: A; σ; V; ϕ; f; B; τ; X; U′′; K′′; ua; v′b; Y; A′′; σ′′; V′′; ϕ′′; f′′; B′′; τ′′]

commutes.

To define composition, let us first observe that if ⟨(σ, A), (ϕ, f), (τ, B)⟩ represents a morphism in G and (σ′, A′) is another representative of its domain, there is a span [figure: A′; V′; ϕ′; f′; B] representing the same morphism, for if

[figure: A; σ; X; W; α; β; A′; σ′] witnesses that (A, σ) and (A′, σ′) represent the same object,

the span [figure: A′; V′; βϕ′; fα′; B] gives the same morphism.

To compose morphisms represented by the spans

[figure: X; A; σ; V; ϕ; f; B; τ; Y]

and

[figure: Y; B′; τ′; W; ψ; g; C; ν; Z]

, find a span (ψ′, g′) representing the latter, such that the codomain of ψ′ is B, a square

[figure: U; χ; f′; W′; ψ′; V; f; B]

as usual with χ ∈ S, and take the span [figure: X; A; σ; U; ϕχ; g′f′; C; ν; Z] as a representative for the composition. We must check that this is independent of the choice of representatives; that is if a span (ϕ′, f′) is equivalent to (ϕ, f) and (ψ′, g′) is equivalent to (ψ, g) then the compositions are equivalent. Let’s look at the diagram witnessing those equivalences, in which also the relevant squares for the compositions are drawn:

[figure: D; η; f̄; A; σ; V; ϕ; f; B; W; ψ; g; C; ν; X; K; L; M; m; m′; N; Z; A′; σ′; V′; ϕ′; f′; B′; W′; ψ′; g′; C′; ν′; D′; η′; f̄′]

Now find \xymatrix{L & L′ \ar[l] \ar[r] & M} with \xymatrix{L & L′ \ar[l]} in S such that

[figure: B; W; ψ; L; L′; M; m; m′; B′; W′; ψ′]

commutes, and [figure: K′; k; L′; K; L], [figure: K_{1}; D; η; K′; V] and [figure: K_{2}; D′; η′; K′; V′] with all the left hand arrows in S; finally \xymatrix{K′′ \ar[d] \ar[r] & K_{1} \ar[d] \\ K_{2} \ar[r] & K′} with all arrows in S. Perhaps replacing K′′ by

K′′′ with \xymatrix{K′′′ \ar[r] & K′′} in S, then

[figure: A; σ; D; ϕη; gf̄; C; ν; X; K′′; N; Z; A′; σ′; D′; ϕ′η′; g′f̄′; C′; ν′]

The proof that composition is associative, as well as the typing of it, is left to the reader. This completes the definition of G. The functor [figure: G; q; E[Σ^{−1}]] sends the object represented by (σ, A) to the codomain of σ and the map represented by the span (ϕ, f) to the map represented by the span (σp(ϕ), τp(f)). It is clear that this defines a functor.

The functor [figure: E; q; G] sends the object A to the equivalence class of the identity on p(A) and a morphism f : A → B to the equivalence class of the span [figure: A; A; =; f; B] . It is clear that we have a commutative square of categories.

To see that q is a fibration, as well as that i is a cartesian functor we prove that the morphism represented by the span [figure: A; V; ϕ; f; B] is cartesian (from (σ, A) to (τ, B)) if the arrow f is cartesian w.r.t. p. So suppose we have

[figure: X; A; σ; V; ϕ; f; B; τ; Y; X′; A′; ρ; W; ψ; g; B′; τ′]

as two morphisms: from [(A, σ)] to [(B, τ)] and from [(A′, σ′)] to [(B′, τ′)] = [(B, τ)], respectively, such that the q-image of the downmost arrow factors through the q-image of the topmost one. That means that in B we have:

[figure: X; p(A); σ; p(V); p(ϕ); p(f); p(B); τ; C; h; π; D; λ; h̄; b; Y; X′; p(A′); ρ; p(W); p(ψ); p(g); p(B′); ν]

We know that (τ, B) and (τ′, B′) represent the same object so there is

[figure: B; τ; B′′; α; β; Y; B′; ν]

in E with α and β in S. Let [figure: D̄; \underline{b}; W] cartesian over b, and

[figure: |D|; β′; g′; B′′; β; D̄; g\underline{b}; B′]

with β′ ∈ S. Then we have: τp(αg′) = νp(β)p(g′) = νp(g)bp(β′) = τp(f)h̄p(β′). Since τ ∈ Σ there is t ∈ Σ, t : D′ → p(|D|) such that p(αg′)t = p(f)h̄p(β′)t. Choose |t| : |D′| → |D| cartesian over t. Then αg′|t| factors uniquely through f via an |h| : |D′| → V over h̄p(β′)t.

So upstairs we have:

[figure: A; V; ϕ; f; B; τ; |D′|; |h|; g′t; \underline{b}β′t; B′′; β; Y; A′; W; ψ; g; B′; ν]

and this gives the factorization. For (ρ, A′) and (ρp(ψ), W) represent the same object, and the span W ← |D| → V therefore gives the factorization [(ρ, A′)] → [(σ, A)] = [(σp(ϕ), V)], and the composition is clear.

For the universal property, if

[figure: E; p; F; H; r; B; g; C]

is a map of fibrations such that g inverts every map in g, then F inverts every map in S since cartesian over an iso implies being an iso; we can therefore define a unique (up to isomorphism) functor from G to H by sending the span [figure: A; V; ϕ; f; B] to F (f)F (ϕ)^{−1}.

The left exactness property is proved in a similar way as in [GZ].

In the case of a left exact fibration (by which I mean a fibration which is a finite limit preserving functor between left exact categories), or even just a fi-

bration [figure: E; p; B] such that B has pullbacks, a far more conceptual and simple proof

can be given, because the construction in the proof of theorem 2.1 is really a two-step construction: first add freely cocartesian arrows over arrows in Σ, and then force (by a calculus of fractions construction) these to be isomorphic to the existing cartesian arrows over arrows in Σ. First a theorem about preservation of coproducts in the situation where one inverts vertical maps.

Theorem 2.2 Let [figure: E; p; B] be a fibration and M a class of vertical maps in E which admits a calculus of right fractions, so [figure: E; p; B] factors through a functor E[M^{−1}] → B.

Then this functor is a fibration and P_{M} : E → E[M^{−1}] is cartesian.

Moreover, suppose Σ ⊂ B is a class of arrows such that [figure: E; p; B] has cocartesian

liftings over elements of Σ; then P_{M} preserves those cocartesian liftings if and only if the two following conditions hold:

1. Any diagram [figure: V′; τ′; X; f; Y] in E with f cocartesian over p(f) ∈ Σ and

τ′ ∈ M, can be completed to a commutative square [figure: V′; τ′; f′; V; τ; X; f; Y] with f′

cocartesian over p(f) and τ in P_{M}^{−1}(iso);

2. Any diagram [figure: V; τ; X; f; Y] with τ ∈ M and f cocartesian, can be completed

to a commutative diagram [figure: V′; τ′; f′; V; τ; X; f; Y] with τ′ ∈ M and f′ satisfying the

property: if k_{1}fs = k_{2}fs for s ∈ M and k_{1}, k_{2} a parallel pair with p(k_{1}) = p(k_{2}), then there is t ∈ M with k_{1}t = k_{2}t

Proof. Following [B1] I write p/M for the unique factorization of p through E[M^{−1}]. I prove that P_{M} preserves cartesian arrows; since E[M^{−1}] has the same objects as E, this shows that p/M is a fibration. If f : X → Y is cartesian w.r.t. p and (s, g) : Z → Y an arrow in E[M^{−1}] such that p/M((s, g)) factors through f, then g factors through f so (s, g) factors through f. As for uniqueness, suppose (s, g) and (t, h) represent maps in E[M^{−1}] such that f(s, g) = f(t, h) and p/M((s, g)) = p/M((t, h)) then p(g) = p(h) and there is a diagram

[figure: s; g; f; a; b; t; h; f]

with a, b vertical, fga = fhb. So ga = hb; so (s, g) and (t, h) represent the same map in E[M^{−1}]; so f is cartesian in E[M^{−1}].

Now suppose P_{M} preserves Σ-indexed coproducts. Condition 1) follows at

once: given [figure: V′; τ′; X; f; Y] , let f′ : V′ → V be cocartesian over p(f) at V′ and

τ : V → Y the canonical vertical. Then since P_{M}(f′) and P_{M}(fτ′) are both cocartesian, τ ∈ P_{M}^{−1}(iso). As for 2), since M is a calculus of fractions there is a square as pictured with τ′ ∈ M, and P_{M}(f′) will be cocartesian; so if k_{1}f′s = k_{2}f′s for k_{1}, k_{2}, s as in 2), then since f′s is also cocartesian in E[M^{−1}], k_{1} = k_{2} in E[M^{−1}]; so k_{1}t = k_{2}t for some t ∈ M.

Conversely, let the conditions hold and f : X → Y cocartesian in E. Given (τ′, g) : X → Z in E[M^{−1}] such that its image factors through f i.e. p(g) = hp(f)

for some h, since there is a square [figure: V′; τ′; f′; V; τ; X; f; Y] with f′ cocartesian, there is h̄ in

E over h with g = h̄f′ so (τ′, g) is the composition (τ, h̄)f. As for uniqueness, suppose for two arrows in E[M^{−1}]: (s_{1}, k_{1}) and (s_{2}, k_{2}) that their images are equal and (s_{1}, k_{1})f = (s_{2}, k_{2})f. Without loss of generality we may assume that s_{1} = s_{2} = τ, say. Find a square

[figure: V′; τ′; f′; V; τ; X; f; Y]

as in 2); the compositions are (τ, k_{i})f = (τ′, k_{i}f′) and they are equal in E[M^{−1}] which means there is a diagram

[figure: τ′; k_{1}f′; u; v; τ′; k_{2}f′]

with u, v ∈ M. Again, we may assume u = v and k_{1}f′u = k_{2}f′u. By property 2) then, k_{1}t = k_{2}t for some t ∈ M, which means that k_{1} = k_{2} in E[M^{−1}], so (τ, k_{1}) = (τ, k_{2}).

Theorem 2.3 Suppose the category B has pullbacks. Then the free fibration (in

the category of fibrations over B) on [figure: E; p; B] with the property that all reindexing

functors σ^{∗} for σ ∈ Σ are equivalences, can be constructed in the following way: first, let E′ be the category (E↓B) ∩ Σ, that is the category whose objects are pairs (A, σ) where A ∈ E and σ : p(A) → X is an element of Σ, and whose maps: (A, σ) → (B, τ) are pairs (f, m) with f : A → B and m : X → Y such that τp(f) = mσ. This is fibered over B by the functor which sends (A, σ) to the codomain of σ. Then take E′[M^{−1}], where M is the class of vertical maps (ϕ, id) with ϕ cartesian over p(ϕ) ∈ Σ.

Proof. Of course this follows by combining theorems 0.1 and 2.1 since the re-

quired fibration must be the pullback of the fibration [figure: G; q; B[Σ^{−1}]] constructed in 2.1,

along P_{Σ}. However there is an independent argumentation which also serves to explain the construction in 2.1. The category E′ is fibered over B since for an arrow m : X → Y in B and an object (B, τ : p(B) → Y) of E′, to get the cartesian over m one takes the pullback

[figure: p(A); σ; m′; p(B); τ; X; m; Y]

and chooses m̄ : A → B cartesian (w.r.t. p) over m′ at B. The point is, that [figure: E′; cod; B]

is the free fibration on [figure: E; p; B] with Σ-indexed coproducts: that is, E′ has cocartesian

liftings over all arrows in Σ, and any cartesian map E → H of fibrations over B for which H has Σ-indexed coproducts, factors through E′ by a cartesian functor E′ → H which preserves cocartesian arrows over elements of Σ. This is easy to check: an arrow (f, m) is cocartesian if and only if f is an isomorphism.

It is not hard to see that the class M admits a calculus of right fractions.

Moreover, all the canonical vertical comparison maps [figure: i; σ̄; \underline{σ}] and [figure: j; σ̄; \underline{σ}]be-

tween a cocartesian and a cartesian lifting of σ ∈ Σ, are in M, as is obvious. Furthermore, it follows by checking the conditions of theorem 2.2 for M that P_{M} preserves cocartesian liftings over elements of Σ. So in E′[M^{−1}], all the σ^{∗}’s are equivalences, and it follows that if K is the free one on [figure: E; p; B] with this property, we

have a unique (up to natural isomorphism) cartesian functor from K to E′[M^{−1}] over B. On the other hand, since K has Σ-indexed coproducts there is a unique one from E′ to K, preserving these coproducts; but this functor must invert all arrows in M since let (ϕ, id) : (A, σ : p(A) → X) → (B, τ : p(B) → X) an element of M. Then (ϕ, p(ϕ)) is cartesian: (A, id) → (B, id) and the cocartesian lifting over p(ϕ) at (A, id) lands at (A, p(ϕ)) so (ϕ, id) : (A, p(ϕ)) → (B, id) is a comparison map. But the map (ϕ, id) : (A, σ) → (B, τ) is the Σ_{τ}-image of this comparison map (Σ_{τ} being the left adjoint of τ^{∗}) which must be inverted since E′ → K preserves Σ-indexed coproducts. The only reason I asked for pullbacks in B in theorem 2.3 was, that without it, the functor cod from E′ = (E↓B) ∩ Σ to B, need not be a fibration and therefore the reasoning in the proof does not apply. However, the functor E′[M^{−1}] → B constructed there always is, and it is equivalent (as a fibration over B) to the pullback along P_{Σ} : B → B[Σ^{−1}] of the fibration G → B[Σ^{−1}] constructed in 2.1.

So we can always apply the construction in 2.3, even if B does not have pullbacks. By the pullback property then, we know that the resulting fibration has fibrewise categorical property P if and only if G → B[Σ^{−1}] has (categorical=stable under equivalences).

Proposition 2.4 The construction of 2.3 preserves the properties of being fibrewise a preorder and of being fibrewise a groupoid. The construction of 2.1 moreover preserves the property of being fibrewise discrete. The resulting functor from Set^{Bop} to Set^{B[Σ^{−1}]op} is (P_{Σ})_{!}, the left Kan extension along P_{Σ}^{op}.

Proof. Recall that [figure: E; p; B] is fibrewise a preorder if and only if p is faithful, and [figure: E; p; B]

is fibrewise a groupoid if and only if every map in E is cartesian.

So let [figure: E; p; B] be faithful and

[figure: A; σ; ϕ_{1}; ϕ_{2}; B; τ; X; f; Y]

two maps in E′ (notation from 2.3) over the same map in B; since τp(ϕ_{1}) = τp(ϕ_{2}) there is a ψ ∈ Σ, ψ : C′ → p(A) with p(ϕ_{1})ψ = p(ϕ_{2})ψ. Pick \underline{ψ} : C → A cartesian over ψ. Then since p is faithful, ϕ_{1}ψ = ϕ_{2}ψ where now \underline{ψ} is a map:

[figure: C; σψ; X] → [figure: A; σ; X]

in E′ over the identity on X. But this means that the two maps ϕ_{1}, ϕ_{2} will be equal in E′[M^{−1}].

If [figure: E; p; B] is fibrewise a groupoid, let [figure: A; σ; A′; ψ; ϕ; σ′; B; τ; X] represent a vertical map

in E′[M^{−1}]; then assuming Σ saturated, since τp(ϕ) ∈ Σ, p(ϕ) ∈ Σ and ϕ is cartesian because all maps are; so the map is iso.

Moreover, if in the case of construction 2.1 we have that the original fibration is discrete, then certainly the new one is fibrewise a preorder and a groupoid, but then for any vertical map the domain and codomain are the same object, and the unique iso is the identity. The statement about the functor between presheaf categories is an easy verification.

3 Some mathematical examples

3.1 Filter quotient toposes and germs of topological spaces

Let Et^{∗} denote the category of étale maps Y → (X, ∗) of topological spaces, where ∗ is a point in the base space X; maps are commutative squares of spaces, where the base map preserves the base point.

Et^{∗} is fibered over Top^{∗} (the category of topological spaces with a base point), and the fibre over the space (X, ∗) is the topos of sheaves over X. Let Σ ⊂ Top^{∗} consist of the open embeddings. It is clear that Top^{∗}[Σ^{−1}] is the category with as maps the germs of maps (X, ∗) → (Y, ∗). It is easy to see what the fibers of the fibration over Top^{∗}[Σ^{−1}], resulting from the construction in 2.1, will be: namely, the fiber over (X, ∗) is the quotient of Sh(X) by the neighborhood filter of ∗. This is because the fiber over object X in B[Σ^{−1}], is the colimit of the fibers E_{Y} for all σ : Y → X ∈ Σ. The filter quotient construction is described in detail in [MM].

It should be noted that the filter quotient construction itself is an example of 2.1. Every topos E is fibered over the lattice Sub(1) of subobjects of 1, in the sense that over U ≤ 1 we have the slice E/U. Given a filter U on Sub(1), the class of those inequalities U ≤ V such that for some S ∈ U, S ∧ U = S ∧ V, admits a calculus of right fractions, resulting in the fraction category (poset) Sub(1)/U; and the new fiber over 1 (applying 2.1) is the filter quotient E/U.

3.2 Subtoposes of the effective topos

Let R be the category of subsets of IN and partial recursive functions: a map f : A → B in R is the restriction to A of a partial recursive function which is defined on A and lands in B.

R is fully embedded in the effective topos Eff as ¬¬-closed subobjects of N (N denotes the natural numbers object of Eff), and I denote its image under the embedding also by R. The fibration Eff_{R} → R is the restriction of the codomain fibration to R.

[RR] show that this fibration arises from the following construction. Let Proj_{R}

be the fibration over R defined by: objects are diagrams X −▷^{f} I →^{α} J with X a set, I →^{α} J in R and f a surjection of sets. Maps are commutative diagrams

[figure: X; f; X′; f′; I; α; I′; α′; J; J′]

with the top row a map in Set and the bottom square in R. This is fibered over R by the functor which takes the last component (Proj_{R} is itself a kind of universal construction, but that doesn’t concern me here). Now Eff_{R} is the fiberwise exact completion of Proj_{R}. This is a construction which can be performed on any left exact fibration, and goes as follows (the reader is referred to [CCM] or [RR] for

unexplained notions): given a left exact fibration [figure: E; p; B], let the objects of E_{ex} be

vertical pseudoequivalence relations (i. e. \xymatrix{R \ar[r] \ar[r] & X} are vertical maps, as well as those maps witnessing that it is a pseudoequivalence relation), and morphisms

from [figure: R; r_{1}; r_{2}; X] to [figure: S; s_{1}; s_{2}; Y] are equivalence classes of arrows X →^{f} Y such that

for some ϕ : R → S we have fr_{i} = s_{i}ϕ (i = 1, 2). Two such f, f′ are equivalent if for some T : X → S, s_{1}T = f and s_{2}T = f′.

Let’s call a fibration fiberwise exact if it is left exact, every fiber is exact and reindexing preserves the exact structure (quotients of equivalence relations). Every map: E → F of fibrations over B such that F is fiberwise exact, factors essentially uniquely through E_{ex} → F which preserves the fiberwise exact structure. By an easy adaptation of the theory of exact completions (see [CCM] or [RR]), a fiberwise exact fibration is of form E_{ex} if and only if every fiber has enough projectives, the category of projectives in each fiber is left exact, and reindexing preserves projectives in the fibers. In that case, it is the fiberwise exact completion of its subfibration of projectives in the fibers.

Now [RR] remark that their construction of Eff applies as well to any other Eff-like topos, constructed over another partial combinatory structure. In particular, one can look at the structure of A-recursive functions for a subset A ⊂ IN. Computing these functions, one is allowed to consult an “oracle” which gives answers to the question x ∈ A? for any x; of course this begins to be interesting when A is not recursive. One has a topos Eff_{A} and it is known ([Hy], [P]) that Eff_{A} is a sheaf subtopos of Eff. Let R_{A} be the analogon of R with respect to A-partial recursive functions. One has the fibration (Eff_{A})_{R_{A}} → R_{A}, and it is likewise the exact completion of a left exact fibration Proj_{R_{A}} → R_{A}.

Theorem 3.1 R_{A} arises as a calculus of fractions construction out of R, and the construction of 2.1, applied to the fibration Eff_{R} → R with respect to this calculus of fractions, yields (Eff_{A})_{R_{A}} → R_{A}.

Proof. Assume some standard, primitive recursive coding of finite sequences of natural numbers, written ⟨x_{1}, …, x_{n}⟩. Say that σ ∈ IN is an A-information sequence if σ is of form ⟨⟨x_{1}, i_{1}⟩, …, ⟨x_{n}, i_{n}⟩⟩ where x_{1} < … < x_{n} and for all k, 1 ≤ k ≤ n, i_{k} = 0 if x_{k} ∈ A, and i_{k} = 1 otherwise. In particular, the empty sequence ⟨⟩ is an A-information sequence.

Let the class P of arrows in R be defined by: X′ →^{π} X is in P if and only if X′ is of form X′ = {⟨x, σ_{x}⟩ | x ∈ X}, where all σ_{x} are A-information sequences, π is the projection ⟨x, σ_{x}⟩ ↦ x, and there is a machine M which, consulting an oracle, for all x ∈ X has a terminating A-recursive computation and σ_{x} codes exactly the information about A this computation requires.

Let Σ be the class of arrows in R which are of form →^{f} or →^{f}→^{π} with f iso and π ∈ P. I show that Σ admits a calculus of right fractions, and that R_{A} is isomorphic to R[Σ^{−1}].

First, given X →^{π} Y →^{f} Z with π ∈ P and f iso, there is a commutative diagram

[figure: X; g; π; Y; f; X′; π′; Z]

with g iso and π′ ∈ P, for if X = {⟨y, σ_{y}⟩ | y ∈ Y } let X′ = {⟨z, σ_{f^{−1}(z)}⟩ | z ∈ Z}. Secondly, given X →^{π} Y →^{π′} Z with π, π′ ∈ P, there is a commutative diagram

[figure: X; g; π; Y; π′; X′; π′′; Z]

with g iso and π′′ ∈ P. For, if X = {⟨y, σ_{y}⟩ | y ∈ Y } and Y = {⟨z, τ_{z}⟩ | z ∈ Z}, let X′ = {⟨z, τ_{z} ∘ σ_{⟨z,τ_{z}⟩}⟩ | z ∈ Z} where τ_{z} ∘ σ_{⟨z,τ_{z}⟩} is the A-information sequence obtained by taking the union of the sequences τ_{z} and σ_{⟨z,τ_{z}⟩}. Suppose M computes A-recursively τ_{z} for each z, and N computes likewise σ_{y} for each y. Then there is obviously a machine which A-recursively computes τ_{z} ∘ σ_{⟨z,τ_{z}⟩} for each z. So π′′ ∈ P. To show that g is iso, adapting M to act on ⟨z, τ_{z} ∘σ_{⟨z,τ_{z}⟩}⟩, let it act on z and instead of asking the oracle, consult the second part of the input τ_{z} ∘ σ_{⟨z,τ_{z}⟩}. This yields ⟨z, τ_{z}⟩ and repeating this with N gives the required inverse of g′.

¿From these two remarks it follows that Σ is closed under composition. It trivially contains all identities, and since all arrows in Σ are mono in R the last axiom for a calculus of fractions is trivially verified.

Furthermore, given [figure: X; π; Z; f; Y] with π ∈ P, there is a pullback diagram

[figure: W; g; f′; X; π; Z′; π′; Z; f; Y]

in R, with g iso and π′ ∈ P. For let Z′ = {⟨z, σ_{f(z)}⟩ | z ∈ Z}, then Z′ ≃ {⟨⟨y, σ_{y}⟩, z⟩ | y ∈ Y, z ∈ Z, f(z) = y} = {⟨x, z⟩ | πx = fz}.

Finally, note that any arrow f : X → Y in R_{A} fits in a diagram

[figure: X′; π; f′; X; f; Y] with f′ and π in R, and π ∈ P; from this one easily deduces

that R_{A} is isomorphic to R[Σ^{−1}].

The last remark may be strengthened a bit by noting that for every commu-

tative square [figure: J; g; l; H; h; K; f; L] in R_{A} with g and h in R, and every such resolution [figure: K′; π; f′; K; f; L] with π ∈ P and f ∈ R, there is a commutative prism

[figure: J′; π′; l′; J; l; g; H; K′; π; f′; K; f; L]

with π′ ∈ P, l′ ∈ R.

To show that the fibration Proj_{R_{A}} → R_{A} arises from Proj_{R} → R by applying the construction of 2.1 w.r.t. the class Σ, write E for Proj_{R}, and let E′ and M be as in 2.3. A typical object of E′ is of form

[figure: X; I; α; J; σ; K]

with σ ∈ Σ; send this to X−▷I →^{σα} K. This defines a functor E′[M^{−1}] → P_{Σ}^{∗}(Proj_{R}) over R which, by the help of the prism remark, is seen to be fully faithful and essentially surjective on objects.

The final statement of the theorem now follows from the following lemma.

Lemma 3.2 Let [figure: E; p; B] be a left exact fibration. Then the construction of 2.3 (hence

that of 2.1) commutes with fibrewise exact completion: writing Σ(E) → B for the effect of construction 2.3 on E → B, Σ(E_{ex}) is equivalent to (Σ(E))_{ex} as fibrations over B.

Proof. This is a simple consequence, by the universal properties of these constructions, of the following two remarks:

1) If E → B is such that the reindexing functors σ^{∗} for all σ ∈ Σ are equivalences, then the same holds for E_{ex} → B.

For, a map [f] : \xymatrix{S \ar[d] \ar[d] \\ Y}→ \xymatrix{R \ar[d] \ar[d] \\ X}between vertical pseudoequivalence relations is carte-

sian in E_{ex} if and only if \xymatrix{S \ar[d] \ar[d] \\ Y}is isomorphic to (pf)^{∗}( \xymatrix{R \ar[d] \ar[d] \\ X}), where (pf)^{∗} is reindexing

in E.

Similarly, if E → B has cocartesian liftings over σ ∈ Σ such that the corre-

sponding coproduct functors Σ_{σ} are left exact, and [f] : \xymatrix{S \ar[d] \ar[d] \\ Y}→ \xymatrix{R \ar[d] \ar[d] \\ X}is over pf ∈ Σ,

then this is cocartesian if and only if \xymatrix{R \ar[d] \ar[d] \\ X}is isomorphic to Σ_{pf}( \xymatrix{S \ar[d] \ar[d] \\ Y}).

Alternatively, using choice to obtain a cleavage for E → B and using the 2functoriality of the construction (−)_{ex}, one sees that it must preserve equivalences.

2) If E → B is fiberwise exact then so is Σ(E) → B. For again, let E′ and M as in 2.3. To find the regular epi-mono factorization of a

typical vertical map [figure: A; σ; V; ϕ; f; B; τ; X] , factor f as \underline{f}i with \underline{f} cartesian and i ver-

tical (w.r.t. E → B); and factor i. This is obviously stable under pullback. Since

τp(f) = σp(ϕ) ∈ Σ, the map [figure: V′; τp(f); \underline{f}; B; τ; X] is in M. To see that equivalence

relations are effective, it suffices to observe that every vertical equivalence relation in Σ(E) is isomorphic to a suitable coproduct of vertical equivalence relations in E. This goes as follows: let

[figure: R; τ; V; ϕ; f_{1}; f_{2}; A; σ; X]

a typical equivalence relation in E′[M^{−1}]. Since σp(f_{1}) = σp(f_{2}) there is ψ : p(C) → p(V) in Σ with p(f_{1})ψ = p(f_{2})ψ Choose \underline{ψ} : C → V cartesian over ψ and let C′ →^{q} A cartesian over p(f_{1})ψ. There are vertical maps [figure: C; q_{1}; q_{2}; C′] which

are the unique factorizations of f_{i}\underline{ψ} through q. [figure: C; q_{1}; q_{2}; C′] may not be a vertical

equivalence relation in E, but pulling it back along a suitable element of Σ we get one, and that one is the kernel pair of its quotient, since E → B is fiberwise exact. This structure can then be transferred back again.

Alternatively, using choice to obtain a cleavage for E → B, one may observe that exactness is the kind of structure that is preserved under filtered colimits.

There is a point about the definition of Σ in the proof of theorem 3.1 which I think deserves to be made, although I’m not sure I understand the significance of it. The definition is sufficiently “effective”, that is the axioms for a calculus of fractions are validated recursively in indices for the morphisms of R (e.g. given

[figure: f; σ] with σ ∈ Σ, one can get indices for σ′, f′ with σf′ = fσ′ recursively in

indices for σ and f; and given an index m̄ of a machine which A-recursively computes m : A → B in R_{A} one can find, recursively in m̄, indices for its resolution

[figure: A′; π; m′; A; m; B] with π ∈ Σ).

This means the following. R lives as internal category in Eff and there is an internal functor p : R → Ω displaying Ω as the poset reflection of R in Eff. Now the above remark entails that we can carry out the calculus of fractions construction R[Σ^{−1}] in Eff, and prove that it is isomorphic to R_{A} (which also lives in Eff). The poset reflection of R_{A} is Ω_{A}, the object of closed truth values for the topology j_{A} giving Eff_{A} as subtopos of Eff, and there is a commutative diagram

[figure: R; p; P_{Σ}; R_{A}; p_{A}; Ω; j_{A}; Ω_{A}]

in Eff.

This must have some meaning for the internal logic of Eff. For example, suppose that Σ is an internal calculus of fractions in Eff, such that P_{Σ} : R → R[Σ^{−1}] has a full and faithful right adjoint. This adjunction carries over to the poset reflections, giving an internal topology in Eff.

Acknowledgements. I thank John Power, Anders Kock and Ieke Moerdijk, who expressed interest in this work by asking questions and suggesting further topics of research.

I thank especially Claudio Hermida for many discussions; he also brought a lot of material to my attention and supplied some otherwise inaccessible material of J. Bénabou.

Finally, I thank BRICS for support, and its local leader Glynn Winskel and his close colleagues for creating an extremely pleasant working atmosphere at the department of Datalogi in Århus.

References

[B1] J. Bénabou, Some remarks on 2-categorical algebra (part I), Bulletin de la Société Mathématique de Belgique (série A), Tome XLI (1989), fascicule 2, pp.127-94

[B2] J. Bénabou, Some geometrical aspects of the calculus of fractions, talk at the ECCT conference in Tours, July 1994

[CCM] A. Carboni & R. Celia Magno, The free exact category on a left exact one, Journal of the Australian Mathematical Society 33A (1982), 295-301

[GZ] P. Gabriel & M. Zisman, Calculus of Fractions and Homotopy Theory, Springer, Berlin 1967

[H] C. Hermida, Some properties of Fib as a fibered 2-category, Århus 1994, manuscript

[Hy] J.M.E. Hyland, The effective topos, in: Troelstra & Van Dalen (eds.), The L.E.J. Brouwer Centenary Symposium, Studies in Logic, Amsterdam 1982, pp. 165-216

[PTJ] P.T. Johnstone, Fibrations and partial products in a 2-category, Applied Categorical Structures 1(1993), pp.141-179

[MM] S. MacLane & I. Moerdijk, Sheaves in Geometry and Logic, Berlin (Springer) 1992

[P] W. Phoa, Relative computability in the Effective topos, Mathematical Proceedings of the Cambridge Philosophical Society 106 (1989), pp. 419-422

[RR] E. Robinson & G. Rosolini, Colimit completions and the effective topos, Journal of Symbolic Logic 55 (1990), pp. 678-699

Recent Publications in the BRICS Report Series

RS-94-37 Jaap van Oosten. Fibrations and Calculi of Fractions. November 1994. 18 pp.

RS-94-36 Alexander A. Razborov. On provably disjoint NP-pairs. November 1994. 27 pp.

RS-94-35 Gerth St�lting Brodal. Partially Persistent Data Structures of Bounded Degree with Constant Update Time. November 1994. 24 pp.

RS-94-34 Henrik Reif Andersen, Colin Stirling, and Glynn Winskel. A Compositional Proof System for the Modal μ-Calculus. October 1994. 18 pp. Appears in: Proceedings of LICS ’94, IEEE Computer Society Press.

RS-94-33 Vladimiro Sassone. Strong Concatenable Processes: An Approach to the Category of Petri Net Computations. October 1994. 40 pp.

RS-94-32 Alexander Aiken, Dexter Kozen, and Ed Wimmers. Decidability of Systems of Set Constraints with Negative Constraints. October 1994. 33 pp.

RS-94-31 Noam Nisan and Amnon Ta-Shma. Symmetric Logspace is Closed Under Complement. September 1994. 8 pp.

RS-94-30 Thore Husfeldt. Fully Dynamic Transitive Closure in Plane Dags with one Source and one Sink. September 1994. 26 pp.

RS-94-29 Ronald Cramer and Ivan Damg� ard. Secure Signature Schemes Based on Interactive Protocols. September 1994. 24 pp.

RS-94-28 Oded Goldreich. Probabilistic Proof Systems. September 1994. 19 pp.

RS-94-27 Torben Bra� uner. A Model of Intuitionistic Af�ne Logic from Stable Domain Theory (Revised and Expanded Version). September 1994. 19 pp. Full version of paper appearing in: ICALP ’94, LNCS 820, 1994.