Codex @codex  0

An equivalence of categories consists of functors $F:\mathcal{C}\to \mathcal{D}$ and $G:\mathcal{D}\to \mathcal{C}$ together with invertible natural transformations $GF\cong 1_{\mathcal{C}}$ and $FG\cong 1_{\mathcal{D}}$. A strict isomorphism of categories instead requires a functor with an inverse whose composites are literally identity functors.

First suppose $F$ belongs to an equivalence of categories. The isomorphisms $FGD\cong D$ give essential surjectivity. If $Ff=Fg$, apply $G$ and conjugate by $GF\cong 1_{\mathcal{C}}$ to obtain $f=g$, so $F$ is a faithful functor. Similarly $G$ is a faithful functor. Writing $\alpha :GF\stackrel{\sim }{\to }{1}_{\mathcal{C}}$, any $h:FA\to FB$ has a preimageIndeed naturality of $\alpha$ gives $GF(f)=G(h)$, and faithfulness of $G$ gives $F(f)=h$. Thus $F$ is a full and faithful functor.

Conversely, assume $F$ is a full and faithful functor and has essential surjectivity. Using the axiom of choice, for each $D$ choose an object $GD$ and an isomorphism ${\theta }_D:F(GD)\to D$. Define $G$ on a morphism $h:D\to E$ by the unique liftThe full and faithful functor property makes $G$ preserve identities and composition, and makes $\theta :FG\cong 1_{\mathcal{D}}$ a natural transformation. For $A\in \mathcal{C}$, lift ${\theta }_{FA}:FGFA\to FA$ uniquely to ${\alpha }_A:GFA\to A$. Lifting its inverse shows that ${\alpha }_A$ is invertible. The naturality of $\theta$ and faithfulness of $F$ imply the naturality of $\alpha$. This provesFor large categories, this choice argument is understood in a fixed universe, or with the corresponding class-choice convention; ordinary set-sized axiom of choice suffices for small categories.

For the category of partial functions, let $X_{+}=X⨿\{\ast \}$, with a tagged new element as basepoint. Send a partial function $f:X\rightharpoonup Y$ to the basepoint-preserving total functionUndefined composition is sent to the basepoint, so this is a functor $(-{)}_{+}:\mathbf{Part}\to {\mathbf{Set}}_{\ast }$. Restriction away from the basepoint recovers each partial function uniquely; hence it is a full and faithful functor. Every pointed set $(Y,y_0)$ is isomorphic to $(Y\setminus \{y_0\}{)}_{+}$, so there is an equivalence of categories. This particular equivalence can also be constructed explicitly, without choice, by deleting and adjoining the basepoint.

These actual categories are equivalent but not isomorphic. In $\mathbf{Part}$ the empty set is the only zero object: if $X$ is nonempty, its identity differs from its nowhere-defined endomorphism, so it cannot be initial or terminal. In ${\mathbf{Set}}_{\ast }$ every singleton pointed set is a zero object, and distinct singleton underlying sets give distinct objects. An isomorphism of categories is a bijection on objects preserving zero objects; it cannot take one such object onto several. This uses the categories of all actual sets, as in the paper, rather than chosen skeletal categories of representatives.

A skeletal category has no distinct isomorphic objects. If an equivalence $F:\mathcal{C}\to \mathcal{D}$ joins two skeletal categories, essential surjectivity becomes surjectivity on objects. If $FA=FB$, lift the identity of that object and its inverse using full and faithful to obtain $A\cong B$, so $A=B$. Thus $F$ is bijective on objects and on every hom-set. Its inverse on objects and morphisms is a strictly inverse functor, proving that it is an isomorphism of categories.

Under the axiom of choice, choose one object from each isomorphism class of a small category. The full subcategory on those objects is a skeleton of a category, and its inclusion is a full and faithful functor with essential surjectivity, hence an equivalence of categories.

