Unification of categories and functors

DATABASE.md

@@ -23,7 +23,7 @@ But they are abstracted away by using the view `category_implications_view`.
 
 Further tables are:
 
-- `tags`
+- `category_tags`
 - `category_tag_assignments`
 - `related_categories`
 - `relations`

databases/catdat/data/config.yaml

@@ -1,4 +1,4 @@
-tags:
+shared_tags:
   - algebra
   - algebraic geometry
   - analysis
@@ -8,10 +8,14 @@ tags:
   - order theory
   - set theory
   - topology
+
+category_tags:
   - finite
   - thin
   - single object
 
+functor_tags: []
+
 relations:
   - relation: is
     negation: is not

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

@@ -4,3 +4,9 @@ description: A functor is <i>cocontinuous</i> when it preserves all small colimi
 nlab_link: https://ncatlab.org/nlab/show/cocontinuous+functor
 invariant_under_equivalences: true
 dual_property: continuous
+related_properties:
+  - coproduct-preserving
+  - right exact
+  - left adjoint
+  - coequalizer-preserving
+  - finitary

databases/catdat/data/functor-properties/coequalizer-preserving.yaml

@@ -4,3 +4,6 @@ description: 'A functor $F$ <i>preserves coequalizers</i> when for every paralle
 nlab_link: null
 invariant_under_equivalences: true
 dual_property: equalizer-preserving
+related_properties:
+  - cocontinuous
+  - right exact

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

@@ -4,3 +4,5 @@ description: A functor is <i>cofinitary</i> when it preserves cofiltered limits.
 nlab_link: null
 invariant_under_equivalences: true
 dual_property: finitary
+related_properties:
+  - continuous

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

@@ -4,3 +4,6 @@ description: 'A functor $F : \C \to \D$ is <i>comonadic</i> when there is a como
 nlab_link: https://ncatlab.org/nlab/show/comonadic+functor
 invariant_under_equivalences: true
 dual_property: monadic
+related_properties:
+  - left adjoint
+  - faithful

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

@@ -4,3 +4,5 @@ description: 'A functor $F : \C \to \D$ is <i>conservative</i> when it is isomor
 nlab_link: https://ncatlab.org/nlab/show/conservative+functor
 invariant_under_equivalences: true
 dual_property: conservative
+related_properties:
+  - equivalence

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

@@ -4,3 +4,9 @@ description: A functor is <i>continuous</i> when it preserves all small limits.
 nlab_link: https://ncatlab.org/nlab/show/continuous+functor
 invariant_under_equivalences: true
 dual_property: cocontinuous
+related_properties:
+  - product-preserving
+  - left exact
+  - right adjoint
+  - equalizer-preserving
+  - cofinitary

databases/catdat/data/functor-properties/coproduct-preserving.yaml

@@ -4,3 +4,7 @@ description: A functor $F$ <i>preserves coproducts</i> when for every family of
 nlab_link: null
 invariant_under_equivalences: true
 dual_property: product-preserving
+related_properties:
+  - finite-coproduct-preserving
+  - initial-object-preserving
+  - cocontinuous

databases/catdat/data/functor-properties/epimorphism-preserving.yaml

@@ -6,3 +6,5 @@ description: |-
 nlab_link: https://ncatlab.org/nlab/show/epimorphism
 invariant_under_equivalences: true
 dual_property: monomorphism-preserving
+related_properties:
+  - right exact

databases/catdat/data/functor-properties/equalizer-preserving.yaml

@@ -4,3 +4,6 @@ description: 'A functor $F$ <i>preserves equalizers</i> when for every parallel
 nlab_link: null
 invariant_under_equivalences: true
 dual_property: coequalizer-preserving
+related_properties:
+  - continuous
+  - left exact

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

@@ -4,3 +4,9 @@ description: A functor is an <i>equivalence</i> if it has a pseudo-inverse funct
 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

databases/catdat/data/functor-properties/essentially surjective.yaml

