Skip to content

Commit 6a3aa91

Browse files
phijorphijor
committed
Develop hGroups in their own submodule
1 parent 4be0b04 commit 6a3aa91

File tree

12 files changed

+1755
-759
lines changed

12 files changed

+1755
-759
lines changed

‎GpdCont/HomotopyGroup/Action.agda‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
module GpdCont.HomotopyGroup.Action where
2+
3+
open import GpdCont.Prelude
4+
open import GpdCont.Connectivity
5+
open import GpdCont.Embedding
6+
open import GpdCont.HomotopySet
7+
import GpdCont.SetTruncation as ST
8+
9+
open import GpdCont.HomotopyGroup.Base
10+
11+
open import Cubical.Foundations.Equiv
12+
open import Cubical.Foundations.HLevels
13+
open import Cubical.Data.Sigma
14+
open import Cubical.HITs.PropositionalTruncation as PT using (∥_∥₁)
15+
16+
17+
private
18+
variable
19+
ℓ ℓX ℓY : Level
20+
21+
hAction : (ℓX : Level) → hGroup ℓ → Type _
22+
hAction ℓX G = ⟨ G ⟩ᵗ → hSet ℓX
23+
24+
isFaithful : (G : hGroup ℓ) (X : hAction ℓX G) → Type _
25+
isFaithful G X = isOfHLevelFun 2 X
26+
27+
isPropIsFaithful : (G : hGroup ℓ) (X : hAction ℓX G) → isProp (isFaithful G X)
28+
isPropIsFaithful G X = isPropΠ λ _ → isPropIsSet
29+
30+
Pr' : (G : hGroup ℓ) → ⟨ G ⟩ᵗ → hAction ℓ G
31+
Pr' G g₀ g .fst = g₀ ≡ g
32+
Pr' G g₀ g .snd = hGroup.is-groupoid G g₀ g
33+
34+
Pr : (G : hGroup ℓ) → hAction ℓ G
35+
Pr G = Pr' G $ hGroup.pt₀ G
36+
37+
Pr* : (G : hGroup ℓ) → ⟨ G ⟩ᵗ → Σ[ X ∈ hAction ℓ G ] ∥ Pr G ≡ X ∥₁
38+
Pr* G g₀ .fst = Pr' G g₀
39+
Pr* G g₀ .snd = PT.map (λ p → funExt λ g → hSet≡ (cong (_≡ g) p)) (hGroup.mere-path G g₀)
40+
41+
-- Pr⁻ : (G : hGroup ℓ) → Σ[ X ∈ hAction ℓ G ] ∥ Pr G ≡ X ∥₁ → ⟨ G ⟩ᵗ
42+
-- Pr⁻ G = uncurry λ X → PT.rec→Gpd {! !} (λ h → {! h ≡$ hGroup.pt₀ G !}) (record { link = {! !} ; coh₁ = {! !} })
43+
44+
-- yonedaPr≃ : (G : hGroup ℓ) (g h : ⟨ G ⟩ᵗ) → (g ≡ h) ≃ (Pr* G g ≡ Pr* G h)
45+
-- yonedaPr≃ G g h = {! !}
46+
-- -- (g ≡ h) ≃⟨ {! !} ⟩
47+
-- -- ((G.pt₀ ≡ g) ≡ (G.pt₀ ≡ h)) ≃⟨ hSet≡Equiv ⟩
48+
-- -- (Pr G g ≡ Pr G h) ≃∎
49+
-- -- where module G = hGroup G
50+
51+
52+
-- yonedaPr : (G : hGroup ℓ) (g h : ⟨ G ⟩ᵗ) → isEquiv (λ (p : g ≡ h) → cong (Pr* G) p)
53+
-- yonedaPr G g h = isoToIsEquiv λ where
54+
-- .Iso.fun → _
55+
-- .Iso.inv x → {! cong (fst) x !}
56+
-- .Iso.leftInv → {! !}
57+
-- .Iso.rightInv → {! !}
58+
59+
-- ???
60+
isFaithfulPr : (G : hGroup ℓ) → isFaithful G (Pr G)
61+
isFaithfulPr G = ST.isEmbeddingCong→hasSetFibers (Pr G) λ g h → injEmbedding (isOfHLevelPath' 2 isGroupoidHSet _ _) (Pr⁻ g h _ _) where
62+
module G = hGroup G
63+
Pr⁻ : (g h : ⟨ G ⟩ᵗ) → (p q : g ≡ h) → cong (Pr G) p ≡ cong (Pr G) q → p ≡ q
64+
Pr⁻ g h p q sq = {! !} where
65+
sq' : Square (λ i → G.pt₀ ≡ p i) (λ i → G.pt₀ ≡ q i) refl refl
66+
sq' i j = ⟨ sq i j ⟩
67+
-- isOfHLevelFunOfImage→isOfHLevelFun 1 _ (G.elimProp {! !} goal) where
68+
-- module G = hGroup G
69+
-- foo : (fiber (Pr G) (Pr G G.pt₀)) ≃ {! !}
70+
-- foo =
71+
-- (fiber (Pr G) (Pr G G.pt₀)) ≃⟨ {! !} ⟩
72+
-- Σ[ g ∈ ⟨ G ⟩ᵗ ] (Pr G g) ≡ (Pr G G.pt₀) ≃⟨ {! !} ⟩
73+
-- Σ[ g ∈ ⟨ G ⟩ᵗ ] (G.pt₀ ≡ g) ≡ (G.pt₀ ≡ G.pt₀) ≃⟨ {! !} {- Yoneda? -} ⟩
74+
-- Σ[ g ∈ ⟨ G ⟩ᵗ ] g ≡ G.pt₀ ≃⟨ {! !} ⟩
75+
-- singl G.pt₀ ≃∎
76+
77+
-- goal : (x y : fiber (Pr G) (Pr G G.pt₀)) → isProp (x ≡ y)
78+
-- goal = {! !}
79+
80+
∫ : (G : hGroup ℓ) (X : hAction ℓX G) → hGroupoid (ℓ-max ℓ ℓX)
81+
∫ G X .fst = Σ[ g ∈ ⟨ G ⟩ᵗ ] ⟨ X g ⟩
82+
∫ G X .snd = isGroupoidΣ (hGroup.is-groupoid G) λ g → isSet→isGroupoid $ str $ X g
83+
84+
isTransitive : (G : hGroup ℓ) (X : hAction ℓX G) → Type _
85+
isTransitive G X = isPathConnected ⟨ ∫ G X ⟩
86+
87+
isPropIsTransitive : (G : hGroup ℓ) (X : hAction ℓX G) → isProp (isTransitive G X)
88+
isPropIsTransitive G X = isPropIsPathConnected _
89+
90+
precompAction : ∀ {ℓ′} (G : hGroup ℓ) (X : hAction ℓX G) (Y : hSet ℓ′) → hAction (ℓ-max ℓX ℓ′) G
91+
precompAction G X Y = λ g → X g →Set Y
92+
93+
precompAction∫ : ∀ {ℓ′} (G : hGroup ℓ) (X : hAction ℓX G) (Y : hSet ℓ′)
94+
→ ⟨ ∫ G (precompAction G X Y) ⟩ ≃ {! !}
95+
precompAction∫ G X Y =
96+
Σ[ g ∈ ⟨ G ⟩ᵗ ] (⟨ X g ⟩ → ⟨ Y ⟩) ≃⟨ {! !} ⟩
97+
{! !} ≃∎
98+
99+
module _ (G : hGroup ℓ) (X : hAction ℓX G) (Y : hAction ℓY G) where
100+
private module G = hGroup G
101+
102+
hActionHom : Type _
103+
hActionHom = ∀ g → ⟨ X g ⟩ → ⟨ Y g ⟩
104+
105+
ev : {g : ⟨ G ⟩ᵗ} (x : ⟨ X g ⟩) → hActionHom → ⟨ Y g ⟩
106+
ev {g} x f = f g x
107+
108+
isTransitive→isEmbeddingEv : isTransitive G X → ∀ {g₀ : ⟨ G ⟩ᵗ} (x₀ : ⟨ X g₀ ⟩) → isOfHLevelFun 1 (ev x₀)
109+
isTransitive→isEmbeddingEv is-transitive-X {g₀} x₀ y (f₀ , p₀) (f₁ , p₁) = goal where
110+
p : f₀ g₀ x₀ ≡ f₁ g₀ x₀
111+
p = p₀ ∙ sym p₁
112+
113+
-- Assuming some path from (g₀ , x₀) to (g , x) exists, we can equate f₀ and f₁:
114+
path-ext-conn : ∀ g x
115+
→ (pᵍ : g₀ ≡ g)
116+
→ (pˣ : PathP (λ i → ⟨ X (pᵍ i) ⟩) x₀ x)
117+
→ f₀ g x ≡ f₁ g x
118+
path-ext-conn g x pᵍ pˣ = goal where
119+
-- Substituting under f₀ and f₁, we get paths in Y over pᵍ:
120+
p₀′ : PathP (λ i → ⟨ Y (pᵍ i) ⟩) (f₀ g₀ x₀) (f₀ g x)
121+
p₀′ = cong₂ f₀ pᵍ pˣ
122+
p₁′ : PathP (λ i → ⟨ Y (pᵍ i) ⟩) (f₁ g₀ x₀) (f₁ g x)
123+
p₁′ = cong₂ f₁ pᵍ pˣ
124+
125+
-- We compose (p : f₀ g₀ x₀ ≡ f₁ g₀ x₀) on either side with the ajusted paths from above,
126+
-- over the identification (pᵍ : g₀ ≡ g). This gives us the desired (non-dependent)
127+
-- path from (f₀ g x) to (f₁ g x).
128+
goal : PathP (λ _ → ⟨ Y g ⟩) (f₀ g x) (f₁ g x)
129+
goal = doubleCompPathP (λ i _ → ⟨ Y (pᵍ i) ⟩) p₀′ p p₁′
130+
131+
-- Since X is transitive (= ∫ G X is connected), there merely exists a path (g₀ , x₀) ≡ (g , x)
132+
-- for any g, x. The goal is a proposition, so we can apply [path-ext-conn] from above:
133+
path-ext : ∀ g x → f₀ g x ≡ f₁ g x
134+
path-ext g x = PT.rec (str (Y g) _ _)
135+
(λ ∫-path → path-ext-conn g x (cong fst ∫-path) (cong snd ∫-path))
136+
(isPathConnected→merePath is-transitive-X (g₀ , x₀) (g , x))
137+
138+
path : f₀ ≡ f₁
139+
path i g x = path-ext g x i
140+
141+
goal : Path (fiber (ev x₀) y) (f₀ , p₀) (f₁ , p₁)
142+
goal = Σ≡Prop (λ f → str (Y g₀) _ _) path

‎GpdCont/HomotopyGroup/Aut.agda‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
module GpdCont.HomotopyGroup.Aut where
2+
3+
open import GpdCont.HomotopyGroup.Base
4+
open import GpdCont.HomotopyGroup.Equiv
5+
6+
open import GpdCont.Prelude
7+
open import GpdCont.Connectivity
8+
open import GpdCont.Embedding
9+
open import GpdCont.SetTruncation as ST using (isConnected-fiber-∣-∣₂)
10+
11+
open import Cubical.Foundations.Equiv
12+
open import Cubical.Foundations.Equiv.Properties using (congEquiv)
13+
open import Cubical.Foundations.HLevels
14+
open import Cubical.Foundations.Pointed.Base as Pointed using (Pointed)
15+
open import Cubical.Data.Sigma
16+
open import Cubical.HITs.SetTruncation as ST using (∥_∥₂ ; ∣_∣₂)
17+
open import Cubical.HITs.PropositionalTruncation as PT using (∥_∥₁)
18+
19+
private
20+
variable
21+
ℓ ℓ′ : Level
22+
23+
Aut : (A : hGroupoid ℓ) (a₀ : ⟨ A ⟩) → hGroup _
24+
Aut (A , is-groupoid-A) a₀ = pointedConnectedGroupoid→hGroup G g₀ conn-G is-groupoid-G where
25+
G : Type _
26+
G = fiber ∣_∣₂ ∣ a₀ ∣₂
27+
28+
g₀ : G
29+
g₀ .fst = a₀
30+
g₀ .snd = refl′ ∣ a₀ ∣₂
31+
32+
conn-G : isPathConnected G
33+
conn-G = isConnected-fiber-∣-∣₂ ∣ a₀ ∣₂
34+
35+
is-groupoid-G : isGroupoid G
36+
is-groupoid-G = isGroupoidΣ is-groupoid-A λ a → isProp→isOfHLevelSuc 2 (ST.isSetSetTrunc ∣ a ∣₂ ∣ a₀ ∣₂)
37+
38+
module _ (A : hGroupoid ℓ) (a₀ : ⟨ A ⟩) where
39+
AutEmbedding : ⟨ Aut A a₀ ⟩ᵗ ↪ ⟨ A ⟩
40+
AutEmbedding = EmbeddingΣProp λ a → ST.isSetSetTrunc ∣ a ∣₂ ∣ a₀ ∣₂
41+
42+
AutPathEquiv : ∀ (x y : ⟨ Aut A a₀ ⟩ᵗ) → (x ≡ y) ≃ Path ⟨ A ⟩ (x .fst) (y .fst)
43+
AutPathEquiv x y .fst = cong fst
44+
AutPathEquiv x y .snd = AutEmbedding .snd x y
45+
46+
AutPath : {x y : ⟨ Aut A a₀ ⟩ᵗ} → Path ⟨ A ⟩ (x .fst) (y .fst) → (x ≡ y)
47+
AutPath = invEq (AutPathEquiv _ _)
48+
49+
Aut∙ : (A : Pointed ℓ) → isGroupoid ⟨ A ⟩ → hGroup _
50+
Aut∙ (A , a₀) is-groupoid-A = Aut (A , is-groupoid-A) a₀
51+
52+
Sym : (X : hSet ℓ) → hGroup (ℓ-suc ℓ)
53+
Sym X = Aut (hSet _ , isGroupoidHSet) X
54+
55+
isContrAut : (A : hGroupoid ℓ) (a₀ : ⟨ A ⟩)
56+
→ isContr ⟨ A ⟩
57+
→ isContr ⟨ Aut A a₀ ⟩ᵗ
58+
isContrAut (A , _) a₀ is-contr-A = isContrΣ
59+
is-contr-A
60+
λ a → isContr→isContrPath (ST.isContr→isContrSetTrunc is-contr-A) ∣ a ∣₂ ∣ a₀ ∣₂
61+
62+
AutEquiv : (A : hGroupoid ℓ) {a₀ : ⟨ A ⟩} (B : hGroupoid ℓ′) {b₀ : ⟨ B ⟩}
63+
→ (e : ⟨ A ⟩ ≃ ⟨ B ⟩)
64+
→ (pres-pt : equivFun e a₀ ≡ b₀)
65+
→ hGroupEquiv (Aut A a₀) (Aut B b₀)
66+
AutEquiv A {a₀} B {b₀} e pres-pt = mkHGroupEquiv (Aut A _) (Aut B _) aut-equiv pres-pt-aut where
67+
hey : ∀ a → ∣ a ∣₂ ≡ ∣ a₀ ∣₂ → ∣ equivFun e a ∣₂ ≡ ∣ b₀ ∣₂
68+
hey a p = ST.merePath→pathSetTrunc $ PT.map (λ a≡a₀ → cong (equivFun e) a≡a₀ ∙ pres-pt) (ST.pathSetTrunc→merePath p)
69+
70+
hoo : ∀ a → ∣ equivFun e a ∣₂ ≡ ∣ b₀ ∣₂ → ∣ a ∣₂ ≡ ∣ a₀ ∣₂
71+
hoo a p = ST.merePath→pathSetTrunc $ PT.map (λ ea≡b₀ → invEq (congEquiv e) (ea≡b₀ ∙ sym pres-pt)) (ST.pathSetTrunc→merePath p)
72+
73+
aut-equiv : ⟨ Aut A _ ⟩ᵗ ≃ ⟨ Aut B _ ⟩ᵗ
74+
aut-equiv = Σ-cong-equiv e λ a → propBiimpl→Equiv (ST.isSetSetTrunc _ _) (ST.isSetSetTrunc _ _) (hey a) (hoo a)
75+
76+
pres-pt-aut : equivFun aut-equiv (a₀ , refl) ≡ (b₀ , refl)
77+
pres-pt-aut = Σ≡Prop (λ _ → ST.isSetSetTrunc _ _) pres-pt

‎GpdCont/HomotopyGroup/Base.agda‎

Lines changed: 137 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,137 @@
1+
module GpdCont.HomotopyGroup.Base where
2+
3+
open import GpdCont.Prelude
4+
open import GpdCont.Connectivity
5+
6+
open import GpdCont.StrictGroupoid.Base renaming (elimProp to elimProp')
7+
8+
open import Cubical.Foundations.HLevels
9+
open import Cubical.Foundations.Equiv
10+
open import Cubical.Foundations.Pointed.Base as Pointed using (Pointed)
11+
open import Cubical.Data.Sigma
12+
open import Cubical.HITs.SetTruncation as ST using (∥_∥₂ ; ∣_∣₂)
13+
open import Cubical.HITs.PropositionalTruncation as PT using (∥_∥₁)
14+
15+
private
16+
variable
17+
ℓ : Level
18+
19+
isHGroup : StrictGroupoid ℓ → Type ℓ
20+
isHGroup G = isPathConnected ⟨ G ⟩
21+
22+
isPropIsHGroup : (G : StrictGroupoid ℓ) → isProp (isHGroup G)
23+
isPropIsHGroup G = isPropIsPathConnected ⟨ G ⟩
24+
25+
hGroup : (ℓ : Level) → Type (ℓ-suc ℓ)
26+
hGroup ℓ = Σ[ G ∈ StrictGroupoid ℓ ] isHGroup G
27+
28+
⟨_⟩ᵗ : hGroup ℓ → Type ℓ
29+
⟨ (G , _) , _ ⟩ᵗ = G
30+
-- {-# INJECTIVE_FOR_INFERENCE ⟨_⟩ᵗ #-}
31+
32+
module hGroup (G : hGroup ℓ) where
33+
open StrictGroupoidStr (str (G .fst)) public
34+
35+
Tr : Type _
36+
Tr = ∥ ⟨ G .fst ⟩ ∥₂
37+
38+
is-connected : isPathConnected ⟨ G .fst ⟩
39+
is-connected = G .snd
40+
41+
center : Tr
42+
center = is-connected .fst
43+
44+
centerElimEquiv : ∀ {ℓB} {B : Tr → Type ℓB}
45+
→ B center ≃ (∀ x → B x)
46+
centerElimEquiv {B} = invEquiv (Π-contractDom is-connected)
47+
48+
centerElim : ∀ {ℓB} {B : ∥ ⟨ G .fst ⟩ ∥₂ → Type ℓB}
49+
→ B center
50+
→ ∀ x → B x
51+
centerElim = equivFun centerElimEquiv
52+
53+
pt₀ : ⟨ G .fst ⟩
54+
pt₀ = pt center
55+
56+
asPointed : Pointed ℓ
57+
asPointed .fst = ⟨ G .fst ⟩
58+
asPointed .snd = pt₀
59+
60+
asGroupoid : hGroupoid ℓ
61+
asGroupoid .fst = ⟨ G . fst ⟩
62+
asGroupoid .snd = is-groupoid
63+
64+
mere-path : ∀ g → ∥ pt₀ ≡ g ∥₁
65+
mere-path g = isPathConnected→merePath is-connected pt₀ g
66+
67+
elimProp : ∀ {ℓP} {P : ⟨ G ⟩ᵗ → Type ℓP}
68+
→ (∀ g → isProp (P g))
69+
→ (P pt₀)
70+
→ ∀ g → P g
71+
elimProp {P} is-prop-P p₀ = elimProp' (G .fst) is-prop-P p* where
72+
-- G has a unique connected component,
73+
-- so the domain of this map is contractible:
74+
p* : (x : ∥ ⟨ G .fst ⟩ ∥₂) → P (pt x)
75+
p* = Π-contractDomIso is-connected .Iso.inv p₀
76+
77+
elimPropᵝ : ∀ {ℓP} {P : ⟨ G ⟩ᵗ → Type ℓP}
78+
→ (is-prop-P : ∀ g → isProp (P g))
79+
→ (p₀ : P pt₀)
80+
→ elimProp is-prop-P p₀ pt₀ ≡ p₀
81+
elimPropᵝ is-prop-P p₀ = is-prop-P _ _ p₀
82+
83+
module _ {ℓX} {X : Type ℓX} (is-set-X : isSet X) where
84+
recSetEquiv : X ≃ (⟨ G ⟩ᵗ → X)
85+
recSetEquiv = isPathConnected→constEquiv is-connected is-set-X
86+
87+
recSet : (x₀ : X) → ⟨ G ⟩ᵗ → X
88+
recSet = equivFun recSetEquiv
89+
90+
{-
91+
elimConnected : {X : ⟨ G ⟩ᵗ → Type ℓX} (is-conn-X : ∀ g → isPathConnected (X g))
92+
→ (x₀ : X pt₀)
93+
→ ∀ g → X g
94+
elimConnected is-conn-X x₀ = isConnectedPoint.elim 1 (isPathConnected→is2Connected is-connected) {! !} {! !}
95+
96+
elimSet' : {X : ⟨ G ⟩ᵗ → Type ℓX} (is-set-X : ∀ g → isSet (X g))
97+
→ (x₀ : X pt₀)
98+
→ {! !}
99+
→ ∀ g → X g
100+
elimSet' {X} is-set-X x₀ p = {! recSet !}
101+
102+
elimSet : {X : ⟨ G ⟩ᵗ → Type ℓX} (is-set-X : ∀ g → isSet (X g))
103+
→ (x₀ : X pt₀)
104+
→ {! !}
105+
→ ∀ g → X g
106+
elimSet {X} is-set-X x₀ p g = PT.elim→Set {! !} f {! !} (mere-path g) where
107+
f : pt₀ ≡ g → X g
108+
f p = subst X p x₀
109+
110+
f-filler : (p : pt₀ ≡ g) → PathP (λ i → X (p i)) x₀ (f p)
111+
f-filler p = subst-filler X p x₀
112+
113+
link : (p q : pt₀ ≡ g) → f p ≡ f q
114+
link p q = {!doubleCompPathP (λ i j → X (p i)) (f-filler p) !}
115+
-}
116+
117+
hGroup≡ : ∀ {G H : hGroup ℓ} → G .fst ≡ H .fst → G ≡ H
118+
hGroup≡ = Σ≡Prop isPropIsHGroup
119+
120+
pointedConnectedGroupoid→hGroup : ∀ (G : Type ℓ)
121+
→ (g₀ : G)
122+
→ isPathConnected G
123+
→ isGroupoid G
124+
→ hGroup ℓ
125+
pointedConnectedGroupoid→hGroup G g₀ is-conn-G is-groupoid-G = G* where
126+
G* : hGroup _
127+
G* .fst .fst = G
128+
G* .fst .snd .StrictGroupoidStr.is-groupoid = is-groupoid-G
129+
G* .fst .snd .StrictGroupoidStr.pt = const g₀
130+
G* .fst .snd .StrictGroupoidStr.pt-section = isContr→isProp is-conn-G ∣ g₀ ∣₂
131+
G* .snd = is-conn-G
132+
133+
isTrivial : (G : hGroup ℓ) → Type ℓ
134+
isTrivial G = isContr ⟨ G ⟩ᵗ
135+
136+
isSet→isTrivial : (G : hGroup ℓ) → isSet ⟨ G ⟩ᵗ → isTrivial G
137+
isSet→isTrivial G is-set-G = isOfHLevel×isConnected→isContr 2 ⟨ G ⟩ᵗ is-set-G $ isPathConnected→is2Connected $ hGroup.is-connected G

0 commit comments

Comments
 (0)