ZFC foundations used by the Wallace construction

This file records the parts of the set-theoretic and topological construction that can be checked directly against mathlib. In particular, it proves the ultrafilter extension step and the basic facts about the initial topology generated by a family of circle-valued characters.

No declaration in this file is an axiom and no proof is omitted.

Families with the finite-intersection property

theorem Wallace.exists_free_ultrafilter_le_filter {α : Type u} (l : Filter α) [l.NeBot] (hl : l ≤ Filter.cofinite) : ∃ (p : Ultrafilter α), ↑p ≤ l ∧ ↑p ≤ Filter.cofinite

Any proper filter extending the cofinite filter admits a free ultrafilter refinement.

Cardinal bookkeeping for the continuum-indexed free group

theorem Wallace.aleph0_lt_cof_continuum : Cardinal.aleph0 < Cardinal.continuum.ord.cof

König's theorem gives the strict uncountable cofinality of the continuum. This is the precise fact used to bound a countable union of supports below the initial ordinal of 𝔠.

A continuum-sized almost-disjoint family

@[reducible, inline]

abbrev Wallace.BinaryTreeNode : Type

A concrete node on the binary tree: a level and the values below that level.

Equations

• Wallace.BinaryTreeNode = ((n : ℕ) × (Fin n → Bool))

def Wallace.binaryPrefix (x : ℕ → Bool) (n : ℕ) : BinaryTreeNode

The length-n initial segment of a binary stream.

Equations

• Wallace.binaryPrefix x n = ⟨n, fun (i : Fin n) => x ↑i⟩

def Wallace.binaryBranch (x : ℕ → Bool) : Set BinaryTreeNode

The branch through the binary tree associated to a stream.

Equations

• Wallace.binaryBranch x = Set.range (Wallace.binaryPrefix x)

theorem Wallace.binaryPrefix_injective (x : ℕ → Bool) : Function.Injective (binaryPrefix x)

theorem Wallace.binaryBranch_infinite (x : ℕ → Bool) : (binaryBranch x).Infinite

Every branch is infinite.

theorem Wallace.eq_on_Iio_of_binaryPrefix_eq {x y : ℕ → Bool} {m n : ℕ} (h : binaryPrefix x m = binaryPrefix y n) : m = n ∧ ∀ k < m, x k = y k

If two branches share a node at level n, then their streams agree below n.

theorem Wallace.binaryBranch_inter_finite {x y : ℕ → Bool} (hxy : x ≠ y) : (binaryBranch x ∩ binaryBranch y).Finite

Distinct binary streams define branches with finite intersection.

theorem Wallace.binaryTreeNode_infinite : Infinite BinaryTreeNode

The binary-tree node type is infinite.

def Wallace.binaryTreeNodeEquivNat : BinaryTreeNode ≃ ℕ

A fixed identification of the countably infinite binary tree with ℕ.

Equations

• Wallace.binaryTreeNodeEquivNat = Denumerable.eqv Wallace.BinaryTreeNode

def Wallace.binaryBranchOnNat (x : ℕ → Bool) : Set ℕ

The same branch family, transported to an almost-disjoint family literally on ℕ.

Equations

• Wallace.binaryBranchOnNat x = ⇑Wallace.binaryTreeNodeEquivNat '' Wallace.binaryBranch x

theorem Wallace.binaryBranchOnNat_infinite (x : ℕ → Bool) : (binaryBranchOnNat x).Infinite

theorem Wallace.binaryBranchOnNat_inter_finite {x y : ℕ → Bool} (hxy : x ≠ y) : (binaryBranchOnNat x ∩ binaryBranchOnNat y).Finite

A reusable transfinite-iteration fact