Pullback Preorders

A PullbackPreorder Carrier Target is a Preorder Carrier realized as the pullback of a Preorder Target through a projection proj : Carrier → Target. The induced order is a ≤ a' ↔ proj a ≤ proj a'.

This is mathlib's Preorder.lift packaged with the witnessing projection and decidability of ≤. It is the common pattern behind several constructions in linglib:

• Preorder.ofCriteria (Core/Order/OfCriteria.lean) — the general criteria-derived preorder; its ≤ is the pullback of ⊇ along the satisfied-set map (Preorder.ofCriteria_le_iff_subset), without the bundled decidability.
• Core.Order.SatisfactionOrdering α Criterion — the projection is the satisfied criterion set, the target is (Finset Criterion)ᵒᵈ (or equivalently, the violated set with standard ⊆).
• Core.Optimization.paretoPullbackPreorder — the projection is the score vector, the target is Profile β n with pointwise ≤.
• Semantics.Modality.Kratzer.worldOrdering — the projection is the satisfied proposition set, same shape as SatisfactionOrdering.
• BundleLike.subsumptionPreorder — the projection is a feature bundle's valuation, the target is Features.Bundle with subsumption.

The reusable theorem

coarsen_via_monotone states that a monotone map φ : F1 → F2 between targets lifts dominance under the finer projection to dominance under the coarser one, provided o2.proj = φ ∘ o1.proj. This is the schema underlying "Pareto-on-violations ⇒ Pareto-on-satisfaction" and any other forgetful coarsening between qualitatively-comparable representations.

structure Core.Order.PullbackPreorder (Carrier : Type u_1) (Target : Type u_2) [Preorder Target] extends Preorder Carrier : Type (max u_1 u_2)

A preorder on Carrier realized as the pullback of a Preorder Target through proj : Carrier → Target.

extends Preorder Carrier, so all of mathlib's order vocabulary (≤, <, Maximal, IsMax) is available; proj/decLE expose the construction data. le_iff_proj is the load-bearing coherence field — the bundled ≤ agrees with the projection pullback.

• le : Carrier → Carrier → Prop
• lt : Carrier → Carrier → Prop
• le_refl (a : Carrier) : a ≤ a
• le_trans (a b c : Carrier) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : Carrier) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• proj : Carrier → Target
• decLE (a a' : Carrier) : Decidable (a ≤ a')
• le_iff_proj (a a' : Carrier) : a ≤ a' ↔ self.proj a ≤ self.proj a'

@[implicit_reducible]

instance Core.Order.PullbackPreorder.instDecidableLe {Carrier : Type u_1} {Target : Type u_2} [Preorder Target] (o : PullbackPreorder Carrier Target) (a a' : Carrier) : Decidable (a ≤ a')

Equations

• o.instDecidableLe a a' = o.decLE a a'

def Core.Order.PullbackPreorder.ofProj {Carrier : Type u_1} {Target : Type u_2} [Preorder Target] (proj : Carrier → Target) (dec : (a a' : Carrier) → Decidable (proj a ≤ proj a')) : PullbackPreorder Carrier Target

Smart constructor: build a PullbackPreorder from a projection plus decidability of target comparison. The induced ≤ is Preorder.lift, so le_iff_proj is Iff.rfl.

Equations

• Core.Order.PullbackPreorder.ofProj proj dec = { toPreorder := Preorder.lift proj, proj := proj, decLE := dec, le_iff_proj := ⋯ }

theorem Core.Order.PullbackPreorder.coarsen_via_monotone {Carrier : Type u_3} {F1 : Type u_4} {F2 : Type u_5} [Preorder F1] [Preorder F2] (o1 : PullbackPreorder Carrier F1) (o2 : PullbackPreorder Carrier F2) (φ : F1 → F2) (hmono : Monotone φ) (hcoh : ∀ (c : Carrier), o2.proj c = φ (o1.proj c)) {a a' : Carrier} (h : a ≤ a') : a ≤ a'

Change of target (coarsening).

Given two PullbackPreorders on the same carrier with projections o1.proj : Carrier → F1 and o2.proj : Carrier → F2, plus a monotone map φ : F1 → F2 such that o2.proj = φ ∘ o1.proj, dominance under o1 implies dominance under o2.

The converse generally fails: collapsing the target discards information. This is the schema behind every "qualitative coarsening" bridge — e.g. pointwise-Pareto-on-violations ⇒ subset-of-satisfied in Core/Optimization/Pareto.lean.