Sets, Types, Partitions, Eqv Relations

Stream: new members

[Brandon Brown]

This took me a really long time (to prove that equivalence relations are equivalent to set partitions). I made fast progress in the beginning, but proving that (G : partition X → setoid X) (F : setoid X → partition X) = id took me a few weeks for some reason (granted I have a day job as a physician and just doing this for my own edification). Also my proofs are probably way longer than they need to be. But I learned a lot nonetheless.

import data.setoid
import data.equiv.basic
open set
open setoid
#check eq_of_mem_eqv_class
#check eq_of_subset_of_subset
#check @eq_of_mem_classes
#check exists_unique.intro
--set_option trace.simplify.rewrite true

@[ext] structure partition (X : Type*) :=
(F : set (set X))
(disjoint : ∀ A B ∈ F, A ≠ B → A ∩ B = ∅)
(cover : ∀ x : X, ∃ A ∈ F, x ∈ A)
(nonempty : ∀ A ∈ F, A ≠ ∅)

variable X : Type*

def F {X : Type*} (S : setoid X) : partition X :=
partition.mk
(
     classes S
)
( -- ⊢ (disjoint : ∀ A B ∈ ℱ, A ≠ B → A ∩ B = ∅)
  begin
    intros,
    apply eq_of_subset_of_subset,
    {
      intro x,
      intros,
      rw mem_empty_eq,
      apply a,
      cases a_1,
      --have F : set (set X), from classes S,
      apply eq_of_mem_classes,
      repeat {assumption},
    },
    {
      apply set.empty_subset,
    }
  end
)
( -- ⊢ (cover : ∀ x : X, ∃ A ∈ ℱ, x ∈ A)
  begin
    intros,
    split,
    use x,
    simp,
  end
)
( -- ⊢ (nonempty : ∀ A ∈ ℱ, A ≠ ∅)
  begin
    intros,
    intro aqn,
    apply empty_not_mem_classes,
    rwa ← aqn,
  end
)
#check F

/-
Q3 : now define a map the other way
-/
--open_locale classical

def G {X : Type*} (P : partition X) : setoid X :=
begin
  cases P,
  let r := λ x y : X, (∃ h ∈ P_F, x ∈ h ∧ y ∈ h),
  /-have rt : X → X → Prop,
  {
    exact r,
  },-/
  have iseqv : equivalence r,
  {
    split,
    intro x,
    {
      have h : ∃ h ∈ P_F, x ∈ h,
      {
        apply P_cover,
      },
      {
        cases h,
        cases h_h,
        have z : ∃ h ∈ P_F, x ∈ h ∧ x ∈ h,
        {
          finish,
        },
        assumption,
      },
    },
    split,
    {
      --symmetric
      finish,
    },
    {
      -- transitive
      unfold transitive,
      intros,
      dsimp [r],
      have p1 : ∃ h ∈ P_F, (x ∈ h ∧ y ∈ h), assumption,
      have p2 : ∃ h ∈ P_F, (y ∈ h ∧ z ∈ h), assumption,
      cases p1,
      cases p2,
      use p1_w,
      split,
      finish,
      split,
      finish,
      {
        cases p1_h,
        cases p2_h,
        cases p1_h_h,
        cases p2_h_h,
        suffices k : p1_w = p2_w,
        finish,
        {
            suffices f1 : p1_w = p2_w ↔ p1_w ∩ p2_w ≠ ∅,
            cases f1,
            apply f1_mpr,
            have f2 : y ∈ p1_w ∩ p2_w,
            apply set.mem_inter,
            repeat {assumption},
            set f3 := p1_w ∩ p2_w with h,
            apply set.nonempty.ne_empty,
            apply set.nonempty_of_mem,
            exact f2,
            split,
            repeat {intro},
            apply set.nonempty.ne_empty,
            repeat {assumption},
            finish,
            finish,
        },
      },
    },
  },
  exact {r := r, iseqv := iseqv},
end
lemma eq_iff_classes_eq' {α : Type*} {r₁ r₂ : setoid α} :
  r₁ = r₂ ↔ ∀ x, {y | r₁.rel x y} = {y | r₂.rel x y} :=
⟨λ h x, h ▸ rfl, λ h, ext' $ λ x, set.ext_iff.1 $ h x⟩

variable (s : partition X)
#check G s
/-
Q4 : now finally prove that the composite of maps in both directions
is the identity
-/
#check F
#check G
#check function.left_inverse G F
variable (R : setoid X)
variables (a b : X)
variable (h : R.rel a b)
#check h
#check R.rel
#check G (F R)

