Implications are not equivalences by default

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 <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>.
-  is_equivalence: false
 
 - id: malcev_implies_unital
   assumptions:
@@ -33,7 +30,6 @@
   conclusions:
     - unital
   proof: This follows from Corollary 2.2.10 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>. The proof is also written down in <a href="https://math.stackexchange.com/a/5034834" target="_blank">MSE/5033161</a>.
-  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

database/data/category-implications/NNO.yaml

@@ -6,15 +6,13 @@
   conclusions:
     - finite products
   proof: This holds by definition.
-  is_equivalence: false
 
 - id: nno_criterion
   assumptions:
     - countably distributive
   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

database/data/category-implications/accessible.yaml

@@ -34,31 +34,27 @@
   conclusions:
     - exact filtered colimits
   proof: Special case of <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Prop. 1.59 with $\lambda = \aleph_0$.
-  is_equivalence: false
 
 - id: finitely_accessible_stable_monos
   assumptions:
     - finitely accessible
   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:
     - locally finitely presentable
   conclusions:
     - locally ℵ₁-presentable
   proof: This is trivial.
-  is_equivalence: false
 
 - id: locally_countably_presentable_raise
   assumptions:
     - locally ℵ₁-presentable
   conclusions:
     - locally presentable
   proof: This is trivial.
-  is_equivalence: false
 
 - id: accessible_trivial_consequence
   assumptions:
@@ -67,23 +63,20 @@
     - 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:
     - accessible
   conclusions:
     - well-powered
   proof: See <a href="https://ncatlab.org/nlab/show/accessible+category#wellpoweredness_and_wellcopoweredness" target="_blank">nLab</a>.
-  is_equivalence: false
 
 - id: accessible_locally_small
   assumptions:
     - accessible
   conclusions:
     - locally essentially small
   proof: See the proof of Prop. 2.1.5 in <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>.
-  is_equivalence: false
 
 - id: accessible_well-copowered
   assumptions:
@@ -92,7 +85,6 @@
   conclusions:
     - well-copowered
   proof: See Thm. 2.49 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a> or Prop. 6.1.3 in <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>.
-  is_equivalence: false
 
 - id: finite_accessible
   assumptions:
@@ -101,7 +93,6 @@
   conclusions:
     - finitely accessible
   proof: See <a href="https://mathoverflow.net/questions/509853" target="_blank">MO/509853</a>, 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,31 +101,27 @@
   conclusions:
     - essentially small
   proof: This follows from <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Thm. 1.64.
-  is_equivalence: false
 
 - id: grothendieck_abelian_presentable
   assumptions:
     - Grothendieck abelian
   conclusions:
     - locally presentable
   proof: See <a href="https://arxiv.org/abs/1409.7051" target="_blank">Deriving Auslander's formula</a>, Cor. 5.2, or <a href="https://arxiv.org/abs/math/0102087" target="_blank">Sheafifiable homotopy model categories</a>, Prop. 3.10.
-  is_equivalence: false
 
 - id: algebraic_implies_lfp
   assumptions:
     - finitary algebraic
   conclusions:
     - locally finitely presentable
   proof: See <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Cor. 3.7.
-  is_equivalence: false
 
 - id: finitely_accessible_raise
   assumptions:
     - finitely accessible
   conclusions:
     - ℵ₁-accessible
   proof: This is because any regular cardinal is strictly smaller than its successor cardinal. See <a href="https://ncatlab.org/nlab/show/sharply+smaller+cardinal" target="_blank">nLab</a>.
-  is_equivalence: false
 
 - id: countably_accessible_special_case
   assumptions:
@@ -143,23 +130,20 @@
     - accessible
     - ℵ₁-filtered colimits
   proof: This is trivial.
-  is_equivalence: false
 
 - id: accessible_require_filtered_colimit
   assumptions:
     - finitely accessible
   conclusions:
     - filtered colimits
   proof: This holds by definition.
-  is_equivalence: false
 
 - id: accessible_require_Cauchy_complete
   assumptions:
     - accessible
   conclusions:
     - Cauchy complete
   proof: This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$. See also <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>, Prop. 2.2.1.
-  is_equivalence: false
 
 - id: small_accessible_characterization
   assumptions:
@@ -168,7 +152,6 @@
   conclusions:
     - accessible
   proof: See <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>, 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 (<a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, 4.30). Since multi-reflective full subcategories are in general closed under connected limits (<a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, 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

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 <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, 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 <a href="https://ncatlab.org/nlab/show/additive+category" target="_blank">nLab</a>.
-  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 <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. VIII.
-  is_equivalence: false
 
 - id: grothendieck_abelian_definition
   assumptions:
@@ -72,7 +68,6 @@
   conclusions:
     - cogenerator
   proof: See <a href="https://ncatlab.org/nlab/show/Categories+and+Sheaves" target="_blank">Kashiwara-Schapira</a>, Thm. 9.6.3.
-  is_equivalence: false
 
 - id: grothendieck_abelian_self-dual
   assumptions:
@@ -81,15 +76,13 @@
   conclusions:
     - trivial
   proof: This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, <i>Abelian categories</i>, p. 116.
-  is_equivalence: false
 
 - id: split_abelian_condition
   assumptions:
     - split abelian
   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

database/data/category-implications/algebraic.yaml

@@ -6,39 +6,34 @@
   conclusions:
     - finitary algebraic
   proof: This is trivial.
-  is_equivalence: false
 
 - id: algebraic_well-copowered
   assumptions:
     - one-sorted finitary algebraic
   conclusions:
     - well-copowered
   proof: See <a href="https://mathoverflow.net/questions/486607" target="_blank">MSE/486607</a>. 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:
     - finitary algebraic
   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:
     - generalized variety
   conclusions:
     - sifted colimits
   proof: This holds by definition.
-  is_equivalence: false
 
 - id: generalized_variety_implies_accessible
   assumptions:
     - generalized variety
   conclusions:
     - ℵ₁-accessible
   proof: See <a href="http://www.tac.mta.ca/tac/volumes/8/n3/8-03abs.html" target="_blank">[AR01, Remark 4.8(2)]</a>.
-  is_equivalence: false
 
 - id: groupoids_are_generalized_varieties
   assumptions:
@@ -48,7 +43,6 @@
     - generalized variety
     - finitely accessible
   proof: This is proven <a href="/content/sifted-colimits-in-groupoids">here</a>.
-  is_equivalence: false
 
 - id: generalized_variety_left_cancellative
   assumptions:
@@ -60,31 +54,27 @@
     Let $\C$ be a finitely accessible left cancellative category. The proof of <a href="/category-implication/sifted_colimits_left_cancellative">this result</a> 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:
     - generalized variety
   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:
     - multi-algebraic
   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:
     - finitary algebraic
   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 <a href="https://doi.org/10.1007/BF01224953" target="_blank">Yves Diers, Catégories Multialgébriques</a> or <a href="https://translations.thosgood.net/ADM-34-1980-193.pdf" target="_blank">its English translation</a>.
-  is_equivalence: false