lib.graph-classes.CyclicGraph.Stuff.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-classes.CyclicGraph.Stuff
where
open import foundations.Core
open import lib.graph-definitions.Graph
open import lib.graph-homomorphisms.Hom
open import lib.graph-homomorphisms.classes.Isomorphisms
open import lib.graph-relations.Isomorphic
open import lib.graph-transformations.U
open import lib.graph-embeddings.Map
open import lib.graph-classes.CyclicGraph
open import foundations.Cyclic
open import foundations.Fin
open import lib.graph-families.CycleGraph
open import lib.graph-families.CycleGraph.RotHom
open import lib.graph-classes.UnitGraph
open CyclicGraph
open Hom
Nodes-with-pred-is-cyclic
: {ℓ : Level}
→ (G : Graph ℓ)
→ (G↺ : CyclicGraph ℓ G)
→ CyclicSet ℓ (Node G)
-- zero case:
CyclicSet.φ (Nodes-with-pred-is-cyclic {ℓ} G (cyclic-graph phi zero p)) = α phi
CyclicSet.n (Nodes-with-pred-is-cyclic {ℓ} G (cyclic-graph φ zero p)) = 1
CyclicSet.cyclicity (Nodes-with-pred-is-cyclic {ℓ} G (cyclic-graph φ zero p))
= trunc-elim truncated-is-prop (λ {idp → ∣ 𝟙-≃-⟦1⟧ ℓ , idp ∣}) p
where open import foundations.FunExtAxiom
-- succ case:
CyclicSet.φ (Nodes-with-pred-is-cyclic {ℓ} G G↺@(cyclic-graph φ n@(succ m) p)) = α (CyclicGraph.φ G↺)
CyclicSet.n (Nodes-with-pred-is-cyclic {ℓ} G G↺@(cyclic-graph φ n@(succ m) p)) = n
CyclicSet.cyclicity (Nodes-with-pred-is-cyclic {ℓ} G G↺@(cyclic-graph φ n@(succ m) p))
= trunc-elim truncated-is-prop proof p
where
φ↺ = α (CyclicGraph.φ G↺)
pred-↺ = Hom.α φ
proof
: Path {A = ∑[ H ] (Hom H H)}
(G , φ)
(Cycle ℓ n , rot ℓ n)
→ ∥ ∑[ e ∶ (Node G ≃ Fin ℓ n) ] ((pred-↺ ︔ (e ∙→)) ≡ ((e ∙→)︔ fin-pred ℓ )) ∥
proof idp = ∣ (idEqv , idp) ∣
pred-↺-is-equiv
: {ℓ : Level}
→ (G : Graph ℓ)
→ (G↺ : CyclicGraph ℓ G)
→ isEquiv (Hom.α (CyclicGraph.φ G↺))
pred-↺-is-equiv {ℓ} G G↺@(cyclic-graph phi zero G-is-cyclic)
= trunc-elim (is-equiv-is-prop _) (λ {idp → π₂ idEqv} ) G-is-cyclic
pred-↺-is-equiv {ℓ} G G↺@(cyclic-graph phi n@(succ m) G-is-cyclic)
= helper
where
helper : isEquiv (α (φ G↺))
helper = φ-is-equiv ℓ (Nodes-with-pred-is-cyclic G G↺)
size-cyclic-graph
: {ℓ : Level}
→ (G : Graph ℓ)
→ (G↺ : CyclicGraph ℓ G)
→ ℕ
size-cyclic-graph {ℓ} G G↺@(cyclic-graph φ₁ 0 is-cyclic₁) = 1
size-cyclic-graph {ℓ} G G↺@(cyclic-graph φ₁ (succ n) is-cyclic₁) = succ n
ccw-node-steps
: {ℓ : Level}
→ (G : Graph ℓ)
→ (G↺ : CyclicGraph ℓ G)
→ (a b : Node G)
→ let ord = size-cyclic-graph G G↺ in
∑[ k ∶ Fin ℓ ord ]
((α (φ G↺) ^ π₁ k) a ≡ b)
× (∏[ k' ∶ Fin ℓ ord ]
((α (φ G↺) ^ π₁ k') a ≡ b
→ k ≡ k'))
ccw-node-steps {ℓ} G G↺@(cyclic-graph φ₁ zero is-cyclic₁) a b =
(zero , ∗) , trunc-elim (∑-prop (Node-is-set G _ _) λ { idp
→ pi-is-prop (λ { (zero , snd₁)
→ pi-is-prop λ _ → Fin-is-set _ _ _ ; (succ fst₁ , snd₁)
→ pi-is-prop (λ {p → Fin-is-set _ _ _})})})
(λ {idp → idp , λ { (zero , ∗) → λ _ → idp
; (succ n , p) → ⊥-elim {ℓ}{ℓ} (n<0 ℓ {n = n} p)}}) is-cyclic₁
where
open import foundations.Nat
ccw-node-steps {ℓ} G G↺@(cyclic-graph φ₁ (succ n₁) is-cyclic₁)
= ccw-steps-in_from_to_ ℓ (Nodes-with-pred-is-cyclic G G↺)
module cyclic-graph-stuff
{ℓ : Level}
(G : Graph ℓ)
(G↺ : CyclicGraph ℓ G)
where
φ↺ : Hom G G
φ↺ = CyclicGraph.φ G↺
pred-↺ : Node G → Node G
pred-↺ = Hom.α φ↺
n↺ : ℕ
n↺ = CyclicGraph.n G↺
G-is-cyclic = CyclicGraph.is-cyclic G↺
φ-cyclic-graph-has-rot-properties
: (P : ∀ {X : Graph ℓ} → Hom X X → hProp ℓ)
→ (rot ℓ n↺) has-endo-hom-property P
→ φ↺ has-endo-hom-property P
φ-cyclic-graph-has-rot-properties P rot-has-the-property
= trunc-elim (π₂ (P φ↺)) proof G-is-cyclic
where
proof
: Path {A = ∑[ H ] (Hom H H)}
(G , φ↺)
(Cycle ℓ n↺ , rot ℓ n↺)
→ φ↺ has-endo-hom-property P
proof idp = rot-has-the-property
φ↺-is-iso : IsoHom φ↺
φ↺-is-iso
= φ-cyclic-graph-has-rot-properties
iso-is-property ( rot-is-iso ℓ n↺ )
where
iso-is-property : ∀ {X} → Hom X X → hProp ℓ
iso-is-property {X} h = IsoHom h , being-iso-is-prop h
φ⁻¹↺ : Hom G G
φ⁻¹↺ = inv-from-iso φ↺ φ↺-is-iso
where open hom-from-iso
φ⁻¹↺-is-iso : IsoHom φ⁻¹↺
φ⁻¹↺-is-iso = inv-from-iso-is-iso φ↺ φ↺-is-iso
where open hom-from-iso
suc-↺ : Node G → Node G
suc-↺ = Hom.α φ⁻¹↺
oinv : Node G → Node G
oinv = φ⁻¹ ℓ (Nodes-with-pred-is-cyclic G G↺)
open cyclic-graph-stuff
module _ where
suc-is-suc :
{ℓ : Level}
(G : Graph ℓ)
(G↺ : CyclicGraph ℓ G)
→ oinv G G↺ ≡ suc-↺ G G↺
suc-is-suc G G↺@(cyclic-graph φ₁ zero is-cyclic₁)
= trunc-elim (pi-is-set (λ _ → Node-is-set G) _ _)
(λ {idp → idp}) is-cyclic₁
where
open import foundations.FunExtAxiom
suc-is-suc G G↺@(cyclic-graph φ₁ (succ n₁) is-cyclic₁) =
funext (λ x → (! (ii _)) · (iii x) · (ii _))
where
open import foundations.FunExtAxiom
i : (x : Node G) → pred-↺ G G↺ (suc-↺ G G↺ x) ≡ x
i x = lrmap-inverse-h (π₁ (is-iso-to-≅ (φ G↺) ( φ↺-is-iso G G↺ ))) x
ii : (x : Node G)
→ suc-↺ G G↺ (pred-↺ G G↺ x) ≡ x
ii x = rlmap-inverse-h (π₁ (is-iso-to-≅ (φ G↺) (φ↺-is-iso G G↺ ))) x
iv : (x : Node G)
→ pred-↺ G G↺ (oinv G G↺ x) ≡ x
iv x = trunc-elim (Node-is-set G _ _)
(λ { idp → lrmap-inverse-h
(pred-↺ G G↺ , pred-↺-is-equiv G G↺) x}) (is-cyclic G↺)
iii : (x : Node G)
→ suc-↺ G G↺ (pred-↺ G G↺ (oinv G G↺ x)) ≡ suc-↺ G G↺ (pred-↺ G G↺ (suc-↺ G G↺ x))
iii x =
ap (suc-↺ G G↺ ) $
begin
pred-↺ G G↺ (oinv G G↺ x)
≡⟨ iv x ⟩
x
≡⟨ ! i x ⟩
pred-↺ G G↺ (suc-↺ G G↺ x) ∎
open cyclic-graph-stuff
open ℕ-ordering
pred-edge
: {ℓ : Level}
(G : Graph ℓ)
(G↺ : CyclicGraph ℓ G)
→ _<_ ℓ 0 (n G↺)
→ (x : Node G) → Edge G (α (φ G↺) x) x
pred-edge G (cyclic-graph phi zero G-is-cyclic) ()
pred-edge {ℓ} G G↺@(cyclic-graph phi n@(succ m) G-is-cyclic) p
= trunc-elim
(φ-cyclic-graph-has-rot-properties
G
G↺
(λ {X} h → isProp ((x : Node X) → Edge X (α h x) x)
, is-prop-is-prop)
(pi-is-prop λ _ → with-pred-is-prop ℓ _ ))
(λ { idp x → refl (α phi x)})
G-is-cyclic
cw-node-steps
: {ℓ : Level}
→ (G : Graph ℓ)
→ (G↺ : CyclicGraph ℓ G)
→ (a b : Node G)
→ let ord = size-cyclic-graph G G↺ in
∑[ k ∶ Fin ℓ ord ]
((suc-↺ G G↺ ^ π₁ k) a ≡ b)
× (∏[ k' ∶ Fin ℓ ord ]
((suc-↺ G G↺ ^ π₁ k') a ≡ b
→ k ≡ k'))
cw-node-steps {ℓ} G G↺@(cyclic-graph φ₁ zero is-cyclic₁) a b =
let ord = size-cyclic-graph G G↺ in
tr (λ f → ∑[ k ∶ _ ]
((f ^ π₁ k) a ≡ b) × (∏[ k' ∶ Fin ℓ ord ] ((f ^ π₁ k') a ≡ b
→ k ≡ k')))
(suc-is-suc G G↺)
(cw-steps-in_from_to_ ℓ (Nodes-with-pred-is-cyclic G G↺) a b)
cw-node-steps {ℓ} G G↺@(cyclic-graph φ₁ (succ n₁) is-cyclic₁) a b
= tr (λ f → ∑[ k ∶ Fin ℓ (n G↺) ]
((f ^ π₁ k) a ≡ b) × (∏[ k' ∶ Fin ℓ (n G↺) ] ((f ^ π₁ k') a ≡ b
→ k ≡ k')))
(suc-is-suc G G↺)
(cw-steps-in_from_to_ ℓ (Nodes-with-pred-is-cyclic G G↺) a b)
suc-edge
: {ℓ : Level}
(G : Graph ℓ)
(G↺ : CyclicGraph ℓ G)
→ _<_ ℓ 0 (n G↺)
→ (x : Node G) → Edge G x (suc-↺ G G↺ x)
suc-edge G G↺@(cyclic-graph φ₁ (succ n) is-cyclic₁) p x = coe q e
where
e : Edge G (pred-↺ G G↺ (suc-↺ G G↺ x)) (suc-↺ G G↺ x)
e = pred-edge G G↺ p (suc-↺ G G↺ x)
q : Edge G (pred-↺ G G↺ (suc-↺ G G↺ x)) (suc-↺ G G↺ x) ≡ Edge G x (suc-↺ G G↺ x)
q = ap (λ p' → Edge G p' (suc-↺ G G↺ x)) helper
where
helper : (pred-↺ G G↺ (suc-↺ G G↺ x)) ≡ x
helper = lrmap-inverse-h (π₁ (is-iso-to-≅ (φ G↺) (φ↺-is-iso G G↺))) x
module _ {ℓ : Level} {A : Graph ℓ}
where
module _ (A↺ : CyclicGraph ℓ A)
where
open Hom
open import foundations.Cyclic ℓ
module ge {G : Graph ℓ}(h : Hom A G)
where
pred-edge-from : (p : _<_ ℓ 0 (n A↺)) → (x : Node A) → Edge G (α h (pred-↺ A A↺ x)) (α h x)
pred-edge-from p x = β h (pred-↺ A A↺ x) x (pred-edge A A↺ p x)
suc-edge-from : (p : _<_ ℓ 0 (n A↺)) → (x : Node A) → Edge G (α h x) (α h (suc-↺ A A↺ x))
suc-edge-from p x = (β h) x (suc-↺ A A↺ x) (suc-edge A A↺ p x)
edge-in-star-with-pred : (p : _<_ ℓ 0 (n A↺)) → (x : Node A) → Star G (α h x)
edge-in-star-with-pred p x = α h (pred-↺ A A↺ x) , inr (pred-edge-from p x)
edge-after-suc-by-map : (p : _<_ ℓ 0 (n A↺)) → (x : Node A) → Map G → Star G (α h x)
edge-after-suc-by-map p x 𝕄
= CyclicSet.φ (𝕄 (α h x)) (α h (suc-↺ A A↺ x) , inl (suc-edge-from p x))
module _ {G : Graph ℓ} (h : Hom A (U G))
where
edge-in-star-with-pred : (p : _<_ ℓ 0 (n A↺)) → (x : Node A) → Star G (α h x)
edge-in-star-with-pred p x = α h (pred-↺ A A↺ x) , U-reverse-edge {G = G} e
where
e : Edge (U G) (α h (pred-↺ A A↺ x)) (α h x)
e = ge.pred-edge-from h p x
edge-after-suc-by-map : (p : _<_ ℓ 0 (n A↺)) → (x : Node A) → Map G → Star G (α h x)
edge-after-suc-by-map p x 𝕄 =
CyclicSet.φ (𝕄 (α h x)) (α h (suc-↺ A A↺ x) , ge.suc-edge-from h p x)
-- -- ```
(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