diff --git a/content/functors_on_discrete_categories.md b/content/functors_on_discrete_categories.md new file mode 100644 index 000000000..31d1b55f3 --- /dev/null +++ b/content/functors_on_discrete_categories.md @@ -0,0 +1,45 @@ +--- +title: Functors on discrete categories +description: We describe which functors on discrete categories are continuous or cocontinuous. +author: Martin Brandenburg +--- + +## Functors on discrete categories + +Let $\S$ be a discrete category. Thus, a functor $F : \S \to \C$ is the same as a family of objects $F(s) \in \C$ indexed by the objects $s \in \S$. Here, we want to determine under which conditions $F$ is continuous (or cocontinuous). The case $\S = \varnothing$ is rather boring, which is why we assume from now on that $\S \neq \varnothing$, i.e. that $\S$ is inhabited. + +First, we consider the trivial case $\S = 1$. + +::: Lemma 1 +Consider the trivial category $1 = \{0\}$ with a unique object $0$. Let $F : 1 \to \C$ be a functor corresponding to an object $F(0) \in \C$. Then $F$ is continuous if and only if $F(0)$ is a terminal object in $\C$. +::: + +_Proof._ If $F$ is continuous, it preserves terminal objects. Since $0 \in 1$ is terminal, it follows that $F(0) \in \C$ is terminal. Conversely, suppose that $F(0) \in \C$ is terminal. Then $F$ is continuous: for every index category $\I$, there is a unique diagram $D : \I \to 1$, namely $D(i) = 0$ and $D(i \to j) = \id_0$. Its limit is $0$, with the universal cone $(\id_0 : 0 \to D(i))_{i \in \I}$. We need to show that $(\id_{F(0)} : F(0) \to F(0))_{i \in \I}$ is a universal cone in $\C$. This is easy to see using that $F(0)$ is terminal. $\square$ + +::: Lemma 2 +Let $\S$ be a non-trivial inhabited discrete category. Then a functor $F : \S \to \C$ is continuous if and only if, for every $s \in \S$, the object $F(s) \in \C$ is [subterminal](https://ncatlab.org/nlab/show/subterminal+object), i.e. every two morphisms with codomain $F(s)$ are equal. +::: + +_Proof._ Assume first that $F$ is continuous. An object $X$ is subterminal if and only if $X \times X$ exists and the diagonal $X \to X \times X$ is an isomorphism. Thus, every functor preserving binary products preserves subterminal objects. Since every object in a discrete category is subterminal, it follows that each $F(s) \in \C$ is subterminal. + +Conversely, assume that each $F(s) \in \C$ is subterminal. To show that $F$ is continuous, let $D : \I \to \S$ be a (small) diagram admitting a universal cone $(s \to D(i))_{i \in \I}$. Then $D(i) = s$ for all $i \in \I$, and each morphism $s \to D(i)$ is the identity. Since $\S$ has no terminal object (otherwise, $\S$ would be trivial), $\I$ is inhabited. We need to show that $(\id_{F(s)} : F(s) \to F(s))_{i \in \I}$ is a universal cone in $\C$. This follows immediately from $F(s)$ being subterminal: for a family of morphisms $X \to F(s)$ indexed by $\I$, all morphisms must be equal, and there is one such morphism since $\I$ is inhabited. $\square$ + +Remark that in a thin category, every object is subterminal. Of course, Lemma 2 can also be dualized: A functor on a non-trivial inhabited discrete category is cocontinuous if and only if each object in its image is "co-subterminal". Here, an object $X$ is co-subterminal if any two morphisms with domain $X$ are equal (see [MSE/1092122](https://math.stackexchange.com/questions/1092122) for a discussion of the terminology). + +Next, let us determine which of the continuous functors are right adjoints. + +::: Lemma 3 +Let $\S$ be a discrete category. Then a functor $F : \S \to \C$ is a right adjoint if and only if there is a decomposition $\C = \coprod_{s \in \S} \C_s$ into full subcategories such that $F(s) \in \C_s$ is a terminal object for every $s \in \S$. +::: + +_Proof._ A functor $G : \C \to \S$ corresponds to a decomposition $\C = \coprod_{s \in \S} \C_s$ via +$$G(X) = s \iff X \in \C_s.$$ +It is left adjoint to $F$ if and only if there are natural bijections +$$\Hom(G(X),s) \cong \Hom(X,F(s))$$ +for $X \in \C$ and $s \in \S$. For $X \in \C_s$, this means that there is a unique morphism $X \to F(s)$. For $X \in \C_t$ with $t \neq s$, it means that there is no morphism $X \to F(s)$. In other words, $F(s) \in \C_s$. Naturality in $s$ is automatic since $\S$ is discrete. Naturality in $X$, say for $X \in \C_s$, is also automatic. $\square$ + +::: Corollary 4 +Let $\S$ be a discrete category, and let $\C$ be a connected category. If there is a right adjoint functor $\S \to \C$, then $\S$ is trivial. +::: + +_Proof._ By Lemma 3, such a right adjoint yields a decomposition $\C = \coprod_{s \in \S} \C_s$ into full subcategories, each having a terminal object. In particular, each $\C_s$ is inhabited. Since $\C$ is connected, it follows that $\S$ has exactly one object. $\square$ diff --git a/database/data/functor-implications/adjoints.yaml b/database/data/functor-implications/adjoints.yaml index 938911cf1..0666b2e47 100644 --- a/database/data/functor-implications/adjoints.yaml +++ b/database/data/functor-implications/adjoints.yaml @@ -30,3 +30,27 @@ - right-invertible proof: 'If $F : \C \to \D$ is a reflector, it is left adjoint to a fully faithful functor $G : \D \to \C$. Thus, the counit $\varepsilon : F \circ G \to \id_{\D}$ is an isomorphism (Prop. 3.4 at the nLab). This shows that $G$ is a right inverse of $F$.' is_equivalence: false + +- id: representable_right_adjoint + assumptions: + - representable + mapped_assumptions: + domain: + - locally essentially small + - coproducts + conclusions: + - right adjoint + proof: 'If $\C$ is a locally small category with coproducts and $X \in \C$ is any object, then the copower functor $\Set \to \C$, $T \mapsto T \otimes X$ is left adjoint to $\Hom(X,-) : \C \to \Set$.' + is_equivalence: false + +- id: initial_object_as_left_adjoint + assumptions: [] + mapped_assumptions: + domain: + - initial object + codomain: + - trivial + conclusions: + - coreflector + proof: 'Let $F : \C \to 1$ be the unique functor into the trivial category, and assume that $\C$ has an initial object $X$. Then the constant functor $X : 1 \to \C$ is fully faithful and left adjoint to $F$ because $\Hom(X(*),Y) \cong * \cong \Hom(*,F(Y))$.' + is_equivalence: false diff --git a/database/data/functor-implications/limits preservation.yaml b/database/data/functor-implications/limits preservation.yaml index 0be46bcf2..2cc9670da 100644 --- a/database/data/functor-implications/limits preservation.yaml +++ b/database/data/functor-implications/limits preservation.yaml @@ -203,3 +203,23 @@ - regular proof: This holds by definition of a regular functor. is_equivalence: true + +- id: trivial_functors_continuous + assumptions: [] + mapped_assumptions: + codomain: + - trivial + conclusions: + - continuous + proof: 'We need to show that for every category $\C$ the unique functor $!_{\C} : \C \to 1$ into the trivial category is continuous. This easy to verify directly because in the trivial category every limit is, well, trivial. More generally, for every category $\C$ and every set $S$ the diagonal functor $\Delta : \C \to \C^S$ is continuous. Here we apply this to $S = \varnothing$ so that $\C^S$ is the trivial category.' + is_equivalence: false + +- id: automatically_preserve_equalizers + assumptions: [] + mapped_assumptions: + domain: + - regular-subobject-trivial + conclusions: + - preserves equalizers + proof: This is trivial. + is_equivalence: false diff --git a/database/data/functor-implications/misc.yaml b/database/data/functor-implications/misc.yaml index 2cace7e9c..9e915b32b 100644 --- a/database/data/functor-implications/misc.yaml +++ b/database/data/functor-implications/misc.yaml @@ -78,3 +78,72 @@ - dominant proof: This is trivial. is_equivalence: false + +- id: surjective_functor_to_core_connected_category + assumptions: [] + mapped_assumptions: + domain: + - inhabited + codomain: + - core-connected + conclusions: + - essentially surjective + proof: 'Let $F : \C \to \D$ be a functor from an inhabited category to a core-connected category. Choose any object $X \in \C$. For every $Y \in \D$ we have $Y \cong F(X)$. Thus, $F$ is essentially surjective.' + is_equivalence: false + +- id: right_invertible_functor_to_trivial_category + assumptions: [] + mapped_assumptions: + domain: + - inhabited + codomain: + - trivial + conclusions: + - right-invertible + proof: 'Let $\C$ be an inhabited category and let $F : \C \to 1$ be the unique functor to the trivial category. Choose any object $X \in \C$. Then the constant functor $X : 1 \to \C$ satisfies $F \circ X = \id_1$.' + is_equivalence: false + +- id: full_functor_to_trivial_category + # TODO: add the converse once we have category_conclusions + assumptions: [] + mapped_assumptions: + domain: + - strongly connected + codomain: + - trivial + conclusions: + - full + proof: 'Let $\C$ be a strongly connected category. Then the unique functor $F : \C \to 1$ to the trivial category is full: for all $X,Y \in \C$ the map $\Hom(X,Y) \to \Hom(F(X),F(Y))$ is surjective since its domain is non-empty and its codomain is a singleton set.' + is_equivalence: false + +- id: functor_conservative_on_groupoids + assumptions: [] + mapped_assumptions: + domain: + - groupoid + conclusions: + - conservative + proof: This is trivial. + is_equivalence: false + +- id: automatic_ess_injective_functors + assumptions: [] + mapped_assumptions: + domain: + - core-connected + conclusions: + - essentially injective + proof: This is trivial. + is_equivalence: false + +- id: automatic_full_on_isos_functors + assumptions: [] + mapped_assumptions: + domain: + - core-connected + codomain: + - trivial + conclusions: + - full on isomorphisms + proof: This is trivial. + is_equivalence: false diff --git a/database/data/functors/simple_group_probing.yaml b/database/data/functors/simple_group_probing.yaml new file mode 100644 index 000000000..f5975e225 --- /dev/null +++ b/database/data/functors/simple_group_probing.yaml @@ -0,0 +1,58 @@ +id: simple_group_probing +name: simple-group probing functor +notation: $F$ +domain: Grp +codomain: Set +description: >- + This functor maps a group $G$ to the collection + $$F(G) := \textstyle\prod_{\kappa} \Hom(L_\kappa,G),$$ + where $\kappa$ ranges over all infinite cardinals and $L_\kappa$ is an infinite simple group of cardinality $\kappa$; we choose $L_\kappa := \Alt_{\fin}(\kappa)$ to make things concrete. For each $G$, the collection $F(G)$ is isomorphic to a set, since for $\kappa > \card(G)$ every homomorphism $L_\kappa \to G$ is trivial. Thus, a more precise definition would be + $$F(G) := \textstyle\prod_{\kappa \leq \card(G)} \Hom(L_\kappa,G),$$ + 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 + +tags: + - algebra + +related: [] + +satisfied_properties: + - property: continuous + proof: It is a product of representable functors. + +unsatisfied_properties: + - property: right adjoint + # TODO: refactor this once functor implications may have category equality assumptions + proof: 'If $F : \Grp \to \Set$ is right adjoint to $G : \Set \to \Grp$, then $F$ is representable with representing object $U := G(1)$. Let $u \in F(U)$ be a universal element, consisting of homomorphisms $u_\kappa : L_\kappa \to U$. Choose an infinite cardinal $\kappa > \card(U)$. Then $u_\kappa$ must be trivial. The set $F(L_\kappa) = \prod_{\lambda \leq \kappa} \Hom(L_\lambda,L_\kappa)$ contains the element $x$ whose $\kappa$-component is $\id_{L_\kappa}$ and all other components are trivial. Since $u \in F(U)$ is universal, there is a unique homomorphism $f : U \to L_\kappa$ such that $F(f)(u) = x$ in $F(L_\kappa)$. The $\kappa$-component of this equality is $f \circ u_\kappa = \id_{L_\kappa}$. Thus, $u_\kappa$ is injective, contradicting our previous observation that $u_\kappa$ is trivial and the fact that $L_\kappa$ is non-trivial.' + + # TODO: refactor this once functor implications may have category conclusions + # here: if a functor preserves terminal objects, and the domain is pointed, + # then the codomain is pointed as well. + - property: preserves initial objects + proof: The functor maps the trivial group to the singleton set, which is not initial. + + - property: preserves binary coproducts + proof: The canonical map $F(1) \sqcup F(1) \to F(1 \sqcup 1) = F(1)$ is not injective, since $F(1)$ has one element, whereas $F(1) \sqcup F(1)$ has two elements. + + - property: essentially injective + proof: Every finite group is mapped to a singleton set. + + - property: faithful + proof: If $G$ is a non-trivial finite group, the trivial homomorphism $G \to G$ and the identity of $G$ are mapped to the same map, because $F(G)$ is a singleton set. + + - property: dominant + proof: There is no group $G$ with a split monomorphism $\varnothing \to F(G)$, since $F(G)$ is not empty. In fact, using trivial homomorphisms $L_\kappa \to G$, we may regard $F(G)$ as a pointed set. + + - property: preserves epimorphisms + proof: >- + We first prove that if $G$ is a torsion-free group, then the pointed set $F(G)$ is trivial, i.e. a singleton set. In fact, our explicit choice $L_\kappa = \Alt_{\fin}(\kappa)$ implies that $L_\kappa$ is a filtered colimit of finite groups and is therefore a torsion group, which implies that every homomorphism $L_\kappa \to G$ is trivial. + + Now choose a free group $G$ that admits an epimorphism $G \to L_{\alpha_0}$. The induced map $F(G) \to F(L_{\alpha_0})$ is not an epimorphism, since otherwise $F(L_{\alpha_0})$ would be trivial, but $(\id_{L_{\alpha_0}},1,1,\dotsc)$ is a non-trivial element. + + - property: full + proof: 'We already mentioned that $F(G)$ can be regarded as a pointed set. Every homomorphism $G \to H$ induces a pointed map $F(G) \to F(H)$. (Thus, the functor should really be regarded as a functor to $\Set_*$, but in this entry, the codomain is $\Set$, which makes life easier.) Thus, it suffices to find a group $G$ with a non-pointed map $F(G) \to F(G)$, which of course exists as soon as $F(G)$ is non-trivial. But we already saw that each $F(L_\kappa)$ is non-trivial.' + + - property: finitary + proof: By our explicit choice of $L_{\aleph_0}$, it is a filtered colimit of finite groups $(\Alt(n))_{n \in \IN}$. But $F(L_{\aleph_0})$ is not the filtered colimit of the sets $F(\Alt(n))$, since these are singleton sets. diff --git a/database/data/functors/span_endpoints_inclusion.yaml b/database/data/functors/span_endpoints_inclusion.yaml new file mode 100644 index 000000000..95ede225d --- /dev/null +++ b/database/data/functors/span_endpoints_inclusion.yaml @@ -0,0 +1,36 @@ +id: span_endpoints_inclusion +name: span endpoints inclusion +notation: $E$ +domain: '2' +codomain: walking_span +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 + +tags: + - category theory + +related: [] + +satisfied_properties: + - property: fully faithful + proof: This is trivial. + + - property: continuous + proof: This follows from Lemma 2 here. + + - property: cocontinuous + proof: This follows from the dual of Lemma 2 here. + +unsatisfied_properties: + - property: dominant + proof: The object $0 \in \Span$ does not admit a split monomorphism to either $1$ or $2$. + + - property: left-invertible + proof: 'Assume that there is a functor $F : \Span \to \{1,2\}$ with $F(E(X)) \cong X$ for $X \in \{1,2\}$. Thus, $F(1) = 1$ and $F(2) = 2$. There are two possible choices for $F(0)$. Without loss of generality, assume that $F(0) = 1$. Then the morphism $0 \to 2$ in the walking span induces a morphism $1 = F(0) \to F(2) = 2$ in the discrete category, but no such morphism exists.' + + - property: right adjoint + proof: This follows from Corollary 4 here. + + - property: left adjoint + proof: This follows from the dual of Corollary 4 here. diff --git a/database/data/functors/trivial_BG.yaml b/database/data/functors/trivial_BG.yaml new file mode 100644 index 000000000..de3af6864 --- /dev/null +++ b/database/data/functors/trivial_BG.yaml @@ -0,0 +1,22 @@ +id: trivial_BG +name: trivial functor from the delooping +notation: $!_{BG}$ +domain: BG_f +codomain: '1' +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 finite group $G$. It is a basic example of a conservative functor which is not faithful.' +nlab_link: null +left_adjoint: null + +tags: + - algebra + +related: + - trivial_groups + - trivial_sets + - trivial_Idem + +satisfied_properties: [] + +unsatisfied_properties: + - property: faithful + proof: This is trivial. diff --git a/database/data/functors/trivial_Idem.yaml b/database/data/functors/trivial_Idem.yaml new file mode 100644 index 000000000..af27dd9bc --- /dev/null +++ b/database/data/functors/trivial_Idem.yaml @@ -0,0 +1,30 @@ +id: trivial_Idem +name: trivial functor from the walking idempotent +notation: $!_{\Idem}$ +domain: walking_idempotent +codomain: '1' +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 + +tags: + - category theory + +related: + - trivial_groups + - trivial_sets + - trivial_BG + +satisfied_properties: [] + +unsatisfied_properties: + - property: conservative + proof: The universal idempotent is mapped to an isomorphism, but is not an isomorphism. + + - property: left adjoint + # TODO: refactor this once functor implications support category conclusions + proof: A functor $1 \to \C$ which is right adjoint to $\Idem \to 1$ provides a terminal object in $\Idem$, which does not exist. + + - property: right adjoint + # TODO: refactor this once functor implications support category conclusions + proof: A functor $1 \to \C$ which is left adjoint to $\Idem \to 1$ provides an initial object in $\Idem$, which does not exist. diff --git a/database/data/functors/trivial_groups.yaml b/database/data/functors/trivial_groups.yaml index b26d6ea23..112e6d358 100644 --- a/database/data/functors/trivial_groups.yaml +++ b/database/data/functors/trivial_groups.yaml @@ -1,9 +1,9 @@ id: trivial_groups name: trivial functor from the category of groups -notation: $!$ +notation: $!_\Grp$ domain: Grp codomain: '1' -description: 'Every category $\C$ has a unique functor $! : \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.' +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 @@ -12,16 +12,10 @@ tags: related: - trivial_sets + - trivial_BG + - trivial_Idem -satisfied_properties: - - property: coreflector - proof: 'The constant functor $1 \to \Grp$ with value the trivial group is a left adjoint of $! : \Grp \to 1$ and fully faithful; this is because the trivial group is an initial object of $\Grp$.' - - - property: reflector - proof: 'The constant functor $1 \to \Grp$ with value the trivial group is a right adjoint of $! : \Grp \to 1$ and fully faithful; this is because the trivial group is a terminal object of $\Grp$.' - - - property: full - proof: This follows easily from the fact that $\Grp$ is strongly connected. +satisfied_properties: [] unsatisfied_properties: - property: essentially injective diff --git a/database/data/functors/trivial_sets.yaml b/database/data/functors/trivial_sets.yaml index adedbc556..aaa860557 100644 --- a/database/data/functors/trivial_sets.yaml +++ b/database/data/functors/trivial_sets.yaml @@ -1,9 +1,9 @@ id: trivial_sets name: trivial functor from the category of sets -notation: $!$ +notation: $!_\Set$ domain: Set codomain: '1' -description: 'Every category $\C$ has a unique functor $! : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of sets.' +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 @@ -12,13 +12,10 @@ tags: related: - trivial_groups + - trivial_BG + - trivial_Idem -satisfied_properties: - - property: coreflector - proof: 'The constant functor $1 \to \Set$ with value $\varnothing$ is a left adjoint of $! : \Set \to 1$ and fully faithful; this is because $\varnothing$ is an initial object of $\Set$.' - - - property: reflector - proof: 'The constant functor $1 \to \Set$ with value $\{\ast\}$ is a right adjoint of $! : \Set \to 1$ and fully faithful; this is because $\{\ast\}$ is a terminal object of $\Set$.' +satisfied_properties: [] unsatisfied_properties: - property: faithful diff --git a/database/data/functors/walking_isomorphism_object_inclusion.yaml b/database/data/functors/walking_isomorphism_object_inclusion.yaml index c19b93f57..8955508cb 100644 --- a/database/data/functors/walking_isomorphism_object_inclusion.yaml +++ b/database/data/functors/walking_isomorphism_object_inclusion.yaml @@ -15,9 +15,11 @@ related: [] satisfied_properties: - property: fully faithful proof: This is trivial. + check_redundancy: false - property: essentially surjective proof: The object $0$ is in the image, and the other object $1$ is isomorphic to $0$. + check_redundancy: false unsatisfied_properties: - property: isomorphism diff --git a/database/data/macros.yaml b/database/data/macros.yaml index c91031fe2..07245296e 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -36,6 +36,7 @@ \fp: \mathrm{fp} \ab: \mathrm{ab} \reg: \mathrm{reg} +\fin: \mathrm{fin} # operators \Mor: \operatorname{Mor} @@ -61,6 +62,7 @@ \cod: \operatorname{cod} \rank: \operatorname{rank} \Gal: \operatorname{Gal} +\Alt: \operatorname{Alt} # categories \Set: \mathbf{Set} diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index b305bee37..23cd445b2 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -452,7 +452,7 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri function insert_implications(implications: ImplicationYaml[]) { for (const impl of implications) { - if (!impl.assumptions.length) { + if (!impl.assumptions.length && !impl.mapped_assumptions) { console.error(`❌ Implication ${impl.id} has no assumptions.`) process.exit(1) } diff --git a/database/scripts/utils/implications.ts b/database/scripts/utils/implications.ts index 2d5f6a5a8..f48cfd039 100644 --- a/database/scripts/utils/implications.ts +++ b/database/scripts/utils/implications.ts @@ -6,16 +6,19 @@ import { type NormalizedImplication } from '$shared/implications' function get_assumption_string( implication: NormalizedImplication, properties_dict: Record, + type: StructureType, conditional = false ): string { const { assumptions } = implication - const own = Array.from(assumptions) - .map( - (assumption) => - `${properties_dict[assumption][conditional ? 'conditional_relation' : 'relation']} ${get_property_label(assumption)}` - ) - .join(' and ') + const own = assumptions.size + ? Array.from(assumptions) + .map( + (assumption) => + `${properties_dict[assumption][conditional ? 'conditional_relation' : 'relation']} ${get_property_label(assumption)}` + ) + .join(' and ') + : `is a ${type}` if (!implication.mapped_assumptions) return own @@ -44,10 +47,11 @@ export function get_proof_string( properties_dict: Record, type: StructureType ) { - const assumption_string = get_assumption_string(implication, properties_dict) + const assumption_string = get_assumption_string(implication, properties_dict, type) const conclusion_string = get_conclusion_string(implication, properties_dict) const ref = `by this result` + return `Since it ${assumption_string}, it ${conclusion_string} (${ref}).` } @@ -57,7 +61,12 @@ export function get_contradiction_string( property: string, type: StructureType ) { - const assumption_string = get_assumption_string(implication, properties_dict, true) + const assumption_string = get_assumption_string( + implication, + properties_dict, + type, + true + ) const conclusion_string = get_conclusion_string(implication, properties_dict, true) const has_multiple_assumptions = diff --git a/src/lib/server/fetchers/content.ts b/src/lib/server/fetchers/content.ts index 5b233684a..ae8204919 100644 --- a/src/lib/server/fetchers/content.ts +++ b/src/lib/server/fetchers/content.ts @@ -1,7 +1,9 @@ import type { PropertyShort, StructureShort } from '$lib/commons/types' import { db } from '$lib/server/db' -export function fetch_category_references(content_id: string) { +export function fetch_content_references(content_id: string) { + // TODO: make this more systematic + const categories = db .prepare<[string], StructureShort>( `SELECT DISTINCT s.id, s.name @@ -12,6 +14,16 @@ export function fetch_category_references(content_id: string) { ) .all(content_id) + const functors = db + .prepare<[string], StructureShort>( + `SELECT DISTINCT s.id, s.name + FROM property_assignments pa + INNER JOIN structures s ON s.id = pa.structure_id + WHERE pa.type = 'functor' + AND pa.proof LIKE '%/content/' || ? || '%'` + ) + .all(content_id) + const category_properties = db .prepare<[string], PropertyShort>( `SELECT id, relation FROM properties @@ -28,5 +40,5 @@ export function fetch_category_references(content_id: string) { ) .all(content_id) - return { categories, category_properties, category_implications } + return { categories, category_properties, category_implications, functors } } diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte index 57eed8c06..e6c4711d0 100644 --- a/src/pages/ImplicationPage.svelte +++ b/src/pages/ImplicationPage.svelte @@ -53,7 +53,7 @@ {/each}, {#if implication.is_equivalence} it - {:else} + {:else if implication.assumptions.length > 0} if it {/if} {:else if implication.is_equivalence} @@ -70,7 +70,7 @@ {/each}{#if implication.is_equivalence}  if and only if it {:else} - , then it + {#if implication.assumptions.length},{/if} then it {/if} {#each implication.conclusions as property, index} {property_relation_dict[type][property]} diff --git a/src/routes/content/[id]/+page.server.ts b/src/routes/content/[id]/+page.server.ts index a2c04ead0..76dce2d9c 100644 --- a/src/routes/content/[id]/+page.server.ts +++ b/src/routes/content/[id]/+page.server.ts @@ -1,6 +1,6 @@ import { get_rendered_content } from '$lib/server/markdown' import { error } from '@sveltejs/kit' -import { fetch_category_references } from '$lib/server/fetchers/content' +import { fetch_content_references } from '$lib/server/fetchers/content' export const load = (event) => { const id = event.params.id @@ -8,7 +8,7 @@ export const load = (event) => { const content = get_rendered_content(id) if (!content) error(404, 'Not Found') - const category_references = fetch_category_references(id) + const references = fetch_content_references(id) - return { ...content, ...category_references } + return { ...content, ...references } } diff --git a/src/routes/content/[id]/+page.svelte b/src/routes/content/[id]/+page.svelte index 3a91d9135..daacc7256 100644 --- a/src/routes/content/[id]/+page.svelte +++ b/src/routes/content/[id]/+page.svelte @@ -19,7 +19,9 @@

Authors: {data.meta_data.authors.join(', ')}

{/if} -{#if data.categories.length > 0 || data.category_properties.length > 0 || data.category_implications.length > 0} + + +{#if data.categories.length > 0 || data.category_properties.length > 0 || data.category_implications.length > 0 || data.functors.length > 0}

Context

{#if data.categories.length > 0} @@ -47,6 +49,12 @@ {/each} {/if} + + {#if data.functors.length > 0} +

This page is referenced by the following functors.

+ + + {/if} {/if}