analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Basic concepts
fiber space, space attachment
Extra stuff, structure, properties
Kolmogorov space, Hausdorff space, regular space, normal space
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
Examples
Basic statements
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
open subspaces of compact Hausdorff spaces are locally compact
compact spaces equivalently have converging subnet of every net
continuous metric space valued function on compact metric space is uniformly continuous
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
injective proper maps to locally compact spaces are equivalently the closed embeddings
locally compact and second-countable spaces are sigma-compact
Theorems
Analysis Theorems
A proper filter is equivalently the eventuality filter of a net.
In predicative mathematics, filters of subsets are large, but locally small.
A subset of a poset is called a filter if it is upward-closed and downward-directed; that is:
Equivalently, a predicate is a filter
One could also use a -overt dominance , a sub--frame . A predicate is a filter
Sometimes the term ‘filter’ is used for an upper set, that is any set satisfying axiom (1). (Ultimately this connects with the use of ‘ideal’ in monoid theory.)
In a lattice, one can use these alternative axioms:
Here, (1) is equivalent to the previous version; the others, which here say that the lattice is closed under finite meets, are equivalent given (1). (These axioms look more like the axioms for an ideal of a ring.)
You can also interpret these axioms to say that, if you think of as a function from to the set of truth values, then is a homomorphism of meet-semilattices.
A filter of subsets of a given set is a filter in the power set of . One also sees filters of open subsets, filters of compact subsets, etc, especially in topology.
In dependent type theory, let be the type of all propositions with its type reflector type family. Given a type , the type of all subsets of is given by the function type . We define the relation by
Let be a poset. Then a filter on is a subtype with dependent functions
The filter properties could also be turned into structure:
A filter is proper if there exists an element of such that . A filter in a lattice is proper iff ; in particular, a filter of subsets of is proper iff . In constructive mathematics, however, one usually wants a stronger (but classically equivalent) notion: a filter of subsets of is proper if every element of is inhabited. If for every (in particular if ), then we have the improper filter. Compare proper subset and improper subset.
Filters are often assumed to be proper by default in analysis and topology, where proper filters correspond to nets. However, we will try to remember to include the adjective ‘proper’.
If the complement of a filter is an ideal, then we say that the filter is prime (and equivalently that the ideal is prime). A prime filter is necessarily proper; a proper filter in a lattice is prime iff, whenever , either or . In other words, must be a homomorphism of lattices. The generalisation to arbitrary joins gives a completely prime filter.
A filter is an ultrafilter, or maximal filter, if it is maximal among the proper filters. (See that article for alternative formulations and applications.) In a distributive lattice, every ultrafilter is prime; the converse holds in a Boolean lattice. In this case, we can say that is a homomorphism of Boolean lattices.
Given an element of , the principal ultrafilter (of subsets of ) at consists of every subset of to which belongs. A principal ultrafilter is also called a fixed ultrafilter; more generally, a filter of subsets is fixed if its intersection is inhabited. In contrast, if is an filter whose meet (of all elements) exists and is a bottom element (the empty set for a filter of subsets), then we call free.
Free ultrafilters on Boolean algebras are important in nonstandard analysis and model theory.
A subset of a lattice is a filterbase if it becomes a filter when closed under axiom (1). Equivalently, a filterbase is any downward-directed subset. Any subset of a meet-semilattice may be used as a filter subbase; form a filterbase by closing under finite meets.
A filterbase of sets is proper (that is, it generates a proper filter of sets) iff each set in is inhabited. A filter subbase of sets is proper iff it satisfies the finite intersection property (well known in topology from a criterion for compact spaces): every finite collection from the subfilter has inhabited intersection.
If is a monotone map and a filter, then is a filter base. Let be the filter generated by this filter base. The set of filters is a poset in its own right w.r.t. inclusion and is monotone. Therefore is a functor from the category of posets to itself.
If satisfies stronger properties than mere monotony, then will be better behaved as well:
If is a meet-semilattice, then is a complete join-semilattice: . If respects finite meets, then respects all joins. If is merely monotone, then respects all filtered joins.
If has all -fold joins for some indexing set , then has -fold meets: . If respects -fold joins, then respects -fold meets.
If is a distributive lattice, then is a frame, i.e. the infinite distributive law holds. The other distributive law also holds for finite meets: if is finite. It holds more generally if has all -fold meets, the -fold distributive law holds in and is closed under -fold meets.
If is a complete join-semilattice, then is a complete lattice. If respects all joins, then respects all meets. In this case has a left adjoint which is given by so that holds. As a left adjoint respects all joins.
If is an adjoint pair between and , that is f, monotone and for all , , then is an adjoint pair between and . Note that the push-forward turns left adjoints into right adjoint and vice versa.
Every net defines an eventuality filter : let belong to if, for some index , for every , . (That is, is eventually in .) Note that is proper; conversely, any proper filter has a net whose eventuality filter is (as described at net). Everything below can be done for nets as well as for (proper) filters, but filters often lead to a cleaner theory.
In a topological space , a filter on converges to a point of if every neighbourhood of belongs to . A filter clusters at a point if every neighbourhood of intersects every element of . With these definitions, the improper filter converges to every point and clusters at no point; a proper filter, however, clusters at every point that it converges to.
The concepts of continuous function and such conditions as compactness and Hausdorffness may be defined quite nicely in terms of the convergence relation. In fact, everything about topological spaces may be defined in terms of the convergence relation, although not always nicely. This is because topological spaces form a full subcategory of the category of convergence spaces, where the convergence relation is the fundamental concept. More details are there.
In a metric space , a filter on is Cauchy if it has elements of arbitrarily small diameter. Then a sequence is a Cauchy sequence iff its eventuality filter is Cauchy. (This can be generalised to uniform spaces.) The concept of completion of a metric space may be defined quite nicely in terms of the Cauchy filters, although not every property (not even every uniform property) of metric spaces can be defined in this way. As for convergence, there is a general notion of Cauchy space, but the forgetful functors from metric and uniform spaces are now not full.
upper set/(0,1)-copresheaf, filter/(0,1)-cosheaf?
Last revised on November 13, 2024 at 01:29:55. See the history of this page for a list of all contributions to it.