topos theory repository

Stream: mathlib4

[Charlie Conneen]

Almost a year ago I asked this question about whether there was any topos theory in mathlib4. Last summer I spent some time working on formaliziing some results, and have just recently made the repo public after updating the code for the recent Lean 4.15 update. My hope is to make this code good enough to PR to mathlib4, but I haven't had much time until now to do that. If there is any interest, I would love any collaboration, suggestions, or critiques of the existing code.

[Johan Commelin]

Nice! From a very first skimming through the code, I can say that this looks ready to for entering the PR/review process.
Well done!

[Kevin Buzzard]

How close are you to proving that a grothendieck topos (or just sheaves on a topological space) is a topos in your sense?

[Pablo Donato]

well done @Charlie Conneen! I have been myself working on a formalization of subobject classifiers lately (available here), and I noticed your repo includes one. There are some subtle differences in the choices of names and formulations, especially for the property you call classifying that corresponds to IsClassifier in my formalization. My choices were aimed at the proof of Proposition 1 in Section I.3 of Sheaves in Geometry and Logic, which is completed at around 40% I would say. I think your development does not include this theorem (nor the definition of the subobject presheaf $\mathrm{Sub}$), so those parts are not overlapping at least.

Naturally if we are to incorporate one of our developments into mathlib, we will need to settle on a canonical definition for the subobject classifier, and adapt our proofs consequently. Thus I would be interested in discussing our respective formalization choices so that we can converge on something :)

[Charlie Conneen]

@Kevin Buzzard It hasn't been a current priority (there are at present no instances of Topos C), but it shouldn't be too far afield.

[Charlie Conneen]

@Pablo Donato Ah, very nice! It seems there is indeed little overlap in our code's content. My results are focused on the content of chapter 4 of the text.

I'm not overly attached to the existing formalism. The implementation is an adaptation of @Bhavik Mehta's implementation in the Lean 3 library. If you have some concrete reason why you think a different formalism makes proving results easier, I'm all ears. Although, your IsClassifier definition seems to be equivalent to the IsSubobjectClassifier structure in my code; classifying is just a helper struct which contains the data that the associated diagram is a pullback, and says nothing about the uniqueness.

[Pablo Donato]

ah yes sorry I meant IsSubobjectClassifier instead of classifying

[Pablo Donato]

so let me list the differences I've noticed one-by-one:

1. My naming scheme is to avoid expliciting Subobject in the name of definitions (e.g. IsClassifier instead of IsSubobjectClassifier), since I put them in the CategoryTheory.Subobject namespace
2. IsClassifier is defined as a $\Pi$-type rather than a structure, by bundling the classifier and its properties in a subtype endowed with the Unique class. Also the helper classifying is avoided by reusing CategoryTheory.IsPullback
3. the canonical subobject classifier (that you call t and I call true!) being a mono is an assumption in my formalization, but a proved fact in yours
4. your HasSubobjectClassifier I call Classifier, because I reserve the name HasClassifier for the idiomatic construction using Nonempty

I am no expert in mathlib (this is my first tentative contribution), but I would say 1. and 4. are more idiomatic in my formalization, 2. is more compact in mine but maybe less idiomatic (although it reuses more existing definitions), 3. is obviously better in yours

But maybe I am getting ahead of myself, and these considerations should be kept for the PR review :)

[Charlie Conneen]

These seem reasonable. I will probably toy with refactoring in some of these respects at some point. It would mostly be a matter of editing the convenience lemmas, since the data is the same either way.

[Charlie Conneen]

Following up on this -- I am preparing to make a PR, but need write access to non-master branches of mathlib4 (as suggested in this document). My github username is CharredLee (linked here).

[Kevin Buzzard]

Can you add your github username to your Zulip profile? Sorry, this extra instruction is on the way!

[Charlie Conneen]

Absolutely. I just did this.

[Kevin Buzzard]

Invitation sent!

[Charlie Conneen]

I have made a pull request. It is located here. I followed the instructions located here. Hopefully my PR formatting is acceptable; I followed this guide as closely as possible. It took a bit to figure out how to make the linter happy, but the process for doing that is more clear now.

[Charlie Conneen]

I'll have to configure my LSP to remove whitespace at the end of lines :lol: that was one of the build issues I ran into because I use neovim. In any case, please let me know what the next steps are.

[Nick Ward]

@Charlie Conneen you may find some help on the lean.nvim channel! Also, a more conventional PR title would be exactly what you have written in the description (feat(CategoryTheory/Topos): topos theory content)

[Charlie Conneen]

Ah, thanks. I clearly misunderstood which fields corresponded to which data.

[Kim Morrison]

It's helpful if you link to PRs using the linkifer, i.e. as #21269. Then you get automatic emoji status updates from a bot!

[Charlie Conneen]

Oh neat, thank you!

[Charlie Conneen]

I've edited the PR title. At the suggestion of one of the reviewers, I'll be editing the PR to be just the content of Classifier.lean. That should be up in a bit, after I finish adapting everything to fit the naming conventions.

[Ben Eltschig]

