From 7eb0eb297164a16bb1eb1c9bbe2d757ca2ef3214 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 2 Jul 2026 11:17:39 +0200 Subject: [PATCH 1/3] add isomorphism of categories --- .../data/functor-implications/equivalences.yaml | 8 ++++++++ .../catdat/data/functor-properties/equivalence.yaml | 6 +++--- .../catdat/data/functor-properties/isomorphism.yaml | 11 +++++++++++ databases/catdat/data/functors/id_Set.yaml | 2 +- .../catdat/scripts/expected-data/forget_vector.json | 1 + databases/catdat/scripts/expected-data/id_Set.json | 3 ++- 6 files changed, 26 insertions(+), 5 deletions(-) create mode 100644 databases/catdat/data/functor-properties/isomorphism.yaml diff --git a/databases/catdat/data/functor-implications/equivalences.yaml b/databases/catdat/data/functor-implications/equivalences.yaml index 14c005250..325dbca91 100644 --- a/databases/catdat/data/functor-implications/equivalences.yaml +++ b/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 diff --git a/databases/catdat/data/functor-properties/equivalence.yaml b/databases/catdat/data/functor-properties/equivalence.yaml index ea2f45649..d113e78c0 100644 --- a/databases/catdat/data/functor-properties/equivalence.yaml +++ b/databases/catdat/data/functor-properties/equivalence.yaml @@ -1,6 +1,6 @@ id: equivalence relation: is an -description: A functor is an equivalence if it has a pseudo-inverse functor. +description: 'A functor $F : \C \to \D$ is an equivalence 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 isomorphic to the identities.' nlab_link: https://ncatlab.org/nlab/show/equivalence+of+categories invariant_under_equivalences: true dual_property: equivalence @@ -8,9 +8,9 @@ related_properties: - full - faithful - essentially surjective - - continuous - - cocontinuous + - right-invertible - left-invertible + - isomorphism tags: - invertibility diff --git a/databases/catdat/data/functor-properties/isomorphism.yaml b/databases/catdat/data/functor-properties/isomorphism.yaml new file mode 100644 index 000000000..cb9d9c1f7 --- /dev/null +++ b/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 isomorphism 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 equal 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 diff --git a/databases/catdat/data/functors/id_Set.yaml b/databases/catdat/data/functors/id_Set.yaml index da4369726..43fc957aa 100644 --- a/databases/catdat/data/functors/id_Set.yaml +++ b/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 diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json index 6bc519cb8..863f1eb49 100644 --- a/databases/catdat/scripts/expected-data/forget_vector.json +++ b/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, diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json index af4099f50..3a5032ffd 100644 --- a/databases/catdat/scripts/expected-data/id_Set.json +++ b/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 } From 38cd6e0b750be06ddb2182cf549174e265852782 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 2 Jul 2026 11:27:21 +0200 Subject: [PATCH 2/3] add opposite monoid and opposite category --- .../data/functors/opposite_category.yaml | 20 +++++++++++++++++++ .../catdat/data/functors/opposite_monoid.yaml | 20 +++++++++++++++++++ 2 files changed, 40 insertions(+) create mode 100644 databases/catdat/data/functors/opposite_category.yaml create mode 100644 databases/catdat/data/functors/opposite_monoid.yaml diff --git a/databases/catdat/data/functors/opposite_category.yaml b/databases/catdat/data/functors/opposite_category.yaml new file mode 100644 index 000000000..324e70774 --- /dev/null +++ b/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: [] diff --git a/databases/catdat/data/functors/opposite_monoid.yaml b/databases/catdat/data/functors/opposite_monoid.yaml new file mode 100644 index 000000000..ee82a7238 --- /dev/null +++ b/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: [] From f3c92e9289d90d7e0b70e20cd3781d419b85349e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 2 Jul 2026 11:55:59 +0200 Subject: [PATCH 3/3] add walking isomorphism object inclusion This is the simplest example of an equivalence of categories which is not an isomorphism. --- .../walking_isomorphism_object_inclusion.yaml | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 databases/catdat/data/functors/walking_isomorphism_object_inclusion.yaml diff --git a/databases/catdat/data/functors/walking_isomorphism_object_inclusion.yaml b/databases/catdat/data/functors/walking_isomorphism_object_inclusion.yaml new file mode 100644 index 000000000..35418ccdb --- /dev/null +++ b/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.