Add isomorphisms of categories

databases/catdat/data/functor-implications/equivalences.yaml

@@ -27,3 +27,11 @@
     - reflector
   proof: This is easy.
   is_equivalence: false
+
+- id: isomorphism_is_equivalence
+  assumptions:
+    - isomorphism
+  conclusions:
+    - equivalence
+  proof: This is trivial.
+  is_equivalence: false

databases/catdat/data/functor-properties/equivalence.yaml

@@ -1,16 +1,16 @@
 id: equivalence
 relation: is an
-description: A functor is an <i>equivalence</i> if it has a pseudo-inverse functor.
+description: 'A functor $F : \C \to \D$ is an <i>equivalence</i> when there is a functor $G : \D \to \C$ with $F \circ G \cong \id_{\D}$ and $G \circ F \cong \id_{\C}$. In contrast to an isomorphism of categories, these compositions are only required to be <i>isomorphic</i> to the identities.'
 nlab_link: https://ncatlab.org/nlab/show/equivalence+of+categories
 invariant_under_equivalences: true
 dual_property: equivalence
 related_properties:
   - full
   - faithful
   - essentially surjective
-  - continuous
-  - cocontinuous
+  - right-invertible
   - left-invertible
+  - isomorphism
 
 tags:
   - invertibility

databases/catdat/data/functor-properties/isomorphism.yaml

@@ -0,0 +1,11 @@
+id: isomorphism
+relation: is an
+description: 'A functor $F : \C \to \D$ is an <i>isomorphism</i> when there is a functor $G : \D \to \C$ with $F \circ G = \id_{\D}$ and $G \circ F = \id_{\C}$. In contrast to an equivalence of categories, these compositions are required to be <i>equal</i> to the identities.'
+nlab_link: https://ncatlab.org/nlab/show/equivalence+of+categories#Isomorphism
+invariant_under_equivalences: false
+dual_property: isomorphism
+related_properties:
+  - equivalence
+
+tags:
+  - invertibility

databases/catdat/data/functors/id_Set.yaml

@@ -16,7 +16,7 @@ related_functors:
   - diagonal_sets
 
 satisfied_properties:
-  - property: equivalence
+  - property: isomorphism
     proof: This is trivial.
 
   - property: representable

databases/catdat/data/functors/opposite_category.yaml

@@ -0,0 +1,20 @@
+id: opposite_category
+name: opposite category functor
+notation: $(-)^{\op}$
+source: Cat
+target: Cat
+description: 'This functor maps a small category $\C$ to its opposite category $\C^{\op}$ and a functor $F : \C \to \D$ to the opposite functor $F^{\op} : \C^{\op} \to \D^{\op}$.'
+nlab_link: https://ncatlab.org/nlab/show/opposite+category
+left_adjoint: opposite_category
+
+tags:
+  - category theory
+
+related_functors:
+  - opposite_monoid
+
+satisfied_properties:
+  - property: isomorphism
+    proof: This functor is inverse to itself.
+
+unsatisfied_properties: []

databases/catdat/data/functors/opposite_monoid.yaml

@@ -0,0 +1,20 @@
+id: opposite_monoid
+name: opposite monoid functor
+notation: $(-)^{\op}$
+source: Mon
+target: Mon
+description: 'This functor maps a monoid $M$ to its opposite monoid $M^{\op}$ which has the multiplication $a *^{\op} b \coloneqq a * b$. A monoid homomorphism $f : M \to N$ is also a monoid homomorphism $f^{\op} : M^{\op} \to N^{\op}$.'
+nlab_link: https://ncatlab.org/nlab/show/opposite+magma
+left_adjoint: opposite_monoid
+
+tags:
+  - algebra
+
+related_functors:
+  - opposite_category
+
+satisfied_properties:
+  - property: isomorphism
+    proof: This functor is inverse to itself.
+
+unsatisfied_properties: []

databases/catdat/data/functors/walking_isomorphism_object_inclusion.yaml

@@ -0,0 +1,23 @@
+id: walking_isomorphism_object_inclusion
+name: walking isomorphism object inclusion
+notation: $\iota$
+source: '1'
+target: walking_isomorphism
+description: 'This is the natural embedding of the trivial category with a single object $0$ into the walking isomorphism given by two objects $0,1$ and an isomorphism $0 \to 1$. This is the simplest example of an equivalence of categories which is not an isomorphism.'
+nlab_link: null
+
+tags:
+  - category theory
+
+related_functors: []
+
+satisfied_properties:
+  - property: fully faithful
+    proof: This is trivial.
+
+  - property: essentially surjective
+    proof: The object $0$ is in the image, and the other object $1$ is isomorphic to $0$.
+
+unsatisfied_properties:
+  - property: isomorphism
+    proof: The object $1$ has no preimage.

databases/catdat/scripts/expected-data/forget_vector.json

@@ -21,6 +21,7 @@
 	"full on isomorphisms": false,
 	"pseudomonic": false,
 	"dominant": false,
+	"isomorphism": false,
 
 	"cofinitary": true,
 	"conservative": true,

databases/catdat/scripts/expected-data/id_Set.json

@@ -38,5 +38,6 @@
 	"coreflector": true,
 	"full on isomorphisms": true,
 	"pseudomonic": true,
-	"dominant": true
+	"dominant": true,
+	"isomorphism": true
 }