Acyclic undirected graphs

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

Created on 2023-05-03.
Last modified on 2024-03-23.

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)

See also

Concept	File
Acyclic maps	`synthetic-homotopy-theory.acyclic-maps`
Acyclic types	`synthetic-homotopy-theory.acyclic-types`
Acyclic undirected graphs	`graph-theory.acyclic-undirected-graphs`
Bracelets	`univalent-combinatorics.bracelets`
The category of cyclic rings	`ring-theory.category-of-cyclic-rings`
The circle	`synthetic-homotopy-theory.circle`
Connected set bundles over the circle	`synthetic-homotopy-theory.connected-set-bundles-circle`
Cyclic finite types	`univalent-combinatorics.cyclic-finite-types`
Cyclic groups	`group-theory.cyclic-groups`
Cyclic higher groups	`higher-group-theory.cyclic-higher-groups`
Cyclic rings	`ring-theory.cyclic-rings`
Cyclic types	`structured-types.cyclic-types`
Euler's totient function	`elementary-number-theory.eulers-totient-function`
Finitely cyclic maps	`elementary-number-theory.finitely-cyclic-maps`
Generating elements of groups	`group-theory.generating-elements-groups`
Hatcher's acyclic type	`synthetic-homotopy-theory.hatchers-acyclic-type`
Homomorphisms of cyclic rings	`ring-theory.homomorphisms-cyclic-rings`
Infinite cyclic types	`synthetic-homotopy-theory.infinite-cyclic-types`
Multiplicative units in the standard cyclic rings	`elementary-number-theory.multiplicative-units-standard-cyclic-rings`
Necklaces	`univalent-combinatorics.necklaces`
Polygons	`graph-theory.polygons`
The poset of cyclic rings	`ring-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`

External links

Acyclic graph at Mathswitch
Trees at $n$ Lab
Forests at Wikipedia
Acyclic graphs at Wolfram Mathworld.

Recent changes

2024-03-23. Vojtěch Štěpančík. Enhancements for the Concepts macro (#1093).
2024-01-28. Egbert Rijke. Span diagrams (#1007).
2023-11-09. Fredrik Bakke. Typeset nlab as $n$Lab (#911).
2023-11-02. Vojtěch Štěpančík. Add a mdbook #concept macro (#884).
2023-10-13. Egbert Rijke. Fix links to wikidata to the recommended links; add concept tags at end of file for testing purposes (#837).