Partitions

A Partition of an element a in a complete lattice is an independent family of nontrivial elements whose supremum is a.

An important special case is where s : Set α, where a Partition s corresponds to a partition of the elements of s into a family of nonempty sets. This is equivalent to a transitive and symmetric binary relation r : α → α → Prop where s is the set of all x for which r x x.

Partitions are ordered by refinement: P ≤ Q if every part of P is less than or equal to a part of Q.

Main declarations

• Partition s: For [CompleteLattice α] and s : α, a Partition s is an independent collection of nontrivial elements whose supremum is s.
• Partition.removeBot: A constructor for Partition s that removes ⊥ from a set of parts.
• Partition.instOrderTop: Partition s has a top element, consisting of just s if s ≠ ⊥ or nothing otherwise.
• Partition.instSemilatticeInf: Partition s has finite meets P ⊓ Q when α is a frame, given by the collection of all non-bottom infima p ⊓ q of parts of the two partitions.
• Partition.Rel: The partial equivalence relation induced by a partition of a set.
• Partition.IsRepFun: A predicate characterizing a representative function for a partition.

Representative functions (IsRepFun)

IsRepFun P f means that f sends each element of the support to a representative in its Partition.Rel-class, agrees on related elements, and is the identity outside the support.

This is useful whenever a construction must pick one distinguished element per part of a partition. For example, in graph theory one may partition edges into parallel classes or vertices into connected components; a representative function can specify which edge remains when simplifying parallel edges, or how supervertices are labeled after contraction. Similar uses arise in matroid theory and in the definition of minors.

Tempting alternatives are to use Classical.choice or fix a global well-order and take minimal representatives. However, these lead to issues with inconsistencies: independent choices need not respect relations between different instances (e.g. monotonicity of simplifications with respect to subgraph order), a global order can clash with structure already carried by the type, and maps between different types need not intertwine two separate canonical choices. Stating hypotheses with IsRepFun keeps the chosen representatives explicit; existence under suitable conditions can be proved separately.

TODO

• Link this to Finpartition.
• Show that when α is a frame Partition α also has finite joins, i.e. that it is a lattice.

structure Partition {α : Type u_1} [CompleteLattice α] (s : α) : Type u_1

A Partition of an element s of a CompleteLattice is a collection of independent nontrivial elements whose supremum is s.

• parts : Set α

  The collection of parts

• sSupIndep' : _root_.sSupIndep self.parts

  The parts are sSupIndep.

• bot_notMem' : ⊥ ∉ self.parts

  The bottom element is not a part.

• sSup_eq' : sSup self.parts = s

  The supremum of all parts is s.

@[implicit_reducible]

instance Partition.instSetLike {α : Type u_1} [CompleteLattice α] {s : α} : SetLike (Partition s) α

Equations

