Practical Foundations of Mathematics

Paul Taylor

9.2  Indexed and Fibred Categories

In the familiar predicate calculus, propositions may depend on elements of sets, but sets do not depend on the actual proofs of propositions. The technology used to take advantage of this separation principle pre-dates the formal study of syntax: it was introduced for algebraic geometry in 1960 by Alexander Grothendieck [Gro64, Exposé VI], to handle the way in which an arbitrary mathematical structure (rather than simply a predicate) varies over an indexing space. John Gray developed the category theory [Gra66]. In 1970, Bill Lawvere applied it to what we would now call type theory, and Jean Bénabou used it to account for the infinitary aspects of category theory.

Separating propositions from types   Instead of beginning, as is usual, with the formal definition of fibrations, let us first consider the feature of the predicate calculus which lies behind it (Remark 9.1.1(b)); Bart Jacobs called this a propositional situation [Jac90].

DEFINITION 9.2.1 Let S = S_type+S_prop be a partition of the class of types of a generalised algebraic theory L (Definition 8.1.10), the members of the second class being styled ``propositions.'' Then L is said to admit a division of contexts if

(a)

the types do not depend on propositional variables,

omitted prooftree environment

(b)

the type terms do not depend on propositional variables,

omitted prooftree environment

(c)

and likewise the laws for type terms,

omitted prooftree environment

So certain converses of weakening hold. Using the exchange rule,

The point is that every jumbled context is isomorphic to a divided one.

We shall study the full subcategory Cn^×_type|prop Ì Cn^×_L of divided contexts. The conditions say that this inclusion is an equivalence, so our results about divided contexts actually apply to the whole category.

We shall write ® for the display maps corresponding to the types and \hookrightarrow for the propositions (Notation  9.1.3). According to the predicate convention, the latter are not necessarily monos.

LEMMA 9.2.2 Every pair of displays GfX® [l = 2.5em]^{[^(x)]}Gf\hookrightarrow [l = 2.5em]^{[^(y)]}G is part of a ( P-) pullback,

PROOF: GfX º GX¢f by (a) and the R equation (Remark 8.2.8). The second diagram follows from (b) and uniqueness from (c). []

Parts (b) and (c) of Definition 9.2.1 say that, given a morphism of divided contexts, we may erase all propositional information: this is well defined as a functor, the fibration. So the tree structure in John Cartmell's contextual categories (Remark 8.3.9) may be pruned to the types. We write ® for the fibration, as it ``displays'' propositions over types.

PROPOSITION 9.2.3 Let Cn^×_type be the full subcategory consisting of those contexts which only involve types. Then there are adjoint functors,

omitted diagram environment

where P forgets the propositional part of a divided context and T gives an empty propositional part to a type-only context. Cn^×_type|prop is called the total category and P the fibration.

For each object G of Cn^×_type (known as the base category), the fibre is the relative slice Cn^x¯ G, whose objects are contexts of the form [G|F] and whose morphism act as the identity on G. TG º [G|] is the terminal object of the fibre over G.

(a)

Syntactic substitution defines a functor

u^*: Cn^x¯ G® Cn^x¯ D for u:D® G; moreover

(u;|)^* f = u^*(|^*f) and id^*f = f.

(b)

Semantically, the analogous operation is pullback (inverse image), but this is only defined up to unique isomorphism.

PROOF: Notice that P cannot be defined for types which depend on the omitted propositional variables. The other two parts of Definition  9.2.1 are needed to define P on morphisms involving type operation-symbols, such that the laws are respected. The substitution functors were defined in Section 8.2 and TG is terminal in the relative slice by Lemma 8.2.10. []

EXAMPLES 9.2.4

(a)

Sets and predicates. The fibre over G is the Lindenbaum algebra of predicates with free variables in G with respect to the provability order; TG is the constantly true predicate. Semantically, the fibre is the powerset P(G), consisting of subsets of [[G]] . The substitution functor u^* is the inverse image u^-1; notice that it preserves Þ , Ú and Ù, and has adjoints on both sides (Remark 3.8.13(b)).

(b)

In declarative programs, the types are those of the run-time program-variables but the propositions or midconditions only appear in the analysis, which may perhaps be carried out by a proof- checking compiler (Remark 5.3.3). The fibration P erases the midconditions (on objects), and the correctness proofs from programs (morphisms). The substitution functors give the weakest precondition interpretation of Remark  4.3.5ff.

(c)

If the types of both kinds are independent of each other's terms then Cn^×_type|prop = Cn^×_typexCn^× _prop, the two projections being fibrations. The normal form theorem (Lemma 8.2.10) expresses each morphism of the product as a commuting pair, as in Proposition  4.8.3.

(d)

