lib.graph-families.CycleGraph.RotHom.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 #-}
open import foundations.Core using (Level)
module lib.graph-families.CycleGraph.RotHom (ℓ : Level)
where
open import foundations.Core
open import lib.graph-definitions.Graph
open import lib.graph-homomorphisms.Hom
open import lib.graph-families.CycleGraph
open import lib.graph-classes.UnitGraph using (𝟙-graph)
module rot-homs (n : ℕ)
where
open import foundations.Fin ℓ
renaming ( fin-pred to α-rot
; fin-pred-equiv to α-rot-is-equiv
; fin-pred-inj to α-rot-is-inj
) public
private
Cn : Graph ℓ
Cn = Cycle ℓ (succ n)
β-rot
: (x y : Node Cn)
→ Edge Cn x y
-----------------------------
→ Edge Cn (α-rot x) (α-rot y)
β-rot x y p = ap α-rot p
β-rot-back
: (x y : Node Cn)
→ Edge Cn (α-rot x) (α-rot y)
→ Edge Cn x y
β-rot-back x y e = α-rot-is-inj e
β-rot-is-equiv
: ∀ (x y : Node Cn)
→ Edge Cn x y ≃ Edge Cn (α-rot x) (α-rot y)
β-rot-is-equiv x y
= qinv-≃ (β-rot _ _)
(β-rot-back _ _
, (λ _ → Fin-is-set _ _ _ _)
, λ _ → Fin-is-set _ _ _ _)
rot' : Hom Cn Cn
rot' = ⟨ α-rot , β-rot ⟩
rot : (n : ℕ) → Hom (Cycle ℓ n) (Cycle ℓ n)
rot zero = id-hom (𝟙-graph ℓ)
rot (succ n) = ⟨ α-rot , β-rot ⟩
where open rot-homs n
open import lib.graph-homomorphisms.classes.Isomorphisms
open import lib.graph-relations.Isomorphic
rot-is-iso : (n : ℕ) → IsoHom (rot n)
rot-is-iso zero = id-iso (𝟙-graph ℓ)
rot-is-iso (succ n) = π₂ (α-rot-is-equiv)
, λ x y → π₂ (β-rot-is-equiv _ _)
where open rot-homs n
rot-≅ : (n : ℕ) → Cycle ℓ n ≅ Cycle ℓ n
rot-≅ n = is-iso-to-≅ (rot n) (rot-is-iso n)
-- open hom-from-iso (rot n) (rot-is-iso n)
rot⁻¹ : (n : ℕ) → Hom (Cycle ℓ n) (Cycle ℓ n)
rot⁻¹ zero = id-hom (𝟙-graph ℓ)
rot⁻¹ (succ n) = inv-from-iso
where open hom-from-iso (rot (succ n)) (rot-is-iso (succ n))
rot⁻¹-is-iso : (n : ℕ) → IsoHom (rot⁻¹ n)
rot⁻¹-is-iso zero = id-iso (𝟙-graph ℓ)
rot⁻¹-is-iso (succ n) = inv-from-iso-is-iso
where open hom-from-iso (rot (succ n)) (rot-is-iso (succ n))
rot⁻¹-≅ : (n : ℕ) → Cycle ℓ n ≅ Cycle ℓ n
rot⁻¹-≅ zero = is-iso-to-≅ (id-hom (𝟙-graph ℓ)) (id-iso (𝟙-graph ℓ))
rot⁻¹-≅ (succ n) = is-iso-to-≅ (rot⁻¹ (succ n)) (rot⁻¹-is-iso (succ n))
where open import lib.graph-calculation-reasoning.Isos
module _ (n : ℕ) where
open import lib.graph-calculation-reasoning.Isos
rot-k-is-iso : (k : ℕ) → IsoHom (rot n ^-hom k )
rot-k-is-iso zero = id-iso (Cycle ℓ n )
rot-k-is-iso (succ k) = π₂ (≅-to-is-iso {G = Cycle ℓ n}{H = Cycle ℓ n} eq₂)
where
to-k-is-iso : IsoHom (rot n ^-hom k)
to-k-is-iso = rot-k-is-iso k
eq₁ : Cycle ℓ n ≅ Cycle ℓ n
eq₁ = is-iso-to-≅ (rot n ^-hom k) to-k-is-iso
eq₂ : Cycle ℓ n ≅ Cycle ℓ n
eq₂ = ≅-trans {ℓ}{A = Cycle ℓ n}{B = Cycle ℓ n}{C = Cycle ℓ n } eq₁ (rot-≅ n)
(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