diff --git a/.cspell.json b/.cspell.json index f8726064..df420421 100644 --- a/.cspell.json +++ b/.cspell.json @@ -100,6 +100,7 @@ "coquotients", "coreflection", "coreflective", + "coreflector", "coreflexive", "coreflexivity", "coregular", diff --git a/databases/catdat/data/functor-implications/adjoints.yaml b/databases/catdat/data/functor-implications/adjoints.yaml index abd14f5b..ba69f290 100644 --- a/databases/catdat/data/functor-implications/adjoints.yaml +++ b/databases/catdat/data/functor-implications/adjoints.yaml @@ -13,11 +13,20 @@ source: - cogenerating set - complete - - locally small + - locally essentially small - well-powered target: - - locally small + - locally essentially small conclusions: - right adjoint proof: This is the Special Adjoint Functor Theorem. The proof can be found, for example, at the nLab, or in Mac Lane, Ch. V, Theorem 8.2. is_equivalence: false + +- id: reflector_consequences + assumptions: + - reflector + conclusions: + - left adjoint + - 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 diff --git a/databases/catdat/data/functor-implications/equivalences.yaml b/databases/catdat/data/functor-implications/equivalences.yaml index c9f1916a..14c00525 100644 --- a/databases/catdat/data/functor-implications/equivalences.yaml +++ b/databases/catdat/data/functor-implications/equivalences.yaml @@ -1,18 +1,29 @@ - id: equivalence_criterion assumptions: - essentially surjective - - faithful - - full + - fully faithful conclusions: - equivalence proof: This is standard, see Mac Lane, Ch. IV, Theorem 4.1. is_equivalence: true +- id: equivalence_invertible + assumptions: + - equivalence + conclusions: + - left-invertible + - right-invertible + proof: >- + If a functor $F$ has a right inverse $R$ and a left inverse $L$, then + $$L \cong L \circ F \circ R \cong R.$$ + Hence, $R$ (and $L$) are (pseudo-)inverse to $F$. + is_equivalence: true + - id: equivalence_consequences assumptions: - equivalence conclusions: - monadic - - left-invertible + - reflector proof: This is easy. is_equivalence: false diff --git a/databases/catdat/data/functor-implications/limits preservation.yaml b/databases/catdat/data/functor-implications/limits preservation.yaml index ee9b91ea..60d46af6 100644 --- a/databases/catdat/data/functor-implications/limits preservation.yaml +++ b/databases/catdat/data/functor-implications/limits preservation.yaml @@ -132,3 +132,51 @@ - preserves monomorphisms proof: Any monomorphism in the domain is a regular monomorphism and is mapped to a regular monomorphism. is_equivalence: false + +- id: zero_preserving_condition + assumptions: + - preserves terminal objects + mapped_assumptions: + source: + - pointed + target: + - pointed + conclusions: + - preserves initial objects + proof: This is trivial. + is_equivalence: false + +- id: biproduct_preserving_condition + assumptions: + - preserves finite products + mapped_assumptions: + source: + - biproducts + target: + - biproducts + conclusions: + - preserves finite coproducts + proof: This is trivial. + is_equivalence: false + +- id: lift_implies_preservation + assumptions: + - lifts small limits + mapped_assumptions: + target: + - complete + conclusions: + - continuous + proof: 'Let $F : \C \to \D$ be the given functor and $X : \I \to \C$ be a small diagram. Since $\D$ is complete, the diagram $F \circ X$ has a limit cone. Since $F$ lifts small limits, there is a limit cone of $X$ which is mapped by $F$ to the limit cone of $F \circ X$. Hence, $F$ preserves this limit cone of $X$. Since any other limit cone of $X$ is isomorphic to it, the claim follows.' + is_equivalence: false + +- id: preservation_implies_lift + assumptions: + - continuous + mapped_assumptions: + source: + - complete + conclusions: + - lifts small limits + proof: 'Let $F : \C \to \D$ be the given functor and $X : \I \to \C$ be a small diagram such that $F \circ X$ has a limit cone. By assumption, $X$ has a limit cone, and $F$ maps it to a limit cone of $F \circ X$. But then the image must be isomorphic to the given limit cone.' + is_equivalence: false diff --git a/databases/catdat/data/functor-implications/misc.yaml b/databases/catdat/data/functor-implications/misc.yaml index bed2217c..e3d52935 100644 --- a/databases/catdat/data/functor-implications/misc.yaml +++ b/databases/catdat/data/functor-implications/misc.yaml @@ -1,3 +1,12 @@ +- id: fully-faithful-definition + assumptions: + - full + - faithful + conclusions: + - fully faithful + proof: This holds by definition. + is_equivalence: true + - id: faithful-via-equalizers assumptions: - conservative @@ -12,8 +21,7 @@ - id: conservative_consequences assumptions: - - full - - faithful + - fully faithful conclusions: - conservative proof: If $F(f)$ is an isomorphism, its inverse has the form $F(g)$ since $F$ is full. Since $F$ is faithful, it follows that $f$ is inverse to $g$. @@ -35,5 +43,13 @@ - faithful - essentially injective - conservative - proof: 'Let $G : \D \to \C$ be a left-inverse to $F : \C \to \D$, meaning that $G \circ F \cong \id_{\C}$. Then $F(A) \cong F(B)$ implies $A \cong G(F(A)) \cong G(F(B)) \cong B$ for all $A,B \in \C$. Thus, $F$ essentially injective. Moreover, since $G \circ F$ is faithful, the composed map $\Hom(A,B) \to \Hom(F(A),F(B)) \to \Hom(G(F(A)),G(F(B))$ is injective, so that also $\Hom(A,B) \to \Hom(F(A),F(B))$ is injective. This shows that $F$ is faithful. Finally, if $f : A \to B$ is am morphism such that $F(f)$ is an isomorphism, then $G(F(f))$ is an isomorphism. Since $G(F(f)) \cong f$ in $\Mor(\C)$, we conclude that $f$ is an isomorphism. Therefore, $F$ is conservative.' + proof: 'Let $G : \D \to \C$ be a left-inverse to $F : \C \to \D$, meaning that $G \circ F \cong \id_{\C}$. Then $F(A) \cong F(B)$ implies $A \cong G(F(A)) \cong G(F(B)) \cong B$ for all $A,B \in \C$. Thus, $F$ essentially injective. Moreover, since $G \circ F$ is faithful, the composed map $\Hom(A,B) \to \Hom(F(A),F(B)) \to \Hom(G(F(A)),G(F(B))$ is injective, so that also $\Hom(A,B) \to \Hom(F(A),F(B))$ is injective. This shows that $F$ is faithful. Finally, if $f : A \to B$ is a morphism such that $F(f)$ is an isomorphism, then $G(F(f))$ is an isomorphism. Since $G(F(f)) \cong f$ in $\Mor(\C)$, we conclude that $f$ is an isomorphism. Therefore, $F$ is conservative.' + is_equivalence: false + +- id: right-invertible_consequences + assumptions: + - right-invertible + conclusions: + - essentially surjective + proof: This is trivial. is_equivalence: false diff --git a/databases/catdat/data/functor-implications/monadic.yaml b/databases/catdat/data/functor-implications/monadic.yaml index e10fe05e..8de8f0fe 100644 --- a/databases/catdat/data/functor-implications/monadic.yaml +++ b/databases/catdat/data/functor-implications/monadic.yaml @@ -20,3 +20,11 @@ - monadic proof: This is the crude monadicity theorem. A proof can be found in Mac Lane & Moerdijk, Thm. IV.4.2. is_equivalence: false + +- id: monadic_lift_limits + assumptions: + - monadic + conclusions: + - lifts small limits + proof: 'See Joy of Cats, Prop. 20.12.' + is_equivalence: false diff --git a/databases/catdat/data/functor-properties/cocontinuous.yaml b/databases/catdat/data/functor-properties/cocontinuous.yaml index 54ea6f3e..5eee49fa 100644 --- a/databases/catdat/data/functor-properties/cocontinuous.yaml +++ b/databases/catdat/data/functor-properties/cocontinuous.yaml @@ -10,3 +10,4 @@ related_properties: - left adjoint - preserves coequalizers - finitary + - lifts small colimits diff --git a/databases/catdat/data/functor-properties/continuous.yaml b/databases/catdat/data/functor-properties/continuous.yaml index 4739d6cf..2f2cca28 100644 --- a/databases/catdat/data/functor-properties/continuous.yaml +++ b/databases/catdat/data/functor-properties/continuous.yaml @@ -10,3 +10,4 @@ related_properties: - right adjoint - preserves equalizers - cofinitary + - lifts small limits diff --git a/databases/catdat/data/functor-properties/coreflector.yaml b/databases/catdat/data/functor-properties/coreflector.yaml new file mode 100644 index 00000000..113cabf7 --- /dev/null +++ b/databases/catdat/data/functor-properties/coreflector.yaml @@ -0,0 +1,9 @@ +id: coreflector +relation: is a +description: 'A functor $F : \C \to \D$ is a coreflector if it is right adjoint to a functor $G : \D \to \C$ which is fully faithful. Hence, $G$ is equivalent to the inclusion of a full coreflective subcategory. The condition that $G$ is fully faithful can also be expressed by the condition that the counit $\eta : \id_{\D} \to F \circ G$ is an isomorphism (Prop. 3.4 at the nLab).' +nlab_link: https://ncatlab.org/nlab/show/coreflective+subcategory +invariant_under_equivalences: true +dual_property: reflector +related_properties: + - right adjoint + - right-invertible diff --git a/databases/catdat/data/functor-properties/faithful.yaml b/databases/catdat/data/functor-properties/faithful.yaml index 2dc054aa..f50df43f 100644 --- a/databases/catdat/data/functor-properties/faithful.yaml +++ b/databases/catdat/data/functor-properties/faithful.yaml @@ -7,5 +7,6 @@ dual_property: faithful related_properties: - equivalence - full + - fully faithful - essentially injective - left-invertible diff --git a/databases/catdat/data/functor-properties/full.yaml b/databases/catdat/data/functor-properties/full.yaml index c7747d34..74cee52c 100644 --- a/databases/catdat/data/functor-properties/full.yaml +++ b/databases/catdat/data/functor-properties/full.yaml @@ -7,4 +7,5 @@ dual_property: full related_properties: - equivalence - faithful + - fully faithful - essentially injective diff --git a/databases/catdat/data/functor-properties/fully faithful.yaml b/databases/catdat/data/functor-properties/fully faithful.yaml new file mode 100644 index 00000000..37a55bfa --- /dev/null +++ b/databases/catdat/data/functor-properties/fully faithful.yaml @@ -0,0 +1,10 @@ +id: fully faithful +relation: is +description: 'A functor is fully faithful when it is full and faithful. This means that for all objects $A,B$ in its domain the map $\Hom(A,B) \to \Hom(F(A),F(B))$, $f \mapsto F(f)$ is a bijection.' +nlab_link: https://ncatlab.org/nlab/show/full+and+faithful+functor +invariant_under_equivalences: true +dual_property: fully faithful +related_properties: + - full + - faithful + - equivalence diff --git a/databases/catdat/data/functor-properties/left adjoint.yaml b/databases/catdat/data/functor-properties/left adjoint.yaml index 810f29cb..c2675966 100644 --- a/databases/catdat/data/functor-properties/left adjoint.yaml +++ b/databases/catdat/data/functor-properties/left adjoint.yaml @@ -7,3 +7,4 @@ dual_property: right adjoint related_properties: - cocontinuous - comonadic + - reflector diff --git a/databases/catdat/data/functor-properties/left-invertible.yaml b/databases/catdat/data/functor-properties/left-invertible.yaml index 081bb50d..82282809 100644 --- a/databases/catdat/data/functor-properties/left-invertible.yaml +++ b/databases/catdat/data/functor-properties/left-invertible.yaml @@ -1,6 +1,6 @@ id: left-invertible relation: is -description: 'A left inverse of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $G \circ F \cong \id_{\C}$. We do not require $G \circ F = \id_{\C}$ here, which is often too strict. A functor is called left-invertible when it has a left inverse.' +description: 'A left inverse of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $G \circ F \cong \id_{\C}$. We do not require $G \circ F = \id_{\C}$ here, which is often too strict. A functor is called left-invertible when it has a left inverse. This notion is self-dual in the sense that $F : \C \to \D$ is left-invertible iff $F^{\op} : \C^{\op} \to \D^{\op}$ is left-invertible.' nlab_link: https://ncatlab.org/nlab/show/inverse+functor invariant_under_equivalences: true dual_property: left-invertible @@ -8,3 +8,4 @@ related_properties: - equivalence - faithful - essentially injective + - right-invertible diff --git a/databases/catdat/data/functor-properties/lifts small colimits.yaml b/databases/catdat/data/functor-properties/lifts small colimits.yaml new file mode 100644 index 00000000..5464f27d --- /dev/null +++ b/databases/catdat/data/functor-properties/lifts small colimits.yaml @@ -0,0 +1,8 @@ +id: lifts small colimits +relation: '' +description: 'A functor $F : \C \to \D$ lifts small colimits when for every small diagram $X : \I \to \C$ and every every colimit cocone of $F \circ X$ there is a colimit cocone of $X$ that is mapped by $F$ to the given colimit cocone of $F \circ X$.' +nlab_link: https://ncatlab.org/nlab/show/lifted+limit +invariant_under_equivalences: true +dual_property: lifts small limits +related_properties: + - cocontinuous diff --git a/databases/catdat/data/functor-properties/lifts small limits.yaml b/databases/catdat/data/functor-properties/lifts small limits.yaml new file mode 100644 index 00000000..e8db2f74 --- /dev/null +++ b/databases/catdat/data/functor-properties/lifts small limits.yaml @@ -0,0 +1,8 @@ +id: lifts small limits +relation: '' +description: 'A functor $F : \C \to \D$ lifts small limits when for every small diagram $X : \I \to \C$ and every every limit cone of $F \circ X$ there is a limit cone of $X$ that is mapped by $F$ to the given limit cone of $F \circ X$.' +nlab_link: https://ncatlab.org/nlab/show/lifted+limit +invariant_under_equivalences: true +dual_property: lifts small colimits +related_properties: + - continuous diff --git a/databases/catdat/data/functor-properties/reflector.yaml b/databases/catdat/data/functor-properties/reflector.yaml new file mode 100644 index 00000000..f631e50a --- /dev/null +++ b/databases/catdat/data/functor-properties/reflector.yaml @@ -0,0 +1,9 @@ +id: reflector +relation: is a +description: 'A functor $F : \C \to \D$ is a reflector if it is left adjoint to a functor $G : \D \to \C$ which is fully faithful. Hence, $G$ is equivalent to the inclusion of a full reflective subcategory. The condition that $G$ is fully faithful can also be expressed by the condition that the counit $\varepsilon : F \circ G \to \id_{\D}$ is an isomorphism (Prop. 3.4 at the nLab).' +nlab_link: https://ncatlab.org/nlab/show/reflective+subcategory +invariant_under_equivalences: true +dual_property: coreflector +related_properties: + - left adjoint + - right-invertible diff --git a/databases/catdat/data/functor-properties/representable.yaml b/databases/catdat/data/functor-properties/representable.yaml index bec89ed0..e5ec76db 100644 --- a/databases/catdat/data/functor-properties/representable.yaml +++ b/databases/catdat/data/functor-properties/representable.yaml @@ -3,6 +3,5 @@ relation: is description: 'A functor $F : \C \to \D$ is representable if $\C$ is locally small, $\D = \Set$, and there is an object $A \in \C$ with $F \cong \Hom(A,-)$.' nlab_link: https://ncatlab.org/nlab/show/representable+functor invariant_under_equivalences: true -dual_property: null related_properties: - continuous diff --git a/databases/catdat/data/functor-properties/right-invertible.yaml b/databases/catdat/data/functor-properties/right-invertible.yaml new file mode 100644 index 00000000..b5a8c90e --- /dev/null +++ b/databases/catdat/data/functor-properties/right-invertible.yaml @@ -0,0 +1,11 @@ +id: right-invertible +relation: is +description: 'A right inverse of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $F \circ G \cong \id_{\D}$. We do not require $F \circ G = \id_{\D}$ here, which is often too strict. A functor is called right-invertible when it has a right inverse. This notion is self-dual in the sense that $F : \C \to \D$ is right-invertible iff $F^{\op} : \C^{\op} \to \D^{\op}$ is right-invertible.' +nlab_link: https://ncatlab.org/nlab/show/inverse+functor +invariant_under_equivalences: true +dual_property: right-invertible +related_properties: + - equivalence + - essentially surjective + - left-invertible + - reflector diff --git a/databases/catdat/data/functors/abelianization.yaml b/databases/catdat/data/functors/abelianization.yaml index d6b54547..c79996e5 100644 --- a/databases/catdat/data/functors/abelianization.yaml +++ b/databases/catdat/data/functors/abelianization.yaml @@ -13,11 +13,8 @@ tags: related_functors: [] satisfied_properties: - - property: left adjoint - proof: This functor is left adjoint to the forgetful functor. - - - property: essentially surjective - proof: For abelian groups $G$ we have $G \cong G^{\ab}$. + - property: reflector + proof: 'This functor is left adjoint to the forgetful functor $U_{\Ab,\Grp} : \Ab \hookrightarrow \Grp$, which is fully faithful.' - property: preserves finite products proof: See MO/386144. diff --git a/databases/catdat/data/functors/coproduct_sets.yaml b/databases/catdat/data/functors/coproduct_sets.yaml index e51c2c75..a45400c5 100644 --- a/databases/catdat/data/functors/coproduct_sets.yaml +++ b/databases/catdat/data/functors/coproduct_sets.yaml @@ -3,7 +3,7 @@ name: binary coproduct functor on sets notation: $+$ source: SetxSet target: Set -description: This functor maps a pair of sets $(X,Y)$ to their coproduct $X + Y$. +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 tags: @@ -14,8 +14,8 @@ related_functors: - product_sets satisfied_properties: - - property: essentially surjective - proof: We have $X \cong X + 0$. + - property: right-invertible + proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,0)$ provides a right inverse since $X + 0 \cong X$. - property: preserves equalizers proof: This can be checked with a straight forward calculation. @@ -37,3 +37,6 @@ unsatisfied_properties: - property: essentially injective proof: Both $(1,0)$ and $(0,1)$ are mapped to $1$. + + - property: reflector + proof: 'Its right adjoint, the diagonal functor $\Delta : X \to X \times X$, is faithful, but not full.' diff --git a/databases/catdat/data/functors/discrete_topology.yaml b/databases/catdat/data/functors/discrete_topology.yaml index c58f9b30..62746944 100644 --- a/databases/catdat/data/functors/discrete_topology.yaml +++ b/databases/catdat/data/functors/discrete_topology.yaml @@ -10,7 +10,8 @@ tags: - topology - free -related_functors: [] +related_functors: + - indiscrete_topology satisfied_properties: - property: left adjoint diff --git a/databases/catdat/data/functors/enveloping_group.yaml b/databases/catdat/data/functors/enveloping_group.yaml index f11b97ae..05451be8 100644 --- a/databases/catdat/data/functors/enveloping_group.yaml +++ b/databases/catdat/data/functors/enveloping_group.yaml @@ -14,11 +14,8 @@ related_functors: - free_group satisfied_properties: - - property: left adjoint - proof: 'By definition, this functor is left adjoint to the forgetful functor $U_{\Grp,\Mon} : \Grp \to \Mon$.' - - - property: essentially surjective - proof: 'In fact, the counit of the adjunction $F \circ U_{\Grp,\Mon} \to \id_{\Grp}$ is an isomorphism since the right adjoint $U_{\Grp,\Mon}$ is fully faithful (Prop. 3.4 at the nLab).' + - property: reflector + proof: 'By definition, this functor is left adjoint to the forgetful functor $U_{\Grp,\Mon} : \Grp \hookrightarrow \Mon$, which is fully faithful.' - property: preserves finite products proof: >- diff --git a/databases/catdat/data/functors/forget_abelian.yaml b/databases/catdat/data/functors/forget_abelian.yaml index 92a87387..4b8ca4bb 100644 --- a/databases/catdat/data/functors/forget_abelian.yaml +++ b/databases/catdat/data/functors/forget_abelian.yaml @@ -25,9 +25,6 @@ satisfied_properties: - property: left-invertible proof: The abelianization functor $\Grp \to \Ab$, $G \mapsto G^{\ab}$ provides a left inverse. - - property: preserves initial objects - proof: The trivial group is initial in both $\Ab$ and $\Grp$. - - property: preserves coequalizers proof: 'This follows from the concrete construction of coequalizers, but it can also be proven as follows: Assume that $f,g : A \rightrightarrows B$ have coequalizer $p : B \to C$ in $\Ab$. If $G$ is any group and $h : B \to G$ is a homomorphism with $hf = hg$, consider the image factorization $h = i h''$ of $h$. We have $h'' f = h'' g$, and the image $\im(h)$ is abelian. Hence, there is a unique homomorphism $k : C \to \im(h)$ with $kp = h''$. Hence, $ik : C \to G$ satisfies $ikp = h$. Uniqueness follows since we already know that the forgetful functor is preserves epimorphisms.' diff --git a/databases/catdat/data/functors/forget_group.yaml b/databases/catdat/data/functors/forget_group.yaml index 312a9cf5..605349e4 100644 --- a/databases/catdat/data/functors/forget_group.yaml +++ b/databases/catdat/data/functors/forget_group.yaml @@ -15,6 +15,7 @@ related_functors: - forget_vector - forget_ring - forget_abelian + - forget_group_pointed satisfied_properties: - property: representable diff --git a/databases/catdat/data/functors/forget_group_pointed.yaml b/databases/catdat/data/functors/forget_group_pointed.yaml new file mode 100644 index 00000000..711dd788 --- /dev/null +++ b/databases/catdat/data/functors/forget_group_pointed.yaml @@ -0,0 +1,44 @@ +id: forget_group_pointed +name: forgetful functor from groups to pointed sets +notation: $U_{\Grp,\Set_*}$ +source: Grp +target: Set* +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 + +tags: + - algebra + - forgetful + +related_functors: + - forget_group + - forget_inverses + +satisfied_properties: + - property: right adjoint + proof: A left adjoint can be constructed by mapping a pointed set $(X,x_0)$ to the free group $F(X)$ modulo $x_0 = 1$. + + - property: conservative + proof: 'We already know that the forgetful functor $U_{\Grp} : \Grp \to \Set$ is conservative.' + + - property: finitary + proof: 'Since the forgetful functor $U_{\Set_*} : \Set_* \to \Set$ is finitary and conservative, it suffices to prove that the composition $U_{\Set_*} \circ U_{\Grp,\Set_*} : \Grp \to \Set_*$ is finitary. This is just the forgetful functor $U_{\Grp} : \Grp \to \Set$ and therefore finitary.' + + - property: preserves reflexive coequalizers + proof: 'It suffices to prove that $U_{\Grp} : \Grp \to \Set$ preserves them, which follows from Theorem 2.5 at the nLab.' + + - property: preserves epimorphisms + proof: This follows from the classifications of epimorphisms in $\Grp$ and in $\Set_*$. + + - property: essentially surjective + proof: Let $(X,x_0)$ be a pointed set. If $X$ is finite, we can endow $X$ with a cyclic group structure in which $x_0$ is the identity element. If $X$ is infinite, there is a bijection between $X$ and the set $P_{<\aleph_0}(X)$ of finite subsets of $X$, and we may assume that $x_0$ is mapped to $\varnothing$. Since $P_{<\aleph_0}(X)$ carries a group structure with identity element $\varnothing$ (it is the underlying set of $\IF_2^{\oplus X}$), it follows that $X$ also carries a group structure with identity element $x_0$. + +unsatisfied_properties: + - property: essentially injective + proof: This is trivial. + + - property: preserves coequalizers + proof: 'The coequalizer of $1,2 : \IZ \rightrightarrows \IZ$ is the trivial group in $\Grp$, but the coequalizer of these maps in $\Set_*$ is infinite.' + + - property: right-invertible + proof: 'Assume that there is a functor $G : \Set_* \to \Grp$ with $U \circ G \cong \id_{\Set_*}$, where $U : \Grp \to \Set_*$ is the forgetful functor. By using transport of structure, we can even assume that $U \circ G = \id_{\Set_*}$. Consider the set $X = \{x_0,x_1,x_2\}$ and the pointed set $(X,x_0)$. It carries a group structure with identity element $x_0$ such that every pointed map $(X,x_0) \to (X,x_0)$ is a group homomorphism (namely, its image under $G$). A group of order $3$ is isomorphic to $C_3$. If $t$ is a generator of $C_3$, then the map $U(C_3) \to U(C_3)$, $1 \mapsto 1$, $t \mapsto t$, $t^2 \mapsto t$ is pointed, but not a group homomorphism.' diff --git a/databases/catdat/data/functors/forget_inverses.yaml b/databases/catdat/data/functors/forget_inverses.yaml index b96f8acf..2b208d6e 100644 --- a/databases/catdat/data/functors/forget_inverses.yaml +++ b/databases/catdat/data/functors/forget_inverses.yaml @@ -12,7 +12,9 @@ tags: - forgetful related_functors: + - forget_group - forget_abelian + - forget_group_pointed satisfied_properties: - property: full diff --git a/databases/catdat/data/functors/forget_topology.yaml b/databases/catdat/data/functors/forget_topology.yaml index f129178b..52375112 100644 --- a/databases/catdat/data/functors/forget_topology.yaml +++ b/databases/catdat/data/functors/forget_topology.yaml @@ -11,20 +11,24 @@ tags: - topology - forgetful -related_functors: [] +related_functors: + - pi_0 + +comments: + - This functor has exactly two right inverses (up to isomorphism), see MSE/4368730. satisfied_properties: - property: faithful proof: This is trivial. - - property: representable - proof: This functor is represented by the singleton space. + - property: reflector + proof: 'The indiscrete topology defines a fully faithful functor $I : \Set \to \Top$ which is right adjoint to $U_{\Top}$.' - - property: essentially surjective - proof: Every set can be equipped with the discrete topology. + - property: coreflector + proof: 'The discrete topology defines a fully faithful functor $D : \Set \to \Top$ which is left adjoint to $U_{\Top}$.' - - property: left adjoint - proof: 'The indiscrete topology defines a functor $I : \Set \to \Top$ which is right adjoint to $U_{\Top}$.' + - property: representable + proof: This functor is represented by the singleton space. unsatisfied_properties: - property: essentially injective diff --git a/databases/catdat/data/functors/group_units.yaml b/databases/catdat/data/functors/group_units.yaml index c223cba4..8a7d05ae 100644 --- a/databases/catdat/data/functors/group_units.yaml +++ b/databases/catdat/data/functors/group_units.yaml @@ -13,11 +13,8 @@ tags: related_functors: [] satisfied_properties: - - property: essentially surjective - proof: If $G$ is a group, then $G$ is isomorphic to its group of units. - - - property: right adjoint - proof: This functor is right adjoint to the forgetful functor $\Grp \to \Mon$. + - property: coreflector + proof: 'This functor is right adjoint to the forgetful functor $U_{\Grp,\Mon} : \Grp \hookrightarrow \Mon$, which is fully faithful.' - property: finitary proof: 'There is a direct way to prove this, but here is an abstract argument: Since the forgetful functor $\Grp \to \Set$ is conservative and finitary, it suffices to prove that the composition $\Mon \to \Set$, which maps a monoid to its set of units, is finitary. This functor is represented by the monoid $\langle x,y : xy = yx = 1 \rangle \cong \IZ$. It has a finite presentation and hence is finitely presentable in the categorical sense (Corollary 3.13 in Adamek-Rosicky).' diff --git a/databases/catdat/data/functors/indiscrete_topology.yaml b/databases/catdat/data/functors/indiscrete_topology.yaml new file mode 100644 index 00000000..93b2d381 --- /dev/null +++ b/databases/catdat/data/functors/indiscrete_topology.yaml @@ -0,0 +1,40 @@ +id: indiscrete_topology +name: indiscrete topology functor +notation: $I$ +source: Set +target: Top +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 + +tags: + - topology + +related_functors: + - discrete_topology + +satisfied_properties: + - property: full + proof: This is trivial. + + - property: preserves initial objects + proof: This is obvious. + + - property: right adjoint + proof: 'This functor is right adjoint to the forgetful functor $U_{\Top} : \Top \to \Set$.' + + - property: left-invertible + proof: The forgetful functor provides a left inverse. + + - property: preserves coequalizers + proof: 'This follows easily from the description of coequalizers in $\Set$ and $\Top$, and the fact that if $p : X \to Y$ is a surjective map, then $I(p) : I(X) \to I(Y)$ is a quotient map.' + + - property: finitary + proof: >- + Let $X$ be a filtered diagram of sets. We need to prove that the filtered colimit of spaces $\colim_i I(X_i)$ is indiscrete. If $X_i$ is empty for all $i$, this is trivial. Otherwise, by considering a slice of the index category, we may assume that every $X_i$ is non-empty. A topological space $Y$ is indiscrete iff there are at most two continuous maps $Y \to S$, where $S$ is the Sierpinski space; there are exactly two when $Y$ is non-empty. We have + $$\textstyle \Hom(\colim_i I(X_i),S) \cong \lim_i \Hom(I(X_i),S) \cong \lim_i \{\varnothing, X_i\}.$$ + For every $i \to j$ the map $I(X_i) \to I(X_j)$ pulls back $\varnothing \mapsto \varnothing$ and $X_j \mapsto X_i$. Thus, the limit has exactly two elements. + +unsatisfied_properties: + - property: preserves finite coproducts + proof: If $X$ and $Y$ are two non-empty sets, the canonical continuous bijection $I(X) + I(Y) \to I(X + Y)$ is not an isomorphism since $I(X) + I(Y)$ is not indiscrete as witnessed by the open subset $X$. diff --git a/databases/catdat/data/functors/p-torsion.yaml b/databases/catdat/data/functors/p-torsion.yaml index a719682b..3b114583 100644 --- a/databases/catdat/data/functors/p-torsion.yaml +++ b/databases/catdat/data/functors/p-torsion.yaml @@ -20,9 +20,6 @@ satisfied_properties: - property: right adjoint proof: 'This functor is clearly right adjoint to $A \mapsto A/pA$.' - - property: preserves coproducts - proof: This is easy to check using the description of coproducts as direct sums. - - property: finitary proof: >- This follows abstractly from the fact that $\IZ/p$ is finitely presentable. We nevertheless give a direct proof. Let $(A_i)$ be a filtered diagram of abelian groups. We need to show that the canonical map diff --git a/databases/catdat/data/functors/pi_0.yaml b/databases/catdat/data/functors/pi_0.yaml new file mode 100644 index 00000000..8cc5c56f --- /dev/null +++ b/databases/catdat/data/functors/pi_0.yaml @@ -0,0 +1,67 @@ +id: pi_0 +name: path components functor +notation: $\pi_0$ +source: Top +target: Set +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 + +tags: + - topology + +related_functors: + - forget_topology + +satisfied_properties: + - property: preserves products + proof: See nLab. + + - property: preserves coproducts + proof: See nLab. + + - property: right-invertible + proof: 'The discrete topology functor $D : \Set \to \Top$ satisfies $\pi_0(D(X)) \cong X$.' + + - property: preserves epimorphisms + proof: If $X \to Y$ is an epimorphism in $\Top$, this means that $U(X) \to U(Y)$ is surjective. Hence, also $X/{\sim} = \pi_0(X) \to \pi_0(Y) = Y/{\sim}$ is surjective. + +unsatisfied_properties: + - property: conservative + proof: 'Any map $\{\ast\} \to [0,1]$ induces an isomorphism $\pi_0(\{\ast\}) \to \pi_0([0,1])$ but is not an isomorphism itself.' + + - property: faithful + proof: 'The two continuous maps $0,1 : \{\ast\} \rightrightarrows [0,1]$ have the same image under $\pi_0$.' + + - property: full + proof: 'Take two totally disconnected spaces $X,Y$ which admit a map $f : U(X) \to U(Y)$ that is not continuous, for example $X = Y = \IQ$ with the usual topology, $f(0)=1$ and $f(x)=0$ for $x \neq 0$. Then $f$ induces a map $\pi_0(X) \cong U(X) \to U(Y) \cong \pi_0(Y)$ that is not induced by a continuous map $X \to Y$.' + + - property: essentially injective + proof: We have $\pi_0(\{\ast\}) \cong \pi_0([0,1])$, but $\{\ast\} \not\cong [0,1]$. + + - property: preserves monomorphisms + proof: The functor $\pi_0$ maps the embedding $\{0,1\} \hookrightarrow [0,1]$ to the (unique) map $\{\{0\},\{1\}\} \to \{[0,1]\}$, which is not injective. + + - property: preserves coequalizers + proof: >- + Let $X \subseteq \IR^2$ be the closed topologist's sine curve defined by $X = S \cup L$, where + $$\begin{align*} + S & \coloneqq \{(x,\sin(1/x)) : 0 < x \leq 1 \} \\ + L & \coloneqq \{(0,y) : y \in [-1,+1] \} + \end{align*}$$ + It is known that $X$ is connected, but not path connected. Its path components are $\pi_0(X) = \{S,L\}$. + + Now let $p : X \to Y$ be the quotient map which collapses $L$ to a point $y_0 \in Y$. Then $p$ is the coequalizer of the two projections $q_1,q_2 : E \rightrightarrows X$, where $E \coloneqq X \times_Y X = \{(x,x') \in X \times X : p(x) = p(x')\}$. + + We claim that $Y$ is path connected. In fact, it is easy to check that the map + $$\gamma : [0,1] \to Y, ~ \gamma(t) \coloneqq \begin{cases} p(1-t, \sin(1/(1-t)) & t < 1 \\ y_0 & t = 1 \end{cases}$$ + is continuous and satisfies $\gamma(0)=p(1,\sin(1))$ and $\gamma(1) = y_0$. Thus, $\pi_0(Y) = \{Y\}$. In other words, $\pi_0(\coeq(q_1,q_2))$ has exactly one element. We will see next that $\coeq(\pi_0(q_1),\pi_0(q_2))$ has two elements, which will prove that $\pi_0$ does not preserve coequalizers. + + As a set, $E$ decomposes into $E = \Delta_S \cup (L \times L)$, where $\Delta_S$ is the diagonal of $S$. Both $\Delta_S$ and $L \times L$ are path connected. Moreover, there is no path from a point in $\Delta_S$ to a point in $L \times L$, since its image under $q_1$ would be a path in $X$ from a point in $S$ to a point in $L$, which does not exist. Thus, $\pi_0(E) = \{\Delta_S, L \times L\}$. + + The map $\pi_0(q_1) : \pi_0(E) \to \pi_0(X)$ sends the path component $\Delta_S$ to $S$ and the path component $L \times L$ to $L$. The map $\pi_0(q_2)$ has exactly the same description. Hence, their coequalizer is just $\pi_0(X)$, which has two elements. + + - property: cofinitary + proof: 'Consider the spaces $X_n = [n,\infty) \subseteq \IR$ and the inclusion maps $X_{n+1} \hookrightarrow X_n$. Then $\lim_n X_n = \varnothing$ and hence $\pi_0(\lim_n X_n) = \varnothing$. However, each $\pi_0(X_n) = \{X_n\}$ is a singleton, so that also $\lim_n \pi_0(X_n)$ is a singleton.' + + - property: finitary + proof: 'Let $A_n = \{1/k : k \geq n\}$ for $n \geq 1$. Let $X_n$ be the interval $[0,1]$ equipped with the topology generated by the Euclidean topology and all the singletons $\{a\}$ for $a \in A_n$. The identity maps $X_n \to X_{n+1}$ are continuous since $A_{n+1} \subseteq A_n$, and we have continuous identity maps $X_n \to [0,1]$. Using $\bigcap_{n \geq 1} A_n = \varnothing$, one can show that $\operatorname{colim}_n X_n = [0,1]$ with the Euclidean topology, which is path connected. In particular, $[0]=[1]$ in $\pi_0(\operatorname{colim}_n X_n)$. However, this equation does not hold in $\operatorname{colim}_n \pi_0(X_n)$. Otherwise, there is some $n$ such that it holds in $\pi_0(X_n)$, i.e. there is a path $\gamma : [0,1] \to X_n$ with $\gamma(0)=0$ and $\gamma(1)=1$. By the intermediate value theorem applied to the composition with the map $X_n \to [0,1]$, the element $1/n$ lies in its image. But $\{1/n\}$ is open and closed in $X_n$. Hence, its preimage is $[0,1]$, which means that the path is constant. This is a contradiction.' diff --git a/databases/catdat/data/functors/product_sets.yaml b/databases/catdat/data/functors/product_sets.yaml index 0e7e1958..5de7318c 100644 --- a/databases/catdat/data/functors/product_sets.yaml +++ b/databases/catdat/data/functors/product_sets.yaml @@ -3,7 +3,7 @@ name: binary product functor on sets notation: $\times$ source: SetxSet target: Set -description: This functor maps a pair of sets $(X,Y)$ to their product $X \times Y$. +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 @@ -15,8 +15,8 @@ related_functors: - coproduct_sets satisfied_properties: - - property: essentially surjective - proof: We have $X \cong X \times 1$. + - property: right-invertible + proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,1)$ provides a right inverse since $X \times 1 \cong X$. - property: preserves initial objects proof: This is obvious. @@ -47,3 +47,6 @@ unsatisfied_properties: - property: preserves coequalizers proof: 'Since the diagonal functor $\Delta : \Set \to \Set \times \Set$ preserves coequalizers (in fact, all colimits), it would follow that the composition $\Set \to \Set$, $X \mapsto X^2$ preserves coequalizers. But this is the squaring functor, from we already know that it does not preserve coequalizers.' + + - property: coreflector + proof: 'Its left adjoint, the diagonal functor $\Delta : X \to X \times X$, is faithful, but not full.' diff --git a/databases/catdat/data/functors/torsion.yaml b/databases/catdat/data/functors/torsion.yaml index 289a7e4d..9a27dea2 100644 --- a/databases/catdat/data/functors/torsion.yaml +++ b/databases/catdat/data/functors/torsion.yaml @@ -14,12 +14,8 @@ related_functors: - p-torsion satisfied_properties: - - property: preserves coproducts - proof: This is easy to check using the description of coproducts as direct sums. - - property: preserves finite products - # TODO: automate this with an implication - proof: Finite products coincide with finite direct sums. + proof: This is easy. - property: preserves equalizers proof: 'Let $E \subseteq A$ be the equalizer of two homomorphisms $f,g : A \rightrightarrows B$. If $a \in T(A)$ is equalized by $T(f),T(g) : T(A) \rightrightarrows T(B)$, then $a \in A$ is equalized by $f,g$, so that $a \in E$. It follows $a \in T(A) \cap E = T(E)$.' diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml index 64b607a5..ef3c6a26 100644 --- a/databases/catdat/data/macros.yaml +++ b/databases/catdat/data/macros.yaml @@ -58,6 +58,7 @@ \Coexp: \operatorname{Coexp} \inc: \operatorname{inc} \eq: \operatorname{eq} +\coeq: \operatorname{coeq} \cod: \operatorname{cod} \rank: \operatorname{rank} \Gal: \operatorname{Gal} diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json index e45b70b6..c2733e69 100644 --- a/databases/catdat/scripts/expected-data/forget_vector.json +++ b/databases/catdat/scripts/expected-data/forget_vector.json @@ -8,11 +8,16 @@ "exact": false, "preserves finite coproducts": false, "full": false, + "fully faithful": false, "preserves initial objects": false, "left adjoint": false, "right exact": false, "essentially injective": false, "left-invertible": false, + "right-invertible": false, + "reflector": false, + "coreflector": false, + "lifts small colimits": false, "cofinitary": true, "conservative": true, @@ -30,5 +35,6 @@ "right adjoint": true, "preserves terminal objects": true, "preserves reflexive coequalizers": true, - "preserves coreflexive equalizers": true + "preserves coreflexive equalizers": true, + "lifts small limits": true } diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json index 486c2879..8cebd163 100644 --- a/databases/catdat/scripts/expected-data/id_Set.json +++ b/databases/catdat/scripts/expected-data/id_Set.json @@ -16,6 +16,7 @@ "preserves finite coproducts": true, "preserves finite products": true, "full": true, + "fully faithful": true, "preserves initial objects": true, "left adjoint": true, "left exact": true, @@ -29,5 +30,10 @@ "preserves reflexive coequalizers": true, "preserves coreflexive equalizers": true, "essentially injective": true, - "left-invertible": true + "left-invertible": true, + "right-invertible": true, + "reflector": true, + "coreflector": true, + "lifts small limits": true, + "lifts small colimits": true } diff --git a/databases/catdat/scripts/utils/implications.ts b/databases/catdat/scripts/utils/implications.ts index f0388769..87d7f9e9 100644 --- a/databases/catdat/scripts/utils/implications.ts +++ b/databases/catdat/scripts/utils/implications.ts @@ -93,12 +93,23 @@ function get_assumption_string( ): string { const { assumptions } = implication - return Array.from(assumptions) + const own = Array.from(assumptions) .map( (assumption) => `${properties_dict[assumption][conditional ? 'conditional_relation' : 'relation']} ${assumption}`, ) .join(' and ') + + if (!implication.mapped_assumptions) return own + + const mapped = Object.entries(implication.mapped_assumptions) + .map( + ([map, props]) => + `and the ${map} has the required properties (${Array.from(props!).join(', ')})`, + ) + .join(', ') + + return `${own}, ${mapped}` } function get_conclusion_string( diff --git a/src/lib/server/fetchers/structures.ts b/src/lib/server/fetchers/structures.ts index d61ee10e..2fc4af8c 100644 --- a/src/lib/server/fetchers/structures.ts +++ b/src/lib/server/fetchers/structures.ts @@ -26,10 +26,14 @@ export function fetch_structures_and_tags(type: StructureType) { WHERE type = ${type} ORDER BY lower(name)`, sql` - SELECT tag - FROM tags - WHERE type = ${type} - ORDER BY id + SELECT t.tag + FROM tags t + WHERE t.type = ${type} + AND EXISTS ( + SELECT 1 FROM structure_tag_assignments a + WHERE a.tag = t.tag AND a.type = ${type} + ) + ORDER BY t.id `, ]) diff --git a/src/lib/server/transforms.ts b/src/lib/server/transforms.ts index fa5685ba..b42098fc 100644 --- a/src/lib/server/transforms.ts +++ b/src/lib/server/transforms.ts @@ -49,6 +49,21 @@ export function display_property_assignment( } } + // TODO: improve this + if ( + property.is_satisfied === 0 && + property.id.startsWith('lifts') && + !property.relation + ) { + return { + id: property.id, + label: property.id.replace(/^lifts/, 'lift'), + proof: property.proof, + is_deduced: Boolean(property.is_deduced), + relation: 'does not', + } + } + if (property.is_satisfied === 0) { property.relation = relation_negations[property.relation] } diff --git a/src/routes/functor/[id]/+page.svelte b/src/routes/functor/[id]/+page.svelte index 5b7bc43d..6d75a430 100644 --- a/src/routes/functor/[id]/+page.svelte +++ b/src/routes/functor/[id]/+page.svelte @@ -18,7 +18,7 @@ {#if data.functor.left_adjoint}
  • - Left adjoint: + Left adjoint functor: - Right adjoint: + Right adjoint functor: