Finiteness of quotients

Stream: new members

[Christian Merten]

I am trying to show that if the set of equivalence classes of an equivalence relation r : Setoid α (in the sense of Setoid.classes r) is finite, then the quotient is finite. For this I hoped to use some bijection or equivalence between the quotient and the set of equivalence classes, but I can't find anything in this direction.

[Adam Topaz]

I suppose you could look around docs#Setoid.classes

[Adam Topaz]

But having said that, if you’re using equivalence classes then it’s likely that you’re trying to do something in a suboptimal way. Can you un - #xy ?

[Christian Merten]

I want to show that in a compact topological group G, any open subgroup U has finite index. This is because the cosets of U form a disjoint open cover of G. Then by compactness, one obtains that the number of cosets is finite. But now I somehow have to say that the number of cosets, aka cardinality of Setoid.classes (QuotientGroup.leftRel U), is the cardinality of G / U.

[Kevin Buzzard]

What is your definition of index?

Every definition matters in lean. In maths we just say "the following five things are equal and they're all called the index". In lean it doesn't work like that, you have to say much more precisely what you mean. The best way to ask your question is not to post what you've written above, but to post something called an #mwe (this is a link explaining what I mean). Then it's much easier to help you. It's work writing a MWE but it's work well spent because it enables people to quickly answer your actual precise question as well as being able to comment on design decisions. You've chosen a very nice mathematical question to work on but now we need to see the details.

[Christian Merten]

I use the definition in Mathlib.GroupTheory.Index. The idea was to use Subgroup.index_ne_zero_of_finite, so I only need to show Finite (G / U). Here is a mwe:

import Mathlib.GroupTheory.Index
import Mathlib.Topology.Algebra.Group.Basic
import Mathlib.Data.Setoid.Partition

universe u

section Partition

variable {α : Type*} [TopologicalSpace α] [CompactSpace α]

lemma IsCompact.openPartition_finite (c : Set (Set α))
    (hp : Setoid.IsPartition c) (hU : ∀ s ∈ c, IsOpen s) : c.Finite :=
  -- I have a proof for this, deduced from IsCompact.elim_finite_subcover
  sorry

end Partition

variable {G : Type u} [Group G] [TopologicalSpace G] [TopologicalGroup G]
  [CompactSpace G]

example (U : Subgroup G) (U_open : IsOpen (U : Set G)) : U.index ≠ 0 := by
  have : Finite (G ⧸ U) := by
    let A : Set (Set G) := Setoid.classes (QuotientGroup.leftRel U)
    have A_partition : Setoid.IsPartition A := Setoid.isPartition_classes (QuotientGroup.leftRel U)
    have A_open : ∀ s ∈ A, IsOpen (s : Set G) := sorry
    have A_finite : A.Finite := IsCompact.openPartition_finite A A_partition A_open
    admit
  exact Subgroup.index_ne_zero_of_finite

Maybe one can try building an indexed partition and use docs#IndexedPartition.equivQuotient

[Christian Merten]

One can certainly construct an IndexedPartition P using the noncomputable docs#IndexedPartition.mk' and one then obtains an equivalence A ≃ IndexedPartition.Quotient P. But now I still need to have some equivalence from the actual quotient G / U and IndexedPartition.Quotient P.

[Kevin Buzzard]

Yeah it seems like there's not much API for Setoid.classes. That file was initially written by Amelia Livingston, who was at the time an undergraduate at Imperial (maybe 2019?), because I assured her that the relationship between equivalence classes and partitions was fundamental to mathematics (why else would I spend an entire hour proving this to 1st year undergraduates every year?). To my great surprise this file got very little use; even now, according to https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Setoid/Partition.html , it is only imported by one other file (in graph theory). So it looks like you found a hole in the API (which should be filled). In fact what is fundamental to mathematics is the universal property of quotients, it turns out.

[Christian Merten]

Do you think it is a good idea to try to establish an equivalence between Quotient s and Setoid.classes s?

[Eric Wieser]

