Theory and Applications of Categories, Vol. 32, No. 10, 2017, pp. 338–379.

KZ-MONADIC CATEGORIES AND THEIR LOGIC

JIŘÍ ADÁMEK AND LURDES SOUSA

Abstract. Given an order-enriched category, it is known that all its KZ-monadic subcategories can be described by Kan-injectivity with respect to a collection of morphisms. We prove the analogous result for Kan-injectivity with respect to a collection ℋ of commutative squares. A square is called a Kan-injective consequence of ℋ if by adding it to ℋ Kan-injectivity is not changed.

We present a sound logic for Kan-injectivity consequences and prove that in “reasonable” categories (such as Pos or Top_{0}) it is also complete for every set ℋ of squares.

1. Introduction

Scott characterized continuous lattices in [15], 3.8 and following, as those T_{0} spaces that are, in modern terminology, Kan-injective with respect to all embeddings. The Kaninjectivity of an object X of an order-enriched category with respect to a morphism h : A [figure] B was defined by Escardó [8] as follows: for every morphism f : A [figure] X we have a commutative triangle

\xymatrix{A \ar[r]^{h} \ar[d]_{f} & B \ar[dl]^{f/h} \\ X}

where f/h is the left Kan-extension of f along h. That is, if g : B [figure] X fulfils f ≤ gh, then f/h ≤ g.

Later Carvalho and Sousa [6] extended the above concept from objects to morphisms: a morphism u : X [figure] X′ is Kan-injective with respect to h when X and X′ are Kaninjective objects and for every morphism f : A [figure] X the following triangle

\xymatrix{B \ar[r]^{f/h} \ar[d]_{(uf)/h} & X \ar[dl]^{u} \\ X′}

The second author acknowledges the support of the Centre for Mathematics of the University of Coimbra – UID/MAT/00324/2013, funded by the Portuguese Government through FCT/MCTES and co-funded by the European Regional Development Fund through the Partnership Agreement PT2020.

Received by the editors 2016-06-18 and, in final form, 2017-02-22. Transmitted by Robert Paré. Published on 2017-02-27. 2010 Mathematics Subject Classification: 18C20, 18B35, 18D20, 54B30, 06B35, 06D22, 18A15. Key words and phrases: order-enriched category, Kan-injectivity, KZ-monad, Kan-injectivity logic,

locally ranked category.

\begin{matrix}c \\ ◯ \end{matrix} Jiří Adámek and Lurdes Sousa, 2017. Permission to copy for private use granted.

commutes. Example: the morphisms of Top_{0} Kan-injective with respect to all embeddings are precisely the continuous maps between continuous lattices preserving all infima. A trivial example: in Pos Kan-injectivity with respect to

[figure: •  •; h; •; •; •]

defines the subcategory of join-semilattices and their homomorphisms.

Moreover, in locally ranked categories, e.g., in Top_{0} or Pos, Kan-injectivity yields a characterization of KZ-monadic categories in the following sense: given a class ℋ of morphisms, let LInj(ℋ) be the subcategory of all objects and all morphisms Kan-injective with respect to all members of ℋ. Then

(1) every KZ-monadic subcategory has the form LInj(ℋ) for some class ℋ of morphisms, see [6],

and

(2) for every set ℋ of morphisms the subcategory LInj(ℋ) is KZ-monadic, see [4].

The topic of our paper is the logic of Kan-injectivity, generalizing the logic of orthogonality studied in [1] and [2]. Observe first that given an ordinary category with its trivial order-enrichment (that is, equality), then LInj(ℋ) is nothing else than the full subcategory ℋ^{⊥} on objects X orthogonal to every member h : A [figure] B of ℋ (that is, each f : A [figure] X has a unique factorization through h). The logic of orthogonality aims to characterize those morphisms h for which orthogonality to ℋ implies that to h, i.e. with ℋ^{⊥} = (ℋ ∪ {h})^{⊥}. See Section 4 where the simple logic presented in [1] is recalled.

Analogously, we hoped to present a logic that would characterize, in order-enriched categories, those morphisms for which Kan-injectivity with respect to ℋ implies that with respect to h. But we have failed so far. What saved our effort was the idea to ”enrich” our language by considering, instead of Kan-injectivity with respect to morphisms, Kaninjectivity with respect to commutative squares S:

\xymatrix{A_{1} \ar[r]^{h_{1}} \ar[d]_{a} & B_{1} \ar[d]^{b} \\ A_{2} \ar[r]_{h_{2}} & B_{2}}

An object X is Kan-injective with respect to S if it is Kan-injective with respect to h_{1} and h_{2} and for every morphism f : A_{2} [figure] X the following triangle

\xymatrix{B_{1} \ar[dr]^{(fa)/h_{1}} \ar[d]_{b} \\ B_{2} \ar[r]_{f/h_{2}} & X}

commutes. And a morphism is Kan-injective with respect to S iff it is Kan-injective with respect to h_{1} and h_{2}.

For every class ℋ of commutative squares we thus obtain a (non-full) subcategory LInj(ℋ) analogously to above. These categories characterize again KZ-monadicity: we prove in Section 3 below that the above statements (1) and (2) remain valid. In other words, this richer language does not lead to more examples! However, it enables a formulation of a sound logic (see Section 4) which for sets of squares is, under mild size conditions, also complete (see Section 5). It is our present impression that this enrichment of the structure from morphisms to commutative squares is probably necessary: we suspect that no logic for Kan-injectivity with respect to just morphisms is sound and complete.

2. KZ-monadic subcategories

2.1. Assumption. Throughout the paper 𝒳 is a category enriched over Pos. All squares in our paper are commutative, so when stating that something is a square, we mean a commutative one.

We introduced Kan-injectivity with respect to a morphism and a square above. Observe that the latter is a generalization of the former: for every morphism h : A [figure] B let S(h) be the following square

S(h) = [figure: A; h; B; A; h; B]

Then Kan-injectivity with respect to h and S(h) is the same concept for objects and morphisms.

2.2. Example. In Pos consider Kan-injectivity with respect to h : 0 ↪ 1, the empty map into the terminal poset. This means the existence (and preservation) of the least element, ⊥. Kan-injectivity with respect to the embedding

[figure: •; •; •; ⊥; k; •; •; •; •; ⊥]

characterizes existence (and preservation) of joins of pairs having a lower bound. Combining those two in a square as follows

[figure: h; •⊥; •; •; •; ⊥; k; •; •; •; •; ⊥]

yields by Kan-injectivity join-semilattices with ⊥ and their homomorphisms.

We have already remarked that using squares does not lead to new examples. Indeed, join-semilattices with ⊥ are also given by Kan-injectivity with respect to h and the following embedding

[figure: •  •; •; •; •]

2.3. Example. Which posets are Kan-injective with respect to all order-embeddings (i.e., regular monomorphisms) in Pos?

As shown in [4], these are precisely the complete lattices, and a monotone map is Kaninjective with respect to order-embeddings iff it preserves joins. We now characterize all squares S that are Kan-injectivity consequences of order-embeddings. That is, such that every complete lattice and every join-preserving map between complete lattices is Kaninjective with respect to S.

Let us denote by Ω_{0} the contravariant endofunctor of Pos assigning to every posed X the posed Ω_{0}X of all ↓-sets of X, and to every monotone function f : X [figure] Y the function Ω_{0}f : Ω_{0}Y [figure] Ω_{0}X forming preimages. Observe that Ω_{0}f has a left adjoint

(Ω_{0}f)^{∗} : Ω_{0}X [figure] Ω_{0}Y , U ↦↓ f [U] (for all U ∈ Ω_{0}X).

2.4. Proposition. For every square

S = \xymatrix{A′ \ar[r]^{h} \ar[d]_{a} & B′ \ar[d]^{b} \\ A \ar[r]_{k} & B}

in Pos the following conditions are equivalent:

(1) S is a Kan-injectivity consequence of order-embeddings;

(2) h and k are order-embeddings such that whenever k(z) ≤ b(y), there exists x ∈ A′ with h(x) ≤ y and z ≤ a(x);

and

(3) h and k are order-embeddings yielding a (commutative) square

\xymatrix{Ω_{0}B′ \ar[d]_{(Ω_{0}b)^{∗}} \ar[r]^{Ω_{0}h} & Ω_{0}A′ \ar[d]^{(Ω_{0}a)^{∗}} \\ Ω_{0}B \ar[r]_{Ω_{0}k} & Ω_{0}A}

Proof. The equivalence of (1) and (2) was proved in [16].

3 ⇒ 2 The inequality k(z) ≤ b(y) states precisely that

z ∈ Ω_{0}k · (Ω_{0}b)^{∗}(↓ y) = (Ω_{0}a)^{∗} · Ω_{0}h(↓ y),

that is, z lies in ↓ a [Ω_{0}h(↓ y)]. This means that an x as in (2) exists.

2 ⇒ 3 It is easy to verify that the inequality

(Ω_{0}a)^{∗} · Ω_{0}h ≤ (Ω_{0}k) · (Ω_{0}b)^{∗}

holds for every square S. Thus we need to show the opposite inequality only. Let V be a ↓-set of B′ and z be an element of (Ω_{0}k)(Ω_{0}b)^{∗}(V), i.e., z ∈ k^{−1} [↓ b [V]]. Then for some y ∈ V we have k(z) ≤ b(y). Given x as in (2) we conclude z ∈ (Ω_{0}a)^{∗}Ω_{0}h(V), establishing the required inequality.

2.5. Example. The category Top_{0} of topological T_{0}-spaces is order enriched via the opposite of the specialization order. Recall that the specialization order is given by x ⊑ y iff x ∈ \overline{\{y\}}. Thus, for continuous functions f, g : X [figure] Y we define

f ≤ g iff g(x) ⊑ f(x) for all x ∈ X.

Escardó and Flagg proved that Kan-injective objects with respect to topological embeddings (= regular monomorphisms) are precisely Scott’s continuous lattices, see [9]. Recall that a T_{0}-space is a continuous lattice iff for the specialization order its topology is the Scott’s one, and it is a complete lattice with

y = ⨆_{U∈nbh(y)}(⊓U) for all y ∈ X.

The morphisms Kan-injective with respect to topological embeddings are precisely the continuous functions preserving meets, see [6]. We characterize the squares which are injectivity consequences of topological embeddings. Let Ω : Top_{0} [figure] Pos^{op} be the functor assigning to a space X the poset ΩX of open sets and to a continuous function f : X [figure] Y the preimage function Ωf : ΩY [figure] ΩX. By (Ωf)_{∗} we denote the right adjoint of Ωf: to an open set U it assigns the union of all openV ⊆ Y with f^{−1}(V) ⊆ U.

