Comparison categories

A comparison category is a Finset Ordering — which of lt/eq/gt a pair of elements of a linear order may stand in. The atomic categories are the singletons (mathlib Ordering itself); unions like ≤/≥ are larger sets. holds s a b says the comparison of a and b falls in s.

This is framework-agnostic order theory (the point analogue of AllenRelation for intervals): it is generic over any [LinearOrder α] and bakes in no notion of time. Tense, evidential, and modal-base-time semantics each supply the order (Time) and name the categories they use (Tense.past = before, etc.).

Finset Ordering is the eight-element Boolean algebra 𝒫 {lt, eq, gt} — the Aristotelian diagram of the trichotomy, with the three singletons as atoms and ≤/≥/≠ as their joins. For each pair a, b, the map s ↦ holds s a b is its Stone-dual point-evaluation at compare a b: a BoundedLatticeHom into Prop (holdsHom, holds_sup/holds_inf/holds_compl/holds_top/ holds_bot). Together with converse (↦ SetRel.inv) and comp (↦ SetRel.comp) below, this exhibits holds as a homomorphism from the finite point algebra into the relation algebra SetRel α α, and makes the named categories' holds_* reductions corollaries of one morphism.

def Core.Order.holds {α : Type u_1} [LinearOrder α] (s : Finset Ordering) (a b : α) : Prop

A pair a, b stands in comparison category s iff compare a b is one of s's orderings.

Equations

• Core.Order.holds s a b = (compare a b ∈ s)

@[implicit_reducible]

instance Core.Order.instDecidableHolds {α : Type u_1} [LinearOrder α] (s : Finset Ordering) (a b : α) : Decidable (holds s a b)

Equations

• Core.Order.instDecidableHolds s a b = Core.Order.instDecidableHolds._aux_1 s a b

holds as a Boolean-algebra homomorphism

For each pair a, b, s ↦ holds s a b preserves the Boolean structure of Finset Ordering: it is point-evaluation of the membership relation at compare a b. These are the ∪/∩/ᶜ/⊤/⊥ half of the relation-algebra homomorphism (the converse/comp half is below).

@[simp]

theorem Core.Order.holds_sup {α : Type u_1} [LinearOrder α] (s t : Finset Ordering) (a b : α) : holds (s ⊔ t) a b ↔ holds s a b ∨ holds t a b

@[simp]

theorem Core.Order.holds_inf {α : Type u_1} [LinearOrder α] (s t : Finset Ordering) (a b : α) : holds (s ⊓ t) a b ↔ holds s a b ∧ holds t a b

@[simp]

theorem Core.Order.holds_compl {α : Type u_1} [LinearOrder α] (s : Finset Ordering) (a b : α) : holds sᶜ a b ↔ ¬holds s a b

@[simp]

theorem Core.Order.holds_top {α : Type u_1} [LinearOrder α] (a b : α) : holds ⊤ a b ↔ True

@[simp]

theorem Core.Order.holds_bot {α : Type u_1} [LinearOrder α] (a b : α) : holds ⊥ a b ↔ False

def Core.Order.holdsHom {α : Type u_1} [LinearOrder α] : BoundedLatticeHom (Finset Ordering) (α → α → Prop)

holds, bundled. For every [LinearOrder α], the map s ↦ fun a b => holds s a b is a BoundedLatticeHom from the eight-element Boolean algebra Finset Ordering (= 𝒫 {lt, eq, gt}) into the relation algebra α → α → Prop — the Stone-dual evaluation of the comparison-category algebra. With converse (holds_converse) and comp (holds_comp) it is the point algebra's image in the concrete relation algebra.

Equations

• Core.Order.holdsHom = { toFun := fun (s : Finset Ordering) (a b : α) => Core.Order.holds s a b, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }

@[simp]

theorem Core.Order.holdsHom_apply {α : Type u_1} [LinearOrder α] (s : Finset Ordering) (a b : α) : holdsHom s a b = holds s a b

Named comparison categories

The three atoms are the singletons before/overlapping/after; every other category is a Boolean combination of them, so the composite holds_* reductions below are corollaries of holds_sup, not separate compare-inspections.

def Core.Order.before : Finset Ordering

a < b (atom lt).