I'm pretty sure that exists, because I remember Kevin PRing a docstring for it!

[Christian Merten]

@loogle Quotient, Setoid.classes

[Kevin Buzzard]

I can't find it. Modulo that, you're done:

section maybe_missing_api

def Setoid.classes_equiv_quotient {α : Type*} (r : Setoid α) : Setoid.classes r ≃ Quotient r := sorry

end maybe_missing_api


variable {G : Type u} [Group G] [TopologicalSpace G] [TopologicalGroup G]
  [CompactSpace G]

example (U : Subgroup G) (U_open : IsOpen (U : Set G)) : U.index ≠ 0 := by
  have : Finite (G ⧸ U) := by
    let A : Set (Set G) := Setoid.classes (QuotientGroup.leftRel U)
    have A_partition : Setoid.IsPartition A := Setoid.isPartition_classes (QuotientGroup.leftRel U)
    have A_open : ∀ s ∈ A, IsOpen (s : Set G) := sorry
    have A_finite : A.Finite := IsCompact.openPartition_finite A A_partition A_open
    rwa [← Set.finite_coe_iff,
         Equiv.finite_iff (QuotientGroup.leftRel U).classes_equiv_quotient] at A_finite
  exact Subgroup.index_ne_zero_of_finite

[Christian Merten]

Yes, thats what I was aiming for.

[Kevin Buzzard]

I don't know why loogle isn't responding here but the web version is reporting 0 matches

[Eric Wieser]

Maybe we lost it in the port?

[Kevin Buzzard]

Ask Jeremy to look under the benches at the Hoskinson

[Kevin Buzzard]

I PR'ed this docstring:

/-- The order-preserving bijection between equivalence relations on a type `α`, and
  partitions of `α` into subsets. -/
