Return to Answer

$\newcommand{\N}{\mathbb N}\newcommand{\paren}[1]{\left(#1\right)}\newcommand{\T}{\mathbb{T}}\newcommand{\m}{\mathfrak{m}}\newcommand{\E}{\mathbf{E}}$I can answer your first set of questions:

There is a geometric theory of blueprints. It's easiest* to work from the definition of a blueprint as a pair $B = (A,R)$ consisting of a semiring $R$ and a multiplicative subset $A \subseteq R$ which contains $0$ and $1$, and which generates all of $R$.

The theory will have a sorts $A,R$, function symbols $+, \cdot$, constant symbols $0_A,1_A, 0_R, 1_R$, and a unary function symbol $\iota$, giving the inclusion of $A$ into $R$. In addition to axioms asserting that $R$ is a semiring and that $A$ embeds monomorphically as a multiplicative submonoid of $R$ such that $\iota(0_A) = 0_R$ and $\iota(1_A) = 1_R$, we have the infinitary axiom $$ \vdash^{x : R} (x = 0) \lor \paren{\bigvee_{n \in \N, \; \varphi \in \text{Oper}_n}\exists a_0\dotsm a_n . \varphi(\iota(a_0),\dotsc,\iota(a_n)) = x }$$ where $\text{Oper}_n$ is the set of $n$-ary semiring operations built from $0_R,1_R,+,\cdot$. This axioms states that $A$ suffices to generate all of $R$

There can be no coherent axiomatization of the theory $\T$ of blueprints. To see this, suppose that $\T$ were coherent. Then we could obtain a new coherent theory $\T\,'$ by introducing the following additional coherent axioms which require a blueprint in $\text{Set}$ to be isomorphic to $(\{0,1\} \hookrightarrow \N)$. $$ \vdash^{a: A} \iota(a) = 0 \lor \iota(a) = 1 $$ $$ x + y = 0 \vdash^{x,y : R} x = y = 0 $$ Since any consistent finitary first-order theory with an infinite model will admit arbitrarily large models in $\text{Set}$, this is impossible.

Regarding local blueprints: The definition of local blueprints as those having a unique maximal ideal of course cannot, in its current form, be stated in geometric logic. However, we can say in $\text{Set}$ that a congruence $\sim_\m$ on a blueprint $B = (A,R)$ is the unique maximal nontrivial congruence on $B$ iff for any pair of elements $x,y \in R$, if $x \sim_\m y$ fails, then the smallest congruence $\sim$ such that $x \sim y$ is trivial. This can be stated in a conservative geometric extension of our theory of blueprints if we adjoin a binary relation symbol $\sim_m$ on $R \times R$, together with axioms stating that $\sim_m$ is a congruence, in addition to the following axiom which states that any unless $x \sim_\m y$ holds, every congruence containing $(x,y)$ contains every pair of elements in $R$. $$\vdash^{x,y,z,w:R} {x \sim_\m y \lor} \paren{\bigvee_{n \in \N, \text{Oper}_n} \exists a_0\dotsm a_n : A . \E(z,\iota(a_0)) \land \E(\iota(a_0), \iota(a_1)) \land \dotsi \land \E(\iota(a_n), w)} $$ where $\E(c,d)$ denotes the sub-expression $$ \bigvee_{n \in \N, \; \varphi \in \text{Oper}_n} \exists b_0 \dotsm b_n : A. \varphi(c,b_0,\dotsc,b_n) = \varphi(d,b_0, \dotsc, b_n) $$

*But not essential. Since the list object is a geometric construction, we could also write down a two-sorted theory which axiomatizes the behavior of an equivalence relation on the set of lists. The downside of that approach is that it would involve lots of complicated-to-state infinitary axioms.

$\newcommand{\N}{\mathbb N}\newcommand{\paren}[1]{\left(#1\right)}\newcommand{\T}{\mathbb{T}}\newcommand{\m}{\mathfrak{m}}\newcommand{\E}{\mathbf{E}}$I can answer your first set of questions:

There is a geometric theory of blueprints. It's easiest* to work from the definition of a blueprint as a pair $B = (A,R)$ consisting of a semiring $R$ and a multiplicative subset $A \subseteq R$ which contains $0$ and $1$, and which generates all of $R$.

The theory will have a sorts $A,R$, function symbols $+, \cdot$, constant symbols $0_A,1_A, 0_R, 1_R$, and a unary function symbol $\iota$, giving the inclusion of $A$ into $R$. In addition to axioms asserting that $R$ is a semiring and that $A$ embeds monomorphically as a multiplicative submonoid of $R$ such that $\iota(0_A) = 0_R$ and $\iota(1_A) = 1_R$, we have the infinitary axiom $$ \vdash^{x : R} (x = 0) \lor \paren{\bigvee_{n \in \N, \; \varphi \in \text{Oper}_{n+1}}\exists a_0\dotsm a_n . \varphi(\iota(a_0),\dotsc,\iota(a_n)) = x }$$ where $\text{Oper}_n$ is the set of $n$-ary semiring operations built from $0_R,1_R,+,\cdot$. This axioms states that $A$ suffices to generate all of $R$

There can be no coherent axiomatization of the theory $\T$ of blueprints. To see this, suppose that $\T$ were coherent. Then we could obtain a new coherent theory $\T\,'$ by introducing the following additional coherent axioms which require a blueprint in $\text{Set}$ to be isomorphic to $(\{0,1\} \hookrightarrow \N)$. $$ \vdash^{a: A} \iota(a) = 0 \lor \iota(a) = 1 $$ $$ x + y = 0 \vdash^{x,y : R} x = y = 0 $$ Since any consistent finitary first-order theory with an infinite model will admit arbitrarily large models in $\text{Set}$, this is impossible.

Regarding local blueprints: The definition of local blueprints as those having a unique maximal ideal of course cannot, in its current form, be stated in geometric logic. However, we can say in $\text{Set}$ that a congruence $\sim_\m$ on a blueprint $B = (A,R)$ is the unique maximal nontrivial congruence on $B$ iff for any pair of elements $x,y \in R$, if $x \sim_\m y$ fails, then the smallest congruence $\sim$ such that $x \sim y$ is trivial. This can be stated in a conservative geometric extension of our theory of blueprints if we adjoin a binary relation symbol $\sim_m$ on $R \times R$, together with axioms stating that $\sim_m$ is a congruence, in addition to the following axiom which states that unless $x \sim_\m y$ holds, every congruence containing $(x,y)$ contains every pair of elements in $R$. $$\vdash^{x,y,z,w:R} {x \sim_\m y \lor} \paren{\bigvee_{n \in \N} \exists a_0\dotsm a_n : A . \E(z,\iota(a_0)) \land \E(\iota(a_0), \iota(a_1)) \land \dotsi \land \E(\iota(a_n), w)} $$ where $\E(c,d)$ denotes the sub-expression $$ \bigvee_{n \in \N, \; \varphi \in \text{Oper}_{n+2}} \exists b_0 \dotsm b_n : A. \varphi(c,b_0,\dotsc,b_n) = \varphi(d,b_0, \dotsc, b_n) $$

*But not essential. Since the list object is a geometric construction, we could also write down a two-sorted theory which axiomatizes the behavior of an equivalence relation on the set of lists. The downside of that approach is that it would involve lots of complicated-to-state infinitary axioms.

$\newcommand{\N}{\mathbb N}\newcommand{\paren}[1]{\left(#1\right)}\newcommand{\T}{\mathbb{T}}\newcommand{\m}{\mathfrak{m}}\newcommand{\E}{\mathbf{E}}$I can answer your first set of questions:

There is a geometric theory of blueprints. It's easiest* to work from the definition of a blueprint as a pair $B = (A,R)$ consisting of a semiring $R$ and a multiplicative subset $A \subseteq R$ which contains $0$ and $1$, and which generates all of $R$.

The theory will have a sorts $A,R$, function symbols $+, \cdot$, constant symbols $0_A,1_A, 0_R, 1_R$, and a unary function symbol $\iota$, giving the inclusion of $A$ into $R$. In addition to axioms asserting that $R$ is a semiring and that $A$ embeds monomorphically as a multiplicative submonoid of $R$ such that $\iota(0_A) = 0_R$ and $\iota(1_A) = 1_R$, we have the infinitary axiom $$ \vdash^{x : R} (x = 0) \lor \paren{\bigvee_{n \in \N, \; \varphi \in \text{Oper}_n}\exists a_0\dotsm a_n . \varphi(\iota(a_0),\dotsc,\iota(a_n)) = x }$$ where $\text{Oper}_n$ is the set of $n$-ary semiring operations built from $0_R,1_R,+,\cdot$. This axioms states that $A$ suffices to generate all of $R$

There can be no coherent axiomatization of the theory $\T$ of blueprints. To see this, suppose that $\T$ were coherent. Then we could obtain a new coherent theory $\T\,'$ by introducing the following additional coherent axioms which require a blueprint in $\text{Set}$ to be isomorphic to $(\{0,1\} \hookrightarrow \N)$. $$ \vdash^{a: A} \iota(a) = 0 \lor \iota(a) = 1 $$ $$ x + y = 0 \vdash^{x,y : R} x = y = 0 $$ Since any consistent finitary first-order theory with an infinite model will admit arbitrarily large models in $\text{Set}$, this is impossible.

Regarding local blueprints: The definition of local blueprints as those having a unique maximal ideal of course cannot, in its current form, be stated in geometric logic. However, we can say in $\text{Set}$ that a congruence $\sim_\m$ on a blueprint $B = (A,R)$ is the unique maximal nontrivial congruence on $B$ iff for any pair of elements $x,y \in R$, if $x \sim_\m y$ fails, then the smallest congruence $\sim$ such that $x \sim y$ is trivial. This can be stated in a conservative geometric extension of our theory of blueprints if we adjoin a binary relation symbol $\sim_m$ on $R \times R$, together with axioms stating that $\sim_m$ is a congruence, in addition to the following axiom which states that any unless $x \sim_\m y$ holds, every congruence containing $(x,y)$ contains every pair of elements in $R$. $$\vdash^{x,y,z,w:R} x \sim_\m y \lor \paren{\bigvee_{n \in \N, \text{Oper}_n}} \exists a_0\dotsm a_n : A . \E(z,\iota(a_0)) \land \E(\iota(a_0), \iota(a_1)) \land \dotsi \land \E(\iota(a_n), w) $$ where $\E(c,d)$ denotes the sub-expression $$ \bigvee_{n \in \N, \; \varphi \in \text{Oper}_n} \exists b_0 \dotsm b_n : A. \varphi(c,b_0,\dotsc,b_n) = \varphi(d,b_0, \dotsc, b_n) $$

*But not essential. Since the list object is a geometric construction, we could also write down a two-sorted theory which axiomatizes the behavior of an equivalence relation on the set of lists. The downside of that approach is that it would involve lots of complicated-to-state infinitary axioms.

$\newcommand{\N}{\mathbb N}\newcommand{\paren}[1]{\left(#1\right)}\newcommand{\T}{\mathbb{T}}\newcommand{\m}{\mathfrak{m}}\newcommand{\E}{\mathbf{E}}$I can answer your first set of questions:

There is a geometric theory of blueprints. It's easiest* to work from the definition of a blueprint as a pair $B = (A,R)$ consisting of a semiring $R$ and a multiplicative subset $A \subseteq R$ which contains $0$ and $1$, and which generates all of $R$.

The theory will have a sorts $A,R$, function symbols $+, \cdot$, constant symbols $0_A,1_A, 0_R, 1_R$, and a unary function symbol $\iota$, giving the inclusion of $A$ into $R$. In addition to axioms asserting that $R$ is a semiring and that $A$ embeds monomorphically as a multiplicative submonoid of $R$ such that $\iota(0_A) = 0_R$ and $\iota(1_A) = 1_R$, we have the infinitary axiom $$ \vdash^{x : R} (x = 0) \lor \paren{\bigvee_{n \in \N, \; \varphi \in \text{Oper}_n}\exists a_0\dotsm a_n . \varphi(\iota(a_0),\dotsc,\iota(a_n)) = x }$$ where $\text{Oper}_n$ is the set of $n$-ary semiring operations built from $0_R,1_R,+,\cdot$. This axioms states that $A$ suffices to generate all of $R$

There can be no coherent axiomatization of the theory $\T$ of blueprints. To see this, suppose that $\T$ were coherent. Then we could obtain a new coherent theory $\T\,'$ by introducing the following additional coherent axioms which require a blueprint in $\text{Set}$ to be isomorphic to $(\{0,1\} \hookrightarrow \N)$. $$ \vdash^{a: A} \iota(a) = 0 \lor \iota(a) = 1 $$ $$ x + y = 0 \vdash^{x,y : R} x = y = 0 $$ Since any consistent finitary first-order theory with an infinite model will admit arbitrarily large models in $\text{Set}$, this is impossible.

Regarding local blueprints: The definition of local blueprints as those having a unique maximal ideal of course cannot, in its current form, be stated in geometric logic. However, we can say in $\text{Set}$ that a congruence $\sim_\m$ on a blueprint $B = (A,R)$ is the unique maximal nontrivial congruence on $B$ iff for any pair of elements $x,y \in R$, if $x \sim_\m y$ fails, then the smallest congruence $\sim$ such that $x \sim y$ is trivial. This can be stated in a conservative geometric extension of our theory of blueprints if we adjoin a binary relation symbol $\sim_m$ on $R \times R$, together with axioms stating that $\sim_m$ is a congruence, in addition to the following axiom which states that any unless $x \sim_\m y$ holds, every congruence containing $(x,y)$ contains every pair of elements in $R$. $$\vdash^{x,y,z,w:R} {x \sim_\m y \lor} \paren{\bigvee_{n \in \N, \text{Oper}_n} \exists a_0\dotsm a_n : A . \E(z,\iota(a_0)) \land \E(\iota(a_0), \iota(a_1)) \land \dotsi \land \E(\iota(a_n), w)} $$ where $\E(c,d)$ denotes the sub-expression $$ \bigvee_{n \in \N, \; \varphi \in \text{Oper}_n} \exists b_0 \dotsm b_n : A. \varphi(c,b_0,\dotsc,b_n) = \varphi(d,b_0, \dotsc, b_n) $$

*But not essential. Since the list object is a geometric construction, we could also write down a two-sorted theory which axiomatizes the behavior of an equivalence relation on the set of lists. The downside of that approach is that it would involve lots of complicated-to-state infinitary axioms.

$\newcommand{\N}{\mathbb N}\newcommand{\paren}[1]{\left(#1\right)}\newcommand{\T}{\mathbb{T}}\newcommand{\m}{\mathfrak{m}}\newcommand{\E}{\mathbf{E}}$I can answer your first set of questions:

There is a geometric theory of blueprints. It's easiest* to work from the definition of a blueprint as a pair $B = (A,R)$ consisting of a semiring $R$ and a multiplicative subset $A \subseteq R$ which contains $0$ and $1$, and which generates all of $R$.

The theory will have a sorts $A,R$, function symbols $+, \cdot$, constant symbols $0_A,1_A, 0_R, 1_R$, and a unary function symbol $\iota$, giving the inclusion of $A$ into $R$. In addition to axioms asserting that $R$ is a semiring and that $A$ embeds monomorphically as a multiplicative submonoid of $R$ such that $\iota(0_A) = 0_R$ and $\iota(1_A) = 1_R$, we have the infinitary axiom $$ \vdash^{x : R} (x = 0) \lor \paren{\bigvee_{n \in \N, \; \varphi \in \text{Oper}_n}\exists a_0\dotsm a_n . \varphi(\iota(a_0),\dotsc,\iota(a_n)) = x }$$ where $\text{Oper}_n$ is the set of $n$-ary semiring operations built from $0_R,1_R,+,\cdot$. This axioms states that $A$ suffices to generate all of $R$

There can be no coherent axiomatization of the theory $\T$ of blueprints. To see this, suppose that $\T$ were coherent. Then we could obtain a new coherent theory $\T\,'$ by introducing the following additional coherent axioms which require a blueprint in $\text{Set}$ to be isomorphic to $(\{0,1\} \hookrightarrow \N)$. $$ \vdash^{a: A} \iota(a) = 0 \lor \iota(a) = 1 $$ $$ x + y = 0 \vdash^{x,y : R} x = y = 0 $$ Since any consistent finitary first-order theory with an infinite model will admit arbitrarily large models in $\text{Set}$, this is impossible.

Regarding local blueprints: The definition of local blueprints as those having a unique maximal ideal of course cannot, in its current form, be stated in geometric logic. However, we can say in $\text{Set}$ that a congruence $\sim_\m$ on a blueprint $B = (A,R)$ is the unique maximal nontrivial congruence on $B$ iff for any pair of elements $x,y \in R$, if $x \sim_\m y$ fails, then the smallest congruence $\sim$ such that $x \sim y$ is trivial. This can be stated in a conservative geometric extension of our theory of blueprints if we adjoin a binary relation symbol $\sim_m$ on $R \times R$, together with axioms stating that $\sim_m$ is a congruence, in addition to the following axiom which states that any unless $x \sim_\m y$ holds, every congruence containing $(x,y)$ contains every pair of elements in $R$. $$\vdash^{x,y,z,w:R} x \sim_\m y \lor \paren{\bigvee_{n \in \N, \text{Oper}_n}} \exists a_0\dotsm a_n : A . \E(z,\iota(a_0)) \land \E(\iota(a_0), \iota(a_1)) \land \dotsi \land \E(\iota(a_n), w) $$ where $\E(c,d)$ denotes the sub-expression $$ \bigvee_{n \in \N, \; \varphi \in \text{Oper}_n} \exists b_0 \dotsm b_n : A. \varphi(c,b_0,\dotsc,b_n) = \varphi(d,b_0, \dotsc, b_n) $$

While there's probably a more elegant way to axiomatize everything, this approach has the nice property that morphisms of $\T_\text{local}$-algebras preserve the maximal ideal.

*But not essential. Since the list object is a geometric construction, we could also write down a two-sorted theory which axiomatizes the behavior of an equivalence relation on the set of lists. The downside of that approach is that it would involve lots of complicated-to-state infinitary axioms.

$\newcommand{\N}{\mathbb N}\newcommand{\paren}[1]{\left(#1\right)}\newcommand{\T}{\mathbb{T}}\newcommand{\m}{\mathfrak{m}}\newcommand{\E}{\mathbf{E}}$I can answer your first set of questions:

There is a geometric theory of blueprints. It's easiest* to work from the definition of a blueprint as a pair $B = (A,R)$ consisting of a semiring $R$ and a multiplicative subset $A \subseteq R$ which contains $0$ and $1$, and which generates all of $R$.

The theory will have a sorts $A,R$, function symbols $+, \cdot$, constant symbols $0_A,1_A, 0_R, 1_R$, and a unary function symbol $\iota$, giving the inclusion of $A$ into $R$. In addition to axioms asserting that $R$ is a semiring and that $A$ embeds monomorphically as a multiplicative submonoid of $R$ such that $\iota(0_A) = 0_R$ and $\iota(1_A) = 1_R$, we have the infinitary axiom $$ \vdash^{x : R} (x = 0) \lor \paren{\bigvee_{n \in \N, \; \varphi \in \text{Oper}_n}\exists a_0\dotsm a_n . \varphi(\iota(a_0),\dotsc,\iota(a_n)) = x }$$ where $\text{Oper}_n$ is the set of $n$-ary semiring operations built from $0_R,1_R,+,\cdot$. This axioms states that $A$ suffices to generate all of $R$

There can be no coherent axiomatization of the theory $\T$ of blueprints. To see this, suppose that $\T$ were coherent. Then we could obtain a new coherent theory $\T\,'$ by introducing the following additional coherent axioms which require a blueprint in $\text{Set}$ to be isomorphic to $(\{0,1\} \hookrightarrow \N)$. $$ \vdash^{a: A} \iota(a) = 0 \lor \iota(a) = 1 $$ $$ x + y = 0 \vdash^{x,y : R} x = y = 0 $$ Since any consistent finitary first-order theory with an infinite model will admit arbitrarily large models in $\text{Set}$, this is impossible.

Regarding local blueprints: The definition of local blueprints as those having a unique maximal ideal of course cannot, in its current form, be stated in geometric logic. However, we can say in $\text{Set}$ that a congruence $\sim_\m$ on a blueprint $B = (A,R)$ is the unique maximal nontrivial congruence on $B$ iff for any pair of elements $x,y \in R$, if $x \sim_\m y$ fails, then the smallest congruence $\sim$ such that $x \sim y$ is trivial. This can be stated in a conservative geometric extension of our theory of blueprints if we adjoin a binary relation symbol $\sim_m$ on $R \times R$, together with axioms stating that $\sim_m$ is a congruence, in addition to the following axiom which states that any unless $x \sim_\m y$ holds, every congruence containing $(x,y)$ contains every pair of elements in $R$. $$\vdash^{x,y,z,w:R} x \sim_\m y \lor \paren{\bigvee_{n \in \N, \text{Oper}_n}} \exists a_0\dotsm a_n : A . \E(z,\iota(a_0)) \land \E(\iota(a_0), \iota(a_1)) \land \dotsi \land \E(\iota(a_n), w) $$ where $\E(c,d)$ denotes the sub-expression $$ \bigvee_{n \in \N, \; \varphi \in \text{Oper}_n} \exists b_0 \dotsm b_n : A. \varphi(c,b_0,\dotsc,b_n) = \varphi(d,b_0, \dotsc, b_n) $$

*But not essential. Since the list object is a geometric construction, we could also write down a two-sorted theory which axiomatizes the behavior of an equivalence relation on the set of lists. The downside of that approach is that it would involve lots of complicated-to-state infinitary axioms.