4/4 Classifying toposes of geometric theories
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 31 | |
| Author | ||
| Contributors | ||
| License | CC Attribution 3.0 Unported: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/54083 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
|
Toposes online, 202131 / 31
2
10
11
12
20
21
25
26
27
28
29
00:00
TopologyEquivalence relationQuadratic formTheoryGeometryAxiomNetwork topologyAbelian categoryLaurent seriesSheaf (mathematics)Algebraic numberRelation <Mathematik>Term (mathematics)TheoremPoint (geometry)FunktorLimit (category theory)Element (mathematics)Musical ensembleTopostheoriePresentation of a groupGrothendieck topologyCategory of beingObject (grammar)Network topologyTerm (mathematics)TheoryGeometryDifferent (Kate Ryan album)LogicPoint (geometry)Linear algebraModulformAxiomFunctional (mathematics)Theory of relativityElement (mathematics)Quadratic formAssociative propertySocial classDirected graphStudent's t-testSigma-algebraQuotientPressureInvariant (mathematics)Order (biology)Proof theoryKörper <Algebra>Direction (geometry)Product (business)Ring (mathematics)Module (mathematics)ResultantPrime idealVector spaceTranslation (relic)MereologyArithmetic meanShift operatorConsistencyMultiplication signWater vaporMetric systemEqualiser (mathematics)Special unitary groupGroup actionGenetic programmingReliefTime zoneFiber bundleSpacetimeSummierbarkeitSeries (mathematics)Hill differential equationReal numberRegular graphNeighbourhood (graph theory)General relativityGroup representationDistanceComputer animation
09:12
TheoremAbelian categoryPoint (geometry)Equivalence relationFunktorElement (mathematics)Limit (category theory)Laurent seriesSheaf (mathematics)TheoryModel theoryPropositional formulaComplete metric spaceMorphismusModel theoryGroup representationCategory of beingIdentical particlesStress (mechanics)Linear algebraFinitismusRing (mathematics)Set theoryFamilyPoint (geometry)Generating set of a groupMorphismusPropositional formulaMereologyTopostheorieFunktorOrder (biology)Object (grammar)Vector spaceGroup actionPresentation of a groupElement (mathematics)Network topologyExtension (kinesiology)TheoremInvariant (mathematics)Term (mathematics)TheoryIdempotentAlgebraic structureEquivalence relationDependent and independent variablesCuboidOrientation (vector space)CausalityComplete metric spaceAssociative propertyMusical ensembleSocial classTessellationExpected valueLimit (category theory)WaveMultiplication signComplex (psychology)FrequencyOpen setTable (information)Game theoryShooting methodSpecial unitary groupHeegaard splittingFiber (mathematics)Sign (mathematics)Different (Kate Ryan album)Process (computing)2 (number)Sheaf (mathematics)Event horizonNumber theoryPlane (geometry)Shift operatorLogicTrailDivisorComputer animation
18:08
GeometryQuadratic formTheoryAbelian categoryQuotientSheaf (mathematics)Network topologyAxiom of choiceNatural numberCubeFunktorObject (grammar)FamilyMorphismusState of matterLogicTopostheorieCanonical ensembleTheoryShift operatorDifferent (Kate Ryan album)Presentation of a groupGeometryCorrespondence (mathematics)Model theoryNetwork topologyCategory of beingMortality rateSocial classGeometryComputer programmingHand fanObject (grammar)Prime idealGame theoryArithmetic meanGroup actionEstimationFamilyGrothendieck topologyWell-formed formulaMorphismusFunktorUniqueness quantificationEquivalence relationAxiomQuotientQuadratic formSet theoryComputer animation
22:34
Representation theorySieve of EratosthenesWell-formed formulaNetwork topologyAbelian categoryGeometryTheoryQuadratic formPrice indexLemma (mathematics)Sheaf (mathematics)Correspondence (mathematics)Object (grammar)Complete metric spaceHeegaard splittingModel theoryTheoremCovering spacePole (complex analysis)Hydraulic jumpCategory of beingObject (grammar)Content (media)FamilyIdentical particlesProjektive GeometrieTheoremShift operatorPresentation of a groupKörper <Algebra>Real numberStress (mechanics)Heegaard splittingMusical ensembleNear-ringGame theoryMoving averageMultiplication signTerm (mathematics)Arithmetic meanState of matterLine (geometry)Well-formed formulaNetwork topologyTheoryFigurate numberRing (mathematics)Connected spaceGrothendieck topologyRepresentation theoryPerturbation theoryMorley's categoricity theoremGeometryLogicModel theoryCorrespondence (mathematics)GeometryBijectionProof theoryComplete metric spaceTopostheoriePrice indexSlide ruleMorphismusResultantInvariant (mathematics)PressureComputer animation
29:37
TheoremTheoryGeometryQuadratic formCondition numberSheaf (mathematics)Model theoryElement (mathematics)FamilyWell-formed formulaCorrespondence (mathematics)MorphismusMany-sorted logicSquare numberSubsetNatural numberInsertion lossSet theoryMatching (graph theory)Model theoryShift operatorModulformCategory of beingLimit (category theory)Condition numberFamilyGroup actionSeries (mathematics)OrbitNetwork topologyForcing (mathematics)EstimationWaveStress (mechanics)Direction (geometry)Well-formed formulaElement (mathematics)Axiom of choiceGeometrySigma-algebraAnnihilator (ring theory)Product (business)Thomas BayesHill differential equationMortality rateProfil (magazine)Social classSphereArithmetic meanPresentation of a groupSpecial unitary groupHand fanMetric systemProof theoryUniverse (mathematics)ForestMultiplication signNear-ringPower (physics)TheoryEquivalence relationMany-sorted logicAssociative propertyDivisorAutocovarianceGame theorySequenceTopostheorieDirected graphSubsetVariable (mathematics)Functional (mathematics)Representation theoryCorrespondence (mathematics)GeometryTerm (mathematics)FunktorQuadratic formEvent horizonTheory of relativityMorphismusComputer animation
36:41
Many-sorted logicMorphismusModel theorySquare numberWell-formed formulaSubsetDirected setEquivalence relationObject (grammar)TopostheorieQuotientNetwork topologyRepresentation theoryTheoryNetwork topologyPresentation of a groupWell-formed formulaRight angleLogicComplex (psychology)TheoryPoint cloudRepresentation theoryMortality rateCategory of beingGame theoryNatural numberEquivalence relationGeometryMathematicsMereologyRankingProof theoryChemical equationDifferent (Kate Ryan album)Combinatory logicSign (mathematics)SpacetimeCompact spaceGroup representationPrincipal idealExistenceSummierbarkeitModel theoryPower (physics)Multiplication signWave packetReal numberMany-sorted logicVarianceObject (grammar)TheoremForcing (mathematics)1 (number)Direction (geometry)Figurate numberProcess (computing)Drop (liquid)Shift operatorProjektive GeometrieGreatest elementPrime idealLine (geometry)Hydraulic jumpGeometryTerm (mathematics)State of matterUniverse (mathematics)Musical ensembleMatching (graph theory)ForestMathematical singularityString theoryCartesian coordinate systemRing (mathematics)Social classStress (mechanics)ModulformSpecial unitary groupEstimationFamilyMatrix (mathematics)SequenceCorrespondence (mathematics)ThetafunktionMorphismusFunctional (mathematics)TopostheorieQuotientGrothendieck topologyProduct (business)Associative propertyInvariant (mathematics)Set theoryResultantFunktionalanalysisExistential quantificationHypothesisCondensationComputer animation
Transcript: English(auto-generated)
00:16
We just explained that this notion of Grothendieck topology is so rich that it gives another
00:29
formulation for the problems of probability in geometric logic. So this is really an incredible result. And it makes all the more important the following question.
00:45
For any geometric theory you are interested in, how to present its classifying topos? So you have the associative classifying topos et, and you wonder how to present it in terms of sites.
01:04
Because any presentation in terms of sites, in terms of topology j or some category c, will give you a new translation of the problems of probability in t in terms of topologies on c
01:22
which contain a j. So the first remark we can make is that for any topos there are so many presentations in terms of sites that in fact it is not even a set. This is just because e itself is not a small category, except the trivial topos with only
01:49
one object and one role. All of them are topos, not small categories. And I remind you that any full subcategory of e which is small and generating gives rise to a presentation.
02:05
So there are incredibly ways to present it. It is not even a set. What we have done so far is to say that of course there is a presentation of the
02:21
classifying topos in terms of the syntactic category on those with a syntactic topology. But this presentation of course is not always the best. In particular it is a presentation
02:40
which is syntactic in nature. So it is very close to logic and it would be probably more telling in many instances to have presentations in terms of sites cj which are not
03:04
so closely related to the linguistic presentation of t. Here I should also mention that in fact the classifying topos of a theory
03:21
in general has several presentations defined even in syntactic terms. There is a syntactic geometric category we already defined, but there also exist other syntactic presentations. For instance, if the theory is algebraic, there is a Cartesian, there is a Cartesian
03:47
syntactic category, a regular syntactic category, a coherent syntactic category on top of different types of presentations. And maybe I can also mention that next week there will be a talk by Yoshua Vadlek, a first year PhD student of Bolivia, who will present in particular
04:07
a new way of constructing the classifying topos of theories which he has found. This also is very interesting, but by now we consider in general the question of presentation
04:23
of a theory in terms of that. So the first remark we can make is that of course if we have such a presentation, then the topos i, equivalent to c at j, will be a topos of the topos c at
04:44
the topos of preshives on c. And the topos of preshives on c, as any topos, can be presented as the classifying topos of some theory t prime. And then, because i is a topos of c at,
05:02
t will appear as a quotient theory of t prime. So we can try to play in this direction. So for that we need a definition, you see that the consideration of preshif toposes and the fact that any topos by definition is a subtopos of a preshif topos. So this
05:26
consideration leads to the following definition. Geometric theory is called of preshif type when its classifying topos can be written as a topos of preshives on a small category.
05:43
Okay, so of course not all toposes verify this property, only parts of the two only, so this is a particular class of toposes. And maybe I should also mention that
06:00
when you have a preshif topos like that, c at, it can be equivalent to some other presentations, so c at c prime at j prime with some non-trivial j prime. So you see, you can define a topos through a non-discrete site and nevertheless get
06:25
the properties that this topos is equivalent to the topos of pressures on some category. It is a quite subtle question. So there are examples of theories which are of preshif type,
06:42
in fact I shall come back to that later, but I immediately state a few examples. First, in any signature sigma you can consider the so-called empty theory, which is a theory without axioms. And then it is a general fact that this theory is of preshif type.
07:07
Another example of another very important class of preshif type theories is a class of algebraic theories. So what is an algebraic theory? It is a theory whose signature has only source
07:22
and function symbols, no relation symbol, and whose axioms all have the form true implies an equality between terms. So if you think for instance about the theory of rules, what are the axioms? There is associativity of multiplication, the fact that the element one
07:46
is a unit, the fact that g is a product of g and g minus one in indian direction is equal to one, so all of these are equalities between terms. It is the same for the theory of rings,
08:01
of modules of rings or vector spaces of our field and so on. So here I am saying that all algebraic theories have preshif type. In fact it is not an obvious fact, it requires a proof.
08:21
Okay, and then what I want to do in the following minutes is to study in general preshif type theories. So for this, first I consider toposies of preshif. Let's consider a topos E which is a topos of preshif and some categories C.
08:45
In order to understand better the relationship between E and C, we shall consider an invariant of the topos under consideration which is the category of its points.
09:02
So let's consider the category of points of C hat. Of course the point of C hat is given by Diaconess-Kuhs equivalence and in that way you prove that the category of points of C hat
09:25
is equivalent to the category of functors from C to set which verifies the two equivalent properties. So first the category of its elements, which means the category of objects of
09:44
X, endowed with an element of P of X, so this category is filtering. And the second equivalent property is the fact that this functor can be written as a filtering co-limit
10:01
of representable functors. So in particular we get that any representable functor defines the point of C hat. So as a consequence of that we get that the category of points of C hat is the hand compression, the hand category built on the opposite category of C. So you see that
10:29
in this way the category of points of C hat is computed from C in a quite concrete way. This is the hand category, the hand compression of the opposite of C.
10:45
Okay, so this theorem can be proved. And of course there is a corollary. By now if we have precious type theory, good classifying topos can be written as a topos of precious on C hat,
11:02
then we get that the category of models of set theoretic models of T is equivalent to the hand category of C opposite, to the hand compression of C opposite. So in order to make that more clear, we just draw the bridge we are considering.
11:28
So here the invariant under consideration is the category of points of the classifying topos. And the classifying topos is presented in two different ways. On one side from a
11:42
on the other side from the category C, under with a discrete topology. And so you compute the category of points on the two sides. On one side by definition of the classifying topos, it is a category of set theoretic models. And on the other side,
12:02
according to our previous theorem, we get the hand compression of the opposite category of C. So this means in particular that the hand category of C op is determined by T up to equivalence.
12:21
So by now we can ask to which extent it is possible to recover C from the topos C hat. So far what we have recovered is the hand compression of C op. We did not recover C. So we may wonder whether it is possible to fully recover C or not.
12:43
So in order to answer this question, we have to introduce the following definition. So let's consider a prescient type theory. Let's consider a set theoretic model M, an object of the category of set theoretic models. And then we say that this model is
13:03
finitely presentable if the covariant functor associated on the category of set theoretic models respects filtering co-limits. And you can check that, for instance, if you think about models
13:27
of algebraic theories such as groups, rings, and things like that, then the definition of finitely presentable really corresponds to finitely presented groups,
13:42
which means groups which are defined by your finite family of generators and relations, or rings which are defined by your finite family of generators and relations. And the same for all type of algebraic structures. So this definition really corresponds to what we
14:01
have in mind, but you see that this is a categorical definition on the category of set theoretic models. And this definition singles out part of the models. Okay, so we can introduce in this category of set theoretic models the full subcategory of models which
14:22
are finitely presentable. And then we have the following proposition. So let's consider a theory T, which is of impressive type, so that the category of its set theoretic models is hand-compression of C-HOP. Yes, you see I have written
14:47
hand of C-HOP hat, I should have removed the hat. Okay, and by now let's consider a model. And so the proposition tells us that such a model is presentable if and only if it is
15:17
of C-HOP, and the pair of morphisms P and I whose composite is the identity of M,
15:26
and you see this is a pair of morphisms from between M and the representable functor associated to X. So this composition tells us that the finitely presentable models
15:47
are exactly objects in the hand-compression which are retracts of representable objects. But this has a name in category theory. When you start from an arbitrary category and you add
16:07
to these categories all the retracts, which means you add an image of P for any idempotent element P. So this is the carubic compression. This construction was introduced
16:22
by carubic, and so by now this means that the category of set theoretic models of T which are finitely presentable is the carubic compression of the category C opposite.
16:41
And if we denote by M this carubic compression, so this is a category of finitely presentable models, we get that the classifying topos of T is equivalent to the topos of preshives
17:03
on the opposite category of M. And we also get that any set theoretic model is a filtering collimate of finitely presentable models. So for instance, any group is a filtering collimate of finitely presentable groups of groups which are defined by a finite family
17:26
of generators and relations, and the same for rings, for vector spaces, and for any type of algebraic structure. So here we see that when preshives type theory T has its associated
17:47
classifying topos presented as a topos of preshives on term C, then C is almost determined by T. It is determined by T up to carubic compression. Okay, and by now
18:08
we can apply that, begin to apply that to the problem of constructing of presenting the classifying topos of a theory. So it starts from a theory, geometric theory T
18:27
on the signature sigma. What we want to do is to construct a preshive-type theory T prime such that T is a quotient of T prime. So suppose we are able to do that, we just
18:43
add them to T, possibly some other thoughts, some other functions, some other facts. No, no, no, we don't, excuse me, we don't change the language, but we remove some of the axioms.
19:02
Okay, we want T to appear as a quotient of T prime. So T prime will have the same language but less axioms than T. And we would want to remove enough axioms so that T prime becomes a preshive-type. And suppose by now that it is done, then we can
19:23
consider the category M of finitely presentable set theoretic models of T prime. And then we get that the classifying topos of T prime would be equivalent to the topos of
19:42
preshives on the opposite of M. And then according to the correspondence between quotient theories and topologies, there would be a unique topology J on the opposite of M
20:04
such that the classifying topos of T is equivalent to the topos associated to the opposite of M endowed with a topology J. Okay, so if we want to realize this program, we see that
20:30
we need criteria for deciding whether geometric theory T prime is of preshive type or not.
20:43
So here I am going to present in fact two different criteria. First criterion, which is purely syntactic, which is a criterion written in the language of logic. And the second criterion, which is a criterion about the special relationship
21:08
of syntax and semantics in the case of preshive theories. So here I begin with the first purely syntactic criterion.
21:20
So for that, I consider an arbitrary geometric theory T together with its classifying topos associated to the syntactic category endowed with a syntactic topology. And let's consider the canonical functor from the syntactic category to the classifying topos.
21:41
And we already said that this canonical functor N is fully faithful. By now, we recall that the object of city by definition are geometric formulas. The morphisms of city are geometric formulas which are tip-provably functional
22:02
up to tip-provable equivalents. And lastly, the GT-governing families are families whose families of morphisms whose unions of images is equal to everything.
22:24
Okay, so I just recall that and by now introduce the following definition. An object of a topos is called irreducible if any globally epimorphic family from a family of objects to this object are the splitting. So this means that there
22:47
should exist an index I naught in the list of index of the family such that the projection from E I naught to E are the splitting, which means there is a morphism from E to E I naught
23:04
whose composite with the projection is the identity of E. So if any globally epimorphic family in the topos verifies this property, we say that the object E is irreducible.
23:24
So by now, we can translate this property in the language of sites. So if we have a small category C on the topology J, we shall say an object X of C is irreducible with respect to the topology J if it's only J covering C is a maximal C.
23:53
And lastly, if we apply this general property to the particular case of the syntactic category
24:04
of geometric derivative, we get the following definition. Geometric formula phi of X is called irreducible if it is irreducible as an object of the category C T with respect to the topology
24:22
J T. And here we can remark that of course this definition we have just given in a geometric language in categorical language can be translated into the language of probability
24:43
because we just make explicit what it means to be a covering family in the syntactic category, what it means to be a morphism. And so here I have written the meaning in terms of probability.
25:04
So you will see that in the slides. So here the remark is complete. There is a complete statement of what it means. So it is a little intricate. I don't say that it is
25:20
property which is easy to verify when you have a theory, but at least it is well defined. And here we have the following lemma, which once again is an illustration of the bridge technique. So these times you can see there's a classifying topos of some theory T. And you suppose this
25:48
is a prescient topos. So it is equivalent to the category of pressures on some category C. And the invariant you can see there is the full subcategory of irreducible objects.
26:07
And by now you represent your topos in two ways. So on one side from the syntactic category CT GT, and on the other side from the category C on those with a discrete topology.
26:26
So on the side C hat, we get the irreducible objects of E are splittings of all presentable objects of the category C. So you see in fact here we get the same result.
26:42
This is the same thing as phonetically presentable models. So here this is the result that in fact we get the same thing. And on the other side, computing the irreducible object of the topos,
27:04
we just get the irreducible objects of the irreducible formulas in the syntactic category, which is a purely logical notion.
27:25
So as a consequence of this lemma, there are some remarks to be made. So first, the fact that the Karubi completion of C is the full subcategory of the topos on irreducible
27:40
objects. So this is just a rephrasing of the first characterization. And secondly, we get for such a preshift type theory that there is a one-to-one correspondence between irreducible formulas and finitely presentable set-based models of the theory.
28:05
So you see, this is really very remarkable because on one side you have the notion of irreducible formula, which is a logical notion, and on the other side you have the notion of finitely presentable model, which was defined as a purely semantic notion. It is
28:26
defined purely in terms of set theoretic models. And then here we have the following first criterion,
28:40
which is a purely syntactic criterion. So consider a geometric theory T, then T is preshift type if and only if any geometric formula considered and as an object of the syntactic category as the covering admits the covering by formulas phi i, which are all irreducible.
29:07
So you see the criterion, the syntactic criterion, is that a theory is preshift type if and only if any formula can be covered for the syntactic topology by irreducible formulas.
29:24
Okay, so I don't give a proof of this theorem, but what I want to do now is to give the other criterion for a theory to be preshift type.
29:40
So let's consider a geometric theory on a signature sigma, and then the criterion is this theory is preshift type if and only if the three following conditions are verified. Before stating them, I want to stress that all three conditions amount to saying that something
30:05
which is defined on the syntactic sides correspond to some other thing which is defined purely in semantic terms. So the conclusion is really that the theory is of preshift type
30:21
if and only if syntax and set-based semantics correspond to each other. Okay, so the first condition is the following. A geometric sequence of sigma is provable in the theory if and only if it is verified by all
30:49
set-based models. So remember that we have already said that for a geometric theory, a sequence is provable if and only if it is verified by the universal model in the
31:02
classifying topos. But you see, this is a model in topos, which of course is almost never the topos set. Here we are saying that the first condition is that t-provable, which is a syntactic notion,
31:23
is equivalent to the fact that this sequence is verified by all set theoretic models. This is the first condition. The second condition is the fact that any set theoretic model
31:43
which is finitely presentable, so I remind you that finitely presentable means that the associated covariance function respects filtering co-limits. So you see, it is a categorical notion. And so the condition here is that finitely presentable
32:06
models are finitely presented by some irreducible geometric formula, phi in some variables x1, xn. So what does it mean, finitely presented? It means that for any model N,
32:27
the model morphism from M to N corresponds to families of elements in the sets N a1, N an, you see the sets associated to the source a1, an in the model N. So families of elements,
32:48
which verifies this formula? So you see, for instance, if you have a group generated, let's say, by two elements, j and h, verifying some formula, for instance, g to the square,
33:05
I call h to the power 3, then what is the group morphism from this group generated by this element with this relation to an arbitrary group? It corresponds to the choice of two elements
33:23
in this group, which verifies an event formula. This makes sense in an arbitrary setting. And so if a formula is prescient type, in fact, any finitely presentable model
33:42
is finitely presented by such a formula. So this is the second condition. And together with the third condition we will immediately give, it is equivalent for the theory to be of prescient type. So here is the third and last condition for any source in the signature, and for any map which associates to any finitely
34:14
presentable model a subset of the product set N a1 cross N an in a sumptorial way.
34:25
So this means that for any morphism of models from N to N, the induced map from N a1 from N an to N a1 cross N an sends the subset Np to the subset Np.
34:44
So here you see p is any choice of subsets indexed by finitely presented set-based models and which are functorial. And the third condition is that if we have such a functorial map,
35:09
then it is defined by your formula in the variables of source a1 an. Of course, in the reverse direction it is obvious that if you have a family of subsets of the finitely
35:24
presentable models which is defined by your geometric formula, then it is functorial. But here we have the reverse condition that anything which is functorial is defined by your formula. And so the criterion for a geometric theory to be prescient type
35:46
is that these three conditions are very fact. It is an equivalent. So I remind you the first condition is for the fact that you can check probability on set theoretic models.
36:04
The second condition is that finitely presentable models are finitely presented by formulas, which in fact happen to be irreducible. And the third criterion is that
36:25
functorial families of subsets in models are necessarily defined by formulas. So we can say a few words about the proof in the direct sense. So when we have
36:46
a theory of prescient type, why are these properties verified? So in fact it is a consequence of three bridges. So for the first it was already done, we just have a classifying purpose
37:01
which by hypothesis is on the one hand the topos of sheaves on the syntactic site, on the other hand it is the topos of sheaves on the opposite category of the category of set-based models,
37:23
of finitely presented fed-based models. So as a consequence of that, it is an immediate corollary, is that it is enough to check probability on set-based models. The second property comes from the bridge which consists in computing the invariance
37:46
of irreducible objects both in the syntactic site and on the presentation sites by finitely presented, finitely presentable set-based models. And for the third property, you just
38:04
consider the universal model of the theory and of course ut associates to the sort a1 a1 objects of the topos and we can consider the product of
38:25
these objects. And by now we are interested in sub-objects of this product. So on the syntactic site what we get is that sub-object of this product is just formulas because in the
38:42
syntactic site sub-objects are always formulas. On the semantic side, the presentation by the opposite category of the set of finitely presented set-based models. So you are in a
39:06
pre-shift topos and you have to just to understand what it means to be a sub-object of a certain pre-shift and you get exactly what is written in condition three. So you get one direction of the theorem just by considering three bridges. Okay, so by now if we
39:36
gather what we have said, we have the following
39:43
thing, the following process we can try to implement. Suppose we are considering a theory which is a quotient of another theory. So here I denote t prime, the quotient of t, and suppose we have proven that t is a pre-shift type theory. So for instance by using
40:03
the one of the two last criteria. So in fact in the book, there are many criteria for a theory to be a pre-shift type. So suppose you have applied one of these criteria
40:23
and you know that t is a pre-shift type theory. And as it is a pre-shift type theory, you know it's classifying topos. It is a topos of pre-shifts on the opposite of the category of
40:40
finitely presentable set-based models. Or you can also say that this opposite category is just a full sub-category of the syntactic category on irreducible formulas. So you see, this category M can be seen either as a semantic thing or as a syntactic thing.
41:09
You see, because pre-shift type theories are really theories for which syntax and set theoretic semantics correspond to each other. And so by now,
41:24
according to the general characterization of quotient theories in terms of topologies, we know that the classifying topos of the quotient theory t prime is equivalent to the topos of pre-shifts on this opposite category M op, and of with some topology j.
41:47
And in fact, the topology j here can be made explicit. So here it is, you will say that the family of morphism between irreducible formulas,
42:02
so you see a family of, this means a family of provably functional, of tip-provably functional formulas between irreducible formulas, is covering if and only if the corresponding sequence from phi to the disjunction of the
42:24
images, which means the existential quantifier applied to the formula theta i's. So if this sequence is provable in the theory t prime. So be careful, you see in this statement,
42:41
when I say that the theta i's are provably functional from phi i to phi, here I am talking about tip-provability. But then he says that the j is defined in the following way, so the
43:02
sequence from phi to the disjunction of the existential quantifier applied to the theta i's, so this sequence is tip-prime provable. And so in fact, this defines topology j on
43:21
this category of irreducible formulas, and the classifying topos of tip-prime is the topos of sheaves defined by this topology on this category. So this gives you a way to present the classifying topos of tip-prime. But here I should stress that this representation
43:49
is not unique. In fact, there are, as I already said, infinitely many theories, infinitely many presentations of the classifying
44:10
topos. So this means that if I allow to replace tip-prime by a syntactically equivalent category, I will be able to present tip-prime in infinitely many ways as a quotient of
44:30
prescient type theories. And each presentation of tip-prime as a quotient of a prescient type theory will give rise to a presentation of the associated classifying topos.
44:45
You see, every presentation can be useful. In general, there is not a best presentation. In fact, the interest of the presentations depends on what you do.
45:01
And in general, it is extremely useful to have many different presentations, and these exactly, so you see the idea of the bridge, such as here. Anytime you have two different
45:20
presentations of topos, and you consider an invariance, you can try to compute the invariance in the different presentations, and this will create a correspondence. And so here, just because topos are so general, we have seen that any geometric theory defines the topos.
45:45
So this means that topos are incredibly general. This is not only for algebraic geometry, it can be defined everywhere in mathematics. So anytime you have a topos, and anytime you
46:01
have different presentations of a topos, and for any invariant, any toposteritic invariance you consider, this generates correspondences, equivalences. So this is really a principle whose generating power is absolutely huge.
46:26
And so Olivier says that this is some type of morphogenesis, of mathematical morphogenesis. So this means that you have a unifying principle, the principle of bridges,
46:40
which depending on the topos you consider, and the presentation of topos you consider, and the invariance you consider will generate extremely diverse results.
47:00
Okay, and so I hope that you have understood that topos are extremely diverse. So you see that this theorem of existence of classifying topos tells you that any geometric theory has a classifying topos. So you don't have to wonder whether it does exist or not.
47:27
You know it always exists. But then the problem is to get more information on the topos. Topos is a huge object. It is a category which is not small. So it is not possible to
47:45
fully know a topos. But what we can hope to do is to extract some partial information on a topos by choosing concrete presentations and considering invariants which are meaningful for the type of
48:06
problems you are considering. So this gives huge flexibility. Okay, and so you will never exhaust all the topos, you will never know all the information contained in the topos,
48:21
but you will be able to extract some information. And as soon as the topos is presented in different ways, which means through different sites or through different or as a classifying topos of different theories, so usually what you will get is that this topos
48:42
with in some sense is mysterious, which you don't know, which is too big to be known, this topos relates, it is really a bridge between things which are concrete and meaningful. And then you will be able to relate two concrete things through an object which in fact
49:08
is too big to be known. But this can be done as soon as you are able to compute or to express some invariants. So here in what I have explained in my lectures, I think I have made
49:24
clear that when we consider practical concrete theories, it is possible to produce concrete presentations of topos, if only by syntactic sites. But in other parts of mathematics,
49:50
different presentations of a topos may also appear. So for instance, I mentioned that next week there will be the topos by Clausen and Petter Scholzer. In fact, what they do in
50:08
their talks is to introduce a particular topos, they call that the topos of condensed spaces, and they introduce this topos as the right context to study functional analysis in a better
50:27
way. This is a new foundation for functional analysis. And in fact, when you begin to read the definitions, one of the first reasons why you understand this topos is a fine topos
50:42
is the fact that it has two natural presentations. So one of these presentations is by the site of compact topological spaces, and the other presentation is by the site of co-finite sets. So these are two very different sites with the same associated topos.
51:03
And the fact that these two very natural sites generate the same topos is a very good reason to believe that this topos is especially interesting. Here you see, I repeat the names, on the one hand you have the site of topological, of compact topological spaces,
51:26
so you see this site belongs to topology, and on the other hand you have the site of co-finite sets. And this site is of combinatorial nature. So here you have two different parts of
51:41
mathematics, on the one hand topology, on the other hand combinatorics, which are related through a joint topos, they both define. Okay, so this is an example, but once again there are infinitely many toposies, and for each topos infinitely many presentations,
52:05
and on toposies infinitely many invariants you may be interested in. This is really a principle of producing a huge diversity of results in mathematics. Okay, so thank you for your attention,
52:22
I think this is the end of my lectures. Thank you.