Exact cofiltered limits and related notions

.vscode/settings.json

@@ -25,6 +25,7 @@
 		"abelianization",
 		"abelianize",
 		"Adamek",
+		"adic",
 		"algébriques",
 		"anneaux",
 		"Artin",
@@ -203,6 +204,7 @@
 		"surjective",
 		"tensoring",
 		"Turso",
+		"uncountably",
 		"unital",
 		"vercel",
 		"Vite",

database/data/003_properties/003_limits-colimits-behavior.sql

@@ -95,7 +95,15 @@ VALUES
 	'has',
 	'In a category $\mathcal{C}$, which we assume to have filtered colimits and finite limits, we say that <i>filtered colimits are exact</i> if for every finite category $\mathcal{I}$ the functor $\lim : [\mathcal{I}, \mathcal{C}] \to \mathcal{C}$ preserves filtered colimits. Equivalently, for every diagram $X : \mathcal{I} \times \mathcal{J} \to \mathcal{C}$, where $\mathcal{I}$ is finite and $\mathcal{J}$ is filtered, the canonical morphism $\mathrm{colim}_{j} \lim_{i} X(i,j) \to \lim_{i} \mathrm{colim}_j X(i,j)$ is an isomorphism.',
 	'https://ncatlab.org/nlab/show/commutativity+of+limits+and+colimits',
-	NULL,
+	'exact cofiltered limits',
+	TRUE
+),
+(
+	'exact cofiltered limits',
+	'has',
+	'In a category $\mathcal{C}$, which we assume to have cofiltered limits and finite colimits, we say that <i>cofiltered limits are exact</i> if for every finite category $\mathcal{I}$ the functor $\mathrm{colim} : [\mathcal{I}, \mathcal{C}] \to \mathcal{C}$ preserves cofiltered limits. Equivalently, for every diagram $X : \mathcal{I} \times \mathcal{J} \to \mathcal{C}$, where $\mathcal{I}$ is finite and $\mathcal{J}$ is cofiltered, the canonical morphism $\lim_{j} \mathrm{colim}_{i} X(i,j) \to \mathrm{colim}_{i} \lim_j X(i,j)$ is an isomorphism.',
+	'https://ncatlab.org/nlab/show/commutativity+of+limits+and+colimits',
+	'exact filtered colimits',
 	TRUE
 ),
 (

database/data/003_properties/005_morphism-behavior.sql

@@ -105,4 +105,20 @@ VALUES
 	'https://ncatlab.org/nlab/show/one-way+category',
 	'one-way',
 	TRUE
+),
+(
+	'filtered-colimit-stable monomorphisms',
+	'has',
+	'A category has <i>filtered-colimit-stable monomorphisms</i> if it has filtered colimits and for every filtered diagram of monomorphisms $(X_i \to Y_i)$ also their colimit $\mathrm{colim}_i X_i \to \mathrm{colim}_i Y_i$ is a monomorphism.',
+	NULL,
+	'cofiltered-limit-stable epimorphisms',
+	TRUE 
+),
+(
+	'cofiltered-limit-stable epimorphisms',
+	'has',
+	'A category has <i>cofiltered-limit-stable epimorphisms</i> if it has cofiltered limits and for every cofiltered diagram of epimorphisms $(X_i \to Y_i)$ also their limit $\lim_i X_i \to \lim_i Y_i$ is an epimorphism.',
+	NULL,
+	'filtered-colimit-stable monomorphisms',
+	TRUE 
 );

database/data/003_properties/100_related-properties.sql

@@ -185,11 +185,20 @@ VALUES
 ('exact filtered colimits', 'filtered colimits'),
 ('exact filtered colimits', 'finitely complete'),
 ('exact filtered colimits', 'cartesian filtered colimits'),
+('exact cofiltered limits', 'cofiltered limits'),
+('exact cofiltered limits', 'finitely cocomplete'),
+('exact cofiltered limits', 'cocartesian cofiltered limits'),
+('exact cofiltered limits', 'cofiltered-limit-stable epimorphisms'),
 ('cartesian filtered colimits', 'filtered colimits'),
 ('cartesian filtered colimits', 'finite products'),
 ('cartesian filtered colimits', 'exact filtered colimits'),
 ('cocartesian cofiltered limits', 'cofiltered limits'),
 ('cocartesian cofiltered limits', 'finite coproducts'),
