Category Theory For Beginners: Topos Theory Essentials

In this video we introduce topos theory in a systematic way, before going for a faster less rigorous tour of some of the deeper ideas in the subject. We start by introducing the idea of a subobject classifier, and how it lets us link ideas about subobjects and logic. We define an elementary topos. We define logical AND, IMPLIES, and FOR ALL. We prove many results interrelating these ideas. Next we discuss other logical notions like FALSE, NOT, and OR. We also discuss epimorphism-monomorphism factorization. Finally, we quickly tour deeper ideas in topos theory, like the idea of forming a Heyting algebra by ordering an object's subobjects by containment. We also discuss notions like the fundamental theorem of topos theory, about how every slice category formed from a topos is also a topos.

Here are some more videos exploring more aspects of topos logic:

Understanding False and Not

More results about exponential and power objects

"If then" statements in a topos

Implications of implication 1

Regarding the latter, the result expressing when an arrow w is in [q double-arrow r] , in terms of when [w after [the pullback of q along w]] is in r, can be used together with the Yoneda lemma to determine the D-type elements of [q double-arrow r], in the category of functors from C to Set (for an object D of C).

Correction at time 3:32:12
In fact, I do not think (w times 1_A) is always monic, so I should write
(w times 1_A) in r, rather than (w times 1_A) contained in r, within Theorem 13.9.

A proof of Theorem 13.9 can be found here
"Universal Quantification Proof"

Proofs involved in the first part of the video (up until and including the discussion of power objects), can be found in the following four videos:

Here is a link in the description
to a video explaining how to
construct subobject classifiers
and exponential objects for a category of functors from C into Set (for some category C)

Proofs of the results about when arrows are in arrows into power objects can be found here:

An (rough) introduction to the Mitchell-Bénabou language can be found in the following videos (I will probably release a higher quality video on this topic later):

An attempt to explain how the a partial ordering can be associated with a power object, to form an internal Heyting Algebra can be found here:

A very rich set of examples of applications can be found in this series of videos
on categories of structured sets:

coequalizer documents and videos

Geometric Morphisms

[JosiahWarren]

Thank you for your contributionnon popularizing category theory.

[gucker]

6 hours! Intimidating :-)
Thank you for your work!

[xyzct]

Awesome. I'll have time this weekend to dive in.

[asalamkamal]

Allah bless your efforts I hope you will continue to create educational content ❤️

[MasonBiamonte]

I bought your book with Gupta. I'm working on a functorial approach to quantum gravity that I think is a good idea. Would love to get in contact with you so we could share ideas.

[anshanshtiwari]

Is it possible for you to trim this into six ~one hour long videos? It is a very intimidating. I will watch it regardless, just a small suggestion. :)

[alexanderlind]

Does this video overlap with your "Topos theory and subobjects"-video or is there a preferred order of viewing?

[him]

What is the difference between in and contained in? You've defined the subset relation and the in relation in exactly the same ways

[ronritekinamatigai]

I kind of understand the idea, but how do you formally define a morphism h:H→B being an element of a monomorphism m:A→B, that you write as h∈m?
Edit: an, I think I found the answer myself, h∈m defined as: there is a morphism g:H→A, such that h = mg, right?

[him]

Is topos theory relevant to an undergraduate student? How does it relate to other areas of mathematics _other than foundations, set theory and logic_? (Which aren’t deeply relevant to most mathematicians)

[Achrononmaster]

@17:58 whoa man! Squaring an infinitesimal to "get zero" seems highly dubious. Zero relative to what? In the hyperreals we already have that sort of thing. Surely topos theory can plumb some of the Surreal Number concepts too, which basically are generalizing reciprocality. When you understand the transfinite cardinals just "go on forever" in ever higher cardinality, then the same must be true for infinitesimals... there can be no smallest type of infinitesimal. If you can square one of them and get literal zero it just means you've coarse grained too much and have filtered out "smaller" infinitesimals (thought of as reciprocals of higher transfinites). This, to my mind, is the real challenge for our generation, how to get some symmetry between the infinite hierarchy of transfinites and an equally infinite hierarchy of infinitesimals. If Conway did not truly complete that program with the Surreals, someone else will, or "should" (if there is such a thing as moral "aught" in sociology of mathematics!). Only then will we have any claim to have "understood" _the continuum_ (as a coherent meaningful concept).
If you cannot identify (in principle) a unique generalized reciprocal of some arbitrary transfinite cardinal, then you've (I claim) missed a vast infinite class of infinitesimals (or you've glombed them together barbarically, so-to-speak).

[ohault]

Beyond set, does topos could help to support concept like indeterminism in non-classical logics ?

[Achrononmaster]

Mathematically you can maybe get a "perfect language" (whatever that means) but not humanely universal. Mathematics is a lot more like engineering than some pristine idealized heaven of reasoning. Topos and Cat theory likened to rivets, nuts, bolts, wiring, while most mathematicians will appreciate knowing that sort of stuff glues things together, they'll be working at a higher level on things like (metaphorically) chassis, engine blocks, whole vehicles, whole microchips, modular robots, etc. If not then they'll be making no progress in their field.