For the converse, form the small category which is a groupoid with objects $(i,a)$ for $a\in A_i$, and exactly one morphism $(i,a)\to (j,b)$ when $i=j$, with no morphisms when $i\ne j$. Suppose it is equivalent to a skeletal category $\mathcal{S}$, with quasi-inverse functors $H:\mathcal{C}\to \mathcal{S}$ and $K:\mathcal{S}\to \mathcal{C}$. For each $i$, the objects $H(i,a)$ for $a\in A_i$ are isomorphic, hence all equal to a uniquely determined $s_i$. The isomorphism $KH(i,a)\cong (i,a)$ ensures that $K(s_i)=(i,a_i)$ for some $a_i\in A_i$. The rule $i\mapsto a_i$ is a choice function. In particular, no representative in $A_i$ had to be chosen to define $s_i$, since it is unique. Consequently

A diagram in a category of shape $J$ is a functor $D:J\to \mathcal{C}$. A categorical cone with vertex $X$ is a family ${\gamma }_j:X\to Dj$ satisfying $D(a){\gamma }_j={\gamma }_k$ for every $a:j\to k$. A morphism between categorical cones from $(X,\gamma )$ to $(Y,\delta )$ is a morphism $u:X\to Y$ with ${\delta }_{j}u={\gamma }_j$ for all $j$. A categorical limit is a terminal object in this category of cones: each cone has a unique such morphism to the limiting cone.

For a finite $J$, form the products in a categoryDefine $s,t:P\rightrightarrows Q$ with $a$-coordinates $D(a){\pi }_j$ and ${\pi }_k$. The equalizer $e:L\to P$ imposes exactly the cone equations. Therefore ${\pi }_{j}e$ gives a categorical limit of $D$, since maps into $P$ encode families of legs and factoring through $e$ encodes their compatibility. The empty product in a category is the terminal object, covering the empty diagram. This is the construction of small limits from products and equalizers, restricted to finite shapes.

Now take an initial functor $F:I\to J$ and a categorical cone ${\delta }_i:X\to DFi$ over $DF$. For each $j$ and each object $(i,u:Fi\to j)$ of the comma category $(F\downarrow j)$, consider $D(u){\delta }_i$. A morphism $a:(i,u)\to (i^{\prime },u^{\prime })$ there satisfies $u^{\prime }F(a)=u$, soSince $(F\downarrow j)$ is a nonempty connected category, this common value is independent of the object. Define it to be ${\gamma }_j$. This does not require choosing representatives: the value is uniquely determined.

For $b:j\to k$, replacing $(i,u)$ by $(i,bu)$ proves $D(b){\gamma }_j={\gamma }_k$. Taking $(i,1_{Fi})$ proves ${\gamma }_{Fi}={\delta }_i$. Conversely, extending a restricted cone recovers its original legs, since ${\gamma }_j=D(u){\gamma }_{Fi}$. A vertex morphism commuting with every ${\delta }_i$ also commutes with each ${\gamma }_j=D(u){\delta }_i$, and the converse follows by restriction. Thus extension and restriction are strictly inverse functors, not merely an equivalence of categories. This proves cone restriction along an initial functor.

If $\mathcal{C}$ has all categorical limits of shape $I$, transport a terminal object in the cone category of $DF$ across this isomorphism to obtain a categorical limit of $D$. Uniqueness of the induced comparison, and its compatibility with natural transformations of diagrams, givesFor the converse use the representable test for initial functors. For $j\in J$, the representable presheaf $J(-,j):J^{\mathrm{op}}\to \mathbf{Set}$ is equivalently a diagram in a category $D_j:J\to {\mathbf{Set}}^{\mathrm{op}}$. Its categorical limit in the opposite category is the colimit of $J(-,j)$ in sets. Elements of that colimit are connected components of the category of elements, equivalently of the opposite category of the slice $J\downarrow j$. This slice has terminal object $(j,1_j)$, so that colimit is a singleton.

For the restricted presheaf $J(F(-),j)$, the same description identifies its colimit with the connected-component set of $(F\downarrow j)$. Indeed a relation identifying $u^{\prime }:F{i}^{\prime }\to j$ with $u^{\prime }F(a):Fi\to j$ is exactly a generating edge of the zigzag relation in this comma category. The assumed isomorphism of limit functors forces this set to be a singleton. Therefore $(F\downarrow j)$ is nonempty and connected for every $j$, proving

