INTERNAL PROFUNCTORS AND COMMUTATOR THEORY;
APPLICATIONS TO EXTENSIONS CLASSIFICATION AND CATEGORICAL GALOIS THEORY
DOMINIQUE BOURN
Abstract. We clarify the relationship between internal profunctors and connectors on pairs (R, S) of equivalence relations which originally appeared in the new profunctorial approach of the Schreier-Mac Lane extension theorem [11]. This clarification allows us to extend this Schreier-Mac Lane theorem to any exact Mal’cev category with centralizers.
On the other hand, still in the Mal’cev context and in respect to the categorical Galois theory associated with a reflection I, it allows us to produce the faithful action of a certain abelian group on the set of classes (up to isomorphism) ofI-normal extensions having a given Galois groupoid.
Introduction
Any extension between the non-abelian groupsK and Y can be canonically indexed by a group homomorphism φ :Y →AutK/IntK. The Schreier-Mac Lane extension theorem for groups [23] asserts that the class Extφ(Y, K) of non-abelian extensions between the groups K and Y indexed by φ is endowed with a simply transitive action of the abelian group Extφ¯(Y, ZK), where ZK is the center of K and the index ¯φ is induced by φ. A recent extension [11] of this theorem to any action representative ([5], [4], [3]) category gave rise to an unexpected interpretation of this theorem in terms of internal profunctors which was closely related with the intrinsic commutator theory associated with the action representative category in question.
So that there was a need of clarification about the general nature of the relationship between profunctors and the main tool of the intrinsic commutator theory, namely the notion of connector on a pair (R, S) equivalence relations, see [12], and also [15], [21], [20], [16].
The first point is that many of the observations made in [11] in the exact Mal’cev and protomodular settings are actually valid in any exact category. The second point is a characterization of those profunctors X1 # Y1 which give rise to a connector on a pair of equivalence relations: they are exactly those profunctors whose associated discrete bifibration (φ1, γ1) : Υ1 →X1×Y1 has its two legs φ1 and γ1 internally fully faithful.
Received by the editors 2010-03-23 and, in revised form, 2010-11-09.
Transmitted by R.J. Wood. Published on 2010-11-10.
2000 Mathematics Subject Classification: 18G50, 18D35, 18B40, 20J15, 08C05.
Key words and phrases: Mal’cev categories, centralizers, profunctor, Schreier-Mac Lane extension theorem, internal groupoid, Galois groupoid.
c Dominique Bourn, 2010. Permission to copy for private use granted.
451
The third point is the heart of Schreier-Mac Lane extension theorem, and deals with the notion of torsor. It is easy to define a torsor above a groupoid Z1 as a discrete fibration
∇1X →Z1 from the indiscrete equivalence relation on an object X with global support, in a way which generalizes naturally the usual notion of G-torsor, when G is a group.
The main point here is that when the groupoid Z1 is aspherical and abelian ([8]) with direction the abelian group A, there is a simply transitive action of the abelian group T orsA on the set T orsZ1 of classes (up to isomorphism) of Z1-torsors.
This simply transitive action allows us on the one hand (fourth point) to extend now the Schreier-Mac Lane extension theorem to any exact Mal’cev category with centralizers, and on the other hand (fifth point) to produce, still in the exact Mal’cev context and in respect to the categorical Galois theory associated with a reflectionI, the faithful action of a certain abelian group on the set of classes (up to isomorphism) of I-normal extensions having a fixed Galois groupoid. Incidentally we are also able to extend the notion of connector from a pair of equivalence relations to a pair of internal groupoids.
A last word: what is rather amazing here is that the notion of profunctor between groupoids which could rather seem, at first thought, as a vector of indistinction (every- thing being isomorphic) appears, on the contrary, as a important tool of discrimination.
The article is organized along the following lines:
Part 1) deals with some recall about the internal profunctors between internal categories and their composition, mainly from [18].
Part 2) specifies the notion of profunctors between internal groupoids and characterizes those profunctorsX1 #Y1 whose associated discrete bifibration (φ
1, γ
1) : Υ1 →X1×Y1 has its two legs φ
1 and γ
1 internally fully faithful. It contains also our main theorem about the canonical simply transitive action on the Z1-torsors, when the groupoid Z1 is aspherical and abelian.
Part 3) deals with some recall about the notion of connector on a pair of equivalence relations, and extends it to a pair of groupoids.
Part 4) asserts the Schreier-Mac Lane extension theorem for exact Mal’cev categories with centralizers.
Part 5) describes the faithful action on the I-normal extensions having a fixed Galois groupoid.
1. Internal profunctors
In this section we shall recall the internal profunctors and their composition.
1.1. Discrete fibrations and cofibrations. We shall suppose that our ambient category E is a finitely complete category. We denote by CatE the category of internal categories inE, and by ()0 :CatE→Ethe forgetful functor associating with any internal category X1 its “object of objects” X0. This functor is a left exact fibration. Any fibre CatXE has the discrete equivalence relation ∆1X as initial object and the indiscrete equivalence relation ∇1X as terminal object.
An internal functor f
1 :X1 →Y1 is then ()0-cartesian if and only if the following square is a pullback in E, in other words if and only if it is internally fully faithful:
X1 f1 //
(d0,d1)
Y1
(d0,d1)
X0×X0
f0×f0
//Y0×Y0
Accordingly any internal functor f
1 produces the following decomposition, where the lower quadrangle is a pullback:
X1 f1 //
(d0,d1)
γO1OOO''
O Y1
(d0,d1)
Z1
{{vvvvv
φ1
66m
mm mm m
X0×X0
f0×f0
//Y0×Y0
with the fully faithful functor φ
1 and the bijective on objects functor γ
1. We need to recall the following pieces of definition:
1.2. Definition. The internal functor f
1 is said to be ()0-faithful when the previous factorization γ1 is a monomorphism. It is said to be ()0-full when this same map γ1 is a strong epimorphism. It is said to be a discrete cofibration when the following square with d0 is a pullback:
X1
d1
d0
f1 //Y1
d1
d0
X0
f0
//
OO
Y0
OO
It is said to be a discrete fibration when the previous square with d1 is a pullback.
Supposef
1 is a discrete cofibration; when the codomainY1 is a groupoid, the domainX1 is a groupoid as well and the square with d1 is a pullback as well; when the codomainY1 is an equivalence relation, then the same holds for its domainX1. Accordingly, when the codomain Y1 of a functor f
1 is a groupoid, it is a discrete cofibration if and only if it is a discrete fibration.
1.3. Lemma. Any discrete fibration is ()0-faithful. A discrete fibration is ()0-cartesian if and only if it is monomorphic.
Proof. Thanks to the Yoneda Lemma, it is sufficient to prove these assertions in Set which is straightforward.
1.4. Profunctors. Let (X1, Y1) be a pair of internal categories. Recall from [2] that an internal profunctor X1 # Y1 is given by a pair X0 ←f0 U0 →g0 Y0 of maps (i.e. a span in E) together with a left action d1 : U1Y1 → U0 of the category Y1 and a right action d0 :U1X1 →U0 of the category X1 which commute with each others, namely which make commute the left hand side upper dotted square in the following diagram, where all those commutative squares that do not contain dotted arrows are pullbacks:
U1
p1 //
π0
//
π1
p0
U1Y1
s0
oo
d1
d0
g1 //Y1
y1
y0
U1X1
d1 //
d0
//
f1
OO
U0
s0
oo
f0
g0 //
OO
Y0
OO
X1
x1 //
xs00 //X0
oo
The middle horizontal reflexive graph is underlying a category UX11, namely the category of “cartesian maps” above X1, while the middle vertical reflexive graph is underlying a category UY11, namely the category of “cocartesian maps” above Y1. The pairs (d0, d1) going out from U1Y1 and U1X1 are respectively coequalized by f0 and g0. A morphism of profunctors is a morphism of spans aboveX0×Y0 which commutes with the left and right actions. We define this way the category Prof(X1, Y1) of internal profunctors between X1 and Y1.
In the set theoretical context, a profunctor X1 # Y1 is explicitely given by a functor U :Xop1 ×Y1 →Set. An object ofU0 is then an element ξ∈U(x, y) for any pair of object in Xop1 ×Y1, in other words U0 = Σ(x,y)∈X0×Y0U(x, y). Elements of U0 can be figured as further maps “gluing” the groupoids X1 and Y1:
x_ _ _ξ_ _ _//y
An object of U1X1 is a pair x0 →f x 99Kξ y and we denote d0(f, ξ) = U(f,1y)(ξ) by ξ.f, while an object ofU1Y1 is a pairx99Kξ y→g y0 and we denoted1(ξ, g) =U(1x, g)(ξ) byg.ξ.
An object of U1 is thus a triple:
x0
f
y
g
x
ξ
88q
q q q q q q
y0
We have π0(g, ξ, f) = (ξ.f, g) and π1(g, ξ, f) = (f, g.ξ). The commutation of the two actions comes from the fact that we have: (g.ξ).f =g.(ξ.f).
In this set theoretical context, the previous diagram can be understood as a map between φ=ξ.f and χ=g.ξ, pictured this way:
x0
f
φ //y
g
x χ //
ξ
88q
q q q q q q
y0
Accordingly this defines a reflexive graph given by the vertical central part of the following diagram in Set, with two morphisms of graphs:
X1
x1
x0
U1
f1.p0
oo
d1.p1
d0.p0
g1.p1 //Y1
y1
y0
X0
OO
U0 f0
oo g0 //
OO
Y0
OO
Actually this reflexive graph takes place in the more general scheme of a category we shall denote byUX11]UY11: its objects are the elements ofU0, a map betweenξ and ¯ξbeing given by a pair (s, t) of map in X1×Y1 such that ¯ξ.s=t.ξ:
x
s
ξ_ _ _//
_ _
_ y
t
¯
x ¯
ξ
//
_ _ _ _ _
_ y¯
Clearly the categories UX11 and UY11 are subcategories of UX11]UY11.
Actually, the same considerations hold in any internal context. The object of objects of the internal category UX11]UY11 isU0, its object of morphisms Υ1 is given by the pullback inE of the maps underlying the two actions:
Υ1 υ0 //
υ1
U1Y1
d1
U1X1 d
0
//U0
Moreover there is a pair (φ
1 : Υ1 →X1, γ
1 : Υ1 →Y1) of internal functors inEaccording to the following diagram:
X1
x1
x0
Υ1
f1.υ0
oo
d1.υ1
d0.υ0
g1.υ1 //Y1
y1
y0
X0
OO
U0
f0
oo g0
//
OO
Y0
OO
Without entering into the details, let us say that this pair of functors is characteristic of the given profunctor under its equivalent definition of a discrete bifibration in the 2- categoryCatE. Moreover the commutation of the two actions induces a natural morphism of reflexive graph:
U1
d1.p1
d0.p0
(π0,π1) //Υ1
d1.υ1
d0.υ0
U0
OO
U0
OO
The previous observations give rise to the following diagram in CatE: UY11 ''
''O
OO OO OO OO
g1 //Y1
∆1U0::
::u
uu uu u
$$ $$IIIII
I Υ1 =UX11]UY11
φ1
**U
UU UU UU UU UU UU U
γ1
44i
ii ii ii ii ii ii ii
UX11 77
77o
oo oo oo o
f1
//X1
1.5. Proposition. Let be given a finitely complete categoryE and an internal profunc- tor X1 #Y1. Then, in the fibre CatU0E, the left hand side quadrangle above is a pullback such that: UX11 ∨UY11 = Υ1 =UX11]UY11.
Proof. Thanks to the Yoneda embedding, it is enough to check it inSet. A map between ξ and ¯ξ in Υ1, as above, is in UY11 (resp. in UX11) if and only if s = 1x (resp. t = 1y).
Accordingly the intersection of these two subgroupoids is ∆1U0. The second point is a consequence of the fact that any map between ξ and ¯ξ in Υ1, as above, has a canonical decomposition through a map in UY11 and a map in UX11:
x_ _ _ξ_ _ _//
1x
y
t
x0
ξ.s=t.ξ¯_ _ _ _//
_ _
s
y
1y0
x0 ¯
ξ
//
_ _ _ _ _
_ y0
Accordingly any subcategory of Υ1 which contains the two subcategories in question is equal to Υ1.
What is remarkable is that, in the set theoretical context, the profunctors can be composed on the model of the tensor product of modules, see [2]. The composition can be transposed in E as soon as any internal category admits a π0 (i.e. a coequalizer of the domain and codomain maps) which is universal (i.e. stable under pullbacks), as it is the case when E is an elementary topos, see [18]. Let Y0 m←0 U0 →n0 Z0 be the span underlying another
profunctor Y1 # Z1 (and let (µ
1, ν1) : Γ1 → Y1 ×Z1 denote its associated discrete bifibration); then consider the following diagram induced by the dotted pullbacks:
V1
""FFFF
""
FF FF
V1Z1
n1
B
BB B
bbFFFF
U1Y1 ×Y1 V1Y1 pV1 //
pU1
θ1
))R
RR RR R
θ0RRRR))
RR V1Y1
""
EE EE
""
EE EE
m1
Z1
U0×Y0 V0 pV0 //
pU0
iiRRRRRR
θ&&&&
V0
m0
n0
""
EE EE
bbEEEE
W0_ _ _ _n¯_0 _ _ _ _////
f¯0
Z0
U1 ////
&&
MM MM MM MM
&&
MM MM MM
MM U1Y1
((R
RR RR RR RR RR
((R
RR RR RR RR RR
g1 //Y1
""
DD DD D
""
DD DD D
U1X1 ////
fS1SSSSSS)) SS
SS ffMMMMMMMM
U0
f0
&&
MM MM MM
M g0 //
hhRRRRRRRRRRR
Y0
bbDDDDD
X1 ////X0
It produces the following internal category Θ1 and the following forgetful functor to Y1: Θ1 :
U1Y1 ×Y1 V1Y1
θ1 //
θ0
//
g1.pU1
U0×Y0 V0
g0.pU0
s0
oo
Y1 : Y1
y1 //
ys00 //Y0
oo
Then take the π0 of the category Θ1 (it is the coequalizer θ of the pair (θ0, θ1)) which produces the dashed span X0 ←f¯0 W0 →n¯0 Z0. The π0 in question being stable under pullbacks, this span is endowed with a left action ofZ1 and a right action ofX1 and gives us the composite (µ
1, ν1)⊗(φ
1, γ
1).
Given an internal categoryX1, the unit profunctor is just given by theYoneda profunctor, i.e. given by the following diagram, whereX1Ois the object of the “commutative triangles”
of the internal category X1 and X1u is the object of the “triple of composable maps” of the internal category X1:
X1u
p1 //
π0 //
π1
p0
X1∆
s0
oo
p1
p0
p2 //X0
x1
x0
XO1
p2 //
p1 //
p0
OO
X1
s1
oo
x0
x1 //
OO
X0
OO
X1
x1 //
xs00 //X0
oo
It is easy to check thatX∆1]XO1 =X21, namely the domain of the universal internal natural transformation with codomain X1.
This tensor product ⊗ : Prof(X1, Y1)× Prof(Y1, Z1) → Prof(X1, Z1) is associative up to coherent isomorphism. By these units and the tensor composition, we get the bicategoryProfE of profunctors inE [18].
1.6. X1-torsor. From now on, we shall be uniquely interested in the full subcategory GrdE of CatE consisting of the internal groupoids in E. Recall that any fibre GrdXE is a protomodular category. We shall suppose moreover that the category E is at least regular.
We say that a groupoidX1 isconnected when it has a global support in its fibre GrdX0E, namely when the map (d0, d1) : X1 → X0×X0 is a regular epimorphism. We say it is aspherical when, moreover, the objectX0 has a global support, namely when the terminal map X0 →1 is a regular epimorphism.
1.7. Proposition. Suppose E is a regular category. Let be given a discrete fibration f1 :X1 →Y1 with Y1 an aspherical groupoid.
1) If f
1 is a monomorphism, then X1 is a connected groupoid.
2) If moreover X0 has global support, then f
1 is an isomorphism.
3) Any discrete fibration f
1 between aspherical groupoids is a levelwise regular epimor- phism.
Proof. 1) Since f
1 is a monomorphic discrete fibration it is ()0-cartesian according to Lemma 1.3 and the following commutative square is a pullback:
X1 f1 //
(d0,d1)
Y1
(d0,d1)
X0×X0
f0×f0//Y0×Y0 Accordingly X1 is connected as soon as such is Y1. 2) Then, since f
1 is discrete fibration, the following square that does not contain dotted arrows is still a pullback:
X0×X0
p1
p0
f0×f0 //Y0×Y0
p1
p0
X0
f0
//
OO
Y0
OO
and, by the Barr-Kock Theorem, when X0 has global support, it is the case also for the following one:
X0 f0 //
Y0
1 1
Accordingly f0 (and thus f1) is an isomorphism.
3) Starting from any discrete fibration f
1 : X1 → Y1, take the canonical reg-epi/mono decomposition of f
1:
X1
d1
d0
q1 ////U1
d1
d0
// m1 //Y1
d1
d0
X0 q0 ////
OO
U0
OO //
m0 //
OO
Y0
OO
Sincem1is a monomorphism, the left hand side squares are a pullback; sinceq1 is a regular epimorphism the right hand side squares are still pullbacks. Then m1 is a monomorphic discrete fibration, and since X0 has global support, so has U0. Then, according to 2), the functor m1 is an isomorphism, and the discrete fibration f
1 is a levelwise regular epimorphism.
1.8. Definition. Let X1 be an aspherical groupoid in E. A X1-torsor is a discrete fibration ∇1U →X1 where U is an object with global support:
U×U
p1
p0
τ1 //X1
d1
d0
U τ //
OO
X0
OO
According to the previous proposition, the maps τ and τ1 are necessarily regular epimor- phisms. Moreover it is clear that this determines a profunctor: 1 # X1. When X1 is a group G, we get back to the classical notion of G-torsor, if we consider G as a groupoid having the terminal object 1 as “object of objects”. In order to emphazise clearly this groupoid structure, we shall denote it by K1G.
2. Fully faithful profunctors
In this section we shall characterize those profunctorsX1 #Y1 between groupoids whose associated discrete bifibration (φ
1, γ
1) : Υ1 →X1×Y1 has its two legsφ
1andγ
1internally fully faithful, namely those profunctors such that their associated discrete bifibration (φ1, γ
1):
UY11 ''
''O
OO OO OO OO
g1 //Y1
∆1U0::
::u
uu uu u
$$ $$IIIII
I Υ1 =UX11]UY11
φ1
**U
UU UU UU UU UU UU U
γ1
44i
ii ii ii ii ii ii ii
UX11 77
77o
oo oo oo o
f1
//X1
is obtained by the canonical decomposition of the discrete fibrations f
1 and g
1 through the ()0-cartesian maps.
When X1 and Y1 are internal groupoids, we have substantial simplifications in the pre- sentation of profunctors X1 # Y1. First, since any discrete fibration between groupoids becomes a discrete cofibration, any commutative square in the definition diagram, even the dotted ones, becomes a pullback1. Accordingly the objects U1 and Υ1 defined above coincide, so that the reflexive graph U1 is actually underlying the groupoid UX11]UY11. On the other hand, the new perfect symmetry of the definition diagram means that the pair (γ
1, φ
1) : U1 → Y1 ×X1 still determines a discrete bifibration, i.e. a profunctor Y1 #X1 in the opposite direction which we shall denote by (φ
1, γ
1)∗.
WhenEis exact, any internal groupoid admits aπ0which is stable under pullback; so that, in the context of exact categories, the profunctors between groupoids are composable. We shall be now interested in some special classes of profunctors between groupoids.
2.1. Proposition. SupposeE is a finitely complete category. Let be given a profunctor (φ1, γ
1) : U1 → X1 ×Y1 between groupoids. Then its functorial leg γ
1 : U1 → Y1 is ()0-faithful if and only the groupoid UX11 is an equivalence relation; it is ()0-cartesian if and only if we have UX11 =R[g0]. By symmetry, the other legφ
1 :U1 →X1 is ()0-faithful if and only the groupoid UY11 is an equivalence relation; it is ()0-cartesian if and only if we have UY11 =R[f0]
Proof. Thanks to the Yoneda embedding, it is enough to prove it in Set. Suppose that γ1 :U1 →Y1 is faithful. Let be given two parallel arrows inUX11 ⊂U1:
x_ _ _ξ_ _ _//
f0
f
y
1y
x0 _ _ _χ_ _ _//y The image of these two arrows of U1 by the functor γ
1 is 1y. Accordingly, since this functor is ()0-faithful, we get f = f0, and UX11 is an equivalence relation. Conversely suppose UX11 is an equivalence relation. Two maps in U1 having the same image g byγ determine a diagram: 1
x_ _ _ξ_ _ _//
f0
f
y
g
x0_ _ _χ_ _ _//y0 which itself determines the following diagram:
x_ _ _g.ξ_ _ _//
f0
f
y0
1y0
x0 _ _ _χ_ _ _//y0
1In this way, any profunctor between groupoids can be seen as a double augmented simplicial object inEsuch that any commutative square is a pullback
But since UX11 is an equivalence relation, we get f = f0. Accordingly the functor γ
1 : U1 →Y1 is faithful.
Suppose we have moreover UX11 = R[g0]. Any pair (ξ, χ) in U0 with a map g between their respective codomains y and y0, determines a pair (g.ξ, χ) in R[g0]:
x g.ξ
%%L
L L
f
y0 x0 χ
99t
tt
and since we have UX11 =R[g0], we get a mapf such that g.ξ=χ.f which determines an arrow in U1 whose image by γ
1 is g:
x_ _ _ξ_ _ _//
f
y
g
x0 _ _ _χ_ _ _//y0 Conversely suppose γ
1 is fully faithful. Since it is faithful we observed that UX11 ⊂R[g0].
Now given any pair (ξ, χ) in R[g0], the fullness property of γ
1 produces a map f which completes the following diagram:
x_ _ _ξ_ _ _//
f
y
1y
x0 χ //______ y
and we get R[g0]⊂UX11.
2.2. Definition. An internal profunctor between groupoids is said to be faithful when its two legs φ
1 and γ
1 are ()0-faithful. It is said to be fully faithful when its two legs φ and γ 1
1 are ()0-cartesian. It is said to be regularly fully faithful when moreover the maps f0 and g0 are regular epimorphisms.
Examples. 1) Given any internal groupoid X1, its associated Yoneda profunctor is a regularly fully faithful profunctor:
R2[x0]
p3 //
p2 //
p1
p0
R[x0]
s1
oo
p1
p0
p2 //X0
x1
x0
R[x0]
p2 //
p1 //
p0
OO
X1
s1
oo
x0
x1 ////
OO
X0
OO
X1
x1 //
x0 //X0
s0
oo
It is this precise diagram which makes the internal groupoids monadic above the split epimorphisms, see [6].
2) Given an abelian group A in E, any A-torsor determines a regularly fully faithful profunctor K1A #K1A. For that, consider the following diagram where the upper right hand side squares are pullbacks by definition of anA-torsor:
R[h1]
R(p1)
R(p0)
p1 //
p0
//T ×T
oo
p1
p0
h1 ////A
T ×T
h1
p1 //
p0 //T
oo τT
////
OO
τT
1
e
OO
Aoo e //1
and complete it by the horizontal kernel equivalence relations. Then, when A is abelian, the same maph1 is the quotient of the vertical left hand side equivalence relation. Thanks to the Barr embedding, it is enough to prove it in Set, which is straighforward. Actually this is equivalent to saying that, when A is abelian, a principal left A-object becomes a principal symmetric two-sided object, according to the terminology of [1].
2.3. Proposition. SupposeEis a regular category. A morphism τ : (φ
1, γ
1)→(φ0
1, γ0
1) between profunctors above groupoids having their legs φ
1 and φ0
1 ()0-cartesian and regu- larly epimorphic is necessarily an isomorphism. In particular, a morphism between two regularly fully faithful profunctors is necessarily an isomorphism.
Proof. Consider the following diagram which is part of the diagram induced by the morphism τ of profunctors:
R[f0]
d1
d0
R(τ) //
g1 //
R[f00]
d1
d0
g01
//Y1
y1
y0
U0 τ //
OO
f0
g0 U00 g //
0 0 //
f00
OO
Y0
OO
X0
1X0
//X0
The functor g
1 and g0
1 being discrete fibrations, the left hand side upper part of the diagram is a discrete fibration between equivalence relations. Since moreover f0 is a regular epimorphism, the lower square is a pullback by the Barr-Kock theorem and τ an isomorphism.
2.4. Proposition. Suppose E is an efficiently regular category [9]. Let X1 # Y1 and Y1 #Z1 be two profunctors between groupoids whose first leg of their associated discrete bifibrations (φ
1, γ
1) and (µ
1, ν1) is ()0-cartesian. Then their profunctor composition does exist in E and has its first leg ()0-cartesian. When, moreover, their first legs are regu- larly epimorphic, their profunctor composition has its first leg regularly epimorphic. By symmetry, the same holds concerning the second legs. Accordingly regularly fully faithful profunctors are composable as profunctors, and are stable under this composition.
Proof. Let us go back to the diagram defining the composition. When the first leg φ
1
is ()0-cartesian, we have U1Y1 = R[f0]. By construction the groupoid Θ1 determines a discrete fibration:
U1Y1 ×Y1 V1Y1
θ1 //
θ0
//
pU1
U0×Y0 V0
pU0
s0
oo θ ////W0
f¯0
R[f0]
p1 //
p0
//U0
s0
oo f0
//X0
Since Eis an efficiently regular category and the codomain of this discrete fibration is an effective equivalence relation, its domain is an effective equivalence relation as well. Thus, this domain admits a quotient θ, and a factorization ¯f0 which makes the right hand side square a pullback. Moreover this quotient is stable under pullback, since E is regular.
Accordingly the two profunctors can be composed. Let us notice immediately that when m0 is a regular epimorphism, such ispU0. If moreover f0 is a regular epimorphism, then f¯0 is a regular epimorphism as well, and we shall get the second point, once the first one is checked.
Suppose now the first leg φ0
1 is ()0-cartesian, i.e. V1Z1 = R[m0]. We have to check that W1Z1 =R[ ¯f0]. Let us consider the diagram where R[pU0] is the result of the pulling back along g0 of V1Z1 =R[m0], and R[pU1] is the result of the result of the pulling back along g1 of V1 =R[m1]:
R[pU1]
p1
p0
R(θ1) //
R(θ0)
//R[pU0]
p1
p0
s0
oo ¯θ ////WZ11
q1
q0
U1Y1 ×Y1 V1Y1
θ1 //
θ0
//
pU1
U0×Y0 V0 pU0
s0
oo θ ////W0
f¯0
R[f0]
p1 //
ps00 //U0
oo
f0
//X0
Since any of the upper left hand side squares are pullbacks and (θ,θ) is a pair of regular¯ epimorphims, the upper right hand side squares are pullbacks. This implies that the right hand side vertical diagram is a kernel equivalence relation. Accordingly we have W1Z1 =R[ ¯f0].
