From e39b3bccb414f1becbc3abfbfdb220080afc5867 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Wed, 11 Oct 2023 10:29:42 +0200 Subject: [PATCH] Adding external link sections --- .../acyclic-undirected-graphs.lagda.md | 37 +++++++++++++------ .../circuits-undirected-graphs.lagda.md | 18 +++++++-- .../closed-walks-undirected-graphs.lagda.md | 15 +++++++- .../complete-bipartite-graphs.lagda.md | 13 +++++++ 4 files changed, 66 insertions(+), 17 deletions(-) diff --git a/src/graph-theory/acyclic-undirected-graphs.lagda.md b/src/graph-theory/acyclic-undirected-graphs.lagda.md index caca26aa95..cc3f8d690a 100644 --- a/src/graph-theory/acyclic-undirected-graphs.lagda.md +++ b/src/graph-theory/acyclic-undirected-graphs.lagda.md @@ -18,21 +18,24 @@ open import graph-theory.undirected-graphs ## Idea -An **acyclic** undirected graph is an undirected graph of which the geometric -realization is contractible. +An **acyclic** undirected graph is an +[undirected graph](graph-theory.undirected-graphs.md) of which the +[geometric realization](graph-theory.geometric-realizations-undirected-graphs.md) +is [contractible](foundation-core.contractible-types.md). The notion of acyclic graphs is a generalization of the notion of [undirected trees](trees.undirected-trees.md). 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](synthetic-homotopy-theory.acyclic-types.md), which -are types of which the -[suspension](synthetic-homotopy-theory.suspensions-of-types.md) is contractible. -The undirected suspension diagram of such types is an acyclic graph. -Furthermore, any [directed tree](trees.directed-trees.md) induces an acyclic -undirected graph by forgetting the directions of the edges. +undirected tree is an undirected graph in which the type of +[trails](graph-theory.trails-undirected-graphs.md) between any two points is +contractible. The type of nodes of such undirected trees consequently has +[decidable equality](foundation.decidable-equality.md). 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](synthetic-homotopy-theory.acyclic-types.md), which are types of +which the [suspension](synthetic-homotopy-theory.suspensions-of-types.md) is +contractible. The undirected suspension diagram of such types is an acyclic +graph. Furthermore, any [directed tree](trees.directed-trees.md) induces an +acyclic undirected graph by forgetting the directions of the edges. ## Definition @@ -57,3 +60,13 @@ is-acyclic-Undirected-Graph l G = ### Table of files related to cyclic types, groups, and rings {{#include tables/cyclic-types.md}} + +## External links + +- Acyclic + undirected graphs at the Math Grand Exchange. +- Trees at the nlab. +- Forests + at Wikipedia +- Acyclic graphs + at Wolfram Mathworld. diff --git a/src/graph-theory/circuits-undirected-graphs.lagda.md b/src/graph-theory/circuits-undirected-graphs.lagda.md index 98a01db985..a5b029d0df 100644 --- a/src/graph-theory/circuits-undirected-graphs.lagda.md +++ b/src/graph-theory/circuits-undirected-graphs.lagda.md @@ -21,9 +21,12 @@ open import graph-theory.undirected-graphs ## Idea -A circuit in an undirected graph `G` consists of a `k`-gon `H` equipped with a -totally faithful morphism of graphs from `H` to `G`. In other words, a circuit -is a closed walk with no repeated edges. +A **circuit** in an [undirected graph](graph-theory.undirected-graphs.md) `G` +consists of a [`k`-gon](graph-theory.polygons.md) `H` equipped with a +[totally faithful](graph-theory.totally-faithful-morphisms-undirected-graphs.md) +[morphism](graph-theory.morphisms-undirected-graphs.md) of undirected graphs +from `H` to `G`. In other words, a circuit is a closed walk with no repeated +edges. ## Definition @@ -38,3 +41,12 @@ module _ ( λ H → totally-faithful-hom-Undirected-Graph (undirected-graph-Polygon k H) G) ``` + +## External links + +- Cycle + at Math Grand Exchange +- Cycle (Graph + Theory) at Wikipedia +- Graph Cycle at + Wolfram Mathworld diff --git a/src/graph-theory/closed-walks-undirected-graphs.lagda.md b/src/graph-theory/closed-walks-undirected-graphs.lagda.md index d804af430c..fad4ba73ac 100644 --- a/src/graph-theory/closed-walks-undirected-graphs.lagda.md +++ b/src/graph-theory/closed-walks-undirected-graphs.lagda.md @@ -21,8 +21,10 @@ open import graph-theory.undirected-graphs ## Idea -A closed walk of length `k : ℕ` in an undirected graph `G` is a morphism of -graphs from a `k`-gon into `G`. +A **closed walk** of length `k : ℕ` in an +[undirected graph](graph-theory.undirected-graphs.md) `G` is a +[morphism](graph-theory.morphisms-undirected-graphs.md) of graphs from a +[`k`-gon](graph-theory.polygons.md) into `G`. ## Definition @@ -35,3 +37,12 @@ module _ closed-walk-Undirected-Graph = Σ (Polygon k) (λ H → hom-Undirected-Graph (undirected-graph-Polygon k H) G) ``` + +## External links + +- Cycle + at Math Grand Exchange +- Cycle (Graph + Theory) at Wikipedia +- Graph Cycle at + Wolfram Mathworld diff --git a/src/graph-theory/complete-bipartite-graphs.lagda.md b/src/graph-theory/complete-bipartite-graphs.lagda.md index 4c513cb1ab..a1ab3edefd 100644 --- a/src/graph-theory/complete-bipartite-graphs.lagda.md +++ b/src/graph-theory/complete-bipartite-graphs.lagda.md @@ -46,3 +46,16 @@ pr2 (complete-bipartite-Undirected-Graph-𝔽 X Y) p = ( element-unordered-pair p) ( inr y))) ``` + +## External links + +- Complete bipartite + graphs at D3 Graph Theory +- Complete + bipartite graphs at Math Grand Exchange +- Bipartite graphs + at nlab +- Complete + bipartite graphs at Wikipedia +- Complete + bipartite graphs at Wolfram Mathworld