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 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 nforum 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: locale of real numbers

Bottom of Page

1 to 16 of 16

  1.  

  1. Adding reference

    as a construction of the locale of real numbers can be found in section 5.3 of that article

    Anonymous

    diff, v20, current

  2. added brief section on the arithmetic/ring operations on the locale of real numbers.

    Anonymous

    diff, v20, current

  3. added reference:

    Anonymous

    diff, v25, current

    • CommentRowNumber4.
    • CommentAuthorGuest
    • CommentTimeJan 22nd 2023

    In section 5, it is stated that the join of two opens, defined as shown using the zig-zag lemma is also open.

    Let U n=(.92 n,12 n−1)U_n = (\frac{.9}{2^n}, \frac{1}{2^{n-1}}), and let EE be the union of the U 2nU_{2n} and let OO be the union of the U 2n−1U_{2n-1} as subsets of the the set of real numbers. It is clear that these are all open subsets of the set ℝ\mathbb{R} and therefore that their associated relations are opens in the locale ℝ\mathbb{R}. It seems that the join of EE and OO “contains” (a,b)(a,b) whenever 0<a<b<10 \lt a \lt b \lt 1, but (0,1)(0,1) is not “contained in” the join. Does this not contradict the 4th property opens in the locale of real numbers are required to satisfy?

    — Casey (guest)

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeJun 24th 2023
    • (edited Jun 24th 2023)

    Use ⋐\Subset instead of (incorrectly) ⊊\subsetneq.

    diff, v26, current

    ETA: The reason that ⊊\subsetneq is incorrect is that we have (for example) (0,1)⊊(0,2)(0,1) \subsetneq (0,2) but not (0,1)⋐(0,2)(0,1) \Subset (0,2), so rule (4) doesn't have its full strength with ⊊\subsetneq. (By the way, the intended meaning of ⋐\Subset is well-contained, that is U⋐VU \Subset V iff ClU⊆IntV\Cl U \subseteq \Int V.)

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeJun 24th 2023

    Casey in #5 is correct. The problem is that when I added the missing clause (4) in the definition of an open, I missed that there was a corresponding missing complication in the definition of a join. So now this is fixed.

    diff, v27, current

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeJun 24th 2023

    The proof of Heine–Borel also needs a slight modification.

    diff, v28, current

    • CommentRowNumber8.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 25th 2023

    In the section “Using the Dedekind real numbers”, it mentions defining a function f′f' on the locale, from a function ff on the set of Dedkind reals. Looks a bit too much like the derivative, to me.

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeJun 27th 2023

    @David # 8:

    That was done by the anonymous contributor from the edits announced at the top of the page. I certainly don't object to changing it. (In the long run, I'd like the page to have an elementary description of the continuous maps like it has for the opens etc.)

    • CommentRowNumber10.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 28th 2023

    Replaced f′f' notation as discussed, updated reference title after correcting MO question title spelling

    diff, v29, current

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeJun 29th 2023

    A stronger Zigzag Lemma, which I plan to use later.

    diff, v31, current

    • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeJun 29th 2023

    A result on measure, showing how the failure of measure theory in Russian constructivism (where the set of all real numbers has measure zero) can be avoided by working with the locale instead of the set of points.

    diff, v32, current

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeJun 29th 2023

    (This is what I needed the stronger version of the Zigzag Lemma for, by the way.)

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeJul 23rd 2023

    Cousin’s Lemma

    diff, v34, current

    • CommentRowNumber15.
    • CommentAuthorJohn Baez
    • CommentTimeNov 10th 2023

    My friend (and landlord here in Edinburgh) Michael Fourman has read this page with interest and may have some comments. He is carefully studying the work of Brouwer, and trying to rework some of it using topos theory.

  16. Added reference

    Anonymouse

    diff, v38, current

1 to 16 of 16

  1.