Three or more kinds obeying the analogous exchange rules give rise to three-part contexts [G|F|L ], and to a composition of fibrations.

(e)

Let L = (S,\triangleright ) be a propositional Horn theory (Section 3.7). Suppose that

S = S_type+S_prop such that Definition  9.2.1(b) holds, ie if K\triangleright t Î S_type then already \dgmK_type º KÇS_type\triangleright t. Let L _type be S_type with the restriction of \triangleright . Then there is a division of the contexts in the classifying semilattice of L (Theorem  3.9.1).

(f)

The classifying category Cn^× _type for the theory of rings has lists of polynomials as morphisms. Contexts for the theory L of rings-with-modules divide into two parts, of which the first refers purely to rings (Exercise  4.23). The dependency of modules on rings is not at the type level, but is due to the term (action) RxM® M.

(g)

The theory of categories (Example  8.1.12) admits a division into objects (O) and morphisms (H[x,y]), if the operation-symbols src and tgt are omitted from the theory ( cf Example 8.2.1 and Exercise 8.1). Similarly the theory of 2-categories is fibred over the theory of categories, dividing natural transformations from functors.

(h)

Let L_type consist of the sorts and operation- symbols of an algebraic theory. Then the laws of the given theory, together with reflexivity, transitivity, symmetry and congruence with respect to each of the operation-symbols, may be formulated as L_prop (Remark 7.4.10).

(i)

More generally, let L be a conservative extension of a generalised algebraic theory  L_type: the type-symbols of L_type are defined in type-only contexts, as are all operation-symbols and laws of L whose types are in L_type. The levels of a stratified algebraic theory (Definition 8.1.11) are successive conservative extensions.

(j)

Let C be a category with two classes D and M of displays (Definition 8.3.2) satisfying Lemma 9.2.2. Then there is a fibration C\relcomma_D|M1® C \relcomma_D1 of relative slices (Definition  8.3.8).

EXAMPLE 9.2.5 An I-indexed family of objects (\typeX_i)_{i Î I} is a context

Jean Bénabou explained how the dependent sum Si:I.X[i] and product Pi:I.X[i], which we study in the next two sections, give an elementary axiomatisation of coproducts and products of infinitary indexed families of sets or other mathematical objects. We regard X[i] and Si.X[i] as idiomatic notation for the associated display map. The previous chapter developed this notation and its formal interpretation.

In practice, more than one such suffix (i:I, j:J, ...) is often needed, so it is better to write [G | x:X] than to collect I, J, ... as a single type IxJ or Si:I.J[i] (category theory exists to eliminate suffixes from mathematics). There may also be several I-indexed families (\typeX_i), (\typeY_i), ..., from which we may for example need to select tuples, so these too we keep together in the many-type divided context [G|F].

I find this example very confusing as the main use used to demonstrate the theory of fibrations, for one thing because the category of sets is too special to illustrate many of the difficulties, such as the Beck-Chevalley condition and quantification over equality (Remark 8.3.5). But, in terms of our definition, lemma and proposition above, how can the principle of independence possibly apply, when the types on both sides of the division are of the same kind (sets)? Making such a division cannot be expressing any semantic fact about the theory of sets: it is a convention:

we don't use elements of indexed sets as indices.

In the process of inventing a formal language with divided contexts that uses displays of sets on both sides, we ``taint'' the displays by their use in the two roles: we take the same class twice, or one class and a subclass M of it, and mark the copies as ``types'' and ``propositions.'' Then the formal language ( ie the arguments we permit ourselves to write in it), is artificially restricted according to the rules in Definition  9.2.1. The axiom of comprehension forgets this restriction (Section 9.5).

Fibrations   The ``substitution'' functors have a universal property, which (like adjunctions) we may capture without making choices of them.

DEFINITION 9.2.6 Let P:C® S be any functor.

(a)

For any object G Î obS, a map g:F® Y with

PF = PY = G and Pg = \id_G in C is called vertical. The subcategory P^-1(G) is known as the fibre over G; its objects are those F Î obC with

PF = G and its maps are the vertical ones. A morphism that is merely made invertible by P (not necessarily an identity) is called pseudo-vertical.

(b)

A morphism \nearrow :Y® Q in C is said to be horizontal, prone or cartesian if it has the universal property illustrated in the right hand diagram below, in which

| = P\nearrow :D = P Y® X = P Q: given any map F® Q whose image factors into | in the sense of forming a commutative triangle in S as illustrated, there is a unique fill-in F® Y such that the upper triangle commutes and the image is the given map G® D.

(c)

The functor P is a fibration if for every object Q Î obC and map

|:D® X = P Q in S there is a prone lifting \nearrow :Y ® Q with P Y = D and P\nearrow = |. In this case the source, C, and target, S, of P are called the total category and base category respectively. omitted diagram environment