+('cocartesian cofiltered limits', 'exact cofiltered limits'),
+('filtered-colimit-stable monomorphisms', 'exact filtered colimits'),
+('filtered-colimit-stable monomorphisms', 'filtered colimits'),
+('cofiltered-limit-stable epimorphisms', 'exact cofiltered limits'),
+('cofiltered-limit-stable epimorphisms', 'cofiltered limits'),
 ('generator', 'generating set'),
 ('generating set', 'generator'),
 ('Grothendieck abelian', 'abelian'),

database/data/004_property-assignments/Ab.sql

@@ -34,4 +34,10 @@ VALUES
 	'skeletal',
 	FALSE,
 	'This is trivial.'
+),
+(
+	'Ab',
+	'cofiltered-limit-stable epimorphisms',
+	FALSE,
+	'We know that $\mathbf{CRing}$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the forgetful functor $\mathbf{CRing} \to \mathbf{Ab}$. Even though it does not preserve epimorphisms, our counterexample for $\mathbf{CRing}$ has used the <i>surjective</i> ring homomorphisms $\mathbb{Z} \to \mathbb{Z}/p^n$, which remain epimorphisms in $\mathbf{Ab}$.'
 );

database/data/004_property-assignments/CRing.sql

@@ -82,4 +82,10 @@ VALUES
 	'regular quotient object classifier',
 	FALSE,
 	'Assume that $P \to \mathbb{Z}$ is a regular quotient object classifier. If $J$ denotes its kernel, this means that every ideal $I \subseteq A$ of any commutative ring has the form $I = \langle \varphi(J) \rangle$ for a unique homomorphism $\varphi : P \to A$. If $\sigma : A \to A$ is an automorphism with $\sigma(I)=I$, then uniqueness gives us $\sigma \circ \varphi = \varphi$, which means that $\varphi(J)$ lies in $A^{\sigma}$, the fixed ring of $\sigma$. But then $I$ is generated by elements in the fixed ring. This fails for $A = \mathbb{Z}[X]$, $I = \langle X \rangle$, $\sigma(X)=-X$. The fixed ring is $\mathbb{Z}[X^2]$, and if $I$ was generated by elements $f \in \mathbb{Z}[X^2] \cap I$, they would be multiples of $X^2$, but $X$ is not a multiple of $X^2$.'
+),
+(
+	'CRing',
+	'cofiltered-limit-stable epimorphisms',
+	FALSE,
+	'For a prime $p$ consider the sequence of projections $\cdots \to \mathbb{Z}/p^2 \to \mathbb{Z}/p$ and the constant sequence $\cdots \to \mathbb{Z} \to \mathbb{Z}$. The surjective homomorphisms $\mathbb{Z} \to \mathbb{Z}/p^n$ induce the homomorphism $\mathbb{Z} \to \mathbb{Z}_p$ in the limit, where $\mathbb{Z}_p$ is the ring of $p$-adic integers. It is not surjective since $\mathbb{Z}_p$ is uncountable, but this is not sufficient (at least, for this category): We need to use <a href="https://stacks.math.columbia.edu/tag/04W0" target="_blank">SP/04W0</a> to conclude that it is no epimorphism in $\mathbf{CRing}$.'
 );

database/data/004_property-assignments/FS.sql

@@ -53,6 +53,12 @@ VALUES
 	TRUE,
 	'If $f : X \to Y$ is a surjective map of finite sets, it is the coequalizer of the two projections $p_1, p_2 : X \times_Y X \rightrightarrows X$ in $\mathbf{FinSet}$, but also in $\mathbf{FS}$. Notice that $p_1,p_2$ are surjective. Even though $X \times_Y X$ is not a pullback in $\mathbf{FS}$, we can use this finite set here.'
 ),
+(
+	'FS',
+	'filtered-colimit-stable monomorphisms',
+	TRUE,
+	'This is because every monomorphism is an isomorphism in this category (see below), and isomorphisms are always stable under any type of colimit.'
+),
 (
 	'FS',
 	'multi-terminal object',

database/data/004_property-assignments/Grp.sql

@@ -92,4 +92,10 @@ VALUES
 	is injective, but often fails to be surjective because the components of an element in the image have bounded <i>free product length</i> (the number of factors appearing in the reduced form). Specifically, consider the free groups $G = \langle y \rangle$ and $H_n = \langle x_1,\dotsc,x_n \rangle$ for $n \in \mathbb{N}$ with the truncation maps $H_{n+1} \to H_n$, $x_{n+1} \mapsto 1$. Define
 	<br>$p_n := x_1 \, y \, x_2 \, y \, \cdots \, x_{n-1} \, y \, x_n \, y^{-(n-1)} \in G \sqcup H_n$.<br>
 	If we substitute $x_{n+1}=1$ in $p_{n+1}$, we get $p_n$. Thus, we have $p = (p_n) \in \lim_n (G \sqcup H_n)$. This element does not lie in the image of $\alpha$ since the free product length of $p_n$ (which is well-defined) is $2n$, which is unbounded.'
+),
+(
+	'Grp',
+	'cofiltered-limit-stable epimorphisms',
+	FALSE,
+	'We know that $\mathbf{Ab}$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the forgetful functor $\mathbf{Ab} \to \mathbf{Grp}$ (which does preserve epimorphisms).'
 );

