Equivalence relations: partitions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

setoid.is_partition.partition and finpartition.is_partition_parts furnish a link between setoid.is_partition and finpartition.

TODO #

Could the design of finpartition inform the one of setoid.is_partition? Maybe bundling it and changing it from set (set α) to set α where [lattice α] [order_bot α] would make it more usable.

Tags #

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

source

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.

source

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

setoid α

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

Equations

setoid.mk_classes c H = {r := λ (x y : α), ∀ (s : set α), s ∈ c → x ∈ s → y ∈ s, iseqv := _}

source

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

set (set α)

Makes the equivalence classes of an equivalence relation.

Equations

r.classes = {s : set α | ∃ (y : α), s = {x : α | r.rel x y}}

source

theorem setoid.mem_classes {α : Type u_1} (r : setoid α) (y : α) :

{x : α | r.rel x y} ∈ r.classes

source

theorem setoid.classes_ker_subset_fiber_set {α : Type u_1} {β : Type u_2} (f : α → β) :

(setoid.ker f).classes ⊆ set.range (λ (y : β), {x : α | f x = y})

source

theorem setoid.finite_classes_ker {α : Type u_1} {β : Type u_2} [finite β] (f : α → β) :

(setoid.ker f).classes.finite

source

theorem setoid.card_classes_ker_le {α : Type u_1} {β : Type u_2} [fintype β] (f : α → β) [fintype ↥((setoid.ker f).classes)] :

fintype.card ↥((setoid.ker f).classes) ≤ fintype.card β

source

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.

source

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

source

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.

source

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

∅ ∉ r.classes

The empty set is not an equivalence class.

source

theorem setoid.classes_eqv_classes {α : Type u_1} {r : setoid α} (a : α) :

∃! (b : set α) (H : b ∈ r.classes), a ∈ b

Equivalence classes partition the type.

source

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.

source

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 : α | (setoid.mk_classes c 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.

source

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

{x : α | (setoid.mk_classes c 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.

source

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

{y : α | (setoid.mk_classes c H).rel x y} ∈ c

source

theorem setoid.eqv_classes_disjoint {α : Type u_1} {c : set (set α)} (H : ∀ (a : α), ∃! (b : set α) (H : b ∈ c), a ∈ b) :

c.pairwise_disjoint id

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

source

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).

source

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

setoid α

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

Equations

setoid.setoid_of_disjoint_union hu H = setoid.mk_classes c _

source

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

setoid.mk_classes r.classes setoid.classes_eqv_classes = r

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

source

@[simp]

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

⋃₀ r.classes = set.univ

source

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

setoid.is_partition c = (∅ ∉ c ∧ ∀ (a : α), ∃! (b : set α) (H : b ∈ c), a ∈ b)

source

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

s.nonempty

A partition of α does not contain the empty set.

source

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

setoid.is_partition r.classes

source

theorem setoid.is_partition.pairwise_disjoint {α : Type u_1} {c : set (set α)} (hc : setoid.is_partition c) :

c.pairwise_disjoint id

source

theorem setoid.is_partition.sUnion_eq_univ {α : Type u_1} {c : set (set α)} (hc : setoid.is_partition c) :

⋃₀ c = set.univ

source

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 : α | (setoid.mk_classes c _).rel x y}

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

source

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

(setoid.mk_classes c _).classes = c

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

source

@[protected, instance]

def setoid.partition.le {α : Type u_1} :

has_le (subtype setoid.is_partition)

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

Equations

setoid.partition.le = {le := λ (x y : subtype setoid.is_partition), setoid.mk_classes x.val _ ≤ setoid.mk_classes y.val _}

source

@[protected, instance]

def setoid.partition.partial_order {α : Type u_1} :

partial_order (subtype setoid.is_partition)

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

Equations

setoid.partition.partial_order = {le := has_le.le setoid.partition.le, lt := λ (x y : subtype setoid.is_partition), x ≤ y ∧ ¬y ≤ x, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected]

def setoid.partition.order_iso (α : Type u_1) :

setoid α ≃o {C // setoid.is_partition C}

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

Equations

setoid.partition.order_iso α = {to_equiv := {to_fun := λ (r : setoid α), ⟨r.classes, _⟩, inv_fun := λ (C : {C // setoid.is_partition C}), setoid.mk_classes C.val _, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[protected, instance]

def setoid.partition.complete_lattice {α : Type u_1} :

complete_lattice (subtype setoid.is_partition)

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

Equations

setoid.partition.complete_lattice = (setoid.partition.order_iso α).to_galois_insertion.lift_complete_lattice

source

def setoid.is_partition.finpartition {α : Type u_1} {c : finset (set α)} (hc : setoid.is_partition ↑c) :

finpartition set.univ

A finite setoid partition furnishes a finpartition

Equations

hc.finpartition = {parts := c, sup_indep := _, sup_parts := _, not_bot_mem := _}

source

@[simp]

theorem setoid.is_partition.finpartition_parts {α : Type u_1} {c : finset (set α)} (hc : setoid.is_partition ↑c) :

hc.finpartition.parts = c

source

theorem finpartition.is_partition_parts {α : Type u_1} (f : finpartition set.univ) :

setoid.is_partition ↑(f.parts)

A finpartition gives rise to a setoid partition

source

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 i → x ∈ s j → i = 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.

Instances for indexed_partition

indexed_partition.has_sizeof_inst
indexed_partition.inhabited

source

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

indexed_partition s

The non-constructive constructor for indexed_partition.

Equations

indexed_partition.mk' s dis nonempty ex = {eq_of_mem := _, some := λ (i : ι), _.some, some_mem := _, index := λ (x : α), _.some, mem_index := _}

source

@[protected, instance]

def indexed_partition.inhabited {ι : Type u_1} {α : Type u_2} [unique ι] [inhabited α] :

inhabited (indexed_partition (λ (i : ι), set.univ))

On a unique index set there is the obvious trivial partition

Equations

indexed_partition.inhabited = {default := {eq_of_mem := _, some := inhabited.default (pi.inhabited ι), some_mem := _, index := inhabited.default (pi.inhabited α), mem_index := _}}

source

theorem indexed_partition.exists_mem {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (x : α) :

∃ (i : ι), x ∈ s i

source

theorem indexed_partition.Union {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) :

(⋃ (i : ι), s i) = set.univ

source

theorem indexed_partition.disjoint {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) {i j : ι} :

i ≠ j → disjoint (s i) (s j)

source

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

source

theorem indexed_partition.eq {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) (i : ι) :

s i = {x : α | hs.index x = i}

source

@[protected, reducible]

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

setoid α

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

source

@[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

source

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

source

@[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

hs.quotient = quotient hs.setoid

Instances for indexed_partition.quotient

indexed_partition.quotient.inhabited

source

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

hs.proj = quotient.mk'

source

@[protected, instance]

def indexed_partition.quotient.inhabited {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) [inhabited α] :

inhabited hs.quotient

Equations

indexed_partition.quotient.inhabited hs = {default := hs.proj inhabited.default}

source

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

source

@[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

source

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

ι ≃ hs.quotient

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

Equations

hs.equiv_quotient = (setoid.quotient_ker_equiv_of_right_inverse hs.index hs.some _).symm

source

@[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

source

@[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

source

theorem indexed_partition.equiv_quotient_index {ι : Type u_1} {α : Type u_2} {s : ι → set α} (hs : indexed_partition s) :

⇑(hs.equiv_quotient) ∘ hs.index = hs.proj

source

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

hs.quotient ↪ α

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

hs.out = hs.equiv_quotient.symm.to_embedding.trans {to_fun := hs.some, inj' := _}

source

@[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'.

source

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

hs.index (quotient.out' x) = hs.index (⇑(hs.out) x)

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

source

@[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'.

source

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)

source

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)