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.
Pcf cofinality ideals and cutoff conventions
Statement
Assume AC. For a set of infinite regular cardinals and a cardinal , put
The first condition means that every member of is strictly less than . These are possibly improper ideals, increasing with the cutoff, and for one has . The singleton belongs to exactly when . If , then is proper.
Membership of in is equivalent to every ultrafilter on containing having . With , one has
The intersection of an empty family here is taken inside , hence equals ; in that case the dual is an improper filter family. No assertion is made here that a fixed ultrafilter of cofinality below must meet ; that later cutoff theorem needs directedness.
Facts & Assumptions
Given: AC, a set of infinite regular cardinals, a cardinal , and the displayed definitions.
The PCF transfer lemma proves the empty and singleton values, monotonicity, and finite-union preservation (Progressive products and true cofinality transfers, Statement).
An ultrafilter contains exactly one of each set and its complement (Characterisation of ultrafilters: every set or its complement).
Restriction to a support in an ultrafilter and extension from that support preserve the ultraproduct order and cofinality (Progressive products and true cofinality transfers, Statement, support-restriction clause).
AC is assumed, as in the PCF transfer lemma (The Axiom of Choice).
Proof
Since , the empty set belongs to . If belongs and , monotonicity gives . If both belong, finite-union preservation gives . Thus it is an ideal; the same argument with gives . Larger cutoffs enlarge the ideals because the corresponding ordinal intervals are nested. For , the statement does not depend on the ambient set, proving the restriction identity in both directions.
By the singleton calculation, , so its membership is exactly , including failure at the endpoint . If , then , so . If is empty, its only ideal here is , improper on the empty support. For nonempty and or , the singleton calculation and monotonicity show that only the empty subset is null, since all coordinates are infinite. For a finite , the same calculation gives exactly .
Suppose first that and is an ultrafilter on containing . Restrict to ; by the support isomorphism its product cofinality is unchanged and belongs to , hence is below . Conversely, if every such has cofinality below , any ultrafilter on extends to one on supported on with the same cofinality. Thus every member of is below , proving membership. For both the universal ultrafilter assertions are vacuous and membership was proved in step 1.1.
A set belongs to every ultrafilter of cofinality at least exactly when none of those ultrafilters contains , by the complementary-pair law in F2. By step 2.1 this is exactly , or . This proves both inclusions in the dual identity. If there are no high-cofinality ultrafilters, step 2.1 with puts in the ideal, so the ideal and its dual are both ; the empty-intersection convention gives the same result. No witnesses are chosen in these computations beyond the AC-dependent facts already proved in F1. QED.
Depends on
- Characterisation of ultrafilters: every set or its complement
- Progressive products and true cofinality transfers
- The Axiom of Choice
- $\operatorname{cf}(\alpha) \le \alpha$; $\operatorname{cf}(0) = 0$ and $\operatorname{cf}(\alpha + 1) = 1$; for a limit ordinal $\lambda$ the value $\operatorname{cf}(\lambda)$ is an infinite cardinal with $\operatorname{cf}(\operatorname{cf}(\lambda)) = \operatorname{cf}(\lambda)$, so it is regular; and every cofinal subset of $\lambda$ has cardinality at least $\operatorname{cf}(\lambda)$, a value that is attained
- $\aleph_0$ is regular in ZF; assuming the Axiom of Choice every successor aleph $\aleph_{\alpha+1}$ is regular; $\operatorname{cf}(\aleph_\omega) = \aleph_0$, so $\aleph_\omega$ is singular, and under choice it is the least singular infinite cardinal
- Transfinite recursion
- Commutativity, associativity, distributivity and monotonicity of $\oplus$ and $\otimes$, the unit laws, the two exponent laws, and $\kappa \le \lambda$ if and only if $\kappa$ injects into $\lambda$
- Absorption: for cardinals $\kappa, \lambda$ with $\kappa$ infinite and $\lambda \le \kappa$, $\kappa \oplus \lambda = \kappa$, and $\kappa \otimes \lambda = \kappa$ when $\lambda \ne 0$
Used by
- Universal pcf sequences have strong increase and exact bounds Lemma
- Pcf cofinality ideals have single generators Theorem
- Pcf generators restrict, finitely cover, and carry scales Theorem
- Pcf has no holes for progressive intervals Theorem
- Pcf ideal directedness and ultrafilter cofinality cutoffs Theorem
- Progressive pcf has a maximum and continuous cutoff ideals Theorem
- Progressive pcf has universally cofinal sequences Theorem
Dependency tree · two levels
43 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Abraham and Magidor, Cardinal Arithmetic, §3.1 opening definitions and dual-filter identity, p. 32 (standard reference, not scraped)