Relation norms and Galois–Tukey morphisms

The definitions and inequalities in the preliminary section of the manuscript. The direction of a morphism agrees with that section: a morphism from A to B gives B.norm ≤ A.norm.

structure NonMRR.Relation : Type (u + 1)

A relation whose every challenge has a response.

• Challenge : Type u

  The objects that must be solved.

• Response : Type u

  The potential solutions to challenges.

• relates : self.Challenge → self.Response → Prop

  Whether a response solves a challenge.

• total (x : self.Challenge) : ∃ (y : self.Response), self.relates x y

def NonMRR.Relation.Dominating (A : Relation) (s : Set A.Response) : Prop

A family of responses solving every challenge.

Equations

• A.Dominating s = ∀ (x : A.Challenge), ∃ y ∈ s, A.relates x y

noncomputable def NonMRR.Relation.norm (A : Relation) : Cardinal.{u}

The least cardinality of a dominating family.

Equations

• A.norm = sInf {κ : Cardinal.{?u.1} | ∃ (s : Set A.Response), A.Dominating s ∧ Cardinal.mk ↑s = κ}

theorem NonMRR.Relation.dominating_univ (A : Relation) : A.Dominating Set.univ

theorem NonMRR.Relation.norm_le (A : Relation) {s : Set A.Response} (hs : A.Dominating s) : A.norm ≤ Cardinal.mk ↑s

theorem NonMRR.Relation.exists_dominating_of_norm (A : Relation) : ∃ (s : Set A.Response), A.Dominating s ∧ Cardinal.mk ↑s = A.norm

structure NonMRR.Relation.Morphism (A B : Relation) : Type u

The contravariant challenge map and covariant response map of a morphism.

• challenge : B.Challenge → A.Challenge

  Pull a target challenge back to the source relation.

• response : A.Response → B.Response

  Send a source response to the target relation.

• map_rel (x : B.Challenge) (y : A.Response) : A.relates (self.challenge x) y → B.relates x (self.response y)

theorem NonMRR.Relation.Morphism.dominating_image {A B : Relation} (f : A.Morphism B) {s : Set A.Response} (hs : A.Dominating s) : B.Dominating (f.response '' s)

theorem NonMRR.Relation.Morphism.norm_le {A B : Relation} (f : A.Morphism B) : B.norm ≤ A.norm

Morphisms reverse the ordering of norms.

def NonMRR.Relation.sequential (A B : Relation) : Relation

The second challenge in a sequential composition depends on the first response.

Equations

• One or more equations did not get rendered due to their size.

theorem NonMRR.Relation.dominating_product {A B : Relation} {s : Set A.Response} {t : Set B.Response} (hs : A.Dominating s) (ht : B.Dominating t) : (A.sequential B).Dominating (s ×ˢ t)

theorem NonMRR.Relation.sequential_norm_le (A B : Relation) : (A.sequential B).norm ≤ A.norm * B.norm

The upper bound for sequential composition used in the manuscript.

theorem NonMRR.Relation.norm_le_of_sequential_morphism {A B C : Relation} (f : (A.sequential B).Morphism C) (hB : Cardinal.aleph0 ≤ B.norm) (hAB : A.norm ≤ B.norm) : C.norm ≤ B.norm

The purely cardinal final step of the argument.