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 set 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))