Proof review: content pages #410

Findings of an AI-assisted review of all proofs in content/ (29 pages with proofs; contribute, foundations, dual-properties, resources and relationships-epis-monos contain none). Each page was reviewed in a fresh context with the check-proofs skill. Line links point to commit 6caec6e.

Severity: major (demonstrated logical gap or error), minor (small gap or imprecision), uncertain (possible issue or missing context), note (no proof error, but something to fix or clarify, such as a deducible implication or an unused hypothesis). A few findings concern YAML files that cite a content page.

Only proofs that need attention are listed; files without findings are omitted. Fix the findings in small PRs that reference this issue, and tick the box of each fixed (or dismissed) finding.

content/constant_morphisms.md

• minor — Lemma 1, ::: Proof (content/constant_morphisms.md:13): the proof takes "constant map in the usual sense" to mean $f(x_1) = f(x_2)$ for all $x_1,x_2 \in X$, but never says so. Under that reading, the empty map $\varnothing \to \varnothing$ is constant. Some texts instead define a constant map as one that factors through a point, or require $X$ to be non-empty. Under those definitions $\varnothing \to \varnothing$ is a constant morphism but not a constant map, and the lemma fails. This matters downstream: database/data/morphisms/empty-map.yaml cites Lemma 1 with "The map is clearly constant". Stating which notion is meant would close this gap.

content/effective-congruence-quotients.md

• minor — page title and heading vs. Lemma statement (content/effective-congruence-quotients.md:2): the title says "Quotients of effective congruences are strict quotients", but the Lemma proves something different: an effective congruence is the kernel pair of its coequalizer. "Strict quotient" is neither defined nor proved here. In the usual sense (a strict epimorphism), every coequalizer is one trivially, so the title misdescribes the result that the linking pages (e.g. Set_c.yaml, FinGrp.yaml, subcategories.md) actually rely on.

content/Grp_total_explicit_proof.md

