From 6c235bcd707dec9e41adfa37dc83895255a8892a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 20 Sep 2026 00:43:16 +0200 Subject: [PATCH 1/5] create valibot schemas --- database/scripts/utils/seed.schemas.ts | 107 +++++++++++++++++++++++++ package.json | 1 + pnpm-lock.yaml | 15 ++++ 3 files changed, 123 insertions(+) create mode 100644 database/scripts/utils/seed.schemas.ts diff --git a/database/scripts/utils/seed.schemas.ts b/database/scripts/utils/seed.schemas.ts new file mode 100644 index 00000000..e7933200 --- /dev/null +++ b/database/scripts/utils/seed.schemas.ts @@ -0,0 +1,107 @@ +import * as v from 'valibot' + +export const config_yaml_schema = v.object({ + structure_tags: v.array(v.string()), + category_tags: v.array(v.string()), + functor_tags: v.array(v.string()), + morphism_tags: v.array(v.string()), + symmetric_monoidal_category_tags: v.array(v.string()), + category_property_tags: v.array(v.string()), + functor_property_tags: v.array(v.string()), + morphism_property_tags: v.array(v.string()), + symmetric_monoidal_category_property_tags: v.array(v.string()), + relations: v.array( + v.object({ + relation: v.string(), + negation: v.string(), + conditional: v.string() + }) + ), + special_objects: v.array( + v.object({ + kind: v.string(), + dual: v.string() + }) + ), + special_morphisms: v.array( + v.object({ + kind: v.string(), + dual: v.string() + }) + ) +}) + +export const special_morphism_rule_yaml_schema = v.array( + v.object({ + property: v.string(), + kind: v.string(), + description: v.string(), + proof: v.string() + }) +) + +export const property_entry_schema = v.object({ + property: v.string(), + proof: v.string(), + check_redundancy: v.optional(v.boolean()), + label: v.optional(v.string()), + references: v.optional(v.array(v.string())) +}) + +export const structure_yaml_schema = v.object({ + id: v.string(), + name: v.string(), + notation: v.string(), + description: v.string(), + nlab_link: v.nullable(v.string()), + tags: v.array(v.string()), + related: v.array(v.string()), + dual: v.optional(v.string()), + parent: v.optional(v.string()), + associated: v.optional(v.record(v.string(), v.nullable(v.string()))), + satisfied_properties: v.array(property_entry_schema), + unsatisfied_properties: v.array(property_entry_schema), + undecidable_properties: v.optional(v.array(property_entry_schema)), + comments: v.optional(v.array(v.string())) +}) + +export const category_yaml_schema = v.object({ + id: v.string(), + objects: v.string(), + morphisms: v.string(), + special_objects: v.record( + v.string(), + v.object({ + description: v.string() + }) + ), + special_morphisms: v.record( + v.string(), + v.object({ + description: v.string(), + proof: v.string() + }) + ) +}) + +export const property_yaml_schema = v.object({ + id: v.string(), + relation: v.string(), + description: v.string(), + nlab_link: v.nullable(v.string()), + dual: v.nullable(v.string()), + invariant_under_equivalences: v.boolean(), + related: v.array(v.string()), + tags: v.array(v.string()) +}) + +export const implications_yaml_schema = v.array( + v.object({ + id: v.string(), + assumptions: v.array(v.string()), + conclusions: v.array(v.string()), + associated_assumptions: v.optional(v.record(v.string(), v.array(v.string()))), + proof: v.string(), + is_equivalence: v.optional(v.boolean()) + }) +) diff --git a/package.json b/package.json index 7938ba10..5b9f3594 100644 --- a/package.json +++ b/package.json @@ -62,6 +62,7 @@ "better-sqlite3": "^12.11.1", "katex": "^0.17.0", "svelte-fa": "^4.0.4", + "valibot": "^1.5.0", "yaml": "^2.8.4" } } diff --git a/pnpm-lock.yaml b/pnpm-lock.yaml index c09e81b3..ee324db5 100644 --- a/pnpm-lock.yaml +++ b/pnpm-lock.yaml @@ -26,6 +26,9 @@ importers: svelte-fa: specifier: ^4.0.4 version: 4.0.4(svelte@5.55.7) + valibot: + specifier: ^1.5.0 + version: 1.5.0(typescript@5.9.3) yaml: specifier: ^2.8.4 version: 2.8.4 @@ -1481,6 +1484,14 @@ packages: util-deprecate@1.0.2: resolution: {integrity: sha512-EPD5q1uXyFxJpCrLnCc1nHnq3gOa6DZBocAIiI2TaSCA7VCJ1UJDMagCzIkXNsUYfD1daK//LTEQ8xiIbrHtcw==} + valibot@1.5.0: + resolution: {integrity: sha512-nil6AkP2TChWL43Z5uJ6GTxX01CUA+g8LWUM+N/rB9NBbkUMaUsi9PUNzlUPgoKASgmx9f7eGOYpJ04/fSa6FQ==} + peerDependencies: + typescript: '>=5' + peerDependenciesMeta: + typescript: + optional: true + vite@8.0.13: resolution: {integrity: sha512-MFtjBYgzmSxmgA4RAfjIyXWpGe1oALnjgUTzzV7QLx/TKxCzjtMH6Fd9/eVK+5Fg1qNoz5VAwsmMs/NofrmJvw==} engines: {node: ^20.19.0 || >=22.12.0} @@ -2764,6 +2775,10 @@ snapshots: util-deprecate@1.0.2: {} + valibot@1.5.0(typescript@5.9.3): + optionalDependencies: + typescript: 5.9.3 + vite@8.0.13(@types/node@25.6.0)(esbuild@0.27.7)(tsx@4.21.0)(yaml@2.8.4): dependencies: lightningcss: 1.32.0 From 442f59282a8e7807ba16bd1b48c73be8c4871fbf Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 20 Sep 2026 00:43:58 +0200 Subject: [PATCH 2/5] group associated structures in YAML files --- database/data/functors/abelianization.yaml | 9 +++++---- database/data/functors/binary_coproduct_sets.yaml | 9 +++++---- database/data/functors/binary_product_sets.yaml | 9 +++++---- database/data/functors/brauer_group.yaml | 9 +++++---- database/data/functors/continuous_functions.yaml | 9 +++++---- database/data/functors/countable_copower_sets.yaml | 9 +++++---- database/data/functors/diagonal_sets.yaml | 9 +++++---- database/data/functors/discrete_topology.yaml | 9 +++++---- database/data/functors/doubling_sets.yaml | 9 +++++---- database/data/functors/empty_sets.yaml | 9 +++++---- database/data/functors/enveloping_group.yaml | 9 +++++---- database/data/functors/forget_abelian.yaml | 9 +++++---- database/data/functors/forget_addition.yaml | 9 +++++---- database/data/functors/forget_commutative.yaml | 9 +++++---- database/data/functors/forget_finite.yaml | 9 +++++---- database/data/functors/forget_finite_abelian_group.yaml | 9 +++++---- database/data/functors/forget_finite_group.yaml | 9 +++++---- database/data/functors/forget_group.yaml | 9 +++++---- database/data/functors/forget_group_pointed.yaml | 9 +++++---- database/data/functors/forget_hausdorff.yaml | 9 +++++---- database/data/functors/forget_inverses.yaml | 9 +++++---- database/data/functors/forget_ring.yaml | 9 +++++---- database/data/functors/forget_topology.yaml | 9 +++++---- database/data/functors/forget_torsion.yaml | 9 +++++---- database/data/functors/forget_torsion_free.yaml | 9 +++++---- database/data/functors/forget_vector.yaml | 9 +++++---- database/data/functors/free_group.yaml | 9 +++++---- database/data/functors/group_units.yaml | 9 +++++---- database/data/functors/id_Set.yaml | 9 +++++---- database/data/functors/inclusion_ordinals.yaml | 9 +++++---- database/data/functors/indiscrete_topology.yaml | 9 +++++---- database/data/functors/modulo-p.yaml | 9 +++++---- database/data/functors/monoid_ring.yaml | 9 +++++---- database/data/functors/morphism_endpoints_inclusion.yaml | 9 +++++---- database/data/functors/nerve.yaml | 9 +++++---- database/data/functors/opposite_category.yaml | 9 +++++---- database/data/functors/opposite_monoid.yaml | 9 +++++---- database/data/functors/p-torsion.yaml | 9 +++++---- database/data/functors/pi_0.yaml | 9 +++++---- database/data/functors/pi_1.yaml | 9 +++++---- database/data/functors/power_set_contravariant.yaml | 9 +++++---- database/data/functors/power_set_covariant.yaml | 9 +++++---- database/data/functors/rational_product.yaml | 9 +++++---- database/data/functors/ring_idempotents.yaml | 9 +++++---- database/data/functors/sequences_sets.yaml | 9 +++++---- database/data/functors/simple_group_probing.yaml | 9 +++++---- database/data/functors/span_endpoints_inclusion.yaml | 9 +++++---- database/data/functors/squaring_sets.yaml | 9 +++++---- database/data/functors/stone-cech-compactification.yaml | 9 +++++---- database/data/functors/torsion.yaml | 9 +++++---- database/data/functors/trivial_BG.yaml | 9 +++++---- database/data/functors/trivial_Idem.yaml | 9 +++++---- database/data/functors/trivial_groups.yaml | 9 +++++---- database/data/functors/trivial_sets.yaml | 9 +++++---- .../functors/walking_isomorphism_object_inclusion.yaml | 9 +++++---- .../data/functors/walking_morphism_representation.yaml | 9 +++++---- database/data/morphisms/A3-S3-embedding.yaml | 3 ++- database/data/morphisms/baer-specker-relations.yaml | 3 ++- database/data/morphisms/empty-map.yaml | 3 ++- database/data/morphisms/extremal-not-strong-example.yaml | 3 ++- database/data/morphisms/fork-handle.yaml | 3 ++- database/data/morphisms/id_G.yaml | 3 ++- database/data/morphisms/id_X.yaml | 3 ++- database/data/morphisms/inclusion_positive_numbers.yaml | 3 ++- database/data/morphisms/integer-rational-embedding.yaml | 3 ++- database/data/morphisms/multiply-2.yaml | 3 ++- database/data/morphisms/reduction-mod-p.yaml | 3 ++- database/data/morphisms/terminal-map.yaml | 3 ++- database/data/morphisms/universal-morphism.yaml | 3 ++- database/data/morphisms/universal-split-epi.yaml | 3 ++- .../data/morphisms/walking-idempotent-presentation.yaml | 3 ++- .../data/symmetric_monoidal_categories/1_tensor.yaml | 3 ++- .../data/symmetric_monoidal_categories/Ab_fg_tensor.yaml | 3 ++- .../data/symmetric_monoidal_categories/Ab_tensor.yaml | 3 ++- .../symmetric_monoidal_categories/Cat_cartesian.yaml | 3 ++- .../symmetric_monoidal_categories/FinVect_tensor.yaml | 3 ++- database/data/symmetric_monoidal_categories/N+.yaml | 3 ++- .../data/symmetric_monoidal_categories/R-Mod_tensor.yaml | 3 ++- .../symmetric_monoidal_categories/R-Mod_tensor_af.yaml | 3 ++- .../symmetric_monoidal_categories/R-Mod_tensor_naf.yaml | 3 ++- .../symmetric_monoidal_categories/Set_cartesian.yaml | 3 ++- .../symmetric_monoidal_categories/Set_cocartesian.yaml | 3 ++- .../symmetric_monoidal_categories/Top_cartesian.yaml | 3 ++- 83 files changed, 334 insertions(+), 251 deletions(-) diff --git a/database/data/functors/abelianization.yaml b/database/data/functors/abelianization.yaml index a20bd0f4..661a7b62 100644 --- a/database/data/functors/abelianization.yaml +++ b/database/data/functors/abelianization.yaml @@ -1,12 +1,13 @@ id: abelianization name: abelianization functor for groups notation: $(-)^{\ab}$ -domain: Grp -codomain: Ab +associated: + domain: Grp + codomain: Ab + left_adjoint: null + right_adjoint: forget_abelian description: This functor maps a group $G$ to its abelianization $G^{\ab} \coloneqq G/[G,G]$. nlab_link: https://ncatlab.org/nlab/show/abelianization -left_adjoint: null -right_adjoint: forget_abelian tags: - algebra diff --git a/database/data/functors/binary_coproduct_sets.yaml b/database/data/functors/binary_coproduct_sets.yaml index 05d01e84..9f0cad25 100644 --- a/database/data/functors/binary_coproduct_sets.yaml +++ b/database/data/functors/binary_coproduct_sets.yaml @@ -1,12 +1,13 @@ id: binary_coproduct_sets name: binary coproduct functor on sets notation: $+$ -domain: SetxSet -codomain: Set +associated: + domain: SetxSet + codomain: Set + left_adjoint: null + right_adjoint: diagonal_sets description: This functor maps a pair of sets $(X,Y)$ to their coproduct $X + Y$. It is an example of a right-invertible left adjoint functor which is not a reflector. nlab_link: null -left_adjoint: null -right_adjoint: diagonal_sets tags: - set theory diff --git a/database/data/functors/binary_product_sets.yaml b/database/data/functors/binary_product_sets.yaml index b4639bbe..6a4c70fd 100644 --- a/database/data/functors/binary_product_sets.yaml +++ b/database/data/functors/binary_product_sets.yaml @@ -1,12 +1,13 @@ id: binary_product_sets name: binary product functor on sets notation: $\times$ -domain: SetxSet -codomain: Set +associated: + domain: SetxSet + codomain: Set + left_adjoint: diagonal_sets + right_adjoint: null description: This functor maps a pair of sets $(X,Y)$ to their product $X \times Y$. It is an example of a right-invertible right adjoint functor which is not a coreflector. nlab_link: null -left_adjoint: diagonal_sets -right_adjoint: null tags: - set theory diff --git a/database/data/functors/brauer_group.yaml b/database/data/functors/brauer_group.yaml index f33d40bf..e85f83b2 100644 --- a/database/data/functors/brauer_group.yaml +++ b/database/data/functors/brauer_group.yaml @@ -1,12 +1,13 @@ id: brauer_group name: Brauer group functor notation: $\Br$ -domain: Fld -codomain: Ab +associated: + domain: Fld + codomain: Ab + left_adjoint: null + right_adjoint: null description: The Brauer group $\Br(K)$ of a field $K$ consists of equivalence classes of central simple algebras over $K$, where $A \sim B$ iff $A \otimes_K M_n(K) \cong B \otimes_K M_n(K)$ for some $n \geq 0$. The group structure is given by $[A] \cdot [B] \coloneqq [A \otimes_K B]$, $1 \coloneqq [K]$ and $[A]^{-1} \coloneqq [A^{\op}]$. A homomorphism $K \to L$ induces the homomorphism $\Br(K) \to \Br(L)$ defined by $[A] \mapsto [A \otimes_K L]$. nlab_link: https://ncatlab.org/nlab/show/Brauer+group -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/continuous_functions.yaml b/database/data/functors/continuous_functions.yaml index 75a0322d..52e95bb4 100644 --- a/database/data/functors/continuous_functions.yaml +++ b/database/data/functors/continuous_functions.yaml @@ -1,12 +1,13 @@ id: continuous_functions name: functor of continuous functions notation: $C$ -domain: Top_op -codomain: CAlg(R) # TODO: specify that R is IR +associated: + domain: Top_op + codomain: CAlg(R) # TODO: specify that R is IR + left_adjoint: null + right_adjoint: null description: 'This functor maps a topological space $X$ to the commutative $\IR$-algebra $C(X)$ of continuous functions $X \to \IR$. A continuous map $f : X \to Y$ is mapped to the algebra homomorphism $f^* : C(Y) \to C(X)$, $u \mapsto u \circ f$.' nlab_link: null -left_adjoint: null -right_adjoint: null tags: - topology diff --git a/database/data/functors/countable_copower_sets.yaml b/database/data/functors/countable_copower_sets.yaml index a75a9cda..1dacb2eb 100644 --- a/database/data/functors/countable_copower_sets.yaml +++ b/database/data/functors/countable_copower_sets.yaml @@ -1,12 +1,13 @@ id: countable_copower_sets name: countable copower functor on sets notation: $\IN \times (-)$ -domain: Set -codomain: Set +associated: + domain: Set + codomain: Set + left_adjoint: null + right_adjoint: sequences_sets description: This functor maps a set $X$ to the product $\IN \times X$, which can also be seen as the copower $\IN \otimes X = \coprod_{n \in \IN} X$. It is an example of a polynomial functor. nlab_link: null -left_adjoint: null -right_adjoint: sequences_sets tags: - set theory diff --git a/database/data/functors/diagonal_sets.yaml b/database/data/functors/diagonal_sets.yaml index 72fc8410..1f1abe36 100644 --- a/database/data/functors/diagonal_sets.yaml +++ b/database/data/functors/diagonal_sets.yaml @@ -1,12 +1,13 @@ id: diagonal_sets name: binary diagonal functor on the category of sets notation: $\Delta$ -domain: Set -codomain: SetxSet +associated: + domain: Set + codomain: SetxSet + left_adjoint: binary_coproduct_sets + right_adjoint: binary_product_sets description: 'Every category $\C$ has a (binary) diagonal functor $\Delta : \C \to \C^2$, $X \mapsto (X,X)$. Here, we specify that $\C$ is the category of sets.' nlab_link: https://ncatlab.org/nlab/show/diagonal+functor -left_adjoint: binary_coproduct_sets -right_adjoint: binary_product_sets tags: - set theory diff --git a/database/data/functors/discrete_topology.yaml b/database/data/functors/discrete_topology.yaml index 79a914b4..0d2f5185 100644 --- a/database/data/functors/discrete_topology.yaml +++ b/database/data/functors/discrete_topology.yaml @@ -1,12 +1,13 @@ id: discrete_topology name: discrete topology functor notation: $D$ -domain: Set -codomain: Top +associated: + domain: Set + codomain: Top + left_adjoint: null + right_adjoint: forget_topology description: This functor maps a set $X$ to the discrete topological space $D(X) \coloneqq (X, P(X))$ in which every subset is open. It is a typical example of a fully faithful functor that preserves finite but does not preserve infinite products. nlab_link: https://ncatlab.org/nlab/show/discrete+and+indiscrete+topology -left_adjoint: null -right_adjoint: forget_topology tags: - topology diff --git a/database/data/functors/doubling_sets.yaml b/database/data/functors/doubling_sets.yaml index 79e27eea..ef85820f 100644 --- a/database/data/functors/doubling_sets.yaml +++ b/database/data/functors/doubling_sets.yaml @@ -1,12 +1,13 @@ id: doubling_sets name: doubling functor on sets notation: $2(-)$ -domain: Set -codomain: Set +associated: + domain: Set + codomain: Set + left_adjoint: null + right_adjoint: squaring_sets description: This functor maps a set $X$ to its double $2 X \coloneqq X + X$. It is a simple example of a polynomial functor. nlab_link: null -left_adjoint: null -right_adjoint: squaring_sets tags: - set theory diff --git a/database/data/functors/empty_sets.yaml b/database/data/functors/empty_sets.yaml index 6a20120e..e8ab8354 100644 --- a/database/data/functors/empty_sets.yaml +++ b/database/data/functors/empty_sets.yaml @@ -1,12 +1,13 @@ id: empty_sets name: empty functor to the category of sets notation: $!_{\Set}$ -domain: '0' -codomain: Set +associated: + domain: '0' + codomain: Set + left_adjoint: null + right_adjoint: null description: 'Every category $\C$ has a unique functor $!_{\C} : \varnothing \to \C$. Here, we specify $\C = \Set$, but most of the properties do not depend on the choice of $\C$, as long as $\C$ is non-empty. This is the simplest example of a functor to $\Set$ that is both continuous and cocontinuous, but is neither representable nor a left or right adjoint.' nlab_link: null -left_adjoint: null -right_adjoint: null tags: - set theory diff --git a/database/data/functors/enveloping_group.yaml b/database/data/functors/enveloping_group.yaml index 260df85b..64c93e5e 100644 --- a/database/data/functors/enveloping_group.yaml +++ b/database/data/functors/enveloping_group.yaml @@ -1,12 +1,13 @@ id: enveloping_group name: enveloping group functor notation: $F_{\Mon,\Grp}$ -domain: Mon -codomain: Grp +associated: + domain: Mon + codomain: Grp + left_adjoint: null + right_adjoint: forget_inverses description: 'This functor maps a monoid $M$ to the group $F(M)$ that is equipped with a universal homomorphism $i_M : M \to F(M)$. It is called the (universal) enveloping group or the group completion of $M$; in the commutative case, it is known as the Grothendieck group of $M$. As a possible construction of $F(M)$, take the free group on generators $\underline{m}$ for $m \in M$ subject to the relations $\underline{1} = 1$ and $\underline{m \cdot n} = \underline{m} \cdot \underline{n}$.' nlab_link: https://ncatlab.org/nlab/show/free+functor -left_adjoint: null -right_adjoint: forget_inverses tags: - algebra diff --git a/database/data/functors/forget_abelian.yaml b/database/data/functors/forget_abelian.yaml index 77c3f8c3..4a136660 100644 --- a/database/data/functors/forget_abelian.yaml +++ b/database/data/functors/forget_abelian.yaml @@ -1,12 +1,13 @@ id: forget_abelian name: forgetful functor from abelian groups to groups notation: $U_{\Ab,\Grp}$ -domain: Ab -codomain: Grp +associated: + domain: Ab + codomain: Grp + left_adjoint: abelianization + right_adjoint: null description: This functor maps an abelian group to itself, considered merely as a group. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: abelianization -right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_addition.yaml b/database/data/functors/forget_addition.yaml index 778b44d9..e5411615 100644 --- a/database/data/functors/forget_addition.yaml +++ b/database/data/functors/forget_addition.yaml @@ -1,12 +1,13 @@ id: forget_addition name: forgetful functor from rings to monoids notation: $U_{\Ring,\Mon}$ -domain: Ring -codomain: Mon +associated: + domain: Ring + codomain: Mon + left_adjoint: monoid_ring + right_adjoint: null description: This functor maps a ring to its underlying multiplicative monoid, which as "forgotten" the addition of the ring. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: monoid_ring -right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_commutative.yaml b/database/data/functors/forget_commutative.yaml index fe2a2241..f928d69c 100644 --- a/database/data/functors/forget_commutative.yaml +++ b/database/data/functors/forget_commutative.yaml @@ -1,12 +1,13 @@ id: forget_commutative name: forgetful functor from commutative rings to rings notation: $U_{\CRing,\Ring}$ -domain: CRing -codomain: Ring +associated: + domain: CRing + codomain: Ring + left_adjoint: null # TODO: add the left adjoint to the database + right_adjoint: null description: This is the inclusion functor $\CRing \hookrightarrow \Ring$ that maps a commutative ring to itself, regarded merely as a ring. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: null # TODO: add the left adjoint to the database -right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_finite.yaml b/database/data/functors/forget_finite.yaml index cd6f87e3..e6a8c231 100644 --- a/database/data/functors/forget_finite.yaml +++ b/database/data/functors/forget_finite.yaml @@ -1,12 +1,13 @@ id: forget_finite name: forgetful functor from finite sets to sets notation: $U_{\FinSet,\Set}$ -domain: FinSet -codomain: Set +associated: + domain: FinSet + codomain: Set + left_adjoint: null + right_adjoint: null description: This functor is the inclusion functor $\FinSet \hookrightarrow \Set$ mapping a finite set to itself. It can also be regarded as a forgetful functor since it makes finite sets "forget" their finiteness. The functor is a basic example of a representable functor which is not a right adjoint. nlab_link: null -left_adjoint: null -right_adjoint: null tags: - set theory diff --git a/database/data/functors/forget_finite_abelian_group.yaml b/database/data/functors/forget_finite_abelian_group.yaml index 649147eb..ec34d751 100644 --- a/database/data/functors/forget_finite_abelian_group.yaml +++ b/database/data/functors/forget_finite_abelian_group.yaml @@ -1,12 +1,13 @@ id: forget_finite_abelian_group name: forgetful functor from finite abelian groups to abelian groups notation: $U_{\FinAb, \Ab}$ -domain: FinAb -codomain: Ab +associated: + domain: FinAb + codomain: Ab + left_adjoint: null + right_adjoint: null description: 'This is the inclusion functor $\FinAb \hookrightarrow \Ab$ that maps a finite abelian group to itself, regarded as an abelian group that has "forgotten" that it is finite. It provides an example of a fully faithful functor that is neither finitary nor cofinitary.' nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_finite_group.yaml b/database/data/functors/forget_finite_group.yaml index 55b23545..c2d8ad4f 100644 --- a/database/data/functors/forget_finite_group.yaml +++ b/database/data/functors/forget_finite_group.yaml @@ -1,12 +1,13 @@ id: forget_finite_group name: forgetful functor from finite groups to groups notation: $U_{\FinGrp, \Grp}$ -domain: FinGrp -codomain: Grp +associated: + domain: FinGrp + codomain: Grp + left_adjoint: null + right_adjoint: null description: 'This is the inclusion functor $\FinGrp \hookrightarrow \Grp$. It can also be viewed as a forgetful functor that forgets the property of being finite. Among other things, it provides an example of a fully faithful functor that is neither finitary nor cofinitary.' nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_group.yaml b/database/data/functors/forget_group.yaml index 50fead21..78c1885d 100644 --- a/database/data/functors/forget_group.yaml +++ b/database/data/functors/forget_group.yaml @@ -1,12 +1,13 @@ id: forget_group name: forgetful functor for groups notation: $U_{\Grp}$ -domain: Grp -codomain: Set +associated: + domain: Grp + codomain: Set + left_adjoint: free_group + right_adjoint: null description: This functor maps a group $G$ to its underlying set $U_{\Grp}(G)$. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: free_group -right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_group_pointed.yaml b/database/data/functors/forget_group_pointed.yaml index bb514185..f144cc84 100644 --- a/database/data/functors/forget_group_pointed.yaml +++ b/database/data/functors/forget_group_pointed.yaml @@ -1,12 +1,13 @@ id: forget_group_pointed name: forgetful functor from groups to pointed sets notation: $U_{\Grp,\Set_*}$ -domain: Grp -codomain: Set_* +associated: + domain: Grp + codomain: Set_* + left_adjoint: null + right_adjoint: null description: This functor maps a group $G$ to its underlying pointed set $U_{\Grp,\Set_*}(G)$, whose base point is the identity element of $G$. It is an example of an essentially surjective functor which is not right-invertible. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_hausdorff.yaml b/database/data/functors/forget_hausdorff.yaml index a4b70c6c..9d6ffa8c 100644 --- a/database/data/functors/forget_hausdorff.yaml +++ b/database/data/functors/forget_hausdorff.yaml @@ -1,12 +1,13 @@ id: forget_hausdorff name: forgetful functor from Hausdorff spaces to topological spaces notation: $U_{\Haus,\Top}$ -domain: Haus -codomain: Top +associated: + domain: Haus + codomain: Top + left_adjoint: null # TODO: add the Hausdorff reflection functor + right_adjoint: null description: This is the inclusion functor $\Haus \hookrightarrow \Top$ that maps a Hausdorff space to itself. It can also be viewed as a forgetful functor, since Hausdorff spaces "forget" that they are Hausdorff. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: null # TODO: add the Hausdorff reflection functor -right_adjoint: null tags: - topology diff --git a/database/data/functors/forget_inverses.yaml b/database/data/functors/forget_inverses.yaml index f25cfbc0..acca1d0f 100644 --- a/database/data/functors/forget_inverses.yaml +++ b/database/data/functors/forget_inverses.yaml @@ -1,12 +1,13 @@ id: forget_inverses name: forgetful functor from groups to monoids notation: $U_{\Grp,\Mon}$ -domain: Grp -codomain: Mon +associated: + domain: Grp + codomain: Mon + left_adjoint: enveloping_group + right_adjoint: group_units description: This functor maps a group to its underlying monoid. We view groups as structured sets $(X,m,e,i)$ (consisting of a set, a multiplication, a neutral element, and an inverse operation), and monoids as structured sets $(X,m,e)$. This forgetful functor precisely maps $(X,m,e,i)$ to $(X,m,e)$. From this point of view, it does not merely forget a property; it forgets an operation. This perspective is useful in contexts where the inverse operation is no longer reducible to a property, for example, the forgetful functor from topological groups to topological monoids. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: enveloping_group -right_adjoint: group_units tags: - algebra diff --git a/database/data/functors/forget_ring.yaml b/database/data/functors/forget_ring.yaml index 5199e2b2..d3e104b8 100644 --- a/database/data/functors/forget_ring.yaml +++ b/database/data/functors/forget_ring.yaml @@ -1,12 +1,13 @@ id: forget_ring name: forgetful functor for rings notation: $U_{\Ring}$ -domain: Ring -codomain: Set +associated: + domain: Ring + codomain: Set + left_adjoint: null + right_adjoint: null description: This functor maps a ring $R$ to its underlying set $U_{\Ring}(R)$. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_topology.yaml b/database/data/functors/forget_topology.yaml index d5e9eb59..0889b59b 100644 --- a/database/data/functors/forget_topology.yaml +++ b/database/data/functors/forget_topology.yaml @@ -1,12 +1,13 @@ id: forget_topology name: forgetful functor for topological spaces notation: $U_{\Top}$ -domain: Top -codomain: Set +associated: + domain: Top + codomain: Set + left_adjoint: discrete_topology + right_adjoint: indiscrete_topology description: This functor maps a topological space $X$ to its underlying set $U_{\Top}(X)$. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: discrete_topology -right_adjoint: indiscrete_topology tags: - topology diff --git a/database/data/functors/forget_torsion.yaml b/database/data/functors/forget_torsion.yaml index adbcfa04..cc966481 100644 --- a/database/data/functors/forget_torsion.yaml +++ b/database/data/functors/forget_torsion.yaml @@ -1,12 +1,13 @@ id: forget_torsion name: forgetful functor from torsion abelian groups to abelian groups notation: $U_{\TorsAb, \Ab}$ -domain: TorsAb -codomain: Ab +associated: + domain: TorsAb + codomain: Ab + left_adjoint: null # we only have the torsion functor Ab -> Ab in the database, not Ab -> TorsAb + right_adjoint: null description: 'This is the inclusion functor $\TorsAb \hookrightarrow \Ab$. It can also be viewed as a forgetful functor that forgets the property of being torsion. It is a typical example of a fully faithful functor that preserves finite products but does not preserve infinite products.' nlab_link: https://ncatlab.org/nlab/show/forgetful+functor -left_adjoint: null # we only have the torsion functor Ab -> Ab in the database, not Ab -> TorsAb -right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_torsion_free.yaml b/database/data/functors/forget_torsion_free.yaml index c5206687..ca667689 100644 --- a/database/data/functors/forget_torsion_free.yaml +++ b/database/data/functors/forget_torsion_free.yaml @@ -1,12 +1,13 @@ id: forget_torsion_free name: forgetful functor from torsion-free abelian groups to abelian groups notation: $U_{\TorsFreeAb, \Ab}$ -domain: TorsFreeAb -codomain: Ab +associated: + domain: TorsFreeAb + codomain: Ab + left_adjoint: null + right_adjoint: null description: 'This is the inclusion functor $\TorsFreeAb \hookrightarrow \Ab$. It can also be seen as a forgetful functor which forgets the property of being torsion-free. The functor provides a typical example of a fully faithful functor that does not preserve coequalizers and does not preserve epimorphisms.' nlab_link: null -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_vector.yaml b/database/data/functors/forget_vector.yaml index 6923a81d..5600dc83 100644 --- a/database/data/functors/forget_vector.yaml +++ b/database/data/functors/forget_vector.yaml @@ -1,12 +1,13 @@ id: forget_vector name: forgetful functor for vector spaces notation: $U_{\Vect}$ -domain: Vect -codomain: Set +associated: + domain: Vect + codomain: Set + left_adjoint: null + right_adjoint: null 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 -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/free_group.yaml b/database/data/functors/free_group.yaml index d08c7edb..baa31797 100644 --- a/database/data/functors/free_group.yaml +++ b/database/data/functors/free_group.yaml @@ -1,12 +1,13 @@ id: free_group name: free group functor notation: $F_{\Grp}$ -domain: Set -codomain: Grp +associated: + domain: Set + codomain: Grp + left_adjoint: null + right_adjoint: forget_group description: This functor maps a set $X$ to the free group $F_{\Grp}(X)$ on that set. In the proofs, we abbreviate $F \coloneqq F_{\Grp}$. nlab_link: https://ncatlab.org/nlab/show/free+functor -left_adjoint: null -right_adjoint: forget_group tags: - algebra diff --git a/database/data/functors/group_units.yaml b/database/data/functors/group_units.yaml index b8329db9..7f51275d 100644 --- a/database/data/functors/group_units.yaml +++ b/database/data/functors/group_units.yaml @@ -1,12 +1,13 @@ id: group_units name: group of units functor notation: $(-)^{\times}$ -domain: Mon -codomain: Grp +associated: + domain: Mon + codomain: Grp + left_adjoint: forget_inverses + right_adjoint: null description: This functor maps a monoid $M$ to its group of units $M^{\times}$, consisting of pairs $(a,b) \in M^2$ satisfying $ab=ba=1$. Equivalently, it takes the submonoid of invertible elements of $M$, equipped with the inverse operation. nlab_link: https://ncatlab.org/nlab/show/group+of+units -left_adjoint: forget_inverses -right_adjoint: null tags: - algebra diff --git a/database/data/functors/id_Set.yaml b/database/data/functors/id_Set.yaml index fd8a13b7..9ea5378e 100644 --- a/database/data/functors/id_Set.yaml +++ b/database/data/functors/id_Set.yaml @@ -1,12 +1,13 @@ id: id_Set name: identity functor on the category of sets notation: $\id_{\Set}$ -domain: Set -codomain: Set +associated: + domain: Set + codomain: Set + left_adjoint: id_Set + right_adjoint: id_Set description: 'Every category $\C$ has an identity functor $\id_{\C} : \C \to \C$. Here, we specify that $\C$ is the category of sets.' nlab_link: https://ncatlab.org/nlab/show/identity+functor -left_adjoint: id_Set -right_adjoint: id_Set tags: - set theory diff --git a/database/data/functors/inclusion_ordinals.yaml b/database/data/functors/inclusion_ordinals.yaml index ac3ceba4..8fa7194c 100644 --- a/database/data/functors/inclusion_ordinals.yaml +++ b/database/data/functors/inclusion_ordinals.yaml @@ -1,12 +1,13 @@ id: inclusion_ordinals name: inclusion functor from extended natural numbers to ordinal numbers notation: $\iota$ -domain: N_oo -codomain: On +associated: + domain: N_oo + codomain: On + left_adjoint: null + right_adjoint: null description: 'This is the inclusion map from the partially ordered set $(\IN \cup \{\infty\},\leq)$ (considered as a thin category as usual) into the partially ordered collection $(\OnColl,\leq)$, where we map $\infty$ to the ordinal $\omega$. It is an example of a functor that preserves binary products, but not terminal objects.' nlab_link: https://ncatlab.org/nlab/show/identity+functor -left_adjoint: null -right_adjoint: null tags: - set theory diff --git a/database/data/functors/indiscrete_topology.yaml b/database/data/functors/indiscrete_topology.yaml index ebda9939..8d0caa91 100644 --- a/database/data/functors/indiscrete_topology.yaml +++ b/database/data/functors/indiscrete_topology.yaml @@ -1,12 +1,13 @@ id: indiscrete_topology name: indiscrete topology functor notation: $I$ -domain: Set -codomain: Top +associated: + domain: Set + codomain: Top + left_adjoint: forget_topology + right_adjoint: null description: This functor maps a set $X$ to the indiscrete topological space $I(X) \coloneqq (X, \{\varnothing,X\})$ in which only the empty set and $X$ are open. nlab_link: https://ncatlab.org/nlab/show/discrete+and+indiscrete+topology -left_adjoint: forget_topology -right_adjoint: null tags: - topology diff --git a/database/data/functors/modulo-p.yaml b/database/data/functors/modulo-p.yaml index 7c6789a0..230f589c 100644 --- a/database/data/functors/modulo-p.yaml +++ b/database/data/functors/modulo-p.yaml @@ -1,12 +1,13 @@ id: modulo-p name: modulo p functor notation: $T^p$ -domain: Ab -codomain: Ab +associated: + domain: Ab + codomain: Ab + left_adjoint: null + right_adjoint: p-torsion description: This functor maps an abelian group $A$ to the quotient $T^p(A) \coloneqq A/pA$, where $p$ is a fixed prime number. This group can also be represented as $A \otimes \IZ/p$. nlab_link: null -left_adjoint: null -right_adjoint: p-torsion tags: - algebra diff --git a/database/data/functors/monoid_ring.yaml b/database/data/functors/monoid_ring.yaml index c3f7a35e..56da77e0 100644 --- a/database/data/functors/monoid_ring.yaml +++ b/database/data/functors/monoid_ring.yaml @@ -1,12 +1,13 @@ id: monoid_ring name: monoid ring functor notation: $\IZ[-]$ -domain: Mon -codomain: Ring +associated: + domain: Mon + codomain: Ring + left_adjoint: null + right_adjoint: forget_addition description: This functor maps a monoid $M$ to the monoid ring $\IZ[M]$, which consists of finite sums of elements in $M$. nlab_link: https://ncatlab.org/nlab/show/group+algebra -left_adjoint: null -right_adjoint: forget_addition tags: - algebra diff --git a/database/data/functors/morphism_endpoints_inclusion.yaml b/database/data/functors/morphism_endpoints_inclusion.yaml index 0de43353..2a1d1cdc 100644 --- a/database/data/functors/morphism_endpoints_inclusion.yaml +++ b/database/data/functors/morphism_endpoints_inclusion.yaml @@ -1,12 +1,13 @@ id: morphism_endpoints_inclusion name: morphism endpoints inclusion notation: $E$ -domain: '2' -codomain: walking_morphism +associated: + domain: '2' + codomain: walking_morphism + left_adjoint: null + right_adjoint: null description: This is the functor that embeds the discrete category $\{0,1\}$ into the walking morphism $\{0 \to 1\}$. It provides an example of a faithful functor that is full on isomorphisms but not full. nlab_link: null -left_adjoint: null -right_adjoint: null tags: - category theory diff --git a/database/data/functors/nerve.yaml b/database/data/functors/nerve.yaml index 9c13396d..b319ac6b 100644 --- a/database/data/functors/nerve.yaml +++ b/database/data/functors/nerve.yaml @@ -1,12 +1,13 @@ id: nerve name: nerve functor notation: $N$ -domain: Cat -codomain: sSet +associated: + domain: Cat + codomain: sSet + left_adjoint: null + right_adjoint: null description: The nerve of a small category $\C$ is the simplicial set $N(\C)$ whose $n$-simplices are chains of morphisms $X_0 \to \cdots \to X_n$. Among other things, it provides an example of a fully faithful functor that does not preserve regular epimorphisms. nlab_link: https://ncatlab.org/nlab/show/nerve -left_adjoint: null -right_adjoint: null tags: - category theory diff --git a/database/data/functors/opposite_category.yaml b/database/data/functors/opposite_category.yaml index 508c338f..f3447ebd 100644 --- a/database/data/functors/opposite_category.yaml +++ b/database/data/functors/opposite_category.yaml @@ -1,12 +1,13 @@ id: opposite_category name: opposite category functor notation: $(-)^{\op}$ -domain: Cat -codomain: Cat +associated: + domain: Cat + codomain: Cat + left_adjoint: opposite_category + right_adjoint: opposite_category 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 -right_adjoint: opposite_category tags: - category theory diff --git a/database/data/functors/opposite_monoid.yaml b/database/data/functors/opposite_monoid.yaml index 5b0ca136..baaef2b2 100644 --- a/database/data/functors/opposite_monoid.yaml +++ b/database/data/functors/opposite_monoid.yaml @@ -1,12 +1,13 @@ id: opposite_monoid name: opposite monoid functor notation: $(-)^{\op}$ -domain: Mon -codomain: Mon +associated: + domain: Mon + codomain: Mon + left_adjoint: opposite_monoid + right_adjoint: opposite_monoid 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 -right_adjoint: opposite_monoid tags: - algebra diff --git a/database/data/functors/p-torsion.yaml b/database/data/functors/p-torsion.yaml index 00e54523..b3f9757c 100644 --- a/database/data/functors/p-torsion.yaml +++ b/database/data/functors/p-torsion.yaml @@ -1,15 +1,16 @@ id: p-torsion name: p-torsion functor notation: $T_p$ -domain: Ab -codomain: Ab +associated: + domain: Ab + codomain: Ab + left_adjoint: modulo-p + right_adjoint: null description: >- This functor maps an abelian group $A$ to its $p$-torsion subgroup $$T_p(A) \coloneqq \{a \in A : pa = 0\},$$ where $p$ is a fixed prime number. This group can also be represented as $\HomInternal(\IZ/p,A)$. nlab_link: null -left_adjoint: modulo-p -right_adjoint: null tags: - algebra diff --git a/database/data/functors/pi_0.yaml b/database/data/functors/pi_0.yaml index 509a2aa1..fa1da95b 100644 --- a/database/data/functors/pi_0.yaml +++ b/database/data/functors/pi_0.yaml @@ -1,12 +1,13 @@ id: pi_0 name: path components functor notation: $\pi_0$ -domain: Top -codomain: Set +associated: + domain: Top + codomain: Set + left_adjoint: null + right_adjoint: null description: This functor maps a topological space $X$ to its set $\pi_0(X)$ of path components. Thus, $\pi_0(X) = U(X) / {\sim}$, where $U(X)$ is the underlying set and $x \sim y$ when there is a path from $x$ to $y$. nlab_link: https://ncatlab.org/nlab/show/connected+space -left_adjoint: null -right_adjoint: null tags: - topology diff --git a/database/data/functors/pi_1.yaml b/database/data/functors/pi_1.yaml index 33768be6..00f2803c 100644 --- a/database/data/functors/pi_1.yaml +++ b/database/data/functors/pi_1.yaml @@ -1,12 +1,13 @@ id: pi_1 name: fundamental group functor notation: $\pi_1$ -domain: Top_* -codomain: Grp +associated: + domain: Top_* + codomain: Grp + left_adjoint: null + right_adjoint: null description: The fundamental group $\pi_1(X,x_0)$ of a pointed topological space $(X,x_0)$ is the group of homotopy classes of loops at $x_0$. The group operation is concatenation of paths. For example, we have $\pi_1(S^1,1) \cong \IZ$ (see Hatcher's Algebraic Topology, Theorem 1.7). nlab_link: https://ncatlab.org/nlab/show/fundamental+group -left_adjoint: null -right_adjoint: null tags: - topology diff --git a/database/data/functors/power_set_contravariant.yaml b/database/data/functors/power_set_contravariant.yaml index f0f6599d..ef3ce22a 100644 --- a/database/data/functors/power_set_contravariant.yaml +++ b/database/data/functors/power_set_contravariant.yaml @@ -1,12 +1,13 @@ id: power_set_contravariant name: contravariant power set functor notation: $P_{\forall}$ -domain: Set_op -codomain: Set +associated: + domain: Set_op + codomain: Set + left_adjoint: null + right_adjoint: null description: 'This functor $P_{\forall}$ 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)$.' nlab_link: https://ncatlab.org/nlab/show/power+set -left_adjoint: null -right_adjoint: null tags: - set theory diff --git a/database/data/functors/power_set_covariant.yaml b/database/data/functors/power_set_covariant.yaml index 31f11461..f9cecbb3 100644 --- a/database/data/functors/power_set_covariant.yaml +++ b/database/data/functors/power_set_covariant.yaml @@ -1,12 +1,13 @@ id: power_set_covariant name: covariant power set functor notation: $P_{\exists}$ -domain: Set -codomain: Set +associated: + domain: Set + codomain: Set + left_adjoint: null + right_adjoint: null description: 'This functor $P_{\exists}$ 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 -left_adjoint: null -right_adjoint: null tags: - set theory diff --git a/database/data/functors/rational_product.yaml b/database/data/functors/rational_product.yaml index a0ab1bea..1d38acc6 100644 --- a/database/data/functors/rational_product.yaml +++ b/database/data/functors/rational_product.yaml @@ -1,12 +1,13 @@ id: rational_product name: rational product functor notation: $- \times \IQ$ -domain: Top -codomain: Top +associated: + domain: Top + codomain: Top + left_adjoint: null + right_adjoint: null description: This functor maps a topological space $X$ to the topological space $X \times \IQ$, where $\IQ \subseteq \IR$ carries the usual topology. It is a typical example of a functor that preserves epimorphisms but not regular epimorphisms. nlab_link: null -left_adjoint: null -right_adjoint: null tags: - topology diff --git a/database/data/functors/ring_idempotents.yaml b/database/data/functors/ring_idempotents.yaml index cd7bb6f6..7f8bd41b 100644 --- a/database/data/functors/ring_idempotents.yaml +++ b/database/data/functors/ring_idempotents.yaml @@ -1,12 +1,13 @@ id: ring_idempotents name: ring idempotents functor notation: $\Id$ -domain: Ring -codomain: Set +associated: + domain: Ring + codomain: Set + left_adjoint: null + right_adjoint: null description: This functor sends a ring $R$ to its set $\Id(R)$ of idempotent elements. A ring homomorphism $R \to S$ restricts to a map $\Id(R) \to \Id(S)$. Among other things, it provides an example of a representable functor that does not preserve regular epimorphisms. nlab_link: null -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/sequences_sets.yaml b/database/data/functors/sequences_sets.yaml index ec7363fd..1d730a06 100644 --- a/database/data/functors/sequences_sets.yaml +++ b/database/data/functors/sequences_sets.yaml @@ -1,12 +1,13 @@ id: sequences_sets name: sequences functor on sets notation: $(-)^{\IN}$ -domain: Set -codomain: Set +associated: + domain: Set + codomain: Set + left_adjoint: countable_copower_sets + right_adjoint: null description: This functor maps a set $X$ to the countable power $X^{\IN}$, i.e. the set of sequences in $X$. It is an example of a polynomial functor. It is also an example of a monadic functor for which the crude monadicity theorem does not apply. nlab_link: null -left_adjoint: countable_copower_sets -right_adjoint: null tags: - set theory diff --git a/database/data/functors/simple_group_probing.yaml b/database/data/functors/simple_group_probing.yaml index 7445a57c..9ebab8c9 100644 --- a/database/data/functors/simple_group_probing.yaml +++ b/database/data/functors/simple_group_probing.yaml @@ -1,8 +1,11 @@ id: simple_group_probing name: simple-group probing functor notation: $F$ -domain: Grp -codomain: Set +associated: + domain: Grp + codomain: Set + left_adjoint: null + right_adjoint: null description: >- This functor maps a group $G$ to the collection $$F(G) \coloneqq \textstyle\prod_{\kappa} \Hom(L_\kappa,G),$$ @@ -11,8 +14,6 @@ description: >- since only then $F(G)$ is actually a set, but the first definition makes it more apparent that $F$ is a functor. This is the canonical example of a continuous functor $\Grp \to \Set$ that is not representable, and not a right adjoint. nlab_link: null -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/span_endpoints_inclusion.yaml b/database/data/functors/span_endpoints_inclusion.yaml index 6a82fd1a..bf1c6aca 100644 --- a/database/data/functors/span_endpoints_inclusion.yaml +++ b/database/data/functors/span_endpoints_inclusion.yaml @@ -1,12 +1,13 @@ id: span_endpoints_inclusion name: span endpoints inclusion notation: $E$ -domain: '2' -codomain: walking_span +associated: + domain: '2' + codomain: walking_span + left_adjoint: null + right_adjoint: null description: This is the functor that embeds the discrete category $\{1,2\}$ into the walking span $\{1 \leftarrow 0 \rightarrow 2\}$. Among other things, it provides an example of a fully faithful functor which is not left-invertible. nlab_link: null -left_adjoint: null -right_adjoint: null tags: - category theory diff --git a/database/data/functors/squaring_sets.yaml b/database/data/functors/squaring_sets.yaml index 59b1a489..be8d9754 100644 --- a/database/data/functors/squaring_sets.yaml +++ b/database/data/functors/squaring_sets.yaml @@ -1,12 +1,13 @@ id: squaring_sets name: squaring functor on sets notation: $(-)^2$ -domain: Set -codomain: Set +associated: + domain: Set + codomain: Set + left_adjoint: doubling_sets + right_adjoint: null description: This functor maps a set $X$ to its square $X^2$. It is a simple example of a polynomial functor. nlab_link: null -left_adjoint: doubling_sets -right_adjoint: null tags: - set theory diff --git a/database/data/functors/stone-cech-compactification.yaml b/database/data/functors/stone-cech-compactification.yaml index 9b43842e..2fe8e397 100644 --- a/database/data/functors/stone-cech-compactification.yaml +++ b/database/data/functors/stone-cech-compactification.yaml @@ -1,15 +1,16 @@ id: stone-cech-compactification name: Stone-Čech compactification functor notation: $\beta$ -domain: Top -codomain: CompHaus +associated: + domain: Top + codomain: CompHaus + left_adjoint: null + right_adjoint: null description: >- This is the functor $\beta : \Top \to \CompHaus$ that is left adjoint to the inclusion functor $\CompHaus \hookrightarrow \Top$. There are various constructions (see Wikipedia), one being that $\beta(X)$ is the closure of the image of the canonical map $$X \to [0,1]^{\Hom(X,[0,1])}.$$ Among other things, this functor provides an example of a reflector that does not preserve binary products. nlab_link: https://ncatlab.org/nlab/show/Stone-%C4%8Cech+compactification -left_adjoint: null -right_adjoint: null tags: - topology diff --git a/database/data/functors/torsion.yaml b/database/data/functors/torsion.yaml index 3fab4b8f..521433f4 100644 --- a/database/data/functors/torsion.yaml +++ b/database/data/functors/torsion.yaml @@ -1,14 +1,15 @@ id: torsion name: torsion functor notation: $T$ -domain: Ab -codomain: Ab +associated: + domain: Ab + codomain: Ab + left_adjoint: null + right_adjoint: null description: >- This functor maps an abelian group $A$ to its torsion subgroup $$T(A) \coloneqq \{a \in A : \exists n \geq 1 \, (na = 0)\}.$$ nlab_link: https://ncatlab.org/nlab/show/torsion+subgroup -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/trivial_BG.yaml b/database/data/functors/trivial_BG.yaml index 51582aed..3fe01821 100644 --- a/database/data/functors/trivial_BG.yaml +++ b/database/data/functors/trivial_BG.yaml @@ -1,12 +1,13 @@ id: trivial_BG name: trivial functor from the delooping notation: $!_{BG}$ -domain: BG -codomain: '1' +associated: + domain: BG + codomain: '1' + left_adjoint: null + right_adjoint: null description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the delooping of a non-trivial group $G$. It is a basic example of a conservative functor which is not faithful.' nlab_link: null -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/trivial_Idem.yaml b/database/data/functors/trivial_Idem.yaml index 1c31eb27..2271458a 100644 --- a/database/data/functors/trivial_Idem.yaml +++ b/database/data/functors/trivial_Idem.yaml @@ -1,12 +1,13 @@ id: trivial_Idem name: trivial functor from the walking idempotent notation: $!_{\Idem}$ -domain: walking_idempotent -codomain: '1' +associated: + domain: walking_idempotent + codomain: '1' + left_adjoint: null + right_adjoint: null description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the walking idempotent. It is a basic example of an essentially injective functor which is not conservative.' nlab_link: null -left_adjoint: null -right_adjoint: null tags: - category theory diff --git a/database/data/functors/trivial_groups.yaml b/database/data/functors/trivial_groups.yaml index 0d40eb32..ef8ee8eb 100644 --- a/database/data/functors/trivial_groups.yaml +++ b/database/data/functors/trivial_groups.yaml @@ -1,12 +1,13 @@ id: trivial_groups name: trivial functor from the category of groups notation: $!_\Grp$ -domain: Grp -codomain: '1' +associated: + domain: Grp + codomain: '1' + left_adjoint: null + right_adjoint: null description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of groups. It is a basic example of a full functor which is not faithful.' nlab_link: null -left_adjoint: null -right_adjoint: null tags: - algebra diff --git a/database/data/functors/trivial_sets.yaml b/database/data/functors/trivial_sets.yaml index 86e3226d..766ff861 100644 --- a/database/data/functors/trivial_sets.yaml +++ b/database/data/functors/trivial_sets.yaml @@ -1,12 +1,13 @@ id: trivial_sets name: trivial functor from the category of sets notation: $!_\Set$ -domain: Set -codomain: '1' +associated: + domain: Set + codomain: '1' + left_adjoint: null + right_adjoint: null description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of sets.' nlab_link: null -left_adjoint: null -right_adjoint: null tags: - set theory diff --git a/database/data/functors/walking_isomorphism_object_inclusion.yaml b/database/data/functors/walking_isomorphism_object_inclusion.yaml index 2a504dbd..61ff6022 100644 --- a/database/data/functors/walking_isomorphism_object_inclusion.yaml +++ b/database/data/functors/walking_isomorphism_object_inclusion.yaml @@ -1,12 +1,13 @@ id: walking_isomorphism_object_inclusion name: walking isomorphism object inclusion notation: $\iota$ -domain: '1' -codomain: walking_isomorphism +associated: + domain: '1' + codomain: walking_isomorphism + left_adjoint: null + right_adjoint: null 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 -left_adjoint: null -right_adjoint: null tags: - category theory diff --git a/database/data/functors/walking_morphism_representation.yaml b/database/data/functors/walking_morphism_representation.yaml index 2691d2b3..2a6d2e58 100644 --- a/database/data/functors/walking_morphism_representation.yaml +++ b/database/data/functors/walking_morphism_representation.yaml @@ -1,12 +1,13 @@ id: walking_morphism_representation name: walking morphism representation notation: $F$ -domain: walking_morphism -codomain: Set +associated: + domain: walking_morphism + codomain: Set + left_adjoint: null + right_adjoint: null description: This is the functor $I \to \Set$ that maps the universal morphism $0 \to 1$ to the unique map $\varnothing \to \{*\}$ in $\Set$. It provides a very simple example of a functor that preserves coequalizers (and hence regular epimorphisms) but does not preserve epimorphisms. nlab_link: null -left_adjoint: null -right_adjoint: null tags: - category theory diff --git a/database/data/morphisms/A3-S3-embedding.yaml b/database/data/morphisms/A3-S3-embedding.yaml index 9e4fae35..57d80e00 100644 --- a/database/data/morphisms/A3-S3-embedding.yaml +++ b/database/data/morphisms/A3-S3-embedding.yaml @@ -1,7 +1,8 @@ id: A3-S3-embedding name: embedding of A3 into S3 notation: $i$ -category: Grp +associated: + category: Grp description: 'This is the embedding of groups $A_3 = \langle (1 \, 2 \, 3 ) \rangle \hookrightarrow S_3$. It serves as an example of a normal monomorphism which is not split.' nlab_link: https://ncatlab.org/nlab/show/alternating+group diff --git a/database/data/morphisms/baer-specker-relations.yaml b/database/data/morphisms/baer-specker-relations.yaml index e4e1f34a..be507c5d 100644 --- a/database/data/morphisms/baer-specker-relations.yaml +++ b/database/data/morphisms/baer-specker-relations.yaml @@ -1,7 +1,8 @@ id: baer-specker-relations name: Baer-Specker relations notation: $m$ -category: FreeAb +associated: + category: FreeAb description: 'Consider the Baer-Specker group $\IZ^\IN$ and choose a free abelian group $F$ with an epimorphism $\pi : F \to \IZ^\IN$ (for example, to make this example explicit, the free abelian group on the underlying set of $\IZ^\IN$). Let $K \subseteq F$ be its kernel (which is also free abelian). In this entry, we consider the inclusion $m : K \hookrightarrow F$. It provides an example of a strict monomorphism which is not regular.' nlab_link: null diff --git a/database/data/morphisms/empty-map.yaml b/database/data/morphisms/empty-map.yaml index fcbcfa14..e5cbc145 100644 --- a/database/data/morphisms/empty-map.yaml +++ b/database/data/morphisms/empty-map.yaml @@ -1,7 +1,8 @@ id: empty-map name: map from the empty set notation: $!$ -category: Set +associated: + category: Set description: 'For every set $X$ there is a unique map $! : \varnothing \hookrightarrow X$, the empty map. In this entry, we require that $X$ is non-empty.' nlab_link: https://ncatlab.org/nlab/show/empty+set diff --git a/database/data/morphisms/extremal-not-strong-example.yaml b/database/data/morphisms/extremal-not-strong-example.yaml index dbc90f8c..7e6724df 100644 --- a/database/data/morphisms/extremal-not-strong-example.yaml +++ b/database/data/morphisms/extremal-not-strong-example.yaml @@ -1,7 +1,8 @@ id: extremal-not-strong-example name: example of a non-strong extremal monomorphism notation: $m$ -category: forked_commutative_square +associated: + category: forked_commutative_square description: 'This is the morphism $m : C \to D$ from the forked commutative square, see details there. It provides an example of an extremal monomorphism which is not strong, and this is the only reason we have added this morphism and its category to the database.' nlab_link: null diff --git a/database/data/morphisms/fork-handle.yaml b/database/data/morphisms/fork-handle.yaml index 6a6c9694..c387e4d3 100644 --- a/database/data/morphisms/fork-handle.yaml +++ b/database/data/morphisms/fork-handle.yaml @@ -1,7 +1,8 @@ id: fork-handle name: handle of the universal fork notation: $i$ -category: walking_fork +associated: + category: walking_fork description: 'This is the morphism $i : 0 \to 1$ from the walking fork, see details there. It provides an example of a regular monomorphism which is neither split nor effective.' nlab_link: null diff --git a/database/data/morphisms/id_G.yaml b/database/data/morphisms/id_G.yaml index b3524a0e..e288b91e 100644 --- a/database/data/morphisms/id_G.yaml +++ b/database/data/morphisms/id_G.yaml @@ -1,7 +1,8 @@ id: id_G name: identity map of a group notation: $\id_G$ -category: Grp +associated: + category: Grp description: 'Every object of a category has an identity morphism. In this case, we take a non-trivial group $G$ and consider its identity morphism $\id_G : G \to G$ in $\Grp$.' nlab_link: https://ncatlab.org/nlab/show/identity+morphism diff --git a/database/data/morphisms/id_X.yaml b/database/data/morphisms/id_X.yaml index ca6b1f16..efb9245f 100644 --- a/database/data/morphisms/id_X.yaml +++ b/database/data/morphisms/id_X.yaml @@ -1,7 +1,8 @@ id: id_X name: identity map of a set notation: $\id_X$ -category: Set +associated: + category: Set description: 'Every object of a category has an identity morphism. In this case, we take a set $X$ and consider its identity morphism $\id_X : X \to X$ in $\Set$. To decide all of its properties, we assume that $X$ has at least two elements.' nlab_link: https://ncatlab.org/nlab/show/identity+morphism diff --git a/database/data/morphisms/inclusion_positive_numbers.yaml b/database/data/morphisms/inclusion_positive_numbers.yaml index 404313e9..4ade91cc 100644 --- a/database/data/morphisms/inclusion_positive_numbers.yaml +++ b/database/data/morphisms/inclusion_positive_numbers.yaml @@ -1,7 +1,8 @@ id: inclusion_positive_numbers name: inclusion of positive numbers notation: $i$ -category: Man +associated: + category: Man description: This is the inclusion map $(0,\infty) \to \IR$ inside the category of smooth manifolds. It provides an example of an extremal monomorphism that is not strong. nlab_link: null diff --git a/database/data/morphisms/integer-rational-embedding.yaml b/database/data/morphisms/integer-rational-embedding.yaml index 57e9527c..06fa0eac 100644 --- a/database/data/morphisms/integer-rational-embedding.yaml +++ b/database/data/morphisms/integer-rational-embedding.yaml @@ -1,7 +1,8 @@ id: integer-rational-embedding name: embedding of integer into rational numbers notation: $\iota_{\IZ,\IQ}$ -category: CRing +associated: + category: CRing description: 'The inclusion $\iota_{\IZ,\IQ} : \IZ \hookrightarrow \IQ$ is a typical example of a localization. It is a standard example of a mono- and epimorphism which is not an isomorphism in the category of (commutative) rings.' nlab_link: https://ncatlab.org/nlab/show/localization+of+a+commutative+ringlization diff --git a/database/data/morphisms/multiply-2.yaml b/database/data/morphisms/multiply-2.yaml index 63cbd54c..12f4d4b4 100644 --- a/database/data/morphisms/multiply-2.yaml +++ b/database/data/morphisms/multiply-2.yaml @@ -1,7 +1,8 @@ id: multiply-2 name: multiplication with 2 notation: $2$ -category: TorsFreeAb +associated: + category: TorsFreeAb description: 'The multiplication map $2 : \IZ \to \IZ$ in $\TorsFreeAb$ provides an example of a monomorphism in an additive category which is not regular (and hence, not normal). Thus, it provides a proof that $\TorsFreeAb$ is not abelian.' nlab_link: null diff --git a/database/data/morphisms/reduction-mod-p.yaml b/database/data/morphisms/reduction-mod-p.yaml index 3465ca57..74aca74e 100644 --- a/database/data/morphisms/reduction-mod-p.yaml +++ b/database/data/morphisms/reduction-mod-p.yaml @@ -1,7 +1,8 @@ id: reduction-mod-p name: reduction modulo p notation: $\bmod\, p$ -category: Ab +associated: + category: Ab description: This is the projection homomorphism $\IZ \to \IZ/p$, where $p$ is a prime number. It is a common example of an epimorphism in $\Ab$ which does not split. nlab_link: null diff --git a/database/data/morphisms/terminal-map.yaml b/database/data/morphisms/terminal-map.yaml index f6f19410..aa8f80d6 100644 --- a/database/data/morphisms/terminal-map.yaml +++ b/database/data/morphisms/terminal-map.yaml @@ -1,7 +1,8 @@ id: terminal-map name: map into the singleton set notation: $!$ -category: Set +associated: + category: Set description: 'For every set $X$ there is a unique map $! : X \to 1$, where $1$ is the singleton set. In this entry, we require that $X$ has at least $2$ elements.' nlab_link: null diff --git a/database/data/morphisms/universal-morphism.yaml b/database/data/morphisms/universal-morphism.yaml index 2a8ca413..d473e4bf 100644 --- a/database/data/morphisms/universal-morphism.yaml +++ b/database/data/morphisms/universal-morphism.yaml @@ -1,7 +1,8 @@ id: universal-morphism name: universal morphism notation: $!$ -category: walking_morphism +associated: + category: walking_morphism description: 'This is the morphism $! : 0 \to 1$ in the walking morphism $I$, see there for details.' nlab_link: null diff --git a/database/data/morphisms/universal-split-epi.yaml b/database/data/morphisms/universal-split-epi.yaml index 80cb8416..837721ce 100644 --- a/database/data/morphisms/universal-split-epi.yaml +++ b/database/data/morphisms/universal-split-epi.yaml @@ -1,7 +1,8 @@ id: universal-split-epi name: universal split epimorphism notation: $p$ -category: walking_splitting +associated: + category: walking_splitting description: 'This is the morphism $p : 1 \to 0$ in the walking splitting, see there for details. It can also be seen as the unique morphism $\IF_2 \to 0$ in the category of $\IF_2$-vector spaces of dimension $\leq 1$. It provides a basic example of a split epimorphism (and hence regular and strict epimorphism) which is not effective.' nlab_link: null diff --git a/database/data/morphisms/walking-idempotent-presentation.yaml b/database/data/morphisms/walking-idempotent-presentation.yaml index 06921a48..901f9bfb 100644 --- a/database/data/morphisms/walking-idempotent-presentation.yaml +++ b/database/data/morphisms/walking-idempotent-presentation.yaml @@ -1,7 +1,8 @@ id: walking-idempotent-presentation name: presentation of the walking idempotent notation: $F$ -category: Cat +associated: + category: Cat description: 'Let $I$ denote the walking morphism and $\Idem$ denote the walking idempotent. In this entry, we consider the functor $F : I \to \Idem$ that sends the universal morphism $! : 0 \to 1$ to the universal idempotent $e : 0 \to 0$ and view $F$ as a morphism in $\Cat$. It provides an example of a strong epimorphism which is not strict.' nlab_link: null diff --git a/database/data/symmetric_monoidal_categories/1_tensor.yaml b/database/data/symmetric_monoidal_categories/1_tensor.yaml index e6b5d28f..278f4ecc 100644 --- a/database/data/symmetric_monoidal_categories/1_tensor.yaml +++ b/database/data/symmetric_monoidal_categories/1_tensor.yaml @@ -1,7 +1,8 @@ id: 1_tensor name: trivial symmetric monoidal category notation: $(1,\times,0)$ -underlying_category: '1' +associated: + underlying_category: '1' description: This is the terminal symmetric monoidal category. It is the trivial category $1$ equipped with its unique strict symmetric monoidal structure. The monoidal unit is the unique object $0$. nlab_link: null diff --git a/database/data/symmetric_monoidal_categories/Ab_fg_tensor.yaml b/database/data/symmetric_monoidal_categories/Ab_fg_tensor.yaml index 28107ba3..f0e33e12 100644 --- a/database/data/symmetric_monoidal_categories/Ab_fg_tensor.yaml +++ b/database/data/symmetric_monoidal_categories/Ab_fg_tensor.yaml @@ -1,7 +1,8 @@ id: Ab_fg_tensor name: symmetric monoidal category of finitely generated abelian groups notation: $(\Ab_{\fg},\otimes,\IZ)$ -underlying_category: Ab_fg +associated: + underlying_category: Ab_fg description: This is the full symmetric monoidal subcategory of $(\Ab,\otimes,\IZ)$ spanned by the finitely generated abelian groups. This is well-defined because $\IZ$ is finitely generated and the tensor product of two finitely generated abelian groups is finitely generated. nlab_link: null diff --git a/database/data/symmetric_monoidal_categories/Ab_tensor.yaml b/database/data/symmetric_monoidal_categories/Ab_tensor.yaml index 52778822..a0ab8af2 100644 --- a/database/data/symmetric_monoidal_categories/Ab_tensor.yaml +++ b/database/data/symmetric_monoidal_categories/Ab_tensor.yaml @@ -1,7 +1,8 @@ id: Ab_tensor name: symmetric monoidal category of abelian groups notation: $(\Ab,\otimes,\IZ)$ -underlying_category: Ab +associated: + underlying_category: Ab description: This is the category of abelian groups equipped with the usual tensor product of abelian groups and the monoidal unit $\IZ$. It is the special case of $(R{-}\Mod,\otimes,R)$ where $R = \IZ$. nlab_link: https://ncatlab.org/nlab/show/tensor+product+of+abelian+groups parent: R-Mod_tensor_naf diff --git a/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml b/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml index 41fb0ef2..3a007e74 100644 --- a/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml +++ b/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml @@ -1,7 +1,8 @@ id: Cat_cartesian name: cartesian symmetric monoidal category of small categories notation: $(\Cat,\times,1)$ -underlying_category: Cat +associated: + underlying_category: Cat description: Every category with finite products (also called a cartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the terminal object and $\otimes$ is the product $\times$. In this case, we apply this to the category $\Cat$ of small categories. nlab_link: https://ncatlab.org/nlab/show/cartesian+monoidal+category diff --git a/database/data/symmetric_monoidal_categories/FinVect_tensor.yaml b/database/data/symmetric_monoidal_categories/FinVect_tensor.yaml index 503dfa6f..1c9cd341 100644 --- a/database/data/symmetric_monoidal_categories/FinVect_tensor.yaml +++ b/database/data/symmetric_monoidal_categories/FinVect_tensor.yaml @@ -1,7 +1,8 @@ id: FinVect_tensor name: symmetric monoidal category of finite-dimensional vector spaces notation: $(\FinVect_K,\otimes,K)$ -underlying_category: FinVect +associated: + underlying_category: FinVect description: This is the full symmetric monoidal subcategory of $(\Vect_K,\otimes,K)$ (see here) spanned by the finite-dimensional vector spaces. nlab_link: https://ncatlab.org/nlab/show/FinDimVect diff --git a/database/data/symmetric_monoidal_categories/N+.yaml b/database/data/symmetric_monoidal_categories/N+.yaml index 931a4eac..f5062ce4 100644 --- a/database/data/symmetric_monoidal_categories/N+.yaml +++ b/database/data/symmetric_monoidal_categories/N+.yaml @@ -1,7 +1,8 @@ id: N+ name: symmetric monoidal poset of natural numbers notation: $(\IN,\leq,+,0)$ -underlying_category: N +associated: + underlying_category: N description: We view the poset $(\IN,\leq)$ as a thin category and equip it with the strict symmetric monoidal structure defined by $a \otimes b \coloneqq a + b$ and the monoidal unit $0$. nlab_link: https://ncatlab.org/nlab/show/monoidal+preorder diff --git a/database/data/symmetric_monoidal_categories/R-Mod_tensor.yaml b/database/data/symmetric_monoidal_categories/R-Mod_tensor.yaml index e833197a..c2beb475 100644 --- a/database/data/symmetric_monoidal_categories/R-Mod_tensor.yaml +++ b/database/data/symmetric_monoidal_categories/R-Mod_tensor.yaml @@ -1,7 +1,8 @@ id: R-Mod_tensor name: symmetric monoidal category of modules over a commutative ring notation: $(R{-}\Mod,\otimes,R)$ -underlying_category: R-Mod +associated: + underlying_category: R-Mod description: When $R$ is a commutative ring, we equip the category of left $R$-modules $R{-}\Mod$ with the usual symmetric monoidal structure, where $\otimes$ is the tensor product of modules and the monoidal unit is $R$. The associator is defined by $(a \otimes b) \otimes c \mapsto a \otimes (b \otimes c)$, the left unitor maps $1 \otimes a \mapsto a$, the right unitor maps $a \otimes 1 \mapsto a$, and the symmetry maps $a \otimes b \mapsto b \otimes a$. nlab_link: https://ncatlab.org/nlab/show/tensor+product+of+modules diff --git a/database/data/symmetric_monoidal_categories/R-Mod_tensor_af.yaml b/database/data/symmetric_monoidal_categories/R-Mod_tensor_af.yaml index 50e60dab..edcb627d 100644 --- a/database/data/symmetric_monoidal_categories/R-Mod_tensor_af.yaml +++ b/database/data/symmetric_monoidal_categories/R-Mod_tensor_af.yaml @@ -1,7 +1,8 @@ id: R-Mod_tensor_af name: symmetric monoidal category of modules over an absolutely flat commutative ring notation: $(R{-}\Mod,\otimes,R)$ -underlying_category: R-Mod +associated: + underlying_category: R-Mod description: This is the special case of this entry where we assume that $R$ is absolutely flat and non-zero. For example, every field has this property, so that this entry also includes the symmetric monoidal category of vector spaces. nlab_link: https://ncatlab.org/nlab/show/tensor+product+of+modules parent: R-Mod_tensor diff --git a/database/data/symmetric_monoidal_categories/R-Mod_tensor_naf.yaml b/database/data/symmetric_monoidal_categories/R-Mod_tensor_naf.yaml index f2eb58d1..02d33b39 100644 --- a/database/data/symmetric_monoidal_categories/R-Mod_tensor_naf.yaml +++ b/database/data/symmetric_monoidal_categories/R-Mod_tensor_naf.yaml @@ -1,7 +1,8 @@ id: R-Mod_tensor_naf name: symmetric monoidal category of modules over a non-absolutely flat commutative ring notation: $(R{-}\Mod,\otimes,R)$ -underlying_category: R-Mod +associated: + underlying_category: R-Mod description: This is the special case of $(R{-}\Mod,\otimes,R)$ where $R$ is a commutative ring that is not absolutely flat. nlab_link: https://ncatlab.org/nlab/show/tensor+product+of+modules parent: R-Mod_tensor diff --git a/database/data/symmetric_monoidal_categories/Set_cartesian.yaml b/database/data/symmetric_monoidal_categories/Set_cartesian.yaml index 4225e650..790f8e6a 100644 --- a/database/data/symmetric_monoidal_categories/Set_cartesian.yaml +++ b/database/data/symmetric_monoidal_categories/Set_cartesian.yaml @@ -1,7 +1,8 @@ id: Set_cartesian name: cartesian symmetric monoidal category of sets notation: $(\Set,\times,1)$ -underlying_category: Set +associated: + underlying_category: Set description: Every category with finite products (also called a cartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the terminal object and $\otimes$ is the product $\times$. In this case, we apply this to the category $\Set$. nlab_link: https://ncatlab.org/nlab/show/cartesian+monoidal+category diff --git a/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml b/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml index a7003fca..ed398933 100644 --- a/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml +++ b/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml @@ -1,7 +1,8 @@ id: Set_cocartesian name: cocartesian symmetric monoidal category of sets notation: $(\Set,\sqcup,0)$ -underlying_category: Set +associated: + underlying_category: Set description: Every category with finite coproducts (also called a cocartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the initial object and $\otimes$ is the coproduct $\sqcup$. In this case, we apply this to the category $\Set$. nlab_link: https://ncatlab.org/nlab/show/cocartesian+monoidal+category diff --git a/database/data/symmetric_monoidal_categories/Top_cartesian.yaml b/database/data/symmetric_monoidal_categories/Top_cartesian.yaml index d8f1659d..fca3504d 100644 --- a/database/data/symmetric_monoidal_categories/Top_cartesian.yaml +++ b/database/data/symmetric_monoidal_categories/Top_cartesian.yaml @@ -1,7 +1,8 @@ id: Top_cartesian name: cartesian symmetric monoidal category of topological spaces notation: $(\Top,\times,1)$ -underlying_category: Top +associated: + underlying_category: Top description: Every category with finite products (also called a cartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the terminal object and $\otimes$ is the product $\times$. In this case, we apply this to the category $\Top$. nlab_link: https://ncatlab.org/nlab/show/cartesian+monoidal+category From 1d3d55bb8a2b47f5690a80cae8e595b46a7c0cb4 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 20 Sep 2026 00:47:39 +0200 Subject: [PATCH 3/5] validate seed files with new valibot schemas --- database/scripts/seed.ts | 99 ++++++++++++++++---------- database/scripts/utils/seed.helpers.ts | 52 ++++++++++---- database/scripts/utils/seed.types.ts | 91 ----------------------- 3 files changed, 100 insertions(+), 142 deletions(-) delete mode 100644 database/scripts/utils/seed.types.ts diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index 0113fbc8..83d5e6b3 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -2,17 +2,18 @@ import fs from 'node:fs' import path from 'node:path' import { get_property_assignments, seed_file, seed_files } from './utils/seed.helpers' import { get_client } from '$shared/db' -import type { - CategoryYaml, - ConfigYaml, - ImplicationYaml, - SpecialMorphismRuleYaml, - StructureYaml, - PropertyYaml -} from './utils/seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' import { are_disjoint, capitalize, devlog } from '$shared/utils' +import { + category_yaml_schema, + config_yaml_schema, + implications_yaml_schema, + property_yaml_schema, + special_morphism_rule_yaml_schema, + structure_yaml_schema +} from './utils/seed.schemas' +import * as v from 'valibot' const db = get_client({ readonly: false }) @@ -40,7 +41,8 @@ function seed() { seed_properties({ type: 'category', folder: 'category-properties' }) seed_special_morphism_rules() seed_implications({ type: 'category', folder: 'category-implications' }) - seed_structures({ type: 'category', folder: 'categories', extra: insert_category }) + seed_structures({ type: 'category', folder: 'categories' }) + seed_special_category_data({ folder: 'categories' }) seed_properties({ type: 'functor', folder: 'functor-properties' }) seed_implications({ type: 'functor', folder: 'functor-implications' }) @@ -154,7 +156,7 @@ function seed_config() { `INSERT INTO special_morphisms (kind, dual) VALUES (?, ?)` ) - function insert_config(config: ConfigYaml) { + function insert_config(config: v.InferOutput) { for (const type of STRUCTURE_TYPES) { for (const tag of config.structure_tags) { structure_tag_insert.run(tag, type) @@ -182,7 +184,13 @@ function seed_config() { } } - seed_file(db, 'config', path.join(data_folder, 'config.yaml'), insert_config) + seed_file( + db, + 'config', + path.join(data_folder, 'config.yaml'), + config_yaml_schema, + insert_config + ) } /** @@ -195,7 +203,9 @@ function seed_special_morphism_rules() { VALUES (?, ?, ?, ?)` ) - function insert_rules(rules: SpecialMorphismRuleYaml[]) { + function insert_rules( + rules: v.InferOutput + ) { for (const { property, kind, description, proof } of rules) { rule_insert.run(property, kind, description, proof) } @@ -205,6 +215,7 @@ function seed_special_morphism_rules() { db, 'special morphism rules', path.join(data_folder, 'special-morphism-rules.yaml'), + special_morphism_rule_yaml_schema, insert_rules ) } @@ -213,19 +224,11 @@ function seed_special_morphism_rules() { * Seeds all structures from YAML files of a given type, * including their property assignments. */ -function seed_structures({ - type, - folder, - extra -}: { - type: StructureType - folder: string - extra?: (structure: T) => void -}) { +function seed_structures({ type, folder }: { type: StructureType; folder: string }) { const structure_associations = db .prepare< [StructureType], - { label: keyof T; target_type: StructureType; required: 0 | 1 } + { label: string; target_type: StructureType; required: 0 | 1 } >( `SELECT label, target_type, required FROM structure_associations WHERE source_type = ?` @@ -275,7 +278,7 @@ function seed_structures({ ) VALUES (?, ?, ?, ?, ?)` ) - function insert_structure(structure: T) { + function insert_structure(structure: v.InferOutput) { const properties_are_disjoint = are_disjoint( [ structure.satisfied_properties, @@ -304,20 +307,20 @@ function seed_structures({ record_structure_addition(structure.id) for (const { label, target_type, required } of structure_associations) { - if (required && !structure[label]) { + if (required && !structure.associated?.[label]) { console.error( `❌ ${capitalize(type)} "${structure.id}" has no ${label.toString()}` ) process.exit(1) } - if (structure[label]) { + if (structure.associated?.[label]) { associated_structure_insert.run( label, type, target_type, structure.id, - structure[label] + structure.associated?.[label] ) } } @@ -356,11 +359,15 @@ function seed_structures({ proof_reference_insert.run(structure.id, entry.property, type, ref) } } - - if (extra) extra(structure) } - seed_files(db, PLURALS[type], path.join(data_folder, folder), insert_structure) + seed_files( + db, + PLURALS[type], + path.join(data_folder, folder), + structure_yaml_schema, + insert_structure + ) } /** @@ -375,9 +382,9 @@ function record_structure_addition(id: string) { } /** - * Inserts the data of a category that is specific to categories. + * Inserts data of categories that is specific to categories. */ -function insert_category(category: CategoryYaml) { +function seed_special_category_data({ folder }: { folder: string }) { const category_insert = db.prepare( `INSERT INTO categories ( id, objects, morphisms @@ -396,15 +403,25 @@ function insert_category(category: CategoryYaml) { ) VALUES (?, ?, ?, ?)` ) - category_insert.run(category.id, category.objects, category.morphisms) + function insert_category(category: v.InferOutput) { + category_insert.run(category.id, category.objects, category.morphisms) - for (const [kind, entry] of Object.entries(category.special_objects)) { - special_object_insert.run(category.id, kind, entry.description) - } + for (const [kind, entry] of Object.entries(category.special_objects)) { + special_object_insert.run(category.id, kind, entry.description) + } - for (const [kind, entry] of Object.entries(category.special_morphisms)) { - special_morphism_insert.run(category.id, kind, entry.description, entry.proof) + for (const [kind, entry] of Object.entries(category.special_morphisms)) { + special_morphism_insert.run(category.id, kind, entry.description, entry.proof) + } } + + seed_files( + db, + 'special category data', + path.join(data_folder, folder), + category_yaml_schema, + insert_category + ) } /** @@ -430,7 +447,7 @@ function seed_properties({ type, folder }: { type: StructureType; folder: string VALUES (?, ?, ?)` ) - function insert_property(property: PropertyYaml) { + function insert_property(property: v.InferOutput) { property_insert.run( property.id, type, @@ -459,6 +476,7 @@ function seed_properties({ type, folder }: { type: StructureType; folder: string db, `properties of ${PLURALS[type]}`, path.join(data_folder, folder), + property_yaml_schema, insert_property ) } @@ -498,7 +516,9 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri ) VALUES (?, ?, ?, ?, ?)` ) - function insert_implications(implications: ImplicationYaml[]) { + function insert_implications( + implications: v.InferOutput + ) { for (const impl of implications) { if (!impl.assumptions.length && !impl.associated_assumptions) { console.error(`❌ Implication ${impl.id} has no assumptions.`) @@ -540,6 +560,7 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri db, `${type} implications`, path.join(data_folder, folder), + implications_yaml_schema, insert_implications ) } diff --git a/database/scripts/utils/seed.helpers.ts b/database/scripts/utils/seed.helpers.ts index 70bf9cd2..7eafaa9d 100644 --- a/database/scripts/utils/seed.helpers.ts +++ b/database/scripts/utils/seed.helpers.ts @@ -3,11 +3,12 @@ import path from 'node:path' import fs from 'node:fs' import YAML from 'yaml' import { devlog } from '$shared/utils' -import { StructureYaml } from './seed.types' +import * as v from 'valibot' +import { structure_yaml_schema } from './seed.schemas' -function read_yaml_file(...parts: string[]): T { +function read_yaml_file(...parts: string[]) { const content = fs.readFileSync(path.join(...parts), 'utf8') - return YAML.parse(content) as T + return YAML.parse(content) as unknown } function get_yaml_files(folder: string) { @@ -17,18 +18,30 @@ function get_yaml_files(folder: string) { .sort() } -export function seed_file( +export function seed_file( db: Database, label: string, file: string, - insert: (item: T) => void + schema: Schema, + insert: (item: v.InferOutput) => void ) { devlog(`\nSeed ${label} ...`) - const item = read_yaml_file(file) + const item = read_yaml_file(file) + + const { output, issues } = v.safeParse(schema, item) + + if (issues) { + console.error(`❌ Contents of ${file} have invalid format`) + issues.forEach((issue) => { + const path = issue.path?.map((item) => item.key).join('.') ?? '' + console.error(`${path}: ${issue.message}`) + }) + process.exit(1) + } const tx = db.transaction(() => { db.pragma('defer_foreign_keys = ON') - insert(item) + insert(output) }) try { @@ -39,11 +52,12 @@ export function seed_file( } } -export function seed_files( +export function seed_files( db: Database, label: string, folder: string, - insert: (item: T) => void + schema: Schema, + insert: (item: v.InferOutput) => void ) { devlog(`\nSeed ${label} ...`) @@ -55,8 +69,20 @@ export function seed_files( for (const file of files) { devlog(`Seed: ${file}`) - const item = read_yaml_file(folder, file) - insert(item) + const item = read_yaml_file(folder, file) + + const { output, issues } = v.safeParse(schema, item) + + if (issues) { + console.error(`❌ Contents of ${file} have invalid format`) + issues.forEach((issue) => { + const path = issue.path?.map((item) => item.key).join('.') ?? '' + console.error(`${path}: ${issue.message}`) + }) + process.exit(1) + } + + insert(output) } }) @@ -68,7 +94,9 @@ export function seed_files( } } -export function get_property_assignments(structure: StructureYaml) { +export function get_property_assignments( + structure: v.InferOutput +) { return [ ...structure.satisfied_properties.map((entry) => ({ ...entry, diff --git a/database/scripts/utils/seed.types.ts b/database/scripts/utils/seed.types.ts deleted file mode 100644 index b2b8e287..00000000 --- a/database/scripts/utils/seed.types.ts +++ /dev/null @@ -1,91 +0,0 @@ -export type ConfigYaml = { - structure_tags: string[] - category_tags: string[] - functor_tags: string[] - morphism_tags: string[] - symmetric_monoidal_category_tags: string[] - category_property_tags: string[] - functor_property_tags: string[] - morphism_property_tags: string[] - symmetric_monoidal_category_property_tags: string[] - relations: { - relation: string - negation: string - conditional: string - }[] - special_objects: { - kind: string - dual: string - }[] - special_morphisms: { - kind: string - dual: string - }[] -} - -export type SpecialMorphismRuleYaml = { - property: string - kind: string - description: string - proof: string -} - -type PropertyEntry = { - property: string - proof: string - check_redundancy?: boolean - label?: string - references?: string[] -} - -type ObjectEntry = { - description: string -} - -type MorphismEntry = { - description: string - proof: string -} - -export type StructureYaml = { - id: string - name: string - notation: string - description: string - nlab_link: string | null - tags: string[] - related: string[] - dual?: string - parent?: string - satisfied_properties: PropertyEntry[] - unsatisfied_properties: PropertyEntry[] - undecidable_properties?: PropertyEntry[] - comments?: string[] -} - -export type CategoryYaml = StructureYaml & { - objects: string - morphisms: string - special_objects: Record - special_morphisms: Record -} - -export type PropertyYaml = { - id: string - relation: string - description: string - nlab_link: string | null - dual: string | null - invariant_under_equivalences: boolean - related: string[] - tags: string[] -} - -export type ImplicationYaml = { - id: string - assumptions: string[] - conclusions: string[] - associated_assumptions?: Partial> - proof: string - is_equivalence?: boolean -} From ad1ee70da47b72a50aece2c0103bb04fc1cb5111 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 20 Sep 2026 01:18:41 +0200 Subject: [PATCH 4/5] move various manual checks from the seed functions to the schema definitions - tags are present - implications have at least one conclusion and at least assumption (possibly associated) - assigned properties of structures are disjoint new rule: check_redundancy can only be set as `false` (since `true` is the default anyway) --- database/scripts/seed.ts | 36 +--------- database/scripts/utils/seed.schemas.ts | 94 ++++++++++++++++---------- 2 files changed, 58 insertions(+), 72 deletions(-) diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index 83d5e6b3..3daa3001 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -4,7 +4,7 @@ import { get_property_assignments, seed_file, seed_files } from './utils/seed.he import { get_client } from '$shared/db' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' -import { are_disjoint, capitalize, devlog } from '$shared/utils' +import { capitalize, devlog } from '$shared/utils' import { category_yaml_schema, config_yaml_schema, @@ -279,20 +279,6 @@ function seed_structures({ type, folder }: { type: StructureType; folder: string ) function insert_structure(structure: v.InferOutput) { - const properties_are_disjoint = are_disjoint( - [ - structure.satisfied_properties, - structure.unsatisfied_properties, - structure.undecidable_properties ?? [] - ], - (entry) => entry.property - ) - - if (!properties_are_disjoint) { - console.error(`❌ Properties of ${structure.id} are contradictory.`) - process.exit(1) - } - structure_insert.run( structure.id, type, @@ -325,11 +311,6 @@ function seed_structures({ type, folder }: { type: StructureType; folder: string } } - if (!structure.tags.length) { - console.error(`❌ ${capitalize(type)} "${structure.id}" has no tags`) - process.exit(1) - } - for (const tag of structure.tags) { tag_insert.run(structure.id, tag, type) } @@ -462,11 +443,6 @@ function seed_properties({ type, folder }: { type: StructureType; folder: string related_insert.run(property.id, related, type) } - if (!property.tags.length) { - console.error(`❌ Property "${property.id}" has no tags`) - process.exit(1) - } - for (const tag of property.tags) { tag_insert.run(property.id, tag, type) } @@ -520,16 +496,6 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri implications: v.InferOutput ) { for (const impl of implications) { - if (!impl.assumptions.length && !impl.associated_assumptions) { - console.error(`❌ Implication ${impl.id} has no assumptions.`) - process.exit(1) - } - - if (!impl.conclusions.length) { - console.error(`❌ Implication ${impl.id} has no conclusions.`) - process.exit(1) - } - implication_insert.run(impl.id, type, impl.proof, impl.is_equivalence ? 1 : 0) for (const assumption of impl.assumptions) { diff --git a/database/scripts/utils/seed.schemas.ts b/database/scripts/utils/seed.schemas.ts index e7933200..f4d5be9f 100644 --- a/database/scripts/utils/seed.schemas.ts +++ b/database/scripts/utils/seed.schemas.ts @@ -1,3 +1,4 @@ +import { are_disjoint } from '$shared/utils' import * as v from 'valibot' export const config_yaml_schema = v.object({ @@ -6,10 +7,12 @@ export const config_yaml_schema = v.object({ functor_tags: v.array(v.string()), morphism_tags: v.array(v.string()), symmetric_monoidal_category_tags: v.array(v.string()), + category_property_tags: v.array(v.string()), functor_property_tags: v.array(v.string()), morphism_property_tags: v.array(v.string()), symmetric_monoidal_category_property_tags: v.array(v.string()), + relations: v.array( v.object({ relation: v.string(), @@ -17,12 +20,14 @@ export const config_yaml_schema = v.object({ conditional: v.string() }) ), + special_objects: v.array( v.object({ kind: v.string(), dual: v.string() }) ), + special_morphisms: v.array( v.object({ kind: v.string(), @@ -40,47 +45,53 @@ export const special_morphism_rule_yaml_schema = v.array( }) ) -export const property_entry_schema = v.object({ +const property_entry_schema = v.object({ property: v.string(), proof: v.string(), - check_redundancy: v.optional(v.boolean()), + check_redundancy: v.optional(v.literal(false)), label: v.optional(v.string()), references: v.optional(v.array(v.string())) }) -export const structure_yaml_schema = v.object({ - id: v.string(), - name: v.string(), - notation: v.string(), - description: v.string(), - nlab_link: v.nullable(v.string()), - tags: v.array(v.string()), - related: v.array(v.string()), - dual: v.optional(v.string()), - parent: v.optional(v.string()), - associated: v.optional(v.record(v.string(), v.nullable(v.string()))), - satisfied_properties: v.array(property_entry_schema), - unsatisfied_properties: v.array(property_entry_schema), - undecidable_properties: v.optional(v.array(property_entry_schema)), - comments: v.optional(v.array(v.string())) -}) +export const structure_yaml_schema = v.pipe( + v.object({ + id: v.string(), + name: v.string(), + notation: v.string(), + description: v.string(), + nlab_link: v.nullable(v.string()), + tags: v.pipe(v.array(v.string()), v.minLength(1)), + related: v.array(v.string()), + dual: v.optional(v.string()), + parent: v.optional(v.string()), + associated: v.optional(v.record(v.string(), v.nullable(v.string()))), + satisfied_properties: v.array(property_entry_schema), + unsatisfied_properties: v.array(property_entry_schema), + undecidable_properties: v.optional(v.array(property_entry_schema)), + comments: v.optional(v.array(v.string())) + }), + v.check( + (structure) => + are_disjoint( + [ + structure.satisfied_properties, + structure.unsatisfied_properties, + structure.undecidable_properties ?? [] + ], + (entry) => entry.property + ), + 'Satisfied, unsatisfied, and undecidable properties must be disjoint.' + ) +) export const category_yaml_schema = v.object({ id: v.string(), objects: v.string(), morphisms: v.string(), - special_objects: v.record( - v.string(), - v.object({ - description: v.string() - }) - ), + special_objects: v.record(v.string(), v.object({ description: v.string() })), special_morphisms: v.record( v.string(), - v.object({ - description: v.string(), - proof: v.string() - }) + v.object({ description: v.string(), proof: v.string() }) ) }) @@ -92,16 +103,25 @@ export const property_yaml_schema = v.object({ dual: v.nullable(v.string()), invariant_under_equivalences: v.boolean(), related: v.array(v.string()), - tags: v.array(v.string()) + tags: v.pipe(v.array(v.string()), v.minLength(1)) }) export const implications_yaml_schema = v.array( - v.object({ - id: v.string(), - assumptions: v.array(v.string()), - conclusions: v.array(v.string()), - associated_assumptions: v.optional(v.record(v.string(), v.array(v.string()))), - proof: v.string(), - is_equivalence: v.optional(v.boolean()) - }) + v.pipe( + v.object({ + id: v.string(), + assumptions: v.array(v.string()), + conclusions: v.pipe(v.array(v.string()), v.minLength(1)), + associated_assumptions: v.optional(v.record(v.string(), v.array(v.string()))), + proof: v.string(), + is_equivalence: v.optional(v.boolean()) + }), + v.check( + (impl) => + impl.assumptions.length > 0 || + (impl.associated_assumptions !== undefined && + Object.keys(impl.associated_assumptions).length > 0), + `Implication must have at least one assumption or associated assumptions.` + ) + ) ) From d295d02f2a1db0ccfe6872ec2f498e9b66343002 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 20 Sep 2026 10:18:28 +0200 Subject: [PATCH 5/5] make schemas more strict --- database/scripts/utils/seed.schemas.ts | 66 +++++++++++++++----------- 1 file changed, 38 insertions(+), 28 deletions(-) diff --git a/database/scripts/utils/seed.schemas.ts b/database/scripts/utils/seed.schemas.ts index f4d5be9f..6787540d 100644 --- a/database/scripts/utils/seed.schemas.ts +++ b/database/scripts/utils/seed.schemas.ts @@ -1,20 +1,28 @@ import { are_disjoint } from '$shared/utils' import * as v from 'valibot' -export const config_yaml_schema = v.object({ - structure_tags: v.array(v.string()), - category_tags: v.array(v.string()), - functor_tags: v.array(v.string()), - morphism_tags: v.array(v.string()), - symmetric_monoidal_category_tags: v.array(v.string()), +const distinct_strings_schema = v.pipe( + v.array(v.string()), + v.check( + (values) => new Set(values).size === values.length, + 'Values must be pairwise distinct.' + ) +) - category_property_tags: v.array(v.string()), - functor_property_tags: v.array(v.string()), - morphism_property_tags: v.array(v.string()), - symmetric_monoidal_category_property_tags: v.array(v.string()), +export const config_yaml_schema = v.strictObject({ + structure_tags: distinct_strings_schema, + category_tags: distinct_strings_schema, + functor_tags: distinct_strings_schema, + morphism_tags: distinct_strings_schema, + symmetric_monoidal_category_tags: distinct_strings_schema, + + category_property_tags: distinct_strings_schema, + functor_property_tags: distinct_strings_schema, + morphism_property_tags: distinct_strings_schema, + symmetric_monoidal_category_property_tags: distinct_strings_schema, relations: v.array( - v.object({ + v.strictObject({ relation: v.string(), negation: v.string(), conditional: v.string() @@ -22,14 +30,14 @@ export const config_yaml_schema = v.object({ ), special_objects: v.array( - v.object({ + v.strictObject({ kind: v.string(), dual: v.string() }) ), special_morphisms: v.array( - v.object({ + v.strictObject({ kind: v.string(), dual: v.string() }) @@ -37,7 +45,7 @@ export const config_yaml_schema = v.object({ }) export const special_morphism_rule_yaml_schema = v.array( - v.object({ + v.strictObject({ property: v.string(), kind: v.string(), description: v.string(), @@ -45,12 +53,12 @@ export const special_morphism_rule_yaml_schema = v.array( }) ) -const property_entry_schema = v.object({ +const property_entry_schema = v.strictObject({ property: v.string(), proof: v.string(), check_redundancy: v.optional(v.literal(false)), label: v.optional(v.string()), - references: v.optional(v.array(v.string())) + references: v.optional(distinct_strings_schema) }) export const structure_yaml_schema = v.pipe( @@ -60,8 +68,8 @@ export const structure_yaml_schema = v.pipe( notation: v.string(), description: v.string(), nlab_link: v.nullable(v.string()), - tags: v.pipe(v.array(v.string()), v.minLength(1)), - related: v.array(v.string()), + tags: v.pipe(distinct_strings_schema, v.minLength(1)), + related: distinct_strings_schema, dual: v.optional(v.string()), parent: v.optional(v.string()), associated: v.optional(v.record(v.string(), v.nullable(v.string()))), @@ -88,33 +96,35 @@ export const category_yaml_schema = v.object({ id: v.string(), objects: v.string(), morphisms: v.string(), - special_objects: v.record(v.string(), v.object({ description: v.string() })), + special_objects: v.record(v.string(), v.strictObject({ description: v.string() })), special_morphisms: v.record( v.string(), - v.object({ description: v.string(), proof: v.string() }) + v.strictObject({ description: v.string(), proof: v.string() }) ) }) -export const property_yaml_schema = v.object({ +export const property_yaml_schema = v.strictObject({ id: v.string(), relation: v.string(), description: v.string(), nlab_link: v.nullable(v.string()), dual: v.nullable(v.string()), invariant_under_equivalences: v.boolean(), - related: v.array(v.string()), - tags: v.pipe(v.array(v.string()), v.minLength(1)) + related: distinct_strings_schema, + tags: v.pipe(distinct_strings_schema, v.minLength(1)) }) export const implications_yaml_schema = v.array( v.pipe( - v.object({ + v.strictObject({ id: v.string(), - assumptions: v.array(v.string()), - conclusions: v.pipe(v.array(v.string()), v.minLength(1)), - associated_assumptions: v.optional(v.record(v.string(), v.array(v.string()))), + assumptions: distinct_strings_schema, + conclusions: v.pipe(distinct_strings_schema, v.minLength(1)), + associated_assumptions: v.optional( + v.record(v.string(), distinct_strings_schema) + ), proof: v.string(), - is_equivalence: v.optional(v.boolean()) + is_equivalence: v.optional(v.literal(true)) }), v.check( (impl) =>