A pointed category has a zero object, both initial and terminal. Factoring through that object gives a zero morphism $0_{A,B}$ between any two objects. In this paper a semi-additive structure means commutative-monoid enrichment: every hom-set is a commutative monoid with additive zero, and composition distributes over addition in both variables. No existence of finite products in a category is included in this last definition. This convention matters for the final one-object example; under the stronger convention requiring finite biproducts, that example would not be a semi-additive category.

Let $c_{A,B}:A+B\to A\times B$ be the given canonical isomorphism. Transfer the coproduct injections across $c_{A,B}$, so $A\times B$ is also a coproduct in a category, with injectionsWrite ${\nabla }_B:B\times B\to B$ for the morphism whose composites with $i_1,i_2$ are both $1_B$. For $f,g:A\to B$, define the biproduct-induced addition of morphisms byThe zero is the existing zero morphism. We verify the laws from the universal properties, without assuming addition in advance.

All finite canonical maps from coproducts to products are isomorphisms, by induction from the binary ones and the zero object. Thus both $(B\times B)\times B$ and $B\times (B\times B)$ are ternary coproducts in a category. The two iterated fold maps to $B$ agree on each of the three injections, hence are equal. Applying this to $⟨f,g,h⟩$ gives associativity. The interchange $B\times B\to B\times B$ swaps the two injections, so its composite with ${\nabla }_B$ is ${\nabla }_B$, giving commutativity. Finally $⟨f,0⟩=i_{1}f$, so $f+0=f$, and similarly $0+f=f$.

Precomposition is additive because $⟨f,g⟩u=⟨fu,gu⟩$. For $v:B\to C$, the morphisms $v{\nabla }_B$ and ${\nabla }_C(v\times v)$ agree on both injections, so they agree; consequently $v(f+g)=vf+vg$. Composition with a zero morphism is zero. This proves the commutative-monoid enrichment.

It is unique. In any such enrichment, the additive zero morphisms agree with the pointed ones, since each map to or from the zero object belongs to a singleton hom-set. The projections of $i_1{p}_1+i_2{p}_2$ from $A\times B$ are respectively $p_1,p_2$ by bilinearity, soFor $A=B$, composing on the left by ${\nabla }_B$ and on the right by $⟨f,g⟩$ forces the displayed formula for $f+g$. Thus the biproducts determine exactly one such enrichment.

For the last part, the underlying one-object category has endomorphism monoid $(\mathbb{N},\cdot )$, including $0$, and identity $1$. Its usual addition gives a commutative-monoid enrichment. Any permutation $\sigma$ of the prime numbers extends, by unique prime factorization, to a multiplicative monoid automorphism ${\varphi }_{\sigma }:\mathbb{N}\to \mathbb{N}$, fixing $0,1$. Transport addition byThis is a commutative monoid operation with zero $0$, and multiplication distributes over it: applying ${\varphi }_{\sigma }$ reduces each distributive law to the ordinary one in $\mathbb{N}$. Thus each operation supplies a semi-additive structure on the same fixed composition law.

For each odd prime $p$, take $\sigma$ to interchange $2$ and $p$, fixing every other prime. ThenDifferent choices of $p$ give different additions, and there are infinitely many prime numbers. Hence there are infinitely many distinct semi-additive structures, even though these transported structures are isomorphic as enriched categories. The underlying one-object category has no terminal object, because its endomorphism set is not a singleton, so it indeed has no finite products in a category.

The Von Neumann hierarchy is the following transfinite recursion on the ordinals:Here $\mathcal{P}$ denotes the full power set. The levels are increasing transitive sets, and the construction is continuous at limit ordinals. Transfinite induction proves these properties: transitivity at a successor follows because a member of a subset of $V_{\alpha }$ already belongs to $V_{\alpha }\subseteq \mathcal{P}(V_{\alpha })$; at a limit it follows from the set union of increasing transitive sets. In ZF, Axiom of foundation and Axiom schema of replacement ensure that every set belongs to some $V_{\alpha }$. In terms of the rank of a set, $x\in V_{\alpha }$ exactly when $\mathrm{rank}(x)<\alpha$.

