Syntactic presentations for glued toposes
and for crystalline toposes

Dissertation

zur Erlangung des akademischen Grades

Dr. rer. nat.

eingereicht an der

Mathematisch-Naturwissenschaftlich-Technischen Fakultät

der Universität Augsburg

von

Matthias Hutzler

Augsburg, Oktober 2021

Gutachter:
Marc Nieper-Wißkirchen, Universität Augsburg
Thierry Coquand, University of Gothenburg

Datum der mündlichen Prüfung:
03.12.2021

Im Gedenken an meinen Papa,
der mich auf seine Schultern hob.

## Abstract

We regard a geometric theory classified by a topos as a syntactic presentation
for the topos and develop tools for finding such presentations. Extensions (or
expansions) of geometric theories, which can not only add axioms but also
symbols and sorts, are treated as objects in their own right, to be able to
build up complex theories from parts. The role of equivalence extensions,
which leave the theory the same up to Morita equivalence, is investigated.

Motivated by the question what the big Zariski topos of a non-affine scheme
classifies, we show how to construct a syntactic presentation for a topos if
syntactic presentations for a covering family of open subtoposes are given.
For this, we introduce a transformation of theory extensions such that when
the result, dubbed a conditional extension, is added to a theory, it requires
part of the data a model is made of only under some condition given in the
form of a closed geometric formula. We also give a general definition for
systems of interdependent theory extensions, to be able to talk about
compatible syntactic presentations not only for the open subtoposes in a given
cover but also for their finite intersections.

An important concept for finding classified theories of toposes in concrete
situations is that of theories of presheaf type. We develop several techniques
for extending a theory while preserving the presheaf type property, and give a
list of examples of simple extensions which can destroy it.

Finally, we determine a syntactic presentation of the big crystalline topos of
a scheme. In the case of an affine scheme, this is accomplished by showing
that the biggest part of the classified theory is of presheaf type and
transforming the site defining the crystalline topos into the canonical
presheaf site for this theory, while the remaining axioms induce the Zariski
topology. Then we can apply our results on gluing classifying toposes to
obtain a classified theory even in the non-affine case.

###### Contents

  1. 1 Introduction
  2. 2 Extensions of geometric theories
    1. 2.1 Background on geometric theories
    2. 2.2 Theory extensions as presentations of geometric morphisms
    3. 2.3 Equivalence extensions
    4. 2.4 Some examples of equivalence extensions
  3. 3 Gluing classifying toposes
    1. 3.1 Introduction
    2. 3.2 Conditional extensions
    3. 3.3 Systems of theory extensions
    4. 3.4 Systems of conditional extensions
    5. 3.5 Syntactic presentation of a glued topos
    6. 3.6 The localic case
    7. 3.7 Application to Zariski toposes
    8. 3.8 Conditional extensions and Artin gluing
  4. 4 Theories of presheaf type
    1. 4.1 Introduction
    2. 4.2 Background
    3. 4.3 Rigid-topology quotients
    4. 4.4 Syntactic constructions preserving presheaf type
    5. 4.5 Some counterexamples
  5. 5 Syntactic presentations for crystalline toposes
    1. 5.1 Introduction
    2. 5.2 Background on divided power rings
    3. 5.3 Relevant geometric theories
    4. 5.4 Definition of the big crystalline topos
    5. 5.5 Preliminary presheaf type results
    6. 5.6 Finiteness conditions for PD schemes
    7. 5.7 Syntactic presentation of the big crystalline topos
    8. 5.8 The non-affine case

##  1 Introduction

This thesis elaborates in various ways on the theme in topos theory that a
Grothendieck topos can be viewed as _the essence of a geometric theory_.
Formally, one says that a Grothendieck topos $\mathcal{E}$ _classifies_ the
geometric theory $\mathbb{T}$ if the models of $\mathbb{T}$ in any
Grothendieck topos $\mathcal{E}^{\prime}$ correspond to the geometric
morphisms from $\mathcal{E}^{\prime}$ to $\mathcal{E}$. Since the topos
$\mathcal{E}$ is then uniquely determined by the theory $\mathbb{T}$, we can
take the dual standpoint that the theory $\mathbb{T}$ is a _presentation_ for
the topos $\mathcal{E}$. (All theories that we will meet will be geometric
theories, and the term topos will always mean Grothendieck topos.)

One reason why we might seek such a presentation for a given topos is that it
can be much more concise and, we would argue, even more intuitive than a
definition of the same topos by a site. The prime example for this,
originating in [6], is the big Zariski topos
$\mathcal{E}=(\operatorname{Spec}\mathbb{Z})_{\mathrm{Zar}}$ of the affine
scheme $\operatorname{Spec}\mathbb{Z}$. A site of definition for $\mathcal{E}$
is given by the opposite category of the category of all finitely presentable
rings, equipped with a certain Grothendieck topology called the Zariski
topology, which involves localizations $A_{a}$ of a ring $A$ at an element
$a\in A$ and the condition that some elements generate the unit ideal $(1)=A$.
On the other hand, one can also define $\mathcal{E}$ as the classifying topos
of the theory of local rings. Here, a full definition consists simply in
writing down the usual algebraic operations and axioms defining a
(commutative, unitary) ring and the extra axiom that the ring be local, stated
in the elementary form that if a sum of elements is invertible, then one of
these elements is invertible too. Of course, to get an actual Grothendieck
topos out of this, one needs the whole machinery of classifying toposes, but
the presentation itself is quite short and very approachable. To a certain
degree, it is even possible to judge manipulations of the syntactic
presentation correctly, based on nothing but intuition from elementary
algebra. For example, the classifying topos stays the same if we add to the
list of axioms a redundant one like $(xy)z=(zy)x$, but not if we add an axiom
like $x=-x$.

Another reason is simply that a classified geometric theory for a topos
$\mathcal{E}$ is a description of the representable functor
$\operatorname{Hom}(-,\mathcal{E})$, that is, it is a definition for
$\mathcal{E}$ by a universal property. We would like to stress that since
Grothendieck toposes form a 2-category, the representable functor
$\operatorname{Hom}(-,\mathcal{E})$ is in fact a pseudofunctor, from the
2-category of Grothendieck toposes to the 2-category of categories. Such a
pseudofunctor comprises a huge amount of data, and it is notoriously difficult
to keep track of the coherence conditions that this data must satisfy. In
contrast, it is simple to check whether a geometric theory is well-defined,
and while it can in general contain arbitrarily big sets (of relation and
function symbols, say) as well, the examples showing up in practice are often
more or less finitary.

It should be mentioned here that syntactic presentations of toposes do always
exist, and there is a clear procedure for constructing a classified geometric
theory out of a given site presentation of a topos. But a presentation
constructed in this way will of course generally not tell us anything more
about the topos then the site itself does. Whenever we speak of searching for
syntactic presentations, we intend to find a _concise_ presentation, or one
that is interesting for some other reason.

The first of our two main goals, which will occupy us in Sections 2 and 3,
will be to give a construction on the level of geometric theories for an
operation which is very natural when viewing toposes as generalized
topological spaces, namely the operation of gluing toposes along open
subtoposes. More precisely, our setup will be that $\mathcal{E}$ is a topos
covered by open subtoposes $\mathcal{E}_{i}=\mathcal{E}_{o(U_{i})}$, and
syntactic presentations for the $\mathcal{E}_{i}$ are given. Then we ask how
to construct a syntactic presentation for $\mathcal{E}$, and what additional
data might be needed for this. The appropriate gluing data will consist,
unsurprisingly, of syntactic presentations of the intersections of the
$\mathcal{E}_{i}$, but not given independently of those for the
$\mathcal{E}_{i}$, but rather compatible with them, or, really, _extending_
them. Here, the notion of extensions of geometric theories will be crucial,
which will therefore be investigated first. The formula we give for the theory
classified by $\mathcal{E}$ (see Theorem 3.5.4) will then be quite elegant, it
simply adds up all the given theory extensions, after transforming them into
theory extensions for “partial models” over the respective open subtoposes.
This gluing technique is then applied to deduce a syntactic presentation for
the big Zariski topos of a non-affine scheme (see Theorem 3.7.6) from the
well-known result in the affine case.

Our second objective, in Sections 4 and 5, is to give syntactic presentations
for another family of toposes from algebraic geometry, namely the crystalline
toposes of schemes. These toposes were introduced around 1970 to study
crystalline cohomology, a tool for extracting geometric information from
schemes, similar to de Rham cohomology, but specifically adapted to schemes
over ground fields of positive characteristic. While more and more classified
theories for other toposes from algebraic geometry were found over the years,
a syntactic presentation of the crystalline topos was up to now missing. The
construction of a crystalline topos depends in fact not on a single scheme, as
for the Zariski topos, but on two schemes with some additional structure. This
is reflected in the more involved classified theory we give (see Theorem
5.7.4), but it is still very much related to the theory of local rings, and
the universal model living in the crystalline topos consists precisely of its
structure sheaf and some additional data associated to it. The case of affine
base schemes is treated first, and relies heavily on techniques for
recognizing theories of presheaf type which we develop for this purpose. It is
then simply another application of the gluing theorem to generalize to the
non-affine case (see Theorem 5.8.3), although some extra care is needed in
constructing an open cover and a system of syntactic presentations for it.

## Acknowledgements

I thank Marc Nieper-Wißkirchen for guiding me towards the topics of this
thesis and for his trusting supervision. I thank Ingo Blechschmidt, who played
a very special role in my mathemetical socialization, for tons of
encouragement and for letting so much knowledge diffuse from his mind to mine.
And I thank Theresa Ritter for being infinitely patient with me and for
supporting me in every way possible!

##  2 Extensions of geometric theories

###  2.1 Background on geometric theories

For a full definition of geometric theories, we refer to [7, Chapter D1.1].
But we want to mention that a geometric theory $\mathbb{T}$ can be thought of
as consisting of three “layers”, first come the _sorts_ , then the _relation_
and _function symbols_ , and finally the _axioms_. The first two layers are
often called the _signature_ of the theory. What is allowed in each layer
depends on the data in the previous layers: The set of sorts of $\mathbb{T}$
is just a set without any additional structure. The relation and function
symbols have their own signatures, which in this case just means a list of
sorts, and which we denote

$R\subseteq A_{1}\times\dots\times A_{n}\qquad\text{and}\qquad
f:A_{1}\times\dots\times A_{n}\to B\hbox to0.0pt{,\hss}$

where $A_{1},\dots,A_{n}$ and $B$ are sorts of $\mathbb{T}$. And the axioms
are sequents of the form

$\phi\;\vdash_{x_{1}\,{:}\,A_{1},\dots,x_{n}\,{:}\,A_{n}}\;\psi\hbox
to0.0pt{,\hss}$

to be read as “$\phi$ implies $\psi$ in the context
$x_{1}\,{:}\,A_{1},\dots,x_{n}\,{:}\,A_{n}$”, where the geometric formulas
$\phi$ and $\psi$ can use the relation and function symbols of $\mathbb{T}$.
The context will sometimes be abbreviated $\vec{x}\,{:}\,\vec{A}$.

A relation symbol with the empty signature, $n=0$, which we might denote
$R\subseteq 1$, is called a _proposition symbol_ , and we will rather use the
letter $p$ for it. Similarly, a function symbol with empty domain, $n=0$, is
called a _constant symbol_ , and instead of $f:1\to B$, we simply denote it as
$f:B$, or rather $c:B$. A geometric theory is _propositional_ if it has no
sorts, and therefore also no function symbols and no relation symbols except
proposition symbols.

A _model_ $M$ of a geometric theory $\mathbb{T}$ in a topos $\mathcal{E}$
consists of objects

$\llbracket A\rrbracket_{M}\in\mathcal{E}$

for all sorts $A$ of $\mathbb{T}$, subobjects

$\llbracket R\rrbracket_{M}\subseteq\llbracket
A_{1}\rrbracket_{M}\times\dots\times\llbracket A_{n}\rrbracket_{M}$

for all relation symbols $R$ of $\mathbb{T}$ and morphisms

$\llbracket f\rrbracket_{M}:\llbracket
A_{1}\rrbracket_{M}\times\dots\times\llbracket
A_{n}\rrbracket_{M}\to\llbracket B\rrbracket_{M}$

for all function symbols $f$ of $\mathbb{T}$, such that the axioms of
$\mathbb{T}$ are fulfilled. Given a model $M$, we can not only _interpret_
individual sorts and symbols in $M$, but also any geometric formula $\phi$ of
$\mathbb{T}$ in a context $x_{1}\,{:}\,A_{1},\dots,x_{n}\,{:}\,A_{n}$,
yielding a subobject

$\llbracket\phi\rrbracket_{M}\subseteq\llbracket
A_{1}\rrbracket_{M}\times\dots\times\llbracket A_{n}\rrbracket_{M}\hbox
to0.0pt{.\hss}$

The requirement that an axiom

$\phi\;\vdash_{\vec{x}\,{:}\,\vec{A}}\;\psi$

is fulfilled in $M$ means that there is an inclusion of subobjects

$\llbracket\phi\rrbracket_{M}\leq\llbracket\psi\rrbracket_{M}\hbox
to0.0pt{.\hss}$

There is also a notion of _morphism_ between models of the same theory in the
same topos, and the resulting category of $\mathbb{T}$-models in $\mathcal{E}$
will be denoted

$\mathbb{T}\text{-}\allowbreak\mathrm{mod}(\mathcal{E})\hbox to0.0pt{.\hss}$

