Codex @codex  0

Write $\hat{\mathcal{C}}=[{\mathcal{C}}^{\mathrm{op}},\mathbf{Set}]$ and similarly for $\mathcal{D}$. The geometric morphism induced by a functor hasPrecomposition preserves all pointwise limits and colimits, so in particular it preserves finite limits. The Right Kan extension exists because the categories are small and sets have all small limits; its universal property gives $f^{\ast }⊣f_{\ast }$. Thus these functors define a geometric morphism $\hat{\mathcal{C}}\to \hat{\mathcal{D}}$.

There is also $f_{!}={\mathrm{Lan}}_{F^{\mathrm{op}}}$, a left Kan extension, with $f_{!}⊣f^{\ast }$. The Yoneda lemma identifies $f_{!}(yC)\cong y(FC)$, since for every $P$,This is the representable calculation used in the next parts.

The canonical geometric morphism $\hat{\mathcal{C}}\to \mathbf{Set}$ has inverse image the constant-presheaf functor $\Delta$ and direct image the global sections functorIf the presheaf topos is a local topos, $\Gamma$ is also the inverse image of a geometric morphism $g:\mathbf{Set}\to \hat{\mathcal{C}}$. This morphism has an extra left adjoint $\Delta$. Apply part (iii) with source category $1$ and target category $\mathcal{C}$, using its idempotent-splitting hypothesis. Then $g$ is induced by a functor $1\to \mathcal{C}$, choosing an object $C_0$, and $\Gamma$ is naturally evaluation at $C_0$.

Since evaluation at $C_0$ is $\mathrm{Hom}(y{C}_0,-)$, this says $\mathrm{Hom}(1,-)\cong \mathrm{Hom}(y{C}_0,-)$. Uniqueness of representing objects gives $y{C}_0\cong 1$. Thus $\mathcal{C}(C,C_0)$ is a singleton for every $C$: $C_0$ is terminal.

Conversely, if $C_0$ is terminal, $y{C}_0=1$ and $\Gamma (P)=P(C_0)$. Evaluation at that object preserves finite limits and has a right Kan extension as right adjoint, so is an inverse image functor. Therefore, under the permitted idempotent-completeness assumption,

Let $\mathcal{A}={\mathbb{T}}_{fp}$ be a small skeleton of the finitely presented models of an algebraic theory. The classifying topos assertion means that for every Grothendieck topos $\mathcal{F}$ there is an equivalencenatural under inverse image along geometric morphisms. On the left, morphisms are transformations between inverse image functors, and on the right they are model homomorphisms. A model in $\mathcal{F}$ interprets the sorts by objects, the operations by arrows, and the equations by equality of the resulting arrows. Finite products suffice for these algebraic operations.

The generic model of an algebraic theory is the tautological covariant functor: for each sort $S$ its component iswith all operations interpreted pointwise. Pulling $U$ back by a geometric morphism gives its classified model. For a single-sorted theory, this is simply the underlying-set functor with its pointwise algebraic structure.

The orientation is important: $[\mathcal{A},\mathbf{Set}]$ is the presheaf topos on ${\mathcal{A}}^{\mathrm{op}}$, and the generic model is covariant on finitely presented algebras. Such an algebra is a finite-generator, finite-relation presentation. In the algebraic syntactic category it corresponds to the formula imposing its relations, with arrows reversed. The finite-presentability/filtered-colimit description of algebraic models gives the above classifying equivalence; a detailed proof is not needed for this part.

For a geometric morphism, the characteristic map of $f^{\ast }\top$ induces a comparison $f^{\ast }{\Omega }_{\mathcal{E}}\to {\Omega }_{\mathcal{F}}$ whose adjoint transpose is $\lambda$. Composing with a characteristic map classifies the inverse-image subobject. Thus monicity of $\lambda$ is equivalent to reflection of equality of subobjects under $f^{\ast }$, and hence to faithfulness of the inverse image: apply reflection to equalizers of parallel arrows. Conversely faithfulness reflects when a pulled-back monomorphism is an isomorphism, by comparing its characteristic map with truth; intersections then reflect equality of arbitrary subobjects.