Polygons

Content created by Egbert Rijke, Jonathan Prieto-Cubides, Fredrik Bakke and Elisabeth Stenholm.

Created on 2022-02-10.

module graph-theory.polygons where

Imports
open import elementary-number-theory.modular-arithmetic
open import elementary-number-theory.natural-numbers

open import foundation.decidable-equality
open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.functoriality-propositional-truncation
open import foundation.mere-equivalences
open import foundation.sets
open import foundation.universe-levels
open import foundation.unordered-pairs

open import graph-theory.equivalences-undirected-graphs
open import graph-theory.mere-equivalences-undirected-graphs
open import graph-theory.undirected-graphs

open import univalent-combinatorics.finite-types


Idea

A polygon is an undirected graph that is merely equivalent to a graph with vertices the underlying type of the standard cyclic group ℤ-Mod k and an edge from each x ∈ ℤ-Mod k to x+1. This defines for each k ∈ ℕ the type of all k-gons. The type of all k-gons is a concrete presentation of the dihedral group D_k.

Definition

Standard polygons

vertex-standard-polygon-Undirected-Graph : ℕ → UU lzero
vertex-standard-polygon-Undirected-Graph k = ℤ-Mod k

unordered-pair-vertices-standard-polygon-Undirected-Graph : ℕ → UU (lsuc lzero)
unordered-pair-vertices-standard-polygon-Undirected-Graph k =
unordered-pair (vertex-standard-polygon-Undirected-Graph k)

edge-standard-polygon-Undirected-Graph :
(k : ℕ) →
unordered-pair-vertices-standard-polygon-Undirected-Graph k → UU lzero
edge-standard-polygon-Undirected-Graph k p =
Σ ( type-unordered-pair p)
( λ x →
fiber
( element-unordered-pair p)
( succ-ℤ-Mod k (element-unordered-pair p x)))

standard-polygon-Undirected-Graph : ℕ → Undirected-Graph lzero lzero
pr1 (standard-polygon-Undirected-Graph k) =
vertex-standard-polygon-Undirected-Graph k
pr2 (standard-polygon-Undirected-Graph k) =
edge-standard-polygon-Undirected-Graph k


The type of all polygons with k vertices

Polygon : ℕ → UU (lsuc lzero)
Polygon k =
Σ ( Undirected-Graph lzero lzero)
( mere-equiv-Undirected-Graph (standard-polygon-Undirected-Graph k))

module _
(k : ℕ) (X : Polygon k)
where

undirected-graph-Polygon : Undirected-Graph lzero lzero
undirected-graph-Polygon = pr1 X

mere-equiv-Polygon :
mere-equiv-Undirected-Graph
( standard-polygon-Undirected-Graph k)
( undirected-graph-Polygon)
mere-equiv-Polygon = pr2 X

vertex-Polygon : UU lzero
vertex-Polygon = vertex-Undirected-Graph undirected-graph-Polygon

unordered-pair-vertices-Polygon : UU (lsuc lzero)
unordered-pair-vertices-Polygon = unordered-pair vertex-Polygon

edge-Polygon : unordered-pair-vertices-Polygon → UU lzero
edge-Polygon = edge-Undirected-Graph undirected-graph-Polygon

mere-equiv-vertex-Polygon : mere-equiv (ℤ-Mod k) vertex-Polygon
mere-equiv-vertex-Polygon =
map-trunc-Prop
( equiv-vertex-equiv-Undirected-Graph
( standard-polygon-Undirected-Graph k)
( undirected-graph-Polygon))
( mere-equiv-Polygon)

is-finite-vertex-Polygon : is-nonzero-ℕ k → is-finite vertex-Polygon
is-finite-vertex-Polygon H =
is-finite-mere-equiv mere-equiv-vertex-Polygon (is-finite-ℤ-Mod H)

is-set-vertex-Polygon : is-set vertex-Polygon
is-set-vertex-Polygon =
is-set-mere-equiv' mere-equiv-vertex-Polygon (is-set-ℤ-Mod k)

has-decidable-equality-vertex-Polygon : has-decidable-equality vertex-Polygon
has-decidable-equality-vertex-Polygon =
has-decidable-equality-mere-equiv'
( mere-equiv-vertex-Polygon)
( has-decidable-equality-ℤ-Mod k)


Properties

The type of vertices of a polygon is a set

is-set-vertex-standard-polygon-Undirected-Graph :
(k : ℕ) → is-set (vertex-standard-polygon-Undirected-Graph k)
is-set-vertex-standard-polygon-Undirected-Graph k = is-set-ℤ-Mod k


Every edge is between distinct points

This remains to be formalized.

Every polygon is a simple graph

This remains to be formalized.

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