Equations

• Core.Order.before = {Ordering.lt}

def Core.Order.after : Finset Ordering

a > b (atom gt).

Equations

• Core.Order.after = {Ordering.gt}

def Core.Order.overlapping : Finset Ordering

a = b, points overlap (atom eq).

Equations

• Core.Order.overlapping = {Ordering.eq}

def Core.Order.notAfter : Finset Ordering

a ≤ b — the join before ⊔ overlapping.

Equations

• Core.Order.notAfter = Core.Order.before ⊔ Core.Order.overlapping

def Core.Order.notBefore : Finset Ordering

a ≥ b — the join after ⊔ overlapping.

Equations

• Core.Order.notBefore = Core.Order.after ⊔ Core.Order.overlapping

def Core.Order.distinct : Finset Ordering

a ≠ b — the join before ⊔ after (the one non-convex category).

Equations

• Core.Order.distinct = Core.Order.before ⊔ Core.Order.after

def Core.Order.unrestricted : Finset Ordering

no constraint (= ⊤, see unrestricted_eq_top); kept as the explicit literal so the decide-checked relation-algebra laws below reduce without unfolding Finset.univ.

Equations

• Core.Order.unrestricted = {Ordering.lt, Ordering.eq, Ordering.gt}

Reductions to the underlying order (so consumers' <-shaped proofs go through)

holds_before/holds_after/holds_overlapping discharge the three atoms; each composite category then reduces through the homomorphism (holds_sup) plus those atoms, rather than by re-inspecting compare.

@[simp]

theorem Core.Order.holds_before {α : Type u_1} [LinearOrder α] (a b : α) : holds before a b ↔ a < b

@[simp]

theorem Core.Order.holds_after {α : Type u_1} [LinearOrder α] (a b : α) : holds after a b ↔ b < a

@[simp]

theorem Core.Order.holds_overlapping {α : Type u_1} [LinearOrder α] (a b : α) : holds overlapping a b ↔ a = b

@[simp]

theorem Core.Order.holds_notAfter {α : Type u_1} [LinearOrder α] (a b : α) : holds notAfter a b ↔ a ≤ b

@[simp]

theorem Core.Order.holds_notBefore {α : Type u_1} [LinearOrder α] (a b : α) : holds notBefore a b ↔ b ≤ a

@[simp]

theorem Core.Order.holds_distinct {α : Type u_1} [LinearOrder α] (a b : α) : holds distinct a b ↔ a ≠ b

theorem Core.Order.unrestricted_eq_top : unrestricted = ⊤

unrestricted is the top of the comparison-category Boolean algebra.

@[simp]

theorem Core.Order.holds_unrestricted {α : Type u_1} [LinearOrder α] (a b : α) : holds unrestricted a b ↔ True

Relation-algebra structure: converse and composition

Beyond Finset's Boolean-lattice structure (⊆, ∩, ∪), Finset Ordering carries a converse (swap lt/gt) and a composition with unit overlapping — the point algebra (the point analogue of AllenRelation's interval relations). comp r s over-approximates which category a stands in to c given holds r a b and holds s b c: the transitivity / path-consistency operation. Generic over any [LinearOrder α], so one algebra structures time, degree, or any other linear domain alike.

theorem Core.Order.swap_compare {α : Type u_1} [LinearOrder α] (a b : α) : (compare a b).swap = compare b a

Swapping the arguments of compare swaps the ordering.

def Core.Order.converse (s : Finset Ordering) : Finset Ordering

Converse of a comparison category: swap lt and gt.

Equations

• Core.Order.converse s = Finset.image Ordering.swap s

@[simp]

theorem Core.Order.holds_converse {α : Type u_1} [LinearOrder α] (s : Finset Ordering) (a b : α) : holds (converse s) a b ↔ holds s b a

def Core.Order.compBase : Ordering → Ordering → Finset Ordering

Base composition table for the point algebra: which categories a may stand in to c given compare a b and compare b c.

Equations

• Core.Order.compBase Ordering.lt Ordering.lt = Core.Order.before
• Core.Order.compBase Ordering.lt Ordering.eq = Core.Order.before
• Core.Order.compBase Ordering.eq x✝ = {x✝}
• Core.Order.compBase Ordering.gt Ordering.eq = Core.Order.after
• Core.Order.compBase Ordering.gt Ordering.gt = Core.Order.after
• Core.Order.compBase x✝¹ x✝ = Core.Order.unrestricted

