Degrees as equivalence classes

Cresswell builds degrees from a comparison instead of assuming them. Two entities are indistinguishable under a comparison φ when they stand in φ to the same entities on both sides, the degrees are the classes of indistinguishable entities, and φ induces a well-defined comparison on them. On a preorder the construction is mathlib's Antisymmetrization, and on an equivalence relation it returns the cells of the partition.

Main definitions

• Degree.cresswellSetoid: indistinguishability under a comparison.
• Degree.CresswellDegree: the degrees of a comparison.

Main statements

• Degree.cresswellSetoid_le_iff: on a preorder the construction is Antisymmetrization.
• Degree.cresswellSetoid_setoid: on an equivalence relation the construction returns the relation itself.

References

• [Cre76]

def Degree.cresswellSetoid {E : Type u_1} (φ : E → E → Prop) : Setoid E

Two pairs are indistinguishable under a comparison φ when they have the same φ-profile on the left and on the right, [Cre76] (4.1).

Equations

• Degree.cresswellSetoid φ = { r := fun (a b : E) => (∀ (c : E), φ a c ↔ φ b c) ∧ ∀ (c : E), φ c a ↔ φ c b, iseqv := ⋯ }

@[reducible, inline]

abbrev Degree.CresswellDegree {E : Type u_1} (φ : E → E → Prop) : Type u_1

Degrees of comparison as φ-equivalence classes ([Cre76] (4.1)).

Equations

• Degree.CresswellDegree φ = Quotient (Degree.cresswellSetoid φ)

@[instance_reducible]

instance Degree.instLTCresswellDegree {E : Type u_1} {φ : E → E → Prop} : LT (CresswellDegree φ)

The comparison a relation induces on its degrees, ⟦a⟧ < ⟦b⟧ iff φ b a, strict exactly when φ is; well-definedness is [Cre76]'s own consistency proof for (4.2).

Equations

• Degree.instLTCresswellDegree = { lt := Quotient.lift₂ (fun (a b : E) => φ b a) ⋯ }

@[simp]

theorem Degree.CresswellDegree.mk_lt_mk {E : Type u_1} {φ : E → E → Prop} {a b : E} : ⟦a⟧ < ⟦b⟧ ↔ φ b a

The degree of a exceeds that of b exactly when φ(a, b), [Cre76] (4.2).

theorem Degree.cresswellSetoid_le_iff {E : Type u_1} [Preorder E] (a b : E) : (cresswellSetoid fun (x1 x2 : E) => x1 ≤ x2) a b ↔ AntisymmRel (fun (x1 x2 : E) => x1 ≤ x2) a b

On a preorder, φ-indistinguishability under ≤ is AntisymmRel, so the Cresswell quotient is Antisymmetrization.

theorem Degree.cresswellSetoid_setoid {E : Type u_1} (s : Setoid E) : cresswellSetoid ⇑s = s

On an equivalence relation, φ-indistinguishability is the relation itself, so the construction returns the cells of a partition as well as degrees.