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 have single generators
Statement
Assume AC. For a nonempty progressive set of infinite regular cardinals and there is such that
For any , this equality holds if and only if and every ultrafilter on with contains . Such a generator is positive modulo and unique modulo that ideal. AC gives a simultaneous family . Neither smoothness nor transitivity of this family is asserted.
Facts & Assumptions
Given: AC, progressive , ; write and .
These are increasing ideals, is proper, and membership of in either is equivalent to its supported ultrafilter cofinalities satisfying the corresponding bound (Pcf cofinality ideals and cutoff conventions).
An ultrafilter has product cofinality exactly when it avoids and meets ; meeting is equivalent to cofinality below (Pcf ideal directedness and ultrafilter cofinality cutoffs).
There is a universal strict -sequence with a positive limit-valued exact bound everywhere, including finite supports (Universal pcf sequences have strong increase and exact bounds).
Exactness passes to larger proper ideals (Bounding projections produce an exact upper bound with large coordinate cofinalities).
Product ultrafilter cofinalities and true cofinalities are regular, and a strict cofinal chain of regular length has that true cofinality (Progressive products and true cofinality transfers).
AC chooses members simultaneously from nonempty sets (The Axiom of Choice).
Proof
First prove the criterion. If , then because . If has cofinality , F2 gives and . Now , so it is not in , and its complement is in . Intersecting with gives , hence . Conversely suppose and every cofinality- ultrafilter contains . For , any ultrafilter containing contains , so its cofinality is at most by F1. It cannot equal , since it then contains both and . Thus every such ultrafilter has cofinality below , and F1 gives . This proves . If , then because and is an ideal. Thus as well. The complementary-pair rule used here follows directly from maximality of a proper filter: if adjoining a missing set preserved properness it would contradict maximality, so some old member is disjoint from it.
Take from F3 and put . Every term satisfies : , and because is an infinite cardinal by F5. For an ultrafilter avoiding , its dual ideal contains and is proper. Thus the chain remains strict modulo . Its exactness transfers by F4 if is infinite. For finite the same transfer follows directly: for , reset to zero where it fails . The reset function is everywhere below positive , so exactness modulo makes it some . Returning the old values changes it only on an -small set, giving . This reset argument works for infinite too, and explains the transfer without requiring singleton-smallness.
Let contain . If it meets , F2 gives cofinality below . Otherwise step 1.2 applies. For any , on , so . Transferred exactness supplies with . Therefore the strict chain is cofinal in , and F5 makes its cofinality . Both cases give cofinality at most for every containing . The supported-ultrafilter test F1 therefore gives .
Let have cofinality . It avoids by F2. If , the complement belongs to by the rule proved in step 1.1. Define off and on . Off we have , and on we have , so . Step 1.2 gives for all . But universality from F3 supplies with , contradicting the strict reverse inequality on the nonempty intersection of two -large comparison sets. Hence .
Steps 2.1–2.2 meet the criterion of step 1.1, giving . A cofinality- ultrafilter exists by the hypothesis ; it contains and avoids , so and in particular . If also generates , then and the two generation equalities give and . Their union lies in . Conversely changing on an -small set does not change the condition , by taking the union with that small set in each direction. Finally is a set: ultrafilters on form a subset of , and Replacement collects their cofinalities. For each such the subsets of generating its ideal form a nonempty set by the proof above. Apply A1 to this indexed family to select all . No compatibility condition between distinct selections was used or follows from this choice. QED.
Depends on
- Progressive products and true cofinality transfers
- Pcf cofinality ideals and cutoff conventions
- Pcf ideal directedness and ultrafilter cofinality cutoffs
- Universal pcf sequences have strong increase and exact bounds
- Bounding projections produce an exact upper bound with large coordinate cofinalities
- 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
Dependency tree · two levels
49 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, Lemma 4.7 and Theorem 4.8, pp. 40–41 (standard reference, not scraped)