/sci/ - Science & Math

>>7523064
well I like the predicative constructive locale theory [the one that you do in any topos [with NNo]]. Note that there is classical treatment of locale theory. There is also what is called synthetic topology which uses the notion of a coverage to generate a locale.

In terms of logic you have the geometric logic
http://ncatlab.org/nlab/show/geometric+theory

it is a positive logic [a logic of ''observation'' thanks to the infinite disjunct], no PEM, no powerset, but finite subsets of Kuratowski finite set [see the quoted bit on finite subsets of finite sets above in the thread] and the power-locale for appropriate locales, no choice at all. You can quantify universally only on finite sets, on N, Z, Q, compact locales, but not R nor C.


THERE IS NO IMPLICATION [because it is not a geometric notion = it behaves badly when we transport the theory from topos to topos, as explained below]
The logic uses sequents and contexts for free variables which permits to deal with the empty set as a carrier set easily.
Locale theory is nice because you have, predicatively-constructively, all the theorems about R in topology that you want form your study of classical mathematics. I think that if you do pointless topology in intuitionist logic, you do not retrieve the theorems. integrals, C*-algebras, all the topology on the reals are defined in geometric logic.

Hott constructs the same localic reals in chapter 11.

there is a video by Johnstone himself explaining the construction of the reals

Peter Johnstone: "Topos-theoretic models of the continuum"
https://www.youtube.com/watch?v=pKWYa9sc5UI

other people in the fields are everybody in HOTT, palgrem, paul taylor, steve vikers, maietti, all the people in synthetic topology.

>>7469958


Peter Johnstone: "Topos-theoretic models of the continuum"

https://www.youtube.com/watch?v=pKWYa9sc5UI

dedekind cuts in constructive settings [hott, or synthetic topology] will give you the locale of the real numbers with the expected topology

>>7294285
>>I am learning algebraic geometry so that I can try and construct a simple framework in which we can do category theory, but where Isbell duality and hopefully "all" of the notions of abstract duality come naturally.
yes they do,

http://ncatlab.org/nlab/show/Isbell+duality


category theory has lots of generalized stone/isbell dualities, with the famous locales -frames one, the quantales (non commutative frames) , the gelfand duality and so on. But there still is not a spectrum for noncommutative algerbas. Perhaps there are spectrum for Noncommutative 'Spaces' and 'Stacks.

perhaps my toposfu can help you on this one

http://www.oliviacaramello.com/Videos/Videos.htm

there was a talk recently on youtube
Prakash Panangaden_ _The Mirror of Mathematics_, Lecture 1, 2, 3

for the topological side.

>>7272055
the fiber bundle is an arrow p:Y->X in the category TOP or LOC


the fiber Y_x over a point x of X is the pullback of the arrow p, along the arrow representing the point x, that is to say, over the arrow x:1->X

the fiber Y_x is then the topological space/locale that hover over x


now, you take a section s of some open U of X

it means that you look at all the fibers Y_x for x in U open in X,

so you take the pullback of Y->X along the subset inclusion U >->X and you get Y_U which is the fiber over U

then a section s is an arrow from U to Y such that p \circ s = the inclusion , that is to say, such that the diagram commutes in TOP or LOC

http://rin.io/swashbuckling-topoi/

>>7271275
look at the toposes


>Why? The idea is this:
>Constructive reasoning allows maps to be treated as generalized points.
>Locales give a better constructive topology (better results hold) than ordinary spaces.
>The constructive reasoning makes it possible to deal with locales as though they were spaces of points.

>Conceptually, a locale is a propositional geometric theory pretending to be a space.

>space <> logical theory
>point <> model of the theory
>open set <> propositional formula
>sheaf <> predicate formula
>continuous map <> transformation of models that is definable within geometric logic
>Opens are Propositions

>A topology (on U, say) has enough lattice structure to model intuitionistic logic: ∩ and ∪, which both preserve openness, model the connectives ∧ and ∨.

>If a proposition P <> open set P,
>then ¬P <> the interior of U–P
>If a proposition Q <> open set Q,
>then P->Q <> the interior of (U–P)uQ

>When I say that a topos is a “generalized space,” it is a space in which the opens are insufficient to define the topological structure, and sheaves have to be used instead.


http://rin
.io/swashbuckling-topoi/

>>7265015
Topos

>Why? The idea is this:
>Constructive reasoning allows maps to be treated as generalized points.
>Locales give a better constructive topology (better results hold) than ordinary spaces.
>The constructive reasoning makes it possible to deal with locales as though they were spaces of points.

>Conceptually, a locale is a propositional geometric theory pretending to be a space.

>space <> logical theory
>point <> model of the theory
>open set <> propositional formula
>sheaf <> predicate formula
>continuous map <> transformation of models that is definable within geometric logic
>Opens are Propositions

>A topology (on U, say) has enough lattice structure to model intuitionistic logic: ∩ and ∪, which both preserve openness, model the connectives ∧ and ∨.

>If a proposition P <> open set P,
>then ¬P <> the interior of U–P
>If a proposition Q <> open set Q,
>then P->Q <> the interior of (U–P)uQ

>When I say that a topos is a “generalized space,” it is a space in which the opens are insufficient to define the topological structure, and sheaves have to be used instead.


http://rin
.io/swashbuckling-topoi/