Complete multipartite graphs

Content created by Egbert Rijke, Jonathan Prieto-Cubides, Fredrik Bakke and Vojtěch Štěpančík.

Created on 2022-07-02.
Last modified on 2024-10-16.

module graph-theory.complete-multipartite-graphs where
Imports 
open import foundation.universe-levels
open import foundation.unordered-pairs

open import graph-theory.finite-graphs

open import univalent-combinatorics.2-element-types
open import univalent-combinatorics.dependent-function-types
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.function-types

Idea

Consider a family of finite types Y indexed by a finite type X. The complete multipartite graph at Y is the finite undirected graph consisting of:

Note: The formalization of the finite type of edges below is different from the above description, and needs to be changed.

Definitions

Complete multipartite graphs

module _
  {l1 l2 : Level} (X : 𝔽 l1) (Y : type-𝔽 X → 𝔽 l2)
  where

  vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽 : 𝔽 (l1 ⊔ l2)
  vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽 =
    Σ-𝔽 X Y

  vertex-complete-multipartite-Undirected-Graph-𝔽 : UU (l1 ⊔ l2)
  vertex-complete-multipartite-Undirected-Graph-𝔽 =
    type-𝔽 vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽

  unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 :
    UU (lsuc lzero ⊔ l1 ⊔ l2)
  unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 =
    unordered-pair vertex-complete-multipartite-Undirected-Graph-𝔽

  edge-finite-type-complete-multipartite-Undirected-Graph-𝔽 :
    unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 → 𝔽 l1
  edge-finite-type-complete-multipartite-Undirected-Graph-𝔽 p =
    ( Π-𝔽
      ( finite-type-2-Element-Type (pr1 p))
      ( λ x →
        Π-𝔽
          ( finite-type-2-Element-Type (pr1 p))
          ( λ y →
            Id-𝔽 X
              ( pr1 (element-unordered-pair p x))
              ( pr1 (element-unordered-pair p y))))) →-𝔽
    ( empty-𝔽)

  edge-complete-multipartite-Undirected-Graph-𝔽 :
    unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 → UU l1
  edge-complete-multipartite-Undirected-Graph-𝔽 p =
    type-𝔽 (edge-finite-type-complete-multipartite-Undirected-Graph-𝔽 p)

  complete-multipartite-Undirected-Graph-𝔽 : Undirected-Graph-𝔽 (l1 ⊔ l2) l1
  pr1 complete-multipartite-Undirected-Graph-𝔽 =
    vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽
  pr2 complete-multipartite-Undirected-Graph-𝔽 =
    edge-finite-type-complete-multipartite-Undirected-Graph-𝔽

Recent changes