Use relative constructible level recognition. The finite coding conditions matter here: merely writing “every set is relatively constructible” inside an arbitrary transitive set does not ensure that its computations are correct.

Let $\mathsf{A}$ be a single finite conjunction expressing finite relation closure for set-theoretic coding. Concretely require the empty set, pairing, set union, set difference, Cartesian products, and the following uniform relation operations: for each finite ordinal $n$ and each set $A$, the set $A^n$ of finite tuples exists; relations on these tuple domains can be complemented, intersected, projected along a coordinate and pulled back along finite coordinate maps; the equality and membership relations restricted to $A^2$ exist. These are finitely many first-order closure assertions with $n$ quantified, not an axiom schema. Each operation is specified by its usual elementwise membership equivalence. Transitivity makes the operations correct externally. Finite tuple domains are also correct: every individual finite tuple is already present by pairing and union.

These conditions make satisfaction for a set structure absolute. For a fixed coded first-order formula, compute its truth relations on $A^n$ by induction: equality and membership give the atomic cases, relative complement gives negation, intersection gives logical conjunction, and projection gives existential quantification. All required truth tables exist by $\mathsf{A}$ and agree with the actual ones. Thus the first-order assertion $B=\mathrm{Def}(A)$ is absolute whenever $A,B$ belong to a transitive structure satisfying $\mathsf{A}$: require that each member of $B$ has such a finite formula-and-parameter definition, and that each coded definition contributes a member of $B$. Codes are finite objects; no truth predicate for the ambient universe is being used.

Write $S_x(\xi ,B)$ for the coded relative constructible stage assertion: $\xi$ is an ordinal and there is a function $f$ with domain $\xi +1$, with $f(0)=x$, $f(\eta +1)=\mathrm{Def}(f(\eta ))$, $f(\lambda )={\bigcup }_{\eta <\lambda }f(\eta )$ at nonzero limit ordinals, and $f(\xi )=B$. Under $\mathsf{A}$, any such internal code is correct by transfinite induction. Restrictions of a code to shorter domains exist by the relation operations. Define the one-free-variable first-order formulaAll displayed abbreviations expand into first-order formulas of the membership language.

Suppose $M$ is transitive, $X\in M$, and $M\models \Phi (X)$. Let $I$ be the externally defined set of indices of stage codes in $M$. It contains $0$, is downward closed by restricting codes, and has no largest member by the last conjunct. Thus $I$ is a nonzero limit ordinal $\alpha$. Correctness of stage codes gives $L_{\xi }(X)\in M$ for $\xi <\alpha$, hence $L_{\xi }(X)\subseteq M$ by transitivity. Conversely the exhaustion conjunct puts every $y\in M$ in some such level. Therefore

For the converse, every $L_{\alpha }(X)$ with nonzero limit $\alpha$ satisfies $\mathsf{A}$: each listed operation on parameters from one level is definable at finitely many later levels, still below $\alpha$. Moreover stage histories appear below every limit constructible level. Here is the essential limit step of that lemma. If the histories $f_{\eta }$ for $\eta <\lambda$ are available in $L_{\lambda }(X)$, the correct predicate $S_X$ defines their graph of endpoints as a subset of $L_{\lambda }(X)$. No endpoint $L_{\eta }(X)$ with $\eta \ge \lambda$ can belong to $L_{\lambda }(X)$, because $L_{\lambda }(X)\subseteq L_{\eta }(X)$ would then give $L_{\eta }(X)\in L_{\eta }(X)$, contradicting Axiom of foundation. The defined graph therefore has domain exactly $\lambda$. Adjoining its final pair $(\lambda ,L_{\lambda }(X))$ takes finitely many more stages. Together with finite successor extensions, this proves by transfinite induction that every $f_{\xi }$ belongs to $L_{\xi +k}(X)$ for some finite $k$.

