Topoi in Mathlib

Stream: new members

[Coleton Kotch]

It seems we do not have topoi in mathlib, has anyone made progress or worked on formalizing them or is this something a person could work on? It seems there are no branches of mathlib with topoi or topos in the name at least.

[Luigi Massacci]

This may interest you

[Nick Decroos]

IIRC, there is no topos theory in mathlib4 at the moment.
Apart from the mathlib4 repository:
Bhavik Mehta's topos repository

This repository contains formal verification of results in Topos Theory, drawing from "Sheaves in Geometry and Logic" and "Sketches of an Elephant".

[Yaël Dillies]

Yes, @Bhavik Mehta is our local topos expert and you two should talk

[Adam Topaz]

@Coleton Kotch what do you want to do with topoi? If you’re happy to use Grothendieck topoi then you can just use the category of (type-valued) sheaves on a site for now.

[Adam Topaz]

As far as I know, mathlib doesn’t yet know about subobject classifiers. I think that’s some low hanging fruit that someone could work on right away.

[Coleton Kotch]

I wasn’t looking at doing anything too fancy with topoi. I was thinking about aiming to formalize the etale fundamental group and felt we should probably have sites and Grothendieck topologies first.

[Johan Commelin]

Those we do have.

[Johan Commelin]

As well as a bunch of stuff on Galois categories

[Anthony Bordg]

Coleton Kotch said:

It seems we do not have topoi in mathlib, has anyone made progress or worked on formalizing them or is this something a person could work on? It seems there are no branches of mathlib with topoi or topos in the name at least.

@Coleton Kotch
Our group has started a formalization of toposes and we're waiting for being granted permission to make the code open-source. In particular, we learned today the permission should be granted on July 26, then I will open a non-master branch to share our code. You will be welcome to participate if you wish so.

[Johan Commelin]

@Anthony Bordg Just to clarify: this will be elementary toposes?

[Anthony Bordg]

Johan Commelin said:

Anthony Bordg Just to clarify: this will be elementary toposes?

@Johan Commelin no, Grothendieck toposes.

[Johan Commelin]

oh ok... but then mathlib has quite a lot already, right?

[Adam Topaz]

We don't yet have Giraud's axioms in mathlib (yet), as far as I know. Maybe that's what @Anthony Bordg and his group are working toward?

[Anthony Bordg]

Johan Commelin said:

oh ok... but then mathlib has quite a lot already, right?

Since a Grothendieck topos has infinitely many presentations, we do not want a definition tied to a specific presentation.

[Anthony Bordg]

I'm glad to announce that we were granted permission yesterday for making this project open-source and contribute our code to mathlib. I open a first PR #14908, hopefully more to come :)

[Adam Topaz]

@Anthony Bordg I left a few comments on your PR. The main points are: (1) the names you chose unfortunately don't follow mathlib's naming conventions. We have an explanation here. (2) A few proofs have nonterminal simps, and several tactics on a single line, which, again, we try to avoid in mathlib. Some of these points are explained in this page.

[Anthony Bordg]

In CoveringFamilies, I'm working on CoveringFamilies.GeneratedTopology, the Grothendieck topology J generated by a collection of covering families cf by the formula

sieves X S := ∃ P ∈ cf.basis X, generate P ≤ S.