(d)

Dually, s:F® Y is called op- horizontal, supine or cocartesian if it has the property shown on the left; P is an op-fibration if each base map u:G® D has a supine lifting at each object F over G.

So P:C® S is an op-fibration iff P:C^op® S^op is a fibration.

(e)

A functor which is both a fibration and an op-fibration is known as a bifibration. This is the case iff the substitution functors are adjunctible, the unit and co-unit being the comparisons between prone and supine maps whose targets and sources agree, respectively.

(d)

A hyperdoctrine is a fibration P:C® S where S and the fibres \nearrow [thick](G) for G Î obS are locally cartesian closed, and the substitution functors u^*:\nearrow [thick](D) ® \nearrow [thick](G) for u:G® D in S have adjoints on both sides obeying the Beck-Chevalley conditions. (As we do not follow Lawvere's approach, we don't use the word hyperdoctrine.)

PROPOSITION 9.2.7 Let \nearrow [thick](-):S^op® Cat be any functor, where we write u^*:\nearrow [thick](D)® \nearrow [thick](G) instead of \nearrow [thick](u) for the action of maps in S. Then the following define a fibration P:C® S:

omitted diagram environment

(a)

the objects of C are pairs, which we write as [G|F], consisting of G Î obS and F Î ob\nearrow [thick](G); and then P[G|F] = G;

(b)

the morphisms [G|F]® [D|Y] are also pairs [u|f], where u:G® D and f:F® u^*Y in \nearrow [thick](G), and then P[u|f] = u;

(c)

vertical morphisms are those of the form [id| f], and the fibre over G is isomorphic to the category \nearrow [thick](G);

(d)

the prone lifting of |:D® X at [X|Q] is

\vQ º [||\id|*Q] :[D||*Q]® [X|Q]

(e)

the composite [u|f];[||g] is [u;||f;u^*g] ( cf Definition  8.4.6(f)).

PROOF: Associativity of composition in C depends on functoriality of \nearrow [thick](-). The mediator for [u;||f] in the universal property of the prone map [||id] is [||g]. Conversely if [||g] is prone then g is invertible, since [u|id] is also prone. Everything else in the definition of fibration is straightforward. []

EXAMPLES 9.2.8 As the data for Proposition 9.2.7 consist merely of an assignment of a category to each object of the base category (in a functorial way), examples of fibrations are not difficult to find.

(a)

For sets and predicates, the total category is the comma category M¯ Set (Remark  9.1.4), of which an object is a set with a subset.

(b)

For indexed families (Example 9.2.5), tgt:Set^® ® Set is the fibration. (Section 9.5 takes up these two examples.)

(c)

Any fibration is a replete functor (Definition  4.4.8(d)), so its strict pullback U^*P against any functor U:A® S is equivalent to the pseudo-pullback (Definition 7.3.9). This is also a fibration, whose fibres over A Î obA are isomorphic to those over UA Î obS. For example, p₁ = U^*tgt in the gluing construction ( Proposition 7.7.1).

(d)

A presheaf S^op® Set is an indexed discrete category. It gives rise to a discrete fibration, characterised by the fact that all vertical maps are identities, eg Remark  7.7.8. Any indexed category S^op® Cat is a (pre)sheaf of categories, or an internal category in Shv( S).

(e)

In an indexed groupoid, all maps are prone, and all vertical maps are isomorphisms. The restriction of the fibration to each slice ( sic, not fibre) C¯ Q ® S¯ PQ is an equivalence of categories ; any functor with the latter property is called an isotomy and is weakly equivalent to a fibration with groupoid fibres.

(f)

A groupoid homomorphism is a fibration iff it is an op-fibration iff it is replete. The substitution functors are equivalences.

(g)

Any continuous function f:X® Y between spaces induces a homomorphism of their fundamental groupoids p₁(f):p₁(X)® p₁(Y). This is a fibration iff the weak path lifting property holds: for every point x Î X and path q:I º [0,1]® Y with f(x) = q(0), there is some path p:I® X with p(0) = x whose image fop is homotopic (relative to the endpoints) to q.

PROPOSITION 9.2.9 Let L_type Ì L be generalised algebraic theories, one a conservative extension of the other. Then there is a bifibration of their categories of models, which has adjoints on both sides.

omitted diagram environment

Let u:R® S be a homomorphism in the sub-theory ( L_type).

(a)

In the final algebra for the larger theory (L) in the fibre over R, the interpretation of each ``proposition'' is a singleton.

(b)

For an algebra N over S, the restriction along R® S has the same interpretation of ``types'' as R, but the `` propositions'' and actions are obtained from those of S by substitution.

(c)

The initial algebra over R is that generated by R together with the ``propositional'' operation-symbols, modulo ``propositional'' laws,