I think what Joël suggested is that you keep the PR as it is, make a new PR with just the contents of Classifier.lean and then return to this PR once the smaller one is merged :)

[Charlie Conneen]

Ah, that makes more sense. Thanks.

[Charlie Conneen]

OK, I've made a new PR which can be found here: #21281. Hopefully everything matches the standard naming conventions in CategoryTheory/Topos/Classifier.lean now.

[Bhavik Mehta]

Charlie Conneen said:

Pablo Donato Ah, very nice! It seems there is indeed little overlap in our code's content. My results are focused on the content of chapter 4 of the text.

I'm not overly attached to the existing formalism. The implementation is an adaptation of Bhavik Mehta's implementation in the Lean 3 library. If you have some concrete reason why you think a different formalism makes proving results easier, I'm all ears. Although, your IsClassifier definition seems to be equivalent to the IsSubobjectClassifier structure in my code; classifying is just a helper struct which contains the data that the associated diagram is a pullback, and says nothing about the uniqueness.

Feel free to request my review on these PRs: I'm sure it is no surprise that I think my implementation was a pretty good one, but there are still certainly things which should be updated from it!

[Charlie Conneen]

Thank you Bhavik for your additional comments on the new PR. I have made the suggested first round of changes. I also renamed the namespace to MonoClassifier to distinguish it from the potential Subobject.Classifier to come later (as well as to resolve name duplication conflicts with the newly renamed MonoClassifier.Classifier). The only thing I'm not sure about is that the linter is angry that the autogenerated lemma MonoClassifier.comm_assoc from the @[reassoc] tag. Is this something to worry about?

[Nick Ward]

@Charlie Conneen not ordinarily, but I'm not sure how the linter usually avoids flagging @[reassoc] lemmas. Did CI give you a linter error, or just running the linter locally?

[Nick Ward]

It looks to me like the CI error was just caused by #lint docBlameThm printing to stdout. Maybe try pushing with @[reassoc] but deleting the linter invocation and see what CI says.

[Charlie Conneen]

I hadn't checked what was causing the CI error, I was just noticing the error locally. Thanks, you're right, the build doesn't mind an auto-generated lemma not having a docstring.

[Pablo Donato]

Hi all @topic,

I wanted to notify you that I have successfully formalized the (proof of) the representation theorem for subobject classifiers (Proposition 1 p.33 of SGL), and that I now intend to make a pull request to mathlib. You can take a look at the code here (theorem CategoryTheory.Subobject.hasClassifier_isRepresentable_iff), although I am going to refine it a little bit with comments and probably corrections with respect to naming conventions before making the PR. I am also going to ask immediately for branch access in #mathlib4 > github permission, as up to now I have worked on a separate repo.

I have already discussed with @Charlie Conneen about some formalization choices, and I am aware of their definition of MonoClassifier.Classifier. In the end I chose to stick with my initial definition of Subobject.Classifier. Here are some reasons why (long explanations ahead, beware):

• Extensionality: the main reason is that I absolutely need the extensional version of subobject classifiers, i.e. the one that sends subobjects to their characteristic map, not monomorphisms. I have spent some time tinkering with the intensional definition that maps monos, which corresponds to Charlie's MonoClassifier.Classifier (and the definition in SGL I believe); I choose to call it "monomorphism classifier" to avoid ambiguity. I recorded the experiments in the file MonoClassifier.lean. My conclusion is that there is one big hurdle with that definition that makes it impossible to prove any representation theorem for it: there is no way to define a Mono X presheaf of monomorphisms over X that would be analogous to the Sub X presheaf of subobjects of X, because the MonoOver.pullback functor only preserves identities and compositions up to isomorphism (see MonoOver.pullbackId and MonoOver.pullbackComp). This is precisely why one needs the notion of subobject to "strictify" the category of monos into a skeletal one. I find it very confusing and unfortunate that in SGL they freely interchange monos and subobjects "by a familiar abuse of language", as this makes the statements of definitions and theorems unclear, and hides a lot of the complexity of proofs under the rug.
• Terminal object: I chose to incorporate the existence (and choice of a) terminal object as an assumption [HasTerminal C], instead of deducing that $\Omega_0$ is terminal from the definition of Classifier (as is done in @Bhavik Mehta's formalization in Lean 3; it looks like it has now changed in Charlie's port). This makes definitions more concise by avoiding to carry around the extra $\Omega_0$ and does not complicate the proof of hasClassifier_isRepresentable_iff, although it is arguably less elegant.
• Data types and notations: I have a slightly different way to package the data, which should be easily refactorable if required. For instance, I define IsClassifier as a $\Pi$-type rather than a structure since it has just one field, and I note the truth morphism true! instead of t. I have no problem aligning with Charlie's presentation, I guess we just need to settle on unified conventions.

Sorry if this discussion was too detailed and should have been kept for the PR, but now it's off my mind :)

[Charlie Conneen]

There has been much discussion about naming conventions in #21281. A lot has been changed since our last discussion. You might have a look at that code. It will probably not take much to align our definitions, but at some point our results will definitely overlap.