lib.graph-families.CycleGraph.Isomorphisms.IdentityType.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.Isomorphisms.IdentityType
where
open import foundations.Core
-- The main result here is that:
-- (Cn iso Cn) = ⟦ n ⟧
module
_
(ℓ : Level)
where
open import foundations.Fin ℓ
open import foundations.Nat ℓ
open import foundations.Cyclic ℓ
open import lib.graph-definitions.Graph
open Graph
open import lib.graph-families.CycleGraph ℓ
open import lib.graph-homomorphisms.Hom
open Hom
open import lib.graph-relations.Isomorphic
open import lib.graph-families.CycleGraph.RotHom
module
_
(m : ℕ)
where
n = succ m
n>0 : 0 < n
n>0 = <-succ zero
Cn = Cycle n
0' : ⟦ n ⟧
0' = (0 , n>0)
find-k-f
: (f : Node Cn → Node Cn)
→ ∑[ k ∶ ⟦ n ⟧ ] ((fin-pred ^ (π₁ k)) 0' ≡ f 0')
× ((k' : ⟦ n ⟧) → (fin-pred ^ (π₁ k')) 0' ≡ (f 0') → k ≡ k')
find-k-f f = find-k-pred 0' (f 0')
find-k-rot
: (f : Node (Cn) → Node (Cn))
→ ∑[ (k , k< ) ∶ ⟦ n ⟧ ] ((α (rot ℓ n ^-hom k) 0') ≡ f 0')
find-k-rot f = π₁ sol ,
(! happly (lemma-on-nodes-hom-expo (rot ℓ n) (π₁ (π₁ sol))) 0' · π₁ (π₂ sol))
where
open import foundations.FunExtAxiom
sol = find-k-f f
Isos-→-Fin : (n : ℕ) (n>0 : n > 0) → (Cycle n ≅ Cycle n) → ⟦ n ⟧
Isos-→-Fin zero ()
Isos-→-Fin n@(succ _) ∗ (f , g) = π₁ (find-k-f _ (f ∙))
Fin-→-Isos : (n : ℕ) (n>0 : n > 0) → ⟦ n ⟧ → (Cycle n ≅ Cycle n)
Fin-→-Isos zero ()
Fin-→-Isos n@(succ _) ∗ (k , _) = is-iso-to-≅ (rot ℓ n ^-hom k) (rot-k-is-iso ℓ n k)
H₁ : (n : ℕ) (n>0 : n > 0) (k : ⟦ n ⟧)
→ Isos-→-Fin n n>0 (Fin-→-Isos n n>0 k) ≡ k
H₁ zero ()
H₁ n@(succ m) ∗ k = eq₁ k eq₂
where
private
f = α (rot ℓ n ^-hom (π₁ k))
eq₁ : (o : ⟦ n ⟧)
→ (fin-pred ^ (π₁ o)) (0' m) ≡ (f (0' m))
→ π₁ (find-k-f _ f) ≡ o
eq₁ = π₂ (π₂ (find-k-f _ f))
eq₂ : (fin-pred ^ π₁ k) (0' _) ≡ f (0' _)
eq₂ = happly (lemma-on-nodes-hom-expo (rot ℓ n) (π₁ k)) (0' _)
where open import foundations.FunExtAxiom
H₂ : (n : ℕ) (n>0 : n > 0) (φ : Cycle n ≅ Cycle n)
→ Fin-→-Isos n n>0 (Isos-→-Fin n n>0 φ) ≡ φ
H₂ zero () iso@(f , g)
H₂ n@(succ _) ∗ iso@(f , g) =
pair= (sameEqv (funext λ {(m , p) → helper m p}) ,
funext (λ x → funext (λ y →
pair= (funext (λ {idp → Fin-is-set _ _ _ _}) , isEquivIsProp _ _ _))))
where
open import foundations.FunExtAxiom
aux : ∑[ (k , k< ) ∶ ⟦ n ⟧ ] ((α (rot ℓ n ^-hom k) (0' _)) ≡ (f ∙) (0' _))
aux = find-k-rot _ (f ∙)
k : ⟦ n ⟧
k = Isos-→-Fin n ∗ iso
open dec-<
helper : (x : ℕ) → (p : x < n) → α (expo-hom (π₁ k) (rot ℓ n)) (x , p) ≡ (f ∙) (x , p)
helper zero p = tr (λ e → (α (expo-hom (π₁ k) (rot ℓ n)) e ≡ (f ∙) e)) aux-oo-1 (π₂ aux)
where
aux-oo-1 : (0' _) ≡ (zero , p)
aux-oo-1 = (pair= (idp , <-prop {n = n}{m = 0} (π₂ (0' n)) p))
helper (succ m) p =
let m+ = (succ m , p) in
α ((rot ℓ n) ^-hom (π₁ k)) m+ ≡⟨ i ⟩
(fin-pred ^ (π₁ k)) m+ ≡⟨ ii ⟩
(fin-pred ^ (π₁ k)) ((fin-suc)(m , m<n)) ≡⟨ iii ⟩
(fin-suc) ((fin-pred ^ (π₁ k)) ((m , m<n))) ≡⟨ iv ⟩
fin-suc (α (expo-hom (π₁ k) (rot ℓ n)) ((m , m<n))) ≡⟨ v ⟩
fin-suc ((f ∙) (m , m<n)) ≡⟨ vi ⟩
fin-suc (fin-pred ((f ∙) m+)) ≡⟨ vii ⟩
(f ∙) m+ ∎
where
-- helpers
open import foundations.FunExtAxiom
m+ = (succ m , p)
m<n : m < n
m<n = <-inj {m = m} p
edge-m-to-m+ : fin-pred (succ m , p) ≡ (m , m<n)
edge-m-to-m+ = pair= (idp , <-prop {m = m} _ m<n)
m+-is-suc-m : (succ m , p) ≡ fin-suc (m , m<n)
m+-is-suc-m = fin-pred^-to-fin-suc^ _ (m , m<n) 1 edge-m-to-m+
-- step explanations:
i = ! happly (lemma-on-nodes-hom-expo (rot ℓ n) (π₁ k)) m+
ii = ap (fin-pred ^ (π₁ k)) m+-is-suc-m
iii = ! succ-pred-comm'' {n = n}{m = π₁ k} (m , m<n)
iv = ap fin-suc (happly (lemma-on-nodes-hom-expo (rot ℓ n) (π₁ k)) (m , m<n))
v = ap fin-suc (helper m m<n)
vi = ap fin-suc ((g ((m , m<n)) m+ ∙) (! edge-m-to-m+))
vii = inverse-of-fin-pred∘fin-pred _
Isos-≃-Fin : (n : ℕ) (_ : n > 0) → (Cycle n ≅ Cycle n) ≃ ⟦ n ⟧
Isos-≃-Fin zero ()
Isos-≃-Fin n@(succ _) ∗ = qinv-≃ (Isos-→-Fin n ∗ ) (Fin-→-Isos n ∗ , H₁ n ∗ , H₂ n ∗ )
Isos-is-cyclic
: (n : ℕ) (n>0 : ℕ-ordering._>_ ℓ n 0)
→ CyclicSet (Cycle n ≅ Cycle n)
Isos-is-cyclic zero ()
Isos-is-cyclic n@(succ _ ) ∗
= tr (λ X → CyclicSet X)
(ua (≃-sym (Isos-≃-Fin n ∗)))
(Fin-with-pred-is-cyclic n)
where open import foundations.UnivalenceAxiom
(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