2.6. Proposition. A square

S = \xymatrix{A′ \ar[r]^{h} \ar[d]_{a} & B′ \ar[d]^{b} \\ A \ar[r]_{k} & B}

in Top_{0} is a Kan-injectivity consequence of topological embeddings iff h and k are topological embeddings yielding the following (commutative) square

\xymatrix{ΩA \ar[r]^{(Ωk)_{∗}} \ar[d]_{Ωa} & ΩB \ar[d]^{Ωb} \\ ΩA′ \ar[r]_{(Ωh)_{∗}} & ΩB′}

Proof. (a) Sufficiency. For every continuous lattice X and every embedding f : A [figure] X the Kan-extension f/k is, as proved in [9], given by

f/k(z) = ⊔{⊓U; U ∈ ΩX and z ∈ (Ωk)_{∗}[Ωf(U)]},  (1)

and analogously for (fa)/h. We are to prove

(f/k) · b = (fa)/h.

Indeed, given b ∈ B′, then b(y) ∈ (Ωk)_{∗}[Ωf(U)] means that y ∈ (Ωb)(Ωk)_{∗}[Ωf(U)], and, by the commutativity of the last square, this means that y ∈ (Ωh)_{∗}[Ω(fa)(U)]. Consequently, taken into account the definitions of (f/k)(b(y)) and ((fa)/h)(y) given by (1), we conclude the desired equality.

(b) Necessity. Since the Sierpińsky space S is Kan-injective with respect to S, k and h are topological embeddings (see 4.3 and 4.4 of [6]). We verify the above square.

Every V ∈ ΩA defines the corresponding characteristic function f_{V} : A [figure] S and, using the formula (1) above, we get (by setting V = {1})

(f_{V} /k)(z) = 1 iff z ∈ (Ωk)_{∗}(V).

Since f_{V} · a = f_{Ωa(V)}, the characteristic function of a^{−1}(V), we analogously get

(f_{V} · a)/h(x) = 1 iff x ∈ (Ωh)_{∗}(Ωa(V)).

Thus, our formula (f_{V} · a)/h = (f_{V} /k) · b reads:

x ∈ (Ωh)_{∗}(Ωa(V)) iff b(x) ∈ (Ωk)_{∗}(V)

for all x ∈ B′. That is,

(Ωh)_{∗}(Ωa(V)) = Ωb((Ωk)_{∗}(V)),

as desired.

2.7. Remark. A slight modification: Scott continuous domains are, as proved by Escardó [8], precisely the T_{0}-spaces Kan-injective with respect to dense embeddings, see [10], Exercise 3.19. And the morphisms Kan-injective with respect to dense embeddings are the continuous functions preserving nonempty meets (see [6]). The above corollary holds analogously, just h and k are required to be dense embeddings.

2.8. Example. Let Loc be the category of locales and localic maps. Thus, the objects of Loc are complete lattices with the infinite distributive law

a ∧ ⋁ B = ⋁{a ∧ b | b ∈ B},

and the morphisms are the monotone maps f which preserve all infima and whose left adjoint f^{∗} preserves finite meets. We recall that a localic map h is an embedding provided that h^{∗}h = id. Johnstone characterized the stably locally compact locales as the locales injective with respect to flat embeddings, i.e. those preserving finite joins, see [11]. Moreover, with convenient morphisms, stably locally compact locales are precisely LInj(ℋ) for ℋ = flat embeddings (see [11] and [7]).

2.9. Proposition. A square

\xymatrix{A′ \ar[r]^{h} \ar[d]_{a} & B′ \ar[d]^{b} \\ A \ar[r]_{k} & B}

in Loc is a Kan-injectivity consequence of flat embeddings iff h and k are flat embeddings yielding the following (commutative) square

\xymatrix{A \ar[r]^{k} \ar[d]_{a^{∗}} & B \ar[d]^{b^{∗}} \\ A′ \ar[r]_{h} & B′}

Proof. Let F_{0}, F_{1} and F_{2} be the free frames generated by the empty set, 1 = {0} and 2 = {0, 1}, respectively, and let f_{i} : F_{i} [figure] F_{1}, i = 0, 2, be the localic maps determined by f_{0}(⊥) = 0, f_{2}(0 ∨ 1) = 0 and f_{2}(x) = ⊥ for x ≠ ⊥, 0 ∨ 1. In [7] flat embeddings were characterized as precisely those morphisms with respect to which both f_{0} and f_{2} are Kan-injective. Furthermore, it was shown there that for every finitely generated free frame F, in particular for every F_{i} (i = 0, 1, 2), given a flat embedding h : A [figure] B and a morphism f : A [figure] F, the map (hf^{∗})_{∗} is localic and

f/h = (hf^{∗})_{∗}.  (2)

(a) Necessity: suppose the given square is a Kan injectivity consequence of flat embeddings. Since we already know that flat embeddings are characterized by means of f_{0} and f_{2}, we only need to prove ha^{∗} = b^{∗}k.

Given x ∈ A, we want to show that b^{∗}k(x) = ha^{∗}(x). Let g : F_{1} [figure] A be the frame homomorphism sending 0 to x. By hypothesis, the localic map g_{∗} : A [figure] F_{1} satisfies (g_{∗}/k) · b = (g_{∗}a)/h, that is, by (2), (kg)_{∗}b = h(g_{∗}a)^{∗} = ha^{∗}g. Consequently, by applying the operator −^{∗} to the localic maps (kg)_{∗}, b and ha^{∗}g, we obtain b^{∗}kg(0) = ha^{∗}g(0), i.e., b^{∗}k(x) = ha^{∗}(x).

(b) Sufficiency: if the lower square commutes, we prove that, given f : A [figure] F_{i}, (fa)/h = (f/k)b. Indeed, from (2), deduce that

