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).
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeNov 19th 2016

    At overt space there was a remark that since the definition quantifies over “spaces”, the overtness of a single space might depend on the general meaning chosen for “space”, but that no example was known to the author. I added an example involving synthetic topology, which may not be quite what the author of that remark was thinking of, but which I think is interesting.

    • CommentRowNumber2.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeApr 2nd 2017
    • (edited Apr 2nd 2017)

    Added to overt space two examples: locales induced by topological spaces and spectra of commutative rings in which nilpotency is decidable. (I’ll add details of the spectrum example later.)

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeApr 2nd 2017

    I added a link to topological locale.

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 20th 2019

    Replace ‘subset’ with ‘subspace’ for generality’s sake (except in one case where the specificity was proper).

    diff, v15, current

    • CommentRowNumber5.
    • CommentAuthortphyahoo
    • CommentTimeFeb 18th 2020
    "2. Motivation
    Recall that a topological space X is compact if and only if, for every other space Y and any open subspace U of X×Y, the subspace

    is open in Y."

    This was not obvious to me. I asked about it on compact spaces page and Todd said this is proven in escardo 09, lemma 4.3. Can we add a pointer here, or otherwise make it easier to understand this fact?

    escardo 09:
    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeFeb 18th 2020
    • (edited Feb 18th 2020)

    Thanks that you are looking into this.

    After your request in the other thread I had already included an informal pointer here.

    But the proper way to do this is, of course. to add a decent Proposition-environment to compact space of the form

      +-- {: .num_defn #EscardoCharacterizationOfCompactness}
      ###### Proposition
      **(Escardo's characterization of compactness)**
      A topological space $X$ is compact precisely if...
      +-- {: .proof} 
      ###### Proof 

    and then link to that from the entry overt space by typing

      Notice that (by [this Prop.](compact+space#EscardoCharacterizationOfCompactness)) a [[topological space]] is _[[compact]]_ if an olny if ...

    You wanna try to do that edit? It would be a nice service to the community!

    • CommentRowNumber7.
    • CommentAuthortphyahoo
    • CommentTimeFeb 18th 2020
    For sure, I'll give it a shot.
    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 18th 2020

    I wouldn’t necessarily call it “Escardo’s characterization of compactness”. Just because it’s in his paper doesn’t mean it originated with him. (I’m not sure who should be credited, but in any case I think it might better be called something like “overt characterization of compactness”.)

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 29th 2020

    It's not the overt characterization but the dual-overt characterization; compact spaces are dual to overt spaces. But I believe that it predates overtness anyway.

    I'd call it a quantifier characterization. If you have some proposition with free variables that stand for points in topological spaces, such that the truth set of the proposition is open in the product space, and you universally quantify one of the variables, then is the truth set still open? If the variable that you quantified over stood for a point in a compact space, then Yes. (And only a compact space will guarantee that the answer is Yes no matter what the rest of the details are.)

    Escardó attributes this to Nachbin. But once you think of it, the proof is very follow-your-nose, especially if you already know the closed-projection characterization of compactness.

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 29th 2020

    I simply meant that (to me, anyway) the etymology of “overt” might serve to remind one that preservation of opens (under appropriate quantification) is taken to be primary. The rest of what you say is obviously true.

  1. moving redirects for overt locale, overt locales, open locale, open locales to article on locally positive locale


    diff, v19, current