The over-topos at a model
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/55519 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
|
Toposes online, 202129 / 31
2
10
11
12
20
21
25
26
27
28
29
00:00
Laurent seriesModel theoryLine (geometry)Musical ensembleModel theoryMatching (graph theory)Division (mathematics)Presentation of a group
00:40
Grothendieck topologyTopostheorieInvariant (mathematics)Presentation of a groupLogicSet theoryTheoryModel theoryGeometryHomomorphismusMorphismusConnected spaceFunktorTransformation (genetics)AxiomDiagramNetwork topologyTopologyFiberFamilyBasis <Mathematik>MereologySineElement (mathematics)Price indexCategory of beingGeometryAreaObject (grammar)TopostheorieTime domainRight angleGame theoryVibrationAngleForcing (mathematics)Fiber (mathematics)Well-formed formulaUniverse (mathematics)ModulformCanonical ensembleNatural numberOrder (biology)Musical ensembleWater vaporFigurate numberCapillary actionHill differential equationCovering spacePhysicalismPivot elementPlane (geometry)Stability theoryCartesian coordinate systemAnalogyDivisorCausalitySpacetimeMetric systemSign (mathematics)Standard deviationPoint (geometry)FamilyCartesian productMatching (graph theory)Connected spaceGreen's functionTotal S.A.Radical (chemistry)Limit (category theory)Correspondence (mathematics)FinitismusFlagBuildingSheaf (mathematics)Twin primeSeries (mathematics)Process (computing)Shift operatorGroup actionPower (physics)Moment (mathematics)LogicResultantPole (complex analysis)RandomizationGenetic programmingExtension (kinesiology)Functional (mathematics)Grundlagen der MathematikLogical constantHorizonAlgebraic structureDifferent (Kate Ryan album)TheoryEvent horizonMultiplication signKeilförmige AnordnungPerspective (visual)Descriptive statisticsProjective planePresentation of a groupState of matterKörper <Algebra>Many-sorted logicEnergy levelNetwork topologyOpen setPhase transitionGroup representationTheory of relativityNeighbourhood (graph theory)Equivalence relationProof theoryProduct (business)Variable (mathematics)MorphismusNumerical analysisFood energyDiagramHelmholtz decompositionMoment of inertiaClosed setGenerating set of a groupConfidence intervalCurvatureModel theoryGrothendieck topologySocial classTransformation (genetics)Goodness of fitCodomainInverse elementHurewicz-FaserungSequenceEinbettung <Mathematik>Maß <Mathematik>CommutatorPosition operatorStatisticsConnectivity (graph theory)FunktorHomomorphismusAxiomAxiom of choiceSet theoryTopologischer RaumFree variables and bound variablesLocal ringAlgebraic closure1 (number)SubsetMilitary baseComputer animation
Transcript: English(auto-generated)
00:15
So the next talk is by Axel Osman, and he will talk about the overtopos at a model.
00:23
And this is joint work with Olivia Caramello. Okay, Axel. Thank you very much. Thank you very much for being there for this talk, where I have the pleasure to present this joint work with Olivia Caramello. So just let me go to the screen. So let me first introduce my topic.
00:43
So if you have a topological space, then you have a specialization order between points, and at a given point you can look at the upset or the downside of this point or the specialization order. The upset contains all points that lie above a given point x, and the downside
01:09
contains a point that are below a given point. And of course, this generalization generalizes to arbitrary subset of your topological space. And in this talk, we are interested in the topos
01:24
theoretic analog of the downside. So recall that a Grothendieck topos has a category of points which are the geometric morphism from set into this topos. And also you can look at the under category and the over category at a given point,
01:43
and those are the analog of the upset and the downside respectively. And of course, this generalizes to arbitrary geometric morphisms, where you can look at the under and over category of the home category of geometric morphism between two topos at a fixed geometric morphism. In this talk, we are interested at the over category at a given point.
02:05
This led us to the notion of totally connected topos. So a geometric morphism is said to be totally connected if the inverse image part has a Cartesian left adjoint that is which preserve finite limit, and then the pair of adjoint given by this left adjoint and the
02:24
inverse image is a terminal object in the category of section of your geometric morphism. And in particular, as it is quite common to classify the geometric properties of topos by the property of their terminal geometric morphism to set their functor of global section,
02:44
we say that a Grothendieck topos is totally connected if its terminal geometric morphism is totally connected as a geometric morphism. And this means that your topos has a terminal point. In particular, if it is a classifying topos of a geometric theory, then this means that this
03:02
geometric theory has a terminal model in set and in fact, in any arbitrary topos. So just I would like first to recall something which is already known, but which will be useful to understand what we are going to do, which is we can construct canonically a totally connected
03:20
geometric morphism at a given arbitrary geometric morphism. To do so, I call that the category of Grothendieck topos has power with two, which is a universal two-cell classifying natural transformation between geometric morphism into a given topos. And the codomain part of this
03:42
universal two-cell, which is called the universal codomain, is always totally connected. This is in some sense a generic totally connected morphism. And actually using the fact that totally connected geometric morphisms are stable under pullbacks, we can use
04:02
this generic morphism to construct a free totally connected geometric morphism at another geometric morphism. To do so, we just have to take the two pullback of the universal codomain along a point, if we want to compute the over topos at a point,
04:22
or at an arbitrary geometric morphism. In both cases, the universal property of this construction is that its point will be exactly the category of the over category at the corresponding point, and for an arbitrary geometric morphism, the over category at this
04:41
geometric morphism. In particular, in the case where this geometric morphism is the name of a model of a geometric theory, that is, if our topos is the classifying topos of a geometric theory, then the universal property of the over topos is that it classifies a homomorphism
05:02
of T-model into the inverse image of this model along arbitrary geometric morphisms. So the purpose of this talk is to provide a site description of the construction of the over topos, because as it is done this way, it is an abstract universal construction which does
05:25
not retain any information about the site, and in particular the syntactic property encoded in the model structure and the structure of the classifying topos of a theory. So we want to provide a canonical site for this construction, and we will have to do in two steps.
05:46
First, we will have to process for the case of a model in set, that is for a point of a topos, and then we can do this for the general case, for an arbitrary geometric morphism, but it will use a bit more involved technologies about starts and next category and so on.
06:05
So for the set-valuated case, just recall before that for geometric theory, you have its syntactic site, which objects are formulas in context, morphism are probability equivalence classes of probably functional formula between those
06:24
formulas in context, and the topology, the syntactic topology on this category, is generated by the cover that are encoding the disjunctive sequence of your theory.
06:41
Now a model in set is a flat functor for the syntactic topology into set, sending a formula in context to its interpretation, and we can look at the category of element, of global element, of this functor, whose objects are paired, made of a formula in context, and the global element of this formula in context,
07:03
and morphisms between two global elements, is just an underlying morphism between the formulas in context, that may commute the corresponding global elements. So in set, we are going to use an interesting property that make the construction easier,
07:22
which is that the one object set is generating in set, that is any set is a co-product of one and X by its global element, and in particular this will be true for the interpretation of formulas in context by a model M, and this will also be preserved under inverse image,
07:46
that is if you look at the inverse image of a model in set, then the decomposition is true after applying inverse image. So moreover, if you consider a model that is a flat functor
08:02
for the syntactic topology, then covering family for the syntactic topology are sent to jointly epimorphic family, which means that if you take a global element of this interpretation, then there is at least one member of the cover, such that this global element
08:24
has an antecedent along this member of the cover. This leads us to consider the following topology on the category of global element, which consists of families of all possible antecedents of a global element along a cover, an interpretation in M, of a syntactic cover.
08:48
And this generates a topology we will call the antecedent topology on the category of global element, and our main result is that the category of global element
09:01
and the antecedent topology on this category of global element is a presentation for the over topos. So to prove this, we have to show that it possesses the universal property of the over topos, which is that we must prove that any geometric morphism for an arbitrary topos
09:24
into this shift topos is the name of a homomorphism of T model into the inverse image of M, that is the inverse image along the global section functor of your arbitrary topos. So to do so, suppose we have a homomorphism to the inverse image of your model,
09:45
this is the same thing as a natural transformation between a flat functor for the syntactic topology into where the codomain of this transformation is the inverse image of your model, and this natural transformation has components indexed by object of the syntactic site.
10:07
And now, if you take an element of an interpretation in M of a formula in context, then you can look at its inverse image and you can take the fiber of its inverse image along
10:21
the component of your natural transformation at the corresponding formula in context. This returns you an object, a fiber object at each element of M, and you can do this in a functorial way thanks to naturality of your natural transformation and using putback property,
10:45
and this returns you a functor from the category of element of M into G, and then proving flatness for the antecedent topology is something which is mostly an application of stability of co-products and epimorphisms in God-tended toposces.
11:06
On the other hand, if you have a geometric morphism into the shift topos over this site, this is the same thing as a flat functor from the category of element for the antecedent topology.
11:22
So in particular, this returns you a family of object indexed by a global element of interpretation, and for a given interpretation and a choice of an element, you can first compose the object corresponding to a given element and take its terminal map into one and compose it
11:44
canonically with the name of the inverse image of this element, and this returns you a map into the interpretation in the inverse image of M, and then you can view all the objects that correspond to global elements of a fixed sort,
12:02
and this returns you a map corresponding to a given formula in context, and this is a way to construct actually a model of T in G whose interpretation of the formula in context, a given formula in context, is given by the corresponding co-product we constructed above,
12:23
and the homomorphism of T model into the inverse image of M just is provided, as you can see there, by the universal property of the co-product at each formula in context. So the reversibility of this process is mostly actually an application of extensiveness and
12:43
stability in content-dictopus, so I won't be too long on it. I prefer to turn to the logical aspect of this construction. So it is entirely as we know that this new overtopus classifies homomorphisms into a fixed model up to inverse image, we would like to know what is the
13:02
geometric theory which is classified by the overtopus. So to do so we have to define for this over theory, we have to define an over language in which this new theory will live, and an auxiliary language in which we will test what kind of sequence we want to have
13:25
in this over theory. So the over language will consist of a new sort for each global element of your model and a new function symbol for each morphism in your category of global element of
13:44
this model, and on the other hand the auxiliary language will be an extension on the ambient language in which you will add a new constant symbol for each global element of your model, and then your model is canonically equipped with a new structure, an extended structure,
14:06
for this extension of the language where you interpret the constant corresponding to an element in two by the corresponding element, and you have also a canonical interpretation from the over language to the auxiliary language which replace in a formula all instance of
14:27
free variable of the sort corresponding to an element with the corresponding constant in the auxiliary language for this element, and then the new theory, the over theory associated
14:41
to a model will have as axioms all the geometric sequence in the over language whose interpretation in the auxiliary language are valid in the extended structure your model have canonically for the auxiliary language, and actually we can also prove that the over topos
15:04
as we constructed it is the classifying topos for this over theory. So now I turn to the general construction in the general case. So in the general case the complication is mostly that one is not anymore a generator in an arbitrary authentic topos.
15:24
This means that we cannot just restrict to global elements of a model, we have to consider arbitrary generalized element, so and they have morphism between them, they have more complicated structure, but at least we can in the following we will also restrict
15:45
to the ones that are indexed by basic element, that is if you have a presentation site for your topos you will be able to at least to restrict to generalized element that are indexed by an object coming from the site of presentation of your topos.
16:05
But in any case the complication will be that not only the formula of the interpretation may be able to vary, but we must also take in account viability of the indexing object
16:21
in the generalized element. So to address this problem properly I have first to give some word about the notion of stacks and the construction of zero topology. So as Ricardo told you in the last talk, there is a notion of zero topology for an index category and in particular if you
16:48
have a Cartesian stack on a Grothendieck topos then you can consider the Grothendieck construction associated to this Cartesian stack and equip the corresponding fibered category with the
17:03
geo topology which is the smallest topology making the corresponding fibration a comorbidism of site. And in particular if you have a small site of presentation for your base topos you can compose your Cartesian stack with the Yoneda embedding and this returns you a
17:25
fibration over the site for your topos and you can restrict the geo topology over for this site and actually you can give the concrete description of the covering family for the geo topology as the Cartesian lift of cover for the G topology of your bases.
17:46
And actually you have those defined the same topos, this is the same thing if you take the topos with the geo topology or its retraction along the Yoneda embedding of a site of presentation and what is important is that you
18:05
get a geometric morphism and used by the comorphism you have thanks to geo topology. So now something which was remarked by Olivia recently is that if you have a geometric morphism
18:22
then you can construct canonically two indexed categories associated to it. One indexed by the domain topos which send an object e to the category of e indexed generalized element of the inverse image part of your geometric morphism and on the other
18:43
hand for the codomain topos you have an index category on the codomain topos which send an object to the category of generalized element of its inverse image and so we and what happened is that both those indexed category and use the same construction and use the same category
19:07
and there's a cotton deconstruction which is the comma of the domain topos and then just major and which is equipped with two fibration on the left over the domain category and on the right
19:21
over the codomain category and now you can equip this comma category with the smallest topology which makes simultaneously those two fibration comorphism of sight and this topology which we call the lifted topology is jointly generated by the two geo topologies associated to those two
19:44
vibrations. In part no something we would like to have is a way to restrict us to small data to site of presentation for the domain and codomain topos because in practice we want small site
20:01
because the category I defined there is a large site so to construct a small site if we have a site of presentation for the codomain topos then we can look at the comma where we on the right we consider the inverse image of basic object that is composed of the inverse
20:25
image with the unit embedding and we can restrict the lifted topology to this category and we still have a fibration over the site for the codomain topos and this restriction
20:42
allow you to have a comorphism of sight. On the left you can also restrict if you have a presentation site for your domain topos you can also restrict along the unit embedding so on the left and again you have an innocent way to restrict your topology as a lifted topology
21:02
on this comma category and the interest is that the new comma category is small and you have a canonical topology on it derived from the lifted topology. So a problem is with this construction is that the new construction is a bit less pure because
21:22
it breaks the properties that we have a fibration because we will see that inverse image of basic generalized element are not necessarily basic but this is not very important for a pure positive. So just a word on the concrete description of the lifted topology
21:44
the restriction of the lifted topology in this context it will consist of restriction it will consist of families where you take first a generalized element of the inverse image of the
22:01
basic element then you look at the inverse image of a cover of the object you look at image of and then you take a cover for each fibers of this generalized element.
22:25
So now I would like to apply this to a Cartesian stat to the case where you consider a model of a
22:41
T-model into a growth-ended topos with a standard site of presentation this is the same thing as a flat functor for the syntactic topology into this topos and this defines a Cartesian stack sending an object of your base site to an object C into the category
23:05
of C indexed generalized element of the functor coding for your model and now again you can define the category of generalized element of your model which is the comma category
23:22
between the unit embedding and the flat functor coding for your model and again you can equip it with the restriction of the lifted topology we described above and in this case it has the following presentation you take a generalized element of an interpretation of
23:43
formula in context you you look at all at at the interpretation in M of a syntactic cover of the corresponding the underlying formula in context and then you ask for covers of each
24:00
fibers of this generalized element along the numbers of your syntactic cover in some sense you ask for having a fiber-wise covering of the fiber and this this is a generalization
24:22
of the antecedent topology we constructed in the set-valuated case and this return you again a comorphism of site from the comma category into the base the site for the topos in which you interpret your model and this comorphism of site returns you a shift topos and a canonical
24:44
geometric morphism and our result is that again this the shift topos over the comma category together with antecedent topology is has the universal property
25:01
of the overtopos at the at the model M and in particular the geometric morphism and used by the comorphism is the totally connected universal morphism at this model so again proving that the this topos has a universal property of the overtopos
25:22
is quite similar to the set-valuated case now the principal difference is just that when you will you will construct a model from from a natural transformation as in the set-valuated case you will have to glue a object indexed by diagram of a generalized
25:44
element rather than just a co-product of discrete set of global element but this is not a very important difference actually and so there is no need to be too long about that so I would prefer to finish now so just perhaps a last remark on this construction which is that
26:06
at some point in for practical reasons we want to restrict us because we want site description we want to restrict us to the restriction of the lifted topology which are concrete but are a bit cumbersome and may seem a bit ad hoc but actually it's again a situation in which
26:27
if you drop the site the site information and go in a more abstract level a more invariant level of the authentic topos themselves you have a more pure description in which the universal
26:41
properties of your object are more evident so now just to finish I would give a few perspectives for this work first which is that actually totally connected geometric morphism and topos are a dual notion to the notion of local geometric morphism topos and it is
27:05
known that for a geometric morphism point of a topos you can look at the local topos over this geometric morphism which is the Grothendieck-Verdier localization and it is obtained as this is a dual of the totally connected to the over topos actually this
27:26
is a dual construction of the over topos and it is obtained through a formula describing it as a co-filtered to limit of et al geometric morphism and something we would like to know is if the
27:41
over topos also has a similar description as a co-filtered to limit but of what kind of morphism it would be a generalization of the fact that the closure of a point is an intersection of the closed neighborhood it has finally I would just perhaps also there is a
28:04
question to know what is the theory the geometric theory which is classified by the over topos in the arbitrary case perhaps this is for a notion of relativized geometric theory you don't know and finally it would be interesting to have some description of the functor which is the analog
28:25
of the functor externalizing topos into et al geometric morphism over e but for totally connected topos so thank you for your attention that's all okay thanks a lot axel for this very nice talk
Recommendations
Series of 28 media