Complete multipartite graphs
Content created by Egbert Rijke, Jonathan Prieto-Cubides, Fredrik Bakke and Vojtěch Štěpančík.
Created on 2022-07-02.
Last modified on 2024-03-23.
module graph-theory.complete-multipartite-graphs where
Imports
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.dependent-function-types open import univalent-combinatorics.dependent-pair-types open import univalent-combinatorics.equality-finite-types open import univalent-combinatorics.finite-types open import univalent-combinatorics.function-types
Idea
Consider a family of finite types Y
indexed by a finite type X
. The
complete multipartite graph¶
at Y
is the finite undirected graph
consisting of:
- The finite type of vertices is the
dependent pair type
Σ (x : X), Y x
. - An unordered pair
f : I → Σ (x : X), Y x
is an edge if the induced unordered pairpr1 ∘ f : I → X
is an embedding.
Note: The formalization of the finite type of edges below is different from the above description, and needs to be changed.
Definitions
Complete multipartite graphs
module _ {l1 l2 : Level} (X : 𝔽 l1) (Y : type-𝔽 X → 𝔽 l2) where vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽 : 𝔽 (l1 ⊔ l2) vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽 = Σ-𝔽 X Y vertex-complete-multipartite-Undirected-Graph-𝔽 : UU (l1 ⊔ l2) vertex-complete-multipartite-Undirected-Graph-𝔽 = type-𝔽 vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽 unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 : UU (lsuc lzero ⊔ l1 ⊔ l2) unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 = unordered-pair vertex-complete-multipartite-Undirected-Graph-𝔽 edge-finite-type-complete-multipartite-Undirected-Graph-𝔽 : unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 → 𝔽 l1 edge-finite-type-complete-multipartite-Undirected-Graph-𝔽 p = ( Π-𝔽 ( finite-type-2-Element-Type (pr1 p)) ( λ x → Π-𝔽 ( finite-type-2-Element-Type (pr1 p)) ( λ y → Id-𝔽 X ( pr1 (element-unordered-pair p x)) ( pr1 (element-unordered-pair p y))))) →-𝔽 ( empty-𝔽) edge-complete-multipartite-Undirected-Graph-𝔽 : unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 → UU l1 edge-complete-multipartite-Undirected-Graph-𝔽 p = type-𝔽 (edge-finite-type-complete-multipartite-Undirected-Graph-𝔽 p) complete-multipartite-Undirected-Graph-𝔽 : Undirected-Graph-𝔽 (l1 ⊔ l2) l1 pr1 complete-multipartite-Undirected-Graph-𝔽 = vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽 pr2 complete-multipartite-Undirected-Graph-𝔽 = edge-finite-type-complete-multipartite-Undirected-Graph-𝔽
External links
- Multipartite graph at Mathswitch
- Multipartite graph on Wikidata
- Multipartite graph on Wikipedia
- Complete multipartite graph on Wolfram Mathworld
Recent changes
- 2024-03-23. Vojtěch Štěpančík. Enhancements for the Concepts macro (#1093).
- 2023-11-28. Egbert Rijke and Vojtěch Štěpančík. Adding concept tags to three files (#952).
- 2023-10-13. Egbert Rijke. Fix links to wikidata to the recommended links; add concept tags at end of file for testing purposes (#837).
- 2023-10-12. Egbert Rijke. Creating internal and external links in Graph Theory (#832).
- 2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).