• major (confirmed by hand) — the claim that $h \mapsto e(Th(x))$ is a group homomorphism (content/Grp_total_explicit_proof.md:24, diagram at line 29 and line 34). The left vertical arrow of the diagram is labelled $T(hh')$, and the relation is applied to $y := T(hh')(x)$. But $T(hh') : TH \to T\mathbb{Z}$, so it cannot be a map $TH \to T(\mathbb{Z} * \mathbb{Z}')$, and $y$ is not an element of $T(\mathbb{Z} * \mathbb{Z}')$, which the relation needs. The argument needs the induced homomorphism $[h,h'] : \mathbb{Z} * \mathbb{Z}' \to H$ (with $1 \mapsto h$, $1' \mapsto h'$). That map is never introduced. Its three identities $[h,h'] \circ \mu = hh'$, $[h,h'] \circ i_1 = h$ and $[h,h'] \circ i_2 = h'$ are what make the three squares commute. With the left arrow $T[h,h']$ and $y := T[h,h'](x)$ the step works. As written, the central computation does not typecheck.
• minor — the existence step (content/Grp_total_explicit_proof.md:50). $U$ is never defined (presumably the forgetful functor $\mathbf{Grp} \to \mathbf{Set}$). The bijection $\mathrm{Hom}(\mathbb{Z} * \mathbb{Z}', G) \cong UG \times UG$ is not specified either, but the identification of the right-hand vertical maps as multiplication and the two projections depends on it: evaluation at $1$ and $1'$. The reader has to reconstruct this to verify the claim at line 56.

content/coslice-effective-congruences.md

• minor — Lemma, ::: Proof, last step (content/coslice-effective-congruences.md:23): "using disjoint coproducts, we may conclude that $x_1, x_2$ factor through $E$" leaves out what this step needs. Let $u : A+T \to A+E$ be the induced map. Disjointness alone does not give a factorization of $u \circ i_2 : T \to A+E$ through $i_2 : E \to A+E$. One also needs:
  • pullback stability, to split $T = T_A + T_E$ along $u \circ i_2$;
  • disjointness together with strictness of the initial object (which holds in extensive categories), to show $T_A \cong 0$, since $T_A$ maps into $A \times_{A+X} X$;
  • monicity of $i_2 : X \to A+X$, to get $f \circ v = x_1$ and $g \circ v = x_2$ from $i_2 \circ f \circ v = i_2 \circ x_1$.
• minor — Lemma, ::: Proof, congruence verification (content/coslice-effective-congruences.md:17): "without loss of generality we may assume each comes from either $A$ or $E$" hides the actual case analysis, so the proof is a sketch rather than complete.
  • Splitting $T$ along two generalized elements $u, v : T \to A+E$ gives four pieces. The proof never says why the mixed pieces (e.g. $u$ landing in $A$ and $v$ in $E$) are harmless. They are initial: they map into $A \times_{A+X} X = 0$, and the initial object is strict. This is the only point where disjointness enters this part.
  • The proof also does not say whether the generalized elements are taken in $\mathcal{C}$ or in $A \backslash \mathcal{C}$. The congruence has to live in $A \backslash \mathcal{C}$. The conditions do transfer from $\mathcal{C}$: for example, a reflexivity witness obtained in $\mathcal{C}$ is automatically a map under $A$, by joint monicity. This transfer is not mentioned.
  • For transitivity, the splitting relies on the pieces being reassembled into a single witness via the coproduct universal property, which is not mentioned.

content/cocongruences_of_groups.md

• minor — Proposition 2, ::: Proof (content/cocongruences_of_groups.md:53): The proof starts from "coreflexive" and "cotransitive" (a retraction $r$ and a morphism $c : Y \to Y \sqcup_{i_2,X,i_1} Y$). CatDat defines a cocongruence differently (see database/data/category-properties/coquotients of cocongruences.yaml): it is jointly epimorphic, and the image of $\mathrm{Hom}(Y,T) \to \mathrm{Hom}(X,T)^2$ is an equivalence relation for every $T$. The proof never connects the two. The step is routine: reflexivity at $T = X$ gives $r$, and transitivity at $T = Y \sqcup_{i_2,X,i_1} Y$, applied to $(u_1 i_1, u_1 i_2)$ and $(u_2 i_1, u_2 i_2)$, gives $c$. It also needs this pushout to exist, which holds because $i_1, i_2$ are monomorphisms. Still, a reader who knows only the linked definition has to supply it.
• minor — Corollary 3 (content/cocongruences_of_groups.md:105): The corollary has no proof and does not say how Propositions 1 and 2 apply. Proposition 2 also needs $\mathbf{Grp}$ to be balanced and to have equalizers of monomorphisms. Neither fact is stated or linked here. Balancedness is not trivial, since it rests on epimorphisms of groups being surjective. Both facts are available in CatDat: balancedness follows from mono-regular in database/data/categories/Grp.yaml, and equalizers follow from finitary algebraicity.

content/Top-embeds-in-LRS.md

• minor — Corollary 3, ::: Proof block (content/Top-embeds-in-LRS.md:45): the proof asserts two things without argument or citation, and both carry the proof. First, that $\mathrm{Spec} k$ is subterminal in $\mathbf{LRS}_R$. Second, that $\mathbf{LRS}_k$ is equivalent to the slice $\mathbf{LRS}_R / \mathrm{Spec} k$. Both need the identification of morphisms $X \to \mathrm{Spec} k$ in $\mathbf{LRS}_R$ with $R$-algebra maps $k \to \mathcal{O}_X(X)$ (the $\mathrm{Spec} \dashv \Gamma$ adjunction for locally ringed spaces). There is also a more elementary route: $R \to k$ is surjective, so a $k$-algebra structure on $\mathcal{O}_X$ is unique if it exists, and $R$-linear morphisms between such objects are automatically $k$-linear. The intended reader is not assumed to know this algebraic geometry background, and the proof gives neither the argument nor a reference. Fully faithfulness, the right adjoint ${-} \times \mathrm{Spec} k$, and preservation of inhabited limits all depend on this equivalence.

content/congruences_in_rel.md

• minor — Claim 6, the bijection $E \to E'$ (content/congruences_in_rel.md:75): the proof calls the map a bijection but never shows it. Three things are left out:
  • The case split covers every element only because of Claim 4.
  • Injectivity uses the injectivity of $i_{\ast}$ on singletons.
  • Surjectivity needs every point of $E'$ to be hit. For $x \notin A$, Claim 3 makes $r_{\ast}(\{x\})$ a pair, so Claim 2 gives elements with images $(\{x\},\varnothing)$ and $(\varnothing,\{x\})$. For $x \in A$, the contrapositive of the pair case of Claim 2 makes $r_{\ast}(\{x\})$ a singleton with image $(\{x\},\{x\})$.
• minor — Claims 2 and 4, the symmetry step (content/congruences_in_rel.md:36, content/congruences_in_rel.md:53): the equations $i_{\ast}(s_{\ast}(\{e\})) = i_{\ast}(\{f\})$ and $i_{\ast}(\{s_0(e)\}) = (T,S)$ rest on $i \circ s = \tau \circ i$, where $\tau$ is the swap on $X \times X$. This identity is never stated: the text only mentions $s^2 = \mathrm{id}$ at line 17. Claim 4's whole argument depends on this compatibility, so it should be stated rather than left implicit.
• minor — Lemma, the statement (content/congruences_in_rel.md:84): the statement says only that $s$ and $t$ are "maps in the reverse direction". It never gives the equations they satisfy ($e s = \mathrm{id}$, $f t = \mathrm{id}$, $g t = s e$). The proof relies on $f t = \mathrm{id}$ and $g t = s e$ (content/congruences_in_rel.md:99), so the hypotheses are not actually specified. The proof also leaves out that the factorization through $E$ is unique. This is routine, since $(f,g)$ is jointly monic.

content/comphaus_copresentable.md

• minor — Proposition 4, ::: Proof, injectivity part (content/comphaus_copresentable.md:80): the proof applies Lemma 1 but never states the diagram it applies it to. That diagram sends each $(f : j \to i) \in \mathcal{I}/i$ to $X_f^{-1}(\{x\}) \subseteq X_j$, with transition maps given by restricting the $X_g$. Two facts are needed and not stated. First, this assignment really is a functor on $\mathcal{I}/i$: if $f \circ g = f'$, then $X_g$ maps $X_{f'}^{-1}(\{x\})$ into $X_f^{-1}(\{x\})$. Second, its limit, taken inside $\lim_{\mathcal{I}/i} X \cong X$, equals $p_i^{-1}(\{x\})$. The phrase "the limit $p_i^{-1}(\{x\})$" assumes both. They are easy to check, but they carry the contradiction, and the rest of the proof is explicit.
• minor — Corollary 5, ::: Proof (content/comphaus_copresentable.md:93): "It suffices to show that the monad … is $\aleph_1$-accessible" relies on a theorem that is neither proved nor cited. The theorem says that the category of algebras for a monad on $\mathbf{Set}$ that preserves $\aleph_1$-filtered colimits is locally $\aleph_1$-presentable (e.g. Adámek–Rosický, Rem. 2.78). It goes beyond the basic category theory the intended reader is assumed to know, and without it the reduction is unsupported.

content/missing_cogenerating_collections.md

• minor — Lemma, ::: Proof block (content/missing_cogenerating_collections.md:18): the proof needs a single cardinal that bounds all $\mathrm{card}(U(Y))$ with $Y \in S$, and it does not say why one exists. In CatDat a cogenerating collection only has to be essentially small (see database/data/category-properties/cogenerating collection.yaml), not a set. The missing step is short: isomorphic objects have underlying sets of the same size because $U$ is a functor, so $\{\mathrm{card}(U(Y)) : Y \in S\}$ is a set. Choose an infinite $\kappa$ strictly above its supremum and apply (2). Without this step, "larger than all the $U(Y)$" is not justified when $S$ is a proper class.
• note — Lemma, hypotheses (content/missing_cogenerating_collections.md:9): The proof never uses that $U$ is faithful. Either drop this hypothesis or explain why it is needed.

content/preadditive_structure_unique.md

• minor — Lemma statement (content/preadditive_structure_unique.md:13): the inverse is written as $\alpha^{-1} : B \oplus B \to B \times B$. Since $\alpha : B \oplus B \to B \times B$, the inverse must go $B \times B \to B \oplus B$. Only that direction lets the composite $\nabla \circ \alpha^{-1} \circ (f,g)$ typecheck, and the proof uses it that way ($\nabla \circ \beta \circ (f,g)$).
• minor — Lemma hypotheses compared with the page description and the incoming link (content/preadditive_structure_unique.md:3, content/preadditive_structure_unique.md:9): the front-matter description, and the link from database/data/category-properties/additive.yaml, say uniqueness holds "in the presence of finite products". The lemma, however, assumes finite products and finite coproducts, and the proof needs the coproduct $B \oplus B$ and $\nabla$. The page never shows that finite products in a category enriched in commutative monoids are also coproducts (the biproduct argument). So the claim as advertised and linked is not quite what is proved.

content/infinite-products-coproducts-additive-categories.md

• minor — front-matter description (content/infinite-products-coproducts-additive-categories.md:3): it says that an infinite coproduct of copies of a non-zero object "cannot be isomorphic to the corresponding infinite product". The Proposition only shows that the canonical morphism $\alpha$ is not an isomorphism, and only for countable index sets. Read literally, the description is false. For example, in $\mathbf{Ab}$, let $A$ be a $\mathcal{Q}$-vector space of dimension $2^{\aleph_0}$. Then $\bigoplus_{n \geq 1} A$ and $\prod_{n \geq 1} A$ both have dimension $2^{\aleph_0}$, so they are abstractly isomorphic even though $A \neq 0$. A reader taking the summary at face value would get a wrong statement.

content/thin_extremal_generator.md

• minor — Corollary, ::: Proof block (content/thin_extremal_generator.md:25): The proof only translates "every morphism with codomain $X$ is an isomorphism" into "$X$ is minimal". It leaves out the remaining steps the Corollary asserts:
  • In a poset, $X \cong G$ means $X = G$, so the Lemma becomes "every element other than $G$ is minimal".
  • The existence of some such $G$ is equivalent to $P$ being non-empty with at most one non-minimal element. Non-emptiness is needed because a generator must exist as an object.
  • The "in particular" claims are not argued. One is that a poset in which every element is minimal is exactly a discrete poset. The other is that if there is a non-minimal element $m$, then any extremal generator must be $m$, so it is unique.

content/thin_algebraic_categories.md

• note — front matter, description (content/thin_algebraic_categories.md:3): The description says that the only thin algebraic categories are $1$ and the interval category, which suggests both directions. The Lemma only proves that every thin algebraic category is one of the two. That both are algebraic is not shown (for example, $I$ is the category of models of the theory with no operations and the axiom $x = y$). Either add this or rephrase the description.

content/generator_construction.md

• minor — Lemma, ::: Proof block, preliminary remark (content/generator_construction.md:13). The proof says that strong connectedness "implies that each coprojection $i_G : G \to U$ has a left inverse", and later that "any morphism $G \to A$ extends to $U$". Neither statement is justified, yet both carry the whole argument. The missing step is to build the retraction $r_G : U \to G$ from the universal property. Its component at $G$ is $\mathrm{id}_G$, and its component at each $G' \neq G$ is a chosen morphism $G' \to G$; this is exactly where strong connectedness is used. A morphism $a : G \to A$ then extends as $\bar a := a \circ r_G$, since $a \circ r_G \circ i_G = a$. This step is routine, but it is the heart of the lemma and needs one sentence. The extension is used again in the second paragraph for $b$.

content/sifted-colimits-in-groupoids.md

• minor — Corollary 2, ::: Proof (content/sifted-colimits-in-groupoids.md:63): the proof starts with "Let $D : \mathcal{I} \to \mathcal{C}$ be a diagram" but never says the diagram is sifted. Siftedness is needed for two things. It is what lets us choose $i_0$ with $D$ constant after $i_0$ (the hypothesis covers only sifted diagrams). It is also what allows Lemma 1 to be applied to both $D$ and $\mathrm{Hom}(X,D(-))$. The proof also does not say why $\mathrm{Hom}(X,D(-))$ is again constant after $i_0$ (because $\mathrm{Hom}(X,-)$ preserves isomorphisms), which Lemma 1 needs when applied in $\mathbf{Set}$.
• minor — Corollary 3, ::: Proof (content/sifted-colimits-in-groupoids.md:81): "follows directly from Lemma 1 and Corollary 2" leaves out one condition of the definition of a generalized variety. The definition asks for an essentially small collection $G$ of strongly finitely presentable objects such that every object is a sifted colimit of objects from $G$. The proof never names $G$ (all objects, which form an essentially small collection by assumption). It also never says that every object is a sifted colimit of objects from $G$ (trivially, as the colimit of itself over the terminal category, which is sifted). Without these, the proof does not visibly cover that condition.
• minor — Corollary 4, ::: Proof (content/sifted-colimits-in-groupoids.md:90): the same omission for finitely accessible. The proof shows that filtered colimits exist and that every object is finitely presentable. It does not name the essentially small collection $G$, and it does not say that every object is a filtered colimit of objects from $G$ (for example over the terminal category, which is filtered). Both are needed for the definition.

content/topos-with-generator.md

• minor — Lemma, ::: Proof block, second paragraph (content/topos-with-generator.md:15): the proof says the equalizer of $i_1, i_2 : 1 \rightrightarrows 1 +_P 1$ is $P$ "by coregularity". Coregularity only guarantees that this cokernel pair and its equalizer exist. That the equalizer is $P$ follows from a different fact, which the proof never states: a regular monomorphism is the equalizer of its cokernel pair. This is also the only place where the proof uses that $P \to 1$ is regular. As written, the step names a reason that does not by itself give the conclusion.

content/inclusion-functors.md

• major (confirmed by hand) — Euclid_coprod, kernel pairs proof, outside this file (database/data/categories/Euclid_coprod.yaml:112): The proof says Lemma 1 shows that $\mathbf{Euclid}_{\sqcup} \hookrightarrow \mathbf{Met}_c$ preserves finite limits, because $\mathbf{Euclid}_{\sqcup}$ contains the extremal cogenerator $\mathbb{R}$. But Lemma 1 with an extremal cogenerating collection only gives preservation of colimits. Limits would need the dual of Lemma 1, which requires $\mathbf{Euclid}_{\sqcup}$ to contain an extremal generating collection of $\mathbf{Met}_c$. The extremal generator recorded for $\mathbf{Met}_c$ is $\{1/n\} \cup \{0\}$, and it is not in $\mathbf{Euclid}_{\sqcup}$. So the cited lemma does not support the first step, which reduces "has kernel pairs" to "closed under kernel pairs in $\mathbf{Top}$". The Met_c_cogenerator reference does not fill this gap.
• minor (confirmed by hand) — Quiv_fc, alternative argument for limit preservation, outside this file (database/data/categories/Quiv_fc.yaml:92): The proof cites "Lemma 1" with an extremal generating set to get preservation of limits. That needs the dual of Lemma 1. The main argument in the same proof (representability) is correct, so only the stated alternative is affected.

content/functors_on_discrete_categories.md

• minor — Lemma 2, definition of subterminal in the statement (content/functors_on_discrete_categories.md:21), and the dual definition of co-subterminal in the remark (content/functors_on_discrete_categories.md:30): the text says "every two morphisms with codomain $F(s)$ are equal" (dually "any two morphisms with domain $X$"). Read literally, this compares morphisms with different domains, so it can never hold, and no object would be subterminal. The intended condition is that any two parallel morphisms $f,g : A \rightrightarrows F(s)$ are equal. The proof uses only this parallel version, and it is also the version that matches the "$X \times X$ with the diagonal an isomorphism" characterization in the proof. So the argument is fine, but the definition as stated is wrong.

content/nice-and-small-presheaves.md

• minor — Lemma 1, ::: Proof, direction small ⟹ nice (content/nice-and-small-presheaves.md:37). The proof says nice presheaves are "clearly closed under colimits of presheaves". As written this is false for large colimits: every presheaf is a large colimit of representables, and the coproduct of $\mathrm{Hom}(-,X)$ over all sets $X$ is not nice. The argument only works for small colimits, and the deciding step is left out. For a small diagram $(F_i)$, the union $\bigcup_i S_{F_i}$ is a set because the index category is small, and it is an exceptional set for the colimit. That step is where smallness enters, which is the whole point of the lemma. Neither the restriction to small colimits nor the choice of exceptional set is stated.
• minor — Lemma 1, ::: Proof, direction nice ⟹ small (content/nice-and-small-presheaves.md:39). The proof uses, without citing it, that a presheaf is small if and only if its category of elements has an essentially small final subcategory. The page instead defines small presheaves through the nLab link (small colimits of representables). The equivalence is item 4 in the characterization in content/free-cocompletion.md, but that page is never linked here, so a reader cannot get from the stated criterion to the definition from this page and its links alone.
• minor — Lemma 1, ::: Proof, zigzag step (content/nice-and-small-presheaves.md:63). The intermediate morphisms $(X,x) \to (A,a_i)$ and $(X,x) \to (B,b_i)$ are only objects of $(X,x) \downarrow \mathcal{D}$ if $u_X^{\ast}(a_i) = x$ and $v_X^{\ast}(b_i) = x$. Both hold, because $u_X^{\ast}$ coequalizes $f^{\ast}$ and $g^{\ast}$ and $v_X^{\ast} = u_X^{\ast} \circ f^{\ast}$, but the proof does not state or check this.

content/natural_numbers_objects.md

• minor — Lemma 1, ::: Proof (content/natural_numbers_objects.md:37). The proof shows that $\Phi := \Psi_1$ exists, then calls it "the unique morphism" without an argument. Uniqueness needs one more step. If $\Phi'$ satisfies $\Phi'(z)=a$ and $\Phi'(s(n)) = g(n,\Phi'(n))$, then $(\mathrm{id}_N,\Phi')$ satisfies the two defining equations of $\Psi$, so $(\mathrm{id}_N,\Phi') = \Psi$ and hence $\Phi' = \Psi_1$. This half of the lemma's claim is currently not shown. Lemma 2 relies on it for the uniqueness of $c$.
• minor — Lemma 5, ::: Proof (content/natural_numbers_objects.md:138). The proof says that $f \circ F(x_0) = y_0$ corresponds to $\widetilde{f} \circ x_0 = G(y_0)$, but this does not type-check as written. $G(y_0)$ has domain $G(1_{\mathcal{D}})$, not $1_{\mathcal{C}}$, so the correct condition is $\widetilde{f} \circ x_0 = G(y_0) \circ \eta_{1_{\mathcal{C}}}$, using the isomorphism $\eta_{1_{\mathcal{C}}} : 1_{\mathcal{C}} \to GF(1_{\mathcal{C}}) = G(1_{\mathcal{D}})$. The correspondence itself also needs justification, which the proof omits: it uses naturality of the adjunction bijection in $X$, and naturality in $Y$ for the condition involving $s$. Line 123 does set the convention $1_{\mathcal{D}} \cong H(1_{\mathcal{C}})$ for $R(G)$, so this is a gap in rigor rather than an error. Still, it is the central step of the proof.

