Coherent category¶

Equip a regular category with finite unions of subobjects that remain stable under pullback, providing categorical semantics for finite-limit, existential, and finite-disjunctive reasoning.

Version: v3 · 2026-09-19 · History
Domain-specific #: 1493
Domain group: Formal Sciences
Origin domain: Mathematics
Subdomains: Category Theory, Categorical Logic and Topos Theory → Mathematics

Core Idea¶

A coherent category is a regular category \(\mathcal C\) in which each subobject poset (Sub(X)) has finite joins and every inverse-image map \(f^*:Sub(Y)\to Sub(X)\) preserves those joins.^[1] Finite limits interpret conjunction and equality, regular images interpret existential quantification, and pullback-stable finite joins interpret disjunction; preservation makes these logical operations compatible with substitution along morphisms.

Its autonomous residual is the conjunction of regular categorical structure with pullback-stable finite subobject unions, and its role as semantics for coherent logic, not generic consistency, categorical coherence diagrams, or coherence of sheaves. The identity fails when the category lacks finite limits or stable images, subobject joins exist but are not pullback-stable, only binary coproducts of objects are available, a functor preserves limits but not finite subobject unions, or coherence is used only in its ordinary-language sense.

Recognition requires an analyst to verify finite limits, construct and test pullback-stable regular epi–mono image factorizations, form finite joins in each subobject poset, test their stability under inverse image, distinguish chosen representatives from subobject equivalence classes, and check that any claimed coherent functor preserves the required structure. Once established, it supports giving semantics to coherent first-order theories, constructing classifying categories and toposes, comparing logical theories through functors, using subobject lattices as internal predicates, and proving completeness or conservativity results without turning those uses into the definition.

How would you explain it like I'm…

No faithful explanation at this level. A child-level picture can only lean on the everyday sense of "coherent" or on "a world with and, or, there is", both of which drop the defining regular structure with pullback-stable finite subobject unions and invite the ordinary-language misreading the concept excludes.

Where Or Keeps Working

Category theory is a part of math that studies objects and the arrows between them, a bit like a map of places and roads. In a coherent category, you can talk about the parts of each object and combine them using logic words: AND (the overlap of two parts), OR (putting two parts together), and 'THERE IS SOME'. The special rule is that when you follow an arrow backward from one object to another, these combinations are carried along correctly: the OR of two parts goes to the OR of the carried parts. That makes a coherent category a place where a certain kind of logic works properly.

Regular Category with Stable Unions

A coherent category is a kind of category designed to interpret a fragment of logic called coherent logic, which uses 'and', 'or', 'there exists', 'true', 'false', and equality. It starts from a regular category, which has finite limits (used for 'and' and equality) and well-behaved images (used for 'there exists'). A coherent category additionally requires that for each object, its subobjects (its 'parts') have finite unions, or joins, and that these unions are preserved when you pull parts back along any arrow. That preservation makes 'or' behave correctly under substitution, just as it does in ordinary logic. The name refers to coherent logic, not to everyday 'coherence' or to other mathematical uses like coherent sheaves.

A coherent category is a regular category in which each subobject poset Sub(X) has finite joins and every inverse-image map f*: Sub(Y) to Sub(X) preserves them. In the logical reading, finite limits interpret conjunction and equality, pullback-stable regular images (from regular epi-mono factorizations) interpret existential quantification, and pullback-stable finite joins interpret disjunction, including the empty join as falsity. Preservation by inverse image makes these operations compatible with substitution along morphisms. The concept fails when finite limits or stable images are missing, when subobject joins exist but are not pullback-stable, when only binary coproducts of objects are available, or when 'coherence' is meant in its everyday sense or in the unrelated senses of coherence diagrams or coherent sheaves. Verifying the structure requires checking finite limits, stable image factorizations, finite subobject joins, their stability under inverse image, and care with subobjects as equivalence classes rather than chosen representatives. Coherent categories provide semantics for coherent first-order theories, support classifying categories and toposes, and underpin completeness and conservativity results.

Structural Signature¶