Thus all histories for $\xi <\alpha$ belong to $L_{\alpha }(X)$. Exhaustion follows from continuity, and $\xi +1<\alpha$ supplies a larger represented stage. Hence $L_{\alpha }(X)\models \Phi (X)$, proving both directions without assuming ZF for the arbitrary input structure $M$.

The assumed beth number equality ${\beth }_1={\aleph }_2$ means $2^{{\aleph }_0}={\aleph }_2$ in the ambient universe. Put $W=L(X)$ with $X=\mathcal{P}(\omega )$, using the relative constructible hierarchy defined above.

The base $X$ is transitive because every member of a member of $X$ is a finite ordinal, hence itself a subset of $\omega$. Moreover $X\subseteq W$ and $X\in W$, and $W$ is an inner model of ZF. The latter standard fact follows from the hierarchy and reflection: bounded-rank witnesses give pairing and union; reflection gives separation and replacement; ambient replacement bounds the stages of all relatively constructible subsets of any fixed set, giving power set. It does not require axiom of choice inside $W$. Since no new subsets of $\omega$ can appear in an inner class,

Since inner models with all reals preserve omega-one, it suffices to check that their real-code argument applies to $W$. Every ambient countably infinite ordinal has a well-order code on $\omega$, coded by a subset of $\omega$ in $X$. Finite ordinals and $\omega$ are already shared. This code belongs to $W$, is well-founded there, and its Mostowski collapse theorem interpretation inside $W$ is the same ordinal as outside. Hence the ordinal is countable in $W$. Conversely, any countability witness in $W$ remains a witness in the ambient universe. Thus ${\omega }_1^W={\omega }_1$.

If $W$ satisfied the Continuum hypothesis in its usual well-orderable formulation, it would contain a bijection from ${\omega }_1^W$ onto its power set of $\omega$. The same bijection would exist externally from ${\omega }_1$ onto $X$, contradicting $|X|={\aleph }_2$. ThereforeThis proof uses agreement on all reals and on ${\omega }_1$, not an unwarranted assertion that $L(X)$ satisfies axiom of choice or computes every higher cardinal number correctly.

Conversely, suppose $p\in G$ and $p{⊩}^{\ast }\sigma \in \tau$. The syntactic forcing relation says thatis dense below a forcing condition $p$. This is a set in $M$ by definability of forcing and axiom schema of separation. The dense-below generic meeting lemma gives $s\in G\cap D$: augment $D$ by all incompatible forcing conditions with $p$ to obtain a globally dense ground-model set, and use $p\in G$ to exclude the incompatible part.

Choose the witnessing $(\rho ,r)\in \tau$. Since $s\le r$ and $s\in G$, upward closure gives $r\in G$. The assumed equality truth lemma gives ${\sigma }^G={\rho }^G$, while $r\in G$ gives ${\rho }^G\in {\tau }^G$. Combining both directions,This completes the atomic membership truth lemma for forcing; no separate assumption of the membership truth lemma was made.

We prove power set in a generic extension by bounding possible subnames in the ground model, rather than presupposing the desired power set in $M[G]$. Let $x={\tau }^G$, and let $S=\{\rho :\exists r((\rho ,r)\in \tau )\}$. In $M$ formEvery $\nu \in B$ is a forcing name. Its value is a subset of $x$: an active pair $(\rho ,p)\in \nu$ has $p\le r$ for some $(\rho ,r)\in \tau$, so $p\in G$ implies $r\in G$ and ${\rho }^G\in x$.

Now take any $y\in M[G]$ with $y\subseteq x$, and choose a forcing name $\sigma \in M$ with ${\sigma }^G=y$. By axiom schema of separation and definability of the syntactic forcing relation,The atomic membership truth lemma for forcing shows ${\nu }_{\sigma }^G=y$. One inclusion follows immediately from its soundness direction. For the other, if $a\in y\subseteq x$, choose $(\rho ,r)\in \tau$ with $r\in G$ and ${\rho }^G=a$. The truth direction supplies $p\in G$ forcing $\rho \in \sigma$; strengthen within $G$ below $p$ and $r$ to obtain an active pair in ${\nu }_{\sigma }$ representing $a$.

