[Merged by Bors] - feat(data/setoid/partition): indexed partition

src/data/quot.lean

@@ -218,6 +218,13 @@ noncomputable def quotient.out [s : setoid α] : quotient s → α := quot.out
 theorem quotient.mk_out [s : setoid α] (a : α) : ⟦a⟧.out ≈ a :=
 quotient.exact (quotient.out_eq _)
 
+lemma quotient.mk_eq_iff_out [s : setoid α] {x : α} {y : quotient s} :
+  ⟦x⟧ = y ↔ x ≈ quotient.out y :=
+begin
+  refine iff.trans _ quotient.eq,
+  rw quotient.out_eq y,
+end
+
 instance pi_setoid {ι : Sort*} {α : ι → Sort*} [∀ i, setoid (α i)] : setoid (Π i, α i) :=
 { r := λ a b, ∀ i, a i ≈ b i,
   iseqv := ⟨

src/data/setoid/basic.lean

@@ -61,6 +61,9 @@ theorem le_def {r s : setoid α} : r ≤ s ↔ ∀ {x y}, r.rel x y → s.rel x
 @[trans] lemma trans' (r : setoid α) : ∀ {x y z}, r.rel x y → r.rel y z → r.rel x z :=
 λ _ _ _ hx, r.2.2.2 hx
 
+lemma comm' (s : setoid α) {x y} : s.rel x y ↔ s.rel y x :=
+⟨s.symm', s.symm'⟩
+
 /-- The kernel of a function is an equivalence relation. -/
 def ker (f : α → β) : setoid α :=
 ⟨λ x y, f x = f y, ⟨λ _, rfl, λ _ _ h, h.symm, λ _ _ _ h, h.trans⟩⟩
@@ -69,6 +72,10 @@ def ker (f : α → β) : setoid α :=
 @[simp] lemma ker_mk_eq (r : setoid α) : ker (@quotient.mk _ r) = r :=
 ext' $ λ x y, quotient.eq
 
+@[simp] lemma ker_apply_mk_out' {f : α → β} (a : α) :
+  f ((quotient.mk' a : quotient $ setoid.ker f).out') = f a :=
+@quotient.mk_out' _ (setoid.ker f) a
+
 lemma ker_def {f : α → β} {x y : α} : (ker f).rel x y ↔ f x = f y := iff.rfl
 
 /-- Given types `α`, `β`, the product of two equivalence relations `r` on `α` and `s` on `β`:

src/data/setoid/partition.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Amelia Livingston. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Amelia Livingston, Bryan Gin-ge Chen
+Authors: Amelia Livingston, Bryan Gin-ge Chen, Patrick Massot
 -/
 
 import data.setoid.basic
@@ -11,6 +11,13 @@ import data.set.lattice
 # Equivalence relations: partitions
 
 This file comprises properties of equivalence relations viewed as partitions.
+There are two implementations of partitions here:
+* A collection `c : set (set α)` of sets is a partition of `α` if `∅ ∉ c` and each element `a : α`
+  belongs to a unique set `b ∈ c`. This is expressed as `is_partition c`
+* An indexed partition is a map `s : ι → α` whose image is a partition. This is
+  expressed as `indexed_partition s`.
+
+Of course both implementations are related to `quotient` and `setoid`.
 
 ## Tags
 
@@ -94,6 +101,10 @@ lemma eqv_class_mem {c : set (set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {y} :
   {x | (mk_classes c H).rel x y} ∈ c :=
 (H y).elim2 $ λ b hc hy hb, eq_eqv_class_of_mem H hc hy ▸ hc
 
+lemma eqv_class_mem' {c : set (set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {x} :
+  {y : α | (mk_classes c H).rel x y} ∈ c :=
+by { convert setoid.eqv_class_mem H, ext, rw setoid.comm' }
+
 /-- Distinct elements of a set of sets partitioning α are disjoint. -/
 lemma eqv_classes_disjoint {c : set (set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) :
   set.pairwise_disjoint c :=
@@ -201,3 +212,113 @@ _ (subtype (@is_partition α)) _ (partial_order.to_preorder _) $ partition.rel_i
 end partition
 
 end setoid
+
+/-- A partition of a type indexed by another type. -/
+@[nolint has_inhabited_instance]
+structure indexed_partition {ι α : Type*} (s : ι → set α) :=
+(eq_of_mem : ∀ {x i j}, x ∈ s i → x ∈ s j → i = j)
+(some : ι → α)
+(some_mem : ∀ i, some i ∈ s i)
+(index : α → ι)
+(mem_index : ∀ x, x ∈ s (index x))
+
+/-- The non-constructive constructor for `indexed_partition`. -/
+noncomputable
+def indexed_partition.mk' {ι α : Type*} (s : ι → set α) (dis : ∀ i j, i ≠ j → disjoint (s i) (s j))
+(empty : ∀ i, (s i).nonempty) (ex : ∀ x, ∃ i, x ∈ s i) : indexed_partition s :=
+{ eq_of_mem := begin
+    classical,
+    intros x i j hxi hxj,
+    by_contra h,
+    exact dis _ _ h ⟨hxi, hxj⟩
+  end,
+  some := λ i, (empty i).some,
+  some_mem := λ i, (empty i).some_spec,
+  index := λ x, (ex x).some,
+  mem_index := λ x, (ex x).some_spec }
+
+namespace indexed_partition
+
+open set
+
+variables {ι α : Type*} {s : ι → set α} (hs : indexed_partition s)
+include hs
+
+lemma exists_mem (x : α) : ∃ i, x ∈ s i := ⟨hs.index x, hs.mem_index x⟩
+
+lemma Union : (⋃ i, s i) = univ :=
+by { ext x, simp [hs.exists_mem x] }
+
+lemma disjoint : ∀ {i j}, i ≠ j → disjoint (s i) (s j) :=
+λ i j h x ⟨hxi, hxj⟩, h (hs.eq_of_mem hxi hxj)
+
+lemma mem_iff_index_eq {x i} : x ∈ s i ↔ hs.index x = i :=
+⟨λ hxi, (hs.eq_of_mem hxi (hs.mem_index x)).symm, λ h, h ▸ hs.mem_index _⟩
+
+/-- The equivalence relation associated to an indexed partition. Two
+elements are equivalent if they belong to the same set of the partition. -/
+protected def setoid (hs : indexed_partition s) : setoid α :=
+setoid.ker hs.index
+
+@[simp] lemma index_some (i : ι) : hs.index (hs.some i) = i :=
+(mem_iff_index_eq _).1 $ hs.some_mem i
+
+lemma some_index (x : α) : hs.setoid.rel (hs.some (hs.index x)) x :=
+hs.index_some (hs.index x)
+
+/-- The quotient associated to an indexed partition. -/
+@[nolint has_inhabited_instance]
+protected def quotient := quotient hs.setoid
+
+/-- The projection onto the quotient associated to an indexed partition. -/
+def proj : α → hs.quotient := quotient.mk'
+
+lemma proj_eq_iff {x y : α} : hs.proj x = hs.proj y ↔ hs.setoid.rel x y :=
+quotient.eq_rel
+
+/-- A map choosing a representative for each element of the quotient associated to an indexed
+partition. -/
+noncomputable
+def out : hs.quotient → α := quotient.out'
+
+@[simp] lemma proj_out (x : hs.quotient) : hs.proj (hs.out x) = x :=
+quotient.out_eq' _
+
+lemma out_proj (x : α) : hs.setoid.rel (hs.out (hs.proj x)) x :=
+quotient.mk_out' x
+
+@[simp] lemma index_out_proj (x : α) : hs.index (hs.out (hs.proj x)) = hs.index x :=
+setoid.ker_apply_mk_out' x
+
+@[simp] lemma proj_some_index (x : α) : hs.proj (hs.some (hs.index x)) = hs.proj x :=
+quotient.eq'.2 (hs.some_index x)
+
+@[simp] lemma out_proj_some (i : ι) : hs.out (hs.proj (hs.some i)) ∈ s i :=
+hs.mem_iff_index_eq.2 $ by simp
+
+@[simp] lemma index_out_proj_some (i : ι) : hs.index (hs.out $ hs.proj $ hs.some i) = i :=
+by simp
+
+lemma class_of {x : α} : set_of (hs.setoid.rel x) = s (hs.index x) :=
+set.ext $ λ y, (hs.mem_iff_index_eq.trans eq_comm).symm
+
+/-- The obvious equivalence between the quotient associated to an indexed partition and
+the indexing type. -/
+def equiv_quotient : ι ≃ hs.quotient :=
+(setoid.quotient_ker_equiv_of_right_inverse hs.index hs.some $ hs.index_some).symm
+
+@[simp] lemma equiv_quotient_index_apply (x : α) : hs.equiv_quotient (hs.index x) = hs.proj x :=
+hs.proj_eq_iff.mpr (some_index hs x)
+
+lemma equiv_quotient_index : hs.equiv_quotient ∘ hs.index = hs.proj :=
+funext hs.equiv_quotient_index_apply
+
+lemma proj_fiber (x : hs.quotient) : hs.proj ⁻¹' {x} = s (hs.equiv_quotient.symm x) :=
+begin
+  ext y,
+  rcases x,
+  simp only [set.mem_preimage, set.mem_singleton_iff, hs.mem_iff_index_eq],
+  exact quotient.eq',
+end
+
+end indexed_partition