How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
On finite sets the ultrafilter monad is naturally isomorphic to the identity; assuming the ultrafilter lemma, its unit is not invertible on the natural numbers
Example
On the full subcategory of finite sets, the principal-unit map is a natural isomorphism, so the ultrafilter monad restricts to the identity monad up to natural isomorphism. Assuming the ultrafilter lemma, this fails on .
Facts & Assumptions
Given: The ultrafilter monad of The ultrafilter endofunctor with principal unit and flattening multiplication and, for the infinite comparison only, the ultrafilter lemma.
An ultrafilter containing a finite union contains one of its members (Ultrafilters are prime: a union in has a member in ).
The principal map is natural, and the flattening map is the multiplication of the ultrafilter monad (The principal-ultrafilter and ultrafilter-flattening formulas are well-defined and natural; The ultrafilter endofunctor with principal unit and flattening multiplication is a monad).
Assuming the Axiom of Choice, every filter on a set is contained in an ultrafilter on that set (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter); a nonprincipal ultrafilter on then exists (FALSE, once the ultrafilter lemma is available: every ultrafilter is principal).
A filter contains the whole carrier, excludes the empty set, is upward closed, and is closed under finite intersections (Filter on a set).
A finite set is equinumerous with a natural number (The cardinality of a finite set), and an ultrafilter is in particular a proper filter (Ultrafilter).
Verification
If is nonempty and finite, [L5] makes its singleton partition finite, and its union belongs to every ultrafilter. Repeated use of [L1] selects a singleton , and no distinct singleton can also belong because their intersection is empty.
Upward closure now shows that the ultrafilter consists exactly of the subsets containing , namely . Thus is bijective for nonempty finite . If , no proper filter exists because the whole carrier is also empty, so and is again bijective.
Naturality in [L2] makes these bijections a natural isomorphism on finite sets. Under the identification, is the identity and sends the principal ultrafilter at to , so the restricted monad is naturally isomorphic to the identity monad.
Assuming [L3], let be the nonprincipal ultrafilter on supplied there. Every value of is principal, so is outside its image and that unit component is not invertible.
Depends on
- The ultrafilter endofunctor with principal unit and flattening multiplication
- The ultrafilter endofunctor with principal unit and flattening multiplication is a monad
- The principal-ultrafilter and ultrafilter-flattening formulas are well-defined and natural
- Ultrafilters are prime: a union in $\mathcal{U}$ has a member in $\mathcal{U}$
- Ultrafilter
- Filter on a set
- The cardinality $\lvert A\rvert$ of a finite set
- The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter
- FALSE, once the ultrafilter lemma is available: every ultrafilter is principal
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 60 results over 16 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.