@@ -4,3 +4,5 @@ description: 'A functor $F : \C \to \D$ is <i>essentially surjective</i> when ev
 nlab_link: https://ncatlab.org/nlab/show/essentially+surjective+functor
 invariant_under_equivalences: true
 dual_property: essentially surjective
+related_properties:
+  - equivalence

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

@@ -4,3 +4,8 @@ description: A functor is <i>exact</i> when it is left exact and right exact.
 nlab_link: https://ncatlab.org/nlab/show/exact+functor
 invariant_under_equivalences: true
 dual_property: exact
+related_properties:
+  - left exact
+  - right exact
+  - continuous
+  - cocontinuous

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

@@ -4,3 +4,6 @@ description: 'A functor is <i>faithful</i> when it is injective on Hom-sets: If
 nlab_link: https://ncatlab.org/nlab/show/faithful+functor
 invariant_under_equivalences: true
 dual_property: faithful
+related_properties:
+  - equivalence
+  - full

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

@@ -4,3 +4,5 @@ description: A functor is <i>finitary</i> when it preserves filtered colimits.
 nlab_link: https://ncatlab.org/nlab/show/finitary+functor
 invariant_under_equivalences: true
 dual_property: cofinitary
+related_properties:
+  - cocontinuous

databases/catdat/data/functor-properties/finite-coproduct-preserving.yaml

@@ -4,3 +4,7 @@ description: A functor $F$ <i>preserves finite coproducts</i> when for every fam
 nlab_link: null
 invariant_under_equivalences: true
 dual_property: finite-product-preserving
+related_properties:
+  - coproduct-preserving
+  - initial-object-preserving
+  - cocontinuous

databases/catdat/data/functor-properties/finite-product-preserving.yaml

@@ -4,3 +4,7 @@ description: A functor $F$ <i>preserves finite products</i> when for every finit
 nlab_link: null
 invariant_under_equivalences: true
 dual_property: finite-coproduct-preserving
+related_properties:
+  - product-preserving
+  - terminal-object-preserving
+  - continuous

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

@@ -4,3 +4,6 @@ description: 'A functor is <i>full</i> when it is surjective on Hom-sets: Every
 nlab_link: https://ncatlab.org/nlab/show/full+functor
 invariant_under_equivalences: true
 dual_property: full
+related_properties:
+  - equivalence
+  - faithful

databases/catdat/data/functor-properties/initial-object-preserving.yaml

@@ -4,3 +4,6 @@ description: A functor $F$ <i>preserves initial objects</i> when it maps every i
 nlab_link: null
 invariant_under_equivalences: true
 dual_property: terminal-object-preserving
+related_properties:
+  - finite-coproduct-preserving
+  - cocontinuous

databases/catdat/data/functor-properties/left adjoint.yaml

@@ -4,3 +4,6 @@ description: 'A functor $F : \C \to \D$ is a <i>left adjoint</i> when there is a
 nlab_link: https://ncatlab.org/nlab/show/left+adjoint
 invariant_under_equivalences: true
 dual_property: right adjoint
+related_properties:
+  - cocontinuous
+  - comonadic

databases/catdat/data/functor-properties/left exact.yaml

@@ -4,3 +4,6 @@ description: A functor is <i>left exact</i> when it preserves finite limits.
 nlab_link: https://ncatlab.org/nlab/show/exact+functor
 invariant_under_equivalences: true
 dual_property: right exact
+related_properties:
+  - exact
+  - continuous

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

@@ -4,3 +4,6 @@ description: 'A functor $F : \C \to \D$ is <i>monadic</i> when there is a monad
 nlab_link: https://ncatlab.org/nlab/show/monadic+functor
 invariant_under_equivalences: true
 dual_property: comonadic
+related_properties:
+  - right adjoint
+  - faithful

databases/catdat/data/functor-properties/monomorphism-preserving.yaml

@@ -6,3 +6,5 @@ description: |-
 nlab_link: https://ncatlab.org/nlab/show/monomorphism
 invariant_under_equivalences: true
 dual_property: epimorphism-preserving
+related_properties:
+  - left exact

