Equivalence Relation associated to a subset

Stream: Is there code for X?

[Xavier Xarles]

I don't know if something like this is already constructed

import Mathlib.Tactic

variable {α : Type*}

def EquiS (s: α → Prop): α → α → Prop:= fun a b ↦ (s a ∧ s b) ∨ (a=b)

It is an equivalence relation, the one generated by the subset s.

[Adam Topaz]

isn't this the kernel of the indicator function of S?

[Adam Topaz]

or rather the function which collapses S to a point

[Patrick Massot]

Yes, it collapses s to a point. Except you should really use Set here instead of predicates.

[Adam Topaz]

I guess it could therefore be modeled as the kernel of Set.indicator S\^c coe where coe is the inclusion into WithZero, or something like that.

[Adam Topaz]

I think I remember seeing something like in mathlib.

[Xavier Xarles]

I don't really know what's the kernel of a function in mathlib. May be something like

example (f:α → β):= ((·=·) on f)

[Eric Wieser]

docs#Setoid.ker

[Eric Wieser]

Does Setoid.ker (PLift.up ∘ s)work?

[Eric Wieser]

Arguably Setoid.ker has bad universe assumptions

[Yury G. Kudryashov]

I guess, Setoid.ker will glue both s and its complement.

[Yury G. Kudryashov]

I think that we should add this definition to Mathlib. E.g., it appears in quite a few (counter)examples in topology.

[Yaël Dillies]

... or in algebraic geometry, for homology computations

[Yury G. Kudryashov]

@Xavier Xarles Could you do this, please? E.g., in Data.Setoid.Basic.

[Yury G. Kudryashov]

Can be called Set.toSetoid.

[Yaël Dillies]

I was hoping for a more visual name, something involving "squash".

[Yury G. Kudryashov]

Then it should be Setoid.squash.

[Eric Wieser]

I think I was confused, the PLift is not needed

[Eric Wieser]

Setoid.ker (· ∈ s) alone works fine

[Eric Wieser]

Or for Xavier's original example without a set but a predicate, simply Setoid.ker p is enough

[Yury G. Kudryashov]

But it's not the relation we need here.

[Eric Wieser]

Whoops; Setoid.map ⊤ ((↑) : s → α) presumably is, right? Though it has a lousy defeq.

[Adam Topaz]

I agree that this construction (of the quotient squashing a set to a point) is important and should be added, but I think that we should just take the Quot by the (generally non-equiv) relation x \in S \and y \in S, and develop an api around that

[Kyle Miller]

Last time we had this discussion, something that I'd thought of was having an API for generating a setoid with some collection of equivalence classes. If the equivalence classes don't cover the whole type, then the assumption could be that it is extended using singleton sets for the rest of the equivalence classes.

This way, the "collapse this set s to a point" is using this with the collection {s}. If you want to collapse one set s to a point and another disjoint set t to another point, you could use the collection {s, t}.

[Yury G. Kudryashov]

If you have S : Set (Set α), then you can define a setoid by Setoid.map (.ker Sigma.fst) fun x : Σ i : S, i.1 => x.2.1

[Yury G. Kudryashov]

Then you can have lemmas for special cases like "all sets in S are pairwise disjoint" or "S is a singleton" or "S is a partition of the whole space into disjoint sets".

[Xavier Xarles]

I really don't understand what your definition does. Given a "collection" of subsets of α, which equivalence relation it defines?

[Yury G. Kudryashov]

A more readable version (not tested):

def Setoid.fromSets (S : Set (Set α)) : Setoid α :=
  EqvGen.Setoid fun a b ↦ ∃ s ∈ S, a ∈ s ∧ b ∈ s

[Yury G. Kudryashov]

It defines the minimal equivalence relation that squashes each s ∈ S.

[Chris Wong]

What are the use cases for taking a collection of sets instead of only one?
Just want to make sure we aren't generalizing unnecessarily.

[Kyle Miller]

I had applications such as graph minors in mind, since it lets you relate a minor of a minor to a minor of the original graph.

[Chris Wong]

I guess the advantage of the original (x ∈ s ∧ y ∈ s) ∨ x = y proposal is that it's already an equivalence - we don't need an extra EqvGen (and the induction dance that entails) to make it work.

[Kyle Miller]

Or, more generally, if you collapse one subset and then another, it's convenient to be able to express collapsing both at once.

[Chris Wong]

