set of equivalences classes is equiv to quotient

Stream: Is there code for X?

[Antoine Chambert-Loir]

If c is a partition of a type α (setoid.is_partition c), then the quotient by the equivalence relation whose classes are the elements of c is equiv to c, as follows, but I couldn't find it in mathlib…

import data.setoid.partition

noncomputable example (α : Type*) (c : set (set α)) (hc : setoid.is_partition c) : quotient (setoid.mk_classes c hc.2) ≃ c :=
begin
  let f : α → c := λ a, ⟨_, @setoid.eqv_class_mem _ c hc.2 a⟩,
  refine equiv.of_bijective (@quotient.lift _ _ (setoid.mk_classes c hc.2) f _) _,
  { -- well defined
    intros a b hab,
    change (setoid.mk_classes c hc.2).rel a b at hab,

    rw setoid.rel_iff_exists_classes at hab,
    rw setoid.classes_mk_classes at hab,
    obtain ⟨u, h, ha, hb⟩ := hab,
    let hc2 := hc.2,
    simp only [f, subtype.mk_eq_mk],
    rw ← setoid.eq_eqv_class_of_mem hc.2 h ha,
    rw ← setoid.eq_eqv_class_of_mem hc.2 h hb, },
  split,
  { -- injective
    intros x y,
    obtain ⟨a, rfl⟩ := @quotient.exists_rep α (setoid.mk_classes c hc.2) x,
    obtain ⟨b, rfl⟩ := @quotient.exists_rep α (setoid.mk_classes c hc.2) y,
    simp only [quotient.lift_mk, f, subtype.mk_eq_mk],
    intro hab,
    apply quotient.sound,
    change (setoid.mk_classes c hc.2).rel a b,
    rw setoid.rel_iff_exists_classes,
    use { x : α | (setoid.mk_classes c hc.2).rel x a},
    split,
    rw setoid.classes_mk_classes,
    apply setoid.eqv_class_mem,
    split,
    rw set.mem_set_of, apply setoid.refl' _ a,
    rw hab, rw set.mem_set_of, apply setoid.refl' _ b, },
  { -- surjective
    rintro ⟨u, hu⟩,
    have hu' : u.nonempty,
    { rw set.nonempty_iff_ne_empty,
      intro hu', apply hc.1,  rw ← hu', exact hu, },
    obtain ⟨a, ha⟩ := hu',
    use @quotient.mk _ (setoid.mk_classes c hc.2) a,
    rw quotient.lift_mk,
    simp only [f, subtype.mk_eq_mk],
    rw setoid.eq_eqv_class_of_mem hc.2 hu ha, }
end

[Eric Wieser]

The forward direction golfs to

λ q, q.lift_on' (λ a, (⟨_, @setoid.eqv_class_mem _ c hc.2 a⟩ : c))
    (λ a b hab, subtype.ext $ set.ext $ λ x,
      ⟨λ h, setoid.trans' _ h hab, λ h, setoid.trans' _ h (setoid.symm' _ hab)⟩),

[Heather Macbeth]

I have been thinking about this lately in the context of teaching, and I think the real answer is that "the set of equivalence classes" is not the fundamental concept in the Lean/mathlib "foundations of mathematics" that it is in conventional mathematics. The lemma docs#quotient.eq states that for an equivalence relation $\sim$ on $X$, two points in $X$ go to the same point in the quotient $X/\sim$ if and only if they are related by $\sim$. In practice one uses this lemma directly without mentioning equivalence classes.

[Heather Macbeth]

See also:

Kevin Buzzard said:

Another thing I found strange was that we don't ever seem to use the bijection between equivalence relations and partitions (which I got Amelia to make, convinced that it would be important). My model of mathematics was that this was used absolutely everywhere; more recently I have become slightly embarrassed to even teach it to the 1st years! Someone suggested to me that it was perhaps because Lean uses type theory and has inbuilt quotients.

[Jireh Loreaux]

I actually very much prefer to teach quotients via the universal property rather than as equivalence classes (as sets). I find that students often fail to completely grasp the concept of a function (out of a quotient) being well-defined, and reasonably so, because (in my opinion) it's such an absurd idea. You pretend to define a function from a quotient, but really if you look you are defining a function on the prequotient and implicitly claiming it factors through the quotient. Then you say, "wait, let's check this function is actually a function" (??) and you proceed to prove the implicit claim. By teaching via the universal property, you force students to think about functions out of quotients as first being functions defined on the prequotient, and I think this makes it easier for them not to tie themselves in knots.

My go to example for why we need to do this (i.e., define from the prequotient and check that the function respects the equivalence) is to "define" f : ℚ → ℤ by f(p/q) = p + q. I find that first-year students are abysmal at recognizing the problem here. I then point out the problem (e.g., what is f(1/2)? f(2/4)?), and then they understand it for that example, but they don't yet comprehend the wider issue. This then leads into an explanation that the function g : ℤ × (ℤ \ {0}) → ℤ (or insert your favorite prequotient here) defined by g x y := x + y is perfectly valid, it just doesn't respect the equivalence relation, thereby leading to the universal property.

I recently wrote up something detailing the link between Lean's quotient and abstract equivalence classes ⟦x⟧, and the concrete equivalence classes as sets. It starts basically from the ground up. It purposefully mirrors some existing definitions (like setoid.is_partition), and even imports data.setoid.partition. This is only for pedagogical purposes, and it's still very rough; I basically just wrote it start-to-finish and haven't edited much, but maybe it will be useful to someone or inspire them to improve it.
partition.lean

[Antoine Chambert-Loir]

I perfectly agree that it is not the correct point of view on the quotient. Taking the set of equivalence classes is just a (well thought) way of constructing the quotient.

[Antoine Chambert-Loir]

(However, I was led to proving exactly that in Lean!)
Does the following exist :

import data.setoid.partition

example (α : Type*) [fintype α] (c : set (set α)) (hc : setoid.is_partition c) :
finsum (λ (x : c), nat.card x) = nat.card α :=
sorry

[Anatole Dedecker]

I don’t think this lemma is true without finiteness assumptions. If you have an infinite type and take a partition with one singleton and its complement, then the rhs is zero but the lhs is one, right?

[Anatole Dedecker]

Regarding the more general issue, I think "use docs#quotient everywhere" is not the right approach either: the real solution is to make sure that all lemmas about docs#quotient have a version for a quotient (i.e docs#function.surjective). Then you should just prove that the function mapping an element to its class in a docs#setoid.is_partition is surjective, and suddenly you wouldn’t even need to get back to docs#quotient anymore

[Anatole Dedecker]

The real reason equivalence classes aren’t the right notion is not that docs#quotient is better. It’s that the construction that is used shouldn’t matter in the first place.

[Anatole Dedecker]

(Except if you care about the nice definitional equalities provided by docs#quot and docs#quotient)

[Eric Wieser]

Anatole Dedecker said:

the real solution is to make sure that all lemmas about docs#quotient have a version for a quotient (i.e docs#function.surjective).

Often an even better solution is to have a version for docs#function.right_inverse

[Anatole Dedecker]

Sure, but you can easily go from one to another in theory

[Anatole Dedecker]

Here's a proof of the two statements with a bunch of API that feels reasonable.

import data.setoid.partition
import algebra.big_operators.finprod
import set_theory.cardinal.finite

lemma setoid.classes_ker_of_surjective {α β : Type*} {f : α → β} (hf : function.surjective f) :
  (setoid.ker f).classes = set.range (λ b : β, f ⁻¹' {b}) :=
begin
  ext s,
  rw [setoid.classes, set.mem_set_of, set.mem_range, hf.exists],
  refine exists_congr (λ a, _),
  rw [eq_comm],
  refl
end

def setoid.is_partition.to {α : Type*} {c : set (set α)} (hc : setoid.is_partition c) : α → c :=
λ x, ⟨classical.some (hc.2 x).exists, (classical.some_spec (hc.2 x).exists).elim (λ h _ _, h)⟩

lemma setoid.is_partition.mem_to {α : Type*} {c : set (set α)} (hc : setoid.is_partition c)
  (x : α) : x ∈ (hc.to x : set α) :=
(classical.some_spec (hc.2 x).exists).elim (λ _ h _, h)

lemma setoid.is_partition.eq_to_iff {α : Type*} {c : set (set α)} {s : set α}
  (hc : setoid.is_partition c) (x : α) (hs : s ∈ c) :
  s = hc.to x ↔ x ∈ s :=
begin
  refine ⟨λ h, h.symm ▸ hc.mem_to x, λ h, (hc.2 x).unique _ _⟩;
  rw exists_unique_prop,
  { exact ⟨hs, h⟩ },
  { exact ⟨subtype.coe_prop _, hc.mem_to x⟩ }
end

lemma setoid.is_partition.fiber_to_eq {α : Type*} {c : set (set α)}
  (hc : setoid.is_partition c) (s : c) :
  hc.to ⁻¹' {s} = s :=
begin
  ext,
  rw [set.mem_preimage, set.mem_singleton_iff, eq_comm, subtype.ext_iff],
  exact hc.eq_to_iff x (subtype.coe_prop s)
end

lemma setoid.is_partition.surjective_to {α : Type*} {c : set (set α)}
  (hc : setoid.is_partition c) : function.surjective hc.to :=
begin
  rintro ⟨s, hs⟩,
  set x := (setoid.nonempty_of_mem_partition hc hs).some,
  use x,
  ext : 1,
  symmetry,
  rw hc.eq_to_iff x (subtype.coe_prop _),
  exact (setoid.nonempty_of_mem_partition hc hs).some_spec
end

lemma setoid.is_partition.ker_to {α : Type*} {c : set (set α)} (hc : setoid.is_partition c) :
  setoid.ker hc.to = setoid.mk_classes c hc.2 :=
begin
  refine setoid.classes_inj.mpr _,
  have : (λ (s : ↥c), hc.to ⁻¹' {s}) = coe := by {ext s : 1, exact hc.fiber_to_eq s},
  rw [setoid.classes_mk_classes, setoid.classes_ker_of_surjective hc.surjective_to, this,
      subtype.range_coe]
end

noncomputable def foo {α : Type*} {c : set (set α)} (hc : setoid.is_partition c) :
  quotient (setoid.mk_classes c hc.2) ≃ c :=
calc quotient (setoid.mk_classes c hc.2)
      ≃ quotient (setoid.ker hc.to) : quotient.congr_right (λ _ _, by rw hc.ker_to)
  ... ≃ c : setoid.quotient_ker_equiv_of_surjective hc.to hc.surjective_to

example {α : Type*} [finite α] {c : set (set α)} (hc : setoid.is_partition c) :
  finsum (λ (x : c), nat.card x) = nat.card α :=
begin
  classical,
  letI := fintype.of_finite α,
  rw [finsum_eq_sum_of_fintype, nat.card_eq_fintype_card,
      fintype.card_congr (equiv.sigma_preimage_equiv hc.to).symm, fintype.card_sigma],
  congr,
  ext s,
  rw [nat.card_eq_fintype_card, hc.fiber_to_eq],
  refl
end

[Anatole Dedecker]

(golf welcome)

[Antoine Chambert-Loir]

Anatole Dedecker said:

I don’t think this lemma is true without finiteness assumptions. If you have an infinite type and take a partition with one singleton and its complement, then the rhs is zero but the lhs is one, right?

(Of course. I corrected the lemma.)

[Yaël Dillies]

I think your lemma can assume the parts are finite, rather than assuming that α is finite.

[Antoine Chambert-Loir]

Yes. If the parts are finite but the set is infinite, there are infinitely many parts, nat.card is zero, as is the finsum. But mathematically, it has not the same meaning.

[Antoine Chambert-Loir]

I went on playing that game…

lemma setoid.nat_sum {α : Type*} [finite α] {c : set (set α)}
  (hc : setoid.is_partition c) :
  finsum (λ (x : c), nat.card x) = nat.card α :=
begin
  classical,
  letI := fintype.of_finite α,
  simp only [finsum_eq_sum_of_fintype, nat.card_eq_fintype_card],
  rw ← fintype.card_sigma,
  refine fintype.card_congr (equiv.of_bijective (λ x, x.snd : (Σ (a : ↥c), ↥a) → α) _),
  split,
  -- injectivity
  rintros ⟨⟨x, hx⟩,⟨a, ha : a ∈ x⟩⟩ ⟨⟨y, hy⟩, ⟨b, hb : b ∈ y⟩⟩ hab,
  dsimp at hab,
  rw hab at ha,
  rw [sigma.subtype_ext_iff],
  simp only [subtype.mk_eq_mk, subtype.coe_mk],
  apply and.intro _ hab,
  refine unique_of_exists_unique (hc.2 b) _ _,
  simp only [exists_unique_iff_exists, exists_prop], exact ⟨hx, ha⟩,
  simp only [exists_unique_iff_exists, exists_prop], exact ⟨hy, hb⟩,

  -- surjectivity
  intro a,
  obtain ⟨x,⟨hx, ha : a ∈ x, ha'⟩, hx'⟩ := hc.2 a,
  use ⟨⟨x, hx⟩, ⟨a, ha⟩⟩, refl,
end

[Eric Wieser]

That proof looks like it should be trivial once you extract the equivalence into its own def (which likely already exists somewhere)

[Antoine Chambert-Loir]

The point is at the split, where I need to prove the bijectivity of the function λ x, x.snd : (Σ (a : ↥c), ↥a) → α).
If I enter rw function.bijective_iff_exists_unique, I am reduced to prove

∀ (b : α), ∃! (a : Σ (a : ↥c), ↥a), ↑(a.snd) = b

which is very close to the definition of set.is_partition c, except that the latter is

∀ (a : α), ∃! (b : set α) (H : b ∈ c), a ∈ b

and I don't know how to change trivially one to another.

[Antoine Chambert-Loir]

Eric Wieser said:

That proof looks like it should be trivial once you extract the equivalence into its own def (which likely already exists somewhere)

I could not find the equivalence (Σ (s : ↥c), ↥s) ≃ α (with hc : setoid.is_partition c) in mathlib.
Once we have it, everything simplifies as you indicated:

def setoid.is_partition.equiv {c : set (set α)}
  (hc : setoid.is_partition c) :
  (Σ (s : ↥c), ↥s) ≃ α := {
to_fun := λ x, x.snd,
inv_fun := λ a, ⟨⟨(exists_unique.exists2 (hc.2 a)).some, (exists_unique.exists2 (hc.2 a)).some_spec.some⟩, ⟨a, (exists_unique.exists2 (hc.2 a)).some_spec.some_spec⟩⟩,
left_inv := λ x,
begin
  rw sigma.subtype_ext_iff,
  split,
  { rw ← subtype.coe_inj,
    apply exists_unique.elim (hc.2 x.snd),
    intros s hs hst,
    simp only [exists_unique_iff_exists, exists_prop] at hs,
    simp only [exists_unique_iff_exists, exists_prop, and_imp] at hst,
    rw hst x.fst x.fst.prop x.snd.prop,
    have := (exists_unique.exists2 (hc.2 (x.snd))).some_spec,
    simp only [exists_prop] at this ⊢,
    exact hst _ this.1 this.2, },
  simp only [subtype.coe_mk],
end,
right_inv := λ a, by simp only [subtype.coe_mk] }

lemma setoid.nat_sum'{α : Type*} [finite α] {c : set (set α)}
  (hc : setoid.is_partition c) :
  finsum (λ (x : c), nat.card x) = nat.card α :=
begin
  classical,
  letI := fintype.of_finite α,
  simp only [finsum_eq_sum_of_fintype, nat.card_eq_fintype_card],
  rw ← fintype.card_sigma,
  apply fintype.card_congr hc.equiv,
end