lib.graph-families.CycleGraph.Map.md.
Version of Sunday, January 22, 2023, 10:42 PM
Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3
{-# OPTIONS --without-K --exact-split #-}
module lib.graph-families.CycleGraph.Map
where
open import foundations.Core
open import lib.graph-definitions.Graph
open Graph
open import lib.graph-embeddings.Map
module
_ (ℓ : Level)
(n : ℕ)
where
open import foundations.Nat ℓ
open import foundations.Fin ℓ
open import lib.graph-families.CycleGraph ℓ
open import lib.graph-classes.UndirectedGraph
module
Star-Cn
where
Star-Cn-≃-𝟚
: (n : ℕ)
→ (x : Node (Cycle (succ n)))
→ Star (Cycle (succ n)) x ≃ 𝟚 ℓ
module
_
(n : ℕ)
(x : Node (Cycle (succ n)))
where
S-f : Star (Cycle (succ n)) x → 𝟚 ℓ
S-f (y , inl p) = 𝟘₂
S-f (y , inr p) = 𝟙₂
S-g : 𝟚 ℓ → Star (Cycle (succ n)) x
S-g 𝟘₂ = fin-suc x , inl (with-succ x)
S-g 𝟙₂ = fin-pred x , inr (with-pred x)
S-H₁ : S-f ∘ S-g ∼ id
S-H₁ 𝟘₂ = idp
S-H₁ 𝟙₂ = idp
S-H₂
: (n : ℕ) (x : Node (Cycle (succ n)))
→ (S-g _ x) ∘ (S-f _ x) ∼ id
-- Case n ≡ 1. G :≡ ↺ and UG:≡ ↺. Be aware of the "two" edges.
S-H₂ 0 (zero , ∗) ((zero , ∗) , inl idp) = idp
S-H₂ 0 (zero , ∗) ((zero , ∗) , inr idp) = idp
S-H₂ 0 (zero , ∗) ((succ zero , ()) , _)
S-H₂ 0 (succ zero , ()) _
-- Case n ≡ 2. G :≡ ∙↔∙ and UG :≡ ∙-∙
-- · The intuition is: at x. there is one edge getting in but also one getting out.
-- For each, we have one edge in UG, therefore a Star at x must contain these two.
S-H₂ 1 (0 , ∗) ((0 , ∗) , inl ())
S-H₂ 1 (0 , ∗) ((0 , ∗) , inr ())
S-H₂ 1 (0 , ∗) ((1 , ∗) , inl idp) = idp
S-H₂ 1 (0 , ∗) ((1 , ∗) , inr idp) = idp
S-H₂ 1 (0 , ∗) ((2 , ()) , _)
S-H₂ 1 (1 , ∗) ((0 , ∗) , inl idp) = idp
S-H₂ 1 (1 , ∗) ((0 , ∗) , inr idp) = idp
S-H₂ 1 (1 , ∗) ((1 , ∗) , inl ())
S-H₂ 1 (1 , ∗) ((1 , ∗) , inr ())
S-H₂ 1 (1 , ∗) ((2 , ()) , _)
S-H₂ 1 (2 , ()) ((0 , ∗) , inr ())
-- Case n ≥ 3.
S-H₂ n@(succ (succ _)) x (y , inl p) =
pair=
( unique-sol-if-exists-with-pred x (fin-suc x) (with-succ x) y p
, Edge-Undirected-Cn-is-prop _ _ _ _)
S-H₂ n@(succ (succ _)) x (y , inr p) =
pair=
( (! p)
, Edge-Undirected-Cn-is-prop _ _ _ _ )
-- proof:
Star-Cn-≃-𝟚 _ x = qinv-≃ (S-f _ x) (S-g _ x , S-H₁ _ x , S-H₂ _ x)
Star-Cn-≃-⟦2⟧
: (n : ℕ) → (x : Node (Cycle (succ n)))
→ (Star (Cycle (succ n)) x) ≃ ⟦ 2 ⟧
Star-Cn-≃-⟦2⟧ n x = ≃-trans (Star-Cn-≃-𝟚 n x) 𝟚-≃-⟦2⟧
Now, we prove such a star defined above posses a cyclic structure.
open import foundations.Cyclic ℓ
Star-Cn-is-cyclic-with-pred
: (n : ℕ) → (x : Node (Cycle (succ n)))
→ (Star (Cycle (succ n)) x) is-cyclic
Star-Cn-is-cyclic-with-pred n x
= tr (λ X → CyclicSet X) (ua (≃-sym (Star-Cn-≃-⟦2⟧ n x))) (Fin-with-pred-is-cyclic 2)
where
open import foundations.UnivalenceAxiom
open Star-Cn
Star-Cn-is-cyclic-with-suc
: (n : ℕ) → (x : Node (Cycle (succ n)))
→ (Star (Cycle (succ n)) x) is-cyclic
Star-Cn-is-cyclic-with-suc n x
= tr (λ X → CyclicSet X) (ua (≃-sym (Star-Cn-≃-⟦2⟧ n x))) Fin2-with-suc-is-cyclic
where
open import foundations.UnivalenceAxiom
open Star-Cn
Now, we are able to give a rotation system for eah node in the Cycle graph with n number of vertices:
Cn-Map₁ : Map (Cycle (succ n))
Cn-Map₁ = λ x → Star-Cn-is-cyclic-with-pred n x
Cn-Map₂ : Map (Cycle (succ n))
Cn-Map₂ = λ x → Star-Cn-is-cyclic-with-suc n x
The two maps are equal. This folows from the charactherization of cyclic structure. The equivalence is \[(A'=B') ≃ ∑[ e : A = B] (coe(e) ∘ f = g ∘ coe(e))\]. However, two cyclic structures for the same type are equal iff the underlying functions are equal. Thus, assumming function extensionality, one can say ⟨⟦2⟧, pred, 2 ⟩ = ⟨⟦2⟧, suc, 2⟩, since pred and succ defined for ⟦ 2 ⟧ are extensionally equal.
Cn-Map₁≡Cn-Map₂ : Cn-Map₁ ≡ Cn-Map₂
Cn-Map₁≡Cn-Map₂ =
funext λ x → ap ( tr _ (ua _))
$ rapply (lemma-2-13 (Fin-with-pred-is-cyclic 2) Fin2-with-suc-is-cyclic)
(funext (λ { (zero , ∗) → idp
; (succ zero , _) → idp
; (succ (succ n) , <0)
→ ⊥-elim {ℓ} (n<0 {ℓ} {n = n} <0)}))
where
open Star-Cn
open import foundations.UnivalenceAxiom
open import foundations.FunExtAxiom
(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides (2022-07-06)(d3a4a8cf) minors by jonathan.cubides (2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides (2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides (2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides (2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides (2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides (2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides (2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides (2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides (2021-12-15)(0630ce66) Minor fixes by jonathan.cubides (2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides (2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides (2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides (2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides