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 elementa : α
belongs to a unique setb ∈ c
. This is expressed asis_partition c
- An indexed partition is a map
s : ι → α
whose image is a partition. This is expressed asindexed_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
The elements of a set of sets partitioning α are the equivalence classes of the equivalence relation defined by the set of sets.
The equivalence classes of the equivalence relation defined by a set of sets partitioning α are elements of the set of sets.
Makes an equivalence relation from a set of disjoints sets covering α.
Equations
The equivalence relation made from the equivalence classes of an equivalence relation r equals r.
A partition of α
does not contain the empty set.
All elements of a partition of α are the equivalence class of some y ∈ α.
The equivalence classes of the equivalence relation defined by a partition of α equal the original 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 _}
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 := _}
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' := _}
A complete lattice instance for partitions; there is more infrastructure for the equivalent complete lattice on equivalence relations.
A finite setoid partition furnishes a finpartition
Equations
- hc.finpartition = {parts := c, sup_indep := _, sup_parts := _, not_bot_mem := _}
A finpartition gives rise to a setoid partition
- 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
The non-constructive constructor for indexed_partition
.
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 := _}}
The equivalence relation associated to an indexed partition. Two elements are equivalent if they belong to the same set of the partition.
The quotient associated to an indexed partition.
Instances for indexed_partition.quotient
The projection onto the quotient associated to an indexed partition.
Equations
- hs.proj = quotient.mk'
Equations
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
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' := _}
This lemma is analogous to quotient.mk_out'
.
The indices of quotient.out'
and indexed_partition.out
are equal.
This lemma is analogous to quotient.out_eq'
.