Add Barr-exact, Barr-coexact, pretopos properties#103
Add Barr-exact, Barr-coexact, pretopos properties#103dschepler wants to merge 15 commits intoScriptRaccoon:mainfrom
Conversation
… some implications
…urns out the proof on ncatlab for categories monadic over Set requires the external axiom of choice on Set, so it will only generalize to elemetary topoi with choice
…cation topos->Barr-coexact, but are still cases of topoi with external axiom of choice
|
It would be better to separate the property "has effective equivalence relations" from "Barr-exact", because it appears in Diers's characterization theorem for multi-algebraic categories, which are in general not regular, hence not Barr-exact. |
|
It's worth adding "monadically concrete → cocomplete"; see, for example, Handbook of Categorical Algebra Vol. 2, Thm. 4.3.5. |
As it happened, I was just in the middle of adding "monadically concrete -> coproducts" which was what I remembered seeing a proof of. If arbitrary coequalizers exist as well, then I'm glad to update that. |
dschepler
changed the title
|
Perhaps rather than "monadically concrete", something like "infinitary algebraic" would be more conventional terminology? |
|
Thanks a lot for this PR! I will have a look at it. This may take a few days till we finish this. Can you perhaps tell me a bit how the setup went for you and if there is anything I can improve in the contribution guidelines and other documentation? Your feedback would be very helpful. Let me ask right away to split this PR into several, smaller PRs. (In particular, since it will grow when we fill in all the property assignments.) For example, we can have one PR that introduces "monadically concrete". I know that these properties are all connected with each other, but these connections can also be added one PR at a time. I wrote something about this (new) guideline also in the contribution guidelines: https://github.com/ScriptRaccoon/catdat?tab=contributing-ov-file#keep-pull-requests-focused Some remarks to the comments here:
We can add both and then add the theorem (proof) that they are equivalent (as an entry in the implications table). Why? For some categories it might be easier to show one, for some it's the other one. The deduction system takes care of the rest. This is what I did with filtered colimits <=> directed colimits, both are in the database, and https://catdat.app/category-implication/directed_colimits_suffice is their equivalence. The exact opposite approach has been done by @ykawase5048 in #97: here several definitions of properties have listed equivalent characterizations of it. This is also OK, but: then in every proof one has to specify which definition one is using.
I completely agree. Let's make this separate. (I have experienced this again and again while working on CatDat that it is best to extract properties.)
Yes, every monadic category over Set is cocomplete. The classical reference is: F. E. Linton. Coequalizers in categories of algebras. In Seminar on triples and categorical homology theory, pages 75–90. Springer, 1969.
Do you plan to fill in the missing data? Or parts of it? Same question for Barr-coexact and monadically concrete. |
| ( | ||
| 'monadically concrete', | ||
| 'is', | ||
| 'A category is <i>monadically concrete</i> if there exists a monadic functor to Set. Note this is not standard terminology, but is used in the CatDat system for its numerous implications.', |
There was a problem hiding this comment.
| 'A category is <i>monadically concrete</i> if there exists a monadic functor to Set. Note this is not standard terminology, but is used in the CatDat system for its numerous implications.', | |
| 'A category is <i>monadically concrete</i> if there exists a monadic functor to the category of sets. Note this is not standard terminology.', |
| 'Barr-exact', | ||
| 'is', | ||
| 'A category is <i>Barr-exact</i> if it is regular, and in addition, every internal equivalence relation is a kernel pair. (Note that because of the regularity condition, that is equivalent to being the kernel pair of a coequalizer of the two projections.)', | ||
| 'https://ncatlab.org/nlab/show/exact', |
There was a problem hiding this comment.
| 'https://ncatlab.org/nlab/show/exact', | |
| 'https://ncatlab.org/nlab/show/exact+category', |
There was a problem hiding this comment.
Properties related to "monadically concrete" would be nice (in both directions).
| 'Barr-exact', | ||
| TRUE, | ||
| 'The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks.' | ||
| 'The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks. This shows the category is regular. For exactness, quotients of equivalence relations are inherited from Group, with a quotient of a finite group clearly being finite as well.' |
There was a problem hiding this comment.
| 'The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks. This shows the category is regular. For exactness, quotients of equivalence relations are inherited from Group, with a quotient of a finite group clearly being finite as well.' | |
| 'The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks. This shows the category is regular. For exactness, quotients of equivalence relations are inherited from $\mathbf{Grp}$, with a quotient of a finite group clearly being finite as well.' |
| ( | ||
| 'Set', | ||
| 'Barr-coexact', | ||
| TRUE, | ||
| '$\mathbf{Set}^{\operatorname{op}}$ is monadic over $\mathbf{Set}$.' | ||
| ), |
There was a problem hiding this comment.
It is best to move all "general arguments" to the deduction system and remove them from property assignments. In this case, I would add the dual of "monadically concrete" to the db (not sure how to call it). Then the implication
monadic => Barr exact
automatically dualizes.
| 'Met_oo', | ||
| 'Barr-exact', | ||
| FALSE, | ||
| 'Any kernel pair of maps $f, g : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' |
There was a problem hiding this comment.
| 'Any kernel pair of maps $f, g : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' | |
| 'We can copy the proof from the <a href="/category/Met">category of metric spaces</a>.' |
(or even better: find a lemma that does this formally. but not urgent.)
| 'Barr-coexact', | ||
| TRUE, | ||
| 'From the other properties we know that (co-)limits exist and that monomorphisms coincide with injective pointed maps. So it suffices to prove that these maps are stable under pushouts. This follows from the corresponding fact for the <a href="/category/Set">category of sets</a> and the observation that the forgetful functor $\mathbf{Set}_* \to \mathbf{Set}$ preserves pushouts.' | ||
| 'According to <a href="https://ncatlab.org/nlab/show/exact+category">nLab</a> with a citation to <a href="http://www.springer.com/us/book/9781402019616">Borceux and Bourn</a>, Appendix A, any slice or co-slice of a Barr-exact category is also Barr-exact. It follows that any slice or co-slice of a Barr-coexact category is also Barr-coexact, and $\mathbf{Set}_*$ is a coslice category of $\mathbf{Set}$, which is Barr-coexact since $\mathbf{Set}^{\operatorname{op}}$ is monadic over $\mathbf{Set}$.' |
There was a problem hiding this comment.
You don't need to repeat the proof for a property. You can just link to the page /category/Set in doubt.
| 'SetxSet', | ||
| 'Barr-coexact', | ||
| TRUE, | ||
| '$(\mathbf{Set} \times \mathbf{Set})^{\operatorname{op}}$ is monadic over $\mathbf{Set} \times \mathbf{Set}$.' |
There was a problem hiding this comment.
The nLab page includes a result that any category which is monadic over a power of Set is Barr-exact. (Probably related to multi-algebraic categories, but I'm not that familiar with that.) But in this case, maybe it's easier just to say that because limits and colimits are done pointwise in Set^2, it's then trivial from the fact it's true in Set.
There was a problem hiding this comment.
Yeah let's use this simple argument and refer to the already known fact that Set is Barr-coexact.
|
Regarding setup: it went smoothly, except for the fact that the installation instructions for pnpm over there didn't quite cover my case where I'm on Linux and I didn't want to do a sudo for an npm install -g. I eventually found a way - that's not something I'd expect you to be able to fix here, though. Otherwise, the setup instructions for this project itself were fairly clear and painless. |
| '["locally strongly finitely presentable"]', | ||
| 'This is trivial because a locally strongly finitely presentable category is a variety of many-sorted finitary algebras.', | ||
| '["locally strongly finitely presentable", "monadically concrete"]', | ||
| 'The first is trivial because a locally strongly finitely presentable category is a variety of many-sorted finitary algebras. For the second, the forgetful functor to Set is monadic because the corresponding monad on Set takes a set to the collection of formal expressions in those variables modulo provable equality, and so it is easy to see an equivalence between an algebra over that monad and a model of the algebraic theory.', |
There was a problem hiding this comment.
| 'The first is trivial because a locally strongly finitely presentable category is a variety of many-sorted finitary algebras. For the second, the forgetful functor to Set is monadic because the corresponding monad on Set takes a set to the collection of formal expressions in those variables modulo provable equality, and so it is easy to see an equivalence between an algebra over that monad and a model of the algebraic theory.', | |
| 'The first is trivial because a locally strongly finitely presentable category is a variety of many-sorted finitary algebras. For the second, the forgetful functor to $\mathbf{Set}$ is monadic [TODO: add reference]., |
There was a problem hiding this comment.
The reference is Theorem VI.8.1 in MacLane
|
On the point of separating out "has effective equivalent relations", I wouldn't be sure which of the definitions - which are equivalent under the regularity assumption - I'd want to use. Just that there exists some map which gives it as a kernel pair? Or more strongly, that it has a coequalizer which gives it as a kernel pair? |
| 'topos_pretopos', | ||
| '["elementary topos"]', | ||
| '["pretopos"]', | ||
| 'All properties of a pretopos can be proved in a way similar to the way they are proved for Set, using the internal language and internal logic of an elementary topos.', |
There was a problem hiding this comment.
While this is the idea, I find this is a bit vague and I think it is better to add a book reference.
There was a problem hiding this comment.
This is a bit vague and I think it is better to add a book reference.
Thanks for reminding me, I meant that more as a placeholder since I don't have access to any of the standard texts such as Elephant, Sheaves in Geometry & Logic, etc.
There was a problem hiding this comment.
elementary topos => extensive is already in the database, it can be combined from three implications. So we should not repeat it here.
elementary topos => locally cartesian closed
elementary topos => disjoint finite coproducts
disjoint finite coproducts + locally cartesian closed => extensive
And the new result elementary topos => Barr-exact is Part A, Proposition 2.4.1 in the Elephant.
| 'barr_exact_def', | ||
| '["Barr-exact"]', | ||
| '["regular"]', | ||
| 'By definition', |
There was a problem hiding this comment.
nit:
| 'By definition', | |
| 'This holds by definition.', |
Proofs should always be full sentences.
| 'pretopos_definition', | ||
| '["pretopos"]', | ||
| '["Barr-exact", "extensive"]', | ||
| 'By definition.', |
There was a problem hiding this comment.
nit:
| 'By definition.', | |
| 'This holds by definition.', |
| ( | ||
| 'Set_op', | ||
| 'monadically concrete', | ||
| TRUE, | ||
| 'The contravariant powerset functor $\mathsf{Set}^{\operatorname{op}} \to \mathsf{Set}$ is monadic.' |
There was a problem hiding this comment.
Assignments for C should normally go in a separate file C.sql.
But this will become redundant anyway because of https://github.com/ScriptRaccoon/CatDat/pull/103/changes#r3106037619 I assume.
| 'FreeAb', | ||
| 'Barr-exact', | ||
| FALSE, | ||
| 'Any kernel pair $E$ of a morphism to a free Abelian group satisfies that $nx \in E \rightarrow x \in E$ for $n > 0$. However, for example the equivalence relation $\{ (x, y) \in \mathbb{Z}^2 \mid x \equiv y \pmod{2} \}$ does not satisfy this property.' |
There was a problem hiding this comment.
| 'Any kernel pair $E$ of a morphism to a free Abelian group satisfies that $nx \in E \rightarrow x \in E$ for $n > 0$. However, for example the equivalence relation $\{ (x, y) \in \mathbb{Z}^2 \mid x \equiv y \pmod{2} \}$ does not satisfy this property.' | |
| 'Any kernel pair $E$ of a morphism to a free abelian group satisfies that $nx \in E \rightarrow x \in E$ for $n > 0$. However, for example the equivalence relation $\{ (x, y) \in \mathbb{Z}^2 \mid x \equiv y \pmod{2} \}$ does not satisfy this property.' |
This and the proof for Met_c suggest that there might be a connection between balanced and Barr-exact?
There was a problem hiding this comment.
Well, yes, Barr-exact + extensive -> balanced. It's one of the implications I put in (as pretopos -> balanced), which happened to resolve a few cases automatically to disprove Barr-exactness.
Actually, that was one of the later entries. It appears that's made the explicit entries for Haus, Met_c, Met_oo, Prost, Top obsolete.
| 'Met_c', | ||
| 'Barr-exact', | ||
| FALSE, | ||
| 'Any kernel pair of a map $f : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' |
There was a problem hiding this comment.
Instead of copy paste I like to link proofs.
| 'Any kernel pair of a map $f : X \to Y$ is closed in $X \times X$, but there are plenty of equivalence relations which are not closed, such as $(\mathbb{Q} \times \mathbb{Q}) \cup \Delta \subseteq \mathbb{R} \times \mathbb{R}$.' | |
| 'We can use the same example as for the <a href="/category/Haus">category of Hausdorff spaces</a>.' |
But oftentimes a lemma is hiding behind the scenes when doing these things.
That should be equivalent if the coequalizer exists (3.1. in https://ncatlab.org/nlab/show/congruence). But in any case I am inclined to say that "this coequalizer exists and this is a kernel" is always a much more natural condition (and more easy to check as well) than "some map exists such that ...". |
Fair enough - that was my original intention, just to focus on Barr-exact and then have pretopos follow along pretty much automatically. But then it branched out into this question of naming "monadic over Set".
I'm not sure how I feel about the term "infinitary algebraic" in cases such as Set^op where the algebraic-like operation is P^2 X -> X, or similarly in the case of compact Hausdorff spaces where the algebraic-like operation is an assignment of a limit to each ultrafilter. To me, "infinitary algebraic" just suggests things more like the category of complete Boolean algebras, where the operations are still X^\kappa -> X and you just allow kappa to be an infinite cardinal now.
I had pretty much reached the point where I was stuck on making progress for the moment. Maybe a few cases where I had an idea but I was not confident enough on the details to put them in -- such as does the proof for metric spaces with continuous maps also apply for metric spaces with non-expansive maps? (Not as sure whether the transitivity morphism in that case is actually a non-expansive map.) Or, maybe Barr-exactness transfers from Set to Z-functors in the same way regularity does? But I noticed on nLab they state the result for functor categories for regularity but not for Barr-exactness, so I'm not sure if that's just an oversight or if it's because there's something subtle I'm missing there. |
|
What split-out part of this PR would you be most interested in seeing first? And regarding that split - do you tend to put in properties and their duals at the same time, or split those into separate PRs as well? |
At least in Diers's characterization theorem for multi-algebraic categories, "has effective equivalence relations" means "Every internal equivalence relation is a kernel pair of some morphism". But, I'm not sure if there is a multi-algebraic category such that internal equivalence relations do not necessarily admit coequalizers. Edit: In a multi-algebraic category, every equivalence relation admits a coequalizer, since it is a reflexive one (hence sifted). |
|
From the discussion, it sounds like maybe it might be useful to break it down even further: into properties of "has quotients of congruences", "has strict quotients of congruences" (where taking the kernel pair of the quotient map recovers exactly the original congruence), and "has effective congruences" (where every congruence is a kernel pair of some morphism). Then we can express the relations as an implication: has strict quotients of congruences <-> has quotients of congruences + has effective congruences. |
|
As for the other thread of discussion, it's occurred to me that we probably don't need to invent a new name; "monadic over Set" itself should be fairly widely understood. (Though I'm not 100% sure whether "comonadic" over Set" would be the dual to this property, and if not, then naming the dual property could be tricky.) |
I have no preference. I assume it would be good to add a property that can be "isolated" somehow.
I tend to add both properties. But in principle it is also good to do it in two PRs.
Sounds good!
You mean that you want to have bounded arities? In other words, accessible monads? |
|
Incidentally, related to the "monadic over Set" question: do we have a property that's equivalent to what I'd called "multi-sorted finitary algebraic" - which would then imply "monadic over a power of Set" and therefore Barr-exact? (As an example, a category of presheaves |
The property "locally strongly finitely presentable (lsfp)" is exactly what you call "multi-sorted finitary algebraic". |
4 participants
Add Barr-exact, Barr-coexact, pretopos properties.
Addresses: #96
I'm very unsure of my addition of a "monadically concrete" property that I put in for deducing exactness. If you prefer, I can remove that and just put in specific implications and assignments with that reasoning.
Currently undecided categories for Barr-exact:
category of Banach spaces with linear contractions
category of metric spaces with non-expansive maps
category of pseudo-metric spaces with non-expansive maps
category of Z-functors
Currently undecided categories for Barr-coexact:
category of Banach spaces with linear contractions
category of combinatorial species
category of Hausdorff spaces
category of locally ringed spaces
category of M-sets
category of measurable spaces
category of metric spaces with ∞ allowed
category of posets
category of sheaves
category of simplicial sets
category of Z-functors
Currently undecided categories for monadically concrete:
category of abelian sheaves
category of Banach spaces with linear contractions
category of pairs of sets
category of sheaves
category of simplicial sets
poset [0,1]
poset of extended natural numbers
proset of integers w.r.t. divisibility
walking commutative square
walking composable pair