diff --git a/databases/catdat/data/functor-implications/equivalences.yaml b/databases/catdat/data/functor-implications/equivalences.yaml index 14c00525..325dbca9 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 ea2f4564..d113e78c 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 00000000..cb9d9c1f --- /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 da436972..43fc957a 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/data/functors/opposite_category.yaml b/databases/catdat/data/functors/opposite_category.yaml new file mode 100644 index 00000000..324e7077 --- /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 00000000..ee82a723 --- /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: [] 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 00000000..35418ccd --- /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. diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json index 6bc519cb..863f1eb4 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 af4099f5..3a5032ff 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 }