Furthermore, the requirement that the axioms of $\mathbb{T}$ are geometric
sequents ensures that pulling back the individual parts of a model
$M\in\mathbb{T}\text{-}\allowbreak\mathrm{mod}(\mathcal{E})$ along a geometric
morphism $f:\mathcal{E}^{\prime}\to\mathcal{E}$ yields a model of $\mathbb{T}$
in $\mathcal{E}^{\prime}$. For a fixed model
$M\in\mathbb{T}\text{-}\allowbreak\mathrm{mod}(\mathcal{E})$ and varying $f$,
this constitutes a functor

$\mathrm{Geom}(\mathcal{E}^{\prime},\mathcal{E})\to\mathbb{T}\text{-}\allowbreak\mathrm{mod}(\mathcal{E}^{\prime})\hbox
to0.0pt{,\hss}$

and the model $M$ is called a _universal model_ of $\mathbb{T}$ if this
functor is an equivalence of categories for all (Grothendieck) toposes
$\mathcal{E}^{\prime}$. The topos $\mathcal{E}$ is then called a _classifying
topos_ for the geometric theory $\mathbb{T}$, and we will call the pair
$(\mathbb{T},M)$ a _syntactic presentation_ of the topos $\mathcal{E}$.

It is a theorem that every (Grothendieck) topos classifies some geometric
theory and every geometric theory admits a classifying topos, that is, a
universal model in some topos. The classifying topos of a theory is also
unique up to equivalence, which justifies writing

$\mathrm{Set}[\mathbb{T}]$

for a classifying topos of a theory $\mathbb{T}$. But it is not at all true
that the classified theory of a topos is unique. Instead, two theories
admitting universal models in the same topos are called _Morita equivalent_
theories.

There is of course also a notion of provability for geometric theories, which
we will not define here. A geometric sequent which is provable in a geometric
theory $\mathbb{T}$ is fulfilled in any model of $\mathbb{T}$ in any topos, so
it could just as well be added as an axiom of $\mathbb{T}$. Two theories
$\mathbb{T}_{1}$ and $\mathbb{T}_{2}$ over the same signature (same sorts and
symbols) are called _syntactically equivalent_ if every axiom of
$\mathbb{T}_{1}$ is provable in $\mathbb{T}_{2}$ and vice versa. Note that
this is a much stronger condition on $\mathbb{T}_{1}$ and $\mathbb{T}_{2}$
than being Morita equivalent, since Morita equivalent theories can have
different signatures. We will simply write syntactic equivalence as equality,

$\mathbb{T}_{1}=\mathbb{T}_{2}\hbox to0.0pt{.\hss}$

The universal model of a theory $\mathbb{T}$ is unique in the sense that for
any two universal models in toposes $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$,
there is an equivalence $\mathcal{E}_{1}\simeq\mathcal{E}_{2}$ sending one to
the other. With respect to provability, it has the following strong property.
A geometric sequent of a theory $\mathbb{T}$ is fulfilled in the universal
model of $\mathbb{T}$ if and only if it is provable in $\mathbb{T}$.

Finally, we would like to make the point that when manipulating geometric
theories, one has to think intuitionistically. This is not the case when the
matter is only about axioms; it is a well-known theorem that any geometric
sequent which is provable from the axioms of a geometric theory using full
classical first-order logic is also provable from these axioms in geometric
logic. But if we are also interested in adding sorts and symbols, the
intuitionistic nature shows clearly. For example, the theory consisting of a
single proposition symbol $p$ has two models (up to isomorphism) in
$\mathrm{Set}$, as the interpretation of $p$ can be either true or false. The
same is true for the theory with two proposition symbols $p$ and $q$ and the
axioms

$\top\;\vdash_{[]}\;p\lor q\quad\text{and}\quad p\land
q\;\vdash_{[]}\;\bot\hbox to0.0pt{.\hss}$

But these are two completely different theories, as a model of the first
theory in a topos $\mathcal{E}$ is just an open subtopos of $\mathcal{E}$,
while a model of the second theory is a decomposition of $\mathcal{E}$ into
two subtoposes which are both open and closed. And even the categories of
models in $\mathrm{Set}$ are not equivalent, since proposition symbols are
allowed to become true but not to become false under model homomorphisms.

###  2.2 Theory extensions as presentations of geometric morphisms

######  Definition 2.2.1.

A (geometric) _extension_ $\mathbb{E}$ of a geometric theory $\mathbb{T}$
consists of a set ${\mathbb{E}\operatorname{-Sort}}$ of sorts, sets
${\mathbb{E}\operatorname{-Rel}}$ and ${\mathbb{E}\operatorname{-Fun}}$ of
relation and function symbols over the sorts
${\mathbb{T}\operatorname{-Sort}}\sqcup{\mathbb{E}\operatorname{-Sort}}$ and a
set of geometric axioms over the sorts
${\mathbb{T}\operatorname{-Sort}}\sqcup{\mathbb{E}\operatorname{-Sort}}$ and
the symbols
${\mathbb{T}\operatorname{-Rel}}\sqcup{\mathbb{E}\operatorname{-Rel}}$ and
${\mathbb{T}\operatorname{-Fun}}\sqcup{\mathbb{E}\operatorname{-Fun}}$. We
denote $\mathbb{T}+\mathbb{E}$ the theory obtained by adding these sorts,
symbols and axioms to $\mathbb{T}$. The extension $\mathbb{E}$ is _localic_ if
${\mathbb{E}\operatorname{-Sort}}=\varnothing$; it is a _quotient extension_
if additionally ${\mathbb{E}\operatorname{-Rel}}=\varnothing$ and
${\mathbb{E}\operatorname{-Fun}}=\varnothing$.

If $\mathbb{E}$ is an extension of $\mathbb{T}$, we have a forgetful functor

