Finn Lawler regular fibration




A pre-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 product-absolute pullback squares of types C, D and E in BB. A regular fibration is a pre-regular fibration that also satisfies the Beck–Chevalley condition for type-B squares.

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^*.

The type-A Beck–Chevalley condition

Here and in my thesis I originally required regular fibrations to satisfy the type-A BC condition, but I now believe that it holds automatically as long as E does.

By Shulman’s construction, a pre-regular fibration EE over BB gives rise to a cartesian equipment BMatr(E)B \to Matr(E), and hence a cartesian bicategory Matr(E)Matr(E). Type-E squares in the bicategory are exact because they satisfy the BC condition in the fibration. Matr(E)Matr(E) then becomes compact closed bicategory, which is to say that there is an equivalence hom(A×B,C)hom(A,C×B)hom(A \times B, C) \simeq hom(A, C \times B) given by composing with A×d e A \times d_\bullet e^\bullet (left to right) and with C×d e C \times d^\bullet e_\bullet (right to left), where dd is the diagonal at BB and ee the map from BB to the terminal object. We will write this as R :AC×BR^\wedge \colon A \to C \times B for R:A×BCR \colon A \times B \to C and S :A×BCS^\vee \colon A \times B \to C for S:AC×BS \colon A \to C \times B. Similarly there is an equivalence hom(A×B,C)hom(B,A×C)hom(A \times B, C) \simeq hom(B, A \times C), which we will write as T{}^\wedge T and U{}^\vee U. If R:ABR \colon A \to B then R = (R ) (R )R^\circ = {}^\vee (R^\wedge) \cong {}^\wedge (R^\vee). The type-E BC condition implies that f f f_\bullet \dashv f_\bullet^\circ, and therefore f f f_\bullet^\circ \cong f^\bullet, and also that d d d_\bullet^\vee \cong d^\bullet and (d ) d (d^\bullet)^\wedge \cong d_\bullet. (See Carboni–Walters and Walters–Wood for all of this.)

The claim now is that modulo these isomorphisms, the morphisms required to be invertible by exactness of or BC for type-A squares are equal to β 1=(d f (f×f) d ) \beta_1 = (d_\bullet f_\bullet \cong (f \times f)_\bullet d_\bullet)^\vee and β 2= β 1\beta_2 = {}^\wedge \beta_1. Being the images under equivalences of invertible morphisms, then, they must themselves be invertible.

The following pictures show the essential parts of the proof using string diagrams, which can be read top-to-bottom as morphisms in a cartesian bicategory or bottom-to-top as objects in a monoidal bifibration as in this paper.


A regular fibration posesses exactly the structure needed to interpret regular logic, i.e. the {\exists}{\wedge}{\top}-fragment of first-order logic.



A category CC is regular if and only if the subobject fibration Sub(C)CSub(C) \to C (that sends SXS \hookrightarrow X to XX) is regular.


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)=Sub(C) ASub(A) = Sub(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) f *(SS)f^*(S \wedge S') and f *Sf *Sf^*S \wedge f^*S' have the same universal property. The projection Sub(C)CSub(C) \to C clearly preserves these products. The Beck–Chevalley condition follows from pullback-stability of images in CC.

Conversely, suppose Sub(C)CSub(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, which holds for all pullback squares in CC by Seely, Theorem sec. 8.

Last revised on December 9, 2015 at 12:37:59. See the history of this page for a list of all contributions to it.