This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Matchings

module graph-theory.matchings where
Imports 
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.unit-type
open import foundation.universe-levels
open import foundation.unordered-pairs

open import graph-theory.undirected-graphs

open import univalent-combinatorics.standard-finite-types

Idea

A matching in a undirected graph is a type of edges without common vertices.

Definitions

module _
  {l1 l2 : Level}
  where

  selected-edges-vertex-Undirected-Graph :
    ( G : Undirected-Graph l1 l2) →
    ( (p : unordered-pair-vertices-Undirected-Graph G) →
      edge-Undirected-Graph G p → Fin 2) →
    vertex-Undirected-Graph G → UU (l1 ⊔ l2)
  selected-edges-vertex-Undirected-Graph G c x =
    Σ ( vertex-Undirected-Graph G)
      ( λ y →
        Σ ( edge-Undirected-Graph G (standard-unordered-pair x y))
          ( λ e → Id (c (standard-unordered-pair x y) e) (inr star)))

  matching : Undirected-Graph l1 l2 → UU (lsuc lzero ⊔ l1 ⊔ l2)
  matching G =
    Σ ( (p : unordered-pair-vertices-Undirected-Graph G) →
        edge-Undirected-Graph G p → Fin 2)
      ( λ c →
        ( x : vertex-Undirected-Graph G) →
        is-prop (selected-edges-vertex-Undirected-Graph G c x))

  perfect-matching : Undirected-Graph l1 l2 → UU (lsuc lzero ⊔ l1 ⊔ l2)
  perfect-matching G =
    Σ ( (p : unordered-pair-vertices-Undirected-Graph G) →
        edge-Undirected-Graph G p → Fin 2)
      ( λ c →
        ( x : vertex-Undirected-Graph G) →
          is-contr (selected-edges-vertex-Undirected-Graph G c x))