add property: cartesian filtered colimits

Author: ScriptRaccoon

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

@@ -82,6 +82,15 @@ VALUES
 	NULL,
 	TRUE
 ),
+(
+	'cartesian filtered colimits',
+	'has',
+	'In a category $\mathcal{C}$, which we assume to have filtered colimits and finite products, we say that <i>filtered colimits are cartesian</i> if for every finite set $I$ the product functor $\prod : \mathcal{C}^I \to \mathcal{C}$ preserves filtered colimits. Equivalently, for every $X \in \mathcal{C}$ the functor $X \times - : \mathcal{C} \to \mathcal{C}$ preserves filtered colimits.<br>
+	This is no standard terminology, it has been suggested in <a href="https://mathoverflow.net/questions/510240" target="_blank">MO/510240</a>. We have added it to the database since it clarifies the relationship between many related properties.',
+	NULL,
+	NULL,
+	TRUE
+),
 (
 	'disjoint finite coproducts',
 	'has',

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

@@ -151,6 +151,10 @@ VALUES
 ('codistributive', 'finite coproducts'),
 ('exact filtered colimits', 'filtered colimits'),
 ('exact filtered colimits', 'finitely complete'),
+('exact filtered colimits', 'cartesian filtered colimits'),
+('cartesian filtered colimits', 'filtered colimits'),
+('cartesian filtered colimits', 'finite products'),
+('cartesian filtered colimits', 'exact filtered colimits'),
 ('generator', 'generating set'),
 ('generating set', 'generator'),
 ('Grothendieck abelian', 'abelian'),

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

@@ -62,6 +62,20 @@ VALUES
 	'This holds by definition.',
 	FALSE
 ),
+(
+	'cartesian_filtered_colimits_condition',
+	'["cartesian filtered colimits"]',
+	'["filtered colimits", "finite products"]',
+	'This holds by definition.',
+	FALSE
+),
+(
+	'exact_includes_cartesian_filtered_colimits',
+	'["exact filtered colimits"]',
+	'["cartesian filtered colimits"]',
+	'If filtered colimits commute with finite limits, they commute with finite products in particular.',
+	FALSE
+),
 (
 	'infinitary_distributive_consequence',
 	'["infinitary distributive"]',
@@ -162,7 +176,7 @@ VALUES
 ),
 (
 	'infinite_distributive_filtered_criterion',
-	'["distributive", "exact filtered colimits", "coproducts"]',
+	'["distributive", "cartesian filtered colimits", "coproducts"]',
 	'["infinitary distributive"]',
 	'Each functor $A \times -$ preserves finite coproducts and filtered colimits, hence all coproducts.',
 	FALSE

database/data/005_implications/006_trivial-categories-implications.sql

@@ -117,4 +117,11 @@ VALUES
 	'["binary powers"]',
 	'This is because $X \times X = X$.',
 	FALSE
+),
+(
+	'thin_exact_filtered_colimits',
+	'["thin", "cartesian filtered colimits"]',
+	'["exact filtered colimits"]',
+	'In a thin category, every (finite) limit can be reduced to a (finite) product.',
+	FALSE
 );

database/data/005_implications/008_topos-theory-implications.sql

@@ -27,6 +27,13 @@ VALUES
 	'See the <a href="https://ncatlab.org/nlab/show/strict+initial+object" target="_blank">nLab</a>.',
 	FALSE
 ),
+(
+	'ccc_cartesian_filtered_colimits',
+	'["cartesian closed", "filtered colimits"]',
+	'["cartesian filtered colimits"]',
+	'Each functor $X \times -$ is a left adjoint and therefore preserves (filtered) colimits.',
+	FALSE
+),
 (
 	'ccc_no_strict_terminal',
 	'["cartesian closed", "strict terminal object"]',