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 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 sheaves 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: ordered field

Bottom of Page

1 to 19 of 19

  1.  

  1. Auke Booij’s thesis Analysis in univalent type theory as well as the HoTT book explicitly defines an ordered field to have an lattice structure on the underlying commutative ring, which is different from the definition of an ordered field in the nlab article, where such a condition is missing. (by lattice I mean unbounded lattice, or what some people call pseudolattices)

    However, there are no references in the current nlab article on ordered fields showing that an ordered field doesn’t have a lattice structure in constructive mathematics. The basic definition lacking a lattice structure was already written in 2010 in the first revision of the article by Toby Bartels, and the other editors of the article, Todd Trimble and a few anonymous editors from earlier this year, all accepted the basic definition provided by Toby Bartels, since it hasn’t been modified since the first revision. So if they are still around I would like them or somebody else to provide references from the mathematical literature justifying that ordered fields do not necessarily have a lattice structure, or prove that every ordered field as currently defined has a compatible lattice structure. Otherwise I’ll insert the lattice structure into the definition.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeJul 5th 2022

    Are the surreal numbers a pseudolattice, constructively? I don’t know, I haven’t thought about it at all.

    • CommentRowNumber3.
    • CommentAuthorGuest
    • CommentTimeJul 5th 2022

    Do the MacNeille real numbers have a pseudolattice structure in constructive mathematics?

    Even if the MacNeille real numbers have a pseudolattice structure, with the weak order defined by a≤b≔max(a,b)=ba \leq b \coloneqq \max(a, b) = b, it is not necessarily true that ¬(a<b)⇔max(a,b)=a\neg (a \lt b) \iff \max(a, b) = a in the MacNeille real numbers.

    Also note that the current definition does not specify how a field is defined, nor set any requirements of invertibility for positive elements, or any relationship to whatever weak order a field might have. Are fields defined as Heyting fields, or Peter Johnstone’s residue fields? Defining fields as Heyting fields would exclude the MacNeille real numbers from being an ordered field.

  4. fixed second definition to align with the first, the old second definition implies that the field is a Heyting, while depending on the definition of field in the first definition of ordered field, such as Peter Johnson’s residue fields, it is not necessarily true that the field is Heyting.

    Anonymous

    diff, v9, current

  5. complete -> Dedekimd complete.

    To disambiguate from Cauchy complete, which is frequently used to refer to Cauchy sequences and is a weaker condition than Dedekind completeness

    Anonymous

    diff, v9, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2022
    • (edited Jul 5th 2022)

    Re #1:

    It seems safe to assume that the short note from ref 1 leaves room for improvement, certainly if it differs from established literature. Also, on the off-chance that there was a deeper claim meant to be implied by rev 1, the author can still come back and expand on it later. So I don’t think you should hold back if you see room to improve the entry and have the energy to do so.

    (NB: In practice one cannot assume that a later edit of an entry is meant as an endorsement of all previous material that is kept.)

  7. Mike,

    Are the surreal numbers even a commutative ring in constructive mathematics? The nlab article on the surreal numbers says the following:

    The definition of ≥\geq for numbers as formulated by Conway leans heavily upon properties of negation, and in particular the classical principle of excluded middle. However, it can be made more constructive by defining <\lt separately from ≤\le:

    • A number xx consists of a set L xL_x of numbers and a set R xR_x of numbers, under the condition that every member of L xL_x is <\lt every member of R xR_x.
    • x≤yx \leq y if x′<yx' \lt y is true for any x′∈L xx' \in L_x, and x<y′x \lt y' is true for any y′∈R yy' \in R_y.
    • x<yx \lt y if there exists an x′∈R xx'\in R_x such that x′≤yx'\le y, or there exists a y′∈L yy'\in L_y such that x≤y′x\le y'.
    • x=yx = y is defined to mean x≤yx \le y and y≤xy \le x.

    This approach works up to a point. However, it encounters a problem in proving that multiplication is well-defined, i.e. that it respects equality. We can prove that if x≥0x\ge 0 then y≤z⇒xy≤xzy\le z \Rightarrow x y \le x z and hence y=z⇒xy=xzy = z \Rightarrow x y = x z, and that if x≤0x\le 0 then y≤z⇒xy≥xzy\le z \Rightarrow x y \ge x z and hence y=z⇒xy=xzy = z \Rightarrow x y = x z; but without excluded middle we can’t say that every xx is either ≥0\ge 0 or ≤0\le 0, so how can we conclude that y=z⇒xy=xzy = z \Rightarrow x y = x z? It is unknown whether there is a solution to this problem.

    Section 11.6 of the HoTT book on surreal numbers never defines multiplication on the surreal numbers either.

  8. I’ve started a reference request on MathOverflow for the definition of ordered field here.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2022

    It looks to me that if a statement is evidently a short informal side remark (not much more than a dozen parenthetical words in rev 1) and given that you have references and expertise already all pointing to it needing improvement, it’s unclear how going to a large public forum with “the nLab claims this statement” serves a purpose? If you are genuinely uncertain then send an email to Toby Bartels – otherwise please just fix it (cf. #6). Thanks!

  10. The MathOverflow user Geoffrey Irving has this to say about ordered fields with and without lattice structure:

    one can convert back and forth between definitions with and without lattice structure. Given a lattice field, one can adjoin a positive transcendental with no other information to get a nonlattice field. And given a nonlattice field, there is a constructive lattice closure that extends it as a constructive field.

    However it was in a comment, and Geoffrey Irving did not provide any proof of his statement, so I’ve opened up another MathOverflow question asking for a proof of Geoffrey Irving’s statement here.

  11. I have sent an email to Toby Bartels regarding his 2010 definition of an ordered field, but Toby Bartels have a weird email system so hopefully I didn’t do anything incorrectly and the email successfully gets through to them.

  12. I just realised that there is another aspect of the definitions in my given sources that isn’t included in the definition of the article: They also define an ordered field to be a Heyting field, with respect to the canonical tight apartness relation defined by a#b≔a<b∨b<aa \# b \coloneqq a \lt b \vee b \lt a.

  13. What is probably better for this article is to keep the original definition that Toby Bartels gave for the definition of an ordered field in classical mathematics, and then create a section on constructive notions of ordered fields, similar to what was done in the field article on the nLab.

    It will either be the case that the constructive definition is much more complicated than the classical definition (assuming that every definition found in the literature is equivalent to the definitions in the HoTT Book and the thesis), or there will be at least two inequivalent definition of an ordered field in constructive mathematics. Both cases would need significant amounts of text explaining why the classical definition is insufficient and why the extra structure is needed, and additionally in the second case, how the definitions relate to each other.

    • CommentRowNumber14.
    • CommentAuthorJoseph
    • CommentTimeJul 5th 2022

    going ahead and adding material about ordered fields in constructive mathematics as discussed in the nForum

    diff, v10, current

    • CommentRowNumber15.
    • CommentAuthorJoseph
    • CommentTimeJul 5th 2022

    Adding the references named on the nForum

    diff, v10, current

    • CommentRowNumber16.
    • CommentAuthorGuest
    • CommentTimeJul 6th 2022

    François G. Dorais proved here that any Cauchy complete Archimedean ordered field without a lattice structure has a lattice structure, so the extra axioms for the lattice structure in the HoTT book are unnecessary.

    The Cauchy real numbers can be constructively proven to satisfy the fundamental theorem of algebra, so one could define the lattice structure on the Cauchy reals from the absolute value, from the square root function, from the FTA.

    I think that just about wraps up all the important ordered fields which have a lattice structure.

  17. the nlab article on strict total order explicitly states that the MacNeille real numbers do not form a strict total order, and are thus by definition not an ordered field.

    Anonymous

    diff, v11, current

    • CommentRowNumber18.
    • CommentAuthorGuest
    • CommentTimeJul 9th 2022

    non-Archimedean Heyting ordered fields do not necessarily have an absolute value function. See for instance the real.numbers used in smooth infinitesimal analysis, as well as the surreal numbers

  19. There are actually two different ways to define an ordered field in constructive mathematics, depending on whether the apartness relation of an ordered local ring is tight or logically equivalent to negation of equality. The former is commonly used in real analysis with the Dedekind real numbers, while the latter is used in synthetic differential geometry.

    diff, v23, current

1 to 19 of 19

  1.