lib.graph-embeddings.Map.Spherical-is-enough.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-embeddings.Map.Spherical-is-enough
where
open import foundations.Core
open import lib.graph-definitions.Graph
open import lib.graph-transformations.U
open Graph
open import lib.graph-embeddings.Map
open import lib.graph-embeddings.Map.Face.Walk.Homotopy
open import lib.graph-embeddings.Map.Spherical
module
hom-normalisation
{ℓ : Level} (G : Graph ℓ)
(_≟Node_ : (x y : Node (U G)) → (x ≡ y) + (x ≠ y))
(M : Map G)
(M-is-spherical : isSphericalMap G M)
where
open import lib.graph-walks.Walk.QuasiSimple
open WR (U G) (_≟Node_)
open quasi-simple-walks {ℓ}{G = U G}
open import lib.graph-walks.Walk hiding (length)
open import lib.graph-walks.Walk.Composition
open ∈-walk (U G)
open ∙-walk (U G)
open import foundations.Nat ℓ
open dec-<
open import lib.graph-embeddings.Map.Face.Walk.Homotopy
open import lib.graph-embeddings.Map.Face.Walk.Whiskering
e⊙∼ : ∀ {x}{e : Edge (U G) x x} → ∥ (e ⊙ ⟨ _ ⟩) ∼⟨ M ⟩∼ ⟨ _ ⟩ ∥
e⊙∼ {x = x} {e = e} = M-is-spherical _ _ _ _ (one-edge-is-quasi-simple e) (one-point-walk-is-quasi-simple x)
PNom : ∀ {x z : Node (U G)}
→ Walk (U G) x z
→ Type (lsuc ℓ)
PNom {x = x}{z} = λ w → ∑[ v ∶ Walk (U G) x z ] ((w →r* v) × ((Normal v) × ∥ w ∼⟨ M ⟩∼ v ∥))
hom-normalize : ∀ {x z} → (w : Walk (U G) x z) → PNom w
hom-normalize = ∑∑walk-rec PNom body
where
open HomotopyWalks {ℓ = ℓ}{G} M
open Whiskering {ℓ = ℓ}{G} M
body
: ∀ {x z : Node G} (b : Walk (U G) x z)
→ ({x' z' : Node G} (a : Walk (U G) x' z') → ∑∑walk a ⊰ ∑∑walk b → PNom a)
-------------------------------------------------------------------------
→ PNom b
body ⟨ x ⟩ φ =
⟨ x ⟩
, (⟨ _ ⟩ →r*∎)
, (normal (one-point-walk-is-quasi-simple x) (No-reduce-no-step ⟨ x ⟩ is-dot))
, ∣ hwalk-refl ∣
body {x = x}{z} (e ⊙ ⟨ _ ⟩) φ
with x ≟Node z
... | inl idp = ⟨ x ⟩
, one-step (ξ₁ _ _ (is-loop idp ⟨ x ⟩) (is-dot idp))
, (normal (one-point-walk-is-quasi-simple x) (No-reduce-no-step ⟨ x ⟩ is-dot))
, M-is-spherical _ _ (e ⊙ ⟨ x ⟩ ) ⟨ x ⟩ (one-edge-is-quasi-simple e) (one-point-walk-is-quasi-simple x)
... | inr x≠z = (e ⊙ ⟨ _ ⟩)
, ((e ⊙ ⟨ z ⟩) →r*∎)
, (normal (one-edge-is-quasi-simple e) (No-reduce-no-step _ (is-edge x≠z)))
, ∣ whiskerL (e ⊙ ⟨ _ ⟩ ) hwalk-refl ∣
body {x = x}{z} (e ⊙ w@(_ ⊙ _)) φ
with (let y = start-of (U G) w
in
x ≟Node y)
... | inl idp = helper
where
helper : PNom (e ⊙ w)
helper with φ w (<-succ (length w))
... | (w' , w→w' , (WR.normal w'-is-quasi-simple no-red) , w∼w')
with x ≟Node z
... | inl idp =
⟨ x ⟩
, one-step (ξ₁ (e ⊙ w) ⟨ x ⟩ (is-loop idp _) (is-dot idp))
, (normal (one-point-walk-is-quasi-simple x) (No-reduce-no-step ⟨ x ⟩ is-dot))
, trunc-elim trunc-is-prop (λ e∼ →
trunc-elim trunc-is-prop (λ w∼ →
trunc-elim trunc-is-prop (λ w'∼ → ∣ whisker-h e∼ (hwalk-trans w∼ w'∼) ∣)
w'∼dot)
w∼w')
(e⊙∼ {e = e})
where
w'∼dot : ∥ w' ∼⟨ M ⟩∼ ⟨ x ⟩ ∥
w'∼dot = M-is-spherical _ _ w' ⟨ x ⟩ w'-is-quasi-simple (one-point-walk-is-quasi-simple x)
... | inr x≠z
= w'
, (begin→r*
e ⊙ w →r*⟨ (e ⊙ w) →r*∎ ⟩
(e ⊙ ⟨ x ⟩) ∙w w →r*⟨ one-step (ξ₃ _ ⟨ _ ⟩ _ (λ { (is-loop x) → x≠z x})
(is-loop idp) (has-edge _) _ idp) ⟩
w →r*⟨ w→w' ⟩
w' →r*∎)
, (normal w'-is-quasi-simple no-red)
, trunc-elim trunc-is-prop (λ ew∼w →
trunc-elim trunc-is-prop (λ w∼ → ∣ whisker-h ew∼w w∼ ∣ )
w∼w')
e⊙∼
... | inr x≠y
with split w at x
... | just w1 w1prefix w1∌x = helper
where
helper : _
helper with find-suffix w1 w w1prefix
... | (w2 , w≡w1∙w2) = helper2
where
helper2 : PNom (e ⊙ w)
helper2 with φ w2 (right-part<whole w w1 w2 w≡w1∙w2)
... | (w' , w2→w' , (normal w'-is-quasi-simple no-red) , w2∼w')
with x ≟Node z
... | inl idp =
⟨ x ⟩
, one-step (ξ₁ (e ⊙ w) ⟨ x ⟩ (is-loop idp _) (is-dot idp))
, (normal (one-point-walk-is-quasi-simple x) (No-reduce-no-step ⟨ x ⟩ is-dot))
, trunc-elim trunc-is-prop
(λ e⊙w∼ →
trunc-elim trunc-is-prop (λ w'∼ → ∣ hwalk-trans e⊙w∼ w'∼ ∣)
w'∼dot)
helper3
where
w'∼dot : ∥ w' ∼⟨ M ⟩∼ ⟨ x ⟩ ∥
w'∼dot = M-is-spherical _ _ w' ⟨ x ⟩ w'-is-quasi-simple (one-point-walk-is-quasi-simple x)
helper3 : ∥ (e ⊙ w) ∼⟨ M ⟩∼ w' ∥
helper3 with φ w1 (left-part<whole w w1 w2 w≡w1∙w2)
... | v , w1→v , (normal v-is-quasi-simple no-red) , w1∼v
= trunc-elim trunc-is-prop (λ ev∼dot
→ trunc-elim trunc-is-prop (λ w1∼
→ trunc-elim trunc-is-prop (λ w2∼
→ ∣ hwalk-trans (tr (λ o → (e ⊙ o) ∼⟨ M ⟩∼ w2) (! w≡w1∙w2)
(whiskerR (hwalk-trans
(whiskerL (e ⊙ ⟨ _ ⟩) w1∼) ev∼dot)
w2))
w2∼ ∣)
w2∼w')
w1∼v )
e⊙v∼dot
where
e⊙v-is-quasi-simple : (e ⊙ v) is-quasi-simple
e⊙v-is-quasi-simple = ⊙-quasi-simple-is-quasi-simple {e = e} v-is-quasi-simple (nf-¬∈ w1 w1∌x v w1→v)
e⊙v∼dot : ∥ (e ⊙ v) ∼⟨ M ⟩∼ ⟨ x ⟩ ∥
e⊙v∼dot = M-is-spherical _ _ (e ⊙ v) ⟨ x ⟩
e⊙v-is-quasi-simple
(one-point-walk-is-quasi-simple x)
... | inr x≠z
= w'
, (begin→r*
e ⊙ w →r*⟨ ξ₂-⊙ {a≠b = x≠y}{x≠z}(subs w≡w1∙w2) e ⟩
(e ⊙ w1) ·w w2 →r*⟨ one-step (ξ₃ _ _ _ (λ { (is-loop x) → x≠z x}) (is-loop idp)
(different-endpoints-is-nontrivial x≠z w2) _ idp) ⟩
w2 →r*⟨ w2→w' ⟩
w' →r*∎)
, (normal w'-is-quasi-simple no-red)
, helper3 -- Need two extra lemmas.
where
helper3 : ∥ (e ⊙ w) ∼⟨ M ⟩∼ w' ∥
helper3 with φ w1 (left-part<whole w w1 w2 w≡w1∙w2)
... | v , w1→v , (normal v-is-quasi-simple no-red) , w1∼v
= trunc-elim trunc-is-prop (λ ev∼dot
→ trunc-elim trunc-is-prop (λ w1∼
→ trunc-elim trunc-is-prop (λ w2∼
→ ∣ hwalk-trans (tr (λ o → (e ⊙ o) ∼⟨ M ⟩∼ w2) (! w≡w1∙w2)
(whiskerR (hwalk-trans
(whiskerL (e ⊙ ⟨ _ ⟩) w1∼) ev∼dot)
w2))
w2∼ ∣)
w2∼w')
w1∼v )
e⊙v∼dot
where
e⊙v-is-quasi-simple : (e ⊙ v) is-quasi-simple
e⊙v-is-quasi-simple = ⊙-quasi-simple-is-quasi-simple {e = e} v-is-quasi-simple (nf-¬∈ w1 w1∌x v w1→v)
e⊙v∼dot : ∥ (e ⊙ v) ∼⟨ M ⟩∼ ⟨ x ⟩ ∥
e⊙v∼dot = M-is-spherical _ _ (e ⊙ v) ⟨ x ⟩
e⊙v-is-quasi-simple
(one-point-walk-is-quasi-simple x)
... | nothing w∌x
with φ w (<-succ (length w))
... | ⟨ _ ⟩ , w→w' , (normal pp no-red) , w∼w' = helper
where
helper : _
helper with x ≟Node z
... | inl idp =
⟨ x ⟩
, one-step (ξ₁ (e ⊙ w) ⟨ x ⟩ (is-loop idp _) (is-dot idp))
, (normal (one-point-walk-is-quasi-simple x) (No-reduce-no-step ⟨ x ⟩ is-dot))
, trunc-elim trunc-is-prop (λ ew∼w →
trunc-elim trunc-is-prop (λ w∼ → ∣ whisker-h ew∼w w∼ ∣ )
w∼w')
e⊙∼
... | inr x≠z
= (e ⊙ ⟨ z ⟩)
, ξ₂-⊙ {a≠b = x≠z}{x≠z} w→w' e
, (normal (one-edge-is-quasi-simple e)
(No-reduce-no-step (e ⊙ ⟨ z ⟩) (is-edge x≠z)))
, trunc-elim trunc-is-prop (λ h∼ → ∣ whiskerL (e ⊙ ⟨ _ ⟩) h∼ ∣) w∼w'
... | (w'@(m ⊙ sw) , w→w' , (normal w'-is-quasi-simple no-red) , w∼w')
with x ≟Node z
... | inl idp =
⟨ x ⟩
, one-step (ξ₁ (e ⊙ w) ⟨ x ⟩ (is-loop idp _) (is-dot idp))
, (normal (one-point-walk-is-quasi-simple x) (No-reduce-no-step ⟨ x ⟩ is-dot))
, trunc-elim trunc-is-prop
(λ e⊙w'∼ →
trunc-elim trunc-is-prop (λ w∼ → ∣ hwalk-trans (whiskerL (e ⊙ ⟨ _ ⟩) w∼) e⊙w'∼ ∣)
w∼w' )
e⊙w'∼dot
where
e⊙w'-is-quasi-simple : (e ⊙ w') is-quasi-simple
e⊙w'-is-quasi-simple = ⊙-quasi-simple-is-quasi-simple {e = e} {w'} w'-is-quasi-simple ¬x∈w'
where
¬x∈w' : ¬ (x ∈w w')
¬x∈w' x∈w' = ⊥-elim (w∌x x∈w)
where
x∈w : x ∈w w
x∈w = nf-∈' w' x∈w' w w→w'
e⊙w'∼dot : ∥ (e ⊙ w') ∼⟨ M ⟩∼ ⟨ x ⟩ ∥
e⊙w'∼dot = M-is-spherical _ _ _ ⟨ x ⟩ e⊙w'-is-quasi-simple (one-point-walk-is-quasi-simple x)
... | inr x≠z
= (e ⊙ w') , e⊙w-to-e⊙w' , (normal e⊙w'-is-quasi-simple ¬red-e⊙w')
, trunc-elim trunc-is-prop (λ h∼ → ∣ whiskerL (e ⊙ ⟨ _ ⟩) h∼ ∣) w∼w'
where
e⊙w-to-e⊙w' : (e ⊙ w) →r* (e ⊙ w')
e⊙w-to-e⊙w' = ξ₂-⊙ {a≠b = x≠y}{x≠z} w→w' e
e⊙w'-is-quasi-simple : (e ⊙ w') is-quasi-simple
e⊙w'-is-quasi-simple = ⊙-quasi-simple-is-quasi-simple {e = e} {w'} w'-is-quasi-simple ¬x∈w'
where
¬x∈w' : ¬ (x ∈w w')
¬x∈w' x∈w' = ⊥-elim (w∌x x∈w)
where
x∈w : x ∈w w
x∈w = nf-∈' w' x∈w' w w→w'
¬red-e⊙w' : Reduce (e ⊙ w') → ⊥ ℓ
¬red-e⊙w' (reduction (ξ₁ _ _ (is-loop x≡y _) to-dot)) = ⊥-elim (x≠z x≡y)
¬red-e⊙w' (reduction (ξ₂ _ _ _ _ _ w'→q)) = no-red (reduction w'→q)
¬red-e⊙w' (reduction (ξ₃ e p q ¬l l nt .(_ ⊙ (m ⊙ sw)) w≡)) = get-⊥ x-in-different-pos
where
x∈q : x ∈w (p ∙w q)
x∈q = ∈-∙w-right _ (∈-non-trivial q nt) p
x∈w' : x ∈w w'
x∈w' with ≡-walks-to-∑ w≡
... | idp , m⊙sw≡p∙q = tr (λ o → x ∈w o) (! m⊙sw≡p∙q) x∈q
x-in-different-pos : inr x∈w' ≡ inl idp
x-in-different-pos = e⊙w'-is-quasi-simple x (inr x∈w') (inl idp)
get-⊥ : inr x∈w' ≡ inl idp → ⊥ ℓ
get-⊥ ()
module _
{ℓ : Level} (G : Graph ℓ)
(_≟Node_ : (x y : Node (U G)) → (x ≡ y) + (x ≠ y))
where
open import lib.graph-embeddings.Map
open import lib.graph-embeddings.Map.Face.Walk.Homotopy
open import lib.graph-walks.Walk
open import lib.graph-walks.Walk.QuasiSimple
open hom-normalisation G (_≟Node_)
isSphericalMapS : Map G → Type (lsuc ℓ)
isSphericalMapS 𝕄 = (x : Node (U G)) → (w : Walk (U G) x x)
→ ∥ (w ∼⟨ 𝕄 ⟩∼ ⟨ x ⟩) ∥
isSphericalMap' : Map G → Type (lsuc ℓ)
isSphericalMap' 𝕄 = (x y : Node (U G)) → (w₁ w₂ : Walk (U G) x y)
→ ∥ w₁ ∼⟨ 𝕄 ⟩∼ w₂ ∥
isSphericalMap'-is-prop : (𝕄 : Map G) → isProp (isSphericalMap' 𝕄)
isSphericalMap'-is-prop 𝕄 =
pi-is-prop
$ λ _ → pi-is-prop
$ λ _ → pi-is-prop
$ λ _ → pi-is-prop
$ λ _ → truncated-is-prop
spherical-equiv : (𝕄 : Map G) → isSphericalMap G 𝕄 ≃ isSphericalMap' 𝕄
spherical-equiv 𝕄 = qinv-≃ go (back , ((λ x → isSphericalMap'-is-prop 𝕄 _ _)) ,
λ x → isSphericalMap-is-prop G 𝕄 _ _)
where
back : isSphericalMap' 𝕄 → isSphericalMap G 𝕄
back g x y w1 w2 _ _ = g x y w1 w2
go : isSphericalMap G 𝕄 → isSphericalMap' 𝕄
go f _ _ w1 w2
with hom-normalize 𝕄 f w1 | hom-normalize 𝕄 f w2
... | u , _ , WR.normal u-is-quasi-simple _ , w1∼u
| v , _ , WR.normal v-is-quasi-simple _ , w2∼v = helper
where
helper : ∥ w1 ∼⟨ 𝕄 ⟩∼ w2 ∥
helper = trunc-elim trunc-is-prop
(λ w1∼ → trunc-elim trunc-is-prop
(λ w2∼ → (trunc-elim trunc-is-prop
(λ w1'∼w2' → ∣ HomotopyWalks.hwalk-trans w1∼
(HomotopyWalks.hwalk-trans
w1'∼w2'
(HomotopyWalks.hwalk-symm w2∼))∣)
(f _ _ u v u-is-quasi-simple v-is-quasi-simple)))
w2∼v)
w1∼u
(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