## Stream: new members

### Topic: Sets, Types, Partitions, Eqv Relations

#### Brandon Brown (Jul 09 2020 at 19:37):

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 (Jul 09 2020 at 22:30):

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

#### Brandon Brown (Jul 10 2020 at 01:48):

oh is it recorded anywhere?

#### Kevin Buzzard (Jul 10 2020 at 14:02):

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

#### Brandon Brown (Jul 10 2020 at 20:17):

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 (Jul 11 2020 at 08:42):

It would be even better to use nonempty

Last updated: May 16 2021 at 21:11 UTC