content/pushouts-of-monos-via-congruence-quotients.md

• minor — Lemma, ::: Proof block (content/pushouts-of-monos-via-congruence-quotients.md:13): The proof reduces joint monicity and transitivity to generalized elements that factor through single summands, then stops without doing the case analysis. The cases need facts the proof never names:
  • Mixed cases, such as $i_1 \circ x = i_2 \circ g \circ s$, are impossible except on an initial piece. This needs disjoint coproducts and a strict initial object; the extensive property's description does not state strictness.
  • Same-summand cases, and the transitivity case that combines the two copies of $S$ (where $g \circ s = g \circ s'$ forces $a = c$), need $f$, $g$ and the coproduct inclusions to be monomorphisms.
  • The reduction step uses that the restrictions to the pieces of a coproduct decomposition of $T$ determine a map out of $T$, and that witnesses on the pieces can be glued.
• minor — Lemma, ::: Proof block, last sentence (content/pushouts-of-monos-via-congruence-quotients.md:13): "Now a quotient of the congruence must be a pushout of $f$ and $g$" is stated without justification. The missing step is short: a morphism $h : X+Y \to Z$ satisfies $h \circ p_1 = h \circ p_2$ if and only if $h \circ i_1 \circ f = h \circ i_2 \circ g$. The pairs $u : X \to Z$, $v : Y \to Z$ with $u \circ f = v \circ g$ then correspond to such $h = [u, v]$. Since this is the step that delivers the lemma's conclusion, it should be spelled out.

content/missing_cogenerator.md

• minor — Lemma, ::: Proof, hypercocompleteness part (content/missing_cogenerator.md:21): The proof says the cocones $\mathcal{F} \to Y$ form an essentially small collection. This needs each $\mathrm{Hom}(X, Y)$ to be a set, and the Lemma does not assume $\mathcal{C}$ is locally small. Faithfulness of $U$ does give this, because $\mathrm{Hom}(X,Y)$ injects into $\mathrm{Hom}(U(X),U(Y))$. However, this is the only place the faithfulness hypothesis is used, and the proof never says so. The step also needs the remaining $X \in \mathcal{F}$ with $\mathrm{card}(U(X)) \le \mathrm{card}(U(Y))$ to form a set, which holds because there is at most one per cardinal. This is also left unstated.
• minor — Lemma, ::: Proof, reduction step (content/missing_cogenerator.md:21): "We may assume that for each small cardinal $\kappa$ there is at most one element $X \in \mathcal{F}$ with $\mathrm{card}(U(X)) = \kappa$" replaces $\mathcal{F}$ with a subcollection, and the reduced $\mathcal{F}$ must still satisfy assumption (2). It does if we keep exactly one representative for each cardinal that occurs, but the proof does not say this. Also, each fibre $\{X \in \mathcal{F} : \mathrm{card}(U(X)) = \kappa\}$ may be a proper class. Choosing from proper classes needs global choice (or a universe setting), not just the axiom of choice for sets.
• minor — Lemma, ::: Proof, cototal implies hypercocomplete (content/missing_cogenerator.md:23): According to database/data/category-properties/total.yaml, Kelly's Thm. 5.6 proves that total categories are hypercomplete. The statement needed here is the dual of that theorem, and the proof cites Thm. 5.6 directly without saying "the dual of". I could not check the external paper itself.

content/monic_sequential_colimits.md

• major (incompleteness, not an error) — Lemma 1, ::: Proof (content/monic_sequential_colimits.md:13): the proof claims that $\coprod E_{m,n} \rightrightarrows Y$ is a congruence, and says only that extensivity lets each generalized element be assumed to factor through one coproduct inclusion. The checks themselves are missing, and they are where the hypotheses do their work.
  • Joint monicity needs the inclusions to be disjoint, the initial object to be strict (for the pieces where the indices differ), and the $f_{m,n}$ to be monic.
  • Transitivity needs a case analysis on the order of $m, n, k$. For example, when $m \le k < n$, building the element of $E_{m,k}$ relies on $f_{k,n}$ being monic.
  • Reflexivity and symmetry are not mentioned. Reflexivity also needs the domain to be split, here along a generalized element of $Y$ rather than of $\coprod E_{m,n}$.
  • The pieces then have to be glued back together along $T \cong \coprod T_i$, which is also not mentioned.
• minor — Lemma 1, ::: Proof (content/monic_sequential_colimits.md:13): the last sentence, "a quotient of this congruence must be a colimit of the sequence", is stated without argument. The missing step is short. A morphism $h : Y \to T$ coequalizes the pair if and only if $h_m = h_n \circ f_{m,n}$ for all $m \le n$ (the case $m \ge n$ is symmetric), so the coequalizer represents cocones. This is the actual conclusion of the lemma, so the step should be written out, as is done in Lemma 2.
• minor — Lemma 2, ::: Proof (content/monic_sequential_colimits.md:24): the proof cites countable extensivity for the isomorphism $\coprod_{n,m} X_n \times_Y X_m \cong \coprod_n X_n \times_Y \coprod_m X_m$, but it never shows that the pullbacks $X_n \times_Y X_m$ exist. The category is only assumed to have pullbacks along coproduct inclusions. They do exist: pull the kernel pair back along the coproduct inclusions in each factor and use pasting of pullbacks. The step at line 35 also covers it once $n \le m$. Still, the order of the argument currently takes their existence for granted.

content/free-cocompletion.md

• minor — Proposition 12, ::: Proof (content/free-cocompletion.md:186): The proof says $f$ and $f'$ are connected in $(X,x) \downarrow \mathcal{K}$. For that, $f' : (X,x) \to (A,b)$ must be an object of that comma category, which requires $(A,b)$ to be an object of $\mathcal{K}$. Only $A \in K$ is known, and $\mathcal{K}$ is an arbitrary final subcategory, so it need not contain $(A,b)$. As written, the zigzag starting at $f$ and ending at $f'$ need not exist. There are two fixes. One is to compose $f'$ with a morphism $(A,b) \to (B,c)$ in $\mathcal{K}$, which exists by finality; then $c \in F_2(B) \setminus E(B)$, because otherwise $b$ would lie in $F_1$, and the induction runs as before. The other is to replace $\mathcal{K}$ by the full subcategory of $\int P$ on all $(A,c)$ with $A \in K$, which is still final. A related point at line 178: $K$ must be chosen small (for example by taking representatives of $\mathcal{K}$) so that the coproduct $\coprod_{A \in K, a \in E(A)} \mathrm{Hom}(-,A)$ is a small coproduct. Also, the source of the final subcategory is not stated: condition (4), via the nLab, gives a final functor from a small category, not a final subcategory.
• minor — Proposition 12, ::: Proof (content/free-cocompletion.md:172): The proof says a cocongruence in $\widehat{\mathcal{C}}$ "is the same as" a cocongruence of presheaves because the inclusion preserves finite colimits. The definition of a cocongruence quantifies over all test objects $T$ in the category and requires joint epimorphicity. So the argument also needs two things. First, the coreflexivity, cosymmetry and cotransitivity maps are obtained in $\widehat{\mathcal{C}}$ (testing with $T = F$, $T = G$, $T = G \sqcup_F G$, which are all small) and then work for all presheaves. Second, joint epimorphicity becomes objectwise by Lemma 5. Neither is stated.
• minor — Lemma 9, ::: Proof (content/free-cocompletion.md:113): "finite colimits are objectwise" does not cover everything needed. The corelation $X \sqcup X \twoheadrightarrow R$ is an epimorphism in $\widehat{\mathcal{C}}$, and it is objectwise surjective only by Lemma 5. Also, the cosymmetry and cotransitivity maps obtained objectwise in $\mathbf{Set}$ must be shown to be natural. This follows from their uniqueness, since the corelation is jointly epic, but the proof does not say it.

content/subcategories.md

• minor (step confirmed by hand) — Lemma 1, ::: Proof (content/subcategories.md:16): The last isomorphism $\mathrm{Sub}(U(X)) \cong \mathrm{Sub}(X)$ is asserted without proof. The obvious map $[m] \mapsto [U(m)]$ only makes sense if $U$ preserves (regular) monomorphisms. Neither the stated hypotheses nor the proof gives this, and it is not automatic for a fully faithful left adjoint. For example, in the coreflective subcategory of perfect groups in $\mathbf{Grp}$, the map $\mathrm{SL}(2,5) \to A_5$ is a monomorphism, but not in $\mathbf{Grp}$. Hypothesis (2) only gives surjectivity, and full faithfulness gives injectivity once the map exists. The bijection must also be natural in $X$ for $\mathrm{Hom}({-},R(\Omega)) \cong \mathrm{Sub}$ to make $R(\Omega)$ a classifier. That needs $U$ to preserve pullbacks of monomorphisms, which is not addressed either. I could not decide whether the lemma stays true without an added hypothesis such as "$U$ preserves (regular) monomorphisms". Either way, the step needs an argument or a stronger hypothesis. (Lemma 1 is cited in Alg(R).yaml, Mon.yaml and Rng.yaml.)
• minor — Lemma 1, ::: Proof (content/subcategories.md:15): By CatDat's definition, a (regular) subobject classifier requires $\mathcal{C}$ to be finitely complete, and the proof never shows this. It does follow, since finite limits in $\mathcal{C}$ can be computed as $R(\lim U(X_i))$ in the finitely complete $\mathcal{D}$. But this step is skipped.
• minor — Lemma 5, ::: Proof (content/subcategories.md:67): Cartesian closed requires all finite products, including a terminal object, but the lemma only assumes binary products in $\mathcal{C}$. The proof only builds exponentials. The terminal object exists as $R(1)$, because $\mathrm{Hom}_\mathcal{C}(X, R(1)) \cong \mathrm{Hom}_\mathcal{D}(UX, 1)$, but the proof does not say so. This matters for Corollary 6 only formally, since there $\mathrm{id}_P$ is terminal.
• minor — Lemma 3, ::: Proof (content/subcategories.md:41): By the definition of exact filtered colimits, the canonical comparison morphism $\mathrm{colim}_j \lim_i X(i,j) \to \lim_i \mathrm{colim}_j X(i,j)$ must be an isomorphism. The proof only gives a chain of isomorphisms and never checks that their composite is this canonical morphism. The check is routine but missing. Compare Lemma 4, which explicitly identifies $Uc$ with the comparison map.