Lax Lean Archive

Partitions, transversals and the partition into atomic types

Lax185574.Partitions · concepts/Lax185574/Partitions.lean · lax-185574

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    For two partitions 𝒫, 𝒬 of the same set, 𝒫 ≼ 𝒬 says that 𝒫 refines 𝒬, that is, each part of 𝒫 is contained in some part of 𝒬. For a partition 𝒫 of V and X ⊆ V, X/𝒫 is the set of parts of 𝒫 that meet X. The part of 𝒫 containing an element v is 𝒫(v). Further, ≡_𝒫 is the equivalence relation on V whose classes are the parts of 𝒫. A transversal of 𝒫 is a set that contains exactly one vertex of every part.

    For a graph G and S ⊆ V(G), two vertices u, v have the same atomic type over S if and only if either u = v, or u, v ∉ S and N(u) ∩ S = N(v) ∩ S. The partition into atomic types 𝒫_S partitions S into singletons and the vertices of V(G) ∖ S according to their neighborhoods in S.

    Concept map
    6 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    In the paper

    • page 12 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.Encodings
    2import Mathlib.Data.Setoid.Basic
    3import Mathlib.Data.Set.Card
    4import Mathlib.Data.Fintype.Basic
    5
    6/-!
    7---
    8title: Partitions, transversals and the partition into atomic types
    9type: definition
    10---
    11For two partitions 𝒫, 𝒬 of the same set, 𝒫 ≼ 𝒬 says that 𝒫 refines 𝒬,
    12that is, each part of 𝒫 is contained in some part of 𝒬. For a partition
    13𝒫 of V and X ⊆ V, X/𝒫 is the set of parts of 𝒫 that meet X. The part of
    14𝒫 containing an element v is 𝒫(v). Further, ≡_𝒫 is the equivalence
    15relation on V whose classes are the parts of 𝒫. A *transversal* of 𝒫 is
    16a set that contains exactly one vertex of every part.
    17
    18For a graph G and S ⊆ V(G), two vertices u, v have the same atomic type
    19over S if and only if either u = v, or u, v ∉ S and N(u) ∩ S = N(v) ∩ S.
    20The *partition into atomic types* 𝒫_S partitions S into singletons and
    21the vertices of V(G) ∖ S according to their neighborhoods in S.
    22
    23# Formalization notes
    24
    25A partition of V is an equivalence relation on V, a `Setoid V`. Its
    26parts are the equivalence classes, so ≡_𝒫 is the relation itself and
    27𝒫 ≼ 𝒬 is the order `P ≤ Q` of setoids. The partition into singletons is
    28`⊥`, and the partition with one part is `⊤`. The number |X/𝒫| is the
    29number of classes of elements of X, `partCount`. It is the exact count
    30on a finite vertex type, which is the case in every statement that uses
    31it.
    32
    33The partition into atomic types is the kernel of the map
    34v ↦ (S ∩ {v}, S ∩ N(v)). Two vertices have the same image exactly when
    35they are equal, or both lie outside S and have the same neighborhood in
    36S. So this is the partition of the paper. It is also the partition
    37into types of quantifier rank 0 over S in the sense of
    38`Lax185574.FirstOrderTypes`, which the paper mentions as the definition.
    39
    40Algorithms exchange partitions of `Fin n` as the finite set of their
    41parts, each part a finite set of vertices, in the encodings of
    42`Lax185574.Encodings`. This is the instance below.
    43-/
    44
    45namespace Lax185574.Partitions
    46
    47open Lax185574.Encoding
    48
    49universe z
    50
    51variable {V : Type z}
    52
    53/-- `|X/𝒫|`: the number of parts of `P` that meet `X`. -/
    54noncomputable def partCount (P : Setoid V) (X : Set V) : ℕ :=
    55 (Quotient.mk P '' X).ncard
    56
    57/-- The part `𝒫(v)` of `P` that contains `v`. -/
    58def part (P : Setoid V) (v : V) : Set V := {u | P u v}
    59
    60/-- `T` is a transversal of `P`: every part of `P` contains exactly one
    61vertex of `T`. -/
    62def IsTransversal (P : Setoid V) (T : Set V) : Prop :=
    63 ∀ v : V, ∃! t : V, t ∈ T ∧ P t v
    64
    65/-- The partition `𝒫_S` into atomic types over `S`: vertices of `S` are
    66singletons, and vertices outside `S` are grouped by their neighborhood
    67in `S`. -/
    68def atomicTypes (G : SimpleGraph V) (S : Set V) : Setoid V :=
    69 Setoid.ker fun v => (S ∩ {v}, S ∩ G.neighborSet v)
    70
    71/-- The parts of a partition of `Fin n`, as a finite set of finite
    72sets. -/
    73noncomputable def parts {n : ℕ} (P : Setoid (Fin n)) : Finset (Finset (Fin n)) :=
    74 open Classical in Finset.univ.image fun v => Finset.univ.filter fun u => P u v
    75
    76/-- A partition of `Fin n` is encoded by the finite set of its parts.
    77A setoid is a relation, so the encoding is not derived. -/
    78noncomputable instance {n : ℕ} : Encode (Setoid (Fin n)) where
    79 encode P := encode (parts P)
    80
    81end Lax185574.Partitions
    82
    Formalization notes

    A partition of V is an equivalence relation on V, a SetoidVSetoid V. Its parts are the equivalence classes, so ≡_𝒫 is the relation itself and 𝒫 ≼ 𝒬 is the order P≤QP ≤ Q of setoids. The partition into singletons is ⊥⊥, and the partition with one part is ⊤⊤. The number |X/𝒫| is the number of classes of elements of X, partCountpartCount. It is the exact count on a finite vertex type, which is the case in every statement that uses it.

    The partition into atomic types is the kernel of the map v ↦ (S ∩ {v}, S ∩ N(v)). Two vertices have the same image exactly when they are equal, or both lie outside S and have the same neighborhood in S. So this is the partition of the paper. It is also the partition into types of quantifier rank 0 over S in the sense of Lax185574.FirstOrderTypesLax185574.FirstOrderTypes, which the paper mentions as the definition.

    Algorithms exchange partitions of FinnFin n as the finite set of their parts, each part a finite set of vertices, in the encodings of Lax185574.EncodingsLax185574.Encodings. This is the instance below.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…