Finn Lawler regular fibration (Rev #6)

Contents

Definition

A regular fibration is a bifibration p:EBp \colon E \to B, where EE and BB have finite products that are preserved by pp and that preserve cartesian arrows, satisfying Frobenius reciprocity and the Beck--Chevalley condition for pullback squares in BB.

The preservation conditions on products are equivalent to requiring that each fibre E AE_A have finite products and that these be preserved by all reindexing functors f *f^*.

Our regular fibrations are those of Pavlovic. A very similar definition is given by Jacobs, whose only essential difference is that the fibres of a regular fibration are required to be preorders. (Hence such fibrations model regular logic where all proofs of the same sequent are considered equal.)

Logic

A regular fibration posesses exactly the structure needed to interpret regular logic?.

Characterization

Proposition

A category CC is regular if and only if the projection cod:Mon(C)Ccod \colon Mon(C) \to C sending SXS \hookrightarrow X to XX is a regular fibration, where Mon(C)Mon(C) is the full subcategory of C C^{\to} on the monomorphisms.

Proof

For our purposes, a regular category is one that has finite limits and pullback-stable images.

If CC is a regular category, then the adjunctions ff *\exists_f \dashv f^* come from pullbacks and images in CC (Elephant lemma 1.3.1) as does the Frobenius property ({}op. cit. lemma 1.3.3). The terminal object of Sub(A)=Mon(C) ASub(A) = Mon(C)_A is the identity 1 A1_A on AA, and binary products in the fibres Sub(A)Sub(A) are given by pullback. The products are preserved by reindexing functors f *f^* because (the f *f^* are right adjoints but also because) a cone over the diagram for f *(SS)f^*(S \wedge S') can be rearranged into a cone over that for f *Sf *Sf^*S \wedge f^*S', giving the two the same universal property. The projection codcod clearly preserves these products. The Beck–Chevalley condition follows from pullback-stability of images in CC.

Conversely, suppose Mon(C)CMon(C) \to C is a regular fibration. We need to show that CC has equalizers (to get finite limits) and pullback-stable images. But the equalizer of f,g:ABf, g \colon A \rightrightarrows B is (f,g) *Δ(f,g)^*\Delta. For images, let imf= f1im f = \exists_f 1 as in Elephant lemma 1.3.1. Pullback-stability follows from the Beck–Chevalley condition.

Revision on February 3, 2011 at 18:41:07 by Finn Lawler?. See the history of this page for a list of all contributions to it.