Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
  
  
• Remember me

• Forgot your password?
• Apply for membership

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

1. • CommentRowNumber1.
   • CommentAuthorDavidRoberts
   • CommentTimeAug 23rd 2016
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI 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.

   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.

2. • CommentRowNumber2.
   • CommentAuthorDaniel Luckhardt
   • CommentTimeAug 23rd 2016
   • (edited Aug 23rd 2016)
   • PermaLink
   Author: Daniel Luckhardt
   Format: MarkdownItexPerhaps 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 $\prod_X [-1,1]$. As discussed [[Tychonoff theorem|here in Remark 2.1]] Tychonoff's theorem holds without AC in this case as $[-1,1]$ is Hausdorff.

   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 . As discussed here in Remark 2.1 Tychonoff’s theorem holds without AC in this case as is Hausdorff.

3. • CommentRowNumber3.
   • CommentAuthorDavidRoberts
   • CommentTimeAug 23rd 2016
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexYou still need the [[ultrafilter theorem|ultrafilter principle/theorem]] though, which is where I found the needed link to the page on the B-A theorem.

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

4. • CommentRowNumber4.
   • CommentAuthorDaniel Luckhardt
   • CommentTimeAug 23rd 2016
   • PermaLink
   Author: Daniel Luckhardt
   Format: MarkdownItexThank 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 $\prod I_j$ we use [[compact+space#definitions|Definition 2.5]]: 1. Given any proper filter $\mathcal{U}$ on $\prod I_j$. 1. For each $j$ take the infimum $x_j$ of all cluster points of $pr_j (\mathcal{U})$. This is again a cluster point. 1. The point $x = (x_j)\in \prod I_j$ is now a cluster point of $\mathcal{U}$. For the second step: take any neighborhood $B$ of $x_j$. It contains a neighborhood of some cluster point of $pr_j (\mathcal{U})$. Hence the intersection of any set in $pr_j (\mathcal{U})$ with $B$ is inhabited. For the last step in this argument: it is obvious that for any neighborhood $A$ belonging to the subbase of the topology of $\prod I_j$ consisting of all preimages of all open sets under all projection maps it holds that $A = pr_j^{-1} B $ has nonempty intersection with every $U \in \mathcal{U}$ as $B_j \cap pr_j(U)$ is inhabited. This holds also for finite intersection $A = A_1\cap \ldots \cap A_n$. Finally, it holds for products.

   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 we use Definition 2.5:

   1. Given any proper filter on .
   2. For each take the infimum of all cluster points of . This is again a cluster point.
   3. The point is now a cluster point of .

   For the second step: take any neighborhood of . It contains a neighborhood of some cluster point of . Hence the intersection of any set in with is inhabited.

   For the last step in this argument: it is obvious that for any neighborhood belonging to the subbase of the topology of consisting of all preimages of all open sets under all projection maps it holds that has nonempty intersection with every as is inhabited. This holds also for finite intersection . Finally, it holds for products.

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 23rd 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexWait, 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^J$ is compact for any set $J$, then so is the power $2^J$ (being a closed subspace). But it is not hard to prove the Boolean prime ideal theorem from compactness of $2^J$, and this is equivalent to the ultrafilter principle.

   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 is compact for any set , then so is the power (being a closed subspace). But it is not hard to prove the Boolean prime ideal theorem from compactness of , and this is equivalent to the ultrafilter principle.

6. • CommentRowNumber6.
   • CommentAuthorDaniel Luckhardt
   • CommentTimeAug 23rd 2016
   • PermaLink
   Author: Daniel Luckhardt
   Format: MarkdownItexYou are right. The last step in my proof is actually wrong.

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

7. • CommentRowNumber7.
   • CommentAuthorspitters
   • CommentTimeAug 30th 2016
   • PermaLink
   Author: spitters
   Format: MarkdownItexI've added some links to the constructive literature, both Bishop and locales. I haven't traced everything back to the original sources yet.

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

8. • CommentRowNumber8.
   • CommentAuthorDavidRoberts
   • CommentTimeAug 30th 2016
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexThanks, Bas!

   Thanks, Bas!