Finn Lawler regular fibration (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

Contents

Definition

A regular fibration is a bifibration p:EBp \colon E \to B, where EE and BB have finite products that are preserved bypp and by that reindexing, preserve cartesian arrows, satisfyingFrobenius 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 funtors 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?finite limits and pullback?pullback-stable images?images.

The ‘only if’ part of the proposition is straightforward: 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)) A Mon(C) Sub(A) = Mon(C)_A is the identity 1 A 1_\top 1_A on the terminal object of C A C A , and binary products are given by pullbacks in the fibres C Sub(A) C 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.

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