diff --git a/database/data/categories/Fld.yaml b/database/data/categories/Fld.yaml
index 2c0bb2835..4dd09eb54 100644
--- a/database/data/categories/Fld.yaml
+++ b/database/data/categories/Fld.yaml
@@ -11,13 +11,14 @@ tags:
related:
- CRing
+ - Fld_0
comments:
- Limits and colimits are discussed in MSE/359352.
satisfied_properties:
- property: locally small
- proof: There is a forgetful functor $\Fld \to \Set$ and $\Set$ is locally small.
+ proof: There is a forgetful functor $\Fld \to \Set$, and $\Set$ is locally small.
- property: inhabited
proof: This is trivial.
@@ -26,10 +27,10 @@ satisfied_properties:
proof: It is well-known that every field homomorphism is injective and hence a monomorphism.
- property: well-copowered
- proof: Epimorphisms are the purely inseparable field extensions. If $K \to L$ is purely inseparable, then for all $x \in L$ there is some $n \in \IN$ with $x^n \in L$. An element of $K$ has at most $n$ $n$th-roots. So we can bound the size of $L$.
+ proof: Epimorphisms are the purely inseparable field extensions (see below). If $K \to L$ is purely inseparable, then for every $x \in L$ there is some $n \in \IN$ such that $x^n \in K$. An element of $K$ has at most $n$ $n$th roots. Hence, we can bound the cardinality of $L$.
- property: multi-algebraic
- proof: See Eg. 4.3(1) in [AR01].
+ proof: Example 4.3(1) in [AR01] presents an FPC-sketch that models fields.
unsatisfied_properties:
- property: skeletal
@@ -39,34 +40,41 @@ unsatisfied_properties:
proof: There are infinitely many homomorphisms $\IQ(X) \to \IQ(X)$, $X \mapsto X^k$.
- property: connected
- proof: A field of characteristic $0$ cannot be connected with a field of characteristic $p > 0$. in fact, the connected components of $\Fld$ are the subcategories $\Fld_p$ of fields of characteristic $p$, where $p$ is a prime or $0$.
+ proof: A field of characteristic $0$ cannot be connected to a field of characteristic $p > 0$. In fact, the connected components of $\Fld$ are the subcategories $\Fld_p$ of fields of characteristic $p$, where $p$ is a prime or $0$.
- property: balanced
proof: Every non-trivial purely inseparable field extension, such as $\IF_p(X^p) \to \IF_p(X)$, provides a counterexample by the descriptions of special morphisms below.
- property: core-thin
- proof: If this category was core-thin, Galois theory would not exist. Specifically, the conjugation $\IC \to \IC$, $z \mapsto \overline{z}$ is a non-trivial automorphism.
+ proof: If this category were core-thin, Galois theory would not exist. Specifically, the conjugation $\IC \to \IC$, $z \mapsto \overline{z}$ is a non-trivial automorphism.
- property: multi-terminal object
- proof: Every field has a non-trivial extension, for instance, the rational function field over itself in one variable. Hence, a multi-terminal object never exists.
+ proof: Every field has a non-trivial extension, for instance, the rational function field in one variable over itself. Hence, a multi-terminal object never exists.
- property: generator
- proof: Assume that $G$ is a generator, say of characteristic $p$. Then for all $q \neq p$ all homomorphisms between two fields of characteristic $q$ would be equal, which is absurd.
+ proof: Assume that $G$ is a generator, say of characteristic $p$. Then for all $q \neq p$, all homomorphisms between two fields of characteristic $q$ would be equal, which is absurd.
- property: cogenerating set
- proof: 'We apply this lemma to the collection of fields: Any homomorphism of fields is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).'
+ proof: 'We apply this lemma to the collection of fields: Any homomorphism of fields is injective. For every infinite cardinal $\kappa$, the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$ and a non-trivial automorphism (swapping two variables).'
+ label: Fld_no_cogenerating_set
- property: binary powers
- proof: 'Assume that the product $P \coloneqq \IQ(\sqrt{2}) \times \IQ(\sqrt{2})$ exists. This field is isomorphic to a subfield of $\IQ(\sqrt{2})$, hence $P \cong \IQ$ or $P \cong \IQ(\sqrt{2})$. In the first case, the two projections $P \rightrightarrows \IQ(\sqrt{2})$ must be equal, which means that every two homomorphisms $K \rightrightarrows \IQ(\sqrt{2})$ are equal, which is absurd (take $K = \IQ(\sqrt{2})$ and its two automorphisms). In the second case, the projections induce for every field $K$ a bijection $\Hom(K,\IQ(\sqrt{2})) \cong \Hom(K,\IQ(\sqrt{2}))^2$, which however fails for $K = \IQ(\sqrt{2})$: the left hand side has $2$ elements, the right hand side has $4$ elements. A more general result about products in $\Fld$ can be found at MSE/359352.'
+ proof: 'Assume that the product $P \coloneqq \IQ(\sqrt{2}) \times \IQ(\sqrt{2})$ exists. This field is isomorphic to a subfield of $\IQ(\sqrt{2})$, hence $P \cong \IQ$ or $P \cong \IQ(\sqrt{2})$. In the first case, the two projections $P \rightrightarrows \IQ(\sqrt{2})$ must be equal, which means that every two homomorphisms $K \rightrightarrows \IQ(\sqrt{2})$ are equal, which is absurd (take $K = \IQ(\sqrt{2})$ and its two automorphisms). In the second case, the projections induce for every field $K$ a bijection $\Hom(K,\IQ(\sqrt{2})) \cong \Hom(K,\IQ(\sqrt{2}))^2$, which, however, fails for $K = \IQ(\sqrt{2})$: the left-hand side has $2$ elements, while the right-hand side has $4$ elements. A more general result about products in $\Fld$ can be found at MSE/359352.'
+ label: Fld_no_binary_powers
- property: locally cartesian closed
- proof: 'Assume that $K$ is a field such that $\Fld / K$ is cartesian closed. This slice category is equivalent to the poset of subfields of $K$. This poset is a lattice, and our assumption implies that it is distributive (see here). But this is quite rare: Consider $K = \IQ(\sqrt{2}, \sqrt{3})$. By Galois theory, the lattice of subfields is isomorphic to the diamond lattice $M_3$ which is not distributive. Specifically, $(\IQ(\sqrt{2}) \wedge \IQ(\sqrt{6})) \vee (\IQ(\sqrt{3}) \wedge \IQ(\sqrt{6})) = \IQ \vee \IQ = \IQ$, while $(\IQ(\sqrt{2}) \vee \IQ(\sqrt{3})) \wedge \IQ(\sqrt{6}) = \IQ(\sqrt{2},\sqrt{3}) \wedge \IQ(\sqrt{6}) = \IQ(\sqrt{6})$.'
+ proof: >-
+ Assume that $K$ is a field such that $\Fld / K$ is cartesian closed. This slice category is equivalent to the poset of subfields of $K$. This poset is a lattice, and our assumption implies that it is distributive (see here). But this is quite rare: Consider $K = \IQ(\sqrt{2}, \sqrt{3})$. By Galois theory, the lattice of subfields is isomorphic to the diamond lattice $M_3$, which is not distributive. Specifically,
+ $$(\IQ(\sqrt{2}) \wedge \IQ(\sqrt{6})) \vee (\IQ(\sqrt{3}) \wedge \IQ(\sqrt{6})) = \IQ \vee \IQ = \IQ,$$
+ while
+ $$(\IQ(\sqrt{2}) \vee \IQ(\sqrt{3})) \wedge \IQ(\sqrt{6}) = \IQ(\sqrt{2},\sqrt{3}) \wedge \IQ(\sqrt{6}) = \IQ(\sqrt{6}).$$
+ label: Fld_not_lcc
- property: cofiltered-limit-stable epimorphisms
proof: >-
- Inside of $\IF_p(X)$ consider the descending sequence of subfields
+ Inside $\IF_p(X)$, consider the descending sequence of subfields
$$\IF_p(X) \supseteq \IF_p(X^p) \supseteq \IF_p(X^{p^2}) \supseteq \cdots,$$
- whose intersection is $\IF_p$. Each $\IF_p(X^{p^n}) \hookrightarrow \IF_p(X)$ is purely inseparable, hence an epimorphism, but in the limit we get $\IF_p \hookrightarrow \IF_p(X)$, which is not even algebraic.
+ whose intersection is $\IF_p$. Each $\IF_p(X^{p^n}) \hookrightarrow \IF_p(X)$ is purely inseparable, hence an epimorphism, but in the limit we obtain $\IF_p \hookrightarrow \IF_p(X)$, which is not even algebraic.
special_objects: {}
diff --git a/database/data/categories/Fld_0.yaml b/database/data/categories/Fld_0.yaml
new file mode 100644
index 000000000..5a7f4e0b4
--- /dev/null
+++ b/database/data/categories/Fld_0.yaml
@@ -0,0 +1,82 @@
+id: Fld_0
+name: category of fields of characteristic zero
+notation: $\Fld_0$
+objects: fields of characteristic $0$
+morphisms: field homomorphisms (i.e., ring homomorphisms)
+description: This is the full subcategory of $\Fld$ consisting of fields of characteristic $0$. It is isomorphic to the coslice category $\IQ / \Fld$.
+nlab_link: https://ncatlab.org/nlab/show/Field
+
+tags:
+ - algebra
+
+related:
+ - Fld
+ - CRing
+
+comments:
+ - Limits and colimits are discussed in MSE/359352.
+
+satisfied_properties:
+ - property: locally small
+ proof: It is a full subcategory of $\Fld$, which is locally small.
+
+ - property: initial object
+ proof: The field $\IQ$ is an initial object; see for example here.
+
+ - property: left cancellative
+ proof: This property is inherited from $\Fld$.
+
+ - property: quotient-trivial
+ proof: 'An epimorphism of fields of characteristic $0$ is clearly also an epimorphism of fields, and is therefore purely inseparable by MSE/687869. In characteristic $0$, a purely inseparable field homomorphism is an isomorphism.'
+
+ - property: multi-algebraic
+ proof: 'Example 4.3(1) in [AR01] presents an FPC-sketch that models fields. It is an extension of the FP-sketch that models commutative rings. To model fields of characteristic $0$, we make the same construction with the FP-sketch that models commutative $\IQ$-algebras.'
+
+unsatisfied_properties:
+ - property: skeletal
+ proof: This is trivial.
+
+ - property: locally finite
+ proof: There are infinitely many homomorphisms $\IQ(X) \to \IQ(X)$, $X \mapsto X^k$.
+
+ - property: core-thin
+ proof: If this category were core-thin, Galois theory would not exist. Specifically, the conjugation $\IC \to \IC$, $z \mapsto \overline{z}$ is a non-trivial automorphism.
+
+ - property: semi-strongly connected
+ proof: There is no homomorphism from $\IQ(\sqrt{2})$ to $\IQ(\sqrt{3})$, since a direct calculation shows that $\IQ(\sqrt{3})$ has no element $a$ with $a^2=2$. Similarly, there is no homomorphism from $\IQ(\sqrt{3})$ to $\IQ(\sqrt{2})$. See also MSE/1069387.
+
+ - property: cogenerating set
+ proof: We can copy the proof from $\Fld$.
+ references:
+ - Fld_no_cogenerating_set
+
+ - property: binary powers
+ proof: We can copy the proof from $\Fld$ that the product $\IQ(\sqrt{2}) \times \IQ(\sqrt{2})$ does not exist.
+ references:
+ - Fld_no_binary_powers
+
+ - property: locally cartesian closed
+ proof: We can copy the proof from $\Fld$ that $\Fld_0 / \IQ(\sqrt{2}, \sqrt{3})$ is not cartesian closed.
+ references:
+ - Fld_not_lcc
+
+ - property: mono-regular
+ proof: >-
+ The following example comes from MSE/5129895, where a more general classification of regular monomorphisms is also given. Assume that $\IQ \hookrightarrow \IR$ is a regular monomorphism, i.e. the equalizer of two field homomorphisms $f,g : \IR \rightrightarrows K$. Consider the real numbers
+ $$x_1 = \sqrt{2}, \quad x_2 = \sqrt{3}, \quad x_3 = \sqrt{6}.$$
+ We have $x_1 x_2 = x_3$ and $f(x_i) = \pm g(x_i)$. Therefore, for some $i$ we have $f(x_i)=g(x_i)$. But $x_i \notin \IQ$.
+
+ - property: generator
+ proof: Assume that $G$ is a generator of $\Fld_0$. It must distinguish the two homomorphisms $\IQ(\sqrt{2}) \rightrightarrows \IQ(\sqrt{2})$. Since $\IQ(\sqrt{2})$ has only two subfields, we see that $G \cong \IQ(\sqrt{2})$. But $G$ must also distinguish the two homomorphisms $\IQ(\sqrt{3}) \rightrightarrows \IQ(\sqrt{3})$, so we likewise obtain $G \cong \IQ(\sqrt{3})$. This contradicts $\IQ(\sqrt{2}) \not\cong \IQ(\sqrt{3})$.
+
+special_objects:
+ initial object:
+ description: $\IQ$
+
+special_morphisms:
+ isomorphisms:
+ description: bijective field homomorphisms
+ proof: It is a full subcategory of $\CRing$, for which we know that isomorphisms are bijective homomorphisms.
+ regular monomorphisms:
+ description: A Galois extension is a regular monomorphism iff it is procyclic, and the general case can be reduced to this situation; see MSE/5129895 for details.
+ proof: See MSE/5129895.
diff --git a/database/data/category-implications/subobject-trivial.yaml b/database/data/category-implications/subobject-trivial.yaml
index e701a27ed..bf79b6338 100644
--- a/database/data/category-implications/subobject-trivial.yaml
+++ b/database/data/category-implications/subobject-trivial.yaml
@@ -1,5 +1,12 @@
# results on subobject-trivial categories
+- id: well_powered_trivial_criterion
+ assumptions:
+ - subobject-trivial
+ conclusions:
+ - well-powered
+ proof: This is trivial.
+
- id: thin_regular-subobject-trivial
assumptions:
- equalizers
diff --git a/database/data/special-morphism-rules.yaml b/database/data/special-morphism-rules.yaml
index 349546d7f..6b0634a5b 100644
--- a/database/data/special-morphism-rules.yaml
+++ b/database/data/special-morphism-rules.yaml
@@ -63,6 +63,16 @@
description: same as epimorphisms
proof: The category is epi-regular.
+- property: subobject-trivial
+ type: monomorphisms
+ description: same as isomorphisms
+ proof: The category is subobject-trivial.
+
+- property: quotient-trivial
+ type: epimorphisms
+ description: same as isomorphisms
+ proof: The category is quotient-trivial.
+
- property: regular-subobject-trivial
type: regular monomorphisms
description: same as isomorphisms