database/data/004_property-assignments/M-Set.sql

@@ -34,4 +34,10 @@ VALUES
 	'Malcev',
 	FALSE,
 	'Endow the set $\mathbb{N}$ with the trivial $M$-action, and consider the subset $\{(a,b) : a \leq b \}$ of $\mathbb{N}^2$.'
+),
+(
+	'M-Set',
+	'cofiltered-limit-stable epimorphisms',
+	FALSE,
+	'We know that $\mathbf{Set}$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the functor $\mathbf{Set} \to M{-}\mathbf{Set}$ that equips a set with the trivial $M$-action.'
 );

database/data/004_property-assignments/Meas.sql

@@ -53,6 +53,12 @@ VALUES
 	TRUE,
 	'Take the two-element set $2$ endowed with the trivial $\sigma$-algebra (where only $\varnothing$ and $2$ are measurable), and use that $2$ is a cogenerator for $\mathbf{Set}$.'
 ),
+(
+	'Meas',
+	'filtered-colimit-stable monomorphisms',
+	TRUE,
+	'This follows from <a href="/lemma/filtered-monos">this lemma</a> applied to the forgetful functor to $\mathbf{Set}$.'
+),
 (
 	'Meas',
 	'semi-strongly connected',

database/data/004_property-assignments/Prost.sql

@@ -94,4 +94,10 @@ VALUES
 	'co-Malcev',
 	FALSE,
 	'See <a href="https://mathoverflow.net/questions/509552">MO/509552</a>: Consider the forgetful functor $U : \mathbf{Prost} \to \mathbf{Set}$ and the relation $R \subseteq U^2$ defined by $R(A) := \{(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.'
+),
+(
+	'Prost',
+	'cofiltered-limit-stable epimorphisms',
+	FALSE,
+	'We know that $\mathbf{Set}$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the functor $\mathbf{Set} \to \mathbf{Prost}$ that equips a set with the chaotic preorder.'
 );

database/data/004_property-assignments/Ring.sql

@@ -90,4 +90,10 @@ VALUES
 	'Consider the ring $A = \mathbb{Z}[X]$ and the sequence of rings $B_n = \mathbb{Z}[Y]/(Y^{n+1})$ with projections $B_{n+1} \to B_n$, whose limit is $\mathbb{Z}[[Y]]$. Every element in the coproduct of rings $\mathbb{Z}[X] \sqcup \mathbb{Z}[[Y]]$ has a finite "free product" length. Now consider the elements
 	<br>$w_n = (1 + XY) (1+XY^2) \cdots (1+X Y^n) \in A \sqcup B_n$.</br>
 	Because of $w_n \equiv w_{n-1} \bmod Y^n$ these form an element $w \in \lim_n (A \sqcup B_n)$. Expanding $w_n$, the longest term is $XY XY^2 \cdots X Y^n$ of "free product" length $2n$, which is unbounded.'
+),
+(
+	'Ring',
+	'cofiltered-limit-stable epimorphisms',
+	FALSE,
+	'We know that $\mathbf{CRing}$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the forgetful functor $\mathbf{CRing} \to \mathbf{Ring}$. Even though it is not clear if it preserves epimorphisms, our counterexample for $\mathbf{CRing}$ has used the <i>surjective</i> ring homomorphisms $\mathbb{Z} \to \mathbb{Z}/p^n$, which remain epimorphisms in $\mathbf{Ring}$.'
 );

database/data/004_property-assignments/Rng.sql

@@ -78,4 +78,10 @@ VALUES
 	'Consider the ring $A = \mathbb{Z}[X]$ and the sequence of rings $B_n = \mathbb{Z}[Y]/(Y^{n+1})$ with projections $B_{n+1} \to B_n$, whose limit is $\mathbb{Z}[[Y]]$ (both in $\mathbf{Ring}$ and $\mathbf{Rng}$). Every element in the coproduct of rngs $\mathbb{Z}[X] \sqcup \mathbb{Z}[[Y]]$ has a finite "free product" length. Now consider the elements
 	<br>$w_n = (1 + XY) (1+XY^2) \cdots (1+X Y^n) - 1 \in A \sqcup B_n$.</br>
 	Because of $w_n \equiv w_{n-1} \bmod Y^n$ these form an element $w \in \lim_n (A \sqcup B_n)$. Expanding $w_n$, the longest term is $XY XY^2 \cdots X Y^n$ of "free product" length $2n$, which is unbounded.'
+),
+(
+	'Rng',
+	'cofiltered-limit-stable epimorphisms',
+	FALSE,
+	'We know that $\mathbf{CRing}$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the forgetful functor $\mathbf{CRing} \to \mathbf{Rng}$. Even though it is not clear if it preserves epimorphisms, our counterexample for $\mathbf{CRing}$ has used the <i>surjective</i> ring homomorphisms $\mathbb{Z} \to \mathbb{Z}/p^n$, which remain epimorphisms in $\mathbf{Rng}$.'
 );

database/data/004_property-assignments/Set.sql

@@ -40,4 +40,10 @@ VALUES
 	'Malcev',
 	FALSE,
 	'There are lots of non-symmetric reflexive relations, for example $\leq$ on $\mathbb{N}$.'
+),
+(
+	'Set',
+	'cofiltered-limit-stable epimorphisms',
+	FALSE,
+	'Pick any decreasing sequence of non-empty sets $X_0 \supseteq X_1 \supseteq \cdots$ with empty intersection, such as $X_n = \mathbb{N}_{\geq n}$. The unique map $X_n \to 1$ is surjective, but their limit $\varnothing \to 1$ is not surjective.'
 );

database/data/004_property-assignments/Set_pointed.sql

@@ -78,4 +78,10 @@ VALUES
 	'conormal',
 	FALSE,
 	'Every cokernel is "injective away from the base point". Formally, if $p : A \to B$ is a cokernel in $\mathbf{Set}_*$, it has the property that $p(x)=p(y) \neq 0$ implies $x=y$ (where $0$ denotes the base point). Clearly this is not satisfied for every surjective pointed map, consider $(\mathbb{N},0) \to (\{0,1\},0)$ defined by $0 \mapsto 0$ and $x \mapsto 1$ for $x > 0$.'
+),
+(
+	'Set*',
+	'cofiltered-limit-stable epimorphisms',
+	FALSE,
+	'We know that $\mathbf{Set}$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the functor $\mathbf{Set} \to \mathbf{Set}_*$ that freely adds a base point.'
 );

database/data/004_property-assignments/Setne.sql

@@ -108,6 +108,12 @@ VALUES
 	TRUE,
 	'Any natural numbers object in $\mathbf{Set}$, such as $(\mathbb{N},0,n \mapsto n+1)$, is clearly also one in $\mathbf{Set}_{\neq \varnothing}$.'
 ),
+(
+	'Setne',
+	'filtered-colimit-stable monomorphisms',
+	TRUE,
+	'This follows from <a href="/lemma/filtered-monos">this lemma</a> applied to the forgetful functor to $\mathbf{Set}$.'
+),
 (
 	'Setne',
 	'sequential limits',

database/data/004_property-assignments/Top.sql

@@ -71,6 +71,12 @@ VALUES
 	TRUE,
 	'The category has all limits and colimits, and the regular monomorphisms are the subspace inclusions. Thus, it suffices to prove that subspace inclusions are stable under pushouts. For a proof see e.g. Lemma 3.6 at the <a href="https://ncatlab.org/nlab/show/subspace+topology#pushout" target="_blank">nLab</a>.'
 ),