(fa)/h = [(h(fa)^{∗}]_{∗} = (ha^{∗}f^{∗})_{∗} = (b^{∗}kf^{∗})_{∗} = (kf^{∗})_{∗}b = (f/k) · b.

2.10. Remark. (a) Given an order-enriched category 𝒳, by a right adjoint retraction we mean a morphism r : X [figure] Y with r^{∗} : Y [figure] X satisfying rr^{∗} = id and r^{∗}r ≥ id.

(b) Recall that a KZ-monad over 𝒳 is a monad T for which

T η ≤ ηT.

Then T-algebras are precisely the right adjoint retractions of η_{A} : A [figure] T A. Thus, 𝒳^{T} is a (non-full) subcategory of 𝒳.

(c) In [4] we proved that KZ-monadic subcategories are precisely the subcategories 𝒦 which are

(1) reflective, i.e., the embedding has a left adjoint,

(2) inserter-ideal, i.e., contain the inserter ins(u, v) of every parallel pair (u, v) with u in Mor(𝒦),

and

(3) closed under right adjoint retractions.

That is, with every morphism p : X → Y the subcategory contains all morphisms \overline{p} : \overline{X} [figure] \overline{Y} for which there exists a square with right adjoint retractions x and y as follows

\xymatrix{X \ar[r]^{p} \ar[d]_{x} & Y \ar[d]^{y} \\ \overline{X} \ar[r]_{\overline{p}} & \overline{Y}}  (3)

(d) Every KZ-monadic subcategory 𝒦 has the form 𝒦 = LInj(ℋ) for some class ℋ of morphisms of 𝒳 ([6]). And we proved that, conversely, for “reasonable” categories 𝒳 (such as Top_{0} and Pos), every set ℋ of morphisms defines a KZ-monadic subcategory LInj(ℋ). (The latter is not true for proper classes ℋ in Top_{0} as demonstrated by an example in [4]).

2.11. Lemma. For every class ℋ of squares the category LInj(ℋ) is inserter-ideal and closed under right adjoint retractions.

Proof. A. Given a pair of morphisms u, v : X [figure] Y and a square

\xymatrix{A′ \ar[d]_{a} \ar[r]^{h′} & B′ \ar[d]^{b} \\ A \ar[r]_{h} & B}  (4)

with respect to which u is Kan-injective, we prove that so is the inserter i = ins(u, v) : I [figure] X. We have already proved in [4] that the fact that u is Kan-injective with respect to h and h′ implies that so is the morphism i. It remains to show that, for every f : A [figure] I, (f/h)b = (fa)/h′, or equivalently, since i is mono, i(f/h)b = i(fa)/h′. But the last equality follows immediately from the fact that i is Kan-injective with respect to both h and h′ and X is Kan-injective w.r.t. the above square.

B. Given a square (3) with the left adjoints x^{∗} and y^{∗}, respectively, and such that the morphism p : X [figure] Y is Kan-injective with respect to the square (4), we prove that also \overline{p} is Kan-injective with respect to this square.

(a) \overline{X} is Kan-injective with respect to the above square, and for every morphism f : A [figure] \overline{X} we have: f/h = x([x^{∗}f]/h).

\xymatrix{A′ \ar[d]_{a} \ar[r]^{h′} & B′ \ar[d]^{b} \\ A \ar[d]_{f} \ar[r]_{h} & B \ar[d]^{(x^{∗}f)/h} \\ \overline{X} \ar@{-->}[r]_{x^{∗}} & X \ar[l]_{x}}

This last formula was proved in [6]. Analogously one proves (fa)/h′ = x([x^{∗}fa]/h′). Consequently, since the Kan-injectivity of X yields

[x^{∗}fa]/h′ = ([x^{∗}f]/h)b

we conclude (fa)/h′ = (f/h)b.

(b) \overline{Y} is Kan-injective. This is completely analogous.

(c) \overline{p} is Kan-injective with respect to h and h′. This was also proved in [6].

3. The reflection chain

Throughout the rest of the paper 𝒳 denotes an order-enriched category with weighted colimits. Given a set ℋ of squares, we associate with every object X a transfinite chain starting in X. For “reasonable” categories we then prove that there exists a connecting morphism from X in our chain which is the reflection of X in the subcategory LInj(ℋ).

3.1. Definition. Let ℋ be a set of squares. For every object X define a transfinite chain X_{i} (i ∈ Ord) with connecting morphisms called x_{ij} or simply \xymatrix{X_{i} \ar@{-->}[r] & X_{j}} (for i ≤ j). We proceed by transfinite recursion. In the isolated steps, given i we define X_{i} −−→ X_{i+1} −−→ X_{i+2}, therefore, we can assume that i is an even ordinal (that is, i = 2n or i = i_{0} + 2n for n < ω and i_{0} a limit ordinal).

(a) Initial step. X_{0} = X.

(b) Limit steps. If i is a limit ordinal then

X_{i} = colim_{j<i} X_{j}

is the colimit of the previous chain with X_{j} −−→ X_{i} forming the colimit cocone.

(c) Isolated step i ↦ i + 1 (i even). Consider all pairs (S, f) where

S = \xymatrix{A_{1} \ar[r]^{h_{1}} \ar[d]_{a} & B_{1} \ar[d]^{b} \\ A_{2} \ar[r]_{h_{2}} & B_{2}}  (5)

is a member of ℋ and f : A_{r} [figure] X_{i} a morphism with r = 1 or 2. Form the pushout of h_{r} along f:

\xymatrix{A_{r} \ar[r]^{h_{r}} \ar[d]_{f} & B_{r} \ar[d]^{f̄} \\ X_{i} \ar[r]_{_{\overline{h}_{r}}} & Q_{f}}  (6)

Define X_{i} −−→ X_{i+1} as the wide pushout of all the morphisms \overline{h}_{r}:

\xymatrix{X_{i} \ar@{-->}[d] \ar[r]^{^{\overline{h}^{r}}} & Q_{f} \ar[dl]^{q_{f}} \\ X_{i+1}}  (7)

ranging over all the above pairs (S, f).

Notation: put

f⫽h_{r} : \xymatrix{B_{r} \ar[r]^{\overline{f}} & Q_{f} \ar[r]^{q_{f}} & X_{i+1}}  (8)

This “approximates” the desired Kan extension f/h_{r} in the following sense: we get a (commutative) square

\xymatrix{A_{r} \ar[d]_{f} \ar[r]^{h_{r}} & B_{r} \ar[d]^{f⫽h_{r}} \\ X_{i} \ar@{-->}[r] & X_{i+1}}  (9)

(d) Isolated step i + 1 ↦ i + 2 (i even). Consider all triples (S, f, g) consisting of S ∈ ℋ, as above, and two morphisms forming an inequality as follows:

\xymatrix{A_{r} \ar[dd]_{f} \ar[rr]^{h_{r}} &  & B_{r} \ar[dd]^{g} \\  & ≤ \\ X_{i} \ar@{-->}[rr] &  & X_{i+1}}  (r = 1 or 2)  (10)

For every decomposition of f as follows

f ≡ \xymatrix{A_{r} \ar[r]^{f′} & X_{j} \ar@{-->}[r] & X_{i}} (j ≤ i even)  (11)

form the coinserter of \xymatrix{A_{r} \ar[r]^{f′⫽h_{r}} & X_{j+1} \ar@{-->}[r] & X_{i+1}} and g:

c_{f,g} = coins(x_{j+1,i+1}[f′⫽h_{r}], g) : X_{i+1}  [figure] C_{f,g}.  (12)

And in case r = 1 for every decomposition of f as follows

f ≡ \xymatrix{A_{1} \ar[r]^{a} & A_{2} \ar[r]^{f′} & X_{i}}  (13)

form the coinserter of \xymatrix{B_{1} \ar[r]^{b} & B_{2} \ar[r]^{f′⫽h_{2}} & X_{i+1}} and g:

c_{f,g} = coins([f′⫽h_{2}].b, g).  (14)

Define X_{i+1} −−→ X_{i+2} as the wide pushout of all c_{f,g} above:

\xymatrix{X_{i+1} \ar@{-->}[d] \ar[r]^{c_{f,g}} & C_{f,g} \ar[dl]^{t_{f,g}} \\ X_{i+2}}  (15)

3.2. Lemma. Given a morphism p_{0} : X_{0} [figure] P where P is Kan-injective with respect to ℋ, there exists a unique cocone p_{i} : X_{i} [figure] P (i ∈ Ord) of the reflection chain such that for all pairs (S, f) in step i ↦ i + 1 the following triangle

\xymatrix{A_{r} \ar[d]_{f⫽h_{r}} \ar[dr]^{(p_{i}f)/h_{r}} \\ X_{i+1} \ar[r]_{p_{i+1}} & P}  (16)

commutes.

Proof. We only need to prove the isolated step of the transfinite induction. Given p_{i}, i even, we obtain p_{i+1} as follows. From the following square

\xymatrix{A_{r} \ar[d]_{f} \ar[r]^{h_{r}} & B_{r} \ar[d]^{(p_{i}f)/h_{r}} \\ X_{i} \ar[r]_{p_{i}} & P}

we conclude that the pushout (6) yields a unique factorization morphism p_{f} : Q_{f} [figure] P. These morphisms p_{f} form a cocone of the wide pushout (7). Define p_{i+1} as the unique factorization morphism

p_{i+1} · q_{f} = p_{f}.

It fulfils p_{i+1} · (f⫽h_{r}) = p_{i+1}.q_{f} · \overline{f} = p_{f}.\overline{f} = (p_{i}f)⫽h_{r}. Conversely, whenever the above triangle commutes, then p_{i+1} is a factorization map of the wide pushout (7).

Next we define p_{i+2}: since X_{i+1} −−→ X_{i+2} is a wide pushout of epimorphisms, p_{i+2} is unique. And for the proof of existence we only need to verify that p_{i+1} factorizes through each c_{f,g}. That is:

(a) In case of (11) we want to verify the inequality

\xymatrix{B_{r} \ar[d]_{f′⫽h_{r}} \ar[rr]^{g} &  & X_{i+1} \ar[dd]^{p_{i+1}} \\ X_{j+1} \ar@{-->}[d] & ≤ \\ X_{i+1} \ar[rr]_{p_{i+1}} &  & P}

The lower passage is, due to p_{j+1} = p_{i+1} · x_{j+1,i+1} and (16), equal to (p_{j}.f′)/h_{r}. By composing (10) with p_{i+1} we get

p_{j}f′ ≤ p_{i+1}gh_{r}

hence,

(p_{j}f′)/h_{r} ≤ p_{i+1}g

(b) In case of (13) we want to verify the inequality

\xymatrix{B_{1} \ar[d]_{b} \ar[rr]^{g} &  & X_{i+1} \ar[dd]^{p_{i+1}} \\ B \ar[d]_{f′⫽h_{2}} & ≤ \\ X_{i+1} \ar[rr]_{p_{i+1}} &  & P}

Indeed, the lower passage is, due to (16) and injectivity of P with respect to S, equal to

[(p_{i}f′)/h_{2}]b = (p_{i}f′a)/h_{1} = (p_{i}f)/h_{1}.

By composing (10) with p_{i+1} we get p_{i}f ≤ p_{i+1}.g.h_{1}. This proves (p_{i}f)/h_{1} ≤ p_{i+1}.g as desired.

Recall that in a category with a factorization system (ℰ, ℳ) an object is said to have rank λ (a regular cardinal) if its hom-functor preserves λ-directed colimits of morphisms in ℳ. We use the following concept introduced in [4]:

3.3. Definition. Let 𝒳 be an order-enriched category with a factorization system (ℰ, ℳ) such that ℰ ⊆ Epi and ℳ ⊆ Order-Mono (i.e., given m ∈ ℳ then mu ≤ mv implies u ≤ v). We call 𝒳 locally ranked if

(i) it has weighted colimits, (ii) it is ℰ-cowellpowered,

and

(iii) every object has a rank.

3.4. Example. Pos is locally ranked w.r.t. ℰ = Epi and ℳ = Order-Embedding. Top_{0} is locally ranked w.r.t. ℰ = surjective morphisms and ℳ = subspace embeddings.

3.5. Remark. Let 𝒳 be locally ranked and let (X_{i}) be a transfinite chain with connecting morphisms \xymatrix{X_{i} \ar@{-->}[r] & X_{j}} (i ≤ j). By Proposition 4.1 of [12] there exists a chain (Y_{i}) of monomorphisms in ℳ, a join-preserving function φ : Ord [figure] Ord and natural transformations

\xymatrix{X_{i} \ar[r]^{γ_{i}} & Y_{i} \ar[r]^{β_{i}} & X_{φ(i+1)}} (i ∈ Ord)

such that for all i:

(1) β_{i}γ_{i} is the connecting morphism \xymatrix{X_{i} \ar@{-->}[r] & X_{φ(i+1)}} ;

(2) the composite \xymatrix{Y_{i} \ar[r]^{β_{i}} & X_{φ(i+1)} \ar@{-->}[r] & X_{j}} lies in ℳ for all j ≥ φ(i + 1);

and

(3) if i is a limit ordinal, then a colimit of the chain (Y_{j})_{j<i} is given by the following

cocone

\xymatrix{Y_{j} \ar[r]^{β_{j}} & X_{φ(j+1)} \ar@{-->}[r] & X_{φ(i)}}

Moreover, given such a function φ, every join-preserving function φ′ ≥ φ works too. Consequently, we can clearly choose φ so that φ(i) is even for all ordinals i.

3.6. Theorem. Let 𝒳 be a locally ranked order-enriched category. For every set ℋ of squares the subcategory LInj(ℋ) is reflective: the reflection of every object X is given by X −−→ X_{k} (in Definition 3.1) where k is a suitable cardinal.

Proof. Apply the above remark to the chain of Definition 3.1, using notation î = φ(i+1). Since ℋ is a set, there exists a cardinal λ such that for every square in ℋ all the four objects involved have rank λ. The cardinal k of our theorem is chosen to be

k = φ(λ).

(1) We first prove that the object X_{k} is Kan-injective with respect to every square in ℋ:

S = \xymatrix{A_{1} \ar[d]_{a} \ar[r]^{h_{1}} & A_{2} \ar[d]^{b} \\ B_{1} \ar[r]_{h_{2}} & B_{2}}

(a) Kan extensions modulo h_{1} and h_{2} exist. Indeed, every morphism f_{0} : A_{r} [figure] X_{k} (r = 1, 2) has, since A_{r} has rank λ, a factorization f through some colimit injection of the colimit X_{k} = colim_{j<λ} Y_{j} of Remark 3.5(3):

\xymatrix{ &  & A_{r} \ar[dll]_{f} \ar[dl]^{f′} \ar[d]^{f_{0}} \\ Y_{j} \ar[r]_{β_{j}} & Xĵ \ar@{-->}[r] & X_{k}}

Put f′ = β_{j}f. We use Notation (8) and prove that the desired Kan extension is

f_{0}/h_{r} ≡ \xymatrix{A_{r} \ar[r]^{f′⫽h_{r}} & X_{ĵ+1} \ar@{-->}[r] & X_{k}} .  (17)

Indeed, from (9) we get f_{0} = (f_{0}/h_{r}) · h_{r} via f′ = (f′⫽h_{r}) · h_{r}:

(f_{0}/h) · h_{r} ≡ \xymatrix{A_{r} \ar[r]^{f′} & X_{ĵ+1} \ar@{-->}[r] & X_{k}}

Next, let g_{0} = B_{r} [figure] X_{k} fulfil

f_{0} ≤ g_{0}h_{r}.

Since B_{r} has rank λ, we can find an analogous factorization:

\xymatrix{ &  & B_{r} \ar[dll]_{g} \ar[dl]^{g′} \ar[d]^{g_{0}} \\ Y_{i} \ar[r]_{β_{i}} & Xî \ar@{-->}[r] & X_{k}}

for some ordinal i < k. Without loss of generality, j ≤ i. The above inequality yields the following one:

\xymatrix{A_{r} \ar[dd]_{f} \ar[r]^{h_{r}} & B_{r} \ar[r]^{g} & Y_{i} \ar[d]^{β_{i}} \\  & ≤ & Xî \ar@{-->}[d] \\ Y_{j} \ar[dd]_{y_{ji}} \ar[r]_{β_{j}} & Xĵ \ar@{-->}[d] \ar@{-->}[r] & X_{k} \\  & Xî \ar@{-->}[ur] \\ Y_{i} \ar[ur]_{β_{i}}}

Since by Remark 3.5 the colimit morphisms lie in ℳ, (thus, they are order-monomorphisms) this proves

y_{ji} · f ≤ g · h_{r}

which by composition with β_{i} yields the inequality

\xymatrix{A_{r} \ar[d]_{f′} \ar[rr]^{h_{r}} &  & B_{r} \ar[d]^{g′} \\ Xĵ \ar@{-->}[d] & ≤ & Xî \ar@{-->}[d] \\ Xî \ar@{-->}[rr] &  & X_{î+1}}

This is an instance of (10) and (11) with respect to x_{î,î+1}·g′. Let c_{f,g′} be the corresponding coinserter (12). Since the map X_{î+1} −−→ X_{î+2} factorizes through c_{f,g′}, we obtain the following inequality

\xymatrix{B_{r} \ar[d]_{f′⫽h_{r}} \ar[r]^{g′} & Xî \ar@{-->}[r] & X_{î+1} \ar@{-->}[dd] \\ X_{ĵ+1} \ar@{-->}[d] & ≤ \\ X_{î+1} \ar@{-->}[rr] &  & X_{î+2}}

Composed with X_{î+2} −−→ X_{k} this states that

x_{ĵ+1,k} · (f′⫽h_{r}) ≤ x_{îk} · g′

which is the desired inequality

f_{0}/h_{r} ≤ g_{0}.

(b) It remains to prove that for every f_{0} : A_{2} [figure] X_{k} we have

(f_{0}a)/h_{1} = (f_{0}/h_{2})b.

Put f̂_{0} = f_{0}a and factorize it analogously as f_{0} above, assuming (without loss of generality) that the same colimit injection can be applied:

\xymatrix{ &  & A_{r} \ar[dll]_{f̂} \ar[dl]^{f̂′} \ar[d]^{f̂_{0}} \\ Y_{j} \ar[r]_{β_{j}} & Xĵ \ar@{-->}[r] & X_{k}}

Thus the equality to be proved is, due to (16), the following square

\xymatrix{B_{1} \ar[d]_{b} \ar[r]^{f̂′⫽h_{1}} & X_{ĵ+1} \ar@{-->}[dd] \\ B_{2} \ar[d]_{f′⫽h_{2}} \\ X_{ĵ+1} \ar@{-->}[r] & X_{k}}  (18)

Since x_{ĵk} ·β_{j} is monic by Remark 3.5, the equality f̂_{0} = f_{0}a clearly implies f̂ = f ·a which multiplied by β_{j} yields f̂′ = f′ · a. From (9) we thus get the square

\xymatrix{A_{1} \ar[d]_{a} \ar[r]^{h_{1}} & B_{1} \ar[dd]^{f̂′⫽h_{1}} \\ A_{2} \ar[d]_{f′} \\ Xĵ \ar@{-->}[r] & X_{ĵ+1}}

This is an instance of (10) and (13). Let c_{f,g} be the corresponding coinserter. Since the map X_{ĵ+1} −−→ X_{ĵ+2} factorizes through it, we obtain the following inequality

\xymatrix{B_{1} \ar[d]_{b} \ar[rr]^{f̂′⫽h_{1}} &  & X_{ĵ+1} \ar@{-->}[dd] \\ B_{2} \ar[d]_{f′⫽h_{2}} & ≤ \\ X_{ĵ+1} \ar@{-->}[rr] &  & X_{ĵ+2}}

which multiplied by X_{ĵ+2} −−→ X_{k} yields ”almost” the desired square (18): indeed, the opposite inequality (f_{0}/h_{2}) · b ≥ (f_{0}a)/h_{1} is trivial.

(2) For every morphism p : X_{0} [figure] P where P lies in LInj(ℋ) we prove that the morphism p_{k} : X_{k} [figure] P in Lemma 3.2 is Kan-injective with respect to ℋ. The proof is entirely analogous to that of Part (2) of the proof of Theorem 6.10 of [4]. The proof that the extension of the morphism p via X −−→ X_{k} is unique in LInj(ℋ) is entirely analogous to Part (3) of the proof mentioned above.

3.7. Remark. (a) The ordinal k above depends on the choice of the object X. However, given two objects X and X̃, we can find an ordinal k such that both of the reflection chains for X and X̃ yield reflections in LInj(ℋ) after k steps. This follows from the choice k = φ(λ) made in the above proof, since the same function φ can be used for both chains. (This can be deduced from the fact that we can always use any function φ′ ≥ φ preserving joins.)

(b) Denote by

R : 𝒳 [figure] LInj(ℋ)

the reflector, i.e., the left adjoint of the embedding. And by η_{X} : X [figure] RX the reflection morphisms. We have just proved that for all objects X we have

η_{X} ≡ X −−→ X_{k}

How is R characterized on morphisms u : X [figure] X̃?

We prove below that

Ru = u_{k} : X_{k} [figure] X̃_{k}

for the following natural transformation u_{i} : X_{i} [figure] X̃_{i} (i ∈ Ord). Here X̃_{i} denotes the reflection chain for X̃ (and we use the obvious notation Q̃_{f}, C̃_{f,g}, etc.).

3.8. Notation. Let u : X [figure] X̃ be a morphism of 𝒳. We define a natural transformation u_{i} : X_{i} [figure] X̃_{i} (i ∈ Ord) of the reflection chains of X and X̃ by the following transfinite induction:

Initial step: u_{0} = u.

Limit step: this is automatic from naturality.

Isolated step i ↦ i + 1 (i even): every pair (S, f) with respect to X_{i} defines a pair (S, u_{i} · f) with respect to X̃_{i}. For the corresponding pushouts Q_{f} and Q̃_{u_{i}f}, see (6), we get a unique factorization f^{∗} as follows:

[figure: A_{r}; f; h_{r}; B_{r}; \overline{f}; B_{r}; ũ_{i}f; X_{i}; u_{i}; _{\overline{h}_{r}}; Q_{f}; f^{∗}; X̃_{i}; h̃_{r}; Q̃_{u_{i}f}]  (19)

Then (q̃_{u_{i}f} · f^{∗})h̄_{r} = x̃_{i,i+1} · u_{i} is independent of f. Therefore we can define u_{i+1} via the following squares (for all (S, f)):

\xymatrix{Q_{f} \ar[d]_{q_{f}} \ar[r]^{f^{∗}} & Q̃_{u_{i}f} \ar[d]^{q̃_{u_{i}f}} \\ X_{i+1} \ar[r]_{u_{i+1}} & X̃_{i+1}}  (20)

Observe also that (u_{i}f)⫽h_{r} is the composite of f⫽h_{r} and u_{i+1}:

[figure: B_{r}; \overline{f}; f⫽h_{r}; B_{r}; ũ_{i}f; (u_{i}f)⫽h_{r}; Q_{f}; q_{f}; f^{∗}; Q̃_{u_{i}f}; q̃_{u_{i}f}; X_{i+1}; u_{i+1}; X̃_{i+1}]  (21)

Isolated step i + 1 ↦ i + 2 (i even). Every triple (S, f, g) in the definition of X_{i+2} yields a triple (S, f̃, g̃) with respect to X̃_{i+2} as follows:

f̃ ≡ \xymatrix{A_{r} \ar[r]^{f} & X_{i} \ar[r]^{u_{i}} & X̃_{i}} and g̃ ≡ \xymatrix{B_{r} \ar[r]^{g} & X_{i+1} \ar[r]^{u_{i+1}} & X̃_{i+1}}

The naturality of (u_{j}) guarantees that every factorization (11) of f yields the corresponding factorization

f̃ ≡ \xymatrix{A_{r} \ar[r]^{f′} & X_{j} \ar[r]^{u_{j}} & X̃_{j} \ar@{-->}[r] & X̃_{i}}

of f̃. And we prove below that this leads to a unique morphism d_{f,g} forming the following square

\xymatrix{X_{i+1} \ar[d]_{u_{i+1}} \ar[r]^{c_{f,g}} & C_{f,g} \ar[d]^{d_{f,g}} \\ X̃_{i+1} \ar[r]_{c̃_{f̃,g̃}} & C̃_{f̃,g̃}}  (22)

Analogously, every factorization (13) of f yields one for f̃ and we again obtain a square (22). We define u_{i+2} via the following squares (for all (S, f, g)):

\xymatrix{C_{f,g} \ar[d]_{t_{f,g}} \ar[r]^{d_{f,g}} & C̃_{f,g} \ar[d]^{t̃_{f̃,g̃}} \\ X_{i+2} \ar[r]_{u_{i+2}} & X̃_{i+2}}  (23)

3.9. Proposition. The above natural transformation u_{i} : X_{i} [figure] X̃_{i} (i ∈ Ord) is well defined, and u_{k} = Ru for every morphism u : X [figure] X̃.

Proof. (1) Firstly, given an even ordinal i, the morphisms q_{u_{i}f} · f^{∗} form a cocone of the wide pushout (7) defining X_{i} −−→ X_{i+1}, hence, in (21) the morphism u_{i+1} is unique. We need to verify the naturality square. For that observe that the following diagram

\xymatrix{X_{i} \ar@{-->}[dd] \ar[dr]^{h_{r}} \ar[rrr]^{u_{i}} &  &  & X̃_{i} \ar[dl]_{h̃_{r}} \ar@{-->}[dd] \\  & Q_{f} \ar[dl]^{q_{f}} \ar[r]^{f^{∗}} & Q̃_{u_{i}f} \ar[dr]_{q̃_{u_{i}f}} \\ X_{i+1} \ar[rrr]_{u_{i+1}} &  &  & X̃_{i+1}}

commutes.

(2) Next we verify the existence of d_{f,g} in (22). In case (11) this is equivalent to proving that c̃_{f̃,g̃} u_{i+1} satisfies the following inequality:

\xymatrix{A_{r} \ar[d]_{f′⫽h_{r}} \ar[rr]^{g} &  & X_{i+1} \ar[d]^{u_{i+1}} \\ X_{j+1} \ar@{-->}[d] & ≤ & X̃_{i+1} \ar[d]^{c̃_{f̃,g̃}} \\ X_{i+1} \ar[r]_{u_{i+1}} & X̃_{i+1} \ar[r]_{c̃_{f̃,g̃}} & C̃_{f̃,g̃}}

Indeed, this follows from the definition of c̃_{f̃,g̃} and (21). And in case (13) we need the inequality

\xymatrix{B_{1} \ar[d]_{b} \ar[rr]^{g} &  & X_{i+1} \ar[d]^{u_{i+1}} \\ B \ar[d]_{f′⫽h_{2}} & ≤ & X̃_{i+1} \ar[d]^{c̃_{f̃,g̃}} \\ X_{i+1} \ar[r]_{u_{i+1}} & X̃_{i+1} \ar[r]_{c̃_{f̃,g̃}} & C̃_{f̃,g̃}}

which also follows from the definition of c̃_{f̃,g̃} and (21). The morphisms

\xymatrix{C_{f,g} \ar[r]^{d_{f,g}} & C̃_{f̃,g̃} \ar[r]^{t̃_{f̃,g̃}} & X̃_{i+2}}

form a cocone of the wide pushout (15) due to (22):

t̃_{f̃,g̃} · d_{f,g} · c_{f,g} = t_{f̃,g̃} · c̃_{f̃,g̃} · u_{i+1} = x̃_{i+1,i+2} · u_{i+1}.

Thus (23) defines u_{i+2} uniquely. Moreover, the naturality square now follows:

\xymatrix{X_{i+1} \ar@{-->}[dd] \ar[dr]^{c_{f,g}} \ar[rrr]^{u_{i+1}} &  &  & X̃_{i+1} \ar[dl]_{c̃_{f̃,g̃}} \ar@{-->}[dd] \\  & C_{f,g} \ar[dl]^{t_{f,g}} \ar[r]^{d_{f,g}} & C̃_{f̃,g̃} \ar@{-->}[dr]^{t̃_{f̃,g̃}} \\ X_{i+1} \ar[rrr]_{u_{i+2}} &  &  & X̃_{i+2}}

(3) Consequently, for every morphism u : X [figure] X̃ the ordinal k of Theorem 3.6 provides a square

[figure: X; u; η_{X}; RX; X_{k}; u_{k}; X̃; ηX̃; RX̃; X̃_{k}]

To prove u_{k} = Ru, we only need to verify that u_{k} is a morphism of LInj(ℋ). That is, for every square

\xymatrix{A_{1} \ar[d]_{a} \ar[r]^{h_{1}} & B_{1} \ar[d]^{b} \\ A_{2} \ar[r]_{h_{2}} & B_{2}}

in ℋ and every morphism f_{0} : A_{r} [figure] X_{k} the triangle

\xymatrix{B_{r} \ar[dr]_{(u_{k}f_{0})/h_{r}} \ar[r]^{f_{0}/h_{r}} & X_{k} \ar[d]^{u_{k}} \\  & X̃_{k}}

commutes. We use (17) for f_{0}/h_{r}, and we assume without loss of generality that the same ordinal j can be used for (u_{k}f_{0})/h_{r}. Then the triangle above commutes due to (21):

\xymatrix{A_{r} \ar[dr]_{(uĵf′)⫽h_{r}} \ar[r]^{f′⫽h_{r}} & X_{ĵ+1} \ar[d]^{u_{ĵ+1}} \ar@{-->}[r] & X_{k} \ar[d]^{u_{k}} \\  & X̃_{ĵ+1} \ar@{-->}[r] & X̃_{k}}

3.10. Remark. In the following diagram (see (19))

\xymatrix{A_{r} \ar[d]_{f} \ar[r]^{h_{r}} & B_{r} \ar[d]^{\overline{f}} \\ X_{i} \ar[d]_{u_{i}} \ar[r]^{_{\overline{h}_{r}}} & Q_{f} \ar[d]^{f^{∗}} \\ X̃_{i} \ar[r]_{h̃_{r}} & Q̃_{u_{i}f}}

the lower square is a pushout. This follows from the fact that both the composite and the upper square are pushouts.

4. Kan-injectivity logic

We now introduce a sound logic for deriving a square S from a given class ℋ of squares of 𝒳. (Recall that “square” means a commutative one throughout.) Soundness means that every object and every morphism Kan-injective with respect to members of ℋ is also Kan-injective with respect to squares derived from ℋ. In the subsequent section we prove that our logic is also complete if ℋ is small and the base category is locally ranked.

Since for ordinary categories Kan-injectivity w.r.t. a morphism is just the usual orthogonality, it is not surprising that our logic is very close to the orthogonality logic presented in [1]. Let us recall this logic here shortly. Firstly, every isomorphism s has the property that all objects are orthogonal to s. Hence that logic has one axiom

AXIOM  \overline{s}  for s an isomorphism.

The deduction rules are such that whenever an object is orthogonal to the assumptions (above the horizontal line), then it is orthogonal also to the conclusion. We have the following deduction rules:

COMPOSITION  \frac{h_{1} h_{2}}{h_{2} · h_{1}}  for morphisms [figure: h_{1}; h_{2}]

PUSHOUT  \frac{h}{k}  for a pushout [figure: h; k]

WIDE PUSHOUT  \frac{h_{i} (i ∈ I)}{k}  for a wide pushout [figure: h_{i}; k; h̄_{i}; (i∈I)]

COEQUALIZER

\frac{k}{c}
for a coequalizer [figure: k; g_{2}; g_{1}; c]
and a morphism k with g_{1}k = g_{2}k

WEAK CANCELLATION  \frac{h_{3} · h_{2} h_{2} · h_{1}}{h_{1}}  for morphisms [figure: h_{1}; h_{2}; h_{3}]

This logic is sound in every category 𝒳 with colimits. And for small sets of morphisms ℋ it is complete, i.e., every morphism h such that ℋ^{⊥} = (ℋ ∪ {h})^{⊥} can be derived from ℋ (and the isomorphisms) provided that 𝒳 is locally ranked, see [1]. This means that for some factorization system (ℰ, ℳ)

(a) 𝒳 is cocomplete and ℰ-cowellpowered

and

(b) every object X has a rank, i.e., an infinite cardinal λ such that 𝒳(X, −) preserves λ-directed colimits of ℳ-monics.

The logic presented below deals with collections ℋ of squares and the following concept:

4.1. Definition. A square S is said to be a Kan-injectivity consequence of a class ℋ of squares provided that every object and every morphism Kan-injective with respect to the members of ℋ is also Kan-injective with respect to S. Shortly:

LInj(ℋ) = LInj(ℋ ∪ {S}).

4.2. Example. If ℋ = ∅, we are speaking about squares w.r.t. everything is Kaninjective. Let us call a square

\xymatrix{A_{1} \ar[r]^{h_{1}} \ar[d]_{a} & B_{1} \ar[d]^{b} \\ A_{2} \ar[r]_{h_{2}} & B_{2}}  (24)

split if h_{1} and h_{2} are left adjoint sections and the Beck-Chevalley condition holds. That is, we have a commutative square

\xymatrix{A_{1} \ar[d]_{a} & B_{1} \ar[l]_{h_{1}^{∗}} \ar[d]^{b} \\ A_{2} & B_{2} \ar[l]^{h_{2}^{∗}}}  (25)

with h_{i}^{∗}h_{i} = id and h_{i}h_{i}^{∗} ≤ id for i = 1, 2.

Each such square has the property that every object is Kan-injective with respect to it. Indeed, given f : A_{r} [figure] X for r = 1, 2 the formula for the Kan extension is easily seen to be

f/h_{r} = f · h_{r}^{∗}

from which this fact is obvious. Moreover, this formula implies also that every morphism is Kan-injective w.r.t. S.

This explains why in the following deduction system the split squares can serve as axioms.

The following logic has as formulas (commutative) squares in a given category. Recall that every morphism h : A [figure] B is represented by the square

S(h) = [figure: A; h; B; A; h; B] .

4.3. Definition. The Kan-injectivity Logic consists of one

AXIOM  \overline{S}  for split squares S

and the following deduction rules:

COMPOSITION

\frac{S_{1} , S_{2}}{S}

for a composite S, horizontal or vertical, of S_{1} and S_{2}

PUSHOUT

[figure: h_{1}; h_{2}; h_{r}; a]

for a pushout of h_{r}, r = 1 or 2, along an arbitrary morphism a

WIDE PUSHOUT

[figure: h; b_{i} (i∈I); b_{i}h; h; b_{j}; b̄_{j}; h; k]
for any wide pushout [figure: h; b_{i}; k; b̄_{i}; (i∈I)]
and any j ∈ I

COINSERTER

\frac{S , S_{0} , \overline{S}}{[figure: k′; c; k′; c]}

for a coinserter [figure: k; g_{2}; g_{1}; c],

a morphism k with g_{1}k ≤ g_{2}k, and a commutative diagram

[figure: S; k; g_{1}; S_{0}; \overline{S}; c; h_{0}; k′]

RIGHT

CANCELLATION

\frac{S , S(h) , S(k)}{S_{0}} for S = [figure: S_{0}; h; k]

UPPER

CANCELLATION

\frac{S_{i} , \overline{S}_{i} (i ∈ I)}{S} for \overline{S}_{i} = [figure: h_{i}; a_{i}; S_{i}; b_{i}; a; S; b; h]

with (b_{i})_{i∈I} collectively epic

By a deduction of a square S from a collection ℋ of squares is, as usual, meant a sequence of squares obtained by the application of the above rules where S is the last square and the assumptions are (a) members of ℋ, (b) axiom instances or (c) squares already deduced.

4.4. Proposition. (Soundness of the Kan-Injectivity Logic) Let 𝒳 have weighted colimits. Every square deduced from a class of squares is a Kan-injectivity consequence of that class.

Proof. For the soundness of axiom see Example 4.2. Therefore, all we need to prove is that for every deduction rule in Definition 4.3 the deduced square S is a Kan-injectivity consequence of the assumptions of that rule. To do so we take an object X Kan-injective with respect to each of the assumptions and verify that X is Kan-injective with respect to S. By doing so we actually give a formula for the Kan extensions needed.

We leave out the verification that also morphisms u : X [figure] X′ Kan-injective with respect to all assumptions are Kan-injective with respect to S. Indeed, due to the formula presented for objects this verification is in each case trivial.

(1) composition. (a) Horizontal composition:

\xymatrix{A_{1} \ar[d]_{a} \ar[r]^{h} & B_{1} \ar[d]_{b} \ar[r]^{h′} & C_{1} \ar[d]^{c} \\ A_{2} \ar[d]_{f} \ar[r]_{k} & B_{2} \ar[dl]_{f/k} \ar[r]_{k′} & C_{3} \ar[dll]^{(f/k)/k′} \\ X}

Let X be Kan-injective with respect to both of the above squares. We prove for all f : A_{2} [figure] X the formula

f/(k′k) = (f/k)/k′.

Clearly,

[(f/k)/k′] k′k = f.

Given g with f ≤ gk′k, we conclude f/k ≤ gk′, hence (f/k)/k′ ≤ g. Analogously,

\overline{f}/(h′h) = (\overline{f}/h)/h′ for all \overline{f} : A_{1} [figure] X.

The formula [fa] /(h′h) = [f/(k′k)] · c easily follows.

(b) For a vertical composition:

\xymatrix{A′′ \ar[dd]_{a_{1}} \ar[rr]^{h′′} &  & B′′ \ar[dd]^{b_{1}} \\  & S_{1} \\ A′ \ar[dd]_{a_{2}} \ar[rr]^{h′} &  & B′ \ar[dd]^{b_{2}} \\  & S_{2} \\ A \ar[dr]_{f} \ar[rr]_{h} &  & B \ar[dl]^{f/h} \\  & X}

we prove that (fa_{2}a_{1})/h′′ = (f/h)b_{2}b_{1} easily from (fa_{2})/h′ = (f/h)b_{2} and [(fa_{2})a_{1}] /h′′ = [(fa_{2})/h′] · b_{1}.

(2) Pushout. (a) Suppose X is Kan-injective w.r.t. [figure: h_{1}; h_{2}]. Let r = 1 and f :

\overline{A}_{1} [figure] X be given:

[figure: A_{1}; \overline{a}; h_{1}; B_{1}; \overline{b}; (f\overline{a})/h_{1}; _{\overline{A}_{1}}; f; _{\overline{h}_{1}}; _{\overline{B}_{1}}; f/\overline{h}_{1}; X]

For the square formed by f and (f\overline{a})/h_{1} we have a unique factorization, let us call it f/\overline{h}_{1}. This is justified by the lower triangle above together with the implication

f ≤ g\overline{h}_{1} implies f/\overline{h}_{1} ≤ g

which we verify easily. The above pushout is conical so to prove f/\overline{h}_{1} ≤ g we only need a verification when precomposed by \overline{h}_{1} (this is our assumption) and by \overline{b}. To prove (f/\overline{h}_{1})\overline{b} ≤ g\overline{b}, that is, (f\overline{a})h_{1} ≤ g\overline{b}, we just observe that our assumption implies f\overline{a} ≤ g\overline{b}h_{1} due to \overline{b}h_{1} = \overline{h}_{1}\overline{a}.

The required rule (f/h_{1})/\overline{b} = (f\overline{a})/h_{1} is the right-hand triangle above.

(b) The proof for r = 2 is completely analogous.

(3) Wide pushout. Let X be Kan-injective w.r.t. each of the squares [figure: h; b_{i}; b_{i}h]. Given

a morphism f : A [figure] X

[figure: A; h; B; b_{i}; B_{i}; _{\overline{b}_{i}}; A; f; h; B; k; P; X]

we know that f/h and f/(b_{i}h) exist and fulfil

(f/(b_{i}h))b_{i} = f/h.

Consequently, for the given wide pushout P there exists a unique morphism

f̂: P [figure] X with f̂\overline{b}_{i} = f/(b_{i}h) for i ∈ I.

We prove

f/(kh) = f̂.

Firstly

f̂kh = f̂\overline{b}_{i}b_{i}h = [f/(b_{i}h)] b_{i}h = f.

Next if f ≤ gkh, we prove f̂ ≤ g. It suffices to observe that for all i we have f̂\overline{b}_{i} ≤ g\overline{b}_{i}, and use that our wide pushout is conical. Indeed, we have

f̂\overline{b}_{i} = f/(b_{i}h) ≤ g\overline{b}_{i}

or, equivalently,

f ≤ g\overline{b}_{i}b_{i}h

by assumption.

The desired formula

(f/(kh)) · \overline{b}_{j} = f/(b_{j}h)

now follows from f̂\overline{b}_{j} = f/(b_{j}h).

(4) coinserter. We are given a diagram

\xymatrix{A \ar[r]^{k} & B \ar[r]^{g_{2}} \ar[r]_{g_{1}} & C \ar[r]^{c} & D}

with g_{1}k ≤ g_{2}k and c = coins(g_{1}, g_{2}), and a commutative diagram

[figure: A; S; k; a; B; g_{1}=h′b; b; C; A_{0}; S_{0}; h; B_{0}; \overline{S}; h′; C; R; h_{0}; R; R; k′]

Observe that k′ = h′hh_{0}. If X is Kan-injective with respect to S, S_{0} and \overline{S}, we prove Kan-injectivity with respect to the following square:

[figure: R; h_{0}; A_{0}; h; B_{0}; h′; C; c; R; h_{0}; A_{0}; h; B_{0}; h′; C; c; D]

Kan-injectivity with respect to \overline{S} yields

f̂ = f/(h′hh_{0}) with f̂h′ = f/(hh_{0})  (26)

We prove below that

f̂g_{1} ≤ f̂g_{2}  (27)

which means that f̂ factorizes through c = coins(g_{1}, g_{2}). This concludes the proof: the factorization

f̃: C [figure] X with f̂ = f̃c

is the desired f/(ch′hh_{0}). Indeed,

f̃ch′hh_{0} = f̂(h′hh_{0}) = f

and given t with f ≤ tch′hh_{0}, then f̂ = f/(h′hh_{0}) ≤ tc. Thus f̃c ≤ tc which implies f̃ ≤ t. The desired equality

[f/(ch′hh_{0})] · c = f/(h′hh_{0})

in other words

f̂ = f̃c = f/(h′hh_{0})

is the definition of f̂.

In order to prove (27) first recall that X is Kan-injective with respect to S_{0} and S, hence, f/h_{0} and (f/h_{0})/h exist. From this we easily deduce

f/(hh_{0}) = (f/h_{0})/h

and then (26) yields

f̂h′ = (f/h_{0})/h.  (28)

By Kan-injectivity with respect to S this implies

f̂g_{1} = f̂h′b = [(f/h_{0})/h] · b = [(f/h_{0}) · a] /k.  (29)

Next recall that coinserter also assumes g_{1}k ≤ g_{2}k, thus f̂g_{1}k ≤ f̂g_{2}k, and then, using (29), we obtain (27).

(5) Right cancellation. Let X be Kan-injective with respect to the squares

S = \xymatrix{A′ \ar[d]_{a} \ar[r]^{k′} & B′ \ar[d]^{b} \ar[r]^{k} & C′ \ar[d]^{c} \\ A \ar[r]_{h′} & B \ar[r]_{h} & C} ,  S(h) = [figure: B; h; C; B; h; C]  and S(k) = [figure: B′; k; C′; B′; k; C′] .

Given a morphism f : A [figure] X, put

f/h′ = [f/(hh′)] · h.

Then (f/h′) · h′ = f is clear. And if f ≤ gh′, then, recalling Kan-injectivity with respect to S(h), we get g = (g/h)h, hence

f ≤ (g/h)(hh′)

which implies

f/(hh′) ≤ g/h

and yields

[f/(h′h)] · h ≤ g

366  JIŘÍ ADÁMEK AND LURDES SOUSA

as desired. Analogously, (fa)/k′ = [(fa)/(kk′)] · k and this yields

(f/h′) · b = (fa)/k′

as required.

(6) Upper cancellation. Let X be Kan-injective w.r.t. the squares S_{i} and composites of S_{i} with S (i ∈ I). Given a morphism f as follows

[figure: A_{i}; a_{i}; h_{i}; S_{i}; B_{i}; b_{i}; A; a; k; S; B; b; A′; f; h; B′; f/h; X]

we have f/h satisfying

(f/h)bb_{i} = (faa_{i})/h_{i} (i ∈ I).

The desired equality

(fa)/k = (f/h) · b

follows, since (b_{i}) is collectively epic, from

[(fa)/k] · b_{i} = (faa_{i})/h_{i} by Kan-injectivity with respect to S

= (f/h)(bb_{i}) by Kan-injectivity with respect to the composite.

This concludes the proof of soundness.

4.5. Lemma. The following deduction rules are consequences of the Kan-injectivity Logic:

S-RULE  \frac{[figure: h_{1}; h_{2}]}{S(h_{r})}  for r = 1 or 2

and

TRANSFER  [figure: h; h; h]

Proof. S-rule is a special case of pushout: S(h_{r}) is a pushout square. Transfer follows by applying right cancellation as follows:

S(h) = [figure: h; h; h]

4.6. Lemma. The following deduction rule is a consequence of the Kan-Injectivity Logic:

COEQUALIZER  [figure: k; a; b_{1}; h; k; a; b_{2}; h; h; c; ch]  for c = coeq(b_{1}, b_{2})

Proof. Form coinserters

k_{1} = coins(b_{1}, b_{2}) and k_{2} = coins(b_{2}, b_{1}).

Then we apply coinserter to the following diagrams

[figure: k; a; S; b_{i}; b_{i}; A; h; S_{0}; B; B; A; A; h; A; h; \overline{S}]  (i = 1, 2)

where S_{0} follows by transfer and \overline{S} by S-rule, and we deduce the squares below from the above assumptions:

[figure: A; h; B; k_{1}; A; k_{1}h; K_{1}; and; A; h; B; k_{2}; A; k_{2}h; K_{2}]

The coequalizer c is clearly a pushout of k_{1} and k_{2}:

\xymatrix{ & B \ar[dl]_{k_{1}} \ar[dr]^{k_{2}} \ar[dd]^{c} \\ K_{1} \ar[dr] &  & K_{2} \ar[dl] \\  & C}

By applying wide pushout with s = h we derive

[figure: h; c; ch]

4.7. Remark. Let X_{i} (i < λ) be an α-chain with connecting maps x_{ij}. We can construct its colimit using wide pushouts as follows:

First form a wide pushout of all x_{0i}

\xymatrix{X_{0} \ar[ddr]_{p_{0}} \ar[r]^{x_{0i}} & X_{i} \ar[dd]^{p_{i}} \\  &  & (i < α) \\  & P}  (30)

For all pairs i ≤ i′ < α form the following coequalizer

\xymatrix{X_{i} \ar[r]^{p_{i}} \ar[r]_{p_{i′}x_{ii′}} & P \ar[r]^{c_{ii′}} & C_{ii′}}  (31)

Finally, the wide pushout of all these coequalizers is formed

\xymatrix{P \ar[dr]_{g} \ar[r]^{c_{ii′}} & C_{ii′} \ar[d]^{_{\overline{c}_{ii′}}} \\  & K}  (32)

Then K is the colimit of the given diagram with the following colimit cocone:

\xymatrix{X_{i} \ar[r]^{p_{i}} & P \ar[r]^{g} & K} (i < α).

Indeed, since g merges the parallel pair in (31), all gp_{i} form a cocone.

Let y_{i} : X_{i} [figure] Y (i < α) be another cocone. Then the unique y : P [figure] Y with y_{i} = yp_{i} (i < α) clearly merges the parallel pair of (31). Hence, y factorizes through each c_{ii′}. Consequently, y = \overline{y}g for a unique \overline{y} : K [figure] Y. This is the desired factorization:

y_{i} = yp_{i} = \overline{y}(gp_{i}) for i < α.

The uniqueness of this factorization is easy to verify.

4.8. Lemma. (Transfinite Composition) Let (X_{i})_{i∈α} be an α-chain with connecting morphisms X_{i} −−→ X_{j} and a colimit k_{i} : X_{i} [figure] K (i < α). The following deduction rule follows, for every j < α, from the Kan-Injectivity Logic.

TRANSFINITE COMPOSITION

[figure: X_{0}; X_{j}; X_{0}; X_{k}; (j ≤ k ≤ α); X_{0}; X_{j}; k_{j}; X_{0}; k_{0}; K]

Proof. We can assume k_{i} = gp_{i} for all i, see the above remark. By applying wide pushout to the premisses of our rule we get, for every i < α, the deduction of the square

[figure: X_{0}; X_{i}; p_{i}; X_{0}; p_{0}; P]  (33)

This makes it possible to apply coequalizer to (30) to derive

[figure: X_{b}; p_{0}; P; c_{ii′}; X_{0}; c_{ii′}p_{0}; C_{ii′}]  (34)

for all i ≤ i′ < α. Next apply wide pushout to (34) with h = p_{0} to derive

[figure: X_{0}; p_{0}; P; c_{ii′}; C_{ii′}; _{\overline{c}_{ii′}}; X_{0}; p_{0}; P; g; K] .

For i = i′ = j we can put c_{jj} = id in (31), thus g = \overline{c}_{jj} in (32). Hence we have derived the following square

[figure: X_{0}; p_{0}; P; g; X_{0}; p_{0}; P; g; K]

Vertical composition with (33) (for i = j) yields the desired square:

[figure: X_{0}; X_{j}; h_{j}=gp_{j}; X_{0}; h=gp_{0}; K]

5. Proof of Completeness

Throughout this section ℋ is a set of squares in a locally ranked order-enriched category 𝒳. We prove that the Kan-Injectivity Logic is complete.

First a preliminary result. Recall the reflection chain from Section 3.

5.1. Lemma. For all ordinals m ≤ i the squares

[figure: X_{0}; X_{m}; X_{0}; X_{i}]  (35)

can be deduced from ℋ.

Proof. We proceed by transfinite induction in i.

Initial step. Use axiom on the split square

X_{0}  X_{0} X_{0}  X_{0}

Limit step. This follows from transfinite composition, see Lemma 4.8.

For m = i, S(X_{0} −−→ X_{i}) is obtained by S-rule (Lemma 4.5).

Isolated step i ↦ i + 1 (i even). Given a square

\xymatrix{A_{1} \ar[dd]_{a} \ar[rr]^{h_{1}} &  & B_{1} \ar[dd]^{b} \\  & S \\ A_{2} \ar[rr]_{h_{2}} &  & B_{2}}

in ℋ and a morphism f : A_{r} [figure] X_{i} (r = 1 or 2), we have the following deduction:

S pushout

[figure: f; h_{r}; \overline{f}; _{\overline{h}_{r}}]  (36)

transfer (Lemma 4.5)

[figure: X_{i}; X_{i}; _{\overline{h}_{r}}; X_{i}; _{\overline{h}_{r}}; Q_{f}]

wide pushout

[figure: X_{i}; ^{\overline{h}^{r}}; Q_{f}; q_{f}; X_{i}; X_{i+1}]  (37)

transfer (Lemma 4.5)

[figure: X_{i}; X_{i}; X_{i}; X_{i+1}]  (38)

By induction hypothesis, (35) are given. Our task is to verify, for every m ≤ i + 1, the corresponding square. Horizontal composition of (38) with (35) for m = i deduces

[figure: X_{0}; X_{i}; X_{0}; X_{i+1}]

and vertical composition of (38) with (35), m ≤ i, yields the desired square

[figure: X_{0}; X_{k}; X_{0}; X_{i}; X_{0}; X_{i+1}]  (39)

For m = i + 1, we deduce the square S(X_{0} −−→ X_{i+1}) by (39) via S-rule (Lemma 4.5).

Isolated step i + 1 ↦ i + 2 (i even). We first observe that the square (9) of Definition 3.1 is deduced from ℋ by composition applied to (36) and (37):

[figure: A_{r}; f; h_{r}; B_{r}; \overline{f}; f⫽h_{r}; X_{i}; _{\overline{h}_{r}}; Q_{f}; q_{f}; X_{i}; X_{i+1}]  (40)

For every coinserter (12) we can thus apply coinserter to k = h_{r} and the following diagram

[figure: A_{r}; h_{r}; f′; S; B_{r}; f′⫽h_{r}; X_{j}; X_{j+1}; X_{i+1}; c_{f,g}; C_{f,g}; X_{0}; S_{0}; X_{0}; \overline{S}; X_{0}]

Indeed, the assumptions are S, by (40), S_{0}, which is (35) for m = j and i = j + 1, and \overline{S}, which is (35) with m = j + 1 and i + 1 in the place of i. Consequently, we deduce the square

[figure: X_{0}; X_{i+1}; c_{f,g}; X_{0}; X_{i+1}; c_{f,g}; C_{f,g}]  (41)

For every coinserter (14), first observe that the square

S = [figure: A_{1}; h_{1}; a; S′; B_{1}; b; A_{2}; h_{2}; f′; B_{2}; f′⫽h_{2}; X_{i}; X_{i+1}]

is deduced from S′ and (40) by composition. We apply coinserter to k = h_{1} and the following diagram

[figure: A_{1}; h_{1}; S; B_{1}; X_{i+1}; X_{i}; X_{i+1}; X_{i+1}; c_{f,g}; C_{f,g}; X_{0}; S_{0}; X_{0}; \overline{S}; X_{0}]

where the second and last assumptions of coinserter are just instances of (35) which are deduced from ℋ by induction hypothesis. Thus we again deduce the square (41).

Apply wide pushout to (15) with h ≡ X_{0} −−→ X_{i+1} to deduce all the squares

[figure: X_{0}; X_{i+1}; c_{f,g}; C_{f,g}; t_{f,g}; X_{0}; X_{i+1}; X_{i+2}]  (42)

A vertical composition with (41) deduces

[figure: X_{0}; X_{i+1}; X_{0}; X_{i+2}]

which vertically composed with (39) yields

[figure: X_{0}; X_{m}; for all m ≤ i + 1.; X_{0}; X_{i+2}]

The remaining case m = i + 2 is then deduced by S-rule.

5.2. Theorem. (Kan-Injectivity Logic is Complete and Sound) A square is a Kaninjectivity consequence of a set of squares iff it can be deduced from that set.

Proof. For soundness see Proposition 4.4. Let ℋ be a set of squares and let the following square

S ≡ \xymatrix{A_{1} \ar[d]_{a} \ar[r]^{h_{1}} & B_{1} \ar[d]^{b} \\ A_{2} \ar[r]_{h_{2}} & B_{2}}

be a Kan-injectivity consequence of ℋ. We find a deduction of S from ℋ.

Let R : 𝒳 [figure] LInj(ℋ) denote the reflector, RX = X_{k} and Ru = u_{k} (see Proposition 3.9).

(1) We first use the fact that RA_{1} and RA_{2} are Kan-injective with respect to S, thus, η_{A_{1}}/h_{1} and η_{A_{2}}/h_{2} exist, and we prove that they form a square as follows:

\xymatrix{B_{1} \ar[d]_{b} \ar[r]^{η_{A_{1}}/h_{1}} & RA_{1} \ar[d]^{Ra} \\ B_{2} \ar[r]_{η_{A_{2}}/h_{2}} & RA_{2}}

Indeed, the morphism Ra is Kan-injective with respect to h_{1}, thus

Ra · (η_{A_{1}}/h_{1}) = (Ra · η_{A_{1}})/h_{1} = (η_{A_{2}} · a)/h_{1}

and, since RA_{2} is Kan-injective with respect to S, we have

(η_{A_{2}} · a)/h_{1} = (η_{A_{2}}/h_{2}) · b.

(2) The morphism Rh_{1} : RA_{1} [figure] RB_{1} is a left adjoint section. (This was proved in [6] but we include the short proof for he convenience of the reader.) Indeed, since RA_{1} is Kan-injective with respect to h_{1} (being Kan-injective with respect to S), using the universal property of η_{A_{1}}, we have η_{A_{1}}/h_{1} = h_{1}^{∗} · η_{B_{1}}

\xymatrix{A_{1} \ar[d]_{η_{A_{1}}} \ar[r]^{h_{1}} & B_{1} \ar[dl]_{η_{A_{1}}/h_{1}} \ar[d]^{η_{B_{1}}} \\ RA_{1} \ar[r]^{Rh_{1}} & RB_{1} \ar[l]^{h_{1}^{∗}}}

for a unique h_{1}^{∗} in LInj(ℋ). This is the desired morphism with

h_{1}^{∗} · Rh_{1} = id and Rh_{1} · h_{1}^{∗} ≤ id.

Indeed, both composites lie in LInj(ℋ), thus, it is sufficient to verify (a) h_{1}^{∗} ·Rh_{1} ·η_{A_{1}} = η_{A_{1}} - see the above diagram, and (b) Rh_{1} · h_{1}^{∗} · η_{B_{1}} ≤ η_{B_{1}}. We use the trivial inequality (η_{B_{1}} · h_{1})/h_{1} ≤ η_{B_{1}} and the above diagram to see that (b) holds.

(3) The square

R(S) ≡ \xymatrix{RA_{1} \ar[d]_{Ra} \ar[r]^{Rh_{1}} & RB_{1} \ar[d]^{Rb} \\ RA_{2} \ar[r]_{h_{2}} & RB_{2}}

splits. (This is Lemma 3.4 in [16]; here we present a different proof.) Indeed, we have h_{1}^{∗} : RB_{1} [figure] RA_{1} in (2) and, analogously, h_{2}^{∗} : RB_{2} [figure] RA_{2}. It remains to verify the following square

\xymatrix{RB_{1} \ar[d]_{Rb} \ar[r]^{h_{1}^{∗}} & RA_{1} \ar[d]^{Ra} \\ RB_{2} \ar[r]_{h_{2}^{∗}} & RA_{2}}

It lies in LInj(ℋ), thus, it is sufficient to prove that it commutes when precomposed by η_{B_{1}}:

\xymatrix{RB_{1} \ar[ddd]_{Rb} \ar[rr]^{h_{1}^{∗}} &  & RA_{1} \ar[ddd]^{Ra} \\  & B_{1} \ar[ul]^{η_{B_{1}}} \ar[d]_{b} \ar[ur]_{η_{A_{1}}/h_{1}} \\  & B_{2} \ar[dl]_{η_{B_{2}}} \ar[dr]^{η_{A_{2}}/h_{2}} \\ RB_{2} \ar[rr]_{h_{2}^{∗}} &  & RA_{2}}

Indeed, use the square in (1) above.

(4) In part (5) we are going to prove that every naturality square of η, in particular

\xymatrix{A_{1} \ar[d]_{a} \ar[r]^{η_{A_{1}}} & RA_{1} \ar[d]^{Ra} \\ A_{2} \ar[r]_{η_{A_{2}}} & RA_{2}}

can be deduced from ℋ. Due to axiom, the square R(S) of part (3) is also deducible, and their horizontal composite yields

\xymatrix{A_{1} \ar[d]_{a} \ar[r]^{η_{A_{1}}} & RA_{1} \ar[r]^{Rh_{1}} & RB_{1} \ar[d]^{Rb} \\ A_{2} \ar[r]_{η_{A_{2}}} & RA_{2} \ar[r]_{Rh_{2}} & RB_{2}}

which is the same square as the following composite

\xymatrix{A_{1} \ar[dd]_{a} \ar[rr]^{h_{1}} &  & B_{1} \ar[dd]^{b} \ar[r]^{η_{B_{1}}} & RB_{1} \ar[dd]^{Rb} \\  & S \\ A_{2} \ar[rr]_{h_{2}} &  & B_{2} \ar[r]_{η_{B_{2}}} & RB_{2}}

Thus, S is deduced via right cancellation, since the right-hand square is deducible (being, again, a naturality square of η). This concludes the proof.

(5) To prove that naturality squares of η are deducible from ℋ, we consider the squares

\xymatrix{X \ar[d]_{u} \ar@{-->}[r] & X_{i} \ar[d]^{u_{i}} \\ X̃ \ar@{-->}[r] & X̃_{i}}  (43)

for all ordinals i and prove their deducibility by transfinite induction. By Proposition 3.9 the case i = k is the desired square.

Initial step: the square

[figure: X; u; X; u; X̃; X̃]

is split, we can apply axiom .

Limit step: Given a limit ordinal i, such that (43) is deducible for every m < i in place of i, compose (43) vertically with (35) to get a deducible (outward) square as follows:

[figure: X_{0}; X_{m}; X; u; X_{i}; u_{i}; X̃; X̃_{i}]

The upper square is deducible by Lemma 5.1, and all \xymatrix{X_{m} \ar@{-->}[r] & X_{i}} are collectively epic, hence, the desired lower square is deduced by upper cancellation .

Isolated step i ↦ i + 1 (i even). We are going to derive the square

\xymatrix{X_{i} \ar[d]_{u_{i}} \ar@{-->}[r] & X_{i+1} \ar[d]^{u_{i+1}} \\ X̃_{i} \ar@{-->}[r] & X_{i+1}}

and compose it horizontally with the square assumed by induction hypothesis.

For that take all pairs (S, f) defining the step i ↦ i + 1. Then we apply upper cancellation to the following diagram

[figure: X_{i}; ^{\overline{h}^{r}}; Q_{f}; q_{f}; X_{i}; u_{i}; X_{i+1}; u_{i+1}; X̃_{i}; X̃_{i+1}]

The upper squares are deduced, see (37), and all q_{f} are collectively epic, thus, we only need a deduction of the composite square. This is, by the definition of u_{i+1} in Remark 3.7 the square

\xymatrix{X_{i} \ar[dd]_{u_{i}} \ar[r]^{^{\overline{h}^{r}}} & Q_{f} \ar[d]^{f^{∗}} \\  & Q̃_{u_{i}f} \ar[d]^{q̃_{u_{i}f}} \\ X̃_{i} \ar@{-->}[r] & X̃_{i+1}}  (44)

Now in order to derive (44), recall the pushout

[figure: X_{i}; u_{i}; S_{0}; ^{\overline{h}^{r}}; Q′_{f}; f^{∗}; X̃_{i}; h̃_{r}; Q̃_{u_{i}f}]

from Notation 3.8 and compose it vertically with the square

[figure: X̃_{i}; h̃_{r}; Q̃_{u_{i}f}; q̃_{u_{i}f}; X̃_{i}; X̃_{i+1}]

The former square can be deduced from (36) via pushout, for the latter one see (37). Thus (44) is deducible.

Isolated step i + 1 ↦ i + 2 (i even). Using (42), we can again apply upper cancellation :

[figure: X; X_{i+1}; c_{f,g}; C_{f,g}; _{\overline{c}_{f,g}}; X; u; X_{i+2}; u_{i+2}; X̃; X̃_{i+2}]  (45)

We only need to deduce the composite square.

The following composite

[figure: X; u; X_{i+1}; u_{i+1}; X̃; X̃_{i+1}; X̃; X̃_{i+2}]

is deducible due to Lemma 5.1, and the right-hand vertical morphism is

\xymatrix{X_{i+1} \ar[r]^{c_{f,g}} & C_{f,g} \ar[r]^{d_{f,g}} & C̃_{f̃,g̃} \ar[r]^{t̃_{f̃,g̃}} & X̃_{i+2}}

by (22). Thus we have deduced the following composite

[figure: X; X_{i+1}; c_{f,g}; X; u; X_{i+1}; c_{f,g}; C_{fg}; d_{f,g}; C̃_{f̃,g̃}; t̃_{f̃,g̃}; X̃; X̃_{i+2}]

The upper square is (41). Moreover, c_{f,g} is an epimorphism (being a coinserter). Thus upper cancellation yields the deduction of the lower square. This is the desired composite square (45): indeed, see (23).

References

[1] J. Adámek, M. Hébert, L. Sousa, A logic of orthogonality, Archivum Mathematicum 42, no.4, (2006), 309-334.

[2] J. Adámek, M. Hébert and L. Sousa, The orthogonal subcategory problem and the small object argument, Appl. Categ. Structures 17 (2009), 211–246.

[3] J. Adámek, M. Sobral, L. Sousa, A logic of implications in algebra and coalgebra, Algebra Univers. 61 (2009) 313-337.

[4] J. Adámek, L. Sousa, J. Velebil, Kan injectivity in order-enriched categories, Math. Structures Comput. Sci. 25 (2015), no. 1, 6-45.

[5] B. Banaschewski and G. Bruns, Categorical characterisation of the MacNeille completion, Arch. Math. (Basel) 18 (1967), 369-377.

[6] M. Carvalho and L. Sousa, Order-preserving reflectors and injectivity, Topology Appl. 158 (2011), no. 17, 2408-2422.

[7] M. Carvalho and L. Sousa, On Kan-injectivity of locales and spaces, Appl. Categor. Struct. 25 (2017), no. 1, 83-104.

[8] M. H. Escardó, Properly injective spaces and function spaces, Topology Appl. 89(1-2) (1998), 75 -120.

[9] M. H. Escardó, R. C. Flagg, Semantic domains, injective spaces and monads, Electronic Notes in Theoretical Computer Science 20 (1999).

[10] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, D. S. Scott, A Compendium of Continuous Lattices, Springer Verlag 1980.

[11] P. T. Johnstone, Sketches of an Elephant: A Topos Theory Compendium, vol. 2. Number 44 in Oxford Logic Guides, The Clarendon Press, Oxford University Press, Oxford, 2002.

[12] M. Kelly, A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on, Bull. Austral. Math. Soc. 22 (1980), 1-84.

[13] G. M. Kelly, Basic concepts of enriched category theory, London Math. Soc. Lecture Notes Series 64, Cambridge Univ. Press, 1982, Repr. Theory Appl. Categ. 10 (2005), 1-136.

[14] A. Kock, Monads for which structures are adjoint to units (version 3), J. Pure Appl. Algebra 104 (1995), 41-59.

[15] D.S. Scott, Continuous lattices. In Toposes, Algebraic Geometry and Logic, F.W. Lawvere (ed.), Lect. Notes in Math. 274 , Springer (1972) 3.

[16] L. Sousa, A calculus of lax fractions, J. Pure Appl. Algebra 221 (2017), 422-448.

Department of Mathematics, Faculty of Electrical Engineering Czech Technical University in Prague, Czech Republic

CMUC, University of Coimbra, Portugal Polytechnic Institute of Viseu, Portugal

Email: adamek@iti.cs.tu-bs.de
  sousa@estv.ipv.pt
This article may be accessed at http://www.tac.mta.ca/tac/

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available from the journal’s server at http://www.tac.mta.ca/tac/. It is archived electronically and in printed paper format.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors The typesetting language of the journal is TEX, and L^{A}TEX2e is required. Articles in PDF format may be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor. Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors.

Clemens Berger, Université de Nice-Sophia Antipolis: cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com Valeria de Paiva: Nuance Communications Inc: valeria.depaiva@gmail.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne: kathryn.hess@epfl.ch Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Edinburgh: Tom.Leinster@ed.ac.uk Ieke Moerdijk, Utrecht University: i.moerdijk@uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Alex Simpson, University of Ljubljana: Alex.Simpson@fmf.uni-lj.si James Stasheff, University of North Carolina: jds@math.upenn.edu Ross Street, Macquarie University: ross.street@mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Université du Québec à Montréal : tierney.myles4@gmail.com R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca