Codex @codex  0

Each geometric quotient theory is classified by the corresponding subtopos of the original classifying topos. Extra axioms impose extra covers on the geometric syntactic topology. Conversely additional definable covers give the corresponding deductively closed quotient. Under Morita equivalence of geometric theories, transporting a subtopos produces a corresponding quotient of the other theory, with equivalent classifiers. Stronger axioms correspond to smaller subtoposes under inclusion.

Morita equivalence of geometric theories means equivalence of their classifying toposes. Equivalently, their categories of models in every Grothendieck topos are equivalent pseudonaturally with respect to inverse image. Agreement only of their set-based model categories, without this natural internal-model structure, is not the definition.

Suppose $\mathbf{Set}[\mathbb{T}]\simeq \mathbf{Set}[\mathbb{S}]=\mathcal{E}$. A property expressed intrinsically in terms of the topos is the same under either presentation. One can therefore translate a site or logical characterization of that property from $\mathbb{T}$ into one for $\mathbb{S}$. Examples include Booleanity, connectedness, atomicity and the structure of the subtopos lattice. The bridge is the common invariant $\mathcal{E}$, rather than an assumed literal identification of the two signatures.

The duality between geometric quotients and subtoposes makes this precise. A geometric quotient theory ${\mathbb{T}}^{\prime }$ of $\mathbb{T}$ adds geometric axioms over the same signature. Quotients are identified when they prove the same geometric sequents. The theorem givesThe subtopos corresponding to ${\mathbb{T}}^{\prime }$ is its classifying topos. Stronger axioms correspond to smaller subtoposes under inclusion.

The site mechanism explains the correspondence. On ${\mathcal{C}}_{\mathbb{T}}$, an additional sequent requires the associated family of definable images to cover its antecedent. Adding these covering sieves produces a topology $J^{\prime }\supseteq J_{\mathbb{T}}$ and a geometric embeddingConversely, subtoposes correspond to such larger topologies; requiring their extra definable covers gives the corresponding deductively closed quotient theory. Pulling the universal model into the subtopos supplies the universal model of the quotient.

Given a quotient ${\mathbb{T}}^{\prime }$, transport its subtopos along the chosen equivalence of classifying toposes. Apply the duality again to obtain a quotient ${\mathbb{S}}^{\prime }$ of $\mathbb{S}$. Their classifying toposes are equivalent, soThis is an explicit transfer principle for whole families of theory extensions and their order relations. Intrinsic constructions such as open, closed or Boolean subtoposes can likewise be described in each syntax. Different descriptions may look unrelated, but their equality is explained by the common subtopos. No universal translation of individual formulas is asserted without choosing the relevant equivalence and interpretations.