# mathlibdocumentation

data.setoid.partition

# 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 #

setoid, equivalence, iseqv, relation, equivalence relation, partition, equivalence class

theorem setoid.eq_of_mem_eqv_class {α : Type u_1} {c : set (set α)} (H : ∀ (a : α), ∃! (b : set α) (H : b c), a b) {x : α} {b b' : set α} (hc : b c) (hb : x b) (hc' : b' c) (hb' : x b') :
b = b'

If x ∈ α is in 2 elements of a set of sets partitioning α, those 2 sets are equal.

def setoid.mk_classes {α : Type u_1} (c : set (set α)) (H : ∀ (a : α), ∃! (b : set α) (H : b c), a b) :

Makes an equivalence relation from a set of sets partitioning α.

Equations
def setoid.classes {α : Type u_1} (r : setoid α) :
set (set α)

Makes the equivalence classes of an equivalence relation.

Equations
theorem setoid.mem_classes {α : Type u_1} (r : setoid α) (y : α) :
{x : α | r.rel x y} r.classes
theorem setoid.eq_iff_classes_eq {α : Type u_1} {r₁ r₂ : setoid α} :
r₁ = r₂ ∀ (x : α), {y : α | r₁.rel x y} = {y : α | r₂.rel x y}

Two equivalence relations are equal iff all their equivalence classes are equal.

theorem setoid.rel_iff_exists_classes {α : Type u_1} (r : setoid α) {x y : α} :
r.rel x y ∃ (c : set α) (H : c r.classes), x c y c
theorem setoid.classes_inj {α : Type u_1} {r₁ r₂ : setoid α} :
r₁ = r₂ r₁.classes = r₂.classes

Two equivalence relations are equal iff their equivalence classes are equal.

theorem setoid.empty_not_mem_classes {α : Type u_1} {r : setoid α} :

The empty set is not an equivalence class.

theorem setoid.classes_eqv_classes {α : Type u_1} {r : setoid α} (a : α) :
∃! (b : set α) (H : b r.classes), a b

Equivalence classes partition the type.

theorem setoid.eq_of_mem_classes {α : Type u_1} {r : setoid α} {x : α} {b : set α} (hc : b r.classes) (hb : x b) {b' : set α} (hc' : b' r.classes) (hb' : x b') :
b = b'

If x ∈ α is in 2 equivalence classes, the equivalence classes are equal.

theorem setoid.eq_eqv_class_of_mem {α : Type u_1} {c : set (set α)} (H : ∀ (a : α), ∃! (b : set α) (H : b c), a b) {s : set α} {y : α} (hs : s c) (hy : y s) :
s = {x : α | H).rel x y}

The elements of a set of sets partitioning α are the equivalence classes of the equivalence relation defined by the set of sets.

theorem setoid.eqv_class_mem {α : Type u_1} {c : set (set α)} (H : ∀ (a : α), ∃! (b : set α) (H : b c), a b) {y : α} :
{x : α | H).rel x y} c

The equivalence classes of the equivalence relation defined by a set of sets partitioning α are elements of the set of sets.

theorem setoid.eqv_class_mem' {α : Type u_1} {c : set (set α)} (H : ∀ (a : α), ∃! (b : set α) (H : b c), a b) {x : α} :
{y : α | H).rel x y} c
theorem setoid.eqv_classes_disjoint {α : Type u_1} {c : set (set α)} (H : ∀ (a : α), ∃! (b : set α) (H : b c), a b) :

Distinct elements of a set of sets partitioning α are disjoint.

theorem setoid.eqv_classes_of_disjoint_union {α : Type u_1} {c : set (set α)} (hu : ⋃₀c = set.univ) (H : c.pairwise_disjoint id) (a : α) :
∃! (b : set α) (H : b c), a b

A set of disjoint sets covering α partition α (classical).

def setoid.setoid_of_disjoint_union {α : Type u_1} {c : set (set α)} (hu : ⋃₀c = set.univ) (H : c.pairwise_disjoint id) :

Makes an equivalence relation from a set of disjoints sets covering α.

Equations
theorem setoid.mk_classes_classes {α : Type u_1} (r : setoid α) :

The equivalence relation made from the equivalence classes of an equivalence relation r equals r.

@[simp]
theorem setoid.sUnion_classes {α : Type u_1} (r : setoid α) :
def setoid.is_partition {α : Type u_1} (c : set (set α)) :
Prop

A collection c : set (set α) of sets is a partition of α into pairwise disjoint sets if ∅ ∉ c and each element a : α belongs to a unique set b ∈ c.

Equations
theorem setoid.nonempty_of_mem_partition {α : Type u_1} {c : set (set α)} (hc : setoid.is_partition c) {s : set α} (h : s c) :

A partition of α does not contain the empty set.

theorem setoid.is_partition_classes {α : Type u_1} (r : setoid α) :
theorem setoid.is_partition.pairwise_disjoint {α : Type u_1} {c : set (set α)} (hc : setoid.is_partition c) :
theorem setoid.is_partition.sUnion_eq_univ {α : Type u_1} {c : set (set α)} (hc : setoid.is_partition c) :
theorem setoid.exists_of_mem_partition {α : Type u_1} {c : set (set α)} (hc : setoid.is_partition c) {s : set α} (hs : s c) :
∃ (y : α), s = {x : α | _).rel x y}