• Partition.instSetLike = { coe := Partition.parts, coe_injective' := ⋯ }

def Partition.Simps.coe {α : Type u_1} [CompleteLattice α] {s : α} (P : Partition s) : Set α

See Note [custom simps projection].

Equations

• Partition.Simps.coe P = ↑P

@[simp]

theorem Partition.coe_parts {α : Type u_1} {s : α} [CompleteLattice α] {P : Partition s} : P.parts = ↑P

theorem Partition.ext {α : Type u_1} {s : α} [CompleteLattice α] {P Q : Partition s} (hP : ∀ (x : α), x ∈ P ↔ x ∈ Q) : P = Q

theorem Partition.ext_iff {α : Type u_1} {s : α} [CompleteLattice α] {P Q : Partition s} : P = Q ↔ ∀ (x : α), x ∈ P ↔ x ∈ Q

@[simp]

theorem Partition.sSupIndep {α : Type u_1} {s : α} [CompleteLattice α] (P : Partition s) : _root_.sSupIndep ↑P

theorem Partition.disjoint {α : Type u_1} {s x y : α} [CompleteLattice α] {P : Partition s} (hx : x ∈ P) (hy : y ∈ P) (hxy : x ≠ y) : Disjoint x y

theorem Partition.pairwiseDisjoint {α : Type u_1} {s : α} [CompleteLattice α] {P : Partition s} : (↑P).PairwiseDisjoint id

theorem Partition.eq_or_disjoint {α : Type u_1} {s x y : α} [CompleteLattice α] {P : Partition s} (hx : x ∈ P) (hy : y ∈ P) : x = y ∨ Disjoint x y

theorem Partition.eq_of_not_disjoint {α : Type u_1} {s x y : α} [CompleteLattice α] {P : Partition s} (hx : x ∈ P) (hy : y ∈ P) (hxy : ¬Disjoint x y) : x = y

@[simp]

theorem Partition.sSup_eq {α : Type u_1} {s : α} [CompleteLattice α] (P : Partition s) : sSup ↑P = s

@[simp]

theorem Partition.iSup_eq {α : Type u_1} {s : α} [CompleteLattice α] (P : Partition s) : ⨆ x ∈ P, x = s

theorem Partition.le_of_mem {α : Type u_1} {s x : α} [CompleteLattice α] (P : Partition s) (hx : x ∈ P) : x ≤ s

theorem Partition.parts_nonempty {α : Type u_1} {s : α} [CompleteLattice α] (P : Partition s) (hs : s ≠ ⊥) : (↑P).Nonempty

@[simp]

theorem Partition.bot_notMem {α : Type u_1} {s : α} [CompleteLattice α] (P : Partition s) : ⊥ ∉ P

theorem Partition.ne_bot_of_mem {α : Type u_1} {s x : α} [CompleteLattice α] {P : Partition s} (hx : x ∈ P) : x ≠ ⊥

theorem Partition.bot_lt_of_mem {α : Type u_1} {s x : α} [CompleteLattice α] {P : Partition s} (hx : x ∈ P) : ⊥ < x

def Partition.copy {α : Type u_1} {s t : α} [CompleteLattice α] (P : Partition s) (hst : s = t) : Partition t

Convert a Partition s into a Partition t via an equality s = t.

Equations

• P.copy hst = { parts := ↑P, sSupIndep' := ⋯, bot_notMem' := ⋯, sSup_eq' := ⋯ }

@[simp]

theorem Partition.coe_copy {α : Type u_1} {s t : α} [CompleteLattice α] (P : Partition s) (hst : s = t) : ↑(P.copy hst) = ↑P

@[simp]

theorem Partition.mem_copy_iff {α : Type u_1} {s t x : α} [CompleteLattice α] {P : Partition s} (hst : s = t) : x ∈ P.copy hst ↔ x ∈ P

def Partition.partscopyEquiv {α : Type u_1} {s t : α} [CompleteLattice α] (P : Partition s) (hst : s = t) : ↥(P.copy hst) ≃ ↥P

The natural equivalence between the subtype of parts and the subtype of parts of a copy.

Equations

• P.partscopyEquiv hst = Equiv.setCongr ⋯

@[simp]

theorem Partition.partscopyEquiv_symm_apply_coe {α : Type u_1} {s t : α} [CompleteLattice α] (P : Partition s) (hst : s = t) (b : { b : α // (fun (x : α) => x ∈ ↑P) b }) : ↑((P.partscopyEquiv hst).symm b) = ↑b

@[simp]

theorem Partition.partscopyEquiv_apply_coe {α : Type u_1} {s t : α} [CompleteLattice α] (P : Partition s) (hst : s = t) (a : { a : α // (fun (x : α) => x ∈ ↑(P.copy hst)) a }) : ↑((P.partscopyEquiv hst) a) = ↑a

def Partition.removeBot {α : Type u_1} {s : α} [CompleteLattice α] (P : Set α) (indep : _root_.sSupIndep P) (sSup_eq : sSup P = s) : Partition s

A constructor for Partition s that removes ⊥ from the set of parts.

Equations

• Partition.removeBot P indep sSup_eq = { parts := P \ {⊥}, sSupIndep' := ⋯, bot_notMem' := ⋯, sSup_eq' := ⋯ }

@[simp]

theorem Partition.coe_removeBot {α : Type u_1} {s : α} [CompleteLattice α] (P : Set α) (indep : _root_.sSupIndep P) (sSup_eq : sSup P = s) : ↑(removeBot P indep sSup_eq) = P \ {⊥}

@[simp]

theorem Partition.mem_removeBot {α : Type u_1} {s x : α} [CompleteLattice α] (P : Set α) (indep : _root_.sSupIndep P) (sSup_eq : sSup P = s) : x ∈ removeBot P indep sSup_eq ↔ x ∈ P ∧ x ≠ ⊥

@[simp]

theorem Partition.notMem_of_bot {α : Type u_1} [CompleteLattice α] (P : Partition ⊥) (x : α) : x ∉ P

@[implicit_reducible]

instance Partition.instUniqueBot {α : Type u_1} [CompleteLattice α] : Unique (Partition ⊥)

There is a unique partition of ⊥.

Equations

• Partition.instUniqueBot = { default := Partition.removeBot ∅ ⋯ ⋯, uniq := ⋯ }

theorem Partition.ne_bot_of_mem' {α : Type u_1} {s x : α} [CompleteLattice α] {P : Partition s} (hxP : x ∈ P) : s ≠ ⊥

@[implicit_reducible]

instance Partition.instPartialOrder {α : Type u_1} {s : α} [CompleteLattice α] : PartialOrder (Partition s)

Partitions on s are ordered by refinement: P ≤ Q if every part of P is contained in a part of Q.

Equations

• Partition.instPartialOrder = { le := fun (P Q : Partition s) => ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem Partition.le_def {α : Type u_1} {s : α} [CompleteLattice α] {P Q : Partition s} : P ≤ Q ↔ ∀ x ∈ P, ∃ y ∈ Q, x ≤ y

theorem Partition.exists_le_of_mem_le {α : Type u_1} {s x : α} [CompleteLattice α] {P Q : Partition s} (h : P ≤ Q) (hx : x ∈ P) : ∃ y ∈ Q, x ≤ y

theorem Partition.existsUnique_of_mem_le {α : Type u_1} {s x : α} [CompleteLattice α] {P Q : Partition s} (h : P ≤ Q) (hx : x ∈ P) : ∃! y : α, y ∈ Q ∧ x ≤ y

@[implicit_reducible]

instance Partition.instOrderTop {α : Type u_1} {s : α} [CompleteLattice α] : OrderTop (Partition s)

The top partition of s is the partition with the single part s, or no parts if s is the bottom element.

Equations

• Partition.instOrderTop = { top := Partition.removeBot {s} ⋯ ⋯, le_top := ⋯ }

theorem Partition.top_def {α : Type u_1} {s : α} [CompleteLattice α] : ⊤ = removeBot {s} ⋯ ⋯

@[simp]

theorem Partition.parts_top {α : Type u_1} {s : α} [CompleteLattice α] (hs : s ≠ ⊥) : ↑⊤ = {s}

@[simp]

theorem Partition.mem_top_iff {α : Type u_1} {s : α} [CompleteLattice α] {a : α} : a ∈ ⊤ ↔ a = s ∧ a ≠ ⊥

theorem Partition.parts_top_subset {α : Type u_1} {s : α} [CompleteLattice α] : ↑⊤ ⊆ {s}

@[implicit_reducible]

instance Partition.instSemilatticeInf {α : Type u_2} [Order.Frame α] (s : α) : SemilatticeInf (Partition s)

When α is a frame, the meet P ⊓ Q of two partitions is the partition consisting of all non-bottom meets p ⊓ q for p ∈ P and q ∈ Q.

Note that while finite meets of partitions can be constructed in this way, arbitrary meets generally do not exist: for example when α is the frame of open subsets of the Cantor space, Partition α has no bottom element.

Equations

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

@[simp]

theorem Partition.mem_inf_iff {α : Type u_2} [Order.Frame α] {s a : α} {P Q : Partition s} : a ∈ P ⊓ Q ↔ a ≠ ⊥ ∧ ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q

@[simp]

theorem Partition.sUnion_eq {α : Type u_1} {s : Set α} (P : Partition s) : ⋃₀ ↑P = s

theorem Partition.nonempty_of_mem {α : Type u_1} {u t : Set α} {P : Partition u} (ht : t ∈ P) : t.Nonempty

theorem Partition.empty_notMem {α : Type u_1} {u : Set α} {P : Partition u} : ∅ ∉ P

theorem Partition.subset_of_mem {α : Type u_1} {u t : Set α} {P : Partition u} (ht : t ∈ P) : t ⊆ u

theorem Partition.mem_iff_exists {α : Type u_1} {x : α} {u : Set α} {P : Partition u} : x ∈ u ↔ ∃ t ∈ P, x ∈ t

theorem Partition.eq_of_mem_inter {α : Type u_1} {x : α} {u s t : Set α} {P : Partition u} (ht : t ∈ P) (hs : s ∈ P) (hx : x ∈ t ∩ s) : t = s

theorem Partition.eq_of_mem_of_mem {α : Type u_1} {x : α} {u s t : Set α} {P : Partition u} (ht : t ∈ P) (hus : s ∈ P) (hxt : x ∈ t) (hxs : x ∈ s) : t = s

theorem Partition.mem_iff_unique {α : Type u_1} {x : α} {u : Set α} {P : Partition u} : x ∈ u ↔ ∃! t : Set α, t ∈ P ∧ x ∈ t

theorem Partition.subset_sUnion_and_mem_iff_mem {α : Type u_1} {S : Set (Set α)} {u t : Set α} {P : Partition u} (hSP : S ⊆ ↑P) : t ⊆ ⋃₀ S ∧ t ∈ P ↔ t ∈ S

theorem Partition.subset_sUnion_iff_mem {α : Type u_1} {S : Set (Set α)} {u t : Set α} {P : Partition u} (ht : t ∈ P) (hSP : S ⊆ P.parts) : t ⊆ ⋃₀ S ↔ t ∈ S

noncomputable def Partition.rep {α : Type u_1} {u t : Set α} (P : Partition u) (ht : t ∈ P) : α

Noncomputably choose a representative from an equivalence class.

Equations

• P.rep ht = ⋯.some

@[simp]

theorem Partition.rep_mem {α : Type u_1} {u t : Set α} {P : Partition u} (ht : t ∈ P) : P.rep ht ∈ t

The representative of a part belongs to that part.

@[simp]

theorem Partition.rep_mem_supp {α : Type u_1} {u t : Set α} {P : Partition u} (ht : t ∈ P) : P.rep ht ∈ u

The representative of a part belongs to the underlying set.

Induced relation

def Partition.Rel {α : Type u_1} {s : Set α} (P : Partition s) (a b : α) : Prop

Every partition of s : Set α induces a transitive, symmetric binary relation on α whose equivalence classes are the parts of P. The relation is irreflexive outside s.

Equations

• P.Rel a b = ∃ t ∈ P, a ∈ t ∧ b ∈ t

theorem Partition.rel_le_iff_le {α : Type u_1} {u : Set α} {P Q : Partition u} : P.Rel ≤ Q.Rel ↔ P ≤ Q

theorem Partition.Rel.exists {α : Type u_1} {x y : α} {u : Set α} {P : Partition u} (h : P.Rel x y) : ∃ t ∈ P, x ∈ t ∧ y ∈ t

theorem Partition.Rel.forall {α : Type u_1} {x y : α} {u t : Set α} {P : Partition u} (h : P.Rel x y) (ht : t ∈ P) : x ∈ t ↔ y ∈ t

@[simp]

theorem Partition.rel_rfl_iff {α : Type u_1} {x : α} {u : Set α} {P : Partition u} : P.Rel x x ↔ x ∈ u

instance Partition.instSymmRel {α : Type u_1} {u : Set α} (P : Partition u) : Std.Symm P.Rel

instance Partition.instIsTransRel {α : Type u_1} {u : Set α} (P : Partition u) : IsTrans α P.Rel

theorem Partition.Rel.symm {α : Type u_1} {x y : α} {u : Set α} {P : Partition u} (h : P.Rel x y) : P.Rel y x

theorem Partition.rel_comm {α : Type u_1} {x y : α} {u : Set α} {P : Partition u} : P.Rel x y ↔ P.Rel y x

theorem Partition.Rel.trans {α : Type u_1} {x y z : α} {u : Set α} {P : Partition u} (hxy : P.Rel x y) (hyz : P.Rel y z) : P.Rel x z

theorem Partition.Rel.left_mem {α : Type u_1} {x y : α} {u : Set α} {P : Partition u} (h : P.Rel x y) : x ∈ u

theorem Partition.Rel.right_mem {α : Type u_1} {x y : α} {u : Set α} {P : Partition u} (h : P.Rel x y) : y ∈ u

theorem Partition.rep_rel {α : Type u_1} {x : α} {u t : Set α} {P : Partition u} (ht : t ∈ P) (hx : x ∈ t) : P.Rel x (P.rep ht)

Any element of a part is related to the representative of that part.

def Partition.partOf {α : Type u_1} {u : Set α} (P : Partition u) (a : α) : Set α

The part of a partition containing a given element. If the element is not in the underlying set, this is empty.

Equations

• P.partOf a = {b : α | P.Rel a b}

theorem Partition.partOf_subset {α : Type u_1} {x : α} {u : Set α} {P : Partition u} : P.partOf x ⊆ u

@[simp]

theorem Partition.mem_partOf_iff {α : Type u_1} {x y : α} {u : Set α} {P : Partition u} : x ∈ P.partOf y ↔ P.Rel y x

theorem Partition.eq_partOf_of_mem {α : Type u_1} {x : α} {u t : Set α} {P : Partition u} (ht : t ∈ P) (hxt : x ∈ t) : t = P.partOf x

theorem Partition.mem_iff_mem_partOf_mem {α : Type u_1} {x : α} {u : Set α} {P : Partition u} : x ∈ u ↔ x ∈ P.partOf x ∧ P.partOf x ∈ P

theorem Partition.mem_partOf {α : Type u_1} {x : α} {u : Set α} {P : Partition u} (hxu : x ∈ u) : x ∈ P.partOf x

theorem Partition.partOf_mem {α : Type u_1} {x : α} {u : Set α} {P : Partition u} (hxu : x ∈ u) : P.partOf x ∈ P

@[simp]

theorem Partition.partOf_rep {α : Type u_1} {u s : Set α} {P : Partition u} (hs : s ∈ P) : P.partOf (P.rep hs) = s

theorem Partition.mem_iff_exists_partOf {α : Type u_1} {u s : Set α} {P : Partition u} : s ∈ P ↔ ∃ x ∈ u, P.partOf x = s

theorem Partition.partOf_nonempty_iff {α : Type u_1} {x : α} {u : Set α} {P : Partition u} : (P.partOf x).Nonempty ↔ x ∈ u

@[simp]

theorem Partition.partOf_eq_empty_iff {α : Type u_1} {x : α} {u : Set α} {P : Partition u} : P.partOf x = ∅ ↔ x ∉ u

theorem Partition.rel_iff_partOf_eq_partOf_of_mem {α : Type u_1} {x y : α} {u : Set α} (P : Partition u) (hx : x ∈ u) (hy : y ∈ u) : P.Rel x y ↔ P.partOf x = P.partOf y

theorem Partition.rel_iff_partOf_eq_partOf {α : Type u_1} {x y : α} {u : Set α} (P : Partition u) : P.Rel x y ↔ ∃ (_ : x ∈ u) (_ : y ∈ u), P.partOf x = P.partOf y

Representative functions

See the module docstring for motivation (graph simplification, minors, and why we use an explicit IsRepFun hypothesis rather than a global choice of representatives).

structure Partition.IsRepFun {α : Type u_1} {u : Set α} (P : Partition u) (f : α → α) : Prop

A predicate characterizing when a function f : α → α is a representative function for a partition P. A representative function maps each element to a canonical representative in its equivalence class, is the identity outside the support, and maps related elements to the same representative.

• apply_of_notMem ⦃a : α⦄ : a ∉ u → f a = a

  The function is the identity outside the support.

• rel_apply ⦃a : α⦄ : a ∈ u → P.Rel a (f a)

  The function maps each element in the support to a related element.

• apply_eq_apply ⦃a b : α⦄ : P.Rel a b → f a = f b

  The function maps related elements to the same representative.

theorem Partition.IsRepFun.apply_mem {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α} {a : α} (hf : P.IsRepFun f) (ha : a ∈ u) : f a ∈ u

theorem Partition.IsRepFun.image_subset {α : Type u_1} {s u : Set α} {P : Partition u} {f : α → α} (hf : P.IsRepFun f) (hs : u ⊆ s) : f '' s ⊆ s

theorem Partition.IsRepFun.mapsTo {α : Type u_1} {s u : Set α} {P : Partition u} {f : α → α} (hf : P.IsRepFun f) (hs : u ⊆ s) : Set.MapsTo f s s

theorem Partition.IsRepFun.mapsTo_of_disjoint {α : Type u_1} {s u : Set α} {P : Partition u} {f : α → α} (hf : P.IsRepFun f) (hs : Disjoint u s) : Set.MapsTo f s s

theorem Partition.IsRepFun.apply_mem_iff {α : Type u_1} {s u : Set α} {P : Partition u} {f : α → α} {a : α} (hf : P.IsRepFun f) (hs : u ⊆ s) : f a ∈ s ↔ a ∈ s

theorem Partition.IsRepFun.apply_eq_apply_iff_rel {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α} {a b : α} (hf : P.IsRepFun f) (ha : a ∈ u) : f a = f b ↔ P.Rel a b

theorem Partition.IsRepFun.apply_eq_apply_iff {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α} {a b : α} (hf : P.IsRepFun f) : f a = f b ↔ a = b ∨ P.Rel a b

theorem Partition.IsRepFun.forall_apply_eq_apply_iff {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α} (hf : P.IsRepFun f) (a : α) : (∀ (x : α), f a = f x ↔ a = x) ∨ ∀ (x : α), f a = f x ↔ P.Rel a x

theorem Partition.IsRepFun.apply_eq_apply_iff' {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α} {a b : α} (hf : P.IsRepFun f) : f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel a b

theorem Partition.IsRepFun.idem {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α} {a : α} (hf : P.IsRepFun f) : f (f a) = f a

theorem Partition.IsRepFun.apply_apply {α : Type u_1} {u : Set α} {P : Partition u} {f g : α → α} (hf : P.IsRepFun f) (hg : P.IsRepFun g) (x : α) : f (g x) = f x

theorem Partition.IsRepFun.exists_extend_partial {α : Type u_1} {t u : Set α} (P : Partition u) (f₀ : ↑t → α) (h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x) (h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)) (h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y) : ∃ (f : α → α), P.IsRepFun f ∧ ∀ (x : ↑t), f ↑x = f₀ x

Any partially defined representative function extends to a complete one.

theorem Partition.IsRepFun.exists_extend_partial' {α : Type u_1} {t u : Set α} (P : Partition u) (h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y) : ∃ (f : α → α), P.IsRepFun f ∧ Set.EqOn f id t

For any set t containing no two distinct related elements, there is a representative function equal to the identity on t.

theorem Partition.IsRepFun.nonempty {α : Type u_1} {u : Set α} (P : Partition u) : ∃ (f : α → α), P.IsRepFun f

Every partition has a representative function.