Complete bipartite graphs
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Vojtěch Štěpančík and Victor Blanchi.
Created on 2022-07-03.
Last modified on 2024-03-23.
module graph-theory.complete-bipartite-graphs where
Imports
open import foundation.coproduct-types open import foundation.universe-levels open import foundation.unordered-pairs open import graph-theory.finite-graphs open import univalent-combinatorics.2-element-types open import univalent-combinatorics.cartesian-product-types open import univalent-combinatorics.coproduct-types open import univalent-combinatorics.dependent-pair-types open import univalent-combinatorics.fibers-of-maps open import univalent-combinatorics.finite-types
Idea
Consider two finite sets X
and Y
.
The
complete bipartite graph¶
on X
and Y
is the undirected finite graph
consisting of:
-
The finite set of vertices is the coproduct type
X + Y
. -
Given an unordered pair
f : I → X + Y
of vertices, the finite type of edges on the unordered pair(I , f)
is given by(Σ (x : X), fiber f (inl x)) × (Σ (y : Y), fiber f (inr y)).
In other words, an unordered pair of elements of the coproduct type
X + Y
is an edge in the complete bipartite graph onX
andY
precisely when one of the elements of the unordered pair comes fromX
and the other comes fromY
.
Definition
module _ {l1 l2 : Level} (X : 𝔽 l1) (Y : 𝔽 l2) where vertex-finite-type-complete-bipartite-Undirected-Graph-𝔽 : 𝔽 (l1 ⊔ l2) vertex-finite-type-complete-bipartite-Undirected-Graph-𝔽 = coproduct-𝔽 X Y vertex-complete-bipartite-Undirected-Graph-𝔽 : UU (l1 ⊔ l2) vertex-complete-bipartite-Undirected-Graph-𝔽 = type-𝔽 vertex-finite-type-complete-bipartite-Undirected-Graph-𝔽 unordered-pair-vertices-complete-bipartite-Undirected-Graph-𝔽 : UU (lsuc lzero ⊔ l1 ⊔ l2) unordered-pair-vertices-complete-bipartite-Undirected-Graph-𝔽 = unordered-pair vertex-complete-bipartite-Undirected-Graph-𝔽 edge-finite-type-complete-bipartite-Undirected-Graph-𝔽 : unordered-pair-vertices-complete-bipartite-Undirected-Graph-𝔽 → 𝔽 (l1 ⊔ l2) edge-finite-type-complete-bipartite-Undirected-Graph-𝔽 p = product-𝔽 ( Σ-𝔽 X ( λ x → fiber-𝔽 ( finite-type-2-Element-Type (pr1 p)) ( coproduct-𝔽 X Y) ( element-unordered-pair p) ( inl x))) ( Σ-𝔽 Y ( λ y → fiber-𝔽 ( finite-type-2-Element-Type (pr1 p)) ( coproduct-𝔽 X Y) ( element-unordered-pair p) ( inr y))) edge-complete-bipartite-Undirected-Graph : unordered-pair-vertices-complete-bipartite-Undirected-Graph-𝔽 → UU (l1 ⊔ l2) edge-complete-bipartite-Undirected-Graph p = type-𝔽 (edge-finite-type-complete-bipartite-Undirected-Graph-𝔽 p) complete-bipartite-Undirected-Graph-𝔽 : Undirected-Graph-𝔽 (l1 ⊔ l2) (l1 ⊔ l2) pr1 complete-bipartite-Undirected-Graph-𝔽 = vertex-finite-type-complete-bipartite-Undirected-Graph-𝔽 pr2 complete-bipartite-Undirected-Graph-𝔽 = edge-finite-type-complete-bipartite-Undirected-Graph-𝔽
External links
- Complete bipartite graph at Mathswitch
- Complete bipartite graph at D3 Graph Theory
- Bipartite graphs at Lab
- Complete bipartite graph at Wikidata
- Complete bipartite graph at Wikipedia
- Complete bipartite graphs at Wolfram Mathworld
Recent changes
- 2024-03-23. Vojtěch Štěpančík. Enhancements for the Concepts macro (#1093).
- 2024-02-06. Fredrik Bakke. Rename
(co)prod
to(co)product
(#1017). - 2023-11-28. Egbert Rijke and Vojtěch Štěpančík. Adding concept tags to three files (#952).
- 2023-11-09. Fredrik Bakke. Typeset
nlab
as$n$Lab
(#911). - 2023-10-13. Egbert Rijke. Fix links to wikidata to the recommended links; add concept tags at end of file for testing purposes (#837).