Why do we care about categories that behave "like" the category of sets, or abstracting set-theoretic properties to the language of category theory?
because we can think about them
So that there is actually something to talk about ?
so we can have axiomatic systems as objects, and study what happens to those objects when you use them as foundations of mathematics
>>7872543
>why would we try to generalize a category we know very well?
gee, I wonder
Why do we care about multiplication "like" in the integers, or abstracting prime factorization properties to the language of rings?
If you hadn't noticed, all we're ever trying to do is understand complicated things by thinking about how simple things work.
>>7873570
i think this is the correct reply to OP
it's nice when things are familiar
but of course, unfamiliar things should also be explored, but one step at a time
>>7872543
because SET is just the topos Sh(1) of sheaves over 1. other toposes are toposes over other structures,
>>7872543
also, because toposes of sheaves and their geometric functors are the way to generalize topology, which is called topology without points.
>>7872543
>>7873595
>>7873606
These and more.
Reason one is that it shows us what we "really needed" in set theory. By "really need" I mean the elementary topos properties: power objects, image factorization, etc. which turn out to be sufficient to interpret intuitionist logic/simply typed lamba calculus with a truth type, and follow from elementary axioms. For example, it's pretty cool to see how quantification can be derived from the powersets, so that it has the "correct" meaning in an arbitrary topos.
Two: for grothendieck toposes they really do act like spaces. For their connection with logic, they act like massive generalizations of Tarski-Lindenbaum algebras for geometric logic, which allows for infinitary disjunction. Now, concepts like "open map" "classifying space" "quotient" all have logical import as preserving certain quantifiers, finding models of a theory, and localizing the logic around a particular open or point (like taking an arbitrary boolean logic and "honing in" on a single "truth table"). "Continuous" functions are geometric morphisms and preserve geometric theories.
For example, a set-theoretic statement about a ring often scales up to a sheaf-theoretic statement about a scheme with little new effort. L-T topologies on the zariski topos correspond to local operators which give "modality" to your ring language. That's all very nice.
But IMO, it's largely an aesthetics thing: I like being able to be "hands on" with my categories, and now we can "really" see a model of "set theory" without middle or choice or what have you looks like and how to build one. Semantics of "variable objects" is also just useful for my research. For me, categorical semantics is the most straightforward, as it directly gives you arrows as interpretations. Examples like semantics for a kripke frame show that, when viewed the right way, classical and kripke systems works identically - its just the semantics of the internal language.
>>7874319
can you talk about the internal and external language ?
I heard that externally, you cannot see tell what happens in the topos, which would mean that you can translate the internal language into the external one, but not always the external one into the internal language.
>>7874319
>finding models of a theory
This is what really caught my attention. Are you telling me that topos theory provides a way other than forcing to expand models of set theory? Has it thus found use in new independence proofs outside the scope of strictly set- and model-theoretic tools?
This all seems like the emperor's new clothes of math. All this "new" jargon seems like a schizophrenic attempt at reinventing the wheel, disguising simple concepts in complex and ad-hoc jargon. How misguided and out of touch am I?
>>7874903
I can see why this would seem to be the case, but only because a lot of the relevant developments were concurrent with, or just prior to development of topos theory.
for example, Kripke frames and their semantics were nearly concurrent with the Joyal sheaf semantics. you see independent development of various "duality" theorems - such as stone and Priestley duality about a decade before (and after) locale theory.
so effectively, you can kind of get these facts independently from other branches of math, but in topos theory you can see all of these as properties of a unified theory.
I think part of this attitude is just because people see the non-topos versions first, so think that they are the "real" math and topos theory is the "rewording" which is of course very silly. I think the reason many people don't simply learn these as natural results of topos theory is because most people don't need tools that general and it has a bigger learning curve. even if it were simply a rewording, it's still a lot nicer to have a single category of grothenieck toposes whose internal structures already has all of these properties over a bag of facts.
>>7875059
I can understand and sympathize with that. Thank you for the calm and rational response to what could have been perceived as a hostile post.
hi
>>7875931
The way she's being treated by all the topos theory veterans makes me not want to bother with topos theory at all and instead go into something else.
>>7876023
she gave a course in Paris last year, I think that she is fine.
Topos theory honestly seems like a fleeting meme field, a passing vogue. How wrong am I?
>>7876951
topos theory is pretty much just logic+topology, so unless you see those fields disappearing soon... Most common toposes are made up of sheaves which underlie algebraic geometry, homology, the theory of manifolds, ...
It's just an approach to all of these subjects in a cohesive way. A better way to unite all of these may come along which has nothing to do with toposes. But right now, it looks like categories which naturally handle these constructions well are all based on something topos-like.
>>7874405
I responded to this earlier, but it seems my response failed to post. As a warning, I use sheaves in my research for practical reasons, and I am no expert on toposes, and certainly not their philosophy, but I'll give it a shot.
From what I understand, the correlation actually goes the other way - you can pretty much always externalize a fact about a topos into some other category, but external facts aren't necessarily internal facts. For example, if you have an "internal lattice object" in a sheaf topos, you can take its global sections to get an actual SET which is a lattice.
The idea is that if a sheaf topos consists of "variable sets" then from the point of view of the internal language, these are simply "sets". So a logical statement about an internal ring externally looks like a sheaf of rings, an internal sub"set" is actually a subsheaf, an internal power"set" a sheaf exponential, etc.
I almost exclusively work externally, because then you are allowed to use any standard math trick you have up your sleeve, because the topos and its objects are just like any other mathematical object. When working "internally" you act like this topos is the whole of the mathematical universe you are interested in. People seem to like to do this when they are working on foundations, because you can describe many constructions without reference to any other category, such as Set. I don't work on foundations, so generally I DGAF, and don't stay "pure".
>>7875166
Also, IMO, you'll find that while the proofs are more roundabout than you may be used to, I actually find the definitions to be less ad hoc than in set theory.
Most of the constructions in topos theory come from universal constructions and adjoints, usually revolving around the powerset/characteristic function relationship.
While still "syncategorematic" like in the set-theoretic constructions, we get some sort of answer to "why" we have truth objects that look the way they do, "why" universal and existential quantification work the way they do, etc.
Take even a super simple example: how do I represent a tuple in set theory - Kuratowski encoding {{x},{x,y}}? The grothendieck-tarski encoding {x,{x,y}}? As an element of a cartesian product XxY - and why do we define the product that way anyway?
All of these seem kind of arbitrary in a way that categorical product is not. Obviously, scale that "argument" up to any of the major constructions that you can do in an elementary topos.
>>7876977
It sounds like topos theory has a lot of motivation outside pure category theory + mathematical logic. What would you say to a set theorist (whose field of knowledge is strictly limited to mathematical logic) potentially interested in studying topos theory?
Other people are welcome to answer too.
>>7877044
If you like logic, I would suggest Goldblatt's book. I would wager that even a highschooler could understand it if they were dedicated. It's an intro to categorical logic, which essentially means the internal language of toposes, thought he doesn't quite phrase it that way. Expect undergrad intro to logic level stuff but from a new perspective, essentially.
If you want more "deep cuts" after - brush up on category theory with Awodey's free book, and then get Mac Lane and Moerdijk. I cannot recommend this book enough. Tons of example, beautifully written, fun, cool, shows all sides of topos theory, much less dense than Johnstone (though you'll eventually need it if you want to get into the spatial side). Has motivation from differential manifolds, group theory, and much more, and exhibits the Cohen proof of the independence of the CH from ZF completely topos-theoretically as an application. Also shows how to construct a classifying topos for various important objects like local rings. Essentially, maps into this topos finds models of a local ring in ANY grothendieck topos: for example, in the category of sheaves of the one point space - this returns local rings, which are sets; for sheaves on an arbitrary space - this returns locally ringed sheaves on that space.
HoTT vs Topos Theory vs Abstract Stone Duality?
>>7877236
HoTT for memes
Topos and Stone Duality for autism
>>7877077
>exhibits the Cohen proof of the independence of the CH from ZF completely topos-theoretically as an application
That's amazing! I am so motivated to learn this now. Thank you immensely for your references and awesome post.
I wonder if large-cardinal hypotheses have been extended to the topos-theoretic language, or indeed if any new large-cardinal properties can arise from it.
>>7876977
>>I almost exclusively work externally, because then you are allowed to use any standard math trick you have up your sleeve, because the topos and its objects are just like any other mathematical object.
do you work in predicative constructive logic ?
>>7877044
>It sounds like topos theory has a lot of motivation outside pure category theory + mathematical logic. What would you say to a set theorist (whose field of knowledge is strictly limited to mathematical logic) potentially interested in studying topos theory?
lawere has a book to cast usual set theory in terms of category theory. this is the best book to start.
then you take the borceux who exposes what you can do with categories at a graduate level, which is not pure logic at all, but math. then you switch to hott if you want logic, or other works which are explicitly logic, such as locale theory as stated above (toposes are pointless topology done through predicative logic, or predicative logic done through pointless topology)
>>7876990
I agree that it is dubious to do math without these universalities. category theory is math, formalisation done the most natural way, to the point that everything else seems contrived and ugly.
>>7878527
No, I just need sheaves fairly often and I treat them as objects in classical mathematics.
>>7877486
I don't know if they are new or not, but since analogues of "set-theoretic" surjectivity, injectivity, and power objects can be defined topos-theoretically, you can definitely state most things about large cardinals in toposes.
>>7877077
the book by maclane deals only with finitary geometric logic.
the application of the full geometric logic is found in the book by steven vickers topology via logic. there is also the fundamental work michael_makkai_&_gonzalo_reyes_-_first_order_categorical_logic_model-theoretical_methods_in_the_theory_of_topoi_and_related_categories_[springer_1977_9783540084396]
plus of course
https://ncatlab.org/nlab/show/category+theory#TextBooks
there is also a good historical exposition
-Andrei Rodin
(Submitted on 25 Sep 2012)
Lawvere's axiomatization of topos theory and Voevodsky's axiomatization of heigher homotopy theory exemplify a new way of axiomatic theory building, which goes beyond the classical Hibert-style Axiomatic Method. The new notion of Axiomatic Method that emerges in Categorical logic opens new possibilities for using this method in physics and other natural sciences.
http://arxiv.org/abs/1210.1478
and two books
-From a Geometrical Point of View
A Study of the History and Philosophy of Category Theory
Authors: Marquis, Jean-Pierre
http://www.springer.com/us/book/9781402093838
-ralf_kromer_-tool_and_object_a_history_and_philosophy_of_category_theory_[springer_2007_9783764375232]
>>7872543
bumperoo
sheer autism tbqh
>>7880923
better than HS math.
reminder that the german from nlab formalizes, with toposes, the philosophy from hegel
https://ncatlab.org/nlab/show/Hegelian+taco
>>7884849
>you will never be well-rounded enough to formalize philosophy in topos theory
>>7877077
Going from Goldblatt to Mac Lane and Moerdijk is going to be too difficult in my opinion. I think Bell's Toposes and Local Set Theories could help filling the gap between those two.
>>7885566
Maybe. desu the first few chapters were helpful for bringing me up to speed on category theory, but unless you have been a logician for a while, I actually found that book way less intuitive and more abrupt.
I would maybe even supplant that with Awodey's free book. But >>7879452 was right that Mac Lane is not the most comprehensive presentation of the logical side; but the Vickers is quite comprehensible even for a CS student, easier than Makkai and Reyes imo.
>>7884849
>taco
Did Haskell memes spread to category theory?
>>7886762
They originated in category theory, anon.
I feel there is a more straight forward way to it
Let's say you have some things a,b,c,... in a set X with possibly some additional structure
(X may be just the set, a vector space, an algebra, a topological space...).
The space of function from X to the complex numbers C is always a rich object because C is.
Even if it makes no sense to add b and c in X
(e.g. if b=["Austria", "Japan"] is a list and c="9 kelvins" is the sea temperature)
if u and v are functions in X->C, then you can add them by defining their addition +' in terms of the addition + of the image in C:
(u +' v)(b) := u(b) + v(v)
Same goes for multiplication and exponentiation and so on.
The function space, written C^X, is richer than X.
Except with things like Hilbert spaces, where this dual space is isomorphic to X again ... in this case X was already as nice as C^X.
If X is a topological group (like R with shift operators), you get the theory of Fourier analysis and so on.
Now if X is a category, then the category of functors with values in the category of sets Set^X (i.e. the category of sheaves in the 1960's sense) is nice exactly for the same reason.
The elements u, v of Set^X can be multiplied, added and exponentiation because the image, sets, have the Cartesian product AxB and the disjoint union of A and B and function spaces A^B.
The Yoneda lemma for the functors
B -> Hom(B,A)
(you consider the mapping of X to Set^X, where pass from an object A in X to the hom-functor Hom(-,A) in Set^X)
then says that the arrows Hom(A,B) in X are in bijection with the arrows in Set^X.
Hom(Hom(-,A), Hom(-,B) ) <=> Hom(A,B)
But Set^X is richer than X because you have new functors F lying in it, which however behave not scaries than the Hom-functors as again the Yoneda lemma tells you:
Hom(Hom(-,A), G) <=> G(A)
Topos theory (pic related) is then just
"look at those categories, those with multiplication and exponentiation"
(and you oops dropped the need for set theory, and oops logics are topoi)
>>7887242
Sorry for the bad notation there.
I meant
(u +' v)(b) := u(b) + v(b)
And u,v in the second half are functors, A,B are both object in X and at another time in Set.
Later, I wrote F, but meant G.
Btw. (pic related), it's a theorem in that case that addition arises from multiplication and exponentiation
(it's called limit and co-limit instead of addition and multiplication because it's something that also respects the homomorphsim structure of the elements)
Oh, and my answer to OP
>Why do we care about categories that behave "like" the category of sets, or abstracting set-theoretic properties to the language of category theory?
is that this sounds like
>Why do we care about sets that behave "like" the category of complex numbers, or abstracting properties of C to the language of category theory?
Well the complex valued functions have Fourier analysis, for example, while the complex numbers themselves are just a field. I mean there is actually a subject called function fields.
For topoi, the initial application was algebraic geometry.
Then again, I find topoi unhandy at the same time, it's too tough to learn. The killed apps and possible practical stuff have all already be established before in other languages, that's the problem for the field, I think.
>>7887242
This power object. How is it different from an exponential in category theory?
>>7887330
an exponential of what ?
>>7887330
The exponential is more general.
Normally the exponential refers to a general X^Y sort of object (or the functor sending an object to this), and the power object is a 2^X sort of thing.
>>7887330
https://ncatlab.org/nlab/show/power+object
-If 1 is a terminal object, then \Omega^1 is precisely a subobject classifier.
-A power object in Set is precisely a power set.
-A category with finite limits and power objects for all objects is precisely a topos. The power object PA of any object A in the topos is the exponential object PA=\Omega^A into the subobject classifier.
I have only one question: Can topos theory be used to answer questions that contain neither the words category nor topos ?
For example, a problem that stumped analysts for a while at the end of the 19th century was knowing whether, if f is a non-vanishing function whose Fourier coefficients are l^1, the Fourier coefficients of 1/f are also l^1. It turns out that this problem is easily solved using simple facts about Banach algebras.
In the same vein, the Jordan curve theorem and the Brouwer fixed point theorem provide a great motivation for homology.
This is how I measure the usefulness of a theory. I do not mind abstraction but I do mind pointless abstraction (our time on earth being limited and all).
>>7887344
I know that you can formalize infinitesimals through synthetic differential geometry
https://ncatlab.org/nlab/show/infinitesimal+object
otherwise, it is more about foundations on the sides of logic and philosophy
>>7887359
there is also the descent theory and lax descent theory. this is about the quotient of a space by a relation, like a preorder or an order.
https://ncatlab.org/nlab/show/descent
>>7887344
i would say, read this one
http://mathoverflow.net/questions/83437/the-main-theorems-of-category-theory-and-their-applications
>>7887330
The logical chain of thinking is this:
In the cateogry of sets, consider
X={a,b,c,d,e}
and it's subsets like
U={a,d,e}
The above information can be together be encoded in an injection
j : U -> X
j(x) = x
(injection means [math]j(x)=j(y)[/math] implies [math]x=y[/math])
At the same time, the subsets of X are in bijection with the characteristic functions X -> {0,1}.
E.g. U resp. j above is encoded by [math]\chi_j[/math] mapping
a to 1
b to 0
c to 0
d to 1
e to 1
Note two more things:
I) The ist only one function from any set Y to the set 1:={0}, namely the one that maps any argument to 1.
II) Going from U to X to {0,1} via j followed by [math]\chi_j[/math], we necessarily map to 1, because j filters all that's not in U. That's a commuting diagram.
"Subobject classifier" here is {0,1}, resp the map from {0} to {0,1} that maps 0 to 1.
%%%%%%%%%%%
To axiomize the notion of subobject in category theory proper, you must capture the above situation without any reference to anything that's inside an object (i.e. the seven values a,b,c,d,e,0,1).
It's done like this:
"Monomorphism" is defined by
[math]j\circ f = j \circ g[/math] implies [math]f=g[/math])
and terminal object (1 above) is defined by saying there is only one arrow into it.
The subobject classifier [math]\Omega[/math] is the map from 1 to [math]\Omega[/math], such that for all monomorphisms j, there is a unique representative [math]\chi_j[/math] such that the diagram commutes.
A topos is a cateogry with products where there is an [math]\Omega[/math], i.e. where you can abstractly speak of sub-object.
>>7887401
To add to the definition in (>>7887340)
In the cateogry of sets [math]\Omega = \{0,1\}[/math] and it classifies in that [math]Hom(-, \Omega)[/math] is the functor that maps any object X to the set [math]Hom(X, \Omega)[/math], which is [math]\{0,1\}^X[/math], which is in bijection with the power object.
So if you got an abstract [math]\Omega[/math], you can speak of the power object.
Btw. I said "so that the diagram commutes", while actually it's a little stronger, the diagram must be a pullback (which means that U is full but minimal). The definition of pullback is just a little more complicated than "monomorphism".
>>7887179
Okay, I've always thought that "a monad is just like a burrito" is a Haskell meme, referencing the various monad tutorials using shitty analogies - culminating in this: https://www.cs.cmu.edu/~edmo/silliness/burrito_monads.pdf April Fool's paper. So is the meme originally from ctegory theory, or is the "taco" referencing something else?
>>7884849
As someone who has a bit of a background in Hegel (through Marx) and is just getting into category theory, this is a huge incentive to keep studying. Cool link, and great thread all.
>>7889404
I don't know why this anon posted this gimmick example, the crazy shit is here
https://ncatlab.org/nlab/show/Science+of+Logic
But beware, David and Urs are the only people looking at this, motivated by Lawvers thoughts two decades ago. And they mostly do it to generate ideas, otherwise they do math
>>7889429
>https://ncatlab.org/nlab/show/Science+of+Logic
It's fine with me if no one is really working on this. I'd like to learn a bit about category theory anyways, since I'm planning on going into CS or math in college, hopefully alongside philosophy. The crazy Hegel interpretations are just good for keeping me excited and wanting to learn more. Speaking of which, just downloaded a copy of Goldblatt!
>>7874726
the semantics of the internal language is a generalization of forcing. for any geometric theory you can take the models in any grothendieck topos in a systematic way preserved by geometric morphisms.
anything stateable in the mitchel-benabou language (effectively higher-order logic with lambda abstraction) can be interpreted in any topos, but don't expect it to be preserved in any useful sense between toposes.
topos theory, like topology, has more been about "when" or "where" does something hold (in what kind of topos) over "is this thing independent for the fixed topos E" - such as Set
bupm
boop
Last bump.
