diff --git a/database/data/category-implications/Malcev.yaml b/database/data/category-implications/Malcev.yaml index e11de605..f94b1f42 100644 --- a/database/data/category-implications/Malcev.yaml +++ b/database/data/category-implications/Malcev.yaml @@ -6,7 +6,6 @@ conclusions: - finitely complete proof: This holds by definition. - is_equivalence: false - id: malcev_thin_condition assumptions: @@ -15,7 +14,6 @@ conclusions: - Malcev proof: In a thin category, every subobject of $X^2 = X$ containing $X$ is already $X$. - is_equivalence: false - id: malcev_additive_criterion assumptions: @@ -24,7 +22,6 @@ conclusions: - Malcev proof: See Prop. 2.2.13. in Malcev, protomodular, homological and semi-abelian categories. - is_equivalence: false - id: malcev_implies_unital assumptions: @@ -33,7 +30,6 @@ conclusions: - unital proof: This follows from Corollary 2.2.10 in Malcev, protomodular, homological and semi-abelian categories. The proof is also written down in MSE/5033161. - is_equivalence: false - id: biproducts_unital assumptions: @@ -42,7 +38,6 @@ conclusions: - unital proof: For all objects $X,Y$ the canonical morphism $X \sqcup Y \to X \times Y$ is an isomorphism, hence a strong epimorphism. - is_equivalence: false - id: unital_assumptions assumptions: @@ -51,4 +46,3 @@ - finitely complete - pointed proof: This holds by definition. - is_equivalence: false diff --git a/database/data/category-implications/NNO.yaml b/database/data/category-implications/NNO.yaml index 98298588..8e7a5fb6 100644 --- a/database/data/category-implications/NNO.yaml +++ b/database/data/category-implications/NNO.yaml @@ -6,7 +6,6 @@ conclusions: - finite products proof: This holds by definition. - is_equivalence: false - id: nno_criterion assumptions: @@ -14,7 +13,6 @@ conclusions: - natural numbers object proof: 'Consider the copower $N \coloneqq \coprod_{n \in \IN} 1$ with inclusions $i_n : 1 \to N$ for $n \in \IN$. We define $z \coloneqq i_1 : 1 \to N$ and $s : N \to N$ by $s \circ i_n = i_{n+1}$. Since the category is countably distributive, we have $A \times N \cong \coprod_{n \in \IN} A$ for every object $A$. Given morphisms $f : A \to X$, $g : X \to X$, a morphism $\Phi : A \times N \to X$ therefore corresponds to a family of morphisms $\phi_n : A \to X$ for $n \in \IN$. The condition $\Phi(a,z)=f(a)$ becomes $\phi_0 = f$. The condition $\Phi(a,s(n)) = g(\Phi(a,n))$ becomes $\phi_{n+1} = g \circ \phi_n$. This recursively defines the morphisms $\phi_n$. (We are basically using that $\IN$ is a natural numbers object in $\Set$.) Concretely, $\phi_n = g^n \circ f$.' - is_equivalence: false - id: nno_pointed_case assumptions: @@ -23,7 +21,6 @@ conclusions: - trivial proof: 'Let $(N,z,s)$ be a natural numbers object in a category with a zero object, denoted $0$. The morphism $z : 0 \to N$ must be zero. The universal property applied to $A=1$ implies that $s : N \to N$ is an initial object in the category of endomorphisms. This exists, it is given by the identity $0 \to 0$. Therefore, $N = 0$. The general universal property now becomes: For all $f : A \to X$, $g : X \to X$ there is a unique $\Phi : A \to X$ such that $\Phi(a) = f(a)$ and $\Phi(a)=g(\Phi(a))$. Apply this to $g = 0$ to conclude $f = 0$.' - is_equivalence: false - id: nno_terminal assumptions: @@ -32,7 +29,6 @@ conclusions: - one-way proof: 'By assumption, $z : 1 \to N$ is an isomorphism. Therefore, the terminal object $1$ is a NNO with $z = \id_1$ and $s = \id_1$. This precisely means that for all $f : A \to X$ and $g : X \to X$ there is a unique $\Phi : A \to X$ with $\Phi = f$ and $\Phi = g \circ \Phi$. In other words, we have $f = g \circ f$, and therefore $g = \id_X$ (take $f = \id_X$), which proves the claim. (From here one can further deduce that the category is thin.)' - is_equivalence: false - id: nno_thin assumptions: @@ -41,4 +37,3 @@ conclusions: - natural numbers object proof: The triple $(1, \id_1, \id_1)$ is clearly a NNO. - is_equivalence: false diff --git a/database/data/category-implications/accessible.yaml b/database/data/category-implications/accessible.yaml index fe81d41d..49e73d9f 100644 --- a/database/data/category-implications/accessible.yaml +++ b/database/data/category-implications/accessible.yaml @@ -34,7 +34,6 @@ conclusions: - exact filtered colimits proof: Special case of Adamek-Rosicky, Prop. 1.59 with $\lambda = \aleph_0$. - is_equivalence: false - id: finitely_accessible_stable_monos assumptions: @@ -42,7 +41,6 @@ conclusions: - filtered-colimit-stable monomorphisms proof: 'Let $\C$ be a finitely accessible category and let $G$ be a set of finitely presentable objects which generates $\C$ under filtered colimits. Consider $G$ as a full subcategory and consider the restricted Yoneda embedding $\C \hookrightarrow [G^{\op},\Set]$. It preserves filtered colimits (essentially by the definition of a finitely presentable object) and all limits, in particular monomorphisms. It also reflects monomorphisms since $G$ is a generating set. Therefore, since $\Set$ and hence the functor category has filtered-colimit-stable monomorphisms, this is also true for $\C$.' - is_equivalence: false - id: locally_finitely_presentable_raise assumptions: @@ -50,7 +48,6 @@ conclusions: - locally ℵ₁-presentable proof: This is trivial. - is_equivalence: false - id: locally_countably_presentable_raise assumptions: @@ -58,7 +55,6 @@ conclusions: - locally presentable proof: This is trivial. - is_equivalence: false - id: accessible_trivial_consequence assumptions: @@ -67,7 +63,6 @@ - extremal generating set # TODO: refactor this once we add the property "has small dense subcategory" proof: The set appearing in the definition of a $\kappa$-accessible category gives a small dense full subcategory, which is in particular an extremal generating set. - is_equivalence: false - id: accessible_well-powered assumptions: @@ -75,7 +70,6 @@ conclusions: - well-powered proof: See nLab. - is_equivalence: false - id: accessible_locally_small assumptions: @@ -83,7 +77,6 @@ conclusions: - locally essentially small proof: See the proof of Prop. 2.1.5 in Makkai-Pare. - is_equivalence: false - id: accessible_well-copowered assumptions: @@ -92,7 +85,6 @@ conclusions: - well-copowered proof: See Thm. 2.49 in Adamek-Rosicky or Prop. 6.1.3 in Makkai-Pare. - is_equivalence: false - id: finite_accessible assumptions: @@ -101,7 +93,6 @@ conclusions: - finitely accessible proof: See MO/509853, where it is in fact shown that the ind-completion of any finite Cauchy-complete category becomes itself. - is_equivalence: false - id: locally_presentable_essentially_small assumptions: @@ -110,7 +101,6 @@ conclusions: - essentially small proof: This follows from Adamek-Rosicky, Thm. 1.64. - is_equivalence: false - id: grothendieck_abelian_presentable assumptions: @@ -118,7 +108,6 @@ conclusions: - locally presentable proof: See Deriving Auslander's formula, Cor. 5.2, or Sheafifiable homotopy model categories, Prop. 3.10. - is_equivalence: false - id: algebraic_implies_lfp assumptions: @@ -126,7 +115,6 @@ conclusions: - locally finitely presentable proof: See Adamek-Rosicky, Cor. 3.7. - is_equivalence: false - id: finitely_accessible_raise assumptions: @@ -134,7 +122,6 @@ conclusions: - ℵ₁-accessible proof: This is because any regular cardinal is strictly smaller than its successor cardinal. See nLab. - is_equivalence: false - id: countably_accessible_special_case assumptions: @@ -143,7 +130,6 @@ - accessible - ℵ₁-filtered colimits proof: This is trivial. - is_equivalence: false - id: accessible_require_filtered_colimit assumptions: @@ -151,7 +137,6 @@ conclusions: - filtered colimits proof: This holds by definition. - is_equivalence: false - id: accessible_require_Cauchy_complete assumptions: @@ -159,7 +144,6 @@ conclusions: - Cauchy complete proof: This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$. See also Makkai-Pare, Prop. 2.2.1. - is_equivalence: false - id: small_accessible_characterization assumptions: @@ -168,7 +152,6 @@ conclusions: - accessible proof: See Makkai-Pare, Thm. 2.2.2. - is_equivalence: false - id: countably_accessible_criterion assumptions: @@ -223,8 +206,6 @@ \end{align*}$$ Therefore, $u_{j'}$ is a split epimorphism in $\widehat{\C}$. Since $\C$ is Cauchy complete, it follows that $D_\infty$ is representable, represented by a retract of $D(j')$. Since $Y$ is fully faithful, this object is a colimit of $D$. - is_equivalence: false - - id: locally_presentable_another_definition assumptions: - accessible @@ -294,4 +275,3 @@ conclusions: - filtered-colimit-stable monomorphisms proof: Every locally finitely multi-presentable category is a multi-reflective full subcategory of a presheaf category closed under filtered colimits (Adamek-Rosicky, 4.30). Since multi-reflective full subcategories are in general closed under connected limits (Adamek-Rosicky, Thm. 4.26), in particular, we can calculate not only filtered colimits but also kernel pairs as well as in a presheaf category. - is_equivalence: false diff --git a/database/data/category-implications/additive.yaml b/database/data/category-implications/additive.yaml index 136b5e40..7b00f504 100644 --- a/database/data/category-implications/additive.yaml +++ b/database/data/category-implications/additive.yaml @@ -7,7 +7,6 @@ - locally essentially small - zero morphisms proof: This is trivial. - is_equivalence: false - id: preadditive_products_criterion assumptions: @@ -16,7 +15,6 @@ conclusions: - finite products proof: See Mac Lane, VIII.2., Theorem 2. - is_equivalence: false - id: additive_definition assumptions: @@ -33,7 +31,6 @@ conclusions: - biproducts proof: This is standard, see e.g. Prop. 2.1 on the nLab. - is_equivalence: false - id: abelian_definition assumptions: @@ -53,7 +50,6 @@ conclusions: - regular proof: In an abelian category, every epimorphism is regular, and epimorphisms are stable under pullbacks, see Mac Lane, Ch. VIII. - is_equivalence: false - id: grothendieck_abelian_definition assumptions: @@ -72,7 +68,6 @@ conclusions: - cogenerator proof: See Kashiwara-Schapira, Thm. 9.6.3. - is_equivalence: false - id: grothendieck_abelian_self-dual assumptions: @@ -81,7 +76,6 @@ conclusions: - trivial proof: This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, Abelian categories, p. 116. - is_equivalence: false - id: split_abelian_condition assumptions: @@ -89,7 +83,6 @@ conclusions: - abelian proof: This holds by definition. - is_equivalence: false - id: biproducts_definition_consequences assumptions: @@ -99,4 +92,3 @@ - finite products - zero morphisms proof: This holds by definition of biproducts. - is_equivalence: false diff --git a/database/data/category-implications/algebraic.yaml b/database/data/category-implications/algebraic.yaml index c5eae3bb..2d907a73 100644 --- a/database/data/category-implications/algebraic.yaml +++ b/database/data/category-implications/algebraic.yaml @@ -6,7 +6,6 @@ conclusions: - finitary algebraic proof: This is trivial. - is_equivalence: false - id: algebraic_well-copowered assumptions: @@ -14,7 +13,6 @@ conclusions: - well-copowered proof: See MSE/486607. Alternatively, one may combine the facts that one-sorted finitary algebraic categories are locally (finitely) presentable and that locally presentable categories are well-copowered, both of which are saved in the database. But we include the direct proof here as well, since it makes it easier to deduce the property for one-sorted finitary algebraic categories appearing in practice. - is_equivalence: false - id: finitary_algebraic_implies_regular assumptions: @@ -22,7 +20,6 @@ conclusions: - regular proof: The regular epimorphisms are precisely the sort-wise surjective homomorphisms, which are clearly stable under pullbacks. - is_equivalence: false - id: generalized_variety_require_sifted_colimit assumptions: @@ -30,7 +27,6 @@ conclusions: - sifted colimits proof: This holds by definition. - is_equivalence: false - id: generalized_variety_implies_accessible assumptions: @@ -38,7 +34,6 @@ conclusions: - ℵ₁-accessible proof: See [AR01, Remark 4.8(2)]. - is_equivalence: false - id: groupoids_are_generalized_varieties assumptions: @@ -48,7 +43,6 @@ - generalized variety - finitely accessible proof: This is proven here. - is_equivalence: false - id: generalized_variety_left_cancellative assumptions: @@ -60,7 +54,6 @@ Let $\C$ be a finitely accessible left cancellative category. The proof of this result shows that every sifted diagram $\I \to \C$ factors through the preorder reflection of $\I$, and hence reduces to a filtered diagram. Since $\C$ has filtered colimits, it therefore also has sifted colimits. It follows that every functor on $\C$ preserving filtered colimits automatically preserves sifted colimits. In particular, for representable functors this means that every finitely presentable object is automatically strongly finitely presentable. Now let $G$ be a set of finitely presentable objects in $\C$ generating all objects via filtered colimits. The claim follows because every filtered colimit is sifted and the objects in $G$ are strongly finitely presentable. - is_equivalence: false - id: generalized_variety_stable_monos assumptions: @@ -68,7 +61,6 @@ conclusions: - filtered-colimit-stable monomorphisms proof: 'Let $\C$ be a generalized variety and let $G$ be a set of strongly finitely presentable objects which generates $\C$ under sifted colimits. Consider $G$ as a full subcategory of $\C$ and consider the restricted Yoneda embedding $\C \hookrightarrow [G^{\op},\Set]$. It preserves sifted colimits (essentially by the definition of a strongly finitely presentable object) and therefore filtered colimits. It also preserves all limits, in particular monomorphisms, and it reflects monomorphisms since $G$ is a generating set. Therefore, since $\Set$ and hence the functor category has filtered-colimit-stable monomorphisms, this is also true for $\C$.' - is_equivalence: false - id: multi-algebraic_implies_locally_finitely_multi-presentable assumptions: @@ -76,7 +68,6 @@ conclusions: - locally finitely multi-presentable proof: This is because that every (finite product, coproduct)-sketch is clearly a (finite limit, coproduct)-sketch. - is_equivalence: false - id: algebraic_implies_multi-algebraic assumptions: @@ -84,7 +75,6 @@ conclusions: - multi-algebraic proof: This is because every finite-product-sketch is clearly a (finite product, coproduct)-sketch. - is_equivalence: false - id: multi-algebraic_another_definition assumptions: @@ -101,4 +91,3 @@ conclusions: - effective congruences proof: This is Thm. 4.0 in Yves Diers, Catégories Multialgébriques or its English translation. - is_equivalence: false diff --git a/database/data/category-implications/cancellative.yaml b/database/data/category-implications/cancellative.yaml index dc61d3ca..f83befd0 100644 --- a/database/data/category-implications/cancellative.yaml +++ b/database/data/category-implications/cancellative.yaml @@ -7,7 +7,6 @@ conclusions: - thin proof: 'If $f,g : A \rightrightarrows B$ are two morphisms, then $0_{B,B} \circ f = 0_{A,B} = 0_{B,B} \circ g$, so that $f = g$.' - is_equivalence: false - id: codiagonal-no-mono assumptions: @@ -16,7 +15,6 @@ conclusions: - thin proof: 'For every object $A$ the codiagonal $A + A \to A$ is a split epimorphism, and by assumption a monomorphism, hence an isomorphism. Hence, the two inclusions $i_1,i_2 : A \rightrightarrows A + A$ coincide. Now, if $f, g : A \rightrightarrows B$ are two morphisms, consider the induced morphism $h : A + A \to B$ and compute $f = h \circ i_1 = h \circ i_2 = g$.' - is_equivalence: false - id: cauchy_complete_criterion assumptions: @@ -24,7 +22,6 @@ conclusions: - Cauchy complete proof: Any idempotent monomorphism must be the identity and therefore splits. - is_equivalence: false - id: reflexive_pair_trivial assumptions: @@ -35,4 +32,3 @@ - effective congruences - reflexive coequalizers proof: 'Any parallel pair of morphisms $f,g : A \rightrightarrows B$ with a common section (or retraction) must be a pair of equal isomorphisms. In particular, they are the kernel pair of $\id_B$, and the cokernel pair of $\id_A$.' - is_equivalence: false diff --git a/database/data/category-implications/cartesian closed.yaml b/database/data/category-implications/cartesian closed.yaml index a8e6c17e..7566380c 100644 --- a/database/data/category-implications/cartesian closed.yaml +++ b/database/data/category-implications/cartesian closed.yaml @@ -6,7 +6,6 @@ conclusions: - finite products proof: This holds by definition. - is_equivalence: false - id: ccc_consequence assumptions: @@ -15,7 +14,6 @@ conclusions: - strict initial object proof: See the nLab. - is_equivalence: false - id: ccc_cartesian_filtered_colimits assumptions: @@ -24,7 +22,6 @@ conclusions: - cartesian filtered colimits proof: Each functor $X \times -$ is a left adjoint and therefore preserves (filtered) colimits. - is_equivalence: false - id: ccc_no_strict_terminal assumptions: @@ -33,7 +30,6 @@ conclusions: - thin proof: If a morphism $X \to Y$ exists, we get a morphism $1 \to [X,Y]$, which forces $[X,Y]$ to be a terminal object by assumption. But then any two morphisms $1 \rightrightarrows [X,Y]$ are equal, so that any two morphisms $X \rightrightarrows Y$ are equal. - is_equivalence: false - id: power_construction assumptions: @@ -50,7 +46,6 @@ & \cong \Hom(T,X)^I. \end{align*}$$ In the second isomorphism we have used that $T \times -$ preserves copowers, which is true because it is a left adjoint. - is_equivalence: false - id: countable_power_construction assumptions: @@ -59,7 +54,6 @@ conclusions: - countable powers proof: We can recycle this proof. - is_equivalence: false - id: pullbacks_are_local_products assumptions: @@ -67,7 +61,6 @@ conclusions: - pullbacks proof: Pullbacks are binary products in slice categories. - is_equivalence: false - id: locally_cartesian_closed_with_terminal_is_closed assumptions: @@ -76,7 +69,6 @@ conclusions: - cartesian closed proof: The slice over the terminal object is the category itself. - is_equivalence: false - id: lcc_implies_regular assumptions: @@ -86,7 +78,6 @@ conclusions: - regular proof: See Johnstone, Lemma A1.5.13. From this it follows also that every elementary topos is regular. - is_equivalence: false - id: cartesian_closed_thin_criterion assumptions: @@ -97,7 +88,6 @@ conclusions: - cartesian closed proof: This is an application of the adjoint functor theorem. Specifically, if $P$ is a complete lattice in which $\sup_i \inf(t,x_i) = \inf(t, \sup_i y_i)$ always holds, then the functor $\inf(t,-)$ is a left adjoint because it preserves all suprema. - is_equivalence: false - id: sequential_implies_lcc assumptions: @@ -106,7 +96,6 @@ conclusions: - locally cartesian closed proof: Each slice is thin, semi-strongly connected, and has a terminal object. Thus, it corresponds to a linear order with a largest element $1$. Every such category is cartesian closed, where the exponential $a \Rightarrow b$ (Heyting implication) is $1$ when $a \leq b$ and otherwise $b$. - is_equivalence: false - id: cartesian_closed_thin_implies_lcc assumptions: @@ -115,4 +104,3 @@ conclusions: - locally cartesian closed proof: In a thin category, every object is subterminal. Thus, the result follows from Corollary 6 here. - is_equivalence: false diff --git a/database/data/category-implications/completeness.yaml b/database/data/category-implications/completeness.yaml index 6d33b4a4..7eb169bf 100644 --- a/database/data/category-implications/completeness.yaml +++ b/database/data/category-implications/completeness.yaml @@ -8,7 +8,6 @@ - connected limits - finitely complete proof: This is trivial. - is_equivalence: false - id: complete_characterization assumptions: @@ -35,7 +34,6 @@ conclusions: - complete proof: See the nLab. - is_equivalence: false - id: multi-complete_generalize_limits assumptions: @@ -43,7 +41,6 @@ conclusions: - multi-complete proof: Limits are precisely multi-limits such that the set of cones is singleton. - is_equivalence: false - id: multi-terminal_special_case assumptions: @@ -51,7 +48,6 @@ conclusions: - multi-terminal object proof: This is trivial. - is_equivalence: false - id: multi-terminal_with_connected assumptions: @@ -69,4 +65,3 @@ conclusions: - complete proof: 'Let $\C$ be a category with an initial object, and let $D : \I \to \C$ be a small diagram in $\C$. Since $\C$ has an initial object, the category $\Cone(D)$ of cones over $D$ also has an initial object. In particular, $\Cone(D)$ is connected, hence a multi-terminal object in it automatically becomes a terminal object. In other words, a multi-limit of $D$ is automatically a limit of $D$.' - is_equivalence: false diff --git a/database/data/category-implications/congruences.yaml b/database/data/category-implications/congruences.yaml index c4c678cb..7e85b8bf 100644 --- a/database/data/category-implications/congruences.yaml +++ b/database/data/category-implications/congruences.yaml @@ -6,7 +6,6 @@ conclusions: - finitely complete proof: This holds by definition of a regular category. - is_equivalence: false - id: regular_well-powered_well-copowered assumptions: @@ -16,7 +15,6 @@ conclusions: - well-copowered proof: The regularity condition gives a bijection between the collection of quotients of $X$ and the collection of effective congruences on $X$, where the latter is a subcollection of the collection of subobjects of $X\times X$. - is_equivalence: false - id: regular_balanced_epi-regular assumptions: @@ -25,7 +23,6 @@ conclusions: - epi-regular proof: 'Given any epimorphism $f : X \twoheadrightarrow Y$ in a regular category, we have the factorization into a regular epimorphism $X \twoheadrightarrow \im(f)$ followed by a monomorphism $\im(f) \hookrightarrow Y$. Because the composition is an epimorphism, the monomorphism $\im(f) \hookrightarrow Y$ must also be an epimorphism, and therefore an isomorphism. It follows that $f$ is in fact a regular epimorphism.' - is_equivalence: false - id: congruence_quotients_are_reflexive_coequalizers assumptions: @@ -33,7 +30,6 @@ conclusions: - quotients of congruences proof: A congruence $E \rightrightarrows X$ has a common section $X \to E$ given by the reflexivity morphism. - is_equivalence: false - id: cokernels_via_congruence_quotients assumptions: @@ -43,7 +39,6 @@ conclusions: - cokernels proof: 'By the regularity assumption, it suffices to consider cokernels of subobjects. Given a subobject $Y$ of $X$, we have the congruence on $X$ given by the pullback of ${-} : X \times X \to X$ and $Y$. The quotient of this congruence is a cokernel of $Y \hookrightarrow X$.' - is_equivalence: false - id: congruence_quotients_via_cokernels assumptions: @@ -53,7 +48,6 @@ conclusions: - quotients of congruences proof: 'For any congruence $E$ on an object $X$ of a preadditive category, let $E_0$ be the kernel of $p_2 : E \to X$. The restriction of $p_1$ to $E_0$ is a monomorphism. We can then see that $E$ must be the pullback of $p_1 - p_2 : E \to X$ and $E_0 \hookrightarrow X$. Then the cokernel of $E_0 \hookrightarrow X$ is a quotient of $E$.' - is_equivalence: false - id: core-hin_quotients assumptions: @@ -62,7 +56,6 @@ - effective congruences - quotients of congruences proof: 'If $p_1, p_2 : E \rightrightarrows X$ is a congruence, the symmetry morphism $s : E \to E$ is an automorphism of $E$, hence equal to $\id_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\id_X$ is a coequalizer. Also, for the reflexivity morphism $r : X \to E$, we have $p_1 \circ r = \id$. For the reverse composition, $p_1 \circ r \circ p_1 = p_1 \circ \id$ and $p_2 \circ r \circ p_1 = p_2 \circ \id$, so since $p_1, p_2$ are jointly monomorphic, we get $r \circ p_1 = \id$. Therefore, $p_1 = p_2$ is an isomorphism, so $E$ is the kernel pair of $\id_X$.' - is_equivalence: false - id: preadditive_kernels_normal_imply_effective_congruences assumptions: @@ -77,7 +70,6 @@ To see this, suppose we have a pair of generalized elements $x_1, x_2 \in X(T)$. Then we have $$\begin{align*} (x_1,x_2) \in E & \iff (x_1 - x_2,0) \in E \\ & \iff x_1 - x_2 \in E_0 \\ & \iff h(x_1 - x_2) = 0 \\ & \iff h(x_1) = h(x_2). \end{align*}$$ In particular, applying the forward implications in the case $T \coloneqq E$, $x_1 \coloneqq f$, $x_2 \coloneqq g$, we conclude that $h \circ f = h \circ g$, so we get the required commutative diagram. From there, the reverse implications show this diagram is a cartesian square. - is_equivalence: false - id: additive_effective_congruences_imply_normal assumptions: @@ -87,7 +79,6 @@ - normal proof: >- Let $i : Y \hookrightarrow X$ be a monomorphism. Then we define a relation on $X$ via $E \coloneqq X \times Y$ with maps $f, g : E \rightrightarrows X$ defined by $f : (x, y) \mapsto x+i(y)$ and $g : (x, y) \mapsto x$. It is straightforward to check that $f$ and $g$ are jointly monomorphic. Now $E$ is a congruence because for generalized elements $x_1, x_2 \in X(T)$, $(x_1, x_2)$ factors through $E$ if and only if $x_1 - x_2$ factors through $Y$. In other words, the relation on $X(T)$ is exactly $x_1 \equiv x_2 \pmod{Y(T)}$, which is an equivalence relation on $X(T)$ (and in fact a congruence in $\Ab$). Now by assumption, $E$ is the kernel pair of some morphism $h : X \to Z$; in other words, $(x_1, x_2)$ factors through $E$ if and only if $h(x_1) = h(x_2)$. In particular, for $x \in X(T)$, $x$ factors through $Y$ if and only if $(x, 0)$ factors through $E$, which is equivalent to $h(x) = h(0) = 0$. We have thus shown that $Y$ is the kernel of $h$. - is_equivalence: false - id: regular_effective_congruences_implies_quotients assumptions: @@ -96,7 +87,6 @@ conclusions: - quotients of congruences proof: We assume that every congruence is effective, and the regularity condition implies that every effective congruence has a quotient. - is_equivalence: false - id: regular_epi-regular_extensive_consequences assumptions: @@ -118,7 +108,6 @@ Remark: The assumptions are satisfied in particular for every elementary topos. Therefore, every elementary topos has effective cocongruences and is co-Malcev. This special case is Example 2.2.18 in Malcev, protomodular, homological and semi-abelian categories. An alternative proof of this special case is given later in A.5.17. - is_equivalence: false - id: pretopos_balanced assumptions: @@ -137,7 +126,6 @@ g(y) & = \alpha(y)', & g(y') & = \alpha(y), \end{align*}$$ on generalized elements. Extensivity can be used to show that $f, g$ are jointly monomorphic. Clearly, the pair $f, g$ is reflexive and symmetric. For transitivity, one once again uses extensivity. By assumption, there is a morphism $h : B + B' \to C$ such that $f, g$ is the kernel pair of $h$, that is, two generalized elements $x, y \in B + B'$ satisfy $h(x) = h(y)$ if and only if $x = f(e)$, $y = g(e)$ for some $e \in E$. In particular, for $x \in B$, we have $h(x) = h(x')$ if and only if $x = f(e)$, $x' = g(e)$ for some $e \in E$. By disjointness of coproducts, we must necessarily have $e \in A$, and $x = \alpha(e)$. This shows that $\alpha$ is the equalizer of $h \circ i_1, h \circ i_2 : B \rightrightarrows C$. - is_equivalence: false - id: Barr-exact_definition assumptions: diff --git a/database/data/category-implications/connected.yaml b/database/data/category-implications/connected.yaml index 1c280ba1..0300ff75 100644 --- a/database/data/category-implications/connected.yaml +++ b/database/data/category-implications/connected.yaml @@ -6,7 +6,6 @@ conclusions: - inhabited proof: This holds by definition. - is_equivalence: false - id: strongly_connected_consequence assumptions: @@ -14,7 +13,6 @@ conclusions: - semi-strongly connected proof: This is immediate from the definition. - is_equivalence: false - id: semi-strongly_connected_consequence assumptions: @@ -22,7 +20,6 @@ conclusions: - connected proof: This is immediate from the definition. - is_equivalence: false - id: thin_not_strongly_connected assumptions: @@ -31,7 +28,6 @@ conclusions: - trivial proof: This is obvious. - is_equivalence: false - id: zero_morphisms_mean_strongly_connected assumptions: @@ -40,7 +36,6 @@ conclusions: - strongly connected proof: This holds by definition. - is_equivalence: false - id: strongly_connected_pointed_criterion assumptions: @@ -50,7 +45,6 @@ conclusions: - pointed proof: By assumption there is a morphism $1 \to 0$. There is also a unique morphism $0 \to 1$. They are necessarily inverse to each other. - is_equivalence: false - id: core-connected_implies_strongly-connected assumptions: @@ -58,7 +52,6 @@ conclusions: - strongly connected proof: This is trivial. - is_equivalence: false - id: unique_object_generates assumptions: @@ -73,7 +66,6 @@ is a bijection. Then for any object $T$, $$f \circ {-} : \Hom(T, X) \to \Hom(T, Y)$$ is a bijection since $T \cong G$, and the Yoneda embedding of $f$ is a natural transformation $\Hom({-}, X) \to \Hom({-}, Y)$. By the Yoneda Lemma, $f$ is therefore an isomorphism. - is_equivalence: false - id: trivial_is_core-connected assumptions: @@ -81,7 +73,6 @@ conclusions: - core-connected proof: This is trivial. - is_equivalence: false - id: core_connected_becomes_trivial assumptions: @@ -90,4 +81,3 @@ conclusions: - trivial proof: Every object is isomorphic to the initial object. - is_equivalence: false diff --git a/database/data/category-implications/discrete.yaml b/database/data/category-implications/discrete.yaml index b55abfc9..745d22bc 100644 --- a/database/data/category-implications/discrete.yaml +++ b/database/data/category-implications/discrete.yaml @@ -11,7 +11,6 @@ - self-dual - split abelian proof: This is trivial. - is_equivalence: false - id: discrete_consequences assumptions: @@ -22,7 +21,6 @@ - locally small - skeletal proof: This is trivial. - is_equivalence: false - id: essentially_discrete_characterization assumptions: @@ -40,7 +38,6 @@ - connected limits - locally essentially small proof: This is trivial. - is_equivalence: false - id: essentially_discrete_trivial assumptions: @@ -49,4 +46,3 @@ conclusions: - trivial proof: This is trivial. - is_equivalence: false diff --git a/database/data/category-implications/disjoint coproducts.yaml b/database/data/category-implications/disjoint coproducts.yaml index 44acb2df..5b011e9b 100644 --- a/database/data/category-implications/disjoint coproducts.yaml +++ b/database/data/category-implications/disjoint coproducts.yaml @@ -15,7 +15,6 @@ conclusions: - finite coproducts proof: This holds by definition. - is_equivalence: false - id: disjoint_coproducts_thin_trivial assumptions: @@ -24,7 +23,6 @@ conclusions: - trivial proof: For every object $A$ the two inclusions $A \rightrightarrows A + A$ must be equal, so their equalizer is $A$, but also $0$ since the coproduct is disjoint. Hence $A = 0$. - is_equivalence: false - id: disjoint_coproducts_strict assumptions: @@ -33,7 +31,6 @@ conclusions: - thin proof: 'Let $1$ be the strict terminal object, and let $A$ be any object. Then $1 \to A + 1$ is an isomorphism, since $1$ is strict. Also, $A \to A + 1$ is a monomorphism by assumption. It follows that the unique morphism $u : A \to 1$ is a monomorphism. For all $f,g : B \to A$ we have $uf = ug$ (since $1$ is terminal), hence $f = g$.' - is_equivalence: false - id: strongly_connected_disjoint_products assumptions: @@ -42,7 +39,6 @@ conclusions: - disjoint finite products proof: See MSE/5130190 for a proof. - is_equivalence: false - id: disjoint_coproduct_cogenerator assumptions: @@ -51,4 +47,3 @@ conclusions: - cogenerator proof: 'Assume that $S$ is a cogenerating set and let $Q \coloneqq \coprod_{X \in S} X$. For $X \in S$ we have a monomorphism $i_X : X \to Q$. If $f,g : A \rightrightarrows B$ are two distinct morphisms, there is some $X \in S$ and a morphism $h : B \to X$ with $hf \neq hg$. Hence, $i_X h f \neq i_X h g$. This proves that $Q$ is a cogenerator.' - is_equivalence: false diff --git a/database/data/category-implications/distributivity.yaml b/database/data/category-implications/distributivity.yaml index bbba6a4e..d7fc00ae 100644 --- a/database/data/category-implications/distributivity.yaml +++ b/database/data/category-implications/distributivity.yaml @@ -7,7 +7,6 @@ - coproducts - finite products proof: This holds by definition. - is_equivalence: false - id: countably_distributive_assumption assumptions: @@ -16,7 +15,6 @@ - countable coproducts - finite products proof: This holds by definition. - is_equivalence: false - id: distributive_assumption assumptions: @@ -25,7 +23,6 @@ - finite coproducts - finite products proof: This holds by definition. - is_equivalence: false - id: infinitary_distributive_trivial assumptions: @@ -33,7 +30,6 @@ conclusions: - countably distributive proof: This is trivial. - is_equivalence: false - id: countably_distributive_trivial assumptions: @@ -41,7 +37,6 @@ conclusions: - distributive proof: This is trivial. - is_equivalence: false - id: distributive_consequence assumptions: @@ -49,7 +44,6 @@ conclusions: - strict initial object proof: See the nLab or Prop. 3.4 in Introduction to extensive and distributive categories by Carboni-Lack-Walters. - is_equivalence: false - id: distributive_criterion assumptions: @@ -58,7 +52,6 @@ conclusions: - distributive proof: Each functor $A \times -$ is left adjoint and hence preserves finite coproducts (in fact, all colimits). - is_equivalence: false - id: countably_distributive_criterion assumptions: @@ -67,7 +60,6 @@ conclusions: - countably distributive proof: Each functor $A \times -$ is left adjoint and hence preserves countable coproducts (in fact, all colimits). - is_equivalence: false - id: infinitary_distributive_criterion assumptions: @@ -76,7 +68,6 @@ conclusions: - infinitary distributive proof: Each functor $A \times -$ is left adjoint and hence preserves coproducts (in fact, all colimits). - is_equivalence: false - id: infinite_distributive_filtered_criterion assumptions: @@ -86,7 +77,6 @@ conclusions: - infinitary distributive proof: Each functor $A \times -$ preserves finite coproducts and filtered colimits, hence all coproducts. - is_equivalence: false - id: countably_distributive_filtered_criterion assumptions: @@ -96,7 +86,6 @@ conclusions: - countably distributive proof: Each functor $A \times -$ preserves finite coproducts and filtered colimits, hence all countable coproducts. - is_equivalence: false - id: distributive_duality assumptions: @@ -105,4 +94,3 @@ conclusions: - codistributive proof: This is equivalent to the classical result that the distributivity law in a lattice can be defined in two ways, see e.g. Birkhoff, Lattice Theory, Ch. IX, Thm. 1. - is_equivalence: false diff --git a/database/data/category-implications/equalizers.yaml b/database/data/category-implications/equalizers.yaml index 153bb145..de1cf869 100644 --- a/database/data/category-implications/equalizers.yaml +++ b/database/data/category-implications/equalizers.yaml @@ -7,7 +7,6 @@ conclusions: - equalizers proof: 'The equalizer of $f,g : X \rightrightarrows Y$ is the pullback of $(f,g) : X \to Y \times Y$ with the diagonal $Y \to Y \times Y$.' - is_equivalence: false - id: coreflexive_equalizers_are_equalizers assumptions: @@ -15,7 +14,6 @@ conclusions: - coreflexive equalizers proof: This is trivial. - is_equivalence: false - id: equalizers_via_coreflexive_equalizers assumptions: @@ -24,7 +22,6 @@ conclusions: - equalizers proof: 'If $f,g : X \rightrightarrows Y$ are two morphisms, we have a coreflexive pair $(\id_X,f), (\id_X,g) : X \rightrightarrows X \times Y$. A morphism with codomain $X$ equalizes $f$ and $g$ if and only if it equalizes $(\id_X,f)$ and $(\id_X,g)$. Thus, their equalizers agree.' - is_equivalence: false - id: equalizers_consequence assumptions: @@ -32,7 +29,6 @@ conclusions: - Cauchy complete proof: 'If $e : X \to X$ is an idempotent, then the equalizer of $e, \id_X : X \rightrightarrows X$ provides a splitting of $e$.' - is_equivalence: false - id: reflexive_pair_trivial_2 assumptions: @@ -41,7 +37,6 @@ - coreflexive equalizers - reflexive coequalizers proof: Any parallel pair of morphisms with a common section (or retraction) must be a pair of equal isomorphisms. - is_equivalence: false - id: one-way_reflexive assumptions: @@ -49,7 +44,6 @@ conclusions: - reflexive coequalizers proof: 'Every reflexive pair is equal: If $f s = g s = \id$, then since $s f = \id$ (one-way), we must have $f = s^{-1}$, and likewise $g = s^{-1}$.' - is_equivalence: false - id: kernels_condition assumptions: @@ -57,7 +51,6 @@ conclusions: - zero morphisms proof: This is part of our definition of having kernels. - is_equivalence: false - id: kernels_criterion assumptions: @@ -66,7 +59,6 @@ conclusions: - kernels proof: This is trivial. - is_equivalence: false - id: equalizers_via_kernels assumptions: @@ -75,4 +67,3 @@ conclusions: - equalizers proof: The equalizer of $f,g$ is the kernel of $f-g$. - is_equivalence: false diff --git a/database/data/category-implications/exact filtered colimits.yaml b/database/data/category-implications/exact filtered colimits.yaml index bcddc8ba..17fdc590 100644 --- a/database/data/category-implications/exact filtered colimits.yaml +++ b/database/data/category-implications/exact filtered colimits.yaml @@ -8,7 +8,6 @@ - filtered colimits - finitely complete proof: This holds by definition. - is_equivalence: false - id: exact_filtered_colimits_monos assumptions: @@ -19,7 +18,6 @@ This is because $f : X \longrightarrow Y$ is a monomorphism iff the diagram $$\begin{CD} X @>{\id}>> X \\ @V{\id}VV @VV{f}V \\ X @>>{f}> Y \end{CD}$$ is a pullback, and if a functor preserves finite limits, it preserves pullbacks in particular. - is_equivalence: false - id: cartesian_filtered_colimits_condition assumptions: @@ -28,7 +26,6 @@ - filtered colimits - finite products proof: This holds by definition. - is_equivalence: false - id: exact_includes_cartesian_filtered_colimits assumptions: @@ -36,7 +33,6 @@ conclusions: - cartesian filtered colimits proof: If filtered colimits commute with finite limits, they commute with finite products in particular. - is_equivalence: false - id: thin_exact_filtered_colimits assumptions: @@ -45,7 +41,6 @@ conclusions: - exact filtered colimits proof: In a thin category, every (finite) limit can be reduced to a (finite) product. - is_equivalence: false - id: biproducts_cartesian_filtered_colimits assumptions: @@ -54,7 +49,6 @@ conclusions: - cartesian filtered colimits proof: If $I$ is a finite set, the product functor $\C^I \to \C$ is isomorphic to the coproduct functor $\C^I \to \C$, hence preserves all colimits that exist in $\C$. - is_equivalence: false - id: extensive_cocartesian_cofiltered_limits assumptions: @@ -64,7 +58,6 @@ conclusions: - cocartesian cofiltered limits proof: 'Let $\C$ be an extensive category with cofiltered limits and a terminal object. Then the coproduct functor $\C \times \C \cong \C/1 \times \C/1 \to \C/(1+1)$ is an equivalence. The forgetful functor $\C/A \to \C$ creates connected limits, and hence preserves cofiltered limits. For every $X \in \C$ the functor $(X,-) : \C \to \C \times \C$ also preserves cofiltered limits. The composition of these functors is $X \sqcup - : \C \to \C$ and therefore also preserves cofiltered limits.' - is_equivalence: false - id: filtered_monos_assumption assumptions: @@ -72,7 +65,6 @@ conclusions: - filtered colimits proof: This holds by definition. - is_equivalence: false - id: filtered_monos_trivial assumptions: @@ -81,7 +73,6 @@ conclusions: - filtered-colimit-stable monomorphisms proof: This is trivial. - is_equivalence: false - id: filtered_monos_iso assumptions: @@ -90,7 +81,6 @@ conclusions: - filtered-colimit-stable monomorphisms proof: This is trivial. - is_equivalence: false - id: CIP_assumption assumptions: @@ -100,7 +90,6 @@ - products - zero morphisms proof: This is true by definition. - is_equivalence: false - id: CIP_criterion assumptions: @@ -111,4 +100,3 @@ conclusions: - CIP proof: Let $(X_i)_{i \in I}$ be a family of objects. For every finite subset $E \subseteq I$ the canonical morphism $\coprod_{i \in E} X_i = \prod_{i \in E} X_i \to \prod_{i \in I} X_i$ is a (split) monomorphism. Hence, their colimit is also a monomorphism, which is the canonical morphism $\coprod_{i \in I} X_i \to \prod_{i \in I} X_i$. - is_equivalence: false diff --git a/database/data/category-implications/extensive.yaml b/database/data/category-implications/extensive.yaml index d44b6b32..e833b060 100644 --- a/database/data/category-implications/extensive.yaml +++ b/database/data/category-implications/extensive.yaml @@ -6,7 +6,6 @@ conclusions: - finite coproducts proof: This holds by definition. - is_equivalence: false - id: countably_extensive_assumption assumptions: @@ -14,7 +13,6 @@ conclusions: - countable coproducts proof: This holds by definition. - is_equivalence: false - id: infinitary_extensive_assumption assumptions: @@ -22,7 +20,6 @@ conclusions: - coproducts proof: This holds by definition. - is_equivalence: false - id: infinitary_extensive_countable assumptions: @@ -30,7 +27,6 @@ conclusions: - countably extensive proof: This is obvious. - is_equivalence: false - id: countably_extensive_finitary assumptions: @@ -38,7 +34,6 @@ conclusions: - extensive proof: This is obvious. - is_equivalence: false - id: extensive_consequences assumptions: @@ -47,7 +42,6 @@ - disjoint finite coproducts - strict initial object proof: These are Prop. 2.6 and 2.8 in Introduction to extensive and distributive categories by Carboni-Lack-Walters. - is_equivalence: false - id: extensive_distributivity assumptions: @@ -56,7 +50,6 @@ conclusions: - distributive proof: This is Prop. 4.5 in Introduction to extensive and distributive categories by Carboni-Lack-Walters. - is_equivalence: false - id: infinitary_extensive_distributivity assumptions: @@ -65,7 +58,6 @@ conclusions: - infinitary distributive proof: One can adjust the proof of Prop. 4.5 in Introduction to extensive and distributive categories by Carboni-Lack-Walters (which deals with the finite case). - is_equivalence: false - id: countably_extensive_distributivity assumptions: @@ -74,7 +66,6 @@ conclusions: - countably distributive proof: One can adjust the proof of Prop. 4.5 in Introduction to extensive and distributive categories by Carboni-Lack-Walters (which deals with the finite case). - is_equivalence: false - id: lcc_implies_extensive assumptions: @@ -83,7 +74,6 @@ conclusions: - extensive proof: 'The pullback functor preserves finite coproducts because it has a right adjoint. Remark: In combination with other implication, this result implies that every elementary topos is extensive.' - is_equivalence: false - id: lcc_extensive_yields_infinitary assumptions: @@ -93,4 +83,3 @@ conclusions: - infinitary extensive proof: The pullback functor preserves coproducts because it has a right adjoint. See also Remark 2.6 at the nLab. - is_equivalence: false diff --git a/database/data/category-implications/filtered + sifted.yaml b/database/data/category-implications/filtered + sifted.yaml index 6cc12900..651d39b2 100644 --- a/database/data/category-implications/filtered + sifted.yaml +++ b/database/data/category-implications/filtered + sifted.yaml @@ -6,7 +6,6 @@ conclusions: - sifted proof: 'Every filtered category $\C$ is inhabited and has final diagonal functors $\Delta : \C \to \C^J$ for all finite index categories $J$; in particular, it is inhabited and its diagonal $\Delta: \C \to \C \times \C$ is final.' - is_equivalence: false # TODO: with appropriate additional category properties, the hypothesis that the category is sifted could be weakened to a hypothesis that the category is inhabited and has cospans of all pairs, or equivalently that all finite sets of objects have a cospan - id: thin_sifted_is_filtered @@ -16,7 +15,6 @@ conclusions: - filtered proof: The assumption that the category is sifted implies that any finite set of objects (including an empty set) has a cospan. In order to conclude the category is filtered, the only thing left to show is that any parallel pair is coequalized by some morphism; but this is trivial in a thin category. - is_equivalence: false - id: sifted_is_connected assumptions: @@ -24,7 +22,6 @@ conclusions: - connected proof: Sifted categories are inhabited, and any two objects in a sifted category are joined by a cospan. - is_equivalence: false - id: coproducts_implies_sifted assumptions: @@ -33,7 +30,6 @@ conclusions: - sifted proof: The category is inhabited by assumption, and the coproduct of two objects is initial in the corresponding category of cospans. - is_equivalence: false - id: sifted_left_cancellative_implies_thin assumptions: @@ -47,7 +43,6 @@ in the category of cospans from $X$ to $X$ consists only of cospans $$X \xrightarrow{f} Y \xleftarrow{g} X$$ where $f=g$; hence when the category is also sifted, all cospans must be of this form, and so any two parallel morphisms are equal. - is_equivalence: false - id: filtered_criterion assumptions: @@ -55,7 +50,6 @@ conclusions: - filtered proof: Every finite diagram even admits a universal cocone. - is_equivalence: false - id: filtered_via_coequalizers assumptions: @@ -64,7 +58,6 @@ conclusions: - filtered proof: This is obvious. - is_equivalence: false - id: aleph1-filtered-consequence assumptions: @@ -72,7 +65,6 @@ conclusions: - filtered proof: This is trivial. - is_equivalence: false - id: aleph1-filtered_criterion assumptions: @@ -81,7 +73,6 @@ conclusions: - ℵ₁-filtered proof: Every countable diagram even admits a universal cocone. - is_equivalence: false - id: terminal_object_yields_kappa_filtered assumptions: @@ -89,7 +80,6 @@ conclusions: - ℵ₁-filtered proof: This is obvious. - is_equivalence: false - id: filtered-finite-thin assumptions: @@ -99,7 +89,6 @@ conclusions: - terminal object proof: Let $\C$ be a thin, filtered, and w.l.o.g. finite category. The identity diagram $\C \to \C$ admits a cocone. That is, there is an object $T$ with a morphism $A \to T$ for all $A \in \C$. Then $T$ is terminal. - is_equivalence: false - id: aleph1-filtered-countable-thin assumptions: @@ -109,4 +98,3 @@ conclusions: - terminal object proof: Let $\C$ be a thin, $\aleph_1$-filtered, and w.l.o.g. countable category. The identity diagram $\C \to \C$ admits a cocone. That is, there is an object $T$ with a morphism $A \to T$ for all $A \in \C$. Then $T$ is terminal. - is_equivalence: false diff --git a/database/data/category-implications/filtered colimits.yaml b/database/data/category-implications/filtered colimits.yaml index c9fc2b5c..c64fe6c5 100644 --- a/database/data/category-implications/filtered colimits.yaml +++ b/database/data/category-implications/filtered colimits.yaml @@ -22,7 +22,6 @@ Then $$f_n = f_{n+1} e = f_{n+2} e^2 = f_{n+2} e = f_{n+1}$$ shows that all the morphisms are equal. Thus, a cocone is the same as a morphism $f_0 : X \to Y$ with $f_0 = f_0 e$, meaning it coequalizes $\id_X,e : X \rightrightarrows X$. Hence, if a colimit exists, $e$ splits. - is_equivalence: false - id: directed_limits_consequence assumptions: @@ -30,7 +29,6 @@ conclusions: - sequential limits proof: This is trivial. - is_equivalence: false - id: sequential_limits_criterion assumptions: @@ -39,7 +37,6 @@ conclusions: - sequential limits proof: See Mac Lane, V.2, Prop. 3. The proof can easily be adapted to this case. Namely, the limit of $\cdots \to X_2 \to X_1 \to X_0$ is the equalizer of two suitable endomorphisms of $\prod_{n \geq 0} X_n$. - is_equivalence: false - id: direct_implies_sequential_limits assumptions: @@ -47,7 +44,6 @@ conclusions: - sequential limits proof: Assume that $\cdots \to A_2 \to A_1 \to A_0$ is a sequence of morphisms. We will prove that almost all of them are identities, so that the sequence is eventually constant and the limit exists. Assume the opposite, i.e. that there are infinitely many $A_k \to A_{k-1}$ which are not the identity. Pick some $n_1$ such that $A_{n_1} \to A_{n_1 - 1}$ is not the identity, and let $n_0 \coloneqq n_1 - 1$. If $A_{n_i} \to A_{n_{i-1}}$ has been constructed, there is some $n_{i+1} > n_i$ such that the composite $A_{n_{i+1}} \to A_{n_i}$ is not the identity, because otherwise it would follow inductively that all $A_{k+1} \to A_k$, $k \geq n_i$ would be identities, which would contradict our infiniteness assumption. This way we construct an infinite sequence of non-identity morphisms $A_{n_{i+1}} \to A_{n_i}$, a contradiction. - is_equivalence: false - id: finite_filtered_colimits # TODO: combine this with the implication with ID "finite_accessible" @@ -59,7 +55,6 @@ - filtered colimits - filtered-colimit-stable monomorphisms proof: We may assume that the category $\C$ is finite and Cauchy complete. The answer at MO/509853 shows that every filtered colimit in $\C$ exists, in fact it is a retract of one of the objects in the diagram. Now apply this to the morphism category of $\C$. It follows that for every filtered diagram of morphisms $X_i \to Y_i$ their colimit $X_\infty \to Y_\infty$ exists, which is a retract of one of the $X_i \to Y_i$. Therefore, if every $X_i \to Y_i$ is a monomorphism, also $X_\infty \to Y_\infty$ is a monomorphism. - is_equivalence: false - id: aleph1-filtered-colimits-include-filtered-colimits assumptions: @@ -67,7 +62,6 @@ conclusions: - ℵ₁-filtered colimits proof: Every $\aleph_1$-filtered category is also $\aleph_0$-filtered, i.e. filtered. Therefore, every $\aleph_1$-filtered diagram is also a filtered diagram, hence has a colimit by assumption. - is_equivalence: false - id: kappa-filtered-colimits_require_Cauchy_complete assumptions: @@ -75,7 +69,6 @@ conclusions: - Cauchy complete proof: More generally, if $\kappa$ is any infinite regular cardinal, a category with $\kappa$-filtered colimits must be Cauchy cocomplete. This is because the walking idempotent is $\kappa$-filtered. See also Makkai-Pare, Prop. 2.2.1. - is_equivalence: false - id: sifted_categories_are_connected assumptions: @@ -83,7 +76,6 @@ conclusions: - sifted colimits proof: This is because every sifted category is connected. - is_equivalence: false - id: sifted_colimits_consequence assumptions: @@ -92,7 +84,6 @@ - filtered colimits - reflexive coequalizers proof: This is because filtered categories are sifted and because the index category for a reflexive coequalizer is sifted. - is_equivalence: false - id: sifted_colimits_criterion assumptions: @@ -102,7 +93,6 @@ conclusions: - sifted colimits proof: See Cor. 5.2 in Chen's paper. - is_equivalence: false - id: sifted_colimits_left_cancellative assumptions: @@ -118,4 +108,3 @@ It follows that the diagram $D$ factors as $\I \to \I_p \to \C$, where $\I_p$ is the preorder reflection of $\I$ (same objects, with $i \leq j$ whenever there exists a morphism $i \to j$). Since $\I$ is sifted, the preordered set $\I_p$ is filtered. Hence, the diagram $\I_p \to \C$ has a colimit, and this colimit is also a colimit of the original diagram $\I \to \C$. - is_equivalence: false diff --git a/database/data/category-implications/generators.yaml b/database/data/category-implications/generators.yaml index deb3e38a..0f3b0062 100644 --- a/database/data/category-implications/generators.yaml +++ b/database/data/category-implications/generators.yaml @@ -7,7 +7,6 @@ - generating set - inhabited proof: This is trivial. - is_equivalence: false - id: extremal_generator_consequence assumptions: @@ -16,7 +15,6 @@ - extremal generating set - generator proof: This is trivial. - is_equivalence: false - id: extremal_generating_set_consequence assumptions: @@ -24,7 +22,6 @@ conclusions: - generating set proof: This is trivial. - is_equivalence: false - id: generator_balanced_consequence assumptions: @@ -33,7 +30,6 @@ conclusions: - extremal generator proof: This is immediate from the fact that any faithful functor out of a balanced category is also conservative (see here). - is_equivalence: false - id: generating_set_balanced_consequences assumptions: @@ -42,7 +38,6 @@ conclusions: - extremal generating set proof: This is immediate from the fact that any faithful functor out of a balanced category is also conservative (see here). - is_equivalence: false - id: generator_via_coproduct assumptions: @@ -52,7 +47,6 @@ conclusions: - generator proof: We get this as a corollary of this result. - is_equivalence: false - id: extremal_generator_via_coproduct assumptions: @@ -62,7 +56,6 @@ conclusions: - extremal generator proof: We get this as a corollary of this result. - is_equivalence: false - id: free-algebra-generates assumptions: @@ -70,7 +63,6 @@ conclusions: - extremal generator proof: Pick an algebraic theory that represents the category. The free algebra $F(1)$ on one generator is an extremal generator since it represents the underlying set functor, which is faithful and conservative. - is_equivalence: false - id: locally-finite_left-cancellative_semi-strongly-connected_extremal-generating-set assumptions: @@ -88,4 +80,3 @@ is an injective function between finite sets of equal cardinality, and therefore is also a bijection. By the assumption that $S$ is an extremal generating set, we thus have $f$ is an isomorphism. This shows that the collection of isomorphism classes of objects of $X$ is in bijection with a set. Together with the assumption that the category is locally finite, this implies the category is essentially small. - is_equivalence: false diff --git a/database/data/category-implications/groupoids.yaml b/database/data/category-implications/groupoids.yaml index a995b124..e72ac290 100644 --- a/database/data/category-implications/groupoids.yaml +++ b/database/data/category-implications/groupoids.yaml @@ -11,7 +11,6 @@ - self-dual - well-powered proof: This is easy. - is_equivalence: false - id: groupoid_criterion assumptions: @@ -21,7 +20,6 @@ conclusions: - groupoid proof: This is trivial. - is_equivalence: false - id: groupoid_connected assumptions: @@ -30,7 +28,6 @@ conclusions: - strongly connected proof: This is trivial. - is_equivalence: false - id: groupoid_lcc assumptions: @@ -38,7 +35,6 @@ conclusions: - locally cartesian closed proof: Every slice category is a trivial category. - is_equivalence: false - id: groupoid_generator assumptions: @@ -47,7 +43,6 @@ conclusions: - extremal generator proof: This is trivial. - is_equivalence: false - id: groupoid_generating_set assumptions: @@ -56,7 +51,6 @@ conclusions: - extremal generating set proof: This is trivial. - is_equivalence: false - id: groupoid_with_multi-terminal assumptions: @@ -65,4 +59,3 @@ conclusions: - thin proof: 'Let $f,g : A \rightrightarrows B$ be a parallel pair of morphisms. Since the category has a multi-terminal object, the connected component containing $A$ and $B$ has a terminal object. But since the category is a groupoid, both $A$ and $B$ are terminal objects in the connected component, hence $f=g$.' - is_equivalence: false diff --git a/database/data/category-implications/initial objects.yaml b/database/data/category-implications/initial objects.yaml index 00c4c284..b2cc1b6f 100644 --- a/database/data/category-implications/initial objects.yaml +++ b/database/data/category-implications/initial objects.yaml @@ -15,7 +15,6 @@ conclusions: - initial object proof: This holds by definition. - is_equivalence: false - id: strict_initial_trivial assumptions: @@ -24,7 +23,6 @@ conclusions: - trivial proof: If $0$ is the zero object, then for every object $A$ the unique morphism $A \to 0$ is an isomorphism by assumption. - is_equivalence: false - id: strict_initial_left_criterion assumptions: @@ -33,4 +31,3 @@ conclusions: - strict initial object proof: 'It suffices to prove that in general any monomorphism $f : A \to 0$ into an initial object is an isomorphism. If $g : 0 \to A$ is the unique morphism, then $f \circ g = \id_0$ since $0$ is initial. But then $f$ is a split epimorphism and a monomorphism, hence an isomorphism.' - is_equivalence: false diff --git a/database/data/category-implications/mono-regular.yaml b/database/data/category-implications/mono-regular.yaml index 1603ef10..ccb0ed09 100644 --- a/database/data/category-implications/mono-regular.yaml +++ b/database/data/category-implications/mono-regular.yaml @@ -6,7 +6,6 @@ conclusions: - balanced proof: Any regular monomorphism that is an epimorphism must be an isomorphism. - is_equivalence: false - id: normal_condition assumptions: @@ -14,7 +13,6 @@ conclusions: - zero morphisms proof: This is part of our definition of a normal category. - is_equivalence: false - id: mono_regular_via_kernels assumptions: @@ -22,7 +20,6 @@ conclusions: - mono-regular proof: This is trivial. - is_equivalence: false - id: normal_criterion assumptions: @@ -31,4 +28,3 @@ conclusions: - normal proof: The a monomorphism is the equalizer of $f,g$, it is the kernel of $f-g$. - is_equivalence: false diff --git a/database/data/category-implications/products.yaml b/database/data/category-implications/products.yaml index b348e231..bb752887 100644 --- a/database/data/category-implications/products.yaml +++ b/database/data/category-implications/products.yaml @@ -6,7 +6,6 @@ conclusions: - powers proof: This is trivial. - is_equivalence: false - id: products_include_aleph2-small_products assumptions: @@ -14,7 +13,6 @@ conclusions: - ℵ₂-small products proof: This is trivial. - is_equivalence: false - id: aleph2-small_products_consequences assumptions: @@ -23,7 +21,6 @@ - ℵ₂-small powers - countable products proof: This is trivial. - is_equivalence: false - id: finite_products_characterization assumptions: @@ -41,7 +38,6 @@ conclusions: - products proof: The product $\prod_{i \in I} X_i$ is the cofiltered limit of the finite partial products $\prod_{i \in E} X_i$ where $E$ ranges over the finite subsets of $I$. - is_equivalence: false - id: products_criterion_countable assumptions: @@ -50,7 +46,6 @@ conclusions: - products proof: The product $\prod_{i \in I} X_i$ is the $\aleph_1$-cofiltered limit of the countable partial products $\prod_{i \in C} X_i$ where $C$ ranges over the countable subsets of $I$. - is_equivalence: false - id: binary_products_criterion assumptions: @@ -59,7 +54,6 @@ conclusions: - binary products proof: If $1$ is a terminal object, then $X \times_1 Y = X \times Y$. - is_equivalence: false - id: countable_products_consequence assumptions: @@ -68,7 +62,6 @@ - countable powers - finite products proof: This is trivial. - is_equivalence: false - id: countable_products_criterion assumptions: @@ -77,7 +70,6 @@ conclusions: - countable products proof: If $X_1,X_2,\dotsc$ is an infinite sequence of objects, then their product is the limit of the sequence $\cdots \to X_2 \times X_1 \to X_1$. - is_equivalence: false - id: finite_products_include_finite_powers assumptions: @@ -85,7 +77,6 @@ conclusions: - finite powers proof: This is trivial. - is_equivalence: false - id: binary_products_include_binary_powers assumptions: @@ -93,7 +84,6 @@ conclusions: - binary powers proof: This is trivial. - is_equivalence: false - id: powers_include_aleph2-small_powers assumptions: @@ -101,7 +91,6 @@ conclusions: - ℵ₂-small powers proof: This is trivial. - is_equivalence: false - id: aleph2-small-powers_include_countable_powers assumptions: @@ -109,7 +98,6 @@ conclusions: - countable powers proof: This is trivial. - is_equivalence: false - id: countable_powers_include_finite_powers assumptions: @@ -117,7 +105,6 @@ conclusions: - finite powers proof: This is trivial. - is_equivalence: false - id: finite_powers_consequences assumptions: @@ -126,7 +113,6 @@ - binary powers - terminal object proof: This is trivial. - is_equivalence: false - id: countable_powers_criterion assumptions: @@ -135,7 +121,6 @@ conclusions: - countable powers proof: 'We can write $X^{\IN}$ as the limit of the sequence $\cdots \to X^3 \to X^2 \to X \to 1$ with transition morphisms $f_n : X^{n+1} \to X^n$, $(x_1,\dotsc,x_{n+1}) \mapsto (x_1,\dotsc,x_n)$, i.e., $p_i f_n = p_i$ for $1 \leq i \leq n$.' - is_equivalence: false - id: copowers_criterion assumptions: @@ -144,7 +129,6 @@ conclusions: - copowers proof: Let $\C$ be a category with filtered colimits and finite copowers. Let $X \in \C$ be an object and $I$ be a set. The poset $P_{<\aleph_0}(I)$ of finite subsets of $I$ is filtered, and we have a diagram $P_{<\aleph_0}(I) \to \C$, $A \mapsto A \otimes X$. Its colimit is the copower $I \otimes X$. - is_equivalence: false - id: copowers_criterion_countable assumptions: @@ -153,4 +137,3 @@ conclusions: - copowers proof: Let $\C$ be a category with $\aleph_1$-filtered colimits and countable copowers. Let $X \in \C$ be an object and $I$ be a set. The poset $P_{<\aleph_1}(I)$ of countable subsets of $I$ is $\aleph_1$-filtered, and we have a diagram $P_{<\aleph_1}(I) \to \C$, $A \mapsto A \otimes X$. Its colimit is the copower $I \otimes X$. - is_equivalence: false diff --git a/database/data/category-implications/pullbacks.yaml b/database/data/category-implications/pullbacks.yaml index 6b419247..0169b47a 100644 --- a/database/data/category-implications/pullbacks.yaml +++ b/database/data/category-implications/pullbacks.yaml @@ -7,7 +7,6 @@ conclusions: - pullbacks proof: 'The pullback of $f : X \to S$ and $g : Y \to S$ is the equalizer of $p_1 \circ f, \, p_2 \circ g : X \times Y \rightrightarrows S$.' - is_equivalence: false - id: connected_limits_characterization assumptions: @@ -34,4 +33,3 @@ conclusions: - wide pullbacks proof: Each slice category has finite products and is essentially finite, hence has all products by this result followed by this result. - is_equivalence: false diff --git a/database/data/category-implications/size.yaml b/database/data/category-implications/size.yaml index 3a036dfd..55d61f8f 100644 --- a/database/data/category-implications/size.yaml +++ b/database/data/category-implications/size.yaml @@ -7,7 +7,6 @@ - essentially small - locally small proof: This is trivial. - is_equivalence: false - id: essentially_small_consequences assumptions: @@ -18,7 +17,6 @@ - well-copowered - well-powered proof: All conclusions are trivial except perhaps that the category has an extremal generating set. For that, let $S$ be a set with one representative of each isomorphism class of objects of the category. Then it is easy to show using the Yoneda Lemma that $S$ is an extremal generating set. - is_equivalence: false - id: finite_consequence assumptions: @@ -27,7 +25,6 @@ - countable - essentially finite proof: This is trivial. - is_equivalence: false - id: essentially_finite_raise assumptions: @@ -36,7 +33,6 @@ - essentially countable - locally finite proof: This is trivial. - is_equivalence: false - id: countable_consequence assumptions: @@ -44,7 +40,6 @@ conclusions: - essentially countable proof: This is trivial. - is_equivalence: false - id: essentially_countable_consequence assumptions: @@ -52,7 +47,6 @@ conclusions: - essentially small proof: This is trivial. - is_equivalence: false - id: locally_small_consequence assumptions: @@ -60,7 +54,6 @@ conclusions: - locally essentially small proof: This is trivial. - is_equivalence: false - id: locally_finite_consequence assumptions: @@ -68,4 +61,3 @@ conclusions: - locally essentially small proof: This is trivial. - is_equivalence: false diff --git a/database/data/category-implications/subobject classifiers.yaml b/database/data/category-implications/subobject classifiers.yaml index 51680f15..079ac735 100644 --- a/database/data/category-implications/subobject classifiers.yaml +++ b/database/data/category-implications/subobject classifiers.yaml @@ -7,7 +7,6 @@ - finitely complete - mono-regular proof: 'The first part holds by convention, and the second part: any monomorphism $U \to X$ is the equalizer of $\chi_U,\chi_X : X \rightrightarrows \Omega$.' - is_equivalence: false - id: subobject_classifier_well-powered assumptions: @@ -16,7 +15,6 @@ conclusions: - well-powered proof: See Mac Lane & Moerdijk, Prop. I.3.1. - is_equivalence: false - id: subobject_classifier_pointed_case assumptions: @@ -25,7 +23,6 @@ conclusions: - normal proof: 'The universal property of $\top : 0 \to \Omega$ precisely says that every monomorphism $A \to B$ is the kernel of a unique morphism $B \to \Omega$, so it is normal.' - is_equivalence: false - id: additive_trivial_condition assumptions: @@ -34,7 +31,6 @@ conclusions: - trivial proof: See MSE/4086192. - is_equivalence: false - id: regular_subobjects_trivial assumptions: @@ -43,7 +39,6 @@ conclusions: - regular subobject classifier proof: In a right cancellative category, every regular monomorphism is an isomorphism, so that a terminal object is a regular subobject classifier. - is_equivalence: false - id: regular_subobject_weaker assumptions: @@ -51,7 +46,6 @@ conclusions: - regular subobject classifier proof: This is obvious. - is_equivalence: false - id: regular_subobject_assumption assumptions: @@ -59,7 +53,6 @@ conclusions: - finitely complete proof: This holds by definition. - is_equivalence: false - id: regular_subobjects_suffice assumptions: @@ -68,7 +61,6 @@ conclusions: - subobject classifier proof: This is obvious. - is_equivalence: false - id: regular_subobject_classifier_strict assumptions: @@ -77,4 +69,3 @@ conclusions: - thin proof: 'Let $\Omega$ be a regular subobject classifier. Since $1$ is a strict terminal object, $\top : 1 \to \Omega$ is an isomorphism. This implies that every regular monomorphism is an isomorphism. Hence, by taking the equalizer of two parallel morphisms, we see that the category is thin.' - is_equivalence: false diff --git a/database/data/category-implications/subobject-trivial.yaml b/database/data/category-implications/subobject-trivial.yaml index aa8fe61f..e701a27e 100644 --- a/database/data/category-implications/subobject-trivial.yaml +++ b/database/data/category-implications/subobject-trivial.yaml @@ -24,7 +24,6 @@ conclusions: - subobject-trivial proof: This is trivial. - is_equivalence: false - id: subobject-trivial_criterion assumptions: @@ -33,7 +32,6 @@ conclusions: - subobject-trivial proof: This is because a monomorphism which is also a regular epimorphism is an isomorphism. - is_equivalence: false - id: regular-subobject-trivial_criterion assumptions: @@ -41,7 +39,6 @@ conclusions: - regular-subobject-trivial proof: This is because any regular monomorphism is also an epimorphism, and therefore an isomorphism. - is_equivalence: false - id: regular_subobject_classifier_disallows_malcev assumptions: @@ -50,7 +47,6 @@ conclusions: - regular-subobject-trivial proof: 'The regular subobject classifier $\Omega$ is an internal poset (cf. Mac Lane & Moerdijk, IV.8). Concretely, since the category is Malcev, it has binary products, so the intersection of regular subobjects is again a regular subobject. Namely, the intersection of the equalizer of $f_1, g_1 : X \rightrightarrows Y_1$ with the equalizer of $f_2, g_2 : X \rightrightarrows Y_2$ is the equalizer of $(f_1, f_2), (g_1, g_2) : X \rightrightarrows Y_1 \times Y_2$. This intersection operation on regular subobjects yields a morphism $\wedge : \Omega \times \Omega \to \Omega$, and the internal relation ${\leq_{\Omega}} \subseteq \Omega \times \Omega$ is defined as the equalizer of $\wedge, p_1 : \Omega \times \Omega \rightrightarrows \Omega$. The relation ${\leq_{\Omega}}$ is reflexive, hence symmetric by assumption. Since it also antisymmetric and has a largest element $\top$, every regular monomorphism must be an isomorphism. (From here, we can infer that the category is thin – or, if the category has a subobject classifier, that the category is trivial.)' - is_equivalence: false - id: disjoint_finite_coproducts_disallows_regular-subobject-trivial assumptions: @@ -59,7 +55,6 @@ conclusions: - trivial proof: 'For any object $X$, the unique morphism $! : 0 \to X$ is a regular monomorphism, as the equalizer of the two coprojections $X \rightrightarrows X \sqcup X$. Therefore, it is an isomorphism.' - is_equivalence: false - id: disjoint_finite_coproducts_disallows_regular-quotient-trivial assumptions: @@ -68,4 +63,3 @@ conclusions: - trivial proof: 'For any object $X$, the coequalizer of the two coprojections $X \rightrightarrows X \sqcup X$ is the codiagonal $\nabla : X \sqcup X \to X$. Therefore, these two coprojections are equal. But their equalizer is also the unique morphism $! : 0 \to X$. It follows that $! : 0 \to X$ is an isomorphism.' - is_equivalence: false diff --git a/database/data/category-implications/thin.yaml b/database/data/category-implications/thin.yaml index 71f3a2e8..d6edc56e 100644 --- a/database/data/category-implications/thin.yaml +++ b/database/data/category-implications/thin.yaml @@ -10,7 +10,6 @@ - equalizers - left cancellative proof: This is trivial. - is_equivalence: false - id: thin_inhabited_consequence assumptions: @@ -19,7 +18,6 @@ conclusions: - generator proof: Any object will be a generator for trivial reasons. - is_equivalence: false - id: core-thin_products_thin assumptions: @@ -28,7 +26,6 @@ conclusions: - thin proof: 'Let $X$ be any object. The swap $\tau : X \times X \to X \times X$ is an automorphism, hence equal to the identity. It follows that the projections $p_1,p_2 : X \times X \rightrightarrows X$ are the same. And this means that every two morphisms $Y \rightrightarrows X$ are the same.' - is_equivalence: false - id: thin_via_locally-finite assumptions: @@ -37,7 +34,6 @@ conclusions: - thin proof: If $A,B$ are objects, we have a bijection $\Hom(A,B)^{\IN} \cong \Hom(A,B^{\IN})$. By assumption, this set is finite. Hence, $\Hom(A,B)$ has at most one element. - is_equivalence: false - id: thin_groupoids assumptions: @@ -46,7 +42,6 @@ conclusions: - thin proof: This is trivial. - is_equivalence: false - id: gaunt_characterization assumptions: @@ -64,7 +59,6 @@ - one-way - skeletal proof: 'The category is one-way since any non-identity endomorphism yields an infinite sequence of equal non-identity morphisms. The category is skeletal since any non-identity isomorphism $f : A \to B$ yields the infinite sequence $\dotsc,f^{-1},f,f^{-1},f$.' - is_equivalence: false - id: one-way_zero assumptions: @@ -75,7 +69,6 @@ proof: >- If $f,g : A \rightrightarrows B$ are two morphisms, then since $0_{B,B} = \id_B$ we have $$f = 0_{B,B} \circ f = 0_{A,B} = 0_{B,B} \circ g = g.$$ - is_equivalence: false - id: direct_criterion assumptions: @@ -85,7 +78,6 @@ conclusions: - direct proof: See the nLab for a proof. - is_equivalence: false - id: one-way_implies_core-thin assumptions: @@ -93,7 +85,6 @@ conclusions: - core-thin proof: This is trivial. - is_equivalence: false - id: freyd_small assumptions: @@ -102,7 +93,6 @@ conclusions: - thin proof: See Mac Lane, V.2, Prop. 3. The proof works for any category with powers. - is_equivalence: false - id: freyd_countable assumptions: @@ -111,7 +101,6 @@ conclusions: - thin proof: Adjust the proof of Mac Lane, V.2, Prop. 3. - is_equivalence: false - id: freyd_finite assumptions: @@ -120,7 +109,6 @@ conclusions: - thin proof: Adjust the proof of Mac Lane, V.2, Prop. 3. - is_equivalence: false - id: thin_finite_product_reduction assumptions: @@ -130,7 +118,6 @@ conclusions: - products proof: The category is equivalent to a finite preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a finite one. - is_equivalence: false - id: thin_countable_product_reduction assumptions: @@ -140,7 +127,6 @@ conclusions: - products proof: The category is equivalent to a countable preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a countable one. - is_equivalence: false - id: cocomplete_thin_criterion assumptions: @@ -150,7 +136,6 @@ conclusions: - cocomplete proof: The supremum of a subset in a (small) preordered set is the infimum of the set of upper bounds. - is_equivalence: false - id: thin_implies_regular assumptions: @@ -159,7 +144,6 @@ conclusions: - regular proof: In a thin category, regular epimorphisms are isomorphisms, and the rest is clear as well. - is_equivalence: false - id: thin_zero_trivial assumptions: @@ -169,7 +153,6 @@ conclusions: - trivial proof: This is easy. - is_equivalence: false - id: thin_power assumptions: @@ -178,7 +161,6 @@ conclusions: - powers proof: This is because for non-empty set $I$ the power $X^I$ is just $X$. - is_equivalence: false - id: thin_binary_power assumptions: @@ -186,4 +168,3 @@ conclusions: - binary powers proof: This is because $X \times X = X$. - is_equivalence: false diff --git a/database/data/category-implications/topos.yaml b/database/data/category-implications/topos.yaml index f52d5c02..05a89d3e 100644 --- a/database/data/category-implications/topos.yaml +++ b/database/data/category-implications/topos.yaml @@ -19,7 +19,6 @@ - epi-regular - finitely cocomplete proof: See Mac Lane & Moerdijk, Cor. IV.5.4, Cor. IV.10.5, Thm. 4.7.8; and Johnstone, Part A, Proposition 2.4.1. - is_equivalence: false - id: topos_well-copowered_criterion assumptions: @@ -28,7 +27,6 @@ conclusions: - well-copowered proof: This follows from Mac Lane & Moerdijk, Theorem IV.7.8 (and Prop. I.3.1). - is_equivalence: false - id: topos_implies_coregular assumptions: @@ -36,7 +34,6 @@ conclusions: - coregular proof: This is proven in Johnstone, A2.6.3. - is_equivalence: false - id: grothendieck_topos_definition assumptions: @@ -58,7 +55,6 @@ - infinitary extensive - locally presentable proof: A Grothendieck topos is locally presentable by Prop. 3.4.16 in Handbook of Categorical Algebra Vol. 3, has a cogenerator (see nLab) and is infinitary extensive by Giraud's Theorem. To show that it has exact filtered colimits, first observe that this is clearly true in every presheaf topos (since $\Set$ has the property). Every Grothendieck topos is a full reflective subcategory of a presheaf topos such that the reflector preserves finite limits (nLab), so we conclude with Lemma 3 here. - is_equivalence: false - id: topos_is_locally_cartesian_closed assumptions: @@ -66,7 +62,6 @@ conclusions: - locally cartesian closed proof: See Johnstone, Cor. A2.3.4. - is_equivalence: false - id: topos_no_stable_epis assumptions: @@ -76,7 +71,6 @@ 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$. - is_equivalence: false - id: pretopos_definition assumptions: diff --git a/database/data/functor-implications/adjoints.yaml b/database/data/functor-implications/adjoints.yaml index 2df2c48d..f4957adf 100644 --- a/database/data/functor-implications/adjoints.yaml +++ b/database/data/functor-implications/adjoints.yaml @@ -4,7 +4,6 @@ conclusions: - continuous proof: This is standard, see Mac Lane, Ch. V, Theorem 5.1. - is_equivalence: false - id: saft assumptions: @@ -20,7 +19,6 @@ conclusions: - right adjoint proof: This is the Special Adjoint Functor Theorem. The proof can be found, for example, at the nLab, or in Mac Lane, Ch. V, Theorem 8.2. - is_equivalence: false - id: reflector_consequences assumptions: @@ -29,7 +27,6 @@ - left adjoint - right-invertible proof: 'If $F : \C \to \D$ is a reflector, it is left adjoint to a fully faithful functor $G : \D \to \C$. Thus, the counit $\varepsilon : F \circ G \to \id_{\D}$ is an isomorphism (Prop. 3.4 at the nLab). This shows that $G$ is a right inverse of $F$.' - is_equivalence: false - id: representable_right_adjoint assumptions: @@ -41,7 +38,6 @@ conclusions: - right adjoint proof: 'If $\C$ is a locally small category with coproducts and $X \in \C$ is any object, then the copower functor $\Set \to \C$, $T \mapsto T \otimes X$ is left adjoint to $\Hom(X,-) : \C \to \Set$.' - is_equivalence: false - id: initial_object_as_left_adjoint assumptions: [] @@ -53,7 +49,6 @@ conclusions: - coreflector proof: 'Let $F : \C \to 1$ be the unique functor into the trivial category, and assume that $\C$ has an initial object $X$. Then the constant functor $X : 1 \to \C$ is fully faithful and left adjoint to $F$ because $\Hom(X(*),Y) \cong * \cong \Hom(*,F(Y))$.' - is_equivalence: false - id: reflector_preserves_terminal_objects assumptions: @@ -61,4 +56,3 @@ conclusions: - preserves terminal objects proof: 'Let $\C \subseteq \D$ be a full reflective subcategory with reflector $R : \D \to \C$ and unit morphisms $u(X) : X \to R(X)$ for $X \in \D$. The universal property says that every morphism from $X$ into an object in $\C$ factors uniquely through $u(X)$. Let $1 \in \D$ be a terminal object. We claim that $u(1) : 1 \to R(1)$ is an isomorphism. In fact, since $1$ is terminal, there is a (unique) morphism $v : R(1) \to 1$ in $\D$. The composition $v \circ u(1)$ is the identity since $1$ is terminal. To show that also the composition $u(1) \circ v$ is the identity of $R(1)$, by the universal property of $u(1)$ it suffices to prove $u(1) \circ v \circ u(1) = u(1)$, which is immediate from $v \circ u(1) = \id_1$. This shows $R(1) \cong 1$. Now, since $R(1)$ is an object in $\C$ which is terminal in $\D$, it is a terminal object of $\C$.' - is_equivalence: false diff --git a/database/data/functor-implications/equivalences.yaml b/database/data/functor-implications/equivalences.yaml index 325dbca9..b071242f 100644 --- a/database/data/functor-implications/equivalences.yaml +++ b/database/data/functor-implications/equivalences.yaml @@ -26,7 +26,6 @@ - monadic - reflector proof: This is easy. - is_equivalence: false - id: isomorphism_is_equivalence assumptions: @@ -34,4 +33,3 @@ conclusions: - equivalence proof: This is trivial. - is_equivalence: false diff --git a/database/data/functor-implications/limits preservation.yaml b/database/data/functor-implications/limits preservation.yaml index 86cbef07..463b489c 100644 --- a/database/data/functor-implications/limits preservation.yaml +++ b/database/data/functor-implications/limits preservation.yaml @@ -6,7 +6,6 @@ - preserves products - left exact proof: This is trivial. - is_equivalence: false - id: products_consequences assumptions: @@ -14,7 +13,6 @@ conclusions: - preserves finite products proof: This is trivial. - is_equivalence: false - id: preserve_finite_products_consequences assumptions: @@ -23,7 +21,6 @@ - preserves terminal objects - preserves binary products proof: This is trivial. - is_equivalence: false - id: preserve_finite_products_criterion assumptions: @@ -35,7 +32,6 @@ conclusions: - preserves finite products proof: This is because finite products can be constructed recursively via $X_1 \times \cdots \times X_{n+1} = (X_1 \times \cdots \times X_n) \times X_{n+1}$. We need the assumption on the domain since otherwise $X_1 \times \cdots \times X_n$ might not exist. See MSE/5142961. - is_equivalence: false - id: continuous_criterion assumptions: @@ -47,7 +43,6 @@ conclusions: - continuous proof: This follows from the construction of limits via equalizers and products, see Mac Lane, Ch. V, Theorem 2.2. - is_equivalence: false - id: continuous_criterion_filtered assumptions: @@ -59,7 +54,6 @@ conclusions: - continuous proof: This is because every limit can be written as a filtered limit of finite limits, see Mac Lane, Ch. IX, Theorem 1.1. - is_equivalence: false - id: product_criterion_filtered assumptions: @@ -71,7 +65,6 @@ conclusions: - preserves products proof: This is because every product can be written as a filtered limit of finite products, see Mac Lane, Ch. IX, Theorem 1.1. - is_equivalence: false - id: exact_definition assumptions: @@ -93,7 +86,6 @@ Finite products and equalizers are special cases of finite limits. Moreover, a morphism $f : X \to Y$ is a monomorphism if and only the square $$\begin{CD} X @>{\id_X}>> X \\ @V{\id_X}VV @VV{f}V \\ X @>>{f}> Y \end{CD}$$ is a pullback square, and pullbacks are special cases of finite limits. - is_equivalence: false - id: left_exact_criterion assumptions: @@ -105,7 +97,6 @@ conclusions: - left exact proof: This follows from the construction of finite limits via equalizers and finite products, see Mac Lane, Ch. V, Theorem 2.2. - is_equivalence: false - id: representable_is_continuous assumptions: @@ -113,7 +104,6 @@ conclusions: - continuous proof: This is standard, see Mac Lane, Ch. V, Theorem 4.1. - is_equivalence: false - id: equalizers_preservation_consequences assumptions: @@ -122,7 +112,6 @@ - preserves coreflexive equalizers - preserves regular monomorphisms proof: This is trivial. - is_equivalence: false - id: criterion_coreflexive_equalizers assumptions: @@ -134,7 +123,6 @@ conclusions: - preserves equalizers proof: This follows easily from this result about categories and its proof. - is_equivalence: false - id: mono-preserving_criterion assumptions: @@ -145,7 +133,6 @@ conclusions: - preserves monomorphisms proof: This is trivial. - is_equivalence: false - id: regular-mono-preserving_criterion assumptions: @@ -156,7 +143,6 @@ conclusions: - preserves regular monomorphisms proof: This is trivial. - is_equivalence: false - id: another_regular-mono-preserving_criterion assumptions: @@ -167,7 +153,6 @@ conclusions: - preserves regular monomorphisms proof: 'Let $F : \C \to \D$ be a functor preserving coreflexive equalizers, where $\C$ has pushouts; we only need that $\C$ has cokernel pairs. Let $i : X \to Y$ be a regular monomorphism in $\C$. By Prop. 3.2 at the nLab, $i$ is the equalizer of the two canonical morphisms $u_1,u_2 : Y \rightrightarrows Y \sqcup_X Y$ into the cokernel pair of $i$. By the universal property of the pushout, there is a morphism $\nabla : Y \sqcup_X Y \to Y$ with $\nabla u_1 = \nabla u_2 = \id_Y$. Thus, $u_1,u_2$ is a coreflexive pair. Since $F$ preserves coreflexive equalizers by assumption, $F(i)$ is the equalizer of $F(u_1), F(u_2)$. In particular, $F(i)$ is a regular monomorphism.' - is_equivalence: false - id: zero_preserving_condition assumptions: @@ -180,7 +165,6 @@ conclusions: - preserves initial objects proof: This is trivial. - is_equivalence: false - id: biproduct_preserving_condition assumptions: @@ -220,7 +204,6 @@ Remark: It now follows that $F$ is also additive, i.e., for two morphisms $f,g : A \rightrightarrows B$, we have $F(f+g) = F(f) + F(g)$. In fact, $f+g$ decomposes as $$A \xrightarrow{(f,g)} B \times B \xrightarrow{\mu^{-1}} B \sqcup B \xrightarrow{\nabla} B,$$ and each of these components is preserved by $F$. - is_equivalence: false - id: regular_functor_definition assumptions: @@ -239,7 +222,6 @@ conclusions: - continuous proof: 'We need to show that for every category $\C$ the unique functor $!_{\C} : \C \to 1$ into the trivial category is continuous. This easy to verify directly because in the trivial category every limit is, well, trivial. More generally, for every category $\C$ and every set $S$ the diagonal functor $\Delta : \C \to \C^S$ is continuous. Here we apply this to $S = \varnothing$ so that $\C^S$ is the trivial category.' - is_equivalence: false - id: automatically_preserve_equalizers assumptions: [] @@ -249,7 +231,6 @@ conclusions: - preserves equalizers proof: This is trivial. - is_equivalence: false - id: trivial_coreflexive_equalizer_preservation # TODO: rework this once we add "split-epi-trivial" @@ -260,7 +241,6 @@ conclusions: - preserves coreflexive equalizers proof: 'Let $f,g : X \rightrightarrows Y$ be a coreflexive pair, i.e. there is a morphism $r : Y \to X$ with $rf = rg = \id_X$. Then $r$ is a split and hence a regular epimorphism. Thus, $r$ is an isomorphism. But then $f=g$, and $\id_X$ is an equalizer of $f,g$. This equalizer is obviously preserved.' - is_equivalence: false - id: thin_binary_product_preservation assumptions: [] @@ -273,4 +253,3 @@ conclusions: - preserves binary products proof: 'It is enough to prove that if $P$ is a linearly ordered set and $Q$ is a partially ordered set, then any order-preserving map $f : P \to Q$ preserves binary meets. Let $x,y \in P$. We may assume $x \leq y$. Then $x \wedge y = x$. Since we also have $f(x) \leq f(y)$, we have $f(x) \wedge f(y) = f(x)$. Therefore, $f(x \wedge y) = f(x) = f(x) \wedge f(y)$ holds.' - is_equivalence: false diff --git a/database/data/functor-implications/misc.yaml b/database/data/functor-implications/misc.yaml index 6ff468de..15fc0930 100644 --- a/database/data/functor-implications/misc.yaml +++ b/database/data/functor-implications/misc.yaml @@ -17,7 +17,6 @@ conclusions: - faithful proof: 'Let $f,g : X \rightrightarrows Y$ be two morphisms in the domain, and choose an equalizer $E \hookrightarrow X$. By assumption, $F(E) \to F(X)$ is the equalizer of $F(f),F(g) : F(X) \rightrightarrows F(Y)$. Thus, if $F(f) = F(g)$, then $F(E) \to F(X)$ is an isomorphism. Since $F$ is conservative, $E \to X$ is an isomorphism, which means $f = g$.' - is_equivalence: false - id: conservative_criterion assumptions: @@ -25,7 +24,6 @@ conclusions: - conservative proof: If $F(f)$ is an isomorphism, its inverse has the form $F(g)$ since $F$ is full. Since $F$ is faithful, it follows that $f$ is inverse to $g$. - is_equivalence: false - id: faithful_with_balanced_domain assumptions: @@ -37,7 +35,6 @@ - conservative # TODO: refactor this if adding "reflects monomorphisms" / "reflects epimorphisms" properties proof: 'It is easy to see that a faithful functor $F$ reflects monomorphisms: If we have two morphisms $x_1, x_2 : U \rightrightarrows X$ and $f : X \to Y$ such that $f(x_1) = f(x_2)$, and $F(f)$ is a monomorphism, then $F(x_1) = F(x_2)$; therefore, $x_1 = x_2$, so $f$ is also a monomorphism. The dual argument shows that $F$ also reflects epimorphisms. Therefore, if $F(f)$ is an isomorphism, then $f$ is both a monomorphism and an epimorphism; by the assumption on the domain category, this implies that $f$ is an isomorphism.' - is_equivalence: false - id: left-invertible_consequences assumptions: @@ -47,7 +44,6 @@ - essentially injective - conservative proof: 'Let $G : \D \to \C$ be a left-inverse to $F : \C \to \D$, meaning that $G \circ F \cong \id_{\C}$. Then $F(A) \cong F(B)$ implies $A \cong G(F(A)) \cong G(F(B)) \cong B$ for all $A,B \in \C$. Thus, $F$ essentially injective. Moreover, since $G \circ F$ is faithful, the composed map $\Hom(A,B) \to \Hom(F(A),F(B)) \to \Hom(G(F(A)),G(F(B))$ is injective, so that also $\Hom(A,B) \to \Hom(F(A),F(B))$ is injective. This shows that $F$ is faithful. Finally, if $f : A \to B$ is a morphism such that $F(f)$ is an isomorphism, then $G(F(f))$ is an isomorphism. Since $G(F(f)) \cong f$ in $\Mor(\C)$, we conclude that $f$ is an isomorphism. Therefore, $F$ is conservative.' - is_equivalence: false - id: right-invertible_consequences assumptions: @@ -55,7 +51,6 @@ conclusions: - essentially surjective proof: This is trivial. - is_equivalence: false - id: full-on-isomorphisms_criterion assumptions: @@ -64,7 +59,6 @@ conclusions: - full on isomorphisms proof: This is obvious. - is_equivalence: false - id: full-on-isomorphisms_consequences assumptions: @@ -72,7 +66,6 @@ conclusions: - essentially injective proof: This is trivial. - is_equivalence: false - id: pseudomonic_definition assumptions: @@ -89,7 +82,6 @@ conclusions: - conservative proof: 'Let $F$ be a pseudomonic functor and let $f$ be a morphism in its domain such that $F(f)$ is an isomorphism. Then $F(f)^{-1} = F(g)$ for some isomorphism $g$ since $F$ is full on isomorphisms. Then $f \circ g$ and $g \circ f$ are identities since $F$ is faithful and their images are identities.' - is_equivalence: false - id: essentially-surjective_implies_dominant assumptions: @@ -97,7 +89,6 @@ conclusions: - dominant proof: This is trivial. - is_equivalence: false - id: surjective_functor_to_core_connected_category assumptions: [] @@ -109,7 +100,6 @@ conclusions: - essentially surjective proof: 'Let $F : \C \to \D$ be a functor from an inhabited category to a core-connected category. Choose any object $X \in \C$. For every $Y \in \D$ we have $Y \cong F(X)$. Thus, $F$ is essentially surjective.' - is_equivalence: false - id: right_invertible_functor_to_trivial_category assumptions: [] @@ -121,7 +111,6 @@ conclusions: - right-invertible proof: 'Let $\C$ be an inhabited category and let $F : \C \to 1$ be the unique functor to the trivial category. Choose any object $X \in \C$. Then the constant functor $X : 1 \to \C$ satisfies $F \circ X = \id_1$.' - is_equivalence: false - id: full_functor_to_trivial_category # TODO: add the converse once we have category_conclusions @@ -134,7 +123,6 @@ conclusions: - full proof: 'Let $\C$ be a strongly connected category. Then the unique functor $F : \C \to 1$ to the trivial category is full: for all $X,Y \in \C$ the map $\Hom(X,Y) \to \Hom(F(X),F(Y))$ is surjective since its domain is non-empty and its codomain is a singleton set.' - is_equivalence: false - id: functor_conservative_on_groupoids assumptions: [] @@ -144,7 +132,6 @@ conclusions: - conservative proof: This is trivial. - is_equivalence: false - id: automatic_ess_injective_functors assumptions: [] @@ -154,7 +141,6 @@ conclusions: - essentially injective proof: This is trivial. - is_equivalence: false - id: automatic_full_on_isos_functors assumptions: [] @@ -166,7 +152,6 @@ conclusions: - full on isomorphisms proof: This is trivial. - is_equivalence: false - id: thin_dominant_functor # TODO: rework this once we add "split-mono trivial" @@ -178,7 +163,6 @@ conclusions: - essentially surjective proof: This is trivial since every split monomorphism in the codomain is an isomorphism. - is_equivalence: false - id: automatic_preserves_mono assumptions: [] @@ -188,4 +172,3 @@ conclusions: - preserves monomorphisms proof: This is trivial since every morphism in the codomain is a monomorphism. - is_equivalence: false diff --git a/database/data/functor-implications/monadic.yaml b/database/data/functor-implications/monadic.yaml index 591fb5c8..631f45d4 100644 --- a/database/data/functor-implications/monadic.yaml +++ b/database/data/functor-implications/monadic.yaml @@ -6,7 +6,6 @@ - faithful - right adjoint proof: This is clear since for a monad $T$ the forgetful functor from the category of $T$-algebras has these properties. - is_equivalence: false - id: crude_monadicity_theorem assumptions: @@ -19,7 +18,6 @@ conclusions: - monadic proof: This is the crude monadicity theorem. A proof can be found in Mac Lane & Moerdijk, Thm. IV.4.2. - is_equivalence: false - id: monadic_fully_faithful assumptions: @@ -29,4 +27,3 @@ - monadic - left-invertible proof: A direct proof of monadicity is possible and straight forward. Alternatively, one can use Beck's monadicity theorem, since a fully faithful functor $U$ is conservative and creates coequalizers of $U$-split pairs. For the left adjoint $L$ the counit $L \circ U \to \id$ is an isomorphism (since $U$ is fully faithful, see Prop. 3.4 at the nLab), which shows that $U$ is left-invertible. - is_equivalence: false diff --git a/database/data/morphism-implications/misc.yaml b/database/data/morphism-implications/misc.yaml index 6dd21979..9862f1b4 100644 --- a/database/data/morphism-implications/misc.yaml +++ b/database/data/morphism-implications/misc.yaml @@ -6,7 +6,6 @@ conclusions: - constant proof: This is trivial. - is_equivalence: false - id: zero_morphism_definition assumptions: @@ -31,4 +30,3 @@ Furthermore, $0_{A,B}$ is coconstant because for all $g,h : B \rightrightarrows C$ we have $$g \circ 0_{A,B} = 0_{A,C} = h \circ 0_{A,B}.$$ (A similar argument shows that $0_{A,B}$ is also constant.) - is_equivalence: false diff --git a/database/data/morphism-implications/mono-epi-iso.yaml b/database/data/morphism-implications/mono-epi-iso.yaml index 040be5a1..1742ebb5 100644 --- a/database/data/morphism-implications/mono-epi-iso.yaml +++ b/database/data/morphism-implications/mono-epi-iso.yaml @@ -5,7 +5,6 @@ - split monomorphism - effective monomorphism proof: This is trivial. - is_equivalence: false - id: split_mono_is_regular_mono assumptions: @@ -13,7 +12,6 @@ conclusions: - regular monomorphism proof: 'Let $m : A \to B$ be a split monomorphism, and choose a morphism $e : B \to A$ with $e \circ m = \id_A$. Then it is easy to check that $m$ is an equalizer of $\id_B$ and the idempotent morphism $m \circ e : B \to B$.' - is_equivalence: false - id: split_mono_epi_is_iso # This implication follows strictly from the others, but we add it @@ -24,7 +22,6 @@ conclusions: - isomorphism proof: 'Assume that $m : A \to B$ is a split monomorphism, and choose a morphism $e : B \to A$ with $e \circ m = \id_A$. Then $m \circ e \circ m = m = {\id_B} \circ m$. Thus, if $m$ is also an epimorphism, we conclude $m \circ e = \id_B$, showing that $m$ is an isomorphism with inverse $e$.' - is_equivalence: false - id: mono_is_iso assumptions: @@ -35,7 +32,6 @@ conclusions: - isomorphism proof: This holds by definition of a subobject-trivial category. - is_equivalence: false - id: balanced_def assumptions: @@ -47,7 +43,6 @@ conclusions: - isomorphism proof: This holds by definition of a balanced category. - is_equivalence: false - id: mono-regular_def assumptions: @@ -58,7 +53,6 @@ conclusions: - regular monomorphism proof: This is the definition of a mono-regular category. - is_equivalence: false - id: regular_mono_is_strict assumptions: @@ -66,7 +60,6 @@ conclusions: - strict monomorphism proof: 'Let $m : A \to B$ be the equalizer of $f,g : B \rightrightarrows C$. In particular, $m$ is a monomorphism. Let $t : T \to B$ be a morphism that equalizes all pairs that are equalized by $m$. In particular, $t$ equalizes $f,g$, i.e. $f \circ t = g \circ t$. By definition of an equalizer, this means that $t$ factors through $m$.' - is_equivalence: false - id: effective_mono_implies_regular_mono assumptions: @@ -74,7 +67,6 @@ conclusions: - regular monomorphism proof: This is trivial. - is_equivalence: false - id: strict_monos_are_often_effective assumptions: @@ -90,7 +82,6 @@ By composing these equations with $t$, we get $$f \circ t = (f;g) \circ i_1 \circ t = (f;g) \circ i_2 \circ t = g \circ t.$$ Thus, $t$ equalizes every parallel pair that is equalized by $m$. Since $m$ is a strict monomorphism, $t$ factors through $m$. - is_equivalence: false - id: iso_is_normal_mono assumptions: @@ -101,7 +92,6 @@ conclusions: - normal monomorphism proof: This is trivial. - is_equivalence: false - id: normal_mono_is_regular assumptions: @@ -109,7 +99,6 @@ conclusions: - regular monomorphism proof: This is trivial. - is_equivalence: false - id: regular_implies_normal_mono_preadditive_case assumptions: @@ -120,7 +109,6 @@ conclusions: - normal monomorphism proof: 'The equalizer of $f,g : B \rightrightarrows C$ is the kernel of $f-g : B \to C$.' - is_equivalence: false - id: strict_mono_is_strong assumptions: @@ -131,7 +119,6 @@ Consider a commutative diagram $$\begin{CD} C @>e>> D \\ @VVV @VVV \\ A @>>m> B \end{CD}$$ where $e$ is an epimorphism and $m$ is a strict monomorphism. We need to show that $D \to B$ factors through $m$. It suffices to show that it equalizes all pairs $B \rightrightarrows T$ that are equalized by $m$. Since $e$ is an epimorphism, it suffices to check this for the composite $C \to D \to B$. This is equal to $C \to A \to B$, which factors through $m$ and hence equalizes the pair. - is_equivalence: false - id: extremal_mono_is_mono assumptions: @@ -139,7 +126,6 @@ conclusions: - monomorphism proof: This holds by definition. - is_equivalence: false - id: strong_mono_is_extremal assumptions: @@ -150,7 +136,6 @@ Assume that $m : A \to B$ is a strong monomorphism that factors as $m = g \circ e$, where $e : A \to C$ is an epimorphism and $g : C \to B$ is any morphism. Then the commutative diagram $$\begin{CD} A @>e>> C \\ @V{\id_A}VV @VV{g}V \\ A @>>m> B \end{CD}$$ can be filled with a morphism $h : C \to A$. In particular, $h \circ e = \id_A$. Thus, $e$ is an epimorphism and a split monomorphism, hence an isomorphism. - is_equivalence: false - id: extremal_mono_epi_is_iso assumptions: @@ -159,7 +144,6 @@ conclusions: - isomorphism proof: This is obvious. - is_equivalence: false - id: extremal_monos_are_regular_in_coregular_category assumptions: @@ -173,7 +157,6 @@ Let $m : A \to B$ be an extremal monomorphism in a coregular category. By coregularity, we may factor it as $m = i \circ e$, where $i : C \to B$ is a regular monomorphism and $e : A \to C$ is an epimorphism. Since $m$ is an extremal monomorphism, $e$ is an isomorphism. Therefore, $m \cong i$ is a regular monomorphism. The proof shows that the assumption of coregularity can be relaxed to the existence of (Epi, RegMono)-factorizations. - is_equivalence: false - id: extremal_mono_strong_criterion assumptions: @@ -190,7 +173,6 @@ $$\begin{CD} C @>{e}>> D \\ @V{f}VV @VV{u}V \\ A @>>{v}> P. \end{CD}$$ Here, $v$ is an epimorphism since $e$ is an epimorphism. Moreover, by the universal property of the pushout, there is a unique morphism $h : P \to B$ such that $h \circ v = m$ and $h \circ u = g$. Since $m$ is an extremal monomorphism, $v$ is an isomorphism. Then $v^{-1} \circ u : D \to A$ is the required filling of the first diagram, since $$v^{-1} \circ u \circ e = v^{-1} \circ v \circ f = f.$$ - is_equivalence: false - id: extremal_mono_balanced assumptions: @@ -201,7 +183,6 @@ conclusions: - extremal monomorphism proof: Assume $m$ is a monomorphism that factors as $m = g \circ e$, where $e$ is an epimorphism. But then $e$ is also a monomorphism, and since the category is balanced, $e$ must be an isomorphism. - is_equivalence: false - id: every_mono_strong_criterion assumptions: @@ -212,4 +193,3 @@ conclusions: - strong monomorphism proof: Any monomorphism is right orthogonal to any regular epimorphism because regular epimorphisms are strong (by combining this result and this result). - is_equivalence: false diff --git a/database/data/symmetric_monoidal_category_implications/closed.yaml b/database/data/symmetric_monoidal_category_implications/closed.yaml index 5da42f18..c52a4fd4 100644 --- a/database/data/symmetric_monoidal_category_implications/closed.yaml +++ b/database/data/symmetric_monoidal_category_implications/closed.yaml @@ -9,7 +9,6 @@ conclusions: - closed proof: This is just the definition of a cartesian closed category. - is_equivalence: false - id: when_closed_implies_cocomplete assumptions: @@ -20,7 +19,6 @@ conclusions: - cocomplete proof: Each functor $A \otimes -$ is a left adjoint and therefore preserves colimits. - is_equivalence: false - id: when_closed_implies_finitely_cocomplete assumptions: @@ -31,7 +29,6 @@ conclusions: - finitely cocomplete proof: Each functor $A \otimes -$ is a left adjoint and therefore preserves finite colimits. - is_equivalence: false - id: when_closed_implies_distributive assumptions: @@ -42,7 +39,6 @@ conclusions: - distributive proof: Each functor $A \otimes -$ is a left adjoint and therefore preserves finite coproducts. - is_equivalence: false - id: when_closed_implies_infinitary_distributive assumptions: @@ -53,4 +49,3 @@ conclusions: - infinitary distributive proof: Each functor $A \otimes -$ is a left adjoint and therefore preserves coproducts. - is_equivalence: false diff --git a/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml b/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml index de4941f5..cf708c39 100644 --- a/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml +++ b/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml @@ -7,7 +7,6 @@ - finitely cocomplete - infinitary distributive proof: This is trivial. - is_equivalence: false - id: finitely_cocomplete_consequences assumptions: @@ -15,7 +14,6 @@ conclusions: - distributive proof: This is trivial. - is_equivalence: false - id: infinitary_distributive_consequence assumptions: @@ -23,7 +21,6 @@ conclusions: - distributive proof: This is trivial. - is_equivalence: false - id: distributive_cartesian assumptions: @@ -35,7 +32,6 @@ - distributive proof: This is just the definition of a distributive category. # TODO: make this an equivalence when we have category_conclusions - is_equivalence: false - id: infinitary_distributive_cartesian assumptions: @@ -47,7 +43,6 @@ - infinitary distributive proof: This is just the definition of an infinitary distributive category. # TODO: make this an equivalence when we have category_conclusions - is_equivalence: false - id: cartesian_never_complete assumptions: @@ -56,7 +51,6 @@ conclusions: - trivial proof: In a codistributive symmetric monoidal category, for every object $X$, the functor $X \otimes -$ preserves the terminal object $1$. But since the symmetric monoidal structure is assumed to be cartesian, $1$ is the monoidal unit, so $1 = X \otimes 1 = X$. - is_equivalence: false - id: preadditive_codistributive_criterion assumptions: @@ -67,4 +61,3 @@ conclusions: - codistributive proof: This follows from this result on functors. - is_equivalence: false diff --git a/database/data/symmetric_monoidal_category_implications/misc.yaml b/database/data/symmetric_monoidal_category_implications/misc.yaml index e1fdfc0f..c2193b3e 100644 --- a/database/data/symmetric_monoidal_category_implications/misc.yaml +++ b/database/data/symmetric_monoidal_category_implications/misc.yaml @@ -9,7 +9,6 @@ - cocomplete - self-dual proof: This is trivial. - is_equivalence: false - id: trivial_is_well_pointed # we need this separately since well-pointed currently has no dual @@ -18,7 +17,6 @@ conclusions: - well-pointed proof: This is trivial. - is_equivalence: false - id: thin_is_well_pointed assumptions: [] @@ -28,4 +26,3 @@ conclusions: - well-pointed proof: In a thin category, every object is a generator for trivial reasons. - is_equivalence: false diff --git a/database/schema/003_implications.sql b/database/schema/003_implications.sql index a9c94bd2..13979359 100644 --- a/database/schema/003_implications.sql +++ b/database/schema/003_implications.sql @@ -2,7 +2,8 @@ CREATE TABLE implications ( id TEXT PRIMARY KEY, type TEXT NOT NULL, proof TEXT NOT NULL CHECK (length(proof) > 0), - is_equivalence INTEGER NOT NULL DEFAULT FALSE, + is_equivalence INTEGER NOT NULL DEFAULT FALSE + CHECK (is_equivalence IN (TRUE, FALSE)), is_deduced INTEGER NOT NULL DEFAULT FALSE, UNIQUE (id, type), FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index 9d08286f..12ea9d8e 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -482,7 +482,7 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri process.exit(1) } - implication_insert.run(impl.id, type, impl.proof, Number(impl.is_equivalence)) + implication_insert.run(impl.id, type, impl.proof, impl.is_equivalence ? 1 : 0) for (const assumption of impl.assumptions) { assumption_insert.run(impl.id, assumption, type) diff --git a/database/scripts/utils/seed.types.ts b/database/scripts/utils/seed.types.ts index 7009feb8..3220b375 100644 --- a/database/scripts/utils/seed.types.ts +++ b/database/scripts/utils/seed.types.ts @@ -87,5 +87,5 @@ export type ImplicationYaml = { conclusions: string[] associated_assumptions?: Partial> proof: string - is_equivalence: boolean + is_equivalence?: boolean }