Tukey reducibility and cofinal types

DefinitionTukey reducibility#✓fully proved

For preordered sets \(D\) and \(E\), \(D\) is Tukey reducible to \(E\), written \(D \le_T E\), if there is a map \(f \colon D \to E\) that carries unbounded sets to unbounded sets: for every \(A \subseteq D\) with no upper bound in \(D\), the image \(f[A]\) has no upper bound in \(E\).

def TukeyLE (D E : Type) [Preorder D] [Preorder E] : Prop :=
  ∃ f : D → E, ∀ A : Set D, (¬ ∃ b : D, ∀ a ∈ A, a ≤ b) → ¬ ∃ b : E, ∀ a ∈ f '' A, a ≤ b

Used by 2

Used byCofinal type · Tukey equivalence

DefinitionTukey equivalence#✓fully proved

Preordered sets \(D\) and \(E\) are Tukey equivalent (cofinally equivalent), written \(D \equiv_T E\), if \(D \le_T E\) and \(E \le_T D\), where \(\le_T\) is Tukey reducibility.

def TukeyEquiv (D E : Type) [Preorder D] [Preorder E] : Prop := TukeyLE D E ∧ TukeyLE E D

Uses 1 · Used by 1

Statement usesTukey reducibility

Used byCofinal type

DefinitionCofinal type#✓fully proved

A cofinal type is an equivalence class of preordered sets under Tukey equivalence \(\equiv_T\), where \(D \equiv_T E\) means \(D \le_T E\) and \(E \le_T D\) (Tukey reducibility in both directions).

def CofinalType : Type 1 :=
  Quotient (α := Σ D : Type, Preorder D)
    { r := fun X Y => @TukeyEquiv X.1 Y.1 X.2 Y.2
      iseqv := by
        refine ⟨fun X => ⟨⟨id, fun A hA => by rwa [Set.image_id]⟩,
                          ⟨id, fun A hA => by rwa [Set.image_id]⟩⟩,
                fun h => ⟨h.2, h.1⟩, fun h1 h2 => ⟨?_, ?_⟩⟩
        · obtain ⟨f, hf⟩ := h1.1
          obtain ⟨g, hg⟩ := h2.1
          exact ⟨g ∘ f, fun A hA => by rw [Set.image_comp]; exact hg (f '' A) (hf A hA)⟩
        · obtain ⟨f, hf⟩ := h2.2
          obtain ⟨g, hg⟩ := h1.2
          exact ⟨g ∘ f, fun A hA => by rw [Set.image_comp]; exact hg (f '' A) (hf A hA)⟩ }

Uses 2

Statement usesTukey equivalence · Tukey reducibility

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.