Relation lifting to sets

Mirror of Mathlib/Data/Set/Functor.lean: the relation lifting of the powerset functor. Set.LiftRel r s t holds when every member of s is r-related to some member of t and every member of t is r-related from some member of s. This is the Egli–Milner lifting, the Set counterpart of Computation.LiftRel, and at a homogeneous relation the functor-level Functor.Liftr. [UPSTREAM]

Main definitions

• Set.LiftRel r s t: every member of s has an r-partner in t, and conversely.

Main results

• Set.liftRel_iff_subset_preimage_image, Set.liftRel_iff_exists_dom_cod, Set.liftRel_iff_biTotal, Set.liftRel_iff_liftr: the lifting as two SetRel image inclusions, as a subrelation with the given domain and codomain, as bitotality of the restriction, and as Functor.Liftr.
• Set.liftRel_eq, Set.liftRel_comp: the lifting sends equality to equality and relational composition to composition.
• Set.LiftRel.union, Set.LiftRel.biUnion: closure under unions, and under the indexed unions of related families, the bind of Computation.liftRel_bind.
• The lifting of a reflexive, symmetric or transitive relation is reflexive, symmetric or transitive, and Set.LiftRel.equiv for equivalences.

Implementation notes

By liftRel_eq and liftRel_comp the lifting is a functor from relations to relations; a lift of dynamic meanings to plural states is an instance, and inherits identity and sequencing from here.

def Set.LiftRel {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (s : Set α) (t : Set β) : Prop

The relation lifting of r to sets: every member of s is r-related to some member of t, and every member of t is r-related from some member of s.

Equations

• Set.LiftRel r s t = ((∀ a ∈ s, ∃ b ∈ t, r a b) ∧ ∀ b ∈ t, ∃ a ∈ s, r a b)

theorem Set.liftRel_iff_subset_preimage_image {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : Set α} {t : Set β} : LiftRel r s t ↔ s ⊆ SetRel.preimage {q : α × β | r q.1 q.2} t ∧ t ⊆ SetRel.image {q : α × β | r q.1 q.2} s

theorem Set.liftRel_iff_exists_dom_cod {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : Set α} {t : Set β} : LiftRel r s t ↔ ∃ D ⊆ {q : α × β | r q.1 q.2}, D.dom = s ∧ D.cod = t

The lifting holds exactly when some subrelation of r has domain s and codomain t.

theorem Set.liftRel_iff_biTotal {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : Set α} {t : Set β} : LiftRel r s t ↔ Relator.BiTotal fun (a : ↑s) (b : ↑t) => r ↑a ↑b

theorem Set.liftRel_iff_liftr {α : Type u_1} {r : α → α → Prop} {s t : Set α} : LiftRel r s t ↔ Functor.Liftr r s t

At a homogeneous relation, the lifting is the functor-level Functor.Liftr of Set.

theorem Set.liftRel_swap {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : Set α} {t : Set β} : LiftRel (Function.swap r) t s ↔ LiftRel r s t

theorem Set.LiftRel.imp {α : Type u_1} {β : Type u_2} {r p : α → β → Prop} {s : Set α} {t : Set β} (H : ∀ {a : α} {b : β}, r a b → p a b) (h : LiftRel r s t) : LiftRel p s t

theorem Set.liftRel_refl_of_refl_on {α : Type u_1} {s : Set α} {r : α → α → Prop} (H : ∀ a ∈ s, r a a) : LiftRel r s s

@[simp]

theorem Set.liftRel_eq {α : Type u_1} {s t : Set α} : LiftRel (fun (x1 x2 : α) => x1 = x2) s t ↔ s = t

theorem Set.liftRel_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {s : Set α} {p : β → γ → Prop} {u : Set γ} : LiftRel (Relation.Comp r p) s u ↔ ∃ (t : Set β), LiftRel r s t ∧ LiftRel p t u

The lifting of a composite relation is the composite of the liftings.

instance Set.instReflLiftRel {α : Type u_1} {r : α → α → Prop} [Std.Refl r] : Std.Refl (LiftRel r)

instance Set.instSymmLiftRel {α : Type u_1} {r : α → α → Prop} [Std.Symm r] : Std.Symm (LiftRel r)

instance Set.instIsTransLiftRel {α : Type u_1} {r : α → α → Prop} [IsTrans α r] : IsTrans (Set α) (LiftRel r)

theorem Set.LiftRel.equiv {α : Type u_1} {r : α → α → Prop} (H : Equivalence r) : Equivalence (LiftRel r)

@[simp]

theorem Set.liftRel_singleton {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {b : β} : LiftRel r {a} {b} ↔ r a b

theorem Set.liftRel_singleton_right {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : Set α} (hs : s.Nonempty) {b : β} : LiftRel r s {b} ↔ ∀ a ∈ s, r a b

Over a singleton on the right, the lifting from a nonempty set is distribution.

theorem Set.LiftRel.nonempty_iff {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : Set α} {t : Set β} (h : LiftRel r s t) : s.Nonempty ↔ t.Nonempty

theorem Set.LiftRel.eq_empty_iff {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : Set α} {t : Set β} (h : LiftRel r s t) : s = ∅ ↔ t = ∅

theorem Set.LiftRel.union {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s₁ s₂ : Set α} {t₁ t₂ : Set β} (h₁ : LiftRel r s₁ t₁) (h₂ : LiftRel r s₂ t₂) : LiftRel r (s₁ ∪ s₂) (t₁ ∪ t₂)

theorem Set.LiftRel.biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {s : Set α} {t : Set β} {q : γ → δ → Prop} {f : α → Set γ} {g : β → Set δ} (h : LiftRel r s t) (H : ∀ a ∈ s, ∀ b ∈ t, r a b → LiftRel q (f a) (g b)) : LiftRel q (⋃ a ∈ s, f a) (⋃ b ∈ t, g b)

Lifted families over lifted index sets: if s and t are related and related indices carry related sets, the indexed unions are related.