# Acyclic undirected graphs

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

Created on 2023-05-03.

module graph-theory.acyclic-undirected-graphs where

Imports
open import foundation.universe-levels

open import graph-theory.geometric-realizations-undirected-graphs
open import graph-theory.reflecting-maps-undirected-graphs
open import graph-theory.undirected-graphs


## Idea

An acyclic undirected graph is an undirected graph of which the geometric realization is contractible.

The notion of acyclic graphs is a generalization of the notion of undirected trees. Note that in this library, an undirected tree is an undirected graph in which the type of trails between any two points is contractible. The type of nodes of such undirected trees consequently has decidable equality. On the other hand, there are acyclic undirected graphs that are not undirected trees in this sense. One way to obtain them is via acyclic types, which are types of which the suspension is contractible. The undirected suspension diagram of such types is an acyclic graph. Furthermore, any directed tree induces an acyclic undirected graph by forgetting the directions of the edges.

## Definition

### Acyclic undirected graphs

The following is a preliminary definition that requires us to parametrize over an extra universe level. This will not be necessary anymore if we constructed a geometric realization of every undirected graph. Once we did that, we would simply say that the geometric realization of G is contractible.

is-acyclic-Undirected-Graph :
{l1 l2 : Level} (l : Level) (G : Undirected-Graph l1 l2) →
UU (l1 ⊔ l2 ⊔ lsuc l)
is-acyclic-Undirected-Graph l G =
is-geometric-realization-reflecting-map-Undirected-Graph l G
( terminal-reflecting-map-Undirected-Graph G)


ConceptFile
Acyclic mapssynthetic-homotopy-theory.acyclic-maps
Acyclic typessynthetic-homotopy-theory.acyclic-types
Acyclic undirected graphsgraph-theory.acyclic-undirected-graphs
Braceletsunivalent-combinatorics.bracelets
The category of cyclic ringsring-theory.category-of-cyclic-rings
The circlesynthetic-homotopy-theory.circle
Connected set bundles over the circlesynthetic-homotopy-theory.connected-set-bundles-circle
Cyclic finite typesunivalent-combinatorics.cyclic-finite-types
Cyclic groupsgroup-theory.cyclic-groups
Cyclic higher groupshigher-group-theory.cyclic-higher-groups
Cyclic ringsring-theory.cyclic-rings
Cyclic typesstructured-types.cyclic-types
Euler's totient functionelementary-number-theory.eulers-totient-function
Finitely cyclic mapselementary-number-theory.finitely-cyclic-maps
Generating elements of groupsgroup-theory.generating-elements-groups
Hatcher's acyclic typesynthetic-homotopy-theory.hatchers-acyclic-type
Homomorphisms of cyclic ringsring-theory.homomorphisms-cyclic-rings
Infinite cyclic typessynthetic-homotopy-theory.infinite-cyclic-types
Multiplicative units in the standard cyclic ringselementary-number-theory.multiplicative-units-standard-cyclic-rings
Necklacesunivalent-combinatorics.necklaces
Polygonsgraph-theory.polygons
The poset of cyclic ringsring-theory.poset-of-cyclic-rings
Standard cyclic groups (ℤ/k)elementary-number-theory.standard-cyclic-groups
Standard cyclic rings (ℤ/k)elementary-number-theory.standard-cyclic-rings