protected def Partition.orderIso : Setoid α ≃o { C : Set (Set α) // IsPartition C }
...

[Kyle Miller]

@Kevin Buzzard In graph theory, the way Setoid.classes pops up is in going from a graph coloring to a graph partition (docs#SimpleGraph.Coloring.toPartition). The difference between a coloring and a partition is that a coloring is a labeled partition, or conversely a partition is a coloring modulo the symmetry group for the colors. Maybe it's telling that Mathlib.Combinatorics.SimpleGraph.Partition isn't imported by anything yet... In any case, this gives a nice construction to remove unused colors via an adjunction between colorings and partitions (you re-color the graph using the color classes themselves as colors).

[Christian Merten]

So I suppose it does not exist yet, so I try to write a version myself.

[Kevin Buzzard]

It will be fiddly :-/ Get the maps right and hope aesop proves the diagrams commute.

[Christian Merten]

I wrote something down using the universal property of the quotient, it is still quite unpolished, but I am stuck at one seemingly trivial step:

import Mathlib.Data.Setoid.Partition

variable {α : Type*} (s : Setoid α)

noncomputable example : Quotient s ≃ Setoid.classes s := by
  let cls : Set (Set α) := Setoid.classes s
  have is_part : Setoid.IsPartition cls := Setoid.isPartition_classes s
  have f (a : α) : cls := ⟨{ x | Setoid.r x a }, Setoid.mem_classes s a⟩
  have f_val (a : α) : (f a).val = {x | Setoid.r x a} := sorry
  have f_respects_relation : ∀ (a b : α), Setoid.r a b → f a = f b := by
    intro a b a_rel_b
    have : b ∈ {x | Setoid.r x a} := Setoid.symm a_rel_b
    have eq_cls : {x | Setoid.r x a} = {x | Setoid.r x b} := by
      apply Setoid.eq_of_mem_classes
      exact Setoid.mem_classes s a
      exact Setoid.symm a_rel_b
      exact Setoid.mem_classes s b
      exact Setoid.refl b
    let cl_a : cls := ⟨{x | Setoid.r x a}, Setoid.mem_classes s a⟩
    let cl_b : cls := ⟨{x | Setoid.r x b}, Setoid.mem_classes s b⟩
    have : cl_a = cl_b := by simp only [Subtype.mk.injEq]; exact eq_cls
    rw [Subtype.mk.injEq, f_val a, f_val b]
    exact eq_cls
  --have h : Quotient s → cls := Quot.lift f f_respects_relation
  have h_bij : Function.Bijective (Quot.lift f f_respects_relation) := by
    constructor
    . intro (q_a : Quotient s) (q_b : Quotient s)
      obtain ⟨a, ha⟩ := Quotient.exists_rep q_a
      obtain ⟨b, hb⟩ := Quotient.exists_rep q_b
      intro h_eq
      rw [←ha, ←hb] at *
      simp only [Quotient.lift_mk] at h_eq
      have : (f a).val = (f b).val := congrArg Subtype.val h_eq
      have cls_eq : { x | Setoid.r x a} = { x | Setoid.r x b } := by
        rw [←f_val a, ←f_val b]
        assumption
      have : Setoid.r a b := by
        have : a ∈ { x | Setoid.r x a } := Setoid.refl a
        rw [cls_eq] at this
        exact this
      exact Quotient.sound this
    . apply (Quot.surjective_lift f_respects_relation).mpr
      intro ⟨c, c_in_cls⟩
      have : c.Nonempty := Setoid.nonempty_of_mem_partition is_part c_in_cls
      obtain ⟨a, a_in_c⟩ := this
      let cl_a := {x | Setoid.r x a}
      have cl_a_eq_c : cl_a = c := by
        apply Setoid.eq_of_mem_classes
        exact Setoid.mem_classes s a
        exact Setoid.refl a
        exact c_in_cls
        exact a_in_c
      exists a
      rw [Subtype.mk.injEq, ←cl_a_eq_c]
      exact f_val a
  exact Equiv.ofBijective (Quot.lift f f_respects_relation) h_bij

I can't resolve the sorry. Neither rfl, simp, aesop, exact? proof this, although I feel like this should hold by the very definition of f.

[Christian Merten]

I fixed it by replacing have with let. Now I dont even need the f_val. Somehow I thought have and let are the same thing.

[Kevin Buzzard]

have can't be used for data because it forgets the answer. have a : Nat := 37 only ends up with Lean knowing a is a Nat so you can't prove it's 37. Whereas let a : Nat := 37 means that a = 37 and the proof is rfl.

[Christian Merten]

I see, makes sense. Thank you.

[Kevin Buzzard]

This is Ok with proofs becase if I have h : P then who cares what the proof was, all we need to know is that h has type P and is thus a proof of P. Indeed any two proofs of P are equal and the proof is rfl.

[Kevin Buzzard]

Well done for getting that out by the way!

[Christian Merten]

Should I PR a polished version of this? If yes, where should it go? I suppose in Setoid.Data.Partition?

[Kevin Buzzard]

This is what I came up with but it's still pretty horrible:

section maybe_missing_api

theorem Setoid.class_eq_class_of_equiv {α : Type*} (r : Setoid α) (a b : α) (h : a ≈ b) :
    {x | Rel r x a} = {x | Rel r x b} := by
  ext c
  exact ⟨fun h' ↦ trans' r h' h, fun h' ↦ symm' r (trans' r h (symm' r h'))⟩

theorem Setoid.equiv_of_class_eq_class {α : Type*} (r : Setoid α) (a b : α)
    (h : {x | Rel r x a} = {x | Rel r x b}) : a ≈ b := by
  rw [Set.ext_iff] at h
  exact (h a).1 <| refl' r a

noncomputable def Setoid.classes_equiv_quotient {α : Type*} (r : Setoid α) :
    Setoid.classes r ≃ Quotient r where
  toFun := fun x ↦ ⟦x.2.choose⟧
  invFun := fun y ↦ Quotient.lift (fun y : α ↦ ⟨{ x | r.Rel x y }, y, rfl⟩)
    (fun a b h ↦ by simp [r.class_eq_class_of_equiv a b h]) y
  left_inv := by
    rintro ⟨s, a, rfl⟩
    simp only [Quotient.lift_mk, Subtype.mk.injEq]
    exact (Exists.choose_spec (Subtype.property
      (⟨{x | Rel r x a}, a, rfl⟩ : classes r) : {x | Rel r x a} ∈ classes r)).symm
  right_inv := by
    rintro x
    refine Quotient.inductionOn x (fun a ↦ Quotient.sound <| ?_)
    apply r.equiv_of_class_eq_class
    exact (Exists.choose_spec (Subtype.property
      (Quotient.lift (fun y ↦ (⟨{x | Rel r x y}, y, rfl⟩ : classes r))
      (fun a b h ↦ by simp [r.class_eq_class_of_equiv a b h])
      (Quotient.mk r a)) : ↑(Quotient.lift
        (fun y ↦ (⟨{x | Rel r x y}, y, rfl⟩ : ↑(classes r)))
        _ (Quotient.mk r a)) ∈ classes r)).symm

end maybe_missing_api

[Christian Merten]

I don't have the permission to open branches on mathlib4 yet. Could you grant me this? My github handle is @chrisflav

[Christian Merten]

Kevin Buzzard said:

This is what I came up with but it's still pretty horrible:

section maybe_missing_api

theorem Setoid.class_eq_class_of_equiv {α : Type*} (r : Setoid α) (a b : α) (h : a ≈ b) :
    {x | Rel r x a} = {x | Rel r x b} := by
  ext c
  exact ⟨fun h' ↦ trans' r h' h, fun h' ↦ symm' r (trans' r h (symm' r h'))⟩