$U_{\mathbb{E}}:{(\mathbb{T}+\mathbb{E})\operatorname{-mod}(\mathcal{E})}\to{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$

for every Grothendieck topos $\mathcal{E}$. Note that this functor is an
isofibration. Also, after fixing classifying toposes
$\mathrm{Set}[\mathbb{T}]$ and $\mathrm{Set}[\mathbb{T}+\mathbb{E}]$, the
$\mathbb{T}$-model part of the universal $(\mathbb{T}+\mathbb{E})$-model
induces a canonical geometric morphism

$\pi_{\mathbb{E}}:\mathrm{Set}[\mathbb{T}+\mathbb{E}]\to\mathrm{Set}[\mathbb{T}]\hbox
to0.0pt{,\hss}$

which in turn acts on generalized points by the functors $U_{\mathbb{E}}$ (up
to natural isomorphism). This is the geometric morphism _presented_ by the
extension $\mathbb{E}$.

The following theorem says that every geometric morphism can be presented in
this way, thus generalizing the result that every Grothendieck topos
classifies a geometric theory to the relative situation over some base topos
$\mathrm{Set}[\mathbb{T}]$ with an already chosen syntactic presentation.

######  Theorem 2.2.2 ([5, Theorem 7.1.5]).

Let a geometric morphism

$p:\mathcal{E}\to\mathrm{Set}[\mathbb{T}]$

to the classifying topos of a geometric theory $\mathbb{T}$ be given. Then $p$
is, up to isomorphism, of the form
$\pi_{\mathbb{E}}:\mathrm{Set}[\mathbb{T}+\mathbb{E}]\to\mathrm{Set}[\mathbb{T}]$
for some extension $\mathbb{E}$ of $\mathbb{T}$. If $p$ is localic
(respectively an embedding), then we can take $\mathbb{E}$ to be a localic
extension (respectively a quotient extension).

###### Proof.

See [5, Theorem 7.1.5]. The case of an embedding, which is not mentioned
there, is instead part of the duality between subtoposes and quotient theories
[5, Theorem 3.2.5]. ∎

Given two extensions $\mathbb{E}_{1}$ and $\mathbb{E}_{2}$ of a theory
$\mathbb{T}$, it is clear that we can also regard $\mathbb{E}_{2}$ as an
extension of $\mathbb{T}+\mathbb{E}_{1}$ and vice versa. Then we have a strict
pullback diagram of categories

${(\mathbb{T}+\mathbb{E}_{1}+\mathbb{E}_{2})\text{-}\allowbreak\mathrm{mod}(\mathcal{E})}$${(\mathbb{T}+\mathbb{E}_{2})\text{-}\allowbreak\mathrm{mod}(\mathcal{E})}$${(\mathbb{T}+\mathbb{E}_{1})\text{-}\allowbreak\mathrm{mod}(\mathcal{E})}$${\mathbb{T}\text{-}\allowbreak\mathrm{mod}(\mathcal{E})}$${\lrcorner}$

for any topos $\mathcal{E}$, which is also a weak pullback, since the the
forgetful functors are isofibrations. This means that
$\mathrm{Set}[\mathbb{T}+\mathbb{E}_{1}+\mathbb{E}_{2}]$ is the pullback topos
of $\mathrm{Set}[\mathbb{T}+\mathbb{E}_{1}]$ and
$\mathrm{Set}[\mathbb{T}+\mathbb{E}_{2}]$ over $\mathrm{Set}[\mathbb{T}]$. In
particular, the product (as generalized spaces, not as categories) of two
classifying toposes $\mathrm{Set}[\mathbb{T}_{1}]$ and
$\mathrm{Set}[\mathbb{T}_{2}]$ classifies the theory
$\mathbb{T}_{1}+\mathbb{T}_{2}$.

In the same way in which we prefer to have a symbol for an extension
$\mathbb{E}$ instead of only for the extended theory
$\mathbb{T}^{\prime}=\mathbb{T}+\mathbb{E}$, we will also want to regard the
data that is missing in a $\mathbb{T}$-model compared to a
$(\mathbb{T}+\mathbb{E})$-model as an object in its own right.

######  Definition 2.2.3.

A _model extension_ $E$ of a model
$M\in{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$ along a theory extension
$\mathbb{E}$ of $\mathbb{T}$ consists of interpretations for the sorts and
symbols of $\mathbb{E}$ that extend $M$ to a model
$M+E\in{(\mathbb{T}+\mathbb{E})\operatorname{-mod}(\mathcal{E})}$. A
_homomorphism_ of model extensions of $M$ is a family of maps, one for each
sort of $\mathbb{E}$, that constitutes a $(\mathbb{T}+\mathbb{E})$-model
homomorphism when combined with the identity homomorphism of $M$. That is, the
category of model extensions of $M$ along $\mathbb{E}$ is isomorphic to the
strict preimage of $M$ under $U_{\mathbb{E}}$; it will be denoted
${\mathbb{E}\operatorname{-mod}(\mathcal{E},M)}$ or simply
${\mathbb{E}\operatorname{-mod}(M)}$.

######  Remark 2.2.4.

Note that our terminology here is somewhat in conflict with the usage of for
example “elementary extension” in set theory, which means a bigger model of
the same theory.

Using the notion of model extensions, Theorem 2.2.2 can be formulated as
follows. Given any model
$M\in\mathbb{T}\text{-}\allowbreak\mathrm{mod}(\mathcal{E})$ of a geometric
theory in some topos, there is always an extension $\mathbb{E}$ of
$\mathbb{T}$ and a model extension $E$ of $M$ along $\mathbb{E}$ such that the
model
$(M+E)\in(\mathbb{T}+\mathbb{E})\text{-}\allowbreak\mathrm{mod}(\mathcal{E})$
is universal.

###  2.3 Equivalence extensions

######  Definition 2.3.1.

An _equivalence extension_ is an extension $\mathbb{E}$ of $\mathbb{T}$ such
that the forgetful functor
$U_{\mathbb{E}}:{(\mathbb{T}+\mathbb{E})\operatorname{-mod}(\mathcal{E})}\to{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$
is an equivalence of categories for every Grothendieck topos $\mathcal{E}$.
Equivalently, the geometric morphism
$\pi_{\mathbb{E}}:\mathrm{Set}[\mathbb{T}+\mathbb{E}]\to\mathrm{Set}[\mathbb{T}]$
presented by $\mathbb{E}$ is an equivalence.

If $\mathbb{E}$ is an equivalence extension of a theory $\mathbb{T}$, then it
is also an equivalence extension of $\mathbb{T}+\mathbb{E}^{\prime}$, for any
other extension $\mathbb{E}^{\prime}$ of $\mathbb{T}$. This is clear from the
(weak) pullback property of the category
$(\mathbb{T}+\mathbb{E}_{1}+\mathbb{E}_{2})\text{-}\allowbreak\mathrm{mod}(\mathcal{E})$.

######  Lemma 2.3.2.

An extension $\mathbb{E}$ of a theory $\mathbb{T}$ is an equivalence extension
if and only if every model $M\in{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$
in every Grothendieck topos $\mathcal{E}$ admits exactly one model extension
along $\mathbb{E}$ up to isomorphism.

###### Proof.

The given condition means that
$U_{\mathbb{E}}:{(\mathbb{T}+\mathbb{E})\operatorname{-mod}(\mathcal{E})}\to{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$
is bijective on isomorphism classes for every topos $\mathcal{E}$, which at
first sight seems weaker than being an equivalence. But it means that the
functors
$\mathrm{Geom}(\mathcal{E},\mathrm{Set}[\mathbb{T}+\mathbb{E}])\to\mathrm{Geom}(\mathcal{E},\mathrm{Set}[\mathbb{T}])$
induced by the geometric morphism
$\pi_{\mathbb{E}}:\mathrm{Set}[\mathbb{T}+\mathbb{E}]\to\mathrm{Set}[\mathbb{T}]$
are bijective on isomorphism classes, in other words, $\pi_{\mathbb{E}}$ is an
isomorphism in the 1-category of toposes and geometric morphisms up to
isomorphism, which is the same as an equivalence of toposes. ∎

######  Remark 2.3.3.

Lemma 2.3.2 is a version of the slogan that if we know the models of a
geometric theory, we also know the morphisms between them, see [7, below Lemma
B4.2.3]. However, here it does not suffice to simply say that a morphism of
$\mathbb{T}$-models in $\mathcal{E}$ is the same as a $\mathbb{T}$-model in
the topos $\mathcal{E}^{\to}$ (the arrow category of $\mathcal{E}$), as
$U_{\mathbb{E}}$ can be bijective on isomorphism classes for both
$\mathcal{E}$ and $\mathcal{E}^{\to}$ without being an equivalence for
$\mathcal{E}$. For example, let $\mathbb{T}=\varnothing$, let $\mathbb{E}$ be
the theory of $G$-torsors for a group $G$ and let $\mathcal{E}=\mathrm{Set}$.
Denote $\underline{G}$ the one object groupoid associated to $G$. Then both of
the functors

$\displaystyle\underline{G}\simeq{(\mathbb{T}+\mathbb{E})\operatorname{-mod}(\mathrm{Set})}\to{\mathbb{T}\operatorname{-mod}(\mathrm{Set})}\simeq\\{*\\}\hbox
to0.0pt{,\hss}$
$\displaystyle\underline{G}\simeq\underline{G}^{\to}\simeq(\mathbb{T}+\mathbb{E})\text{-}\allowbreak\mathrm{mod}(\mathrm{Set}^{\to})\to\mathbb{T}\text{-}\allowbreak\mathrm{mod}(\mathrm{Set}^{\to})\simeq\\{*\\}^{\to}\simeq\\{*\\}\hbox
to0.0pt{,\hss}$

are bijective on isomorphism classes, but the first is not an equivalence.

######  Lemma 2.3.4.

Let $M\in{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$ be a universal model,
$\mathbb{E}$ an extension of $\mathbb{T}$ and $E$ a model extension of $M$
along $\mathbb{E}$. Then $\mathbb{E}$ is an equivalence extension if and only
if $M+E\in{(\mathbb{T}+\mathbb{E})\operatorname{-mod}(\mathcal{E})}$ is again
universal.

###### Proof.

This is immediate from the two-out-of-three property of equivalences of
categories in the diagram

$\leavevmode\hbox to172.76pt{\vbox
to72.62pt{\pgfpicture\makeatletter\hbox{\hskip
86.38042pt\lower-36.31236pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-86.38042pt}{-36.31236pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
0.0pt\hfil&\hfil\hskip 74.40906pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-34.10341pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${{(\mathbb{T}+\mathbb{E})\operatorname{-mod}(\mathcal{E}^{\prime})}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
38.40895pt\hfil\cr\vskip 8.99994pt\cr\hfil\hskip
29.97142pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-25.66588pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathrm{Geom}(\mathcal{E}^{\prime},\mathcal{E})}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
29.97142pt\hfil&\hfil\hskip 36.0001pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil\cr\vskip 8.99994pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 63.22847pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-22.92282pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${{\mathbb{T}\operatorname{-mod}(\mathcal{E}^{\prime})}\hbox
to0.0pt{.\hss}}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
27.22836pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{47.97148pt}{11.74437pt}\pgfsys@lineto{47.97148pt}{-23.66383pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{47.97148pt}{-23.86382pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{50.32425pt}{-7.86804pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{U_{\mathbb{E}}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-26.23758pt}{1.25177pt}\pgfsys@lineto{13.60513pt}{11.64345pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.96764}{0.25237}{-0.25237}{0.96764}{13.79863pt}{11.6939pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ }}{ } {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-36.8227pt}{10.60083pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{-^{*}(M+E)}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-26.23758pt}{-14.46649pt}\pgfsys@lineto{20.15613pt}{-26.57181pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9676}{-0.25247}{0.25247}{0.9676}{20.34961pt}{-26.62228pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-17.08748pt}{-27.70572pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{-^{*}M}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\qed$

Apart from syntactic equivalences, one way to produce an equivalence extension
of a theory $\mathbb{T}$ is to add new symbols for relations or functions that
were already definable in $\mathbb{T}$. We now want to show that all localic
equivalence extensions are of this form up to syntactic equivalence, meaning
that we have a simple syntactic characterization of equivalence extensions
among the localic extensions.

######  Definition 2.3.5.

Let $\mathbb{T}$ be a geometric theory, let $R_{i}\subseteq\vec{A}^{i}$ and
$f_{j}:\vec{B}^{j}\to C^{j}$ be families of new relation and function symbols
(with signatures consisting of sorts of $\mathbb{T}$) and let
$\\{\vec{x}\,{:}\,\vec{A}^{i}\,.\;\phi_{i}(\vec{x})\\}$ and
$\\{\vec{y}\,{:}\,\vec{B}^{j},z\,{:}\,C^{j}\,.\;\psi_{j}(\vec{y},z)\\}$ be
formulas of $\mathbb{T}$ in corresponding contexts, where every $\psi_{j}$ is
provably functional. Then the _extension by definitions_ for this data is the
localic extension of $\mathbb{T}$ consisting of the symbols $R_{i}$, $f_{j}$
and the axioms

$R_{i}(\vec{x})\;\dashv\vdash_{\vec{x}\,{:}\,\vec{A}^{i}}\;\phi_{i}(\vec{x})\qquad\text{and}\qquad
f_{j}(\vec{y})=z\;\dashv\vdash_{\vec{y}\,{:}\,\vec{B}^{j},z\,{:}\,C^{j}}\;\psi_{j}(\vec{y},z).$

######  Remark 2.3.6.

To show that a given localic extension $\mathbb{E}$ of a theory $\mathbb{T}$
is (syntactically equivalent to) an extension by definitions, one has to find
formulas $\phi_{i}$, $\psi_{j}$ of $\mathbb{T}$, the latter provably
functional, for the relation and function symbols of $\mathbb{E}$, such that
the axioms in Definition 2.3.5 are provable in $\mathbb{T}+\mathbb{E}$, and
furthermore, one has to check that all axioms of $\mathbb{E}$ are already
provable in $\mathbb{T}$ if the symbols $R_{i}$, $f_{j}$ are replaced by the
formulas $\phi_{i}$, $\psi_{j}$. However, this last check can be omitted if a
model extension $E$ along $\mathbb{E}$ of a universal $\mathbb{T}$-model $M$
is available, since then any $\mathbb{T}$-sequent which is true in $M+E$ is
trivially also true in $M$ and therefore provable in $\mathbb{T}$. For the
same reason, it is then automatic that the $\psi_{j}$ are provably functional.
This will be relevant in applications of Corollary 3.6.1.

######  Proposition 2.3.7.

A localic extension is an equivalence extension if and only if it is
(syntactically equivalent to) an extension by definitions.

###### Proof.

If $\mathbb{E}$ is an extension by definitions of $\mathbb{T}$ then any model
$M\in{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$ admits exactly one model
extension $E$ along $\mathbb{E}$, namely $\llbracket
R_{i}\rrbracket_{M+E}\vcentcolon=\llbracket\phi_{i}\rrbracket_{M}$ and
$\llbracket f_{i}\rrbracket_{M+E}$ is the morphism with graph
$\llbracket\psi_{j}\rrbracket_{M}$. So $\mathbb{E}$ is an equivalence
extension by Lemma 2.3.2.

On the other hand, if $\mathbb{E}$ is an equivalence extension of
$\mathbb{T}$, then consider a universal model
$M\in{\mathbb{T}\operatorname{-mod}(\mathrm{Set}[\mathbb{T}])}$ and the unique
(up to isomorphism) extension $E$ of $M$ along $\mathbb{E}$. By Lemma 2.3.4,
$M+E$ is a universal model of $\mathbb{T}+\mathbb{E}$. Now, for every relation
symbol $R\subseteq\vec{A}$ introduced in $\mathbb{E}$, $\llbracket
R\rrbracket_{M+E}$ is a subobject of $\llbracket
A_{1}\rrbracket_{M}\times\dots\times\llbracket A_{n}\rrbracket_{M}$ and since
$M$ is universal, [5, Theorem 6.1.3] tells us that there is a formula
$\phi_{R}$ of $\mathbb{T}$ with $\llbracket\phi_{R}\rrbracket_{M}=\llbracket
R\rrbracket_{M+E}$. Similarly, for every new function symbol $f$ we find a
provably functional formula $\psi_{f}$ of $\mathbb{T}$ such that
$\llbracket\psi_{f}\rrbracket_{M}$ is the graph of $\llbracket
f\rrbracket_{M+E}$. That is, the axioms for defining $R$ by $\phi_{R}$ and $f$
by $\psi_{f}$ are fulfilled for $M+E$ and therefore provable in
$\mathbb{T}+\mathbb{E}$. Thus, we have
$\mathbb{E}=\mathbb{E}_{1}+\mathbb{E}_{2}$ where $\mathbb{E}_{1}$ is an
extension by definitions and $\mathbb{E}_{2}$ is a quotient. But since both
$\mathbb{E}_{1}$ and $\mathbb{E}_{1}+\mathbb{E}_{2}$ are equivalence
extensions, $\mathbb{E}_{2}$ must be one too, and we have (up to syntactic
equivalence) $\mathbb{E}_{2}=\varnothing$ and $\mathbb{E}=\mathbb{E}_{1}$. ∎

The following lemma is about “reverting” an extension $\mathbb{E}$ of
$\mathbb{T}$ by applying another extension $\mathbb{E}^{\prime}$, subject to
extensibility of the universal $\mathbb{T}$-model along $\mathbb{E}$.

######  Lemma 2.3.8.

Let $M\in{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$ be a universal model
and $E$ an extension of $M$ along some theory extension $\mathbb{E}$. Then
there is a localic extension $\mathbb{E}^{\prime}$ of $\mathbb{T}+\mathbb{E}$
and a model extension $E^{\prime}$ of $M+E$ along $\mathbb{E}^{\prime}$ such
that
$(M+E+E^{\prime})\in{(\mathbb{T}+\mathbb{E}+\mathbb{E}^{\prime})\operatorname{-mod}(\mathcal{E})}$
is again universal. (In particular, $\mathbb{E}+\mathbb{E}^{\prime}$ is an
equivalence extension.) If $\mathbb{E}$ is localic, $\mathbb{E}^{\prime}$ can
be chosen as a quotient; if $\mathbb{E}$ is a quotient,
$\mathbb{E}^{\prime}=\varnothing$ fits the bill.

${\mathbb{T}+\mathbb{E}+\mathbb{E}^{\prime}}$${\mathbb{T}+\mathbb{E}}$${\mathbb{T}}$$\scriptstyle{\sim}$

###### Proof.

Fix a classifying topos $\mathcal{E}_{\mathbb{T}+\mathbb{E}}$ for
$\mathbb{T}+\mathbb{E}$. We have the forgetful geometric morphism
$u:\mathcal{E}_{\mathbb{T}+\mathbb{E}}\to\mathcal{E}$, and
$M+E\in{(\mathbb{T}+\mathbb{E})\operatorname{-mod}(\mathcal{E})}$ corresponds
to a section (up to isomorphism)
$s:\mathcal{E}\to\mathcal{E}_{\mathbb{T}+\mathbb{E}}$ of $u$. As such, $s$ is
localic (since $u\circ s$ is). By Theorem 2.2.2, it is therefore presented by
some localic extension $\mathbb{E}^{\prime}$ of $\mathbb{T}+\mathbb{E}$, that
is, we have a universal model of $\mathbb{T}+\mathbb{E}+\mathbb{E}^{\prime}$
in $\mathcal{E}$ extending $M+E$, as required.

The two special cases follow since a section of a localic geometric morphism
is an embedding and a section of an embedding is an equivalence, but we can
also show them more directly. If $\mathbb{E}=\mathbb{Q}$ is a quotient, then
the existence of $E$ just means that the new axioms are fulfilled in $M$. But
this means that they were already provable in $\mathbb{T}$ and $M=M+E$ is
indeed a universal model of $\mathbb{T}+\mathbb{Q}$. For $\mathbb{E}$ localic,
we have to deal with the new relation symbols $R$ and function symbols $f$.
From [5, Theorem 6.1.3] we know that $\llbracket
R(\vec{x})\rrbracket_{M+E}=\llbracket\phi_{R}(\vec{x})\rrbracket_{M}$ and
$\llbracket
f(\vec{x})=y\rrbracket_{M+E}=\llbracket\phi_{f}(\vec{x},y)\rrbracket_{M}$ for
some formulas $\phi_{R}$, $\phi_{f}$, where $\phi_{f}$ is provably functional.
So taking for $\mathbb{E}^{\prime}$ the axioms
$R(\vec{x})\;\dashv\vdash_{\vec{x}}\;\phi_{R}(\vec{x})$ and
$f(\vec{x})=y\;\dashv\vdash_{\vec{x},y}\;\phi_{f}(\vec{x},y)$, we obtain as
$\mathbb{E}+\mathbb{E}^{\prime}$ an extension by definitions. ∎

As a corollary, we find that an equivalence between two theories, and more
generally an equivalence between two extensions of some base theory (meaning
that they present the same geometric morphism), can always be captured in a
syntactic way.

######  Corollary 2.3.9.

Let $\mathbb{E}_{1}$, $\mathbb{E}_{2}$ be two equivalent extensions of a
theory $\mathbb{T}$, that is, there exists a model
$M\in{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$ with extensions to
universal models $M+E_{1}$ and $M+E_{2}$ of $\mathbb{T}+\mathbb{E}_{1}$
respectively $\mathbb{T}+\mathbb{E}_{2}$ in the same topos $\mathcal{E}$. Then
there is a localic extension $\mathbb{E}_{1,2}$ of
$\mathbb{T}+\mathbb{E}_{1}+\mathbb{E}_{2}$ such that both
$\mathbb{E}_{2}+\mathbb{E}_{1,2}$ and $\mathbb{E}_{1}+\mathbb{E}_{1,2}$ are
equivalence extensions (of $\mathbb{T}+\mathbb{E}_{1}$ respectively
$\mathbb{T}+\mathbb{E}_{2}$)

${\mathbb{T}+\mathbb{E}_{1}+\mathbb{E}_{2}+\mathbb{E}_{1,2}}$${\mathbb{T}+\mathbb{E}_{1}}$${\mathbb{T}+\mathbb{E}_{2}}$${\mathbb{T}}$$\scriptstyle{\sim}$$\scriptstyle{\sim}$

and there is a model extension $E_{1,2}$ along $\mathbb{E}_{1,2}$ such that
$M_{0}+E_{1}+E_{2}+E_{1,2}$ is universal. If $\mathbb{E}_{1}$ or
$\mathbb{E}_{2}$ is localic, then $\mathbb{E}_{1,2}=\mathbb{Q}_{1,2}$ can be
chosen as a quotient extension.

###### Proof.

Regard $\mathbb{E}_{2}$ as an extension of $\mathbb{T}+\mathbb{E}_{1}$ for the
moment, then we have an extension $E_{2}$ of the universal model $M+E_{1}$, so
by Lemma 2.3.8 there exists a localic extension $\mathbb{E}_{1,2}$ of
$\mathbb{T}+\mathbb{E}_{1}+\mathbb{E}_{2}$ together with a model extension
$E_{1,2}$ of $M+E_{1}+E_{2}$ such that $M+E_{1}+E_{2}+E_{1,2}$ is universal.
Then, by Lemma 2.3.4, both $\mathbb{E}_{2}+\mathbb{E}_{1,2}$ and
$\mathbb{E}_{1}+\mathbb{E}_{1,2}$ are equivalence extensions, as required. If
$\mathbb{E}_{1}$ is localic, we get a quotient extension
$\mathbb{E}_{1,2}=\mathbb{Q}_{1,2}$ from Lemma 2.3.8, and if $\mathbb{E}_{2}$
is localic, we swap the two. ∎

A completely different proof of Corollary 2.3.9 in the absolute case
$\mathbb{T}=\varnothing$ can be found in [10, Theorem 5.1].

######  Definition 2.3.10.

We call an extension $\mathbb{E}_{1,2}$ as in Corollary 2.3.9 a _diagonal
extension_ for $\mathbb{E}_{1}$ and $\mathbb{E}_{2}$ over $\mathbb{T}$,
because it presents the diagonal geometric morphism of the pullback topos

$\mathrm{Set}[\mathbb{T}+\mathbb{E}_{1}+\mathbb{E}_{2}]=\mathrm{Set}[\mathbb{T}+\mathbb{E}_{1}]\times_{\mathrm{Set}[\mathbb{T}]}\mathrm{Set}[\mathbb{T}+\mathbb{E}_{2}]=\mathcal{E}\times_{\mathrm{Set}[\mathbb{T}]}\mathcal{E}\hbox
to0.0pt{.\hss}$

Diagonal extensions are not unique. For example, if $\mathbb{T}_{1}=\langle
p_{1}\rangle+\langle p_{2}\rangle$ and $\mathbb{T}_{2}=\langle
p_{3}\rangle+\langle p_{4}\rangle$ both consist of two proposition symbols,
there are clearly two different diagonal quotient extensions for
$\mathbb{T}_{1}$ and $\mathbb{T}_{2}$ over $\varnothing$. Corollary 2.3.9
produces a diagonal extension in accordance with the two universal models
$M_{0}+E_{1}$ and $M_{0}+E_{2}$ living in the same topos.

Another easy consequence of Lemma 2.3.8 is that any object of the classifying
topos of a theory can be introduced into the theory as a new sort by means of
an equivalence extension.

######  Corollary 2.3.11.

Let $M\in{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$ be a universal model
and let $X\in\mathcal{E}$ be any object. Then there is an equivalence
extension $\mathbb{E}$ of $\mathbb{T}$ containing exactly one new sort $A$,
such that the unique (up to unique isomorphism) model extension $E$ of $M$
along $\mathbb{E}$ interprets $A$ as $X$.

###### Proof.

Apply Lemma 2.3.8 to the extension $\mathbb{E}_{1}$ adding nothing but the
sort $A$ (and the model extension $E_{1}$ given by $\llbracket
A\rrbracket_{E_{1}}\vcentcolon=X$) to obtain a localic extension
$\mathbb{E}_{2}$, and set
$\mathbb{E}\vcentcolon=\mathbb{E}_{1}+\mathbb{E}_{2}$. ∎

###  2.4 Some examples of equivalence extensions

Giving examples of localic equivalence extensions does not seem necessary
after Proposition 2.3.7, but here are some non-localic equivalence extensions
that will be of use later.

######  Example 2.4.1.

Let $A$ be a sort of a geometric theory $\mathbb{T}$ and let $\phi(x)$ be a
geometric formula in the context $x\,{:}\,A$. Then there is an equivalence
extension of $\mathbb{T}$ consisting of a sort $S_{\phi}$, a function symbol
$\iota:S_{\phi}\to A$ and the axioms

$\iota(x)=\iota(y)\;\vdash_{x,y\,{:}\,S_{\phi}}\;x=y\qquad\text{and}\qquad\exists
x{\,:\,}S_{\phi}.\;\iota(x)=y\;\dashv\vdash_{y\,{:}\,A}\;\phi(y)\hbox
to0.0pt{,\hss}$

the first of which forces the interpretation of $\iota$ in a model to be a
monomorphism, while the second ensures that $\llbracket
S_{\phi}\rrbracket\hookrightarrow\llbracket A\rrbracket$ is the same subobject
as $\llbracket\phi\rrbracket\hookrightarrow\llbracket A\rrbracket$.

######  Example 2.4.2.

Let $A$ be a sort of a geometric theory $\mathbb{T}$ and let $x\sim
x^{\prime}$ be a geometric formula in the context $x,x^{\prime}\,{:}\,A$ such
that the usual axioms of an equivalence relation (which are Horn sequents) are
provable for $\sim$. Then there is an equivalence extension of $\mathbb{T}$
consisting of a sort $A/{\sim}$, a function symbol $\pi:A\to A/{\sim}$ and the
axioms

$\top\;\vdash_{y\,{:}\,A/{\sim}}\;\exists
x{\,:\,}A.\;\pi(x)=y\qquad\text{and}\qquad\pi(x)=\pi(x^{\prime})\;\dashv\vdash_{x,x^{\prime}\,{:}\,A}\;x\sim
x^{\prime}\hbox to0.0pt{.\hss}$

These force the interpretation $\llbracket A\rrbracket\to\llbracket
A/{\sim}\rrbracket$ of $\pi$ to be an epimorphism with kernel pair
$\llbracket\sim\rrbracket\rightrightarrows\llbracket A\rrbracket$.

######  Remark 2.4.3.

An intermediate notion between syntactic equivalence and Morita equivalence is
the notion of (geometric) _bi-interpretability_ , see [5, Definition 2.1.13].
Two geometric theories are bi-interpretable if and only if their syntactic
sites are equivalent categories. So while this notion is still syntactic in
nature, it does not assume any previously given relation between the
signatures of the two theories. For example, a sort $A$ of the first theory,
which is represented in the syntactic site by the object
$\\{x\,{:}\,A.\;\top\\}$, can correspond to any formula in context
$\\{\vec{y}\,{:}\,\vec{B}.\;\phi(\vec{y})\\}$ of the second theory.

The equivalence extension in Example 2.4.1 induces a bi-interpretation,
interpreting the new sort $S_{\phi}$ by the formula in context
$\\{x\,{:}\,A.\;\phi(x)\\}$ of $\mathbb{T}$. But already Example 2.4.2 shows
that bi-interpretability is a stronger condition than Morita equivalence,
since the formula in context $\\{x\,{:}\,A/{\sim}.\;\top\\}$ can not be
expressed as any formula in context of $\mathbb{T}$.

######  Example 2.4.4.

Given a set $A$, define a theory $\underline{A}$ (named after its only sort)
consisting of a sort $\underline{A}$, constant symbols $c_{a}:\underline{A}$
for every element $a\in A$ and the axioms

$c_{a}=c_{a^{\prime}}\;\vdash_{[]}\;\bot\quad\text{for $a\neq a^{\prime}\in
A$},\qquad\qquad\top\;\vdash_{x:\underline{A}}\;\bigvee_{a\in A}(x=c_{a})\hbox
to0.0pt{.\hss}$

One can check that the unique model (up to unique isomorphism) in any
Grothendieck topos is the constant sheaf associated to the set $A$, which is
also denoted $\underline{A}$. The theory $\underline{A}$ is therefore Morita-
equivalent to the empty theory, and adding $\underline{A}$ to any given theory
is an equivalence extension. In other words, we can always _import_ a set $A$
into our theory without changing it up to Morita-equivalence.

If we have a function like $f:A\to B$ or a relation like $R\subseteq A$, we
can import it together with the respective sets. Namely, after adding a
function symbol $\underline{f}:\underline{A}\to\underline{B}$ or a relation
symbol $\underline{R}\subseteq\underline{A}$, the axioms

$\top\;\vdash_{[]}\;\underline{f}(c_{a})=c_{f(a)}\quad\text{for $a\in A$}$

respectively

$\top\;\vdash_{[]}\;\underline{R}(c_{a})\quad\text{for $a\in
R$},\qquad\qquad\underline{R}(c_{a})\;\vdash_{[]}\;\bot\quad\text{for $a\in
A\setminus R$}$

produce an extension by definitions in presence of the axioms of
$\underline{A}$.

Another perspective on this is that if we have any model of a geometric theory
$\mathbb{T}$ in $\mathrm{Set}$, then by Lemma 2.3.8 there is a localic
extension to a universal model in $\mathrm{Set}$, which then yields, by
pulling back along the unique geometric morphism to $\mathrm{Set}$, the unique
model of the extended theory in any topos.

##  3 Gluing classifying toposes

###  3.1 Introduction

In this section we explicitly construct a geometric theory classified by a
given topos from a cover by open subtoposes with known classified theories.

We already saw in Section 2 that taking the product of two toposes, regarded
as generalized spaces, corresponds to the simplest possible operation
involving two unrelated theories, namely forming the sum
$\mathbb{T}_{1}+\mathbb{T}_{2}$. The present topic is a generalization of the
dual question what the coproduct of two toposes classifies. This is much less
obvious, since a geometric morphism
$\mathcal{E}\to\mathrm{Set}[\mathbb{T}_{1}]\amalg\mathrm{Set}[\mathbb{T}_{2}]$
will neither define a $\mathbb{T}_{1}$-model nor a $\mathbb{T}_{2}$-model in
$\mathcal{E}$. Instead, it first of all defines a decomposition of
$\mathcal{E}$ into two clopen subtoposes, and then a $\mathbb{T}_{1}$-model in
one and a $\mathbb{T}_{2}$-model in the other of these subtoposes.

Another good example is the big Zariski topos of the projective line
$\mathbb{P}^{1}_{K}$ over a ring $K$. The big Zariski topos $X_{\mathrm{Zar}}$
of an affine scheme $X=\operatorname{Spec}R$ classifies the geometric theory
of local $R$-algebras. Now, $\mathbb{P}^{1}_{K}$ is not affine, but it can be
covered by two copies of the affine line, $\operatorname{Spec}K[X]$ and
$\operatorname{Spec}K[Y]$, such that the intersection is
$\operatorname{Spec}K[X,Y]/(XY-1)$. We will see that this induces an open
cover of the big Zariski topos $(\mathbb{P}^{1}_{K})_{\mathrm{Zar}}$ by open
subtoposes $(\operatorname{Spec}K[X])_{\mathrm{Zar}}$ and
$(\operatorname{Spec}K[Y])_{\mathrm{Zar}}$, which both classify local
$K$-algebras with one distinguished element. This suggests that
$(\mathbb{P}^{1}_{K})_{\mathrm{Zar}}$ classifies local $K$-algebras which are
equipped with an element $X$ _or_ with an element $Y$, where the two
possibilities are not mutually exclusive but rather, their intersection is
described by the condition $XY=1$. A formulation of this idea as a geometric
theory, which indeed presents $(\mathbb{P}^{1})_{\mathrm{Zar}}$, is given in
Proposition 3.7.5.

###  3.2 Conditional extensions

If a topos $\mathcal{E}$ has an open subtopos
$\mathcal{E}_{1}\subseteq\mathcal{E}$ which classifies some theory
$\mathbb{T}_{1}$, then a geometric morphism
$f:\tilde{\mathcal{E}}\to\mathcal{E}$ does not give us a model of
$\mathbb{T}_{1}$ in $\tilde{\mathcal{E}}$, so to find a classified theory for
$\mathcal{E}$, we should not look among extensions of $\mathbb{T}_{1}$.
However, $f$ does give us a model of $\mathbb{T}_{1}$ in some open subtopos of
$\tilde{\mathcal{E}}$, namely in the preimage of $\mathcal{E}_{1}$. We now
show how to capture syntactically the requirement of “a model in some open
subtopos”.

To avoid technical complications, we exclude function symbols from our
discussion. Recall that a function symbol $f:\vec{A}\to B$ can be considered
an abbreviation for a relation symbol $R\subseteq\vec{A}\times B$ together
with axioms ensuring that $R$ is provably functional, as long as we don’t mind
replacing axioms with nested function applications like $g(f(x))=z$ by
versions with auxiliary variables like $\exists y.\,(f(x)=y)\land(g(y)=z)$.
That is, function symbols can be considered “syntactic sugar”.

######  Definition 3.2.1.

Let $\mathbb{T}$ be a geometric theory, $\phi$ a closed formula of
$\mathbb{T}$ and $\mathbb{E}$ an extension (without function symbols) of
$\mathbb{T}+\phi$. We define the _conditional extension_ $\mathbb{E}/\phi$ of
$\mathbb{T}$ to consist of the following.

  * •

For every sort $S\in{\mathbb{E}\operatorname{-Sort}}$ of $\mathbb{E}$, a sort
$S$ and the axiom $\top\;\vdash_{x:S}\;\phi$.

  * •

For every relation symbol $R\subseteq S_{1}\times\dots\times S_{n}$ of
$\mathbb{E}$, a relation symbol $R\subseteq S_{1}\times\dots\times S_{n}$ and
the axiom $R(\vec{x})\;\vdash_{\vec{x}:\vec{S}}\;\phi$.

  * •

For every axiom $\psi_{1}\;\vdash_{\Gamma}\;\psi_{2}$ of $\mathbb{E}$, the
axiom $\psi_{1}\land\phi\;\vdash_{\Gamma}\;\psi_{2}$.

If the theory $\mathbb{T}+\phi+\mathbb{E}$ asks us to specify a model of
$\mathbb{T}$ that satisfies $\phi$ and furthermore a model extension along
$\mathbb{E}$, then the theory $\mathbb{T}+\mathbb{E}/\phi$ instead asks us to
specify a model of $\mathbb{T}$ and a model extension along $\mathbb{E}$ _in
case_ our $\mathbb{T}$-model happens to satisfy $\phi$ — or, more
geometrically speaking, _wherever_ it satisfies $\phi$.

######  Lemma 3.2.2.

The assignment $\mathbb{E}\mapsto\mathbb{E}/\phi$ is well-defined with respect
to syntactic equivalence. Furthermore, we have the following syntactic
equivalences.

  1. (i)

$\mathbb{T}+\mathbb{E}/\phi+\phi=\mathbb{T}+\phi+\mathbb{E}$

  2. (ii)

$\mathbb{T}+\mathbb{E}_{1}/\phi+\mathbb{E}_{2}/\phi=\mathbb{T}+(\mathbb{E}_{1}+\mathbb{E}_{2})/\phi$

###### Proof.

To show that the construction is well-defined, let
$\psi\;\vdash_{\Gamma}\;\chi$ be a geometric sequent which is provable in
$\mathbb{T}+\phi+\mathbb{E}$. If it was added as an axiom to $\mathbb{E}$, the
axiom $\psi\land\phi\;\vdash_{\Gamma}\;\chi$ would be added to
$\mathbb{E}/\phi$, so we must show that this sequent is already provable in
$\mathbb{T}+\mathbb{E}/\phi$. This is equivalent to showing that
$\psi\;\vdash_{\Gamma}\;\chi$ is provable in
$\mathbb{T}+\mathbb{E}/\phi+\phi$, so we are done if (i) is true. For (i), we
observe that the additional axioms of $\mathbb{E}/\phi$ are indeed trivial and
$\psi_{1}\land\phi\;\vdash_{\Gamma}\;\psi_{2}$ is indeed equivalent to
$\psi_{1}\;\vdash_{\Gamma}\;\psi_{2}$ if our theory already contains $\phi$ as
an axiom. For (ii), Definition 3.2.1 produces the exact same axiomatization
for both sides. ∎

######  Proposition 3.2.3.

Let $\mathbb{E}$ be an extension of $\mathbb{T}+\phi$,
$M\in{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$ and
$\mathcal{F}\vcentcolon=\mathcal{E}_{o(\llbracket\phi\rrbracket_{M})}$ the
open subtopos of $\mathcal{E}$ corresponding to the subterminal object
$\llbracket\phi\rrbracket_{M}\subseteq 1_{\mathcal{E}}$. Then there is an
equivalence of categories

${\mathbb{E}\operatorname{-mod}(\mathcal{F},M|_{\mathcal{F}})}\simeq{(\mathbb{E}/\phi)\operatorname{-mod}(\mathcal{E},M)}\hbox
to0.0pt{.\hss}$

###### Proof.

The open inclusion geometric morphism $i:\mathcal{F}\to\mathcal{E}$ admits a
further (full and faithful) left adjoint $i_{!}:\mathcal{F}\to\mathcal{E}$
with essential image $\mathcal{E}/U$, where
$U\vcentcolon=\llbracket\phi\rrbracket_{M}$. The composition $i_{!}\circ
i^{*}$ is $X\mapsto X\times U$.

${\mathcal{E}/U\simeq\mathcal{F}}$${\mathcal{E}}$$\scriptstyle{i_{!}}$

$\vdash$

$\scriptstyle{i^{*}}$

For a sort $S$ of $\mathbb{E}$, the axiom $\top\;\vdash_{x:S}\;\phi$ of
$\mathbb{E}/\phi$ means precisely that for every
$E\in(\mathbb{E}/\phi)\text{-}\allowbreak\mathrm{mod}(M)$, the object
$\llbracket S\rrbracket_{M+E}$ must lie in the full subcategory
$\mathcal{E}/U$, so we have established the equivalence for the case that
$\mathbb{E}$ contains only sorts. The quasi-inverse is of course the
restriction functor $i^{*}:\mathcal{E}\to\mathcal{F}$, applied to the
interpretation of every sort. For a relation symbol $R\subseteq\vec{S}$ of
$\mathbb{E}$ (where the list $\vec{S}$ may contain sorts from both
$\mathbb{T}$ and $\mathbb{E}$), the axiom
$R(\vec{x})\;\vdash_{\vec{x}:\vec{S}}\;\phi$ similarly means $\llbracket
R\rrbracket_{M+E}\subseteq\llbracket\vec{S}\rrbracket_{M+E}\times U$, so that
$\llbracket R\rrbracket_{M+E}$ corresponds to a subobject of
$i^{*}(\llbracket\vec{S}\rrbracket_{M+E})=\llbracket\vec{S}\rrbracket_{M|_{\mathcal{F}}+E|_{\mathcal{F}}}$.
Finally, the modified axiom $\psi_{1}\land\phi\;\vdash_{\Gamma}\;\psi_{2}$ (or
equivalently $\psi_{1}\land\phi\;\vdash_{\Gamma}\;\psi_{2}\land\phi$) is
satisfied by $M+E$ if and only if $\llbracket\psi_{1}\rrbracket\times
U\subseteq\llbracket\psi_{2}\rrbracket\times U$, that is, if and only if
$\psi_{1}\;\vdash_{\Gamma}\;\psi_{2}$ is satisfied by
$M|_{\mathcal{F}}+E|_{\mathcal{F}}$. ∎

For a model $M\in\mathbb{T}\text{-}\allowbreak\mathrm{mod}(\mathcal{E})$ and
an extension
$E\in\mathbb{E}\text{-}\allowbreak\mathrm{mod}(M|_{\mathcal{E}_{o(\llbracket\phi\rrbracket_{M})}})$,
the corresponding extension of $M$ along $\mathbb{E}/\phi$ will be denoted
$E/\phi$. That means that we have

$(M+E/\phi)|_{\mathcal{E}_{o(\llbracket\phi\rrbracket_{M})}}\cong
M|_{\mathcal{E}_{o(\llbracket\phi\rrbracket_{M})}}+E$

as models of $\mathbb{T}+\mathbb{E}/\phi+\phi=\mathbb{T}+\phi+\mathbb{E}$.

######  Lemma 3.2.4.

An extension $\mathbb{E}$ of $\mathbb{T}+\phi$ is an equivalence extension if
and only if $\mathbb{E}/\phi$ is an equivalence extension of $\mathbb{T}$.

###### Proof.

If $\mathbb{E}/\phi$ is an equivalence extension of $\mathbb{T}$, then it is
also an equivalence extension of $\mathbb{T}+\phi$. But by Lemma 3.2.2 (i),
$\mathbb{E}/\phi$ is syntactically equivalent to $\mathbb{E}$ as an extension
of $\mathbb{T}+\phi$.

Conversely, if $\mathbb{E}$ is an equivalence extension of $\mathbb{T}+\phi$,
then by Lemma 2.3.2, and Proposition 3.2.3 every $\mathbb{T}$-model admits a
unique (up to isomorphism) model extension along $\mathbb{E}/\phi$, so we are
done by the other direction of Lemma 2.3.2. ∎

###  3.3 Systems of theory extensions

Given two equivalence extensions $\mathbb{E}_{1},\mathbb{E}_{2}$ of a theory
$\mathbb{T}$, their sum $\mathbb{E}_{1}+\mathbb{E}_{2}$ is again an
equivalence extension of $\mathbb{T}$. The same is true if $\mathbb{E}_{2}$ is
not an extension of $\mathbb{T}$ but of $\mathbb{T}+\mathbb{E}_{1}$, that is,
if $\mathbb{E}_{2}$ depends on $\mathbb{E}_{1}$. To formulate such statements
in greater generality, we first need to clarify in which ways an extension can
be built up from smaller extensions, possibly with dependencies among them.

######  Definition 3.3.1.

Let $\mathbb{T}$ be a geometric theory. A _system of extensions_ over
$\mathbb{T}$ is a family $(\mathbb{E}_{i})_{i\in I}$, indexed by some
partially ordered set $I$, where each $\mathbb{E}_{i}$ consists of a set of
sorts, sets of relation and function symbols — whose signatures may contain
sorts from $\mathbb{T}$ and all $\mathbb{E}_{j}$ with $j\leq i$, treated
disjointly — and a set of (geometric) axioms — which may again use all sorts
and symbols from $\mathbb{T}$ and $\mathbb{E}_{j}$ with $j\leq i$, treated
disjointly. Taking the disjoint union of the sorts, symbols and axioms of all
$\mathbb{E}_{i}$ thus yields an extension of $\mathbb{T}$, which we denote
$\sum_{i\in I}\mathbb{E}_{i}$.

For a subset $J\subseteq I$ of the partially ordered set $I$, we use the
notation

$J{\downarrow}\vcentcolon=\\{i\in I\mid\exists j\in J:i\leq
j\\}\qquad\text{and}\qquad
J{\downarrow}{\downarrow}\vcentcolon=J{\downarrow}\setminus J\hbox
to0.0pt{.\hss}$

Given an initial segment $J\subseteq I$ (that is, $J{\downarrow}=J$), we can
of course restrict a system $(\mathbb{E}_{i})_{i\in I}$ to $J$, obtaining a
system $(\mathbb{E}_{i})_{i\in J}$ over the same base theory $\mathbb{T}$. In
particular, we see that for every $i\in I$, $\mathbb{E}_{i}$ is an extension
of $\mathbb{T}+\sum_{j<i}\mathbb{E}_{j}$. More generally, the index set $I$
can be restricted to any _inward closed_ subset $J\subseteq I$ (if $i\leq
j\leq k$ and $i,k\in J$ then $j\in J$), resulting in a system
$(\mathbb{E}_{i})_{i\in J}$ over $\mathbb{T}+\sum_{i\in
J{\downarrow}{\downarrow}}\mathbb{E}_{i}$ instead of $\mathbb{T}$.

We can also push a system $(\mathbb{E}_{i})_{i\in I}$ over $\mathbb{T}$
forward along an order-preserving map $f:I\to J$ to another partially ordered
set $J$ by setting $\tilde{\mathbb{E}}_{j}\vcentcolon=\sum_{i\in
f^{-1}(j)}\mathbb{E}_{i}$. Note that $f^{-1}(j)$ is inward closed and
$\tilde{\mathbb{E}}_{j}$ is an extension of $\mathbb{T}+\sum_{i\in
f^{-1}(j){\downarrow}{\downarrow}}\mathbb{E}_{i}$ and therefore also of
$\mathbb{T}+\sum_{j^{\prime}<j}\tilde{\mathbb{E}}_{j^{\prime}}$.

######  Definition 3.3.2.

Let $(\mathbb{E}_{i})_{i\in I}$ be a system of extensions over a theory
$\mathbb{T}$. A _system of model extensions_ $(E_{i})_{i\in I}$ for
$(\mathbb{E}_{i})_{i\in I}$ in a Grothendieck topos $\mathcal{E}$ over some
$M\in{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$ is just a model extension
$\sum_{i\in I}E_{i}$ of $M$ along $\sum_{i\in I}\mathbb{E}_{i}$, regarded as a
family of model extensions $E_{i}$ of $M+\sum_{j<i}E_{j}$ along
$\mathbb{E}_{i}$.

For a family of subtoposes $(\mathcal{E}_{i})_{i\in I}$ of $\mathcal{E}$ with
$\mathcal{E}_{i}\subseteq\mathcal{E}_{j}$ for $j<i$, a system of model
extensions _in the $\mathcal{E}_{i}$_ is similarly a family $(E_{i})_{i\in
I}$, where each $E_{i}$ is an extension of
$M|_{\mathcal{E}_{i}}+\sum_{j<i}E_{j}|_{\mathcal{E}_{i}}$ along
$\mathbb{E}_{i}$. If $M|_{\mathcal{E}_{i}}+\sum_{j\leq
i}E_{j}|_{\mathcal{E}_{i}}$ is a universal model of $\mathbb{T}+\sum_{j\leq
i}\mathbb{E}_{j}$ for every $i\in I$, then we call
$(\mathbb{E}_{i},E_{i})_{i\in I}$ a _system of presentations_ of the
$\mathcal{E}_{i}$ over ($\mathbb{T}$ and) $M$.

The following lemma is our general formulation of how equivalence extensions
can be built up from smaller equivalence extensions. We will also use it (in
Corollary 3.3.5 below) to clarify the role of systems of presentations which
all present the same topos.

######  Lemma 3.3.3.

Let $(\mathbb{E}_{i})_{i\in I}$ be a system over $\mathbb{T}$ where the
partial order $I$ is well-founded. Then the assertions

  1. (i)

For every $i\in I$, $\mathbb{E}_{i}$ is an equivalence extension of
$\mathbb{T}+\sum_{j<i}\mathbb{E}_{j}$.

  2. (ii)

For every $i\in I$, $\sum_{j\leq i}\mathbb{E}_{j}$ is an equivalence extension
of $\mathbb{T}$.

are equivalent and they imply:

  1. (iii)

$\sum_{i\in I}\mathbb{E}_{i}$ is an equivalence extension of $\mathbb{T}$.

###### Proof.

$(i)\Rightarrow(iii)$. We show this implication first, because it will be used
for the others. To see that the functor

$U_{\sum_{i\in I}\mathbb{E}_{i}}:{(\mathbb{T}+\sum_{i\in
I}\mathbb{E}_{i})\operatorname{-mod}(\mathcal{E})}\to{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$

is an equivalence, start by taking two models $M,M^{\prime}$ of
$\mathbb{T}+\sum_{i\in I}\mathbb{E}_{i}$ in $\mathcal{E}$ and homomorphisms
$f,g:M\to M^{\prime}$ with $U_{\sum_{i\in I}\mathbb{E}_{i}}(f)=U_{\sum_{i\in
I}\mathbb{E}_{i}}(g)$. Then we can show $f=g$ by well-founded induction over
$i\in I$ using the faithfulness of each

$U_{\mathbb{E}_{i}}:{(\mathbb{T}+\sum_{j\leq
i}\mathbb{E}_{j})\operatorname{-mod}(\mathcal{E})}\to{(\mathbb{T}+\sum_{j<i}\mathbb{E}_{j})\operatorname{-mod}(\mathcal{E})}\text{.}$

Given instead only $f_{0}:U_{\sum_{i\in I}\mathbb{E}_{i}}(M)\to U_{\sum_{i\in
I}\mathbb{E}_{i}}(M^{\prime})$, we use the fullness of the
$U_{\mathbb{E}_{i}}$ to construct $f:M\to M^{\prime}$ with $U_{\sum_{i\in
I}\mathbb{E}_{i}}(f)=f_{0}$ by well-founded recursion. Finally, let
$M_{0}\in{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$ and notice that the
$U_{\mathbb{E}_{i}}$ are not only essentially surjective but strictly
surjective on objects (since they are isofibrations). This means we can again
use well-founded recursion to construct a model extension $\sum_{i\in I}E_{i}$
of $M_{0}$ and therefore a (strict) preimage $M_{0}+\sum_{i\in I}E_{i}$ of
$M_{0}$ under $U_{\sum_{i\in I}\mathbb{E}_{i}}$.

$(i)\Rightarrow(ii)$. Fix $i\in I$. Then this follows immediately by applying
$(i)\Rightarrow(iii)$ to the restricted system $(\mathbb{E}_{j})_{j\leq i}$.

$(ii)\Rightarrow(i)$. By well-founded induction, let $i\in I$ with
$\mathbb{E}_{j}$ an equivalence extension for all $j<i$. Then by
$(i)\Rightarrow(iii)$ applied to $(\mathbb{E}_{j})_{j<i}$,
$\sum_{j<i}\mathbb{E}_{j}$ is an equivalence extension. But since $\sum_{j\leq
i}\mathbb{E}_{j}=\sum_{j<i}\mathbb{E}_{j}+\mathbb{E}_{i}$ is an equivalence
extension by assumption, $\mathbb{E}_{i}$ must be one too. ∎

######  Remark 3.3.4.

The assumption that $I$ is well-founded is necessary in Lemma 3.3.3. Indeed,
we can take $\mathbb{T}$ to be the empty theory and consider the system of
theory extensions $(\mathbb{E}_{n})_{n\in\mathbb{Z}}$ where every
$\mathbb{E}_{n}$ is the quotient extension consisting of the contradictory
axiom $\top\;\vdash_{[]}\;\bot$. Then none of the $\mathbb{T}+\sum_{m\leq
n}\mathbb{E}_{m}$ is equivalent to $\mathbb{T}$, and neither is
$\mathbb{T}+\sum_{n\in\mathbb{Z}}\mathbb{E}_{n}$, but every $\mathbb{E}_{n}$
is an equivalence extension of $\mathbb{T}+\sum_{m<n}\mathbb{E}_{m}$. If we
insist on treating syntactically equivalent theories as equal, we can even say
that every $\mathbb{E}_{n}$ is the _empty_ extension of its respective base
theory. In this sense, a system of theory extensions $(\mathbb{E}_{i})_{i\in
I}$ is not fully determined by the individual extensions $\mathbb{E}_{i}$, for
$I$ not well-founded. But we would rather argue that the notion of knowing an
extension without knowing its base theory is ill-defined. (In the language of
type theory, the type of extensions is inherently a dependent type.)

######  Corollary 3.3.5.

Let $M\in{\mathbb{T}\operatorname{-mod}(\mathcal{E})}$ be universal. Then a
system of extensions $(\mathbb{E}_{i},E_{i})_{i\in I}$ over $(\mathbb{T},M)$
in $\mathcal{E}$ with $I$ well-founded is a system of presentations of
$\mathcal{E}$ if and only if all $\mathbb{E}_{i}$ are equivalence extensions.
And in this case, $M+\sum_{i\in I}E_{i}\in{(\mathbb{T}+\sum_{i\in
I}\mathbb{E}_{i})\operatorname{-mod}(\mathcal{E})}$ is also universal.

###### Proof.

By Lemma 2.3.4, the universality of the models $M+\sum_{j\leq i}E_{j}$ for all
$i\in I$ is just condition $(ii)$ of Lemma 3.3.3 and the universality of
$M+\sum_{i\in I}E_{i}$ is condition $(iii)$ of Lemma 3.3.3. ∎

###  3.4 Systems of conditional extensions

We now briefly describe how to apply the construction of conditional
extensions to systems of theory extensions. Given a system
$(\mathbb{E}_{i})_{i\in I}$ over $\mathbb{T}$ and a family of closed geometric
formulas $\phi_{i}$ of $\mathbb{T}$, we can of course blindly apply the rules
of Definition 3.2.1 to every $\mathbb{E}_{i}$, and we do get a new system of
extensions

$(\mathbb{E}_{i}/\phi_{i})_{i\in I}$

over $\mathbb{T}$, simply because the signature of $\mathbb{E}_{i}/\phi_{i}$
is the same as that of $\mathbb{E}_{i}$. But then we can not say that the
extension $\mathbb{E}_{i}/\phi_{i}$ of
$\mathbb{T}+\sum_{j<i}\mathbb{E}_{j}/\phi_{j}$ is an honest conditional
extension, since there is no sensible way to regard $\mathbb{E}_{i}$ as an
extension of $\mathbb{T}+\sum_{j<i}\mathbb{E}_{j}/\phi_{j}+\phi_{i}$. For
example, fixing some $\mathbb{T}$, $\mathbb{E}_{1}$ and $\phi_{1}$ and using
$\phi_{2}=\top$, the operation of mapping an extension $\mathbb{E}_{2}$ of
$\mathbb{T}+\phi_{1}+\mathbb{E}_{1}$ to
$\mathbb{T}+\mathbb{E}_{1}/\phi_{1}+\mathbb{E}_{2}$ is not well-defined with
respect to syntactic equivalence.

To remedy this, we impose the condition that

$\phi_{i}\;\vdash_{[]}\;\phi_{j}\qquad\text{for $j\leq i$}$

is provable in $\mathbb{T}$. Then we can regard each $\mathbb{E}_{i}$ as an
extension of

$\mathbb{T}+\sum_{j<i}\mathbb{E}_{j}/\phi_{j}+\phi_{i}=\mathbb{T}+\sum_{j<i}\mathbb{E}_{j}+\phi_{i}\hbox
to0.0pt{,\hss}$

and obtain the system $(\mathbb{E}_{i}/\phi_{i})_{i\in I}$ of conditional
extensions.

In Definition 3.2.1, we treated $\mathbb{E}$ as an extension of
$\mathbb{T}+\phi$, not of $\mathbb{T}$, which is justified in view of Lemma
3.2.4. This refinement is dropped here in order to be able to use our
definition of a system of theory extensions without modification. In our
application (see Theorem 3.5.4 below), the extensions $\mathbb{E}_{i}$ are
such that $\phi_{i}$ is provable from $\mathbb{T}+\sum_{j\leq
i}\mathbb{E}_{i}$.

We also want to be able to construct model extensions, to be denoted as

$M+\sum_{i\in I}E_{i}/\phi_{i}\hbox to0.0pt{,\hss}$

for systems of conditional extensions, as we did in Proposition 3.2.3 for a
single conditional extension. Let $(E_{i})_{i\in I}$ be a family of model
extensions for $(\mathbb{E}_{i})_{i\in I}$, over some
$M\in\mathbb{T}\text{-}\allowbreak\mathrm{mod}(\mathcal{E})$, in the
subtoposes

$\mathcal{E}_{i}\vcentcolon=\mathcal{E}_{o(\llbracket\phi_{i}\rrbracket_{M})}\hbox
to0.0pt{.\hss}$

This makes sense because our requirement on the $\phi_{i}$ ensures
$\mathcal{E}_{i}\subseteq\mathcal{E}_{j}$ for $j\leq i$. Let
$\iota_{i}:\mathcal{E}_{i}\to\mathcal{E}$ be the open embeddings, and also
$\iota_{i}^{j}:\mathcal{E}_{i}\to\mathcal{E}_{j}$ for $j\leq i$.

${\mathcal{E}_{j}}$${\mathcal{E}}$${\mathcal{E}_{i}}$$\scriptstyle{\iota_{j}}$$\scriptstyle{\iota_{i}}$$\scriptstyle{\iota_{i}^{j}}$

Then, like in Proposition 3.2.3, applying $(\iota_{i})_{!}$ to the
interpretations of the sorts of $\mathbb{E}_{i}$ in $E_{i}$ produces objects
in $\mathcal{E}/\llbracket\phi_{i}\rrbracket_{M}$, as required for a model
extension of $M$ along $\sum_{i\in I}\mathbb{E}_{i}/\phi_{i}$. The signatures
of the relation symbols of $\mathbb{E}_{i}$ can contain sorts $S$ from
$\mathbb{E}_{i}$, sorts $S^{\prime}$ from various $\mathbb{E}_{j}$ with $j\leq
i$ and sorts $S^{\prime\prime}$ from $\mathbb{T}$, so the interpretation of
such a symbol is a subobject of an object like

$\llbracket S\rrbracket\times(\iota_{i}^{j})^{*}\llbracket
S^{\prime}\rrbracket\times(\iota_{i})^{*}\llbracket
S^{\prime\prime}\rrbracket\;\in\;\mathcal{E}_{i}\hbox to0.0pt{.\hss}$

Applying $(\iota_{i})_{!}$ yields precisely a subobject of
$(\iota_{i})_{!}\llbracket S\rrbracket\times(\iota_{j})_{!}\llbracket
S^{\prime}\rrbracket\times\llbracket
S^{\prime\prime}\rrbracket\times\llbracket\phi_{i}\rrbracket$, since

$(\iota_{i})_{!}(\iota_{i}^{j})^{*}\llbracket
S^{\prime}\rrbracket=(\iota_{i})_{!}(\iota_{i})^{*}(\iota_{j})_{!}\llbracket
S^{\prime}\rrbracket=(\iota_{j})_{!}\llbracket
S^{\prime}\rrbracket\times\llbracket\phi_{i}\rrbracket\hbox to0.0pt{.\hss}$

Also, the modified axioms of $\mathbb{E}_{i}$ in $\mathbb{E}_{i}/\phi_{i}$
hold for the structure in $\mathcal{E}$ defined this way because they can be
tested after pulling back to $\mathcal{E}_{i}$, as before. In summary, we have
constructed a model extension $\sum_{i\in I}E_{i}/\phi_{i}$ of $M$ (in the
topos $\mathcal{E}$), such that for every $i$, the extension $E_{i}/\phi_{i}$
is obtained from the model extension $E_{i}$ (in the topos $\mathcal{E}_{i}$)
as in Proposition 3.2.3, in accordance with our previous use of the notation
$E/\phi$.

###  3.5 Syntactic presentation of a glued topos

We need a lemma about testing the property of a geometric morphism to be an
equivalence on an open cover of the target topos. Or rather, we need its
reformulation in terms of models of theories (Corollary 3.5.3 below), saying
that the property of a model to be universal can be tested on an “open cover
of the theory”.

######  Lemma 3.5.1.

Let $f:\mathcal{E}\to\mathcal{F}$ be a geometric morphism and let a cover
$\mathcal{F}=\bigcup_{i\in I}\mathcal{F}_{i}$ by open subtoposes
$\mathcal{F}_{i}=\mathcal{F}_{o(U_{i})}$ be given such that the induced
geometric morphisms $f_{i}:\mathcal{E}_{i}\to\mathcal{F}_{i}$, where
$\mathcal{E}_{i}=\mathcal{E}_{o(f^{*}U_{i})}$, are all equivalences.

${\mathcal{E}_{i}}$${\mathcal{F}_{i}}$${\mathcal{E}}$${\mathcal{F}}$$\scriptstyle{f_{i}}$$\scriptstyle{\simeq}$${\lrcorner}$$\scriptstyle{f}$

Then $f$ is an equivalence.

###### Proof.

The fact that the $\mathcal{F}_{i}$ cover $\mathcal{F}$ means
$1_{\mathcal{F}}=\bigvee_{i\in I}U_{i}$ and, equivalently, the sheafification
functors $a_{U_{i}}:\mathcal{F}\to\mathcal{F}_{i}$ are jointly conservative.
Setting $V_{i}\vcentcolon=f^{*}U_{i}$ we similarly have
$1_{\mathcal{E}}=\bigvee_{i\in I}V_{i}$ since $f^{*}$ preserves colimits. We
will show that the unit $\eta_{f}$ and counit $\varepsilon_{f}$ of the
adjunction $f^{*}\dashv f_{*}$ are isomorphisms by showing that
$a_{U_{i}}\eta_{f}$ and $a_{V_{i}}\varepsilon_{f}$ are isomorphisms for all
$i\in I$. More precisely, if $\eta_{f_{i}}$ and $\varepsilon_{f_{i}}$ are the
unit and counit of ${f_{i}}^{*}\dashv{f_{i}}_{*}$ we will show that
$a_{U_{i}}\eta_{f}$ and $\eta_{f_{i}}a_{U_{i}}$ only differ by an isomorphism
of their codomains $a_{U_{i}}f_{*}f^{*}\cong{f_{i}}_{*}{f_{i}}^{*}a_{U_{i}}$,
and similarly $a_{V_{i}}\varepsilon_{f}$ and $\varepsilon_{f_{i}}a_{V_{i}}$
only differ by an isomorphism of their domains
$a_{V_{i}}f^{*}f_{*}\cong{f_{i}}^{*}{f_{i}}_{*}a_{V_{i}}$.

Recall that $a_{U}:\mathcal{F}\to\mathcal{F}_{o(U)}$ has two fully faithful
adjoints $j_{U}\dashv a_{U}\dashv i_{U}$, where $j_{U}(a_{U}(X))=X\times U$
and $i_{U}(a_{U}(X))=X^{U}$. Thus we have the following functors and
adjunctions

${\mathcal{E}_{o(V)}}$${\mathcal{F}_{o(U)}}$${\mathcal{E}}$${\mathcal{F}\hbox
to0.0pt{,\hss}}$$\scriptstyle{i_{V}}$${\dashv}$$\scriptstyle{a_{V}}$${\dashv}$$\scriptstyle{j_{V}}$$\scriptstyle{f^{*}}$${\dashv}$$\scriptstyle{f_{*}}$$\scriptstyle{i_{U}}$${\dashv}$$\scriptstyle{a_{U}}$${\dashv}$$\scriptstyle{j_{U}}$

where $\varepsilon_{U}:a_{U}i_{U}\to\mathrm{Id}_{\mathcal{F}_{o(U)}}$,
$\tilde{\eta}_{U}:\mathrm{Id}_{\mathcal{F}_{o(U)}}\to a_{U}j_{U}$,
$\varepsilon_{V}:a_{V}i_{V}\to\mathrm{Id}_{\mathcal{E}_{o(V)}}$ and
$\tilde{\eta}_{V}:\mathrm{Id}_{\mathcal{E}_{o(V)}}\to a_{V}j_{V}$ are
isomorphisms. The geometric morphism $\mathcal{E}_{o(V)}\to\mathcal{F}_{o(U)}$
is given by $a_{V}f^{*}j_{U}\dashv a_{U}f_{*}i_{V}$. Our assumption therefore
means that the following two natural transformations (denoted as string
diagrams) are isomorphisms.

$\tilde{\eta}_{U}$$\eta_{f}$$\eta_{V}$$j_{U}$$a_{U}$$f^{*}$$f_{*}$$a_{V}$$i_{V}$
$\tilde{\varepsilon}_{U}$$\varepsilon_{f}$$\varepsilon_{V}$$i_{V}$$a_{V}$$f_{*}$$f^{*}$$a_{U}$$j_{U}$

The only additional ingredient we need is a certain compatibility of $f^{*}$
and $f_{*}$ with the adjunctions $j_{U}\dashv a_{U}$ and $j_{V}\dashv a_{V}$.
Since $f^{*}(X\times U)=f^{*}X\times V$ and
$(\tilde{\varepsilon}_{U})_{X}:X\times U\to X$ and
$(\tilde{\varepsilon}_{V})_{Y}:Y\times V\to Y$ are the projections on the
first factor, we have a natural isomorphism

$\leavevmode\hbox to59.38pt{\vbox
to69.42pt{\pgfpicture\makeatletter\hbox{\hskip
29.81718pt\lower-34.24767pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.42264pt}{0.0pt}\pgfsys@curveto{1.42264pt}{0.7857pt}{0.7857pt}{1.42264pt}{0.0pt}{1.42264pt}\pgfsys@curveto{-0.7857pt}{1.42264pt}{-1.42264pt}{0.7857pt}{-1.42264pt}{0.0pt}\pgfsys@curveto{-1.42264pt}{-0.7857pt}{-0.7857pt}{-1.42264pt}{0.0pt}{-1.42264pt}\pgfsys@curveto{0.7857pt}{-1.42264pt}{1.42264pt}{-0.7857pt}{1.42264pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.55264pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\alpha$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}}{{}}
{{}{}}{{}} {{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{{}}{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{-18.77892pt}{18.77892pt}\pgfsys@curveto{-18.77892pt}{8.38072pt}{-7.35263pt}{7.35263pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.81145pt}{-5.81145pt}{9.38945pt}{-10.56027pt}{9.38945pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{}\pgfsys@moveto{-18.77892pt}{18.77892pt}\pgfsys@curveto{-18.77892pt}{8.38072pt}{-7.35263pt}{7.35263pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.81145pt}{-5.81145pt}{9.38945pt}{-10.56027pt}{9.38945pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.48418pt}{23.3883pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.64568pt}{-28.77023pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{V}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}}{{}}
{{}{}}{{}} {{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{{}}{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{-9.38945pt}{18.77892pt}\pgfsys@curveto{-9.38945pt}{10.56027pt}{-5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{7.35263pt}{-7.35263pt}{18.77892pt}{-8.38072pt}{18.77892pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{}\pgfsys@moveto{-9.38945pt}{18.77892pt}\pgfsys@curveto{-9.38945pt}{10.56027pt}{-5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{7.35263pt}{-7.35263pt}{18.77892pt}{-8.38072pt}{18.77892pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.10648pt}{23.3883pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$j_{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{17.02338pt}{-28.77023pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$j_{V}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{9.38945pt}{18.77892pt}\pgfsys@curveto{9.38945pt}{10.56027pt}{5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{-5.81145pt}{-9.38945pt}{-10.56027pt}{-9.38945pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{9.38945pt}{18.77892pt}\pgfsys@curveto{9.38945pt}{10.56027pt}{5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{-5.81145pt}{-9.38945pt}{-10.56027pt}{-9.38945pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.00333pt}{23.5883pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$f^{*}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.77557pt}{-28.97023pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$f^{*}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\quad\text{with}\quad\leavevmode\hbox
to64.02pt{\vbox to73.41pt{\pgfpicture\makeatletter\hbox{\hskip
27.31474pt\lower-46.09389pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.42264pt}{0.0pt}\pgfsys@curveto{1.42264pt}{0.7857pt}{0.7857pt}{1.42264pt}{0.0pt}{1.42264pt}\pgfsys@curveto{-0.7857pt}{1.42264pt}{-1.42264pt}{0.7857pt}{-1.42264pt}{0.0pt}\pgfsys@curveto{-1.42264pt}{-0.7857pt}{-0.7857pt}{-1.42264pt}{0.0pt}{-1.42264pt}\pgfsys@curveto{0.7857pt}{-1.42264pt}{1.42264pt}{-0.7857pt}{1.42264pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.55264pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\alpha$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{20.20155pt}{-28.16838pt}\pgfsys@curveto{20.20155pt}{-27.38268pt}{19.56462pt}{-26.74574pt}{18.77892pt}{-26.74574pt}\pgfsys@curveto{17.99321pt}{-26.74574pt}{17.35628pt}{-27.38268pt}{17.35628pt}{-28.16838pt}\pgfsys@curveto{17.35628pt}{-28.95409pt}{17.99321pt}{-29.59102pt}{18.77892pt}{-29.59102pt}\pgfsys@curveto{19.56462pt}{-29.59102pt}{20.20155pt}{-28.95409pt}{20.20155pt}{-28.16838pt}\pgfsys@closepath\pgfsys@moveto{18.77892pt}{-28.16838pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{18.77892pt}{-28.16838pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{13.74567pt}{-40.54642pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\tilde{\varepsilon}_{V}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}{}{}{{}}{} {{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{}{{}{}{}{{}}{{{{}{}{}{}}} {{}{}{}{}}}}{}
{} {} {} {}{} {{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{-18.77892pt}{18.77892pt}\pgfsys@curveto{-18.77892pt}{8.38072pt}{-7.35263pt}{7.35263pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.8115pt}{-5.8115pt}{9.38956pt}{-10.56036pt}{9.38956pt}{-18.77907pt}\pgfsys@curveto{9.38956pt}{-23.96478pt}{13.59329pt}{-28.16852pt}{18.779pt}{-28.16852pt}\pgfsys@curveto{23.96472pt}{-28.16852pt}{28.16846pt}{-23.96478pt}{28.16846pt}{-18.77907pt}\pgfsys@curveto{28.16847pt}{-5.525pt}{9.37206pt}{-9.37206pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{5.81145pt}{-9.38945pt}{10.56027pt}{-9.38945pt}{18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{}\pgfsys@moveto{-18.77892pt}{18.77892pt}\pgfsys@curveto{-18.77892pt}{8.38072pt}{-7.35263pt}{7.35263pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.8115pt}{-5.8115pt}{9.38956pt}{-10.56036pt}{9.38956pt}{-18.77907pt}\pgfsys@curveto{9.38956pt}{-23.96478pt}{13.59329pt}{-28.16852pt}{18.779pt}{-28.16852pt}\pgfsys@curveto{23.96472pt}{-28.16852pt}{28.16846pt}{-23.96478pt}{28.16846pt}{-18.77907pt}\pgfsys@curveto{28.16847pt}{-5.525pt}{9.37206pt}{-9.37206pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{5.81145pt}{-9.38945pt}{10.56027pt}{-9.38945pt}{18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{}{}{{}}{} {{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{{{}}{}{}{}{{}}{}}
{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{9.38945pt}{18.77892pt}\pgfsys@curveto{9.38945pt}{10.56027pt}{5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{-5.81145pt}{-9.38945pt}{-10.56027pt}{-9.38945pt}{-18.77892pt}\pgfsys@lineto{-9.38945pt}{-37.55806pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{9.38945pt}{18.77892pt}\pgfsys@curveto{9.38945pt}{10.56027pt}{5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{-5.81145pt}{-9.38945pt}{-10.56027pt}{-9.38945pt}{-18.77892pt}\pgfsys@lineto{-9.38945pt}{-37.55806pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}=\leavevmode\hbox
to52.54pt{\vbox to54.63pt{\pgfpicture\makeatletter\hbox{\hskip
17.92528pt\lower-27.31474pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.42264pt}{0.0pt}\pgfsys@curveto{1.42264pt}{0.7857pt}{0.7857pt}{1.42264pt}{0.0pt}{1.42264pt}\pgfsys@curveto{-0.7857pt}{1.42264pt}{-1.42264pt}{0.7857pt}{-1.42264pt}{0.0pt}\pgfsys@curveto{-1.42264pt}{-0.7857pt}{-0.7857pt}{-1.42264pt}{0.0pt}{-1.42264pt}\pgfsys@curveto{0.7857pt}{-1.42264pt}{1.42264pt}{-0.7857pt}{1.42264pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.99483pt}{-12.37787pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\tilde{\varepsilon}_{U}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}{} {}{}{}{{}{}{}{{}}{{{{}{}{}{}}} {{}{}{}{}}}}{} {} {} {} {}{}
{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{-9.38945pt}{18.77892pt}\pgfsys@lineto{-9.38945pt}{9.38945pt}\pgfsys@curveto{-9.38945pt}{4.20374pt}{-5.18571pt}{0.0pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.18571pt}{0.0pt}{9.38945pt}{4.20374pt}{9.38945pt}{9.38945pt}\pgfsys@lineto{9.38945pt}{18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{}\pgfsys@moveto{-9.38945pt}{18.77892pt}\pgfsys@lineto{-9.38945pt}{9.38945pt}\pgfsys@curveto{-9.38945pt}{4.20374pt}{-5.18571pt}{0.0pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.18571pt}{0.0pt}{9.38945pt}{4.20374pt}{9.38945pt}{9.38945pt}\pgfsys@lineto{9.38945pt}{18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} {}{{}}{} {}{}{}{}{{{}{}}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{18.77892pt}{18.77892pt}\pgfsys@lineto{18.77892pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{18.77892pt}{18.77892pt}\pgfsys@lineto{18.77892pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.51192pt}{-3.1514pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$f^{*}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
For $f_{*}$ the situation is slightly different as $f_{*}(V)\neq U$, but we
have an arrow $(\eta_{f})_{U}:U\to f_{*}(V)$ which becomes an isomorphism
after applying $a_{U}$ (since $f_{*}(V)\times U=U$). Thus we have an
isomorphism

$\leavevmode\hbox to75.95pt{\vbox
to68.11pt{\pgfpicture\makeatletter\hbox{\hskip 29.8557pt\lower-34.24767pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.42264pt}{0.0pt}\pgfsys@curveto{1.42264pt}{0.7857pt}{0.7857pt}{1.42264pt}{0.0pt}{1.42264pt}\pgfsys@curveto{-0.7857pt}{1.42264pt}{-1.42264pt}{0.7857pt}{-1.42264pt}{0.0pt}\pgfsys@curveto{-1.42264pt}{-0.7857pt}{-0.7857pt}{-1.42264pt}{0.0pt}{-1.42264pt}\pgfsys@curveto{0.7857pt}{-1.42264pt}{1.42264pt}{-0.7857pt}{1.42264pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.81189pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\beta$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}}{{}}
{{}{}}{{}} {{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{{}}{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{-18.77892pt}{18.77892pt}\pgfsys@curveto{-18.77892pt}{8.38072pt}{-7.35263pt}{7.35263pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.81145pt}{-5.81145pt}{9.38945pt}{-10.56027pt}{9.38945pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{}\pgfsys@moveto{-18.77892pt}{18.77892pt}\pgfsys@curveto{-18.77892pt}{8.38072pt}{-7.35263pt}{7.35263pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.81145pt}{-5.81145pt}{9.38945pt}{-10.56027pt}{9.38945pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.52269pt}{23.3883pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{V}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.68419pt}{-28.77023pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}}{{}}
{{}{}}{{}} {{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{{}}{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{-9.38945pt}{18.77892pt}\pgfsys@curveto{-9.38945pt}{10.56027pt}{-5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{7.35263pt}{-7.35263pt}{18.77892pt}{-8.38072pt}{18.77892pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{}\pgfsys@moveto{-9.38945pt}{18.77892pt}\pgfsys@curveto{-9.38945pt}{10.56027pt}{-5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{7.35263pt}{-7.35263pt}{18.77892pt}{-8.38072pt}{18.77892pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.14499pt}{23.3883pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$j_{V}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{17.06189pt}{-28.77023pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$j_{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{9.38945pt}{18.77892pt}\pgfsys@curveto{9.38945pt}{10.56027pt}{5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{-5.81145pt}{-9.38945pt}{-10.56027pt}{-9.38945pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{9.38945pt}{18.77892pt}\pgfsys@curveto{9.38945pt}{10.56027pt}{5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{-5.81145pt}{-9.38945pt}{-10.56027pt}{-9.38945pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.00333pt}{23.5883pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$f_{*}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.77557pt}{-28.97023pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$f_{*}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{37.55785pt}{18.77892pt}\pgfsys@curveto{37.55785pt}{3.1644pt}{17.96188pt}{0.0pt}{2.34735pt}{0.0pt}\pgfsys@curveto{17.96188pt}{0.0pt}{37.55785pt}{-3.1644pt}{37.55785pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{}\pgfsys@moveto{37.55785pt}{18.77892pt}\pgfsys@curveto{37.55785pt}{3.1644pt}{17.96188pt}{0.0pt}{2.34735pt}{0.0pt}\pgfsys@curveto{17.96188pt}{0.0pt}{37.55785pt}{-3.1644pt}{37.55785pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{32.69786pt}{23.3883pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{32.69786pt}{-28.77023pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\quad\text{with}\quad\leavevmode\hbox
to73.41pt{\vbox to73.41pt{\pgfpicture\makeatletter\hbox{\hskip
27.31474pt\lower-46.09389pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.42264pt}{0.0pt}\pgfsys@curveto{1.42264pt}{0.7857pt}{0.7857pt}{1.42264pt}{0.0pt}{1.42264pt}\pgfsys@curveto{-0.7857pt}{1.42264pt}{-1.42264pt}{0.7857pt}{-1.42264pt}{0.0pt}\pgfsys@curveto{-1.42264pt}{-0.7857pt}{-0.7857pt}{-1.42264pt}{0.0pt}{-1.42264pt}\pgfsys@curveto{0.7857pt}{-1.42264pt}{1.42264pt}{-0.7857pt}{1.42264pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.81189pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\beta$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{20.20155pt}{-28.16838pt}\pgfsys@curveto{20.20155pt}{-27.38268pt}{19.56462pt}{-26.74574pt}{18.77892pt}{-26.74574pt}\pgfsys@curveto{17.99321pt}{-26.74574pt}{17.35628pt}{-27.38268pt}{17.35628pt}{-28.16838pt}\pgfsys@curveto{17.35628pt}{-28.95409pt}{17.99321pt}{-29.59102pt}{18.77892pt}{-29.59102pt}\pgfsys@curveto{19.56462pt}{-29.59102pt}{20.20155pt}{-28.95409pt}{20.20155pt}{-28.16838pt}\pgfsys@closepath\pgfsys@moveto{18.77892pt}{-28.16838pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{18.77892pt}{-28.16838pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{13.78418pt}{-40.54642pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\tilde{\varepsilon}_{U}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}{}{}{{}}{} {{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{}{{}{}{}{{}}{{{{}{}{}{}}} {{}{}{}{}}}}{}
{} {} {} {}{} {{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{-18.77892pt}{18.77892pt}\pgfsys@curveto{-18.77892pt}{8.38072pt}{-7.35263pt}{7.35263pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.8115pt}{-5.8115pt}{9.38956pt}{-10.56036pt}{9.38956pt}{-18.77907pt}\pgfsys@curveto{9.38956pt}{-23.96478pt}{13.59329pt}{-28.16852pt}{18.779pt}{-28.16852pt}\pgfsys@curveto{23.96472pt}{-28.16852pt}{28.16846pt}{-23.96478pt}{28.16846pt}{-18.77907pt}\pgfsys@curveto{28.16847pt}{-5.525pt}{9.37206pt}{-9.37206pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{5.81145pt}{-9.38945pt}{10.56027pt}{-9.38945pt}{18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{}\pgfsys@moveto{-18.77892pt}{18.77892pt}\pgfsys@curveto{-18.77892pt}{8.38072pt}{-7.35263pt}{7.35263pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.8115pt}{-5.8115pt}{9.38956pt}{-10.56036pt}{9.38956pt}{-18.77907pt}\pgfsys@curveto{9.38956pt}{-23.96478pt}{13.59329pt}{-28.16852pt}{18.779pt}{-28.16852pt}\pgfsys@curveto{23.96472pt}{-28.16852pt}{28.16846pt}{-23.96478pt}{28.16846pt}{-18.77907pt}\pgfsys@curveto{28.16847pt}{-5.525pt}{9.37206pt}{-9.37206pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{5.81145pt}{-9.38945pt}{10.56027pt}{-9.38945pt}{18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{}{}{{}}{} {{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{{{}}{}{}{}{{}}{}}
{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{9.38945pt}{18.77892pt}\pgfsys@curveto{9.38945pt}{10.56027pt}{5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{-5.81145pt}{-9.38945pt}{-10.56027pt}{-9.38945pt}{-18.77892pt}\pgfsys@lineto{-9.38945pt}{-37.55806pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{9.38945pt}{18.77892pt}\pgfsys@curveto{9.38945pt}{10.56027pt}{5.81145pt}{5.81145pt}{0.0pt}{0.0pt}\pgfsys@curveto{-5.81145pt}{-5.81145pt}{-9.38945pt}{-10.56027pt}{-9.38945pt}{-18.77892pt}\pgfsys@lineto{-9.38945pt}{-37.55806pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{}{}{{}}{}{{}}{}{}{}
{{}{}}{{}} {{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{{}}{}{}{} {{}{}}{{}}
{{{}}{{}}}{{}}{{{}}{{}}}{}{{}}{}{}{}{{{}}{}{}{}{{}}{}}
{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{37.55785pt}{18.77892pt}\pgfsys@curveto{37.55785pt}{3.1644pt}{17.96188pt}{0.0pt}{2.34735pt}{0.0pt}\pgfsys@curveto{17.96188pt}{0.0pt}{37.55785pt}{-3.1644pt}{37.55785pt}{-18.77892pt}\pgfsys@lineto{37.55785pt}{-37.55806pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{}\pgfsys@moveto{37.55785pt}{18.77892pt}\pgfsys@curveto{37.55785pt}{3.1644pt}{17.96188pt}{0.0pt}{2.34735pt}{0.0pt}\pgfsys@curveto{17.96188pt}{0.0pt}{37.55785pt}{-3.1644pt}{37.55785pt}{-18.77892pt}\pgfsys@lineto{37.55785pt}{-37.55806pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}=\leavevmode\hbox
to72.07pt{\vbox to54.63pt{\pgfpicture\makeatletter\hbox{\hskip
17.92528pt\lower-27.31474pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.42264pt}{0.0pt}\pgfsys@curveto{1.42264pt}{0.7857pt}{0.7857pt}{1.42264pt}{0.0pt}{1.42264pt}\pgfsys@curveto{-0.7857pt}{1.42264pt}{-1.42264pt}{0.7857pt}{-1.42264pt}{0.0pt}\pgfsys@curveto{-1.42264pt}{-0.7857pt}{-0.7857pt}{-1.42264pt}{0.0pt}{-1.42264pt}\pgfsys@curveto{0.7857pt}{-1.42264pt}{1.42264pt}{-0.7857pt}{1.42264pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.99483pt}{-12.37787pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\tilde{\varepsilon}_{U}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}{} {}{}{}{{}{}{}{{}}{{{{}{}{}{}}} {{}{}{}{}}}}{} {} {} {} {}{}
{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{-9.38945pt}{18.77892pt}\pgfsys@lineto{-9.38945pt}{9.38945pt}\pgfsys@curveto{-9.38945pt}{4.20374pt}{-5.18571pt}{0.0pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.18571pt}{0.0pt}{9.38945pt}{4.20374pt}{9.38945pt}{9.38945pt}\pgfsys@lineto{9.38945pt}{18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{}\pgfsys@moveto{-9.38945pt}{18.77892pt}\pgfsys@lineto{-9.38945pt}{9.38945pt}\pgfsys@curveto{-9.38945pt}{4.20374pt}{-5.18571pt}{0.0pt}{0.0pt}{0.0pt}\pgfsys@curveto{5.18571pt}{0.0pt}{9.38945pt}{4.20374pt}{9.38945pt}{9.38945pt}\pgfsys@lineto{9.38945pt}{18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} {}{{}}{} {}{}{}{}{{{}{}}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{18.77892pt}{18.77892pt}\pgfsys@lineto{18.77892pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{18.77892pt}{18.77892pt}\pgfsys@lineto{18.77892pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.51192pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$f_{*}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}{}{}{{{}{}}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{17.07166pt}\pgfsys@invoke{
}\pgfsys@stroke@opacity{0}\pgfsys@invoke{
}\pgfsys@fill@opacity{0}\pgfsys@invoke{
}{}\pgfsys@moveto{37.55785pt}{18.77892pt}\pgfsys@lineto{37.55785pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{}\pgfsys@moveto{37.55785pt}{18.77892pt}\pgfsys@lineto{37.55785pt}{-18.77892pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{41.09085pt}{-1.1961pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$a_{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
Now we can piece together isomorphisms reducing to $a_{U}\eta_{f}$ and
$a_{V}\varepsilon_{f}$ respectively. (Start by introducing a new squiggle
involving $\tilde{\varepsilon}_{V}$ and $\tilde{\eta}_{V}$ below
$\tilde{\eta}_{V}^{-1}$ in the first diagram, and a new squiggle involving
$\eta_{V}$ and $\varepsilon_{V}$ above $\varepsilon_{V}^{-1}$ in the second
diagram.)

$\leavevmode\hbox to168.36pt{\vbox
to215.75pt{\pgfpicture\makeatletter\hbox{\hskip
75.31569pt\lower-197.82947pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}
\par{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}{}{{}}{}{{}}{{}}
{{{}}}{{{}}}{{{{}}{{}}}}{{}}{{{
}}}\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.42264pt}{0.0pt}\pgfsys@curveto{1.42264pt}{0.7857pt}{0.7857pt}{1.42264pt}{0.0pt}{1.42264pt}\pgfsys@curveto{-0.7857pt}{1.42264pt}{-1.42264pt}{0.7857pt}{-1.42264pt}{0.0pt}\pgfsys@curveto{-1.42264pt}{-0.7857pt}{-0.7857pt}{-1.42264pt}{0.0pt}{-1.42264pt}\pgfsys@curveto{0.7857pt}{-1.42264pt}{1.42264pt}{-0.7857pt}{1.42264pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.99483pt}{7.06897pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\tilde{\eta}_{U}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.42264pt}{-18.77892pt}\pgfsys@curveto{1.42264pt}{-17.99321pt}{0.7857pt}{-17.35628pt}{0.0pt}{-17.35628pt}\pgfsys@curveto{-0.7857pt}{-17.35628pt}{-1.42264pt}{-17.99321pt}{-1.42264pt}{-18.77892pt}\pgfsys@curveto{-1.42264pt}{-19.56462pt}{-0.7857pt}{-20.20155pt}{0.0pt}{-20.20155pt}\pgfsys@curveto{0.7857pt}{-20.20155pt}{1.42264pt}{-19.56462pt}{1.42264pt}{-18.77892pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-18.77892pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-18.77892pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.15488pt}{-10.59004pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\eta_{f}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.42264pt}{-37.55785pt}\pgfsys@curveto{1.42264pt}{-36.77214pt}{0.7857pt}{-36.13521pt}{0.0pt}{-36.13521pt}\pgfsys@curveto{-0.7857pt}{-36.13521pt}{-1.42264pt}{-36.77214pt}{-1.42264pt}{-37.55785pt}\pgfsys@curveto{-1.42264pt}{-38.34355pt}{-0.7857pt}{-38.98048pt}{0.0pt}{-38.98048pt}\pgfsys@curveto{0.7857pt}{-38.98048pt}{1.42264pt}{-38.34355pt}{1.42264pt}{-37.55785pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-37.55785pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-37.55785pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.7382pt}{-30.45798pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\eta_{V}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{