diff --git a/content/separated_objects_cocongruences.md b/content/separated_objects_cocongruences.md new file mode 100644 index 00000000..df9beb4f --- /dev/null +++ b/content/separated_objects_cocongruences.md @@ -0,0 +1,17 @@ +--- +title: Cocongruences in a Quasitopos of Separated Objects +description: A proof that the full subcategory of separated objects for a Lawvere-Tierney topology on a topos has effective cocongruences +author: Daniel Schepler +--- + +## Cocongruences in a Quasitopos of Separated Objects + +::: Lemma +Let $\T$ be an elementary topos with a Lawvere-Tierney topology $j$. Then in the full subcategory of $j$-separated objects, every cocongruence is effective. +::: + +_Proof._ Suppose $p : X + X' \twoheadrightarrow E$ is a cocongruence (where $X'$ is an isomorphic copy of $X$), with coreflexivity morphism $r : E \to X$ and cotransitivity morphism $t : E \to E +_X E'$. (Here $E'$ is an isomorphic copy of $E$, and $E +_X E'$ is the coproduct modulo the relations $p(x') = p(x)'$.) We will also let $Y$ be the subobject of $X$ given by $x : X$ such that $p(x) = p(x')$. Note that $Y$ is $j$-closed in $X$ since $E$ is $j$-separated. + +We will first show that $p$ is in fact an epimorphism in $\T$. The argument will be in the internal logic of $\T$. Thus, suppose $e : E$, and let $x \coloneqq r(e) : X$. Then since $p$ is an epimorphism in the subcategory, we have $j(e = p(x) \lor e = p(x'))$. Also, since $E + E' \to E +_X E'$ is an epimorphism in $\T$, we have $t(e)$ is the image of an element of either $E$ or $E'$. In the first case, applying the section $e \mapsto e, e' \mapsto p(r(e)') : E +_X E' \to E$ of the inclusion $E \to E +_X E'$, and the fact that $t$ is the unique map such that $p(y) \mapsto p(y), p(y') \mapsto p(y')'$ for each $y : X$, we conclude the section composed with $t$ is the identity; thus, we get $t(e) = e$. Now if $e = p(x')$, then from $t(e) = e$ we conclude $x \in Y$, so $e = p(x)$ also. Therefore, $(e = p(x) \lor e = p(x')) \rightarrow e = p(x)$, so $j(e = p(x) \lor e = p(x'))$ implies $j(e = p(x))$, which in turn implies $e = p(x)$ since $E$ is $j$-separated. Similarly, if $t(e)$ is the image of an element of $E'$, then $e = p(x)'$. In either case, we have shown that $e$ is in the image of $p$, as desired. + +Since $\T$ is regular and epi-regular, we therefore have that $E$ is the quotient of the kernel pair of $p$. Since $\T$ is extensive, the kernel pair of $p$ is equivalent to $x \sim x, y \sim y', y' \sim y, x' \sim x'$ for $x : X, y : Y$. However, observe that $X + X'$ was formed in the subcategory, so it is the $j$-separated quotient of the coproduct in $\T$. In particular, this means that we already have $x = x'$ for $x$ a section of the $j$-closure of $0$ in $X$. But such sections are also automatically in $Y$, so this quotient is equivalent to $X +_Y X$, and this pushout is the same whether calculated in $\T$ or in the subcategory. $\square$ diff --git a/content/separated_objects_special_morphisms.md b/content/separated_objects_special_morphisms.md new file mode 100644 index 00000000..3d6e7e27 --- /dev/null +++ b/content/separated_objects_special_morphisms.md @@ -0,0 +1,21 @@ +--- +title: Special Morphisms of a Quasitopos of Separated Objects +description: A classification of the special morphisms in the full subcategory of separated objects for a Lawvere-Tierney topology on a topos +author: Daniel Schepler +--- + +## Special Morphisms of a Quasitopos of Separated Objects + +::: Lemma +Let $\T$ be an elementary topos with a Lawvere-Tierney topology $j$. Then in the full subcategory of $j$-separated objects:
+(a) The monomorphisms are the morphisms whose image in $\T$ are monomorphisms.
+(b) The epimorphisms are the morphisms whose image in $\T$ are $j$-dominant (i.e. the image calculated in $\T$ is a $j$-dense subobject of the codomain).
+(c) The regular monomorphisms are the morphisms whose image in $\T$ are $j$-closed monomorphisms.
+(d) The regular epimorphisms are the morphisms whose image in $\T$ are epimorphisms. +::: + +_Proof._ Recall that this subcategory is reflective, where the reflector takes an object $X$ to the quotient of $X$ by the congruence defined by the $j$-closure of the diagonal in $X\times X$. Also recall that the equalizer of $j, \id : \Omega_\T \rightrightarrows \Omega_\T$ is a $j$-separated object $\Omega_j$ which serves as the regular subobject classifier in the subcategory, and since $j$ is idempotent, this can also be described as the image (in $\T$) of $j$.
+(a) ($\Rightarrow$) This follows from the fact that the subcategory is reflective. ($\Leftarrow$) This is trivial for any subcategory.
+(b) ($\Rightarrow$) Given a morphism $f : X \to Y$, form the image $\im(f)$ in $\T$, which corresponds to a morphism $\chi_{\im(f)} : Y \to \Omega_\T$. Then $j \circ \chi_{\im(f)} \circ f = \top_Y \circ f$ as morphisms $Y \to \Omega_j$, so if $f$ is an epimorphism in the subcategory, then we conclude $j \circ \chi_{\im(f)} = \top_Y$. ($\Leftarrow$) Given a morphism $f : X \to Y$ of $j$-separated objects whose image in $\T$ is $j$-dense, suppose we have two morphisms $g, h : Y \rightrightarrows Z$ with $g \circ f = h \circ f$. Then since $Z$ is $j$-separated, the equalizer of $g$ and $h$ is $j$-closed; it also contains the image of $f$ and thus is $j$-dense. We conclude that the equalizer is all of $Y$.
+(c) ($\Rightarrow$) Any equalizer in $\T$ of $f, g : X \rightrightarrows Y$ with $Y$ $j$-separated is a $j$-closed subobject of $X$. If $X$ is $j$-separated as well, then that equalizer subobject is automatically separated, and agrees with the equalizer in the subcategory. ($\Leftarrow$) For a $j$-closed subobject $f : X \hookrightarrow Y$, we see that the characteristic morphism in $\T$, $\chi_X : Y \to \Omega$, factors through $\Omega_j$. Now $X$ is the equalizer of $\chi_X, \top : Y \rightrightarrows \Omega_j$.
+(d) ($\Rightarrow$) We can calculate the coequalizer of $f, g : X \rightrightarrows Y$ in the subcategory by taking the coequalizer $Z$ in $\T$ and then applying the reflector to get $Z_{sep}$. We see that both $Y \to Z$ and $Z \to Z_{sep}$ are epimorphisms in $\T$. ($\Leftarrow$) Suppose $f : X \to Y$ is an epimorphism in $\T$ of $j$-separated objects. Then the subcategory inclusion functor preserves the kernel pair $X \times_Y X \rightrightarrows X$, and since $f$ is a regular epimorphism in $\T$, this kernel pair has coequalizer $f : X \to Y$ in $\T$. Since $Y$ was already $j$-separated, the kernel pair also has coequalizer $f : X \to Y$ in the subcategory. $\square$ diff --git a/databases/catdat/data/categories/Meas.yaml b/databases/catdat/data/categories/Meas.yaml index d7ce5a65..e3516e53 100644 --- a/databases/catdat/data/categories/Meas.yaml +++ b/databases/catdat/data/categories/Meas.yaml @@ -56,9 +56,6 @@ unsatisfied_properties: - property: balanced proof: Take a set $X$ with two different $\sigma$-algebras $\A \subset \B$ (for example, $\A = \{\varnothing,X\}$ and $\B = P(X)$ when $X$ has at least $2$ elements), then the identity map $(X,\B) \to (X,\A)$ provides a counterexample. - - property: Malcev - proof: Use that $\Set$ is not Malcev and endow sets with the trivial $\sigma$-algebra. - - property: cartesian filtered colimits proof: See MSE/5027218. diff --git a/databases/catdat/data/categories/Prost.yaml b/databases/catdat/data/categories/Prost.yaml index c120b60d..24e05617 100644 --- a/databases/catdat/data/categories/Prost.yaml +++ b/databases/catdat/data/categories/Prost.yaml @@ -50,9 +50,6 @@ unsatisfied_properties: - property: skeletal proof: This is trivial. - - property: Malcev - proof: 'Consider the subproset $\{(a,b) : a \leq b \}$ of $\IN^2$.' - - property: co-Malcev proof: 'See MO/509552: Consider the forgetful functor $U : \Prost \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton preordered set and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.' diff --git a/databases/catdat/data/categories/Rng.yaml b/databases/catdat/data/categories/Rng.yaml index d491880c..3cfb9760 100644 --- a/databases/catdat/data/categories/Rng.yaml +++ b/databases/catdat/data/categories/Rng.yaml @@ -55,9 +55,6 @@ unsatisfied_properties: - property: CSP proof: Assume that $\coprod_n \IZ \to \prod_n \IZ$ is an epimorphism in $\Rng$. Then $((\coprod_n \IZ)^+)^{\ab} \to \prod_n \IZ$ would be an epimorphism in $\CRing$, where $(-)^+$ denotes the unitalization and $(-)^{\ab}$ the abelianization. But if $R \to S$ is an epimorphism of commutative rings, then $\card(S) \leq \card(R)$ by SP/04W0. Since $((\coprod_n \IZ)^+)^{\ab}$ is countable and $\prod_n \IZ$ is not, we get a contradiction. - - property: regular subobject classifier - proof: 'Assume that $\Rng$ has a subobject classifier $\Omega$. Since $0$ is a zero object, every regular subobject $R \subseteq S$ would be the kernel of some homomorphism $S \to \Omega$. In particular, it would be an ideal. Now take any pair of homomorphisms $f,g : S \rightrightarrows T$ in $\Ring$. Their equalizer $R \subseteq S$ is also the equalizer in $\Rng$, and it contains $1 \in S$. If it was an ideal, then $R = S$, and hence $f = g$, which is absurd.' - - property: coregular proof: 'We can copy the proof for $\Ring$. In short, the inclusion of diagonal matrices $\IQ^2 \hookrightarrow M_2(\IQ)$ is a regular monomorphism, but becomes zero after taking the pushout with $p_1 : \IQ^2 \twoheadrightarrow \IQ$ because $M_2(\IQ)$ is simple.' diff --git a/databases/catdat/data/categories/SepPsh(X).yaml b/databases/catdat/data/categories/SepPsh(X).yaml new file mode 100644 index 00000000..53218d16 --- /dev/null +++ b/databases/catdat/data/categories/SepPsh(X).yaml @@ -0,0 +1,70 @@ +id: SepPsh(X) +name: category of separated presheaves +notation: $\SepPsh(X)$ +objects: separated presheaves of sets on a topological space $X$ +morphisms: morphisms of presheaves +description: Here, we assume that the topological space $X$ is such that there is a non-empty family of open subsets whose union is not in the family, since otherwise this category is almost the category of all presheaves. For a few of the properties, we will strengthen this assumption to the assumption that there are two open subsets $U, V$ such that neither is contained in the other. +nlab_link: https://ncatlab.org/nlab/show/separated+presheaf + +tags: + - algebraic geometry + - topology + +related_categories: + - Sh(X) + +satisfied_properties: + - property: locally small + proof: This is easy. + + - property: Grothendieck quasitopos + proof: It is equivalent to $\BiSep(\Open(X), J, K)$ where $J$ is the trivial Grothendieck topology and $K$ is the open covering topology. + + - property: cocartesian cofiltered limits + proof: For non-empty $U$, both sides of $X \sqcup \lim_{i\in I} Y_i \to \lim_{i\in I} (X \sqcup Y_i)$ can be calculated component-wise. Therefore, for those $U$, the conclusion follows from the corresponding fact in $\Set$. For $U = \varnothing$, we can see that both sides are empty if and only if $X(\varnothing) = \varnothing$ and $Y_i(\varnothing) = \varnothing$ for some $i$, and otherwise both sides are a singleton. + +unsatisfied_properties: + - property: skeletal + proof: Consider the constant presheaves for two non-equal singleton sets. + + - property: disjoint finite coproducts + proof: The equalizer of the two coprojections $1 \rightrightarrows 1 + 1$ has value $1$ at $\varnothing$. + + - property: generator + proof: 'The subcategory $\Sh(X)$ of $\SepPsh(X)$ is reflective by Johnstone Prop 2.6.12 and A4.4. Therefore, if $\SepPsh(X)$ had a generator then so would $\Sh(X)$, which we know is not the case.' + + - property: effective congruences + proof: 'Let $\{ U_i : i \in I \}$ be a non-empty family of open sets whose union $U$ is not in the family. We then consider the relation $E$ on $X \coloneqq y_U + y_U$ where for $x_1, x_2 \in X(V)$, $(x_1, x_2) \in E(V)$ if and only if either $x_1 = x_2$ or $V \subseteq U_i$ for some $i \in I$. It is easy to see that $E$ is a congruence. However, $E \hookrightarrow X \times X$ is not a regular monomorphism, whereas any effective congruence would necessarily be an equalizer.' + + - property: semi-strongly connected + proof: Let $U$ and $V$ be two open subsets such that neither is contained in the other. Then there is neither a morphism $y_U \to y_V$ nor a morphism $y_V \to y_U$. + + - property: co-Malcev + proof: Let $U$ and $V$ be two open subsets such that neither is contained in the other. We will let $X \coloneqq y_{U \cup V}$, which represents the functor of sections over $U \cup V$, and then consider the reflexive relation on such sections $x, y \in F(U \cup V)$ where $x \sim y$ if and only if there exists $z \in F(U\cup V)$ such that $z |_U = x |_U$ and $z |_V = y |_V$. Note that since $F$ is separated, such a $z$ is unique if it exists. From this, we can see that this relation is representable by the colimit of a diagram where the objects are $y_U$, $y_V$, and three copies of $y_{U\cup V}$, and the morphisms are canonical morphisms from $y_U$ to the first and third copies of $y_{U\cup V}$ and canonical morphisms from $y_V$ to the second and third copies of $y_{U\cup V}$. In fact, we can see that the presheaf colimit is separated, so this presheaf colimit is also the colimit in $\SepPsh(X)$. Thus, we conclude that this corelation is not cosymmetric. + +special_objects: + initial object: + description: empty presheaf sending every open set to $\varnothing$ + terminal object: + description: constant presheaf with value a singleton + coproducts: + description: take the section-wise disjoint union, and then collapse the value at $\varnothing$ to a singleton if it is non-empty + products: + description: section-wise defined direct product + +special_morphisms: + isomorphisms: + description: morphisms of separated presheaves that are bijective on every open set + proof: This is easy. + monomorphisms: + description: morphisms of separated presheaves that are injective on every open set + proof: This is a corollary of (a) here. + epimorphisms: + description: 'morphisms of separated presheaves $\varphi : F \to G$ which are "locally surjective": for every local section $g \in G(U)$ there is an open covering $\bigcup_{i\in I} U_i = U$ such that each $g|_{U_i} \in G(U_i)$ is contained in the image of $\varphi(U_i) : F(U_i) \to G(U_i)$' + proof: This is a corollary of (b) here. + regular monomorphisms: + description: 'morphisms of separated presheaves $\varphi : F \hookrightarrow G$ that are injective on every open set, and such that "every section of $G$ which is locally in $F$ is itself in $F$": if a local section $g \in G(U)$ has an open covering $\bigcup_{i\in I} U_i = U$ such that each $g|_{U_i} \in G(U_i)$ is contained in the image of $\varphi(U_i) : F(U_i) \to G(U_i)$, then $g$ is contained in the image of $\varphi(U) : F(U) \to G(U)$' + proof: This is a corollary of (c) here. + regular epimorphisms: + description: morphisms of separated presheaves that are surjective on every open set + proof: This is a corollary of (d) here. diff --git a/databases/catdat/data/categories/Sh(X).yaml b/databases/catdat/data/categories/Sh(X).yaml index 507d4795..c8d0d4e7 100644 --- a/databases/catdat/data/categories/Sh(X).yaml +++ b/databases/catdat/data/categories/Sh(X).yaml @@ -14,6 +14,7 @@ related_categories: - Set - SetxSet - Sh(X,Ab) + - SepPsh(X) comments: - It is likely that none of the currently remaining unknown properties (locally ℵ₁-presentable, exact filtered colimits, etc.) are satisfied for a generic space $X$, but we need to make this precise by adding additional requirements to $X$. Maybe we need to create separate entries for specific spaces $X$. diff --git a/databases/catdat/data/categories/Top.yaml b/databases/catdat/data/categories/Top.yaml index c6a2b274..2ed7ca45 100644 --- a/databases/catdat/data/categories/Top.yaml +++ b/databases/catdat/data/categories/Top.yaml @@ -72,9 +72,6 @@ unsatisfied_properties: - property: coaccessible proof: 'Assume $\Top$ is coaccessible. Let $p : S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\Set$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\Set$ is not coaccessible, this is a contradiction.' - - property: Malcev - proof: This is clear since $\Set$ is not Malcev and can be interpreted as the subcategory of discrete spaces. - - property: co-Malcev proof: 'See MO/509548. We can also phrase the proof as follows: Consider the forgetful functor $U : \Top \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the singleton and $R$ by the Sierpinski space. It is clear that $R$ is reflexive, but not symmetric.' diff --git a/databases/catdat/data/category-implications/topos.yaml b/databases/catdat/data/category-implications/topos.yaml index 80d56add..9276526b 100644 --- a/databases/catdat/data/category-implications/topos.yaml +++ b/databases/catdat/data/category-implications/topos.yaml @@ -32,10 +32,10 @@ - id: topos_implies_coregular assumptions: - - elementary topos + - quasitopos conclusions: - coregular - proof: This is proven in Johnstone, A2.6.3 (for every quasitopos). + proof: This is proven in Johnstone, A2.6.3. is_equivalence: false - id: grothendieck_topos_definition @@ -70,12 +70,13 @@ - id: topos_no_stable_epis assumptions: - - elementary topos + - quasitopos - cofiltered-limit-stable epimorphisms - countable coproducts conclusions: - - trivial - proof: Let $N \coloneqq \coprod_{m \in \IN} 1$ and consider for every $n \in \IN$ the subobject $N_{\geq n} = \coprod_{m \geq n} 1$ of $N$. For $n \leq n'$ we have $N_{\geq n'} \subseteq N_{\geq n}$. There is a (unique, split) epimorphism $N_{\geq n} \to 1$ for every $n$. By assumption, their limit $\lim_n N_{\geq n} \to 1$ is also an epimorphism. But $\lim_n N_{\geq n} = \bigcap_{n} N_{\geq n} = 0$. Thus, $0 \to 1$ is an epimorphism. It must be a regular epimorphism, but $0$ is strict initial, so that $0 \to 1$ is an isomorphism. Hence, $X \cong X \times 1 \cong X \times 0 \cong 0$ for all $X$. + - thin + proof: >- + Let $N \coloneqq \coprod_{m \in \IN} 1$ and consider for every $n \in \IN$ the subobject $N_{\geq n} = \coprod_{m \geq n} 1$ of $N$. For $n \leq n'$ we have $N_{\geq n'} \subseteq N_{\geq n}$. There is a (unique, split) epimorphism $N_{\geq n} \to 1$ for every $n$. By assumption, their limit $\lim_n N_{\geq n} \to 1$ is also an epimorphism. But $0 \to \lim_n N_{\geq n}$ is also an epimorphism since any morphism $N_{\geq n} \to X$ factors through one of the coprojections $i_{n'} : 1 \to N_{\geq n}$ and therefore does not extend to a map $N_{\geq n'+1} \to X$. Thus, $0 \to 1$ is an epimorphism. It follows that for any parallel pair $f, g : X \rightrightarrows Y$, the characteristic morphism of the equalizer is equal to $\top \circ {!}_X$ so that $f = g$. is_equivalence: false - id: pretopos_definition @@ -86,3 +87,56 @@ - extensive proof: This is true by definition. is_equivalence: true + +- id: quasitopos_definition + assumptions: + - quasitopos + conclusions: + - finitely complete + - finitely cocomplete + - locally cartesian closed + - regular subobject classifier + proof: This is true by definition. + is_equivalence: true + +- id: balanced_quasitopos_is_topos + assumptions: + - quasitopos + - balanced + conclusions: + - elementary topos + proof: This is proven in Johnstone, A2.6.3. + is_equivalence: false + +- id: Giraud_for_quasitopos + assumptions: + - Grothendieck quasitopos + conclusions: + - quasitopos + - locally presentable + proof: See Johnstone, C2.2.13. + is_equivalence: true + +- id: Malcev_quasitopos_is_thin + assumptions: + - regular subobject classifier + - Malcev + conclusions: + - thin + proof: 'By a proof similar to this we conclude that every regular monomorphism is an isomorphism. Applying this to the equalizer of any parallel pair $f, g : X \rightrightarrows Y$, we conclude that $f = g$.' + is_equivalence: false + +- id: Grothendieck_quasitopos_consequences + assumptions: + - Grothendieck quasitopos + conclusions: + - exact filtered colimits + - cogenerator + - effective cocongruences + proof: >- + In order to calculate colimits in $\BiSep(\C, J, K)$, we can first calculate the colimit in the Grothendieck topos $\Sh(\C, J)$, then take the presheaf quotient of the $K$-closure of the diagonal relation, and finally apply the $J$-sheafification functor. (Note that the last two steps can also be viewed as forming the quotient in $\Sh(\C, J)$, where the equivalence relation is also $J$-closed in a $J$-sheaf and therefore itself a $J$-sheaf.) We already know that filtered colimits in $\Sh(\C, J)$ commute with finite limits, and similarly the $K$-separated quotient functor and $J$-sheafification functor commute with finite limits. We conclude that filtered colimits in $\BiSep(\C, J, K)$ also commute with finite limits. + + As for having a cogenerator: we have that $\Sh(\C, K)$ is a reflective subcategory of $\BiSep(\C, J, K)$, and the unit of the reflection adjunction is a monomorphism. It follows that the reflector is faithful, and thus that a cogenerator of $\Sh(\C, K)$ is also a cogenerator of $\BiSep(\C, J, K)$. + + The fact that $\BiSep(\C, J, K)$ has effective cocongruences is a corollary of this result. + is_equivalence: false diff --git a/databases/catdat/data/category-properties/Grothendieck quasitopos.yaml b/databases/catdat/data/category-properties/Grothendieck quasitopos.yaml new file mode 100644 index 00000000..192b1235 --- /dev/null +++ b/databases/catdat/data/category-properties/Grothendieck quasitopos.yaml @@ -0,0 +1,10 @@ +id: Grothendieck quasitopos +relation: is a +description: Given a small category $\C$ with a pair of Grothendieck topologies $J \subseteq K$, we define $\BiSep(\C, J, K)$ to be the full subcategory of presheaves on $\C$ which are both a sheaf for the $J$ topology and also separated for the $K$ topology. A Grothendieck quasitopos is a category which is equivalent to $\BiSep(\C, J, K)$ for some $\C, J, K$. Equivalently, a category is a Grothendieck quasitopos if and only if it is equivalent to the full subcategory of separated objects for a Lawvere-Tierney topology on a Grothendieck topos. +nlab_link: https://ncatlab.org/nlab/show/quasitopos +invariant_under_equivalences: true + +related_properties: + - quasitopos + - Grothendieck topos + - locally presentable diff --git a/databases/catdat/data/category-properties/Grothendieck topos.yaml b/databases/catdat/data/category-properties/Grothendieck topos.yaml index 6c05d94a..5e4ae1c7 100644 --- a/databases/catdat/data/category-properties/Grothendieck topos.yaml +++ b/databases/catdat/data/category-properties/Grothendieck topos.yaml @@ -6,3 +6,4 @@ invariant_under_equivalences: true related_properties: - elementary topos + - Grothendieck quasitopos diff --git a/databases/catdat/data/category-properties/elementary topos.yaml b/databases/catdat/data/category-properties/elementary topos.yaml index 5686a0f4..9fe6afd3 100644 --- a/databases/catdat/data/category-properties/elementary topos.yaml +++ b/databases/catdat/data/category-properties/elementary topos.yaml @@ -11,3 +11,4 @@ related_properties: - natural numbers object - subobject classifier - pretopos + - quasitopos diff --git a/databases/catdat/data/category-properties/quasitopos.yaml b/databases/catdat/data/category-properties/quasitopos.yaml new file mode 100644 index 00000000..fe5c4d36 --- /dev/null +++ b/databases/catdat/data/category-properties/quasitopos.yaml @@ -0,0 +1,17 @@ +id: quasitopos +relation: is a +description: >- + A quasitopos is a category which is finitely complete, finitely cocomplete, locally cartesian closed, and has a regular subobject classifier. This gives the category properties similar to those of an elementary topos; a major difference is that a quasitopos need not be balanced. + + 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 +invariant_under_equivalences: true + +related_properties: + - finitely complete + - finitely cocomplete + - locally cartesian closed + - regular subobject classifier + - elementary topos + - Grothendieck quasitopos + - balanced diff --git a/databases/catdat/data/category-properties/regular subobject classifier.yaml b/databases/catdat/data/category-properties/regular subobject classifier.yaml index fda2e901..590189f3 100644 --- a/databases/catdat/data/category-properties/regular subobject classifier.yaml +++ b/databases/catdat/data/category-properties/regular subobject classifier.yaml @@ -12,3 +12,4 @@ invariant_under_equivalences: true related_properties: - finitely complete - subobject classifier + - quasitopos diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml index 365443b0..5b226924 100644 --- a/databases/catdat/data/macros.yaml +++ b/databases/catdat/data/macros.yaml @@ -61,6 +61,7 @@ \cod: \operatorname{cod} \rank: \operatorname{rank} \Gal: \operatorname{Gal} +\Open: \operatorname{Open} # categories \Set: \mathbf{Set} @@ -118,3 +119,5 @@ \Isom: \mathbf{Isom} \Pair: \mathbf{Pair} \Span: \mathbf{Span} +\BiSep: \mathbf{BiSep} +\SepPsh: \mathbf{SepPsh} diff --git a/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json index 8e906067..08f365c3 100644 --- a/databases/catdat/scripts/expected-data/Ab.json +++ b/databases/catdat/scripts/expected-data/Ab.json @@ -169,5 +169,7 @@ "subobject-trivial": false, "quotient-trivial": false, "locally finite": false, - "pretopos": false + "pretopos": false, + "quasitopos": false, + "Grothendieck quasitopos": false } diff --git a/databases/catdat/scripts/expected-data/Set.json b/databases/catdat/scripts/expected-data/Set.json index 5596e679..658bf742 100644 --- a/databases/catdat/scripts/expected-data/Set.json +++ b/databases/catdat/scripts/expected-data/Set.json @@ -112,6 +112,8 @@ "ℵ₂-small powers": true, "ℵ₂-small copowers": true, "pretopos": true, + "quasitopos": true, + "Grothendieck quasitopos": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/databases/catdat/scripts/expected-data/Top.json b/databases/catdat/scripts/expected-data/Top.json index 8da72ea9..47a69a18 100644 --- a/databases/catdat/scripts/expected-data/Top.json +++ b/databases/catdat/scripts/expected-data/Top.json @@ -169,5 +169,7 @@ "locally finite": false, "Barr-coexact": false, "Barr-exact": false, - "pretopos": false + "pretopos": false, + "quasitopos": false, + "Grothendieck quasitopos": false }