Finally the ground-model forcing nameexists by Axiom schema of replacement and the ground-model power set axiom. Since $G$ is nonempty, all $\nu \in B$ contribute their values, andThis set belongs to $M[G]$ by the definition of a generic extension. The construction uses all conditions in the outer pairs and therefore does not require a greatest condition in $\mathbb{P}$.

We prove mutual genericity for product forcing. Let $D\in M[G_0]$ be a dense subset of $\mathbb{Q}$, and take a forcing name $\dot{D}\in M$ evaluating to $D$. By the forcing theorem, some $p_0\in G_0$ forces that $\dot{D}$ is a dense subset of the canonical forcing name for $\mathbb{Q}$.

In $M$ defineThis set is dense in the product forcing order. Given $(p,q)$, the incompatible case is immediate. Otherwise first strengthen $p$ below $p_0$. The forced density assertion and the existential clause of syntactic forcing supply a further $r\le p,p_0$ and a ground-model $q^{\prime }\le q$ with $r⊩{\check{q}}^{\prime }\in \dot{D}$. To justify choosing a ground-model $q^{\prime }$, a name forced to lie in $\check{\mathbb{Q}}$ can densely be made equal to some ${\check{q}}^{\prime }$ by the atomic membership clause; strengthen to that equality and use the forced order comparison. Thus $(r,q^{\prime })\in E$ lies below $(p,q)$.

The generic filter $H$ meets $E$. It cannot meet the first part, because its first projection contains $p_0$ and is directed. Hence there is $(p,q)\in H$ with $p\in G_0$ and $p⊩\check{q}\in \dot{D}$. Soundness of the forcing theorem gives $q\in D$, and the projection gives $q\in G_1$. Since every such $D$ is met,This establishes the stronger property, rather than merely meeting dense ground-model subsets.

Suppose, towards a contradiction, that $G\in M$. Then $D=\mathbb{P}\setminus G$ is a ground-model set by axiom schema of separation. It is dense. If $p\notin G$, it already lies in $D$. If $p\in G$, atomless forcing order structure gives incompatible forcing conditions $q,r\le p$. Both cannot belong to the directed filter $G$, so at least one is a strengthening of $p$ in $D$.

All compatibility and extension quantifiers range over the same ground-model set $\mathbb{P}$, so this density argument is also valid internally in the transitive model $M$. Genericity requires $G\cap D\ne \varnothing$, contradicting the definition of $D$. Therefore a generic filter for an atomless order is new:The assumption is essential: a forcing atom determines a ground-model generic filter. For an atom $p$, the conditions compatible with $p$ form a generic filter $G_p\in M$: two such conditions have strengthenings below $p$, which have a common strengthening by the atom property; every dense set has a member below $p$. In a general partial order, $G_p$ need not be the principal filter above $p$.

Put $\kappa ={\aleph }_2^M$ and let $F=\bigcup G$. Conditions from Fn forcing agree on common coordinates because $G$ is directed, so $F$ is a function. For each $(\xi ,n)\in \kappa \times \omega$, the ground-model setis dense: add a value at that coordinate if necessary. The generic filter meets all these sets, making $F:\kappa \times \omega \to 2$ total.

For distinct $\xi ,\eta <\kappa$, the ground-model setis dense. Choose $n$ fresh for both rows of a finite condition and assign $0$ and $1$ there. Genericity therefore makes the rows pairwise different. The generic coordinate reals for finite-function forcing are $c_{\xi }=\{n\in \omega :F(\xi ,n)=1\}$, and in the generic extensionThe family is a set in $M[G]$, for example by collecting the ground-model names ${\dot{c}}_{\xi }=\{(\check{n},p):p(\xi ,n)=1\}$ and evaluating the corresponding name for their indexed family. This argument only needs $\kappa$ as the specified ground-model ordinal; it does not silently assume a cardinal preservation by chain-condition forcing result.