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 IsPartition c
• An indexed partition is a map s : ι → α whose image is a partition. This is expressed as IndexedPartition s.

Of course both implementations are related to Quotient and Setoid.

Setoid.isPartition.partition and Finpartition.isPartition_parts furnish a link between Setoid.IsPartition and Finpartition.

TODO

Could the design of Finpartition inform the one of Setoid.IsPartition? Maybe bundling it and changing it from Set (Set α) to Set α where [Lattice α] [OrderBot α] would make it more usable.

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 α, ∃! x : b ∈ c, a ∈ b) {x : α} {b : Set α} {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.mkClasses {α : Type u_1} (c : Set (Set α)) (H : ∀ (a : α), ∃! b : Set α, ∃! x : b ∈ c, a ∈ b) : Setoid α

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

Equations

• Setoid.mkClasses c H = { r := fun (x y : α) => ∀ s ∈ c, x ∈ s → y ∈ s, iseqv := ⋯ }

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

Makes the equivalence classes of an equivalence relation.

Equations

• Setoid.classes r = {s : Set α | ∃ (y : α), s = {x : α | Setoid.Rel r x y}}

theorem Setoid.mem_classes {α : Type u_1} (r : Setoid α) (y : α) : {x : α | Setoid.Rel r x y} ∈ Setoid.classes r

theorem Setoid.classes_ker_subset_fiber_set {α : Type u_1} {β : Type u_2} (f : α → β) : Setoid.classes (Setoid.ker f) ⊆ Set.range fun (y : β) => {x : α | f x = y}

theorem Setoid.finite_classes_ker {α : Type u_2} {β : Type u_3} [Finite β] (f : α → β) : Set.Finite (Setoid.classes (Setoid.ker f))

theorem Setoid.card_classes_ker_le {α : Type u_2} {β : Type u_3} [Fintype β] (f : α → β) [Fintype ↑(Setoid.classes (Setoid.ker f))] : Fintype.card ↑(Setoid.classes (Setoid.ker f)) ≤ Fintype.card β

theorem Setoid.eq_iff_classes_eq {α : Type u_1} {r₁ : Setoid α} {r₂ : Setoid α} : r₁ = r₂ ↔ ∀ (x : α), {y : α | Setoid.Rel r₁ x y} = {y : α | Setoid.Rel r₂ 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 : α} : Setoid.Rel r x y ↔ ∃ c ∈ Setoid.classes r, x ∈ c ∧ y ∈ c

theorem Setoid.classes_inj {α : Type u_1} {r₁ : Setoid α} {r₂ : Setoid α} : r₁ = r₂ ↔ Setoid.classes r₁ = Setoid.classes r₂

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

theorem Setoid.empty_not_mem_classes {α : Type u_1} {r : Setoid α} : ∅ ∉ Setoid.classes r

The empty set is not an equivalence class.

theorem Setoid.classes_eqv_classes {α : Type u_1} {r : Setoid α} (a : α) : ∃! b : Set α, ∃! x : b ∈ Setoid.classes r, a ∈ b

Equivalence classes partition the type.

theorem Setoid.eq_of_mem_classes {α : Type u_1} {r : Setoid α} {x : α} {b : Set α} (hc : b ∈ Setoid.classes r) (hb : x ∈ b) {b' : Set α} (hc' : b' ∈ Setoid.classes r) (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 α, ∃! x : b ∈ c, a ∈ b) {s : Set α} {y : α} (hs : s ∈ c) (hy : y ∈ s) : s = {x : α | Setoid.Rel (Setoid.mkClasses c H) 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 α, ∃! x : b ∈ c, a ∈ b) {y : α} : {x : α | Setoid.Rel (Setoid.mkClasses c H) 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 α, ∃! x : b ∈ c, a ∈ b) {x : α} : {y : α | Setoid.Rel (Setoid.mkClasses c H) x y} ∈ c

theorem Setoid.eqv_classes_disjoint {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b : Set α, ∃! x : b ∈ c, a ∈ b) : Set.PairwiseDisjoint c id

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 : Set.PairwiseDisjoint c id) (a : α) : ∃! b : Set α, ∃! x : b ∈ c, a ∈ b

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

def Setoid.setoidOfDisjointUnion {α : Type u_1} {c : Set (Set α)} (hu : ⋃₀ c = Set.univ) (H : Set.PairwiseDisjoint c id) : Setoid α

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

Equations

• Setoid.setoidOfDisjointUnion hu H = Setoid.mkClasses c ⋯

theorem Setoid.mkClasses_classes {α : Type u_1} (r : Setoid α) : Setoid.mkClasses (Setoid.classes r) ⋯ = r

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 α) : ⋃₀ Setoid.classes r = Set.univ