theorem Setoid.equiv_of_class_eq_class {α : Type*} (r : Setoid α) (a b : α)
    (h : {x | Rel r x a} = {x | Rel r x b}) : a ≈ b := by
  rw [Set.ext_iff] at h
  exact (h a).1 <| refl' r a

noncomputable def Setoid.classes_equiv_quotient {α : Type*} (r : Setoid α) :
    Setoid.classes r ≃ Quotient r where
  toFun := fun x ↦ ⟦x.2.choose⟧
  invFun := fun y ↦ Quotient.lift (fun y : α ↦ ⟨{ x | r.Rel x y }, y, rfl⟩)
    (fun a b h ↦ by simp [r.class_eq_class_of_equiv a b h]) y
  left_inv := by
    rintro ⟨s, a, rfl⟩
    simp only [Quotient.lift_mk, Subtype.mk.injEq]
    exact (Exists.choose_spec (@Subtype.property (Set α) (fun x ↦ x ∈ classes r)
      { val := {x | Rel r x a},
        property := Exists.intro a (Eq.refl {x | Rel r x a}) } : {x | Rel r x a} ∈ classes r)).symm
  right_inv := by
    rintro x
    refine Quotient.inductionOn x (fun a ↦ ?_)
    apply Quotient.sound
    apply r.equiv_of_class_eq_class
    exact (Exists.choose_spec (@Subtype.property (Set α) (fun x ↦ x ∈ classes r)
      (Quotient.lift (fun y ↦ { val := {x | Rel r x y}, property := ⟨y, rfl⟩ })
      (fun a b h ↦ by simp [r.class_eq_class_of_equiv a b h])
      (Quotient.mk r a)) : ↑(Quotient.lift
        (fun y ↦ ({ val := {x | Rel r x y}, property := ⟨y, rfl⟩ } : ↑(classes r)))
        _ (Quotient.mk r a)) ∈ classes r)).symm

end maybe_missing_api

Battling myself with Classical.choose was exactly what I tried to avoid :D

[Kevin Buzzard]

Christian Merten said:

I don't have the permission to open branches on mathlib4 yet. Could you grant me this? My github handle is @chrisflav

@maintainers

[Kevin Buzzard]

yeah, when I was a beginner I would avoid it but I'm more confident now. It's still a bit annoying I have to cut and paste the precise existence statement into Exists.choose_spec.

[Kevin Buzzard]

