Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}

module lib.graph-families.CycleGraph.Isomorphisms.Lemmas
  where
  open import foundations.Core
  module
    _
    (ℓ : Level)
    where


    open import lib.graph-definitions.Graph
    open Graph

    open import lib.graph-homomorphisms.Hom
    open Hom
    open import lib.graph-relations.Isomorphic

    open import lib.graph-families.CycleGraph.Isomorphisms.IdentityType
    open import lib.graph-definitions.Graph.EquivalencePrinciple

    open import foundations.FunExtAxiom
    open import foundations.UnivalenceAxiom

    open import foundations.Fin ℓ
    open import foundations.Nat ℓ
    open import foundations.Cyclic ℓ

    open import lib.graph-families.CycleGraph.RotHom ℓ
    open import lib.graph-families.CycleGraph ℓ

    order-of-an-iso
      :  (n : ℕ) (n>0 : ℕ-ordering._>_ ℓ n ) → (φ : Cycle n ≅ Cycle n)
      → ∑[ (k , _) ∶ ⟦ n ⟧ ] ((rot n ^-hom k) ≡ hom-from-iso φ)

    order-of-an-iso zero ()
    order-of-an-iso n@(succ _) ∗ φ = ((Isos-→-Fin ℓ n ∗) φ) ,
      (begin
        (rot n ^-hom π₁ (((Isos-→-Fin ℓ n ∗) φ)))
        ≡⟨⟩
        hom-from-iso ((Fin-→-Isos ℓ n  ∗ ) (((Isos-→-Fin ℓ n ∗) φ)))
        ≡⟨ ap hom-from-iso (rlmap-inverse-h (Isos-≃-Fin ℓ n ∗ ) φ) ⟩
        hom-from-iso φ
      ∎)

    open import lib.graph-homomorphisms.Lemmas
    module _ (n : ℕ) (n>0 : n > )
      where
      hom-from-≡ = Hom-Lemma-1.hom-from-≡ (Cycle n) (Cycle n)
      ≡-from-iso = Hom-Lemma-1.≡-from-iso (Cycle n) (Cycle n)
      same-hom-from-≡-or-≅ = Hom-Lemma-1.same-hom-from-≡-or-≅ (Cycle n) (Cycle n)

    rot^k-from-iso
     : (n : ℕ) (n>0 : n > )
     → (φ : Cycle n ≅ Cycle n) (G : Graph ℓ)(f g : Hom (Cycle n) G)
     → let k = π₁ (((Isos-≃-Fin ℓ n n>0 ∙) φ))
      in
        (f ≡ ( ((hom-from-≡ n n>0) (≡-from-iso n n>0 φ)) ∘Hom g))
      ≡ (f ≡ ((rot n ^-hom k) ∘Hom g))

    rot^k-from-iso zero () φ G f g
    rot^k-from-iso n@(succ _) ∗ φ G f g
      = ap (λ w → f ≡ (w ∘Hom g))
           ((same-hom-from-≡-or-≅ n ∗ φ) · ! π₂ (order-of-an-iso n ∗ φ))

    m₁
     : (n : ℕ) (n>0 : n > ) (G : Graph ℓ)(f g : Hom (Cycle n) G)
     → (∑[ α ∶ Cycle n ≅ Cycle n ]
        (f ≡ (((hom-from-≡ n n>0) ((≡-from-iso n n>0) α)) ∘Hom g)))
        ≃ (∑[ (k , _ ) ∶  ⟦ n ⟧ ]  (f ≡ ((rot n ^-hom k) ∘Hom g)))

    m₁ zero ()
    m₁ n@(succ _) ∗ G f g = sigma-maps-≃ (Isos-≃-Fin ℓ n ∗ ) $ λ φ →
        idtoeqv (rot^k-from-iso n ∗ φ G f g)
        where open import foundations.UnivalenceAxiom

    abstract
      L1-hom
        : (n : ℕ) (n>0 : n > ) { k₁ k₂ : ⟦ n ⟧}
        → ((x y : Node (Cycle n))
        → (e : Edge (Cycle n) x y)
        → let
          h₁ = rot n ^-hom (π₁ k₁)
          h₂ = rot n ^-hom (π₁ k₂)
          in
          Path {A = ∑[ x ] ∑[ y ] Edge (Cycle n) x y}
            (α h₁ x , α h₁ y , β h₁ x y e)
            (α h₂ x , α h₂ y , β h₂ x y e))
        → k₁ ≡ k₂

      L1-hom zero ()
      L1-hom n@(succ m) ∗ {k₁ = k₁}{k₂} f 
        = fin-exp-is-unique k₁ k₂ (fin-pred (0' ℓ m)) eq₁
        where
        open Sigma
        
        h₁ h₂ : Hom (Cycle n) (Cycle n)
        h₁ = rot n ^-hom (π₁ k₁)
        h₂ = rot n ^-hom (π₁ k₂)

        eq₁ : (fin-pred {k = n} ^ π₁ k₁) (m , <-succ m) ≡ (fin-pred ^ π₁ k₂) (m , <-succ m)
        eq₁ = 
          (fin-pred ^ (π₁ k₁)) (m , <-succ m)
            ≡⟨ happly (lemma-on-nodes-hom-expo (rot n) (π₁ k₁)) (m , <-succ m) ⟩ 
          (α h₁ (m , <-succ m) )
            ≡⟨ π₁ (Σ-componentwise (f (m , <-succ m) (0' ℓ _) idp)) ⟩ 
          (α h₂ (m , <-succ m)) -- (fin-pred (0' ℓ _))
            ≡⟨ ! happly (lemma-on-nodes-hom-expo (rot n) (π₁ k₂)) ((fin-pred (0' ℓ _))) ⟩ 
          (fin-pred ^ π₁ k₂) _
          ∎
          where
          open import foundations.FunExtAxiom

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