Commit 2025-07-06 13:16 59bd63c7

refactor: make Rel less see-through (#25587) There is tension throughout the library between considering relations between α and β simply as α → β → Prop, or as a bundled object Rel α β with dedicated operations and API. The former approach is used almost everywhere as it is very lightweight and has arguably native support from core Lean features, but it cracks at the seams whenever one starts talking about operations on relations. For example:

• composition of relations R : α → β → Prop, S : β → γ → Prop is the unwieldy Relation.Comp R S := fun a c ↦ ∃ b, R a b ∧ S b c
• map of a relation R : α → β → Prop, under f : α → γ, g : β → δ is the monstruous Relation.map R f g := fun c d ↦ ∃ a b, r a b ∧ f a = c ∧ g b = d. The latter approach is embodied by the existing type Rel α β, with dedicated notation like ○ for composition. It makes it much easier to reason about operations relations, but currently its API suffers from the leakage of its definition as

def Rel (α β : Type*) := α → β → Prop

The fact that Rel isn't an abbrev confuses automation. But simply making it an abbrev would kill the point of having a separate less see-through type to perform relation operations on. A final point, and the original motivation for this refactor, is that uniform spaces need a theory of relations on a type α as elements of Set (α × α). This cannot be worked around, since Set (α × α) is the type of elements of a filter on α × α. This theory is already developed in Topology.UniformSpace.Defs, and duplicates the existing Rel material. This PR is a proposal to refactor Rel to be less see-through by redefining it as

abbrev Rel (α β : Type*) := Set (α × β)

This has several advantages:

• The use of α × β means that one can't abuse the defeq of Rel α β with the function type α → β → Prop.
• Instead, we get to provide an explicit notation a ~[R] b that very closely follows the paper convention a ~R b of using relations as infixes. This notation is scoped to the Rel namespace.
• The use of Set is an extra layer of indirection to avoid automation confusing Rel α β with α × β → Prop.
• It can directly be used in the theory of uniform spaces because of the syntactic equality between Rel α α and Set (α × α).
• A relation can still be defined from an explicit function α → β → Prop, with nice notation: What was previously fun a b ↦ R a b becomes {(a, b) | R a b}.
• In general, fallout is manageably small and easily fixed by inserting the {(a, b) | R a b} and a ~[R] b notations. The benefits can be seen in places like CategoryTheory.Category.RelCat where automation is significantly improved, or Combinatorics.Hall.Basic where defeq abuse is avoided and dot notation becomes available. Zulip