(Also, we only need ReflTransGen? Since it's already symmetric :thinking: )

[Chris Wong]

If we require the sets to be disjoint, then we only need ReflGen. That might be easier to work with as it's not recursive.

[Kyle Miller]

I think it's better if we use the EqvGen/ReflTransGen version and then have lemmas that say if the sets are pairwise disjoint then you can use ReflGen.

It's the principle of not requiring additional hypotheses in a definition when possible.

[Kyle Miller]

Something like this:

import Mathlib

variable {α : Type*}

def Setoid.fromSets (S : Set (Set α)) : Setoid α :=
  EqvGen.Setoid fun a b ↦ ∃ s ∈ S, a ∈ s ∧ b ∈ s

theorem Setoid.fromSets_r_iff (S : Set (Set α)) (h : S.Pairwise Disjoint) (a b : α) :
    (Setoid.fromSets S).r a b ↔ a = b ∨ ∃ s ∈ S, a ∈ s ∧ b ∈ s := by
  constructor
  · intro hr
    induction hr with
    | rel x y hr => exact Or.inr hr
    | refl x => exact Or.inl rfl
    | symm x y _ ih =>
      convert ih using 1
      · rw [eq_comm]
      · congr! 3
        rw [and_comm]
    | trans x y z hxy hyz ih1 ih2 =>
      obtain (rfl | ih1) := ih1 <;> obtain (rfl | ih2) := ih2
      · exact Or.inl rfl
      · exact Or.inr ih2
      · exact Or.inr ih1
      · obtain ⟨s1, hs1, hxs1, hys1⟩ := ih1
        obtain ⟨s2, hs2, hys2, hzs2⟩ := ih2
        obtain (rfl | hne) := eq_or_ne s1 s2
        · exact Or.inr ⟨s1, hs1, hxs1, hzs2⟩
        · exfalso
          have := h hs1 hs2 hne
          rw [Set.disjoint_iff] at this
          simpa using this ⟨hys1, hys2⟩
  · rintro (rfl | h)
    · exact EqvGen.refl _
    · exact EqvGen.rel _ _ h

theorem Setoid.fromSets_r_eq_of_disjoint (S : Set (Set α)) (h : S.Pairwise Disjoint) :
    (Setoid.fromSets S).r = Relation.ReflGen fun a b ↦ ∃ s ∈ S, a ∈ s ∧ b ∈ s := by
  ext a b
  rw [Setoid.fromSets_r_iff S h]
  constructor
  · rintro (rfl | hr)
    · constructor
    · constructor
      exact hr
  · intro hr
    induction hr with
    | refl => exact Or.inl rfl
    | single ih => exact Or.inr ih

[Chris Wong]

Thanks! That's a cool idea. I defined it with ReflGen in my code but dealing with the extra (h : S.PairwiseDisjoint) hypotheses was indeed annoying. Having those 2 lemmas instead makes sense to me.

[Chris Wong]

Yaël Dillies said:

I was hoping for a more visual name, something involving "squash".

Note that we already have a docs#Squash. (It's a near-duplicate of docs#Trunc – perhaps we can remove one of them...)

[Chris Wong]

Here's my version using ReflTransGen instead. I think dropping the redundant symm case makes the fromSets_r_iff proof simpler. I also simplified the disjointness proof using docs#Set.PairwiseDisjoint.elim_set.

import Mathlib

open Relation

variable {α : Type*}

def Setoid.fromSets (S : Set (Set α)) : Setoid α where
  r := ReflTransGen fun a b ↦ ∃ s ∈ S, a ∈ s ∧ b ∈ s
  iseqv := {
    refl := fun a ↦ ReflTransGen.refl
    trans := ReflTransGen.trans
    symm := fun h ↦ ReflTransGen.symmetric (by tauto) h
  }

theorem Setoid.fromSets_r_iff (S : Set (Set α)) (h : S.PairwiseDisjoint id) (a b : α) :
    (Setoid.fromSets S).r a b ↔ a = b ∨ ∃ s ∈ S, a ∈ s ∧ b ∈ s := by
  constructor
  · intro hr
    induction hr with
    | refl => exact .inl rfl
    | tail _ hs ih =>
      rcases ih with rfl | ht
      · exact .inr hs
      · right
        obtain ⟨s, hs, hbs, hcs⟩ := hs
        obtain ⟨t, ht, hat, hbt⟩ := ht
        have : s = t := h.elim_set hs ht _ hbs hbt
        exact ⟨s, hs, this ▸ hat, hcs⟩
  · rintro (rfl | hr)
    · exact .refl
    · exact .single hr

[Chris Wong]

Here's what I've got so far:
https://github.com/leanprover-community/mathlib4/commit/b01a0c03cd6db19775e13c8d454bb013d2df4141
I added the fiber lemmas because they were useful for my minor map definition.
If there are no objections, I'll split this off the minor branch and send a PR.

[Chris Wong]

I wonder if it's worth trying the \forall s \in S, x \in s -> y \in s definition used by mkClasses. That relation is reflexive and transitive but not symmetric. Unfortunately there's no SymmGen in mathlib.

[Chris Wong]

Even if SymmGen existed, it would not preserve transitivity, so it would be useless anyway. So I'll stick with the original definition with the existential.

[Chris Wong]

Coming back to this.
Another possibility is

def Contract (S : Set α) := Option (Subtype Sᶜ)

where the elements of S are mapped to .none.
And then we don't really need an API at this point, just manipulate the Subtype directly.