Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

π₄S³≡ℤ/2 #715

Merged
merged 8 commits into from
Feb 8, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
88 changes: 86 additions & 2 deletions Cubical/Algebra/Group/Exact.agda
Original file line number Diff line number Diff line change
Expand Up @@ -3,13 +3,16 @@ module Cubical.Algebra.Group.Exact where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec)
open import Cubical.HITs.PropositionalTruncation
renaming (rec to pRec ; map to pMap)
open import Cubical.Algebra.Group.GroupPath

open import Cubical.Algebra.Group.Instances.Unit
open import Cubical.Data.Unit
renaming (Unit to UnitType)

-- TODO : Define exact sequences
-- (perhaps short, finite, ℕ-indexed and ℤ-indexed)
Expand Down Expand Up @@ -52,3 +55,84 @@ SES→isEquiv {R = R} {G = G} {H = H} =
(λ s → sym (snd s) ∙ IsGroupHom.pres1 (snd lhom))
(lexact _ inker)
BijectionIso.surj bijIso' x = rexact x refl

-- exact sequence of 4 groups. Useful for the proof of π₄S³
record Exact4 {ℓ ℓ' ℓ'' ℓ''' : Level} (G : Group ℓ)
(H : Group ℓ') (L : Group ℓ'') (R : Group ℓ''')
(G→H : GroupHom G H) (H→L : GroupHom H L) (L→R : GroupHom L R)
: Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ'' ℓ'''))) where
field
ImG→H⊂KerH→L : (x : fst H) → isInIm G→H x → isInKer H→L x
KerH→L⊂ImG→H : (x : fst H) → isInKer H→L x → isInIm G→H x

ImH→L⊂KerL→R : (x : fst L) → isInIm H→L x → isInKer L→R x
KerL→R⊂ImH→L : (x : fst L) → isInKer L→R x → isInIm H→L x

open Exact4

extendExact4Surjective : {ℓ ℓ' ℓ'' ℓ''' ℓ'''' : Level}
(G : Group ℓ) (H : Group ℓ') (L : Group ℓ'') (R : Group ℓ''') (S : Group ℓ'''')
(G→H : GroupHom G H) (H→L : GroupHom H L) (L→R : GroupHom L R) (R→S : GroupHom R S)
→ isSurjective G→H
→ Exact4 H L R S H→L L→R R→S
→ Exact4 G L R S (compGroupHom G→H H→L) L→R R→S
ImG→H⊂KerH→L (extendExact4Surjective G H L R S G→H H→L L→R R→S surj ex) x =
pRec (GroupStr.is-set (snd R) _ _)
(uncurry λ g → J (λ x _ → isInKer L→R x)
(ImG→H⊂KerH→L ex (fst H→L (fst G→H g))
∣ (fst G→H g) , refl ∣))
KerH→L⊂ImG→H (extendExact4Surjective G H L R S G→H H→L L→R R→S surj ex) x ker =
pRec squash
(uncurry λ y → J (λ x _ → isInIm (compGroupHom G→H H→L) x)
(pMap (uncurry
(λ y → J (λ y _ → Σ[ g ∈ fst G ] fst H→L (fst G→H g) ≡ H→L .fst y)
(y , refl))) (surj y)))
(KerH→L⊂ImG→H ex x ker)
ImH→L⊂KerL→R (extendExact4Surjective G H L R S G→H H→L L→R R→S surj ex) =
ImH→L⊂KerL→R ex
KerL→R⊂ImH→L (extendExact4Surjective G H L R S G→H H→L L→R R→S surj ex) =
KerL→R⊂ImH→L ex

-- Useful lemma in the proof of π₄S³≅ℤ
transportExact4 : {ℓ ℓ' ℓ'' : Level}
{G G₂ : Group ℓ} {H H₂ : Group ℓ'} {L L₂ : Group ℓ''} {R : Group₀}
(G≡G₂ : G ≡ G₂) (H≡H₂ : H ≡ H₂) (L≡L₂ : L ≡ L₂)
→ Unit ≡ R
→ (G→H : GroupHom G H) (G₂→H₂ : GroupHom G₂ H₂)
(H→L : GroupHom H L) (H₂→L₂ : GroupHom H₂ L₂)
(L→R : GroupHom L R)
→ Exact4 G H L R G→H H→L L→R
→ PathP (λ i → GroupHom (G≡G₂ i) (H≡H₂ i)) G→H G₂→H₂
→ PathP (λ i → GroupHom (H≡H₂ i) (L≡L₂ i)) H→L H₂→L₂
→ Exact4 G₂ H₂ L₂ Unit G₂→H₂ H₂→L₂ (→UnitHom L₂)
transportExact4 {G = G} {G₂ = G₂} {H = H} {H₂ = H₂} {L = L} {L₂ = L₂} {R = R} =
J4 (λ G₂ H₂ L₂ R G≡G₂ H≡H₂ L≡L₂ Unit≡R
→ (G→H : GroupHom G H) (G₂→H₂ : GroupHom G₂ H₂)
(H→L : GroupHom H L) (H₂→L₂ : GroupHom H₂ L₂)
(L→R : GroupHom L R)
→ Exact4 G H L R G→H H→L L→R
→ PathP (λ i → GroupHom (G≡G₂ i) (H≡H₂ i)) G→H G₂→H₂
→ PathP (λ i → GroupHom (H≡H₂ i) (L≡L₂ i)) H→L H₂→L₂
→ Exact4 G₂ H₂ L₂ Unit G₂→H₂ H₂→L₂ (→UnitHom L₂))
(λ G→H G₂→H₂ H→L H₂→L₂ L→R ex pp1 pp2
→ J4 (λ G₂→H₂ H₂→L₂ (x : UnitType) (y : UnitType)
pp1 pp2 (_ : tt ≡ x) (_ : tt ≡ x)
→ Exact4 G H L Unit G₂→H₂ H₂→L₂ (→UnitHom L))
ex G₂→H₂ H₂→L₂ tt tt pp1 pp2 refl refl )
G₂ H₂ L₂ R
where
J4 : ∀ {ℓ ℓ₂ ℓ₃ ℓ₄ ℓ'} {A : Type ℓ}
{A₂ : Type ℓ₂} {A₃ : Type ℓ₃} {A₄ : Type ℓ₄}
{x : A} {x₂ : A₂} {x₃ : A₃} {x₄ : A₄}
(B : (y : A) (z : A₂) (w : A₃) (u : A₄)
→ x ≡ y → x₂ ≡ z → x₃ ≡ w → x₄ ≡ u → Type ℓ')
→ B x x₂ x₃ x₄ refl refl refl refl
→ (y : A) (z : A₂) (w : A₃) (u : A₄)
(p : x ≡ y) (q : x₂ ≡ z) (r : x₃ ≡ w) (s : x₄ ≡ u)
→ B y z w u p q r s
J4 {x = x} {x₂ = x₂} {x₃ = x₃} {x₄ = x₄} B b y z w u =
J (λ y p → (q : x₂ ≡ z) (r : x₃ ≡ w) (s : x₄ ≡ u) →
B y z w u p q r s)
(J (λ z q → (r : x₃ ≡ w) (s : x₄ ≡ u) → B x z w u refl q r s)
(J (λ w r → (s : x₄ ≡ u) → B x x₂ w u refl refl r s)
(J (λ u s → B x x₂ x₃ u refl refl refl s) b)))
3 changes: 1 addition & 2 deletions Cubical/Algebra/Group/Instances/Bool.agda
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,7 @@ fst Bool = BoolType
(snd Bool GroupStr.· false) false = true
(snd Bool GroupStr.· false) true = false
(snd Bool GroupStr.· true) y = y
(inv (snd Bool)) false = false
(inv (snd Bool)) true = true
(inv (snd Bool)) x = x
is-set (isSemigroup (isMonoid (isGroup (snd Bool)))) = isSetBool
assoc' (isSemigroup (isMonoid (isGroup (snd Bool)))) false false false = refl
assoc' (isSemigroup (isMonoid (isGroup (snd Bool)))) false false true = refl
Expand Down
25 changes: 24 additions & 1 deletion Cubical/Algebra/Group/Instances/Int.agda
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,13 @@
module Cubical.Algebra.Group.Instances.Int where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Int renaming (ℤ to ℤType ; _+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Int
renaming (ℤ to ℤType ; _+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Properties

open GroupStr

Expand All @@ -19,3 +24,21 @@ isGroup (snd ℤ) = isGroupℤ
isGroupℤ = makeIsGroup isSetℤ +Assoc (λ _ → refl) (+Comm 0)
(λ x → +Comm x (pos 0 -ℤ x) ∙ minusPlus x 0)
(λ x → minusPlus x 0)

ℤHom : (n : ℤType) → GroupHom ℤ ℤ
fst (ℤHom n) x = n ·ℤ x
snd (ℤHom n) =
makeIsGroupHom λ x y → ·DistR+ n x y

negEquivℤ : GroupEquiv ℤ ℤ
fst negEquivℤ =
isoToEquiv
(iso (GroupStr.inv (snd ℤ))
(GroupStr.inv (snd ℤ))
(GroupTheory.invInv ℤ)
(GroupTheory.invInv ℤ))
snd negEquivℤ =
makeIsGroupHom λ x y
→ +Comm (pos 0) (-ℤ (x +ℤ y))
∙ -Dist+ x y
∙ cong₂ _+ℤ_ (+Comm (-ℤ x) (pos 0)) (+Comm (-ℤ y) (pos 0))
139 changes: 137 additions & 2 deletions Cubical/Algebra/Group/Instances/IntMod.agda
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ module Cubical.Algebra.Group.Instances.IntMod where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Monoid.Base
Expand All @@ -11,14 +12,20 @@ open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Data.Bool
open import Cubical.Data.Fin
open import Cubical.Data.Fin.Arithmetic
open import Cubical.Data.Nat
open import Cubical.Data.Int renaming (_+_ to _+ℤ_ ; ℤ to ℤType)
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
open import Cubical.Data.Unit
open import Cubical.Data.Nat.Mod
open import Cubical.Data.Nat.Order
open import Cubical.Algebra.Group.Instances.Int
renaming (ℤ to ℤGroup)
open import Cubical.Algebra.Group.Instances.Unit
renaming (Unit to UnitGroup)
open import Cubical.Algebra.Group.Instances.Bool
renaming (Bool to BoolGroup)
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.Properties
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

Expand All @@ -27,7 +34,7 @@ open IsGroup
open IsMonoid

ℤ/_ : ℕ → Group₀
ℤ/ zero = UnitGroup
ℤ/ zero = ℤGroup
fst (ℤ/ suc n) = Fin (suc n)
1g (snd (ℤ/ suc n)) = 0
GroupStr._·_ (snd (ℤ/ suc n)) = _+ₘ_
Expand Down Expand Up @@ -67,3 +74,131 @@ snd Bool≅ℤ/2 =

ℤ/2≅Bool : GroupIso (ℤ/ 2) BoolGroup
ℤ/2≅Bool = invGroupIso Bool≅ℤ/2

-- Definition of the quotient map homomorphism ℤ → ℤ/ (suc n)
-- as a group homomorphism.
ℤ→Fin : (n : ℕ) → ℤType → Fin (suc n)
ℤ→Fin n (pos x) = x mod (suc n) , mod< n x
ℤ→Fin n (negsuc x) = -ₘ (suc x mod suc n , mod< n (suc x))

ℤ→Fin-presinv : (n : ℕ) (x : ℤType) → ℤ→Fin n (- x) ≡ -ₘ ℤ→Fin n x
ℤ→Fin-presinv n (pos zero) =
Σ≡Prop (λ _ → m≤n-isProp) ((λ _ → zero) ∙ sym (cong fst help))
where
help : (-ₘ_ {n = n} 0) ≡ 0
help = GroupTheory.inv1g (ℤ/ (suc n))
ℤ→Fin-presinv n (pos (suc x)) = Σ≡Prop (λ _ → m≤n-isProp) refl
ℤ→Fin-presinv n (negsuc x) =
sym (GroupTheory.invInv (ℤ/ (suc n)) _)


-ₘ1-id : (n : ℕ)
→ Path (Fin (suc n)) (-ₘ (1 mod (suc n) , mod< n 1))
(n mod (suc n) , mod< n n)
-ₘ1-id zero = refl
-ₘ1-id (suc n) =
cong -ₘ_ (FinPathℕ ((1 mod suc (suc n)) , mod< (suc n) 1) 1
(modIndBase (suc n) 1 (n , +-comm n 2)) .snd)
∙ Σ≡Prop (λ _ → m≤n-isProp)
((+inductionBase (suc n) _
(λ x _ → ((suc (suc n)) ∸ x) mod (suc (suc n))) λ _ x → x) 1
(n , (+-comm n 2)))

suc-ₘ1 : (n y : ℕ)
→ ((suc y mod suc n) , mod< n (suc y)) -ₘ (1 mod (suc n) , mod< n 1)
≡ (y mod suc n , mod< n y)
suc-ₘ1 zero y =
isContr→isProp
(isOfHLevelRetractFromIso 0 (fst ℤ/1≅Unit) isContrUnit) _ _
suc-ₘ1 (suc n) y =
(λ i → ((suc y mod suc (suc n)) , mod< (suc n) (suc y))
+ₘ (-ₘ1-id (suc n) i))
∙ Σ≡Prop (λ _ → m≤n-isProp)
(cong (_mod (2 +ℕ n))
(cong (_+ℕ (suc n) mod (2 +ℕ n))
(mod+mod≡mod (suc (suc n)) 1 y))
∙∙ sym (mod+mod≡mod (suc (suc n))
((1 mod suc (suc n))
+ℕ (y mod suc (suc n))) (suc n))
∙∙ (mod-rCancel (suc (suc n)) ((1 mod suc (suc n))
+ℕ (y mod suc (suc n))) (suc n)
∙ cong (_mod (suc (suc n)))
(cong (_+ℕ (suc n mod suc (suc n)))
(+-comm (1 mod suc (suc n)) (y mod suc (suc n)))
∙ sym (+-assoc (y mod suc (suc n))
(1 mod suc (suc n)) (suc n mod suc (suc n))))
∙∙ mod-rCancel (suc (suc n)) (y mod suc (suc n))
((1 mod suc (suc n)) +ℕ (suc n mod suc (suc n)))
∙∙ (cong (_mod (2 +ℕ n))
(cong ((y mod suc (suc n)) +ℕ_)
(sym (mod+mod≡mod (suc (suc n)) 1 (suc n))
∙ zero-charac (suc (suc n)))
∙ +-comm _ 0)
∙ mod-idempotent y)))

1-ₘsuc : (n y : ℕ)
→ ((1 mod (suc n) , mod< n 1)
+ₘ (-ₘ (((suc y mod suc n) , mod< n (suc y)))))
≡ -ₘ ((y mod suc n) , mod< n y)
1-ₘsuc n y =
sym (GroupTheory.invInv (ℤ/ (suc n)) _)
∙ cong -ₘ_
(GroupTheory.invDistr (ℤ/ (suc n))
(modInd n 1 , mod< n 1) (-ₘ (modInd n (suc y) , mod< n (suc y)))
∙ cong (_-ₘ (modInd n 1 , mod< n 1))
(GroupTheory.invInv (ℤ/ (suc n)) (modInd n (suc y) , mod< n (suc y)))
∙ suc-ₘ1 n y)

isHomℤ→Fin : (n : ℕ) → IsGroupHom (snd ℤGroup) (ℤ→Fin n) (snd (ℤ/ (suc n)))
isHomℤ→Fin n =
makeIsGroupHom
λ { (pos x) y → pos+case x y
; (negsuc x) (pos y) →
cong (ℤ→Fin n) (+Comm (negsuc x) (pos y))
∙∙ pos+case y (negsuc x)
∙∙ +ₘ-comm (ℤ→Fin n (pos y)) (ℤ→Fin n (negsuc x))
; (negsuc x) (negsuc y) →
sym (cong (ℤ→Fin n) (-Dist+ (pos (suc x)) (pos (suc y))))
∙∙ ℤ→Fin-presinv n (pos (suc x) +ℤ (pos (suc y)))
∙∙ cong -ₘ_ (pos+case (suc x) (pos (suc y)))
∙∙ GroupTheory.invDistr (ℤ/ (suc n))
(modInd n (suc x)
, mod< n (suc x)) (modInd n (suc y) , mod< n (suc y))
∙∙ +ₘ-comm (ℤ→Fin n (negsuc y)) (ℤ→Fin n (negsuc x))}
where
+1case : (y : ℤType) → ℤ→Fin n (1 +ℤ y) ≡ ℤ→Fin n 1 +ₘ ℤ→Fin n y
+1case (pos zero) = sym (GroupStr.rid (snd (ℤ/ (suc n))) _)
+1case (pos (suc y)) =
cong (ℤ→Fin n) (+Comm 1 (pos (suc y)))
∙ Σ≡Prop (λ _ → m≤n-isProp) (mod+mod≡mod (suc n) 1 (suc y))
+1case (negsuc zero) =
Σ≡Prop (λ _ → m≤n-isProp) refl
∙ sym (GroupStr.invr (snd (ℤ/ (suc n))) (modInd n 1 , mod< n 1))
+1case (negsuc (suc y)) =
Σ≡Prop (λ _ → m≤n-isProp)
(cong fst (cong (ℤ→Fin n) (+Comm 1 (negsuc (suc y))))
∙∙ cong fst (cong -ₘ_ (refl {x = suc y mod suc n , mod< n (suc y)}))
∙∙ cong fst (sym (1-ₘsuc n (suc y)))
∙ λ i → fst ((1 mod (suc n) , mod< n 1)
+ₘ (-ₘ (((suc (suc y) mod suc n) , mod< n (suc (suc y)))))))

pos+case : (x : ℕ) (y : ℤType)
→ ℤ→Fin n (pos x +ℤ y) ≡ ℤ→Fin n (pos x) +ₘ ℤ→Fin n y
pos+case zero y =
cong (ℤ→Fin n) (+Comm 0 y)
∙ sym (GroupStr.lid (snd (ℤ/ (suc n))) (ℤ→Fin n y))
pos+case (suc zero) y = +1case y
pos+case (suc (suc x)) y =
cong (ℤ→Fin n) (cong (_+ℤ y) (+Comm (pos (suc x)) 1)
∙ sym (+Assoc 1 (pos (suc x)) y))
∙∙ +1case (pos (suc x) +ℤ y)
∙∙ (cong ((modInd n 1 , mod< n 1) +ₘ_) (pos+case (suc x) y)
∙∙ sym (+ₘ-assoc (modInd n 1 , mod< n 1)
(modInd n (suc x) , mod< n (suc x)) (ℤ→Fin n y))
∙∙ cong (_+ₘ ℤ→Fin n y) (lem x))
where
lem : (x : ℕ)
→ (modInd n 1 , mod< n 1) +ₘ (modInd n (suc x) , mod< n (suc x))
≡ ℤ→Fin n (pos (suc (suc x)))
lem x =
Σ≡Prop (λ _ → m≤n-isProp) (sym (mod+mod≡mod (suc n) 1 (suc x)))
4 changes: 4 additions & 0 deletions Cubical/Algebra/Group/Instances/Unit.agda
Original file line number Diff line number Diff line change
Expand Up @@ -68,3 +68,7 @@ GroupIsoUnitGroup→isContr : {G : Group ℓ-zero}
→ GroupIso Unit G → isContr (fst G)
GroupIsoUnitGroup→isContr is =
isOfHLevelRetractFromIso 0 (invIso (fst is)) isContrUnit

→UnitHom : ∀ {ℓ} (G : Group ℓ) → GroupHom G Unit
fst (→UnitHom G) _ = tt
snd (→UnitHom G) = makeIsGroupHom λ _ _ → refl
Loading