Automorphisms of P(ω)/fin

DefinitionEquality modulo finite sets#✓fully proved

Subsets \(A\) and \(B\) of \(\mathbb{N}\) are equal modulo finite, written \(A =^{\ast} B\), if their symmetric difference \(A \mathbin{\triangle} B\) is finite.

def EqModFinite (A B : Set ℕ) : Prop := (symmDiff A B).Finite

Used by 1

Used byAutomorphisms of P(ω)/fin on representatives

StructureAutomorphisms of P(ω)/fin on representatives#✓fully proved

For subsets \(A\), \(B\) of \(\mathbb{N}\), write \(A =^{\ast} B\) when their symmetric difference is finite. A map \(\Phi\) from subsets of \(\mathbb{N}\) to subsets of \(\mathbb{N}\) presents an automorphism of \(P(\omega)/\mathrm{fin}\) if for all subsets \(A\), \(B\) of \(\mathbb{N}\): it respects \(=^{\ast}\) (\(A =^{\ast} B\) implies \(\Phi(A) =^{\ast} \Phi(B)\)), it preserves meets (\(\Phi(A \cap B) =^{\ast} \Phi(A) \cap \Phi(B)\)) and complements (\(\Phi(\mathbb{N} \setminus A) =^{\ast} \mathbb{N} \setminus \Phi(A)\)), it is one-to-one modulo finite (\(\Phi(A) =^{\ast} \Phi(B)\) implies \(A =^{\ast} B\)), and it is onto modulo finite (for every \(B\) there is \(A\) with \(\Phi(A) =^{\ast} B\)).

structure IsPowModFiniteAutomorphism (Φ : Set ℕ → Set ℕ) : Prop where
  respects : ∀ A B : Set ℕ, EqModFinite A B → EqModFinite (Φ A) (Φ B)
  inter : ∀ A B : Set ℕ, EqModFinite (Φ (A ∩ B)) (Φ A ∩ Φ B)
  compl : ∀ A : Set ℕ, EqModFinite (Φ Aᶜ) (Φ A)ᶜ
  injective : ∀ A B : Set ℕ, EqModFinite (Φ A) (Φ B) → EqModFinite A B
  surjective : ∀ B : Set ℕ, ∃ A : Set ℕ, EqModFinite (Φ A) B

Uses 1

Statement usesEquality modulo finite sets

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.