Carrier: a category with finite limits, regular image factorizations, and a subobject poset for every object
Inputs or antecedent state: finite limits, regular epimorphism–monomorphism factorizations stable under pullback, subobjects and their pullback maps, finite joins of subobjects, and a declared size context
Constitutive operation: Finite limits interpret conjunction and equality, regular images interpret existential quantification, and pullback-stable finite joins interpret disjunction; preservation makes these logical operations compatible with substitution along morphisms
Invariant: regular-category structure is present and finite unions of subobjects exist and are stable under pullback, equivalently the subobject inverse-image maps preserve finite joins under the adopted convention
Recognition test: verify finite limits, construct and test pullback-stable regular epi–mono image factorizations, form finite joins in each subobject poset, test their stability under inverse image, distinguish chosen representatives from subobject equivalence classes, and check that any claimed coherent functor preserves the required structure
Output or consequence: giving semantics to coherent first-order theories, constructing classifying categories and toposes, comparing logical theories through functors, using subobject lattices as internal predicates, and proving completeness or conservativity results
Failure boundary: the category lacks finite limits or stable images, subobject joins exist but are not pullback-stable, only binary coproducts of objects are available, a functor preserves limits but not finite subobject unions, or coherence is used only in its ordinary-language sense

What It Is Not¶

It is not the whole field of category theory; many objects in that field do not satisfy its constitutive rule.
It is not its canonical example. For a coherent first-order theory, its syntactic category has formulas-in-context as objects and provably functional relations as arrows, with conjunction, existential quantification and finite disjunction represented by the coherent categorical operations is an instance, not a definition.
It is not Regular category. Every coherent category is regular, but regularity alone supplies stable finite limits and images without requiring pullback-stable finite unions of subobjects. A Heyting category adds right adjoints to inverse-image maps, supporting implication and universal quantification beyond coherent logic.
It is not an unrestricted metaphor. Equivalent definitions package effective or regular epimorphisms differently, and size assumptions matter for model categories; an axiom list should be compared at the level of derived regular structure rather than by counting superficially different clauses

Scope of Application¶

Coherent category applies when the analyst can specify a category with finite limits, regular image factorizations, and a subobject poset for every object and establish that regular-category structure is present and finite unions of subobjects exist and are stable under pullback, equivalently the subobject inverse-image maps preserve finite joins under the adopted convention. The entry uses the standard categorical-logic definition. It does not assert that every functor category built from a coherent category is coherent without additional hypotheses, and all size and exactness assumptions must remain visible.^[2]

Recognition. verify finite limits, construct and test pullback-stable regular epi–mono image factorizations, form finite joins in each subobject poset, test their stability under inverse image, distinguish chosen representatives from subobject equivalence classes, and check that any claimed coherent functor preserves the required structure
Comparison. Compare legitimate instances through finite-limit structure, image factorization, regular-epimorphism convention, subobject posets, bottom subobject, binary and finite joins, pullback stability, functor preservation, category size, exactness strength, and internal logic fragment.
Boundary. Equivalent definitions package effective or regular epimorphisms differently, and size assumptions matter for model categories; an axiom list should be compared at the level of derived regular structure rather than by counting superficially different clauses
Use. Preserve every assumption when using the identity for giving semantics to coherent first-order theories, constructing classifying categories and toposes, comparing logical theories through functors, using subobject lattices as internal predicates, and proving completeness or conservativity results.

Clarity¶

A clear claim names the carrier, governing rule, assumptions, and recognition test. This matters because coherent describes proof systems, sheaves, rings, configurations and ordinary consistency, while category-theory coherence theorems concern commuting diagrams rather than coherent categories. The disciplined statement is that the object counts as Coherent category exactly when regular-category structure is present and finite unions of subobjects exist and are stable under pullback, equivalently the subobject inverse-image maps preserve finite joins under the adopted convention

Identity and measurement remain separate. A proof should exhibit the required limits, image factorizations and stable joins or cite a theorem transferring them under stated hypotheses; examples checked only on a few objects do not establish a category-wide universal property. Approximation or noisy evidence may weaken a classification without changing its definition.