I know how to prove transitivity' for J on paper, but I'm unsure how to proceed in Lean. Given $R\in \Omega(X)$ and $S\in J(X)$ such that $f^\star(R) \in J(X')$ for every morphism $f: X' \rightarrow X$ in $S$, there exists $Q_f \in \text{basis}\, X'$ satisfying $\text{generate}\, Q_f \leq f^\star(R)$, thus by multicomposition_stable we have P.bind Q ∈ basis X, where P comes from the assumption $S\in J(X)$ and Q is defined as

$$Q \,X'\, f\, (p: P\,f) := Q_f.$$

Since P.bind Q \leq R, one concludes $R\in J(X)$.
How to define Q in this situation in Lean?

[Junyan Xu]

Is the choose tactic what you want?

[Edward van de Meent]

or, to avoid using tactics, the lemma docs#Exists.choose (along with docs#Exists.choose_spec )?

[Dagur Asgeirsson]

Have you looked at docs#CategoryTheory.Coverage.Saturate and docs#CategoryTheory.Coverage.toGrothendieck? Your CoveringFamilies is a coverage (pullback-stable), so you might want to define CoveringFamilies.GeneratedTopology using this API, and then prove a theorem that the covering sieves are precisely the ones that contain a sieve of the form generate P where P is in the basis. It's mathematically the same as proving that your CoveringFamilies.GeneratedTopology is a Grothendieck topology, but you will have access to the induction of docs#CategoryTheory.Coverage.Saturate, which might be convenient.

For an example of how to use this API (the inductive principle) you could take a look at docs#CategoryTheory.extensiveTopology.mem_sieves_iff_contains_colimit_cofan

[Anthony Bordg]

Good to know! I will have a look as soon as possible.

[Adam Topaz]

CategoryTheory.Coverage.toGrothendieck_eq_sInf is probably also relevant if you would like to switch to using coverages.

[Anthony Bordg]

Adam Topaz said:

Anthony Bordg I left a few comments on your PR. The main points are: (1) the names you chose unfortunately don't follow mathlib's naming conventions. We have an explanation here. (2) A few proofs have nonterminal simps, and several tactics on a single line, which, again, we try to avoid in mathlib. Some of these points are explained in this page.

@Adam Topaz @Yaël Dillies A big thank you. Leaned quite a lot during the process, hopefully will be smoother next time. I'm going to rework covering families based on the API for coverages mentioned by @Dagur Asgeirsson .

[Yaël Dillies]

Glad you didn't hate it :blush: I promise I will be less nasty next time :innocent:

[Anthony Bordg]

Dagur Asgeirsson said:

Have you looked at docs#CategoryTheory.Coverage.Saturate and docs#CategoryTheory.Coverage.toGrothendieck? Your CoveringFamilies is a coverage (pullback-stable), so you might want to define CoveringFamilies.GeneratedTopology using this API, and then prove a theorem that the covering sieves are precisely the ones that contain a sieve of the form generate P where P is in the basis.

@Dagur Asgeirsson Is it what you had in mind?

universe u v

open CategoryTheory Sieve

variable (C : Type u) [Category.{v} C]

/-! ### The notion of covering families -/

structure CoveringFamilies extends Coverage C where
  retraction_mem : ∀ ⦃X Y : C⦄ ⦃f : Y ⟶ X⦄, IsSplitEpi f → Presieve.singleton f ∈ covering X
  heredity : ∀ ⦃X : C⦄ (P : Presieve X), (∃ Q, Q ∈ covering X ∧ Q ≤ generate P) → P ∈ covering X
  multicomposition_stable : ∀ ⦃X : C⦄ (P : Presieve X)
    (Q : ∀ ⦃Xi : C⦄ ⦃f : Xi ⟶ X⦄, P f → Presieve Xi), P ∈ covering X →
      (hQ : ∀ ⦃Xi : C⦄ ⦃f : Xi ⟶ X⦄ (p : P f), Q p ∈ covering Xi) → P.bind Q ∈ covering X

variable (cf : CoveringFamilies C)

namespace CoveringFamilies

def GeneratedTopology : GrothendieckTopology C := cf.toGrothendieck

theorem covering_of_generatedTopology_iff {X : C} (S : Sieve X) :
    (GeneratedTopology C cf).sieves X S ↔ ∃ P ∈ cf.covering X, generate P ≤ S := by admit

end CoveringFamilies

[Dagur Asgeirsson]

Yes, exactly

[Anthony Bordg]

Do you know why I'm unable to use use Presieve.singleton (𝟙 X); split in the proof of the case | top X below

theorem covering_of_generatedTopology_iff {X : C} (S : Sieve X) :
    (GeneratedTopology C cf).sieves X S ↔ ∃ P ∈ cf.covering X, generate P ≤ S := by
  constructor
  · intro hS
    induction hS with
    | of X S hS => use S, hS
    | top X => refine ⟨Presieve.singleton (𝟙 X), cf.retraction_mem (IsSplitEpi.of_iso (𝟙 X)), by
        rw [generate_of_singleton_isSplitEpi (𝟙 X)]⟩
    | transitive X R S _ _ _ _ => sorry intro hS
    rw [← CategoryTheory.Sieve.generate_sieve S]
    have : S.arrows ∈ cf.covering X := by
      apply cf.heredity
      rw [CategoryTheory.Sieve.generate_sieve S]
      rcases hS with ⟨P, h1P, h2P⟩
      use P, h1P
      apply LE.le.trans (le_generate P)
      exact h2P
    apply Coverage.Saturate.of X S
    simpa

[Adam Topaz]

can you post a #mwe please?

[Anthony Bordg]

import Mathlib.CategoryTheory.Sites.Coverage

universe u v

open CategoryTheory Sieve

variable (C : Type u) [Category.{v} C]

structure CoveringFamilies extends Coverage C where
  retraction_mem : ∀ ⦃X Y : C⦄ ⦃f : Y ⟶ X⦄, IsSplitEpi f → Presieve.singleton f ∈ covering X
  heredity : ∀ ⦃X : C⦄ (P : Presieve X), (∃ Q, Q ∈ covering X ∧ Q ≤ generate P) → P ∈ covering X
  multicomposition_stable : ∀ ⦃X : C⦄ (P : Presieve X)
    (Q : ∀ ⦃Xi : C⦄ ⦃f : Xi ⟶ X⦄, P f → Presieve Xi), P ∈ covering X →
      (hQ : ∀ ⦃Xi : C⦄ ⦃f : Xi ⟶ X⦄ (p : P f), Q p ∈ covering Xi) → P.bind Q ∈ covering X

variable (cf : CoveringFamilies C)

def GeneratedTopology : GrothendieckTopology C := cf.toGrothendieck

theorem covering_of_generatedTopology_iff {X : C} (S : Sieve X) :
    (GeneratedTopology C cf).sieves X S ↔ ∃ P ∈ cf.covering X, generate P ≤ S := by
  constructor
  · intro hS
    induction hS with
    | of X S hS => use S, hS
    -- tactic 'split' failed, consider using `set_option trace.split.failure true`
    | top X => use Presieve.singleton (𝟙 X); split
    | transitive X R S _ _ _ _ => sorry

[Adam Topaz]

you should use constructor instead of split here

[Adam Topaz]

split is for breaking up ite and pattern matches.

[Anthony Bordg]

Is not split use for proving goal of the form ⊢ P ∧ Q?

[Yakov Pechersky]

In lean3, but it doesn't something else entirely in lean4

[Yakov Pechersky]

The equivalent tactic to lean3's split is lean4's constructor

[Anthony Bordg]

PR #15224

[Anthony Bordg]

I have a conflict in lake-manifest.json.

<<<<<<< AnthonyBordg_covering_families
   "rev": "ac82ca1064a77eb76d37ae2ab2d1cdeb942d57fe",
=======
   "rev": "e7897807913fafdab31b01b9f627550bcc96cff2",
>>>>>>> master

What am I supposed to do ?

[Yaël Dillies]

Drop your change. I don't see why you would need to update lake-manifest.json in this PR?

[Anthony Bordg]

Indeed. Which line(s) to delete?

[Yaël Dillies]

If you've done git merge, the top ones. If you've done git rebase, the lower ones.

[Damiano Testa]

Likely, keeping the one closest to master is the correct choice! :smile:

[Anthony Bordg]

Done. Thanks.

[Anthony Bordg]

Anthony Bordg said:

PR #15224

It's relatively short, ~80 lines of actual code :wink:

[Dagur Asgeirsson]

I left a few comments

[Anthony Bordg]

What would be a short, but not too short, first PR on toposes for quickly getting some feedback and for ease of handling PRs by reviewers? Probably not the def alone? What about the partial order on subtoposes of a given topos?

[Dagur Asgeirsson]

Whenever you contribute something (say a definition of a topos), it's always good to try to relate it to existing notions in the library (if you define a typeclass Topos, this could for example be to give a Topos (Sheaf J Type) instance).

Note that relating your material to existing notions in the library doesn't need to happen in the same PR. However, it's good to point to it already in the initial PR (the way to do this is to open a big PR with the significant contribution, and then split it up into smaller PRs, referencing the big one to say "look, this small contribution Y is useful to prove X")

It's difficult to suggest something to contribute without knowing what you have already formalized. Can you point to a public repo or is your code private?

[Dagur Asgeirsson]

For example, if you had a followup PR to #15224 where CoveringFamilies is applied to do something which shows some advantage of it over GrothendieckTopology, we probably wouldn't be as hesitant to merge it.

[Anthony Bordg]

Dagur Asgeirsson said:

Can you point to a public repo or is your code private?

Will put some code soon in a non-master branch, since this is apparently the workflow.

[Anthony Bordg]

I'm wondering about the best workflow.
Having a separate public Github repo, where collaborators can work in parallel on different files, and having a single non-master branch opened at any time on mathlib4 for the next submission ? Or no need for an external repo and just work with non-master branches, possibly a few opened simultaneously to work on files that are independent from each other or to limit the size of PRs?
Some inputs?

[Yaël Dillies]

The model I have been using for LeanAPAP, PFR, GibbsMeasure, etc... works great (for me and my collaborators). It consists of:

• a external public repository MyProject where everyone has push access (except in PFR where we worked with PRs).
• a MyProject.Mathlib folder mirroring the Mathlib arborescence. The rule is that file MyProject.Mathlib.X only imports Mathlib.X + possibly MyProject.Mathlib.Y where Mathlib.X transitively mports Mathlib.Y.
• a MyProject.ForMathlib folder containing code that should eventually be in Mathlib and is more or less ready for inclusion, but doesn't fit in an existing Mathlib file.
• The rest, containing the unfinished stuff along with the code that should never be in Mathlib.

[Yaël Dillies]

I would discourage you from using Mathlib branches for development as:

1. They are harder to track than both a single external repo and open PRs.
2. You can't host a blueprint alongside it.
3. It's less externally visible. In particular it won't show up on Reservoir.

[Kevin Buzzard]

This very much depends on the scale of the project. I should think branches are fine for smaller developments, for example my experiments with Frobenius elements are on a branch https://github.com/leanprover-community/mathlib4/pull/14155

[Anthony Bordg]

Thank you Yael and Kevin for sharing your experience. Yesterday, I set up an external public repo Topos-Theory.

[Anthony Bordg]

I sketched a definition of topos in the mwe below.
I want to prove that a category of sheaves is a topos. For this, and given my presentation field, I want to reuse the site that comes with this category of sheaves, but there is something fishy with universes, can someone help me figure out the explicit universe declarations required to fix this?

import Mathlib.CategoryTheory.Sites.Sheaf
import Mathlib.CategoryTheory.Equivalence

open CategoryTheory

variable {C : Type*} [Category C]

/-! ### Grothendieck toposes -/

variable [SmallCategory C] (J : GrothendieckTopology C)

namespace InducedPresentation

variable {E : Type*} [Category E] [LocallySmall E] (l : C ⥤ E)

theorem isSheaf_of_induced_presentation (X : E) : Presheaf.IsSheaf J (l.op ⋙ yoneda.obj X) := by admit

def inducedPresentation : E ⥤ Sheaf J Type* where
  obj := fun X => ⟨l.op ⋙ yoneda.obj X, isSheaf_of_induced_presentation J l X⟩
  map := fun f => ⟨whiskerLeft l.op (yoneda.map f)⟩

end InducedPresentation

open InducedPresentation

class Topos (ℰ : Type*) [Category ℰ] [LocallySmall ℰ] : Prop where
  presentation : ∃ (C : Type*) (_ : SmallCategory C) (J : GrothendieckTopology C) (l : C ⥤ ℰ),
    Functor.IsEquivalence (inducedPresentation J l)

variable {A : Type*} [Category A]

instance : Topos (Sheaf J A) where
  presentation := by
  /- type mismatch C has type Type u_1 : Type (u_1 + 1) but is expected to have type Type u_4 : Type
  (u_4 + 1)Lean 4 -/
    use C

Also, since mathlib doesn't require the underlying category of a site to be small, I realise that some of the assumptions in the file, e.g. SmallCategory C or even LocallySmall ℰ may not be needed.

[Joël Riou]

I think that you need to clarify what to do with universes. Presumably, Topos should take only one universe parameter u, and a Topos.{w} should then be a category that is equivalent to Sheaf J (Type w) with J a Grothendieck topology on a small category C : Type w.

[Joël Riou]

(More precisely, if E : Type u and Category.{v} E, then E satisfies Topos.{w} if it is equivalent to Sheaf J (Type w) for some J on a small category C : Type w.)

[Anthony Bordg]

Thank you, Joel.

Joël Riou said:

I think that you need to clarify what to do with universes.

Indeed! I'm not used to handling universes, but your answer helps.

A few remarks:

• Mathlib doesn't require the underlying category of a site to be small, so I certainly can drop my hypothesis [SmallCategory C]
• I believe [LocallySmall E] is not required here for inducedPresentation to be well-defined, contrary to what happens on paper, since one can specify the universe level as in E ⥤ Sheaf J (Type v).
• I should use Type w instead of variable {A : Type w} [Category A], as you did, to avoid the unnecessary instance Category A and benefit from the instantiated categorical structure of Type w.

[Joël Riou]

I do not understand isSheaf_of_induced_presentation: without further assumptions, this seems wrong to me. Also, a category of sheaves in an arbitrary A may not be a topos in general.

The definition I would do for Topos would be this:

universe w v u

class Topos (E : Type u) [Category.{v} E] : Prop where
  exists_equivalence : ∃ (C : Type w) (_ : SmallCategory C)
    (J : GrothendieckTopology C), Nonempty (E ≌ Sheaf J (Type w))

instance (C : Type w) [SmallCategory C] (J : GrothendieckTopology C) :
    Topos.{w} (Sheaf J (Type w)) where
  exists_equivalence := ⟨C, inferInstance, J, ⟨Equivalence.refl⟩⟩

This is SGA 4 IV 1.1.

Using some work by @Dagur Asgeirsson on equivalences of sheaf categories, we may get slightly more general instances (when the category C has more general universe parameters and w is a big enough universe), but for the definition of a topos, I believe this is the most correct definition.

[Anthony Bordg]

Why assuming that C is a small category if a category of sheaves in mathlib is not a category of presheaves on a small index category?

[Dagur Asgeirsson]

The definition of the category of sheaves in mathlib doesn't require the defining site to be small, simply because the notion of a sheaf on a large site may be interesting/useful (e.g. condensed sets). However, you're trying to define what it means to be a Grothendieck topos, and indeed the standard definition there requires the defining site to be small.

Is this not the definition you have in mind? It helps to have a clear mathematical idea beforehand of the concept you're trying to formalize.

[Joël Riou]

Anthony Bordg said:

Why assuming that C is a small category if a category of sheaves in mathlib is not a category of presheaves on a small index category?

If the category is large, e.g. C : Type (u + 1) and morphisms in Type u (or more), we may still consider the category of sheaves of C with values in Type u, but it may not behave properly (sheafification may involve colimits in Type u indexed by a category in Type (u + 1), which may not exist). In mathlib, without universe assumptions, we have typeclasses asserting that it behaves not so badly (e.g. we have a sheafification functor). I believe not all such categories of sheaves deserve to be named topos, only those that are equivalent to a category of sheaves in the most favourable case should be (I am not expert in topos theory though). Then, for example, if C is a small category in Type u, we may consider the topos of sheaves with values in Type u, but we may also consider the category of sheaves with values in Type (u + 1), which does not obviously satisfy my definition (for w := u + 1), but as C is equivalent to a small category in Type (u + 1), it shall satisfy my definition anyway thanks to Dagur's results in CategoryTheory.Sites.Equivalence.

[Adam Topaz]

Joël Riou said:

... I believe this is the most correct definition.

I completely agree with this definition. Alternatively, one could formulate a definition using Giraud's axioms (and in fact this is what I thought @Anthony Bordg had in mind originally).

[Bhavik Mehta]

Yes, this is also the definition I used in the topos project

[Anthony Bordg]

Is there a proposition IsFullyFaithful that corresponds to the type FullyFaithful in the same way there is a proposition IsEquivalence (in addition to the Equivalence type)?

[Dagur Asgeirsson]

There is just docs#CategoryTheory.Functor.Full and docs#CategoryTheory.Functor.Faithful

[Adam Topaz]

no, Full contains the data of a preimage

[Dagur Asgeirsson]

Adam Topaz said:

no, Full contains the data of a preimage

Not anymore

[Adam Topaz]

this is because it is often useful to have good defeq properties of the preimage

[Adam Topaz]

OH!

[Dagur Asgeirsson]

FullyFaithful contains the data of a preimage

[Adam Topaz]

I'm behind the times!

[Adam Topaz]

BTW, I think docs#CategoryTheory.Functor.IsEquivalence does still contain data?

[Adam Topaz]

No it doesn't!

[Adam Topaz]

Okay, I'm really behind the times here :)

[Anthony Bordg]

Joël Riou said:

I do not understand isSheaf_of_induced_presentation

I finally found the time to come back to this. Is it clearer now? Link

[Dagur Asgeirsson]

This seems unnecessarily complicated as a definition. What's wrong with using the definition suggested by Joël, that being a Topos means that there exists an equivalence with a category of sheaves of sets on a small site? That definition gives you a fully faithful functor to presheaves, a left adjoint (sheafification), etc.

If you want to go more in the direction of the approach you linked, then I think you mean something a bit different. Requiring the existence of a functor from the defining site to the topos seems too restrictive, don't you mean to just require the existence of a fully faithful functor to the category of presheaves? Not necessarily of the form associatedFunctor

[Dagur Asgeirsson]

At first glance, I thought you meant to write something like this with your definition of IsPresentation 

import Mathlib.CategoryTheory.Sites.Equivalence
import Mathlib.CategoryTheory.EssentialImage
import Mathlib.CategoryTheory.Limits.Preserves.Basic

namespace CategoryTheory

variable {E : Type u₁} [Category.{v₁} E]
variable {C : Type w} [SmallCategory C]

variable (J : GrothendieckTopology C)

open Presheaf Functor

class IsPresentation (i : E ⥤ (Cᵒᵖ ⥤ Type w)) : Prop where
  faithful : i.Faithful
  full : i.Full
  left_adjoint : ∃ (L : (Cᵒᵖ ⥤ Type w) ⥤ E) (_ : Limits.PreservesFiniteLimits L) (_ : L ⊣ i), True

end CategoryTheory

(although I would probably make the left adjoint part of the data of IsPresentation).

But looking more closely it seems like your doing something different. Is your definition mathematically correct? Are you following a source?

[Anthony Bordg]

Dagur Asgeirsson said:

This seems unnecessarily complicated as a definition. What's wrong with using the definition suggested by Joël, that being a Topos means that there exists an equivalence with a category of sheaves of sets on a small site? [...] Are you following a source?

It would be maybe a bit weird to talk for Laurent, the best is probably to invite him to share his motivations on this Zulip, something I will do.

[Anthony Bordg]

Dagur Asgeirsson said:

left_adjoint : ∃ (L : (Cᵒᵖ ⥤ Type w) ⥤ E) (_ : Limits.PreservesFiniteLimits L) (_ : L ⊣ i), True

end CategoryTheory

(although I would probably make the left adjoint part of the data of IsPresentation).

A remark wrt this, one can show that the functor denoted F in my code is necessarily left adjoint to the functor associatedFunctor l.

[Joël Riou]

In any case, it seems much safer to use the very simple definition given above. The IsPresentation property may have certain merits (mostly, I see it as a complicated way to encode an equivalence with a sheaf category), but this cannot be the definition. With probably some small design modifications (to include some data rather than only properties as Dagur observed), this could be a structure for which we could have a constructor in order to prove the Topos property.

[Laurent Lafforgue]

I suggested this definition of toposes to Anthony Bordg because we need to distinguish the abstract level of toposes and the concrete constructive level of their presentations. A topos is abstract by nature (in the sense that its objects and morphisms are defined only axiomatically, not constructively in general) and cannot be made fully explicit but it can be presented from concrete data consisting in small categories endowed with a topology. In fact, it is even always possible to choose for any topos E presentation categories C which are fully explicit in the sense that their objects are indexed by simple combinatorial data and the Hom sets between arbitrary pairs of objects are finite and computable. When presenting a topos E in terms of such a category C, the natural functor l from C to E can also be made fully explicit. Whereas its extension as a functor from C^ to E preserving colimits cannot be considered explicit as the objects and morphisms in a presheaf category C^ are defined axiomatically, not by a constructive process. The functor l from C to E is the fundamental structure through which abstract topos-theoretic definitions and constructions can get concrete expressions in terms of C and its topology corresponding to E. A topos is a category which is too big and too rich to be known but which can be defined from fully constructive data through the abstract axiomatic definition of sheaves and sheaf morphisms on a site. Anthony and myself propose to formulate in this way the definition of toposes because, for computational purposes, we need to always distinguish between what can be made constructive and what cannot be made constructive.

[Laurent Lafforgue]

By the way, this is also why the definitions of the notion of Grothendieck topology on a category C in terms of covering sieves or in terms of covering families of morphisms (or "presieves") are both worth formulating. They are indeed axiomatically equivalent but not constructively equivalent as, in general, the sieve generated by a family of morphisms cannot be computed. When one wants to make computations on topologies, it appears that most of the time the definition in terms of covering families of morphisms (or presieves) is preferable. In fact, except for very particular cases, a sieve is usually presented in terms of a generating family of morphisms.

[Dagur Asgeirsson]

We do have both: docs#CategoryTheory.GrothendieckTopology and docs#CategoryTheory.Coverage

[Adam Topaz]

If I understand correctly, given a presentation in Dagur's sense the functor C -> E would be the composition of the yoneda embedding with L (which admittedly would be defined with choice if one formulates the definition as Dagur did, but one could instead add L and the adjunction to the data as Dagur suggests). The difference between this and the approach of starting with C -> E is just in terms of the definitional properties of C -> E vs the presentation in terms of presheaves. To be able to control the definitional properties of all functors involved, one could add them all as data and include various isomorphisms and properties ensuring compatibility. Then one could provide constructors which let you start with just C -> E, or just E -> (C^op -> Type), etc.

[Adam Topaz]

Dagur Asgeirsson said:

We do have both: docs#CategoryTheory.GrothendieckTopology and docs#CategoryTheory.Coverage

Additionally it's relatively straightforward to go back and forth between presieves and indexes families with docs#CategoryTheory.Presieve.ofArrows

[Dagur Asgeirsson]

Regarding the definition of a topos: In mathlib, considerations like the ones you mention are not in general part of the definition of an object. We prefer simpler, more widely usable definitions. Then you can develop all the API you want around that definition

[Laurent Lafforgue]

If I understand correctly, a notion of "coverage" has to be stable under pull-back but is not required to verify the "stability" axiom of Grothendieck topologies. So the topology generated by a notion of coverage can have many more covering families than "coverages".

[Dagur Asgeirsson]

Yes, but the sheaf condition can be checked on the covering families of the coverage

[Adam Topaz]

That is this theorem: https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Sites/Coverage.html#CategoryTheory.Presieve.isSheaf_coverage

[Laurent Lafforgue]

The general problem of provability in first-order geometric logic is constructively equivalent to the general problem of generating topologies from given families of morphisms (see for instance : https://www.oliviacaramello.com/Talks/DeductiveSystemsGrothendieckTopologies.pdf). This means that the difference between a notion of coverage and the generated notion of covering presieve cab be as deep as the difference between the axioms of a first-order geometric theory and the results which can be provably deduced from these axioms.

[Adam Topaz]

The Grothendieck topology generated by a coverage is defined inductively in mathlib, unlike the definition one usually finds in books. This is probably much closer to the “provability” point of view.

[Laurent Lafforgue]

Dagur Asgeirsson said:

you

The Lean formalization system is intended for machine processing.
For machine computing, the distinction between what is constructive and what is not constructive seems very important.

[Adam Topaz]

Lean can also be used for computing. That’s not the focus of mathlib, but it is possible to do computations with the category theory library if one sets up the definitions in a suitable way

[Joël Riou]

Yes, and there can be an abstract definition of what is a topos, and at the same time, for more constructive definitions/theorems, the input could be a functor C ⥤ E (+ some extra data and properties packaged in a ToposPresentation structure).