def Core.Order.comp (r s : Finset Ordering) : Finset Ordering

Composition of comparison categories (transitivity / path-consistency): the relations a may stand in to c given r between a, b and s between b, c.

Equations

• Core.Order.comp r s = r.biUnion fun (o₁ : Ordering) => s.biUnion fun (o₂ : Ordering) => Core.Order.compBase o₁ o₂

theorem Core.Order.compare_mem_compBase {α : Type u_1} [LinearOrder α] (a b c : α) : compare a c ∈ compBase (compare a b) (compare b c)

Base soundness: the actual comparison of a and c lies in the composed category determined by compare a b and compare b c.

theorem Core.Order.holds_comp {α : Type u_1} [LinearOrder α] {a b c : α} {r s : Finset Ordering} (hab : holds r a b) (hbc : holds s b c) : holds (comp r s) a c

Composition is sound: it over-approximates the transitive relation. If a stands in r to b and b in s to c, then a stands in comp r s to c.

def Core.Order.IsConvex (s : Finset Ordering) : Prop

A comparison category is convex unless it is the non-convex {lt, gt} ("≠", skipping eq) — the one relation that takes the point algebra out of its path-consistency-complete fragment.

Equations

• Core.Order.IsConvex s = (Ordering.lt ∈ s → Ordering.gt ∈ s → Ordering.eq ∈ s)

@[implicit_reducible]

instance Core.Order.instDecidableIsConvex (s : Finset Ordering) : Decidable (IsConvex s)

Equations

• Core.Order.instDecidableIsConvex s = id inferInstance

Relation-algebra laws

The point algebra is a genuine relation algebra: comp is associative with unit overlapping, converse is an involution that anti-distributes over comp, comp is additive and monotone, and the convex fragment is closed under comp, ∩, and converse. All are finite checks over the 8-element carrier (decide, kernel-verified). mathlib has the concrete relation category (SetRel α β with comp/inv, and CategoryTheory.RelCat) but no abstract relation-algebra class; this is the finite, decidable point algebra, bridged to the concrete one by holds: holds s is the relation {(a, b) | compare a b ∈ s} (a SetRel α α), with converse mirroring SetRel.inv (holds_converse) and comp sound w.r.t. SetRel.comp (holds_comp) — exact only when the order realizes every intermediate point.

theorem Core.Order.comp_assoc (r s t : Finset Ordering) : comp (comp r s) t = comp r (comp s t)

theorem Core.Order.overlapping_comp (s : Finset Ordering) : comp overlapping s = s

theorem Core.Order.comp_overlapping (s : Finset Ordering) : comp s overlapping = s

theorem Core.Order.empty_comp (s : Finset Ordering) : comp ∅ s = ∅

theorem Core.Order.comp_empty (s : Finset Ordering) : comp s ∅ = ∅

theorem Core.Order.converse_converse (s : Finset Ordering) : converse (converse s) = s

theorem Core.Order.converse_comp (r s : Finset Ordering) : converse (comp r s) = comp (converse s) (converse r)

theorem Core.Order.comp_union_left (r s t : Finset Ordering) : comp (r ∪ s) t = comp r t ∪ comp s t

theorem Core.Order.comp_union_right (r s t : Finset Ordering) : comp r (s ∪ t) = comp r s ∪ comp r t

theorem Core.Order.comp_mono {r₁ r₂ s₁ s₂ : Finset Ordering} (hr : r₁ ⊆ r₂) (hs : s₁ ⊆ s₂) : comp r₁ s₁ ⊆ comp r₂ s₂

theorem Core.Order.isConvex_comp {r s : Finset Ordering} (hr : IsConvex r) (hs : IsConvex s) : IsConvex (comp r s)

theorem Core.Order.isConvex_inter {r s : Finset Ordering} (hr : IsConvex r) (hs : IsConvex s) : IsConvex (r ∩ s)

theorem Core.Order.isConvex_converse {s : Finset Ordering} (hs : IsConvex s) : IsConvex (converse s)