Manages Complexity¶

The abstraction compresses syntactic categories of coherent theories, pretoposes, coherent toposes, categories of algebraic or relational structures, small and locally small settings, coherent functors, Heyting enrichments, geometric infinitary extensions, and alternative regularity axiom packages into a stable carrier, rule, invariant, and failure boundary. It makes comparison tractable while retaining the variables that control validity.

Compression can hide assumptions. A responsible use therefore declares finite-limit structure, image factorization, regular-epimorphism convention, subobject posets, bottom subobject, binary and finite joins, pullback stability, functor preservation, category size, exactness strength, and internal logic fragment and returns to the full diagnostic whenever a convention or boundary case changes.

Abstract Reasoning¶

Type the carrier. Establish a category with finite limits, regular image factorizations, and a subobject poset for every object and reject examples from a different problem.
Lock the rule. Express that regular-category structure is present and finite unions of subobjects exist and are stable under pullback, equivalently the subobject inverse-image maps preserve finite joins under the adopted convention independently of one notation or implementation.
Derive carefully. Infer giving semantics to coherent first-order theories, constructing classifying categories and toposes, comparing logical theories through functors, using subobject lattices as internal predicates, and proving completeness or conservativity results only under the stated assumptions.
Stress-test. Contrast the legitimate boundary case—Equivalent definitions package effective or regular epimorphisms differently, and size assumptions matter for model categories; an axiom list should be compared at the level of derived regular structure rather than by counting superficially different clauses—with this counterexample: a finitely complete category whose subobject lattices lack finite joins is not coherent even though many logical conjunctions and equations can still be interpreted.

Knowledge Transfer¶

Transfer within category theory is strong when new cases preserve the same carrier, mechanism, and diagnostic. The move from For a coherent first-order theory, its syntactic category has formulas-in-context as objects and provably functional relations as arrows, with conjunction, existential quantification and finite disjunction represented by the coherent categorical operations to A coherent functor from a small coherent category into Set acts as a model whose interpretation preserves finite limits, regular images and finite unions of definable subobjects demonstrates that continuity.^[3]

Outside the domain, only the skeleton—combine a compositional carrier with operations interpreting a chosen logic and require those operations to remain stable under substitution—travels automatically. The terms finite limit, regular category, regular epimorphism, monomorphism, image, subobject, pullback, finite join, coherent functor, coherent logic, syntactic category, and classifying topos retain domain-specific meanings, so every role and inference must be revalidated.

Examples¶

Canonical¶

For a coherent first-order theory, its syntactic category has formulas-in-context as objects and provably functional relations as arrows, with conjunction, existential quantification and finite disjunction represented by the coherent categorical operations The logic–category correspondence depends on the exact operations: disjunction is a join of subobjects stable under substitution, not merely an object-level coproduct, and existential image must be stable under pullback. It is canonical because the carrier, rule, invariant, and consequence are all inspectable.^[1]

Mapped back: a category with finite limits, regular image factorizations, and a subobject poset for every object → Finite limits interpret conjunction and equality, regular images interpret existential quantification, and pullback-stable finite joins interpret disjunction; preservation makes these logical operations compatible with substitution along morphisms → regular-category structure is present and finite unions of subobjects exist and are stable under pullback, equivalently the subobject inverse-image maps preserve finite joins under the adopted convention → giving semantics to coherent first-order theories, constructing classifying categories and toposes, comparing logical theories through functors, using subobject lattices as internal predicates, and proving completeness or conservativity results

Applied / In Practice¶

A coherent functor from a small coherent category into Set acts as a model whose interpretation preserves finite limits, regular images and finite unions of definable subobjects This turns a structural preservation claim into a semantic one. A general functor into Set does not qualify merely because its object assignments resemble a model. It qualifies only after the same diagnostic and failure boundary are checked.^[2]

Mapped back: declared instance → recognition test → boundary check → qualified use

Structural Tensions¶

