diff --git a/.cspell.json b/.cspell.json index 887f72204..56bcf16d4 100644 --- a/.cspell.json +++ b/.cspell.json @@ -165,6 +165,7 @@ "cospans", "cosymmetric", "cosymmetry", + "cotopos", "cototal", "cotransitive", "cotransitivity", @@ -327,6 +328,7 @@ "precomposed", "precomposing", "precomposition", + "precotopos", "preimage", "preimages", "preorder", @@ -348,6 +350,7 @@ "pushforward", "pushout", "pushouts", + "quasicotopos", "quasitopos", "Quillan", "Reggio", diff --git a/database/data/category-properties/Barr-coexact.yaml b/database/data/category-properties/Barr-coexact.yaml index 908c04008..5f4a66301 100644 --- a/database/data/category-properties/Barr-coexact.yaml +++ b/database/data/category-properties/Barr-coexact.yaml @@ -9,6 +9,7 @@ related: - coregular - effective cocongruences - coquotients of cocongruences + - precotopos tags: - limit–colimit interaction diff --git a/database/data/category-properties/Grothendieck cotopos.yaml b/database/data/category-properties/Grothendieck cotopos.yaml new file mode 100644 index 000000000..4c9c19714 --- /dev/null +++ b/database/data/category-properties/Grothendieck cotopos.yaml @@ -0,0 +1,12 @@ +id: Grothendieck cotopos +relation: is a +description: A Grothendieck cotopos is a category whose opposite is a Grothendieck topos. +nlab_link: https://ncatlab.org/nlab/show/cotopos +dual: Grothendieck topos +invariant_under_equivalences: true + +related: + - elementary cotopos + +tags: + - topos theory diff --git a/database/data/category-properties/Grothendieck topos.yaml b/database/data/category-properties/Grothendieck topos.yaml index 4344078f2..d30869eaf 100644 --- a/database/data/category-properties/Grothendieck topos.yaml +++ b/database/data/category-properties/Grothendieck topos.yaml @@ -2,7 +2,7 @@ id: Grothendieck topos relation: is a description: A Grothendieck topos is a category that is equivalent to the category of sheaves on a site. nlab_link: https://ncatlab.org/nlab/show/Grothendieck+topos -dual: null +dual: Grothendieck cotopos invariant_under_equivalences: true related: diff --git a/database/data/category-properties/coextensive.yaml b/database/data/category-properties/coextensive.yaml index ca5390b71..3be57d838 100644 --- a/database/data/category-properties/coextensive.yaml +++ b/database/data/category-properties/coextensive.yaml @@ -10,6 +10,7 @@ related: - codistributive - infinitary coextensive - countably coextensive + - precotopos tags: - limit–colimit interaction diff --git a/database/data/category-properties/elementary cotopos.yaml b/database/data/category-properties/elementary cotopos.yaml new file mode 100644 index 000000000..e0d08d47f --- /dev/null +++ b/database/data/category-properties/elementary cotopos.yaml @@ -0,0 +1,17 @@ +id: elementary cotopos +relation: is an +description: An elementary cotopos is a category whose dual category is an elementary topos, i.e. a cocartesian coclosed category with finite colimits and a quotient object classifier. +nlab_link: https://ncatlab.org/nlab/show/cotopos +dual: elementary topos +invariant_under_equivalences: true + +related: + - cocartesian coclosed + - finitely cocomplete + - quotient object classifier + - Grothendieck cotopos + - precotopos + - quasitopos + +tags: + - topos theory diff --git a/database/data/category-properties/elementary topos.yaml b/database/data/category-properties/elementary topos.yaml index f471a7049..eb02381cf 100644 --- a/database/data/category-properties/elementary topos.yaml +++ b/database/data/category-properties/elementary topos.yaml @@ -2,17 +2,17 @@ id: elementary topos relation: is an description: An elementary topos is a cartesian closed category with finite limits and a subobject classifier. nlab_link: https://ncatlab.org/nlab/show/topos -dual: null +dual: elementary cotopos invariant_under_equivalences: true related: - - Grothendieck topos - cartesian closed - finitely complete - - parametrized natural numbers object - subobject classifier + - Grothendieck topos - pretopos - quasitopos + - parametrized natural numbers object tags: - topos theory diff --git a/database/data/category-properties/precotopos.yaml b/database/data/category-properties/precotopos.yaml new file mode 100644 index 000000000..b1e6321bc --- /dev/null +++ b/database/data/category-properties/precotopos.yaml @@ -0,0 +1,16 @@ +id: precotopos +relation: is a +description: A precotopos is a category whose opposite is a pretopos. Equivalently, it is Barr-coexact and coextensive. This terminology is not standard. +nlab_link: null +dual: pretopos +invariant_under_equivalences: true + +related: + - Barr-coexact + - coextensive + - elementary cotopos + - epi-regular + +tags: + - topos theory + - limit–colimit interaction diff --git a/database/data/category-properties/pretopos.yaml b/database/data/category-properties/pretopos.yaml index e8820b30f..5a6a0baca 100644 --- a/database/data/category-properties/pretopos.yaml +++ b/database/data/category-properties/pretopos.yaml @@ -2,7 +2,7 @@ id: pretopos relation: is a description: A pretopos is a category which is Barr-exact and extensive. nlab_link: https://ncatlab.org/nlab/show/pretopos -dual: null +dual: precotopos invariant_under_equivalences: true related: diff --git a/database/data/category-properties/quasicotopos.yaml b/database/data/category-properties/quasicotopos.yaml new file mode 100644 index 000000000..90ce11ae5 --- /dev/null +++ b/database/data/category-properties/quasicotopos.yaml @@ -0,0 +1,20 @@ +id: quasicotopos +relation: is a +description: >- + A quasicotopos is a category whose opposite is a quasitopos. This means that it is finitely complete, finitely cocomplete, locally cocartesian coclosed, and has a regular quotient object classifier. This terminology is not standard. +nlab_link: null +dual: quasitopos +invariant_under_equivalences: true + +keywords: + - quasi-cotopos + +related: + - finitely complete + - finitely cocomplete + - locally cocartesian coclosed + - regular quotient object classifier + - elementary cotopos + +tags: + - topos theory diff --git a/database/data/category-properties/quasitopos.yaml b/database/data/category-properties/quasitopos.yaml index 82576e47b..3c1130723 100644 --- a/database/data/category-properties/quasitopos.yaml +++ b/database/data/category-properties/quasitopos.yaml @@ -5,7 +5,7 @@ description: >- Note that some authors use a strong subobject classifier in place of a regular subobject classifier in the definition, i.e. a morphism $\top : 1 \to \Omega$ which classifies strong monomorphisms. For the equivalence of these definitions, see MSE/4335533. nlab_link: https://ncatlab.org/nlab/show/quasitopos -dual: null +dual: quasicotopos invariant_under_equivalences: true keywords: diff --git a/database/data/category-properties/quotient object classifier.yaml b/database/data/category-properties/quotient object classifier.yaml index 600542fac..265156bf9 100644 --- a/database/data/category-properties/quotient object classifier.yaml +++ b/database/data/category-properties/quotient object classifier.yaml @@ -5,13 +5,14 @@ description: >- $$\begin{CD} \Psi @>{\top}>> 0 \\ @V{\psi_e}VV @VV{!}V \\ A @>>{e}> B \end{CD}$$ is a pushout diagram. Equivalently, the functor $\Quot : \C \to \Set^+$ is representable. *Every morphism $\Psi \to 0$ is a split epimorphism anyway. -nlab_link: null +nlab_link: https://ncatlab.org/nlab/show/quotient+object+coclassifier dual: subobject classifier invariant_under_equivalences: true related: - finitely cocomplete - regular quotient object classifier + - elementary cotopos tags: - topos theory diff --git a/database/data/category-properties/regular quotient object classifier.yaml b/database/data/category-properties/regular quotient object classifier.yaml index 0d574ab43..ea6f89484 100644 --- a/database/data/category-properties/regular quotient object classifier.yaml +++ b/database/data/category-properties/regular quotient object classifier.yaml @@ -12,6 +12,7 @@ invariant_under_equivalences: true related: - finitely cocomplete - quotient object classifier + - quasicotopos tags: - topos theory diff --git a/database/scripts/expected-data/Ab.json b/database/scripts/expected-data/Ab.json index 2c597c82d..1bf5ffbde 100644 --- a/database/scripts/expected-data/Ab.json +++ b/database/scripts/expected-data/Ab.json @@ -150,6 +150,7 @@ "direct", "discrete", "distributive", + "elementary cotopos", "elementary topos", "essentially countable", "essentially discrete", @@ -160,6 +161,7 @@ "finite", "finitely coaccessible", "gaunt", + "Grothendieck cotopos", "Grothendieck topos", "groupoid", "infinitary codistributive", @@ -176,7 +178,9 @@ "locally ℵ₁-copresentable", "one-way", "parametrized natural numbers object", + "precotopos", "pretopos", + "quasicotopos", "quasitopos", "quotient object classifier", "quotient-trivial", diff --git a/database/scripts/expected-data/FinSet.json b/database/scripts/expected-data/FinSet.json index dec65c542..0a10138ec 100644 --- a/database/scripts/expected-data/FinSet.json +++ b/database/scripts/expected-data/FinSet.json @@ -124,6 +124,7 @@ "disjoint coproducts", "disjoint finite products", "disjoint products", + "elementary cotopos", "essentially discrete", "essentially finite", "exact cofiltered limits", @@ -137,6 +138,7 @@ "gaunt", "generalized variety", "Grothendieck abelian", + "Grothendieck cotopos", "Grothendieck topos", "groupoid", "infinitary codistributive", @@ -168,7 +170,9 @@ "pointed", "powers", "preadditive", + "precotopos", "products", + "quasicotopos", "quotient object classifier", "quotient-trivial", "regular quotient object classifier", diff --git a/database/scripts/expected-data/N.json b/database/scripts/expected-data/N.json index 927137cc5..3adbd63da 100644 --- a/database/scripts/expected-data/N.json +++ b/database/scripts/expected-data/N.json @@ -126,6 +126,7 @@ "disjoint finite products", "disjoint products", "distributive", + "elementary cotopos", "elementary topos", "epi-regular", "essentially discrete", @@ -144,6 +145,7 @@ "finitely complete", "generalized variety", "Grothendieck abelian", + "Grothendieck cotopos", "Grothendieck topos", "groupoid", "infinitary codistributive", @@ -171,8 +173,10 @@ "pointed", "powers", "preadditive", + "precotopos", "pretopos", "products", + "quasicotopos", "quasitopos", "quotient object classifier", "quotient-trivial", diff --git a/database/scripts/expected-data/Set.json b/database/scripts/expected-data/Set.json index 181deb0be..e7379ce9e 100644 --- a/database/scripts/expected-data/Set.json +++ b/database/scripts/expected-data/Set.json @@ -153,6 +153,7 @@ "discrete", "disjoint finite products", "disjoint products", + "elementary cotopos", "essentially countable", "essentially discrete", "essentially finite", @@ -162,6 +163,7 @@ "finitely coaccessible", "gaunt", "Grothendieck abelian", + "Grothendieck cotopos", "groupoid", "infinitary codistributive", "infinitary coextensive", @@ -178,6 +180,8 @@ "one-way", "pointed", "preadditive", + "precotopos", + "quasicotopos", "quotient object classifier", "quotient-trivial", "regular quotient object classifier", diff --git a/database/scripts/expected-data/Top.json b/database/scripts/expected-data/Top.json index a04ba72d0..171186197 100644 --- a/database/scripts/expected-data/Top.json +++ b/database/scripts/expected-data/Top.json @@ -128,6 +128,7 @@ "disjoint products", "effective cocongruences", "effective congruences", + "elementary cotopos", "elementary topos", "epi-regular", "essentially countable", @@ -145,6 +146,7 @@ "gaunt", "generalized variety", "Grothendieck abelian", + "Grothendieck cotopos", "Grothendieck topos", "groupoid", "infinitary codistributive", @@ -172,8 +174,10 @@ "one-way", "pointed", "preadditive", + "precotopos", "pretopos", "pullback-stable regular epimorphisms", + "quasicotopos", "quasitopos", "quotient object classifier", "quotient-trivial", diff --git a/database/scripts/expected-data/walking_morphism.json b/database/scripts/expected-data/walking_morphism.json index 3ffd66140..241e79180 100644 --- a/database/scripts/expected-data/walking_morphism.json +++ b/database/scripts/expected-data/walking_morphism.json @@ -116,6 +116,7 @@ "pullbacks", "pushout-stable regular monomorphisms", "pushouts", + "quasicotopos", "quasitopos", "quotients of congruences", "reflexive coequalizers", @@ -172,11 +173,13 @@ "disjoint finite coproducts", "disjoint finite products", "disjoint products", + "elementary cotopos", "elementary topos", "epi-regular", "essentially discrete", "extensive", "Grothendieck abelian", + "Grothendieck cotopos", "Grothendieck topos", "groupoid", "infinitary coextensive", @@ -186,6 +189,7 @@ "normal", "pointed", "preadditive", + "precotopos", "pretopos", "quotient object classifier", "quotient-trivial", diff --git a/shared/history.json b/shared/history.json index 140b172ab..560b3fad0 100644 --- a/shared/history.json +++ b/shared/history.json @@ -1985,6 +1985,22 @@ { "type": "category", "id": "locally ℵ₁-copresentable" + }, + { + "type": "category", + "id": "elementary cotopos" + }, + { + "type": "category", + "id": "Grothendieck cotopos" + }, + { + "type": "category", + "id": "precotopos" + }, + { + "type": "category", + "id": "quasicotopos" } ] }