Ultrafilter: Free or Principal (ウルトラフィルターの二択) (Remark II.4.2)
- Ultrafilter: Free or Principal (ウルトラフィルターの二択) (Remark II.4.2) #Card
- ウルトラフィルターは分解定理からどう分類されるか。主ウルトラフィルターの形は？
An ultrafilter $\mathcal{U}$ is either principal or free. 分解 $\mathcal{U} = \mathcal{U}^* \wedge \mathcal{U}^\bullet$ と極大性から、$\mathcal{U} = \mathcal{U}^*$（自由部分のみ）か $\mathcal{U} = \mathcal{U}^\bullet$（主部分のみ）のどちらか。
- 主ウルトラフィルターは必ず $x^\uparrow$ の形: $\mathcal{U} = {A}^\uparrow$ で $A = A_0 \sqcup A_1$（両方非空）なら二分性より $A_0 \in \mathcal{U}$ または $A_1 \in \mathcal{U}$ となり ${A}^\uparrow$ に矛盾。よって $A$ は一点。
- 自由ウルトラフィルターの存在は選択公理に依存（構成的には作れない）。
Ultrafilter.eq_principal_iff 系；自由な場合は Ultrafilter.of cofinite の存在（choice 依存）