lib.graph-homomorphisms.Lemmas.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-homomorphisms.Lemmas
where
open import foundations.Core
open import lib.graph-definitions.Graph
open import lib.graph-homomorphisms.Hom
open Hom
open import lib.graph-relations.Isomorphic
using (_≅_ ; ≅-≃-iso ; hom-from-iso )
open import lib.graph-definitions.Graph.EquivalencePrinciple
module
Hom-Lemma-1
{ℓ : Level}
(A : Graph ℓ)
(B : Graph ℓ)
where
open EquivPrinciple A B public
hom-from-≡ : (A ≡ B) → Hom A B
hom-from-≡ eq = π₁ ((≅-≃-iso ∙) ((equiv-principle ∙) eq))
same-hom-from-≡-or-≅
: (iso : A ≅ B)
→ hom-from-≡ (≡-from-iso iso) ≡ hom-from-iso iso
same-hom-from-≡-or-≅ iso@(n , e) =
begin
hom-from-≡ (≡-from-iso iso)
≡⟨⟩
(π₁ ((≅-≃-iso {G = A}{H = B} ∙) ((equiv-principle ∙)
(((equiv-principle) ∙←) iso))))
≡⟨ ap (λ p → π₁ ((≅-≃-iso {G = A} {H = B} ∙) p))
(lrmap-inverse-h (equiv-principle) iso) ⟩
(π₁ ((≅-≃-iso {G = A} {H = B} ∙) iso))
≡⟨⟩
hom-from-iso iso
∎
∑-change-≡-≅'
: ∀ {G : Graph ℓ}
→ (f : Hom A G) (g : Hom B G)
→ (∑[ α ∶ A ≡ B ] (f ≡ (hom-from-≡ α ∘Hom g)))
≃ (∑[ α ∶ A ≅ B ] (f ≡ (hom-from-iso α ∘Hom g)))
∑-change-≡-≅' f g = sigma-maps-≃ (equiv-principle) λ {iso → idtoeqv (helper₃ iso) }
where
open import foundations.UnivalenceAxiom
aux-helper
: (iso : A ≡ B)
→ (hom-from-≡ iso)
≡ (hom-from-iso (equiv-principle ∙ $ iso))
aux-helper idp = idp
aux-helper₂ :
∀ (P : Hom A B → Type ℓ)
→ (f g : Hom A B)
→ (p : f ≡ g)
→ P f ≡ P g
aux-helper₂ P f g p = ap P p
helper₃ : (iso : A ≡ B) →
(f ≡ ((hom-from-≡ iso) ∘Hom g))
≡ (f ≡ ((hom-from-iso (equiv-principle ∙ $ iso)) ∘Hom g))
helper₃ iso = aux-helper₂ (λ h → f ≡ (h ∘Hom g)) _ _ (aux-helper iso)
∑-change-≡-≅''
: ∀ {G : Graph ℓ}
→ (f : Hom A G) (g : Hom B G)
→ (∑[ α ∶ A ≅ B ] (f ≡ (hom-from-iso α ∘Hom g)))
≃ (∑[ α ∶ A ≅ B ] (f ≡ (hom-from-≡ (≡-from-iso α) ∘Hom g)))
∑-change-≡-≅'' f g = sigma-preserves (λ iso → idtoeqv $ ap (λ h → f ≡ (h ∘Hom g)) (! same-hom-from-≡-or-≅ iso) )
where open import foundations.UnivalenceAxiom
∑-change-≡-≅
: ∀ {G : Graph ℓ}
→ (f : Hom A G) (g : Hom B G)
→ (∑[ α ∶ A ≡ B ] (f ≡ (hom-from-≡ α ∘Hom g)))
≃ (∑[ α ∶ A ≅ B ] (f ≡ (hom-from-≡ (≡-from-iso α) ∘Hom g)))
∑-change-≡-≅ f g = ≃-trans (∑-change-≡-≅' f g) (∑-change-≡-≅'' f g)
on-nodes-≡-on-nodes
: (iso : A ≅ B)
→ (π₁ iso ∙) ≡ Hom.α (hom-from-≡ (≡-from-iso iso))
on-nodes-≡-on-nodes iso@(n , e) =
begin
n ∙
≡⟨⟩
Hom.α (π₁ ((≅-≃-iso {G = A} {H = B} ∙) iso))
≡⟨ ap Hom.α (! same-hom-from-≡-or-≅ iso) ⟩
Hom.α (hom-from-≡ (≡-from-iso iso))
∎
on-nodes-≡-on-nodes-h
: (iso : A ≅ B)
→ (x : Node A)
→ (π₁ iso ∙) x ≡ Hom.α (hom-from-≡ (≡-from-iso iso)) x
on-nodes-≡-on-nodes-h iso x = happly (on-nodes-≡-on-nodes iso) x
where
open import foundations.FunExtAxiom
≡-of-homs-≃-≡-of-pairs
: (f g : Hom A B)
→ (f ≡ g) ≃ ((Hom.α f , Hom.β f) ≡ (Hom.α g , Hom.β g))
≡-of-homs-≃-≡-of-pairs f g =
qinv-≃ from-≡ (from-hom-pair , (λ { idp → idp}) , λ {idp → idp})
where
private
from-≡ = λ { idp → idp}
from-hom-pair = λ { idp → idp}
module
_
(f g : Hom A B)
where
open import foundations.FunExtAxiom
on-nodes-is-prop
: isProp (Hom.α f ≡ Hom.α g)
on-nodes-is-prop =
isProp-≃
(≃-sym eqFunExt)
(pi-is-prop (λ x → Node-is-set B _ _))
on-edges-is-prop
: (p : Hom.α f ≡ Hom.α g )
→ isProp ((tr (λ e → (x y : Node A)
→ Edge A x y → Edge B (e x) (e y))
p (Hom.β f) ≡ Hom.β g ))
on-edges-is-prop p = isProp-≃
(≃-sym eqFunExt) (pi-is-prop
(λ x → isProp-≃ (≃-sym eqFunExt)
(pi-is-prop (λ y → isProp-≃ (≃-sym eqFunExt)
(pi-is-prop (λ e → Edge-is-set B _ _ _ _))))))
∑-≡-of-homs-is-prop
: isProp (∑[ p ∶ Hom.α f ≡ Hom.α g ]
(tr (λ e → (x y : Node A)
→ Edge A x y → Edge B (e x) (e y))
p (Hom.β f) ≡ Hom.β g ))
∑-≡-of-homs-is-prop = ∑-prop on-nodes-is-prop on-edges-is-prop
≡-of-homs-≃-≡-∑
: (f ≡ g)
≃ (∑[ p ∶ Hom.α f ≡ Hom.α g ]
(tr (λ e → (x y : Node A) → Edge A x y → Edge B (e x) (e y))
p (Hom.β f)
≡ Hom.β g ))
≡-of-homs-≃-≡-∑ =
begin≃
(f ≡ g)
≃⟨ ≡-of-homs-≃-≡-of-pairs f g ⟩
(Hom.α f , Hom.β f) ≡ (Hom.α g , Hom.β g)
≃⟨ pair-≃-∑ ⟩
((∑[ p ∶ Hom.α f ≡ Hom.α g ]
(tr (λ e → (x y : Node A)
→ Edge A x y
→ Edge B (e x) (e y))
p (Hom.β f)
≡ Hom.β g )))
≃∎
≡-of-homs-to-triples
: (p : Hom.α f ≡ Hom.α g)
→ (tr (λ e → (x y : Node A)
→ Edge A x y
→ Edge B (e x) (e y))
p (Hom.β f)
≡ Hom.β g)
→ (x y : Node A) (e : Edge A x y)
→ Path {A = ∑[ x ] ∑[ y ] Edge B x y }
(α f x , α f y , Hom.β f x y e)
(α g x , α g y , Hom.β g x y e)
≡-of-homs-to-triples idp idp x y e = idp
module
Hom-Lemma-2
{ℓ : Level}
(A : Graph ℓ)
(B : Graph ℓ)
(C : Graph ℓ)
(f : Hom A C)
(g : Hom B C)
where
{-
A --α-→ B
\ /
f \ / g
\ /
C
-}
open Hom-Lemma-1 A B
g∘ : (α : A ≡ B) → Hom A C
g∘ α = (hom-from-≡ α ∘Hom g)
caℓ₁
: (∑[ α ∶ A ≡ B ]
(∑[ p ∶ Hom.α f ≡ Hom.α (g∘ α) ]
(tr (λ f → (x y : Node A)
→ Edge A x y
→ Edge C (f x) (f y)) p
(Hom.β f) ≡ Hom.β (g∘ α))))
≃ (∑[ iso ∶ A ≅ B ]
∑[ p ∶ α f ≡ α (g∘ (≡-from-iso iso)) ]
(tr (λ f → (x y : Node A) → Edge A x y → Edge C (f x) (f y)) p (β f)
≡ Hom.β (g∘ (≡-from-iso iso))))
caℓ₁ = sigma-preserves-≃ (≃-sym (equiv-principle))
D : ∑[ iso ∶ A ≅ B ] (α f ≡ α (g∘ (≡-from-iso iso)))
→ Type ℓ
D (iso , p) =
(tr (λ f → (x y : Node A) → Edge A x y → Edge C (f x) (f y)) p
(β f) ≡ Hom.β (g∘ (≡-from-iso iso)))
o : (iso : A ≅ B)
→ (α f ≡ (α g) ∘ (λ x → (((π₁ iso) ∙) x)))
≃ (α f ≡ α (g∘ (≡-from-iso iso)))
o iso =
idtoeqv
$ ap (α f ≡_) $ funext λ x →
begin
(α g ∘ (π₁ iso ∙)) x
≡⟨ ap (α g) (on-nodes-≡-on-nodes-h iso x) ⟩
α (g∘ (≡-from-iso iso)) x
∎ where
open import foundations.UnivalenceAxiom
open import foundations.FunExtAxiom
caℓ₂
: (∑[ iso ∶ A ≅ B ]
∑[ p ∶ α f ≡ α (g∘ (≡-from-iso iso)) ]
(D (iso , p)))
≃
(∑[ iso ∶ A ≅ B ]
∑[ p ∶ α f ≡ (α g) ∘ (λ x → (((π₁ iso) ∙) x)) ]
(D (iso , ((o iso ∙) p))))
caℓ₂ = sigma-preserves (λ iso → sigma-preserves-≃ (o iso))
D₃ : ∑[ iso ∶ A ≅ B ] (α f ≡ (α g) ∘ (λ x → (((π₁ iso) ∙) x)))
→ Type ℓ
D₃ (iso , p) = D (iso , ((o iso ∙) p))
caℓ₃
: (∑[ iso ∶ (∑[ α ∶ Node A ≃ Node B ]
((x y : Node A) → Edge A x y ≃ Edge B ((α ∙) x) ((α ∙) y))) ]
∑[ p ∶ α f ≡ (α g) ∘ (λ x → (((π₁ iso) ∙) x)) ]
D₃ (iso , p))
≃
(∑[ p ∶ (∑[ r ∶ Node A ≃ Node B ] (α f ≡ (α g) ∘ (λ x → (r ∙) x))) ]
∑[ q ∶ (((x y : Node A) → Edge A x y ≃ (Edge B (((π₁ p) ∙) x)
(((π₁ p) ∙) y)))) ]
let
iso : A ≅ B
iso = π₁ p , q
in
D₃ (iso , π₂ p))
caℓ₃ = ∑-comm₂
(Node A ≃ Node B)
((λ α → (x y : Node A) → Edge A x y ≃ Edge B ((α ∙) x) ((α ∙) y)))
(((λ α → Hom.α f ≡ (Hom.α g) ∘ (λ x → ((α ∙) x)) )))
_
-- cal4
-- : (∑[ α ∶ (A ≡ B) ]
-- (∑[ p ∶ ((Hom.α f) ≡ (Hom.α (g∘ α))) ]
-- ((tr (λ f → (x y : Node A)
-- → Edge A x y
-- → Edge C (f x) (f y)) p
-- (Hom.β f)) ≡ (Hom.β (g∘ α)))))
-- ≃ (∑[ p ∶ ((∑[ r ∶ Node A ≃ Node B ] (α f ≡ (α g) ∘ (λ x → (r ∙) x)))) ]
-- ∑[ q ∶ ((((x y : Node A) → Edge A x y ≃ (Edge B (((π₁ p) ∙) x) (((π₁ p) ∙) y))))) ]
-- let
-- iso : A ≅ B
-- iso = π₁ p , q
-- in
-- D₃ (iso , π₂ p))
-- cal4 = ≃-trans caℓ₁ (≃-trans caℓ₂ caℓ₃)
\end{document}
(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