Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: field

Bottom of Page

1 to 17 of 17

  1.  
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeNov 26th 2017

    I added to field a mention of some other constructive variants of the definition, with a couple more references.

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 26th 2017

    I fixed up the DOI link for Johnstone’s paper (at field and at local ring), since the geniuses at Elsevier use parentheses in their DOIs, which break markdown syntax.

    For reference, one needs to replace (nn) in the DOI url by %28nn%29.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeNov 26th 2017

    Thanks! I’ve noticed that before, but always forget about it.

  4. Clarify a sentence to say that the discrete field condition implies that 0≠10\neq 1.

    Egbert Rijke

    diff, v49, current

    • CommentRowNumber5.
    • CommentAuthorUlrik
    • CommentTimeJan 8th 2021

    Change definition of denial field to actually match MRR87

    diff, v50, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMar 10th 2021

    cross-linked the discussion of weakly initial sets in the category of fields with the corresponding example at multi-adjoint

    diff, v53, current

  7. one pair of authors defined fields to be possibly trivial.

    Anonymous

    diff, v57, current

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMay 26th 2022
    • (edited May 26th 2022)

    I have taken the liberty of turning this comment from a sub-section into a remark (here). Also tried to adjust the wording a little, for readability.

    diff, v58, current

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJun 25th 2022
    • CommentRowNumber10.
    • CommentAuthorMarkSaving
    • CommentTimeJul 3rd 2022

    There appears to be an error in the section on construction notions of a field. Specifically, the claim is that a residue field is discrete iff equality is decidable. But this seems not to be true.

    In fact, the statement “A residue field with decidable equality is a Heyting field” is equivalent to excluded middle.

    To see this, consider a proposition pp. Consider the set R p=ℤ∪{x∈ℚ∣p}R_p = \mathbb{Z} \cup \{x \in \mathbb{Q} \mid p\}, which is a subring of ℚ\mathbb{Q}. Since R pR_p is a subset of ℚ\mathbb{Q} and ℚ\mathbb{Q} has decidable equality, R pR_p also has decidable equality. And of course 0≠10 \neq 1 in R pR_p.

    I claim that R pR_p is a residue field iff ¬¬p\neg \neg p. For suppose ¬¬p\neg \neg p, and consider some x∈R px \in R_p. Suppose xx does not have a multiplicative inverse. Now suppose x≠0x \neq 0. Then we see that x −1∉R px^{-1} \notin R_p. If pp held, we would have x −1∈R px^{-1} \in R_p. So we know ¬p\neg p holds. But this is a contradiction. Therefore, xx must be zero (using decidable equality).

    Conversely, suppose RR is a residue field. Then 2≠02 \neq 0, so 2 does not fail to have an inverse. That is, 2 −12^{-1} is not not in R pR_p. Then ¬¬p\neg \neg p.

    I claim that R pR_p is a Heyting field iff pp iff R pR_p is a discrete field. For suppose RR is a Heyting field. Then either 2 or 3 has a multiplicative inverse, so either 2 −12^{-1} or 3 −1∈R p3^{-1} \in R_p. In either case, we see that pp holds. If pp holds, then R p=ℚR_p = \mathbb{Q}, which is a discrete field. And if R pR_p is a discrete field, it is clearly a Heyting field.

    With these facts in hand, we see that if every residue field with decidable equality is a Heyting field, then p⇔¬¬pp \iff \neg \neg p holds for all pp. So we have full excluded middle.

    Of course, assuming excluded middle, it is clear that all residue fields with decidable equality are discrete fields. □\square

    I have not yet determined whether all Heyting fields with decidable equality are discrete, but it seems very likely that this also cannot be proven.

    If no one objects, I will change the page to say that a residue field is discrete if and only if unithood is decidable.

  11. added Mark Saying’s proof that not every residue field with decidable equality is Heyting.

    Anonymous

    diff, v61, current

  12. Added reference

    and used the more clear “weak Heyting field” over the ambiguous “residue field” throughout the page.

    Anonymouse

    diff, v70, current

  13. Linked new page for Field, the category of fields.

    diff, v71, current

    • CommentRowNumber14.
    • CommentAuthorMarkSaving
    • CommentTimeJun 19th 2024
    • (edited Jun 19th 2024)

    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∈ℕp \in \mathbb{N}. Suppose QQ is a proposition. Then define F Q⊆ℤF_Q \subseteq \mathbb{Z} by F Q=ℤ∖(p)∪{pn∣n≠0∧Q}F_Q = \mathbb{Z} \setminus (p) \cup \{pn \mid n \neq 0 \wedge Q\}. Then F QF_Q is a prime filter, so F Q −1ℤF_Q^{-1} \mathbb{Z} is a local ring. Let k Qk_Q be the corresponding Heyting field.

    Note that p=0p = 0 in k Qk_Q if and only if pp is not a unit in F Q −1ℤF_Q^{-1} \mathbb{Z}, if and only if p∉F Qp \notin F_Q, if and only if ¬Q\neg Q. Thus, if k Qk_Q has decidable equality, then ¬Q\neg Q is decidable. Conversely, suppose ¬Q\neg Q is decidable. The ideal of nonunits in F Q −1ℤF_Q^{-1} \mathbb{Z} is {x∈(p)∣¬Q}∪(0)\{x \in (p) \mid \neg Q\} \cup (0), which is a decidable subset of ℤ\mathbb{Z}, so k Qk_Q has decidable equality. Thus, k Qk_Q has decidable equality if and only if ¬Q\neg Q is decidable.

    Note that pp is a unit in k Qk_Q if and only if pp is a unit in F Q −1ℤF_Q^{-1} \mathbb{Z}, iff p∈F Qp \in F_Q, iff QQ. So if k Qk_Q is a discrete field, then QQ is decidable. Conversely, if QQ is decidable, then k Qk_Q is either 𝔽 p\mathbb{F}_p or ℚ\mathbb{Q}, and thus is a discrete field. So k Qk_Q is a discrete field if and only if QQ is decidable.

    Now suppose all Heyting fields with decidable equality are discrete fields, and suppose ¬¬Q\neg \neg Q. Then ¬Q\neg Q is decidable, so k Qk_Q is a Heyting field with decidable equality, so k Qk_Q is a discrete field. Because k Qk_Q is a discrete field, QQ is decidable. Since QQ is decidable and ¬¬Q\neg \neg Q, we can conclude QQ. 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.

    • CommentRowNumber15.
    • CommentAuthorAshley
    • CommentTimeJun 19th 2024

    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).

    diff, v73, current

    • CommentRowNumber16.
    • CommentAuthorAshley
    • CommentTimeJun 19th 2024

    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.

    diff, v73, current

  17. changed higher algebra - contents to algebra - contents in context sidebar

    Anonymouse

    diff, v75, current

1 to 17 of 17

  1.