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 $\prod_X [-1,1]$. As discussed here in Remark 2.1 Tychonoff’s theorem holds without AC in this case as $[-1,1]$ 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 $\prod I_j$ we use Definition 2.5:

   1. Given any proper filter $\mathcal{U}$ on $\prod I_j$.
   2. For each $j$ take the infimum $x_j$ of all cluster points of $pr_j (\mathcal{U})$. This is again a cluster point.
   3. 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.

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

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!