Also removed

It is not true that every weak Heyting field with decidable equality is Heyting. See this proof for details.

since decidable equality isn’t really all that important for constructive fields. Locality (in the sense of local ring) and decidable apartness are more important.

]]>corrected Hörmander reference from 2.3 to 7.3

]]>Replaced

A Heyting field is a discrete field if and only if equality is decidable; it is in this sense that a discrete field is ‘discrete’

with

A Heyting field is a discrete field if and only if its apartness relation is a decidable relation.

This exact mistake was made and later corrected on the principle of omniscience page, where editors confused the analytic WLPO (reals have decidable equality) with the analytic LPO (reals have decidable apartness).

]]>Nathaniel Arkor suggested that info about univalence being consistent with excluded middle be added to this article

]]>added remark (here) on the terminology “second fundamental form” (which leaves room to be further expanded…)

]]>added pointer to:

- Frédéric Hélein, John C. Wood:
*Harmonic maps*, in:*Handbook of Global Analysis*, Elsevier (2008) 417-491 [doi:10.1016/B978-044452833-9.50009-7, pdf]

I have hyperlinked “rali”.

(First I thought it was a typo, but now I see that it’s intentional: rali lari lali rari – *lirum larum Löffelstiel*! :-)

Mention terminology **surjective equivalence**.

At least (algebraic) geometers denote inverse image functor/extension of scalars by $f^*$, direct image functor/restriction of scalars by $f_*$ and its right adjoint by $f^!$. Because one wants to think of $f$ being in a geometric direction, that is opposite to the morphism of rings. Geometrically minded algebraists (and sheaf theorists) follow this convention as well.

]]>I recently came back to this page and, after some thought, have demonstrated we cannot constructively prove all Heyting fields with decidable equality are discrete.

Theorem: if all Heyting fields with decidable equality are discrete, then excluded middle holds.

Proof: Fix any prime number $p \in \mathbb{N}$. Suppose $Q$ is a proposition. Then define $F_Q \subseteq \mathbb{Z}$ by $F_Q = \mathbb{Z} \setminus (p) \cup \{pn \mid n \neq 0 \wedge Q\}$. Then $F_Q$ is a prime filter, so $F_Q^{-1} \mathbb{Z}$ is a local ring. Let $k_Q$ be the corresponding Heyting field.

Note that $p = 0$ in $k_Q$ if and only if $p$ is not a unit in $F_Q^{-1} \mathbb{Z}$, if and only if $p \notin F_Q$, if and only if $\neg Q$. Thus, if $k_Q$ has decidable equality, then $\neg Q$ is decidable. Conversely, suppose $\neg Q$ is decidable. The ideal of nonunits in $F_Q^{-1} \mathbb{Z}$ is $\{x \in (p) \mid \neg Q\} \cup (0)$, which is a decidable subset of $\mathbb{Z}$, so $k_Q$ has decidable equality. Thus, $k_Q$ has decidable equality if and only if $\neg Q$ is decidable.

Note that $p$ is a unit in $k_Q$ if and only if $p$ is a unit in $F_Q^{-1} \mathbb{Z}$, iff $p \in F_Q$, iff $Q$. So if $k_Q$ is a discrete field, then $Q$ is decidable. Conversely, if $Q$ is decidable, then $k_Q$ is either $\mathbb{F}_p$ or $\mathbb{Q}$, and thus is a discrete field. So $k_Q$ is a discrete field if and only if $Q$ is decidable.

Now suppose all Heyting fields with decidable equality are discrete fields, and suppose $\neg \neg Q$. Then $\neg Q$ is decidable, so $k_Q$ is a Heyting field with decidable equality, so $k_Q$ is a discrete field. Because $k_Q$ is a discrete field, $Q$ is decidable. Since $Q$ is decidable and $\neg \neg Q$, we can conclude $Q$. We thus have double negation elimination, and hence full excluded middle. $\square$

If no one sees a flaw in this argument, then we should delete the portion of the page claiming “A Heyting field is a discrete field if and only if equality is decidable; it is in this sense that a discrete field is ‘discrete’.” Decidable equality is constructively weaker than decidable unithood.

]]>I am removing the following two paragraphs from the entry, since they don’t seem informative:

Like

Gravitation, the title can be taken to refer not only to the subject matter but also to the immense size and scope of the book itself. LikeThe Lord of the Rings, it consists of 6 parts arranged evenly into 3 volumes (but without appendices). Actually, Volume 3 has not yet been published (so who knows? it may have appendices after all!).The

Elephantis a good reference for anything related to topos theory, and we may often cite it here. However, it introduced many terminological changes, some of which may not be widely accepted or even known. (Fortunately, it will tell you about these in the text.)

The first comment about the number of parts is redundant by the detailed list of contents later in the entry.

For the fact that a part 3 has long been announced but remains unpublished I have added a brief line below that for part 2.

On those unspecified “terminological changes”, where relevant, we should just list them specifically.

]]>added pointer to today’s

- Federico Castellani,
*Nucleon electric and magnetic polarizabilities in Holographic QCD*[arXiv:2402.07553]

added pointer to today’s

- Jian-Hao Zhang, Shang-Qiang Ning, Yang Qi, Zheng-Cheng Gu,
*Construction and classification of crystalline topological superconductor and insulators in three-dimensional interacting fermion systems*[arXiv:2204.13558]

Small correction to the left action on $f_*(M)$. If S is not commutative then the multiplcation needs to be on the right. otherwise you get a right action instead of a left action

Justin Desrochers

]]>typo (“hence hence”)

]]>added pointer to:

Fanghua Lin, Changyou Wang:

*The Analysis of Harmonic Maps and Their Heat Flows*, World Scientific (2008) [doi:10.1142/6679]Jürgen Jost, Ch. 9 in:

*Riemannian Geometry and Geometric Analysis*, Springer (2017) [doi:10.1007/978-3-319-61860-9]

The complete lists RodMcGuire suggested is now at nLab report.

]]>Updated to give university webpage as Leeds personal webpages are in a mess at the moment.

]]>updated webpage address.

]]>Thanks Urs, I will implement your comments in the reports I am supporting in the next day or two. My current focus is on writing the most revealing reports I can because what I am supporting is the software development of a research project. We have many questions and few solid agreed upon facts to work with. Very exploratory.

]]>have touched wording, formatting and hyperlinking of this entry, trying to streamline a bit

]]>I have touched wording, formatting and hyperlinking, trying to brush-up this entry. But there is still room to do more.

]]>a stub entry, for the moment just to make links work

]]>