databases/catdat/data/functor-properties/product-preserving.yaml

@@ -4,6 +4,10 @@ description: A functor $F$ <i>preserves products</i> when for every family of ob
 nlab_link: null
 invariant_under_equivalences: true
 dual_property: coproduct-preserving
+related_properties:
+  - finite-product-preserving
+  - terminal-object-preserving
+  - continuous
 
 # Here is why we do not call this property "preserves products":
 # Either we name the property "preserves products" and choose the

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

@@ -4,3 +4,5 @@ description: 'A functor $F : \C \to \D$ is <i>representable</i> if $\C$ is local
 nlab_link: https://ncatlab.org/nlab/show/representable+functor
 invariant_under_equivalences: true
 dual_property: null
+related_properties:
+  - continuous

databases/catdat/data/functor-properties/right adjoint.yaml

@@ -4,3 +4,6 @@ description: 'A functor $F : \C \to \D$ is a <i>right adjoint</i> when there is
 nlab_link: https://ncatlab.org/nlab/show/right+adjoint
 invariant_under_equivalences: true
 dual_property: left adjoint
+related_properties:
+  - continuous
+  - monadic

databases/catdat/data/functor-properties/right exact.yaml

@@ -4,3 +4,6 @@ description: A functor is <i>right exact</i> when it preserves finite colimits.
 nlab_link: https://ncatlab.org/nlab/show/exact+functor
 invariant_under_equivalences: true
 dual_property: left exact
+related_properties:
+  - exact
+  - cocontinuous

databases/catdat/data/functor-properties/terminal-object-preserving.yaml

@@ -4,3 +4,6 @@ description: A functor $F$ <i>preserves terminal objects</i> when it maps every
 nlab_link: null
 invariant_under_equivalences: true
 dual_property: initial-object-preserving
+related_properties:
+  - finite-product-preserving
+  - continuous

databases/catdat/data/functors/abelianization.yaml

@@ -1,10 +1,16 @@
 id: abelianization
 name: abelianization functor for groups
+notation: $(-)^{\ab}$
 source: Grp
 target: Ab
 description: This functor maps a group $G$ to its abelianization $G^{\ab} \coloneqq G/[G,G]$.
 nlab_link: https://ncatlab.org/nlab/show/abelianization
 
+tags:
+  - algebra
+
+related_functors: []
+
 satisfied_properties:
   - property: essentially surjective
     reason: For abelian groups $G$ we have $G \cong G^{\ab}$.

databases/catdat/data/functors/forget_vector.yaml

@@ -1,10 +1,16 @@
 id: forget_vector
 name: forgetful functor for vector spaces
+notation: $U_{\Vect}$
 source: Vect
 target: Set
-description: This functor $U$ maps a vector space $V$ (over a fixed field $K$) to its underlying set $U(V)$.
+description: This functor maps a vector space $V$ (over a fixed field $K$) to its underlying set $U_{\Vect}(V)$.
 nlab_link: https://ncatlab.org/nlab/show/forgetful+functor
 
+tags:
+  - algebra
+
+related_functors: []
+
 satisfied_properties:
   - property: conservative
     reason: It is standard that the inverse of a bijective linear map is also linear.

databases/catdat/data/functors/free_group.yaml

@@ -1,10 +1,16 @@
 id: free_group
 name: free group functor
+notation: $F_{\Grp}$
 source: Set
 target: Grp
-description: This functor maps a set $X$ to the free group $F(X)$ on that set.
+description: This functor maps a set $X$ to the free group $F_{\Grp}(X)$ on that set. We abbreviate $F \coloneqq F_{\Grp}$.
 nlab_link: https://ncatlab.org/nlab/show/free+functor
 
+tags:
+  - algebra
+
+related_functors: []
+
 satisfied_properties:
   - property: conservative
     reason: 'Let $f : X \to Y$ be a map of sets such that $F(f) : F(X) \to F(Y)$ is an isomorphism of groups. We know that $F$ is faithful, so that it reflects monomorphisms. Thus, $f$ is injective. Choose a complement $U \subseteq Y$ of $f(X) \subseteq Y$. Then $F(X) \to F(Y) = F(X) \sqcup F(U)$ is an isomorphism. This implies $F(U)=1$ and hence $U = \varnothing$.'

