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: v2 · 2026-08-30 · History
Domain-specific #: 1493
Origin domain: category theory
Subdomain: categorical logic and topos theory

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.

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.

The proposed strict upward parent is prime:category. A coherent category is literally a category—objects and composable arrows—equipped with additional exactness and subobject-union structure. Stable images and finite joins supply the autonomous categorical-logic residual. The edge is proposal-only and points to a frozen prior-baseline Prime.

The entry does not collapse into the parent because 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 A thematic neighbor is declined whenever it does not literally subsume that rule.

The prospective workspace queue contains one strict upward edge to prime:category. No live DAG mutation is authorized.

Relationships to Other Abstractions¶

Current abstraction Coherent category Domain-specific

Parents (1) — more general patterns this builds on

Coherent category is a kind of Category Prime

The proposed strict upward parent is prime:category.

Hierarchy paths (3) — routes to 3 parentless roots

Coherent category → Category → Associativity → Invariance

Show alternative paths (2)

Neighborhood in Abstraction Space¶

Coherent category sits in a moderately populated region (41^st percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.

Family — Categorical Algebra & Model Systems (8 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-09-08

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 ↩