lib.graph-walks.Walk.QuasiSimpleFinite

lib.graph-walks.Walk.QuasiSimpleFinite.md.

Version of Sunday, January 22, 2023, 10:42 PM

{-# OPTIONS --without-K --exact-split #-} module lib.graph-walks.Walk.QuasiSimpleFinite where open import foundations.Core open import foundations.Finite open import foundations.NaturalsType open import foundations.TypesofMorphisms open import lib.graph-definitions.Graph open import lib.graph-classes.FiniteGraph module _ {ℓ : Level }(G : Graph ℓ ) (G-is-finite : isFiniteGraph G ) where open import foundations.Nat ℓ open import foundations.Fin ℓ open import lib.graph-walks.Walk hiding (length ) open import lib.graph-walks.Walk.Composition open ∙-walk G open import lib.graph-walks.Walk.QuasiSimple open Graph open quasi-simple-walks {G = G } open ∈-walk G

Nodes-is-finite = isFiniteGraph.NodeDec G-is-finite Edges-is-finite = isFiniteGraph.EdgeDec G-is-finite _≟Node_ : (x y : Node G ) → (x ≡ y ) + (x ≠ y ) _≟Node_ = isFinite-→-isDec Nodes-is-finite open WR G (_≟Node_) Ng : ℕ Ng = cardinal (Node G ) Nodes-is-finite

equiv-fin-sigma-∈ : ∀ {x y } → (w : Walk G x y ) → (∑[ x ] (x ∈w w )) ≃ ⟦ length w ⟧ equiv-fin-sigma-∈ ⟨ x ⟩ = qinv-≃ (λ ()) (g , (λ { (zero , ()) ; (succ _ , ())}) , λ { ()}) where g : _ g (zero , ()) g (succ π₃ , ()) equiv-fin-sigma-∈ {x = x }{y } (e ⊙ w ) = begin≃ (∑[ y ] (y ∈w (e ⊙ w ))) ≃⟨ i ⟩ (∑[ y ] (y ≡ x )) + (∑[ y ] (y ∈w w ) ) ≃⟨ ii ⟩ (𝟙 ℓ ) + (∑[ y ] (y ∈w w )) ≃⟨ iii ⟩ (𝟙 ℓ ) + ⟦ length w ⟧ ≃⟨ iv ⟩ ⟦ succ (length w ) ⟧' ≃⟨ v ⟩ ⟦ succ (length w ) ⟧ ≃∎ where IH : (∑[ y ] (y ∈w w )) ≃ ⟦ length w ⟧ IH = equiv-fin-sigma-∈ w i = ∑-+-≃-+-∑ ii = equiv-+-fixed-right (contr-≃-𝟙 (pathto-is-contr _ _ )) iii = equiv-+-fixed-left IH iv = equiv-+-fixed-left (Fin₁≃Fin₂ _) v = ≃-sym (Fin₁≃Fin₂ _)

proj-node-is-inj-when-w-is-quasi-simple : ∀ {x y } (w : Walk G x y ) → w is-quasi-simple → (proj-node w ) is-injective proj-node-is-inj-when-w-is-quasi-simple w w-s idp = pair= (idp , w-s _ _ _)

finite-quasi-simple-walks-type : ℕ → Node G → Node G → Type ℓ finite-quasi-simple-walks-type n x y = ∑[ w ∶ Walk G x y ] (w is-quasi-simple ) × (length w ≡ n ) finite-quasi-simple-walks-type-is-set : ∀ (n : ℕ ) → ∀ x y → isSet (finite-quasi-simple-walks-type n x y ) finite-quasi-simple-walks-type-is-set n x y = ∑-set (Walk-is-set G ) λ w → ∑-set (prop-is-set (being-quasi-simple-is-prop w )) λ w-s → prop-is-set (ℕ-is-set _ _) where open import lib.graph-walks.Walk.isSet

qswalk-equiv-sigmas : ∀ {x y } → ∀ n → (∑[ w ∶ Walk G x y ] (w is-quasi-simple ) × (length w ≡ succ n )) ≃ (∑[ x' ] (∑[ e ∶ Edge G x x' ] ∑[ IH ∶ (∑[ w' ∶ Walk G x' y ] (w' is-quasi-simple ) × (length w' ≡ n )) ] (¬ (x ∈w (proj₁ IH ))))) qswalk-equiv-sigmas {x = x }{y } n = qinv-≃ f (g , h1 , h2 ) where f : _ f ((e ⊙ w') , w-s , idp ) = (_ , e , (w' , conservation e w' w-s , idp ) , λ x∈w' → get-⊥ x∈w' (x-in-different-pos x∈w')) where x-in-different-pos : (x∈w' : x ∈w w') → inr x∈w' ≡ inl idp x-in-different-pos x∈w' = w-s x (inr x∈w') (inl idp ) get-⊥ : (x∈w' : x ∈w w') → inr x∈w' ≡ inl idp → ⊥ ℓ get-⊥ x∈w' () g : _ g (x' , e , (w' , w'-s , idp ) , x∌ ) = ((e ⊙ w') , ⊙-quasi-simple-is-quasi-simple {e = e } w'-s x∌ , idp ) h1 : _ h1 (x' , e , (w' , w'-s , idp ) , x'∌ ) = pair= (idp , pair= (idp , pair= (pair= (idp , pair= ((being-quasi-simple-is-prop w' _ _ , ℕ-is-set _ _ _ _))) , pi-is-prop (λ _ → ⊥-is-prop ) _ _))) h2 : _ h2 ((e ⊙ w') , w-s , idp ) = pair= (idp , pair= (being-quasi-simple-is-prop (e ⊙ w') _ _ , ℕ-is-set _ _ _ _))

∑∈-is-finite : ∀ {x y } → (w : Walk G x y ) -- → w is-quasi-simple → (∑[ x ] (x ∈w w )) is-finite ∑∈-is-finite w = equiv-preserves-finiteness (≃-sym (equiv-fin-sigma-∈ w )) Fin-is-finite

cardinal-∑∈-is-length : ∀ {x y } → (w : Walk G x y ) → (cardinal (∑[ x ] (x ∈w w )) (∑∈-is-finite w )) ≡ length w cardinal-∑∈-is-length w = same-cardinal (equiv-fin-sigma-∈ w ) (∑∈-is-finite w ) Fin-is-finite

module finiteness-lemmas -- The following are well-known lemmas about finite types. (+-finite : ∀ {A B : Type ℓ } → isFinite A → isFinite B → isFinite (A + B )) (∏-finite : ∀ {ℓ₁ ℓ₂ } {A : Type ℓ₁ } {B : A → Type ℓ₂ } → isFinite A → ((a : A ) → isFinite (B a )) → isFinite (∏ A B )) (∑-finite : ∀ {ℓ₁ ℓ₂ } {A : Type ℓ₁ } {B : A → Type ℓ₂ } → isFinite A → ((a : A ) → isFinite (B a )) → isFinite (∑ A B )) (injection-gives-≤-cardinals : ∀ {ℓ₁ ℓ₂ } {A : Type ℓ₁ } {B : Type ℓ₂ } → (f : A → B ) → (fin-A : A is-finite ) → (fin-B : B is-finite ) → f is-injective → _≤_ (cardinal A fin-A ) (cardinal B fin-B )) where ∈w-is-finite : ∀ {x y z } → (w : Walk G x y ) → (z ∈w w ) is-finite ∈w-is-finite ⟨ _ ⟩ = 𝟘-is-finite ∈w-is-finite (x ⊙ w ) = +-finite (decidable-→-≡-is-finite _≟Node_ _ _) (∈w-is-finite w )

qswalks-has-bounded-length : ∀ {x y } → (w : Walk G x y ) → w is-quasi-simple → length w < succ Ng qswalks-has-bounded-length ⟨ x ⟩ w-s = ∗ qswalks-has-bounded-length w @(e ⊙ w') w-s = ≤-to-< (tr (λ o → o ≤ Ng ) (cardinal-∑∈-is-length w ) is-≤) where is-≤ : (cardinal (∑[ x ] (x ∈w w )) (∑∈-is-finite w )) ≤ Ng is-≤ = injection-gives-≤-cardinals (proj-node w ) (∑∈-is-finite w ) Nodes-is-finite (proj-node-is-inj-when-w-is-quasi-simple w w-s )

quasi-quasi-simple-equiv-qswalk : ∀ x y → (∑[ w ∶ Walk G x y ] (w is-quasi-simple )) ≃ (∑[ (n , _) ∶ ⟦ succ Ng ⟧ ] (finite-quasi-simple-walks-type n x y )) quasi-quasi-simple-equiv-qswalk x y = qinv-≃ f (g , helper , λ { (w , w-s ) → idp }) where f : _ f (w , w-s ) = (length w , len<) , w , w-s , idp where len< : length w < succ Ng len< = qswalks-has-bounded-length w w-s g : _ g (_ , w , w-s , idp ) = w , w-s helper : (f ∘ g ) ∼ id helper ((n , n<) , w , w-s , idp ) rewrite <-prop {n = succ Ng }{m = length w } (proj₂ (proj₁ (f (w , w-s )))) n< = idp

finite-qswalks : ∀ (n : ℕ ) → (x y : Node G ) → isFinite (finite-quasi-simple-walks-type n x y ) finite-qswalks zero x y = equiv-preserves-finiteness (≃-sym (calc x y )) (decidable-→-≡-is-finite _≟Node_ _ _) where -- All walks with length 0 are trivial quasi-simple walk. calc : ∀ x y → (∑[ w ∶ Walk G x y ] (w is-quasi-simple ) × (length w ≡ 0 )) ≃ (x ≡ y ) calc x y with x ≟Node y ... | inr x≠y = qinv-≃ f ((λ x≡y → ⊥-elim (x≠y x≡y )) , (λ {p → Node-is-set G _ _ _ _}) , λ {p → ⊥-elim (x≠y (f p ))}) where f : _ f (w , _ , p ) with length≡0-is-trivial w p ... | idp , idp = ⊥-elim (x≠y idp ) ... | inl idp = qinv-≃ (λ _ → idp ) (g , (λ {p → Node-is-set G _ _ _ _}) , h ) where g : _ g _ = ⟨ x ⟩ , one-point-walk-is-quasi-simple x , idp h : _ h t @(w , _ , p ) with length≡0-is-trivial w p ... | o , q rewrite Node-is-set G x x o idp = pair= (((! q ) , pair= ((being-quasi-simple-is-prop w _ _ , ℕ-is-set _ _ _ _)))) finite-qswalks (succ n ) x y = equiv-preserves-finiteness (≃-sym (qswalk-equiv-sigmas n )) $ ∑-finite Nodes-is-finite λ x' → ∑-finite (Edges-is-finite x x') λ _ → ∑-finite (finite-qswalks n x' y ) λ _ → ∏-finite (∈w-is-finite _) λ _ → 𝟘-is-finite

sigma-qswalks-forms-finite-set : ∀ (n : ℕ ) → (∑[ x ] ∑[ y ] ∑[ m ∶ ⟦ succ n ⟧ ] (finite-quasi-simple-walks-type n x y )) is-finite sigma-qswalks-forms-finite-set n = ∑-finite Nodes-is-finite λ x → ∑-finite Nodes-is-finite λ y → ∑-finite Fin-is-finite (λ m → finite-qswalks n x y ) finite-graph-has-finite-quasi-simple-walks : (∑[ x ] ∑[ y ] ∑[ w ∶ Walk G x y ] (w is-quasi-simple )) is-finite finite-graph-has-finite-quasi-simple-walks = ∑-finite Nodes-is-finite λ x → ∑-finite Nodes-is-finite λ y → equiv-preserves-finiteness (≃-sym (quasi-quasi-simple-equiv-qswalk x y )) (∑-finite Fin-is-finite λ {(n , n<Ng ) → finite-qswalks n x y } )

Latest changes

(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