+(
+	'Top',
+	'filtered-colimit-stable monomorphisms',
+	TRUE,
+	'This follows from <a href="/lemma/filtered-monos">this lemma</a> applied to the forgetful functor to $\mathbf{Set}$.'
+),
 (
 	'Top',
 	'cartesian filtered colimits',

database/data/004_property-assignments/Top_pointed.sql

@@ -84,6 +84,12 @@ VALUES
 	'We continue the proof for <a href="/category/Set*">$\mathbf{Set}_*$</a> by showing that the natural bijective map <br>$\alpha : X \vee \lim_i Y_i \to \lim_i (X \vee Y_i)$<br>
 	is open. It suffices to consider open sets of two types: (1) If $U \subseteq X$ is open, the $\alpha$-image of $U \vee \lim_i Y_i$ is $p_{i_0}^{-1}(U \vee Y_{i_0})$ for any chosen index $i_0$, hence open. (2) If $i$ is an index and $V_i \subseteq Y_i$ is open, then the $\alpha$-image of $X \vee (p_i^{-1}(V_i) \cap \lim_i Y_i)$ is $p_i^{-1}(X \vee V_i)$, hence open.'
 ),
+(
+	'Top*',
+	'filtered-colimit-stable monomorphisms',
+	TRUE,
+	'This follows from <a href="/lemma/filtered-monos">this lemma</a> applied to the forgetful functor to $\mathbf{Set}$.'
+),
 (
 	'Top*',
 	'coregular',

database/data/005_implications/002_limits-colimits-behavior-implications.sql

@@ -69,6 +69,15 @@ VALUES
 	'This holds by definition.',
 	FALSE
 ),
+(
+	'exact_filtered_colimits_monos',
+	'["exact filtered colimits"]',
+	'["filtered-colimit-stable monomorphisms"]',
+	'This is because $X \to Y$ is a monomorphism iff the diagram
+	<p>$\begin{array}{ccc} X & \rightarrow & X \\ \downarrow && \downarrow \\ X & \rightarrow & Y \end{array}$</p>
+	is a pullback, and if a functor preserves finite limits, it preserves pullbacks in particular.',
+	FALSE
+),
 (
 	'cartesian_filtered_colimits_condition',
 	'["cartesian filtered colimits"]',

database/data/005_implications/004_morphism-behavior-implications.sql

@@ -152,4 +152,18 @@ VALUES
 	'["reflexive coequalizers"]',
 	'Every reflexive pair is equal: If $f s = g s = \mathrm{id}$, then since $s f  = \mathrm{id}$ (one-way), we must have $f = s^{-1}$, and likewise $g = s^{-1}$.',
 	FALSE
+),
+(
+	'filtered_monos_assumption',
+	'["filtered-colimit-stable monomorphisms"]',
+	'["filtered colimits"]',
+	'This holds by definition.',
+	FALSE
+),
+(
+	'filtered_monos_trivial',
+	'["left cancellative", "filtered colimits"]',
+	'["filtered-colimit-stable monomorphisms"]',
+	'This is trivial.',
+	FALSE
 );

database/data/010_lemmas/000_lemmas.sql

@@ -93,4 +93,13 @@ INSERT INTO lemmas (
     'Coreflection of subobject classifiers',
     'Let $\mathcal{D}$ be a category with a (regular) subobject classifier $\Omega$. Assume that $\mathcal{C} \to \mathcal{D}$ is a full subcategory such that (1) any (regular) $\mathcal{D}$-subobject of an object in $\mathcal{C}$ already lies in $\mathcal{C}$, (2) it is coreflective, i.e. there is a functor $R : \mathcal{D} \to \mathcal{C}$ right adjoint to the inclusion. Then $R(\Omega)$ is a (regular) subobject classifier in $\mathcal{C}$.',
     'If $X \in \mathcal{C}$, then $\mathrm{Hom}(X,R(\Omega)) \cong \mathrm{Hom}(X,\Omega)$ is isomorphic to the collection of $\mathcal{D}$-subobjects of $X$, which by assumption coincide with the $\mathcal{C}$-subobjects of $X$.'
+),
+(
+    'filtered-monos',
+    'Detection of filtered-colimit-stable monomorphisms',
+    'Let $\mathcal{C}$ be a category with filtered colimits. Assume that $U : \mathcal{C} \to \mathcal{D}$ is faithful functor which preserves monomorphisms and filtered colimits. If monomorphisms in $\mathcal{D}$ are stable under filtered colimits, then the same is true for $\mathcal{C}$.
+    <br><br>
+    For the record, here is the dual statement: Let $\mathcal{C}$ be a category with cofiltered limits. Assume that $U : \mathcal{C} \to \mathcal{D}$ is faithful functor which preserves epimorphisms and cofiltered limits. If epimorphisms in $\mathcal{D}$ are stable under cofiltered limits, then the same is true for $\mathcal{C}$.
+    ',
+    'Since $U$ is faithful, it reflects monomorphisms. From here the proof is straight forward.'
 );