T1: Exact identity vs. practical recognition. The constitutive condition may be exact while evidence is indirect. Diagnostic: Can the reviewer state both the condition and the warrant?
T2: Canonical form vs. variants. syntactic categories of coherent theories, pretoposes, coherent toposes, categories of algebraic or relational structures, small and locally small settings, coherent functors, Heyting enrichments, geometric infinitary extensions, and alternative regularity axiom packages can preserve or change the identity. Diagnostic: Which named role is invariant across the variants?
T3: Compression vs. hidden assumptions. The label is useful only while prerequisites remain visible. Diagnostic: Can each downstream inference be traced to a declared assumption?
T4: Autonomy vs. reduction. The candidate uses broader structures but claims the conjunction of regular categorical structure with pullback-stable finite subobject unions, and its role as semantics for coherent logic, not generic consistency, categorical coherence diagrams, or coherence of sheaves. Diagnostic: Does that residual still support independent recognition after the parent and neighbors are subtracted?

Structural–Framed Character¶

The entry is structurally mixed but domain-framed. Its portable skeleton is combine a compositional carrier with operations interpreting a chosen logic and require those operations to remain stable under substitution; its identity-bearing terms are finite limit, regular category, regular epimorphism, monomorphism, image, subobject, pullback, finite join, coherent functor, coherent logic, syntactic category, and classifying topos. Those terms determine admissible objects, evidence, and consequences inside category theory.

Structural Core vs. Domain Accent¶

The structural core is a carrier governed by Finite limits interpret conjunction and equality, regular images interpret existential quantification, and pullback-stable finite joins interpret disjunction; preservation makes these logical operations compatible with substitution along morphisms and tested by verify finite limits, construct and test pullback-stable regular epi–mono image factorizations, form finite joins in each subobject poset, test their stability under inverse image, distinguish chosen representatives from subobject equivalence classes, and check that any claimed coherent functor preserves the required structure. The domain accent is constitutive rather than decorative, so an analogy that preserves only the skeleton is not another instance of Coherent category.

This entry is a kind of Category.

A coherent category is literally a category—objects and composable arrows—equipped with additional exactness and subobject-union structure. What makes it its own entry is the conjunction of regular categorical structure with pullback-stable finite subobject unions, and its role as semantics for coherent logic rather than generic consistency, coherence diagrams, or coherence of sheaves.

Relationships to Other Abstractions¶

Current abstraction Coherent category Domain-specific

Parents (1) — outgoing typed relations

Coherent category is a kind of Category Prime

A coherent category is literally a category—objects and composable arrows—equipped with additional exactness and subobject-union structure.

Hierarchy paths (3) — routes to 3 parentless roots

Coherent category → is a kind of Category → includes Associativity → is a kind of Invariance

Show alternative paths (2)

Neighborhood in Abstraction Space¶

Coherent category sits in a crowded region of the domain-specific corpus (24^th percentile for distinctiveness): several abstractions share nearly its structure, so a description that fits it tends to fit its neighbors too.

Family — Unclustered & Miscellaneous (2769 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-25

Not to Be Confused With¶

Regular category. Provides finite limits and pullback-stable regular images but need not have stable finite unions of subobjects.
Heyting category. A coherent category with suitable right adjoints interpreting implication and universal quantification.
Coherence theorem. A theorem that canonical diagrams commute in a monoidal or other categorical structure, not this categorical-logic species.
Coherent sheaf. A finiteness condition on modules or sheaves, unrelated to the definition by regularity and stable subobject joins.

References¶

[1] Michael Makkai and Gonzalo E. Reyes, First Order Categorical Logic, Lecture Notes in Mathematics 611, Springer, 1977, DOI 10.1007/BFb0066201. registry ↩a ↩b

[2] Peter T. Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Volume 1, Oxford University Press, 2002, ISBN 978-0-19-853425-9. registry ↩a ↩b

[3] Olivia Caramello, Theories, Sites, Toposes: Relating and Studying Mathematical Theories through Topos-Theoretic Bridges, Oxford University Press, 2018, ISBN 978-0-19-875891-4. registry ↩