databases/catdat/data/functors/id_Set.yaml

@@ -1,10 +1,16 @@
 id: id_Set
 name: identity functor on the category of sets
+notation: $\id_{\Set}$
 source: Set
 target: Set
 description: Every category $\C$ has an identity functor $\id_{\C}$. Here, we specify that it is for the category of sets.
 nlab_link: https://ncatlab.org/nlab/show/identity+functor
 
+tags:
+  - set theory
+
+related_functors: []
+
 satisfied_properties:
   - property: equivalence
     reason: This is trivial.

databases/catdat/data/functors/power_set_contravariant.yaml

@@ -1,10 +1,17 @@
 id: power_set_contravariant
 name: contravariant power set functor
+notation: $\Hom(-,2)$
 source: Set_op
 target: Set
-description: 'This functor maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced preimage operator $f^* : P(Y) \to P(X)$.'
+description: 'This functor maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced preimage operator $f^* : P(Y) \to P(X)$. It is isomorphic to the representable functor $\Hom(-,2) : \Set^{\op} \to \Set$.'
 nlab_link: https://ncatlab.org/nlab/show/power+set
 
+tags:
+  - set theory
+
+related_functors:
+  - power_set_covariant
+
 satisfied_properties:
   - property: epimorphism-preserving
     reason: 'If $f : X \to Y$ is injective, then $f^* : P(Y) \to P(X)$ is surjective, since for all $A \subseteq X$ we have $A = f^*(f_*(A))$.'

databases/catdat/data/functors/power_set_covariant.yaml

@@ -1,10 +1,17 @@
 id: power_set_covariant
 name: covariant power set functor
+notation: $P$
 source: Set
 target: Set
 description: 'This functor maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced image operator $f_* : P(X) \to P(Y)$.'
 nlab_link: https://ncatlab.org/nlab/show/power+set
 
+tags:
+  - set theory
+
+related_functors:
+  - power_set_contravariant
+
 satisfied_properties:
   - property: conservative
     reason: 'Assume that $f : X \to Y$ is a map such that $f_* : P(X) \to P(Y)$ is an isomorphism. There is some $A \subseteq X$ with $Y = f_*(A)$, this proves that $f$ is surjective. It is also injective: If $x,y \in X$ satisfy $f(x) = f(y)$, then $f_*(\{x\}) = f_*(\{y\})$, and hence $\{x\} = \{y\}$, i.e. $x = y$.'

databases/catdat/schema/001_tags.sql

@@ -0,0 +1,9 @@
+CREATE TABLE category_tags (
+    id INTEGER PRIMARY KEY,
+    tag TEXT NOT NULL UNIQUE
+);
+
+CREATE TABLE functor_tags (
+    id INTEGER PRIMARY KEY,
+    tag TEXT NOT NULL UNIQUE
+);

databases/catdat/schema/001_categories.sql → databases/catdat/schema/003_categories.sql

@@ -11,6 +11,14 @@ CREATE TABLE categories (
 
 CREATE UNIQUE INDEX categories_lower_id_unique ON categories (lower(id));
 
+CREATE TABLE category_tag_assignments (
+    category_id TEXT NOT NULL,
+    tag TEXT NOT NULL,
+    PRIMARY KEY (category_id, tag),
+    FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE,
+    FOREIGN KEY (tag) REFERENCES category_tags (tag) ON DELETE CASCADE
+);
+
 CREATE TABLE related_categories (
     category_id TEXT NOT NULL,
     related_category_id TEXT NOT NULL,
@@ -26,4 +34,6 @@ CREATE TABLE category_comments (
     FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE
 );
 
-CREATE INDEX idx_category_comments ON category_comments (category_id);
+CREATE INDEX idx_category_comments ON category_comments (category_id);
+
+