(d)

and induced algebras are computed in a similar way. []

EXAMPLES 9.2.10

(a)

Let u:R® S be a homomorphism of commutative rings and M, N be modules for R and S respectively. Then

RxN® [l = 3em](u,id) SxN® [l = 3em]N

is the action of the restriction of N to R, and the left adjoint M® SÄ_RM is known as induction (not in the logical sense).

(b)

Let

S = S_type+S_prop be a divided Horn theory, M,N Ì S two closed subsets and u:R = MÇS_type Ì S = NÇS _type. Then the initial algebra in the fibre over R is the closure of R with respect to the larger theory; the final one is R+S_prop. The restriction of N is R+NÇS _prop, and the induction of M is the closure of MÈS.

For finitary theories, the restriction functors preserve filtered colimits. Restriction and induction maps between algebraic lattices are called projections and embeddings respectively (Exercises  9.10ff). []

Coherence issues   For any (``semantically given'') fibration, a choice of prone liftings \nearrow :Y® Q for each | and Q is called a cleavage, and extends to ``substitution'' functors |^* between fibres. A split fibration is one for which these act functorially, as they do for syntactic categories. In general, the natural isomorphisms between (u;|)^* and u^*·|^* in a cleavage must be specified, and obey a system of coherence laws.

These isomorphisms are defined by universal properties, so are uniquely determined by certain equations. However, as Jean Bénabou rather forcefully pointed out [B \' en85], there is a casual tendency just to call them ``canonical'' - as if this were an intrinsic property like continuity. The problem is that if isomorphisms are not kept under strict control, they conspire to form non-trivial groups.

PROPOSITION 9.2.11 A group homomorphism P:C® S is a fibration iff it is surjective, and the fibre over the unique object of S is the kernel,

EXAMPLES 9.2.12

(a)

Every product projection in Gp is a split extension, for example the Klein 4-group (Z/(2))² \twoheadrightarrow Z/(2), where Z/(2) is cyclic of order 2.

(b)

Symm3\twoheadrightarrow Z/(2) is a split extension with kernel Z/(3), but not a product, where Symm3 is the non-Abelian group of order 6.

(c)

Z/(4)\twoheadrightarrow Z/(2) is not a split extension, since it cannot be described by conjugation, all three groups being Abelian.

(d)

The squaring map S¹\twoheadrightarrow S¹ on the unit circle S¹ Ì C (Examples 2.4.8 and 6.6.7) is a non-split extension of topological groups.

(e)

There is a double cover SU₂\twoheadrightarrow SO₃, where SO₃ is the group of rotations of the sphere S² = {(ix,y+iz)|x²+y²+z² = 1} Ì C² and SU₂ consists of the complex matrices ((a  b) || ( c  d)) with a c^*+b d^* = 0 and |a|²+|b|² = |c|²+|d |² = 1, which acts by conjugation. This has a manifestation in quantum mechanics called the Pauli exclusion principle: electrons have a non- geometrical property called ``spin'' which changes sign if the particle is rotated through 360^o, whereas it stays the same for photons.

REMARK 9.2.13 Let [`(u)] Î C be a cleavage, ie a choice of pre-images (prone liftings) for each u Î S. This is also known as a transversal for the normal subgroup K\triangleleftC. Then

Example 9.2.12(d) is a topological group. In this case, the base S¹ can be covered by open subsets (in the sense of Section 3.9) for each of which the two square roots may be distinguished continuously. The indexation is now over the frame W(S¹) of open subsets of the circle, but it is also necessary to say how these (and things defined over them) are pasted together with respect to the coverage. A fibration which respects this pasting is called a stack, or champs in French. (The French for a field of numbers is corps, but beware that Bénabou has used the word corpus in yet another sense!) For an account of the Grothendieck school's approach to fibred categories, see [Gir71], in which Jean Giraud studies non-Abelian cohomology of topological groups up to dimension 3. []

Stacks arise in type theory too, for example to say that S² @ S¯ 2, respecting the coproduct 2 = 1+1, cf Exercise 9.20 . They were also used by Hyland, Robinson and Rosolini [ HRR90] to state precisely the completeness of the category of modest sets (Example 7.3.2(l)).

In type theory, Bénabou's criticism has been (mis-understood and) a source of confusion - for syntactically defined indexed structures, the substitutions really are functorial on the nose, and the group- theoretic issues do not arise. The more difficult technology of fibrations has been employed where the simpler indexed one would have been enough. Even for semantics, we saw in Sections 7.6 and  8.4 that there is an equivalent syntactic category: Exercise 9.17 provides a similar construction for fibred versus indexed categories. One should not try to choose product, substitution functors, etc but work instead in the syntactically constructed category, taking the results back along the weak equivalence.