The advantage of my approach is that both toFun and invFun are concrete functions by definition. Your approach via Equiv.ofBijective has the disadvantage that you don't know what the invFun is, all you know is that it's the inverse of the toFun. So for example if someone wanted to prove that the map you're implicitly defining from Setoid.classes to Quotient is fun x ↦ ⟦x.2.choose⟧ they'd have to do what I'm doing in my approach.

[Kevin Buzzard]

In constructive mathematics, a function + proof that it's a bijection is a slightly weaker amount of data than a function plus an inverse function plus the two proofs. Even the inverse of a computable function might not be computable, as I discovered to my surprise when I was trying to get on top of this stuff (see https://xenaproject.wordpress.com/2019/06/11/the-inverse-of-a-bijection/ )

[Anatole Dedecker]

Invitation sent!

[Christian Merten]

https://github.com/leanprover-community/mathlib4/pull/7444

[Christian Merten]

Kevin Buzzard said:

The advantage of my approach is that both toFun and invFun are concrete functions by definition. Your approach via Equiv.ofBijective has the disadvantage that you don't know what the invFun is, all you know is that it's the inverse of the toFun. So for example if someone wanted to prove that the map you're implicitly defining from Setoid.classes to Quotient is fun x ↦ ⟦x.2.choose⟧ they'd have to do what I'm doing in my approach.

I see, do you think we should put your version instead then?

[Adam Topaz]

If you’re going to use choose for one direction of the equiv, you may as well just use docs#Equiv.ofBijective IMO

[Patrick Massot]

The reason why we never use Setoid.classes is there is always something more efficient to do. In the case at hand the answer is pretty clear. If your actual goal is

example {G : Type u} [Group G] [TopologicalSpace G] [TopologicalGroup G]
  [CompactSpace G]  (U : Subgroup G) (U_open : IsOpen (U : Set G)) :   Finite (G ⧸ U)

then the nice proof is to use docs#finite_of_compact_of_discrete. The quotient is compact because it is the image of a compact space under a continuous map, and it it discrete because every singleton is open (because its preimage is a copy of the open set U).

[Christian Merten]

That is very nice and way more elegant than the way around Setoid.classes. Thanks!

[Patrick Massot]

I thought it would be a fun exercise to implement this approach. It seems I found a hole in the subgroup quotient API, but maybe I didn't search correctly. In any case, the whole thing doesn't have to be longer than

import Mathlib

open Function Set

lemma QuotientGroup.preimage_mk_singleton_mk {G : Type*} [Group G] (H : Subgroup G) (g : G) :
    mk (s := H) ⁻¹' {mk g} = (g * ·) '' H := by
  ext g'
  simp only [mem_preimage, mem_singleton_iff, QuotientGroup.eq, image_mul_left, SetLike.mem_coe]
  rw [← H.inv_mem_iff]
  simp

variable {G : Type*} [Group G] [TopologicalSpace G] [TopologicalGroup G] (U : Subgroup G)

lemma Subgroup.discreteTopology  (U_open : IsOpen (U : Set G)) : DiscreteTopology (G ⧸ U) := by
  apply singletons_open_iff_discrete.mp
  rintro ⟨g⟩
  erw [isOpen_mk, QuotientGroup.preimage_mk_singleton_mk]
  exact Homeomorph.mulLeft g |>.isOpen_image|>.mpr U_open

lemma Subgroup.finite_quotient [CompactSpace G] (U_open : IsOpen (U : Set G)) : Finite (G ⧸ U) :=
  have : CompactSpace (G ⧸ U) := Quotient.compactSpace
  have : DiscreteTopology (G ⧸ U) := U.discreteTopology U_open
  finite_of_compact_of_discrete

[Christian Merten]

I was just trying it out myself and found it quite annoying to show the equality you call QuotientGroup.preimage_mk_singleton_mk. Your solution is quite elegant.

[Patrick Massot]

In case this isn't clear, the big simp only in the middle comes from simp? and I didn't try to optimize it.