All elements of a partition of α are the equivalence class of some y ∈ α.

theorem setoid.classes_mk_classes {α : Type u_1} (c : set (set α)) (hc : setoid.is_partition c) :
_).classes = c

The equivalence classes of the equivalence relation defined by a partition of α equal the original partition.

@[protected, instance]
def setoid.partition.le {α : Type u_1} :

Defining ≤ on partitions as the ≤ defined on their induced equivalence relations.

Equations
@[protected, instance]
def setoid.partition.partial_order {α : Type u_1} :

Defining a partial order on partitions as the partial order on their induced equivalence relations.

Equations
@[protected]
def setoid.partition.order_iso (α : Type u_1) :
≃o {C //

The order-preserving bijection between equivalence relations on a type α, and partitions of α into subsets.

Equations
@[protected, instance]
def setoid.partition.complete_lattice {α : Type u_1} :

A complete lattice instance for partitions; there is more infrastructure for the equivalent complete lattice on equivalence relations.

Equations
structure indexed_partition {ι : Type u_1} {α : Type u_2} (s : ι → set α) :
Type (max u_1 u_2)
• eq_of_mem : ∀ {x : α} {i j : ι}, x s ix s ji = j
• some : ι → α
• some_mem : ∀ (i : ι), self.some i s i
• index : α → ι
• mem_index : ∀ (x : α), x s (self.index x)

Constructive information associated with a partition of a type α indexed by another type ι, s : ι → set α.

indexed_partition.index sends an element to its index, while indexed_partition.some sends an index to an element of the corresponding set.

This type is primarily useful for definitional control of s - if this is not needed, then setoid.ker index by itself may be sufficient.

noncomputable def indexed_partition.mk' {ι : Type u_1} {α : Type u_2} (s : ι → set α) (dis : ∀ (i j : ι), i jdisjoint (s i) (s j)) (nonempty : ∀ (i : ι), (s i).nonempty) (ex : ∀ (x : α), ∃ (i : ι), x s i) :

The non-constructive constructor for indexed_partition.

Equations
@[protected, instance]
def indexed_partition.inhabited {ι : Type u_1} {α : Type u_2} [unique ι] [inhabited α] :

On a unique index set there is the obvious trivial partition

Equations
theorem indexed_partition.exists_mem {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (x : α) :
∃ (i : ι), x s i
theorem indexed_partition.Union {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) :
(⋃ (i : ι), s i) = set.univ
theorem indexed_partition.disjoint {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) {i j : ι} :
i jdisjoint (s i) (s j)
theorem indexed_partition.mem_iff_index_eq {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) {x : α} {i : ι} :
x s i hs.index x = i
theorem indexed_partition.eq {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (i : ι) :
s i = {x : α | hs.index x = i}
@[protected]
def indexed_partition.setoid {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) :

The equivalence relation associated to an indexed partition. Two elements are equivalent if they belong to the same set of the partition.

@[simp]
theorem indexed_partition.index_some {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (i : ι) :
hs.index (hs.some i) = i
theorem indexed_partition.some_index {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (x : α) :
hs.setoid.rel (hs.some (hs.index x)) x
@[protected]
def indexed_partition.quotient {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) :
Type u_2

The quotient associated to an indexed partition.

Equations
def indexed_partition.proj {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) :
α → hs.quotient

The projection onto the quotient associated to an indexed partition.

Equations
@[protected, instance]
def indexed_partition.quotient.inhabited {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) [inhabited α] :
Equations
theorem indexed_partition.proj_eq_iff {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) {x y : α} :
hs.proj x = hs.proj y hs.index x = hs.index y
@[simp]
theorem indexed_partition.proj_some_index {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (x : α) :
hs.proj (hs.some (hs.index x)) = hs.proj x
def indexed_partition.equiv_quotient {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) :

The obvious equivalence between the quotient associated to an indexed partition and the indexing type.

Equations
@[simp]
theorem indexed_partition.equiv_quotient_index_apply {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (x : α) :
(hs.equiv_quotient) (hs.index x) = hs.proj x
@[simp]
theorem indexed_partition.equiv_quotient_symm_proj_apply {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (x : α) :
(hs.equiv_quotient.symm) (hs.proj x) = hs.index x
theorem indexed_partition.equiv_quotient_index {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) :
def indexed_partition.out {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) :

A map choosing a representative for each element of the quotient associated to an indexed partition. This is a computable version of quotient.out' using indexed_partition.some.

Equations
@[simp]
theorem indexed_partition.out_proj {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (x : α) :
(hs.out) (hs.proj x) = hs.some (hs.index x)

This lemma is analogous to quotient.mk_out'.

theorem indexed_partition.index_out' {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (x : hs.quotient) :
hs.index = hs.index ((hs.out) x)

The indices of quotient.out' and indexed_partition.out are equal.

@[simp]
theorem indexed_partition.proj_out {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (x : hs.quotient) :
hs.proj ((hs.out) x) = x

This lemma is analogous to quotient.out_eq'.

theorem indexed_partition.class_of {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) {x : α} :
set_of (hs.setoid.rel x) = s (hs.index x)
theorem indexed_partition.proj_fiber {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (x : hs.quotient) :
hs.proj ⁻¹' {x} = s ((hs.equiv_quotient.symm) x)