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 comma 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 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.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 23rd 2016

    I created a short entry Banach-Alaoglu theorem to fulfil a grey link. While the general theorem is equivalent to the Tychonoff theorem for Hausdorff spaces, the case of separable Banach spaces is constructive. I do wonder how constructive, but apparently this gets used to construct solutions to PDEs, so I guess it’s quite concrete.

    • CommentRowNumber2.
    • CommentAuthorDaniel Luckhardt
    • CommentTimeAug 23rd 2016
    • (edited Aug 23rd 2016)

    Perhaps it’s worth noting that even in the non-separable case the Axiom of choice is not required for the proof: it bases on the product X[1,1]\prod_X [-1,1]. As discussed here in Remark 2.1 Tychonoff’s theorem holds without AC in this case as [1,1][-1,1] is Hausdorff.

    • CommentRowNumber3.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 23rd 2016

    You still need the ultrafilter principle/theorem though, which is where I found the needed link to the page on the B-A theorem.

  1. Thank you, I wasn’t aware of this subtlety. But what about this rescue of Tychonov’s theorem:

    In the case of an product of intervals I j\prod I_j we use Definition 2.5:

    1. Given any proper filter 𝒰\mathcal{U} on I j\prod I_j.
    2. For each jj take the infimum x jx_j of all cluster points of pr j(𝒰)pr_j (\mathcal{U}). This is again a cluster point.
    3. The point x=(x j)I jx = (x_j)\in \prod I_j is now a cluster point of 𝒰\mathcal{U}.

    For the second step: take any neighborhood BB of x jx_j. It contains a neighborhood of some cluster point of pr j(𝒰)pr_j (\mathcal{U}). Hence the intersection of any set in pr j(𝒰)pr_j (\mathcal{U}) with BB is inhabited.

    For the last step in this argument: it is obvious that for any neighborhood AA belonging to the subbase of the topology of I j\prod I_j consisting of all preimages of all open sets under all projection maps it holds that A=pr j 1BA = pr_j^{-1} B has nonempty intersection with every U𝒰U \in \mathcal{U} as B jpr j(U)B_j \cap pr_j(U) is inhabited. This holds also for finite intersection A=A 1A nA = A_1\cap \ldots \cap A_n. Finally, it holds for products.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 23rd 2016

    Wait, are you claiming that the Tychonoff theorem for products of intervals doesn’t require the ultrafilter principle?

    I think the ultrafilter principle should follow from the Tychonoff theorem for intervals. If the power I JI^J is compact for any set JJ, then so is the power 2 J2^J (being a closed subspace). But it is not hard to prove the Boolean prime ideal theorem from compactness of 2 J2^J, and this is equivalent to the ultrafilter principle.

  2. You are right. The last step in my proof is actually wrong.

    • CommentRowNumber7.
    • CommentAuthorspitters
    • CommentTimeAug 30th 2016

    I’ve added some links to the constructive literature, both Bishop and locales. I haven’t traced everything back to the original sources yet.

    • CommentRowNumber8.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 30th 2016

    Thanks, Bas!