noncomputable def Setoid.quotientEquivClasses {α : Type u_1} (r : Setoid α) : Quotient r ≃ ↑(Setoid.classes r)

The equivalence between the quotient by an equivalence relation and its type of equivalence classes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Setoid.quotientEquivClasses_mk_eq {α : Type u_1} (r : Setoid α) (a : α) : ↑((Setoid.quotientEquivClasses r) ⟦a⟧) = {x : α | Setoid.Rel r x a}

def Setoid.IsPartition {α : 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.IsPartition c = (∅ ∉ c ∧ ∀ (a : α), ∃! b : Set α, ∃! x : b ∈ c, a ∈ b)

theorem Setoid.nonempty_of_mem_partition {α : Type u_1} {c : Set (Set α)} (hc : Setoid.IsPartition c) {s : Set α} (h : s ∈ c) : Set.Nonempty s

A partition of α does not contain the empty set.

theorem Setoid.isPartition_classes {α : Type u_1} (r : Setoid α) : Setoid.IsPartition (Setoid.classes r)

theorem Setoid.IsPartition.pairwiseDisjoint {α : Type u_1} {c : Set (Set α)} (hc : Setoid.IsPartition c) : Set.PairwiseDisjoint c id

theorem Setoid.IsPartition.sUnion_eq_univ {α : Type u_1} {c : Set (Set α)} (hc : Setoid.IsPartition c) : ⋃₀ c = Set.univ

theorem Setoid.exists_of_mem_partition {α : Type u_1} {c : Set (Set α)} (hc : Setoid.IsPartition c) {s : Set α} (hs : s ∈ c) : ∃ (y : α), s = {x : α | Setoid.Rel (Setoid.mkClasses c ⋯) x y}

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

theorem Setoid.classes_mkClasses {α : Type u_1} (c : Set (Set α)) (hc : Setoid.IsPartition c) : Setoid.classes (Setoid.mkClasses c ⋯) = c

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

instance Setoid.Partition.le {α : Type u_1} : LE (Subtype Setoid.IsPartition)

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

Equations

• Setoid.Partition.le = { le := fun (x y : Subtype Setoid.IsPartition) => Setoid.mkClasses ↑x ⋯ ≤ Setoid.mkClasses ↑y ⋯ }

instance Setoid.Partition.partialOrder {α : Type u_1} : PartialOrder (Subtype Setoid.IsPartition)

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

Equations

• Setoid.Partition.partialOrder = PartialOrder.mk ⋯

def Setoid.Partition.orderIso (α : Type u_1) : Setoid α ≃o { C : Set (Set α) // Setoid.IsPartition C }

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

Equations

• One or more equations did not get rendered due to their size.

instance Setoid.Partition.completeLattice {α : Type u_1} : CompleteLattice (Subtype Setoid.IsPartition)

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

Equations

• Setoid.Partition.completeLattice = GaloisInsertion.liftCompleteLattice (OrderIso.toGaloisInsertion (Setoid.Partition.orderIso α))

@[simp]

theorem Setoid.IsPartition.finpartition_parts {α : Type u_1} {c : Finset (Set α)} (hc : Setoid.IsPartition ↑c) : (Setoid.IsPartition.finpartition hc).parts = c

def Setoid.IsPartition.finpartition {α : Type u_1} {c : Finset (Set α)} (hc : Setoid.IsPartition ↑c) : Finpartition Set.univ

A finite setoid partition furnishes a finpartition

Equations

• Setoid.IsPartition.finpartition hc = { parts := c, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }

theorem Finpartition.isPartition_parts {α : Type u_1} (f : Finpartition Set.univ) : Setoid.IsPartition ↑f.parts

A finpartition gives rise to a setoid partition

structure IndexedPartition {ι : Type u_1} {α : Type u_2} (s : ι → Set α) : Type (max u_1 u_2)

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

IndexedPartition.index sends an element to its index, while IndexedPartition.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.

• eq_of_mem : ∀ {x : α} {i j : ι}, x ∈ s i → x ∈ s j → i = j

  two indexes are equal if they are equal in membership

• some : ι → α

  sends an index to an element of the corresponding set

• some_mem : ∀ (i : ι), self.some i ∈ s i

  membership invariance for some

• index : α → ι

  index for type α

• mem_index : ∀ (x : α), x ∈ s (self.index x)

  membership invariance for index

noncomputable def IndexedPartition.mk' {ι : Type u_1} {α : Type u_2} (s : ι → Set α) (dis : Pairwise fun (i j : ι) => Disjoint (s i) (s j)) (nonempty : ∀ (i : ι), Set.Nonempty (s i)) (ex : ∀ (x : α), ∃ (i : ι), x ∈ s i) : IndexedPartition s

The non-constructive constructor for IndexedPartition.

Equations

• IndexedPartition.mk' s dis nonempty ex = { eq_of_mem := ⋯, some := fun (i : ι) => Set.Nonempty.some ⋯, some_mem := ⋯, index := fun (x : α) => Exists.choose ⋯, mem_index := ⋯ }

instance IndexedPartition.instInhabitedIndexedPartitionUniv {ι : Type u_1} {α : Type u_2} [Unique ι] [Inhabited α] : Inhabited (IndexedPartition fun (_i : ι) => Set.univ)

On a unique index set there is the obvious trivial partition

Equations

• IndexedPartition.instInhabitedIndexedPartitionUniv = { default := { eq_of_mem := ⋯, some := default, some_mem := ⋯, index := default, mem_index := ⋯ } }

theorem IndexedPartition.exists_mem {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α) : ∃ (i : ι), x ∈ s i

theorem IndexedPartition.iUnion {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) : ⋃ (i : ι), s i = Set.univ

theorem IndexedPartition.disjoint {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) : Pairwise fun (i j : ι) => Disjoint (s i) (s j)

theorem IndexedPartition.mem_iff_index_eq {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {x : α} {i : ι} : x ∈ s i ↔ hs.index x = i

theorem IndexedPartition.eq {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (i : ι) : s i = {x : α | hs.index x = i}

@[inline, reducible]

abbrev IndexedPartition.setoid {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) : Setoid α

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

Equations

• IndexedPartition.setoid hs = Setoid.ker hs.index

@[simp]

theorem IndexedPartition.index_some {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (i : ι) : hs.index (hs.some i) = i

theorem IndexedPartition.some_index {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α) : Setoid.Rel (IndexedPartition.setoid hs) (hs.some (hs.index x)) x

def IndexedPartition.Quotient {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) : Type u_2

The quotient associated to an indexed partition.

Equations

• IndexedPartition.Quotient hs = Quotient (IndexedPartition.setoid hs)

def IndexedPartition.proj {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) : α → IndexedPartition.Quotient hs

The projection onto the quotient associated to an indexed partition.

Equations

• IndexedPartition.proj hs = Quotient.mk''

instance IndexedPartition.instInhabitedQuotient {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) [Inhabited α] : Inhabited (IndexedPartition.Quotient hs)

Equations

• IndexedPartition.instInhabitedQuotient hs = { default := IndexedPartition.proj hs default }

theorem IndexedPartition.proj_eq_iff {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {x : α} {y : α} : IndexedPartition.proj hs x = IndexedPartition.proj hs y ↔ hs.index x = hs.index y

@[simp]

theorem IndexedPartition.proj_some_index {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α) : IndexedPartition.proj hs (hs.some (hs.index x)) = IndexedPartition.proj hs x

def IndexedPartition.equivQuotient {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) : ι ≃ IndexedPartition.Quotient hs

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

Equations

• IndexedPartition.equivQuotient hs = (Setoid.quotientKerEquivOfRightInverse hs.index hs.some ⋯).symm

@[simp]

theorem IndexedPartition.equivQuotient_index_apply {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α) : (IndexedPartition.equivQuotient hs) (hs.index x) = IndexedPartition.proj hs x

@[simp]

theorem IndexedPartition.equivQuotient_symm_proj_apply {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α) : (IndexedPartition.equivQuotient hs).symm (IndexedPartition.proj hs x) = hs.index x

theorem IndexedPartition.equivQuotient_index {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) : ⇑(IndexedPartition.equivQuotient hs) ∘ hs.index = IndexedPartition.proj hs

def IndexedPartition.out {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) : IndexedPartition.Quotient hs ↪ α

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 IndexedPartition.some.

Equations

• IndexedPartition.out hs = Function.Embedding.trans (Equiv.toEmbedding (IndexedPartition.equivQuotient hs).symm) { toFun := hs.some, inj' := ⋯ }

@[simp]

theorem IndexedPartition.out_proj {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α) : (IndexedPartition.out hs) (IndexedPartition.proj hs x) = hs.some (hs.index x)

This lemma is analogous to Quotient.mk_out'.

theorem IndexedPartition.index_out' {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : IndexedPartition.Quotient hs) : hs.index (Quotient.out' x) = hs.index ((IndexedPartition.out hs) x)

The indices of Quotient.out' and IndexedPartition.out are equal.

@[simp]

theorem IndexedPartition.proj_out {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : IndexedPartition.Quotient hs) : IndexedPartition.proj hs ((IndexedPartition.out hs) x) = x

This lemma is analogous to Quotient.out_eq'.

theorem IndexedPartition.class_of {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {x : α} : setOf (Setoid.Rel (IndexedPartition.setoid hs) x) = s (hs.index x)

theorem IndexedPartition.proj_fiber {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : IndexedPartition.Quotient hs) : IndexedPartition.proj hs ⁻¹' {x} = s ((IndexedPartition.equivQuotient hs).symm x)

def IndexedPartition.piecewise {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {β : Type u_3} (f : ι → α → β) : α → β

Combine functions with disjoint domains into a new function. You can use the regular expression def.*piecewise to search for other ways to define piecewise functions in mathlib4.

Equations

• IndexedPartition.piecewise hs f x = f (hs.index x) x

theorem IndexedPartition.piecewise_apply {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {β : Type u_3} {f : ι → α → β} (x : α) : IndexedPartition.piecewise hs f x = f (hs.index x) x

theorem IndexedPartition.piecewise_inj {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {β : Type u_3} {f : ι → α → β} (h_injOn : ∀ (i : ι), Set.InjOn (f i) (s i)) (h_disjoint : Set.PairwiseDisjoint Set.univ fun (i : ι) => f i '' s i) : Function.Injective (IndexedPartition.piecewise hs f)

A family of injective functions with pairwise disjoint domains and pairwise disjoint ranges can be glued together to form an injective function.

theorem IndexedPartition.piecewise_bij {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {β : Type u_3} {f : ι → α → β} {t : ι → Set β} (ht : IndexedPartition t) (hf : ∀ (i : ι), Set.BijOn (f i) (s i) (t i)) : Function.Bijective (IndexedPartition.piecewise hs f)

A family of bijective functions with pairwise disjoint domains and pairwise disjoint ranges can be glued together to form a bijective function.