theorem FG_eq_id {X : Type*} : function.left_inverse (G : partition X → setoid X) F :=
begin
intros s,
apply setoid.ext,
intros,
split,
cases s,
set s := setoid.mk s_r s_iseqv,
simp only [s],
intro,
cases a_1,
suffices h3 : s.rel a b,
finish,
rw setoid.rel_iff_exists_classes,
finish,
intro,
split,
split,
apply setoid.mem_classes,
assumption,
split,
simp at *,
simp at *,
solve_by_elim,
end
-- G : partition X → setoid X
-- F : setoid X → partition X

open classical
local attribute [instance] classical.prop_decidable

lemma partition_els_eq_if_share_el
{F : set (set X)}
{disjoint : ∀ A B ∈ F, A ≠ B → A ∩ B = ∅}
{cover : ∀ x : X, ∃ A ∈ F, x ∈ A}
{nonempty : ∀ A ∈ F, A ≠ ∅}
{A B : set X}
{h0 : A ∈ F} {h1 : B ∈ F}
(h2 : ∃ x : X, x ∈ A ∧ x ∈ B) : A = B :=
begin
cases h2,
cases h2_h,
by_contra,
have z : A ∩ B = ∅,
apply disjoint,
repeat {tauto},
have z2 : h2_w ∈ A ∩ B,
apply mem_inter,
repeat {tauto},
rw z at z2,
tauto,
end

theorem GF_eq_id : function.right_inverse (G : partition X → setoid X) F :=
begin
intro,
set S : setoid X := G x,
set P : partition X := F S,
apply partition.ext,
destruct P,
destruct S,
repeat{intro},
cases x,
injections,
simp,
apply eq_of_subset_of_subset,
repeat {intro},
{
  have j1 : F = P.F, tauto,
  rw ← j1 at a_3,
  suffices j2 : a_2 ∈ classes S → a_2 ∈ x_F,
  rw ← h_2 at a_3,
  solve_by_elim,
  intros,
  destruct a_4,
  intros,
  have j3 : rel S = r, solve_by_elim,
  rw j3 at h,
  have j4 : ∃ (a5 ∈ x_F), w ∈ a5,tauto,
  cases j4,
  cases j4_h,
  suffices j5 : a_2 = j4_w,
  rwa j5,
  apply set.ext,intros,
  split,intros,
  have j6 : ∃ (d : set X) (H : d ∈ x_F), x ∈ d ∧ w ∈ d,
  rw h at a_5,
  rw mem_set_of_eq at a_5,
  rw ← h_1 at a_5,tauto,
  cases j6,
  cases j6_h,
  cases j6_h_h,
  suffices j7 : j6_w = j4_w,
  rw ← j7,tauto,
  apply partition_els_eq_if_share_el,
  intros,apply x_disjoint,repeat {tauto},
  use w, repeat {tauto},
  intro,
  cases h,
  suffices h₃ : r x w,
  tauto,
  rw ← h_1,
  use j4_w,
  repeat {tauto},
},
have h₃ : P.F = F, tauto,
rw h₃,
rw ← h_2,
unfold classes,
have j3 : rel S = r, solve_by_elim,
simp at *,
rw j3,
suffices z : ∃ y : X, y ∈ a_2,
cases z,
use z_w,
ext,
split,intros,
rw ← h_1,
rw set.mem_set_of_eq,
apply exists.intro,
split,
repeat {tauto},
intro,
rw set.mem_set_of_eq at a_4,
rw ← h_1 at a_4,
cases a_4,
cases a_4_h,
cases a_4_h_right,
have z2 : a_4_w = a_2,
apply partition_els_eq_if_share_el,
intros,apply x_disjoint,repeat {tauto},
use z_w, repeat {tauto},
rwa ← z2,
have z3 : a_2 ≠ ∅,
solve_by_elim,
suffices z4 : a_2.nonempty,
solve_by_elim,
exact ne_empty_iff_nonempty.mp (x_nonempty a_2 a_3),
end

def partitions_biject_with_equivalence_relations :
  equiv (setoid X) (partition X) :=
  begin
    fconstructor,
    apply F,
    apply G,
    apply FG_eq_id,
    apply GF_eq_id,
  end

[Kevin Buzzard]

Oh nice! I went through some of this on my live stream last week.

[Brandon Brown]

oh is it recorded anywhere?

[Alex J. Best]

https://www.youtube.com/watch?v=FEKsZj3WkTY this one I think!

[Kevin Buzzard]

We finished the job on the Discord afterwards and this wasn't recorded

[Brandon Brown]

Ah I notice this time around your partition definition uses the property (unique : ∀ A B ∈ F, A ∩ B ≠ ∅ → A = B) rather than the disjoint property (disjoint : ∀ A B ∈ F, A ≠ B → A ∩ B = ∅) and I suspect the former makes the subsequent proofs easier. I will try re-doing this

[Kevin Buzzard]

It would be even better to use nonempty