From af2aa7ac902ca6ba903b31a6746b1028d8b13c46 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 5 Nov 2024 17:11:21 -0600 Subject: [PATCH 1/9] exact sequences --- Cubical/Algebra/Group/Exact.agda | 67 +++++++++++++++++++++++++++++++- 1 file changed, 66 insertions(+), 1 deletion(-) diff --git a/Cubical/Algebra/Group/Exact.agda b/Cubical/Algebra/Group/Exact.agda index 6ba146876a..908be3f767 100644 --- a/Cubical/Algebra/Group/Exact.agda +++ b/Cubical/Algebra/Group/Exact.agda @@ -4,7 +4,14 @@ module Cubical.Algebra.Group.Exact where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv open import Cubical.Foundations.Function +open import Cubical.Foundations.Structure +open import Cubical.Data.Empty +open import Cubical.Data.Fin +open import Cubical.Data.Nat +open import Cubical.Data.Nat.Order +open import Cubical.Data.Sigma +open import Cubical.Data.Sum open import Cubical.Data.Unit open import Cubical.Algebra.Group.Base @@ -15,11 +22,68 @@ open import Cubical.Algebra.Group.Instances.Unit open import Cubical.HITs.PropositionalTruncation as PT +private + variable + ℓ ℓ' : Level -- TODO : Define exact sequences -- (perhaps short, finite, ℕ-indexed and ℤ-indexed) -SES→isEquiv : ∀ {ℓ ℓ'} {L R : Group ℓ-zero} + +isWeakExactAt : {A B B' C : Group ℓ} (f : GroupHom A B) (g : GroupHom B' C) (p : B ≡ B') → Type ℓ +isWeakExactAt {B = B} {B' = B'} f g p = + (b : ⟨ B ⟩) → (isInKer g (subst fst p b) → isInIm f b) × (isInIm f b → isInKer g (subst fst p b)) + +isExactAt : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) → Type ℓ +isExactAt {B = B} f g = (b : ⟨ B ⟩) → isWeakExactAt f g refl + +-- Fin-indexed sequences +module _ where + finExactSeq : {len-2 : ℕ} + → (gSeq : (gIdx : Fin (suc (suc len-2))) → Group ℓ) + → (hSeq : (hIdx : Fin (suc len-2)) → GroupHom (gSeq (finj hIdx)) (gSeq (fsuc hIdx))) + → Type ℓ + finExactSeq {len-2 = len-2} gSeq hSeq = (pIdx : Fin len-2) → isWeakExactAt (hSeq (finj pIdx)) (hSeq (fsuc pIdx)) (cong gSeq (toℕ-injective refl)) + +-- ℕ-indexed sequences +module _ where + ℕExactSeq : (gSeq : (n : ℕ) → Group ℓ) → (hSeq : (n : ℕ) → GroupHom (gSeq n) (gSeq (suc n))) → Type ℓ + ℕExactSeq gSeq hSeq = (m : ℕ) → isExactAt (hSeq m) (hSeq (suc m)) + +-- ℤ-indexed sequences +module _ where + open import Cubical.Data.Int + ℤExactSeq : (gSeq : (z : ℤ) → Group ℓ) → (hSeq : (z : ℤ) → GroupHom (gSeq z) (gSeq (sucℤ z))) → Type ℓ + ℤExactSeq gSeq hSeq = (m : ℤ) → isExactAt (hSeq m) (hSeq (sucℤ m)) + +-- Short exact sequences +module _ {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) where + open import Cubical.Data.Vec + + sesGVec : Vec (Group ℓ) 5 + sesGVec = UnitGroup ∷ A ∷ B ∷ C ∷ UnitGroup ∷ [] + + sesGSeq : (gIdx : Fin 5) → Group ℓ + sesGSeq gIdx = lookup (Fin→FinData 5 gIdx) sesGVec + + 0→A : GroupHom (UnitGroup {ℓ}) A + 0→A = let open GroupStr (A .snd) in + (λ _ → 1g) , record { pres· = λ x y → sym (·IdR 1g) ; pres1 = refl ; presinv = λ x → sym (·InvL 1g) ∙ ·IdR (inv 1g) } + + C→0 : GroupHom C (UnitGroup {ℓ}) + C→0 = (λ _ → tt*) , record { pres· = λ x y → refl ; pres1 = refl ; presinv = λ x → refl } + + sesHSeq : (hIdx : Fin 4) → GroupHom (sesGSeq (finj hIdx)) (sesGSeq (fsuc hIdx)) + sesHSeq (zero , _) = 0→A + sesHSeq (suc zero , _) = f + sesHSeq (suc (suc zero) , _) = g + sesHSeq (suc (suc (suc zero)) , _) = C→0 + sesHSeq (suc (suc (suc (suc n))) , p) = Cubical.Data.Empty.rec (¬-<-zero (≤-k+-cancel p)) + + shortExactSeq : Type ℓ + shortExactSeq = (pIdx : Fin 4) → finExactSeq sesGSeq sesHSeq + +SES→isEquiv : {L R : Group ℓ-zero} → {G : Group ℓ} {H : Group ℓ'} → UnitGroup₀ ≡ L → UnitGroup₀ ≡ R @@ -138,3 +202,4 @@ transportExact4 {G = G} {G₂ = G₂} {H = H} {H₂ = H₂} {L = L} {L₂ = L₂ (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))) + \ No newline at end of file From f96cc5059fc07baf6822ccb65afa717013c9a2ab Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 5 Nov 2024 22:39:42 -0600 Subject: [PATCH 2/9] complete five proof --- Cubical/Algebra/Group/Exact.agda | 84 +++++++--- Cubical/Algebra/Group/Five.agda | 270 +++++++++++++++++++++++++++++++ 2 files changed, 329 insertions(+), 25 deletions(-) create mode 100644 Cubical/Algebra/Group/Five.agda diff --git a/Cubical/Algebra/Group/Exact.agda b/Cubical/Algebra/Group/Exact.agda index 908be3f767..9b4106368d 100644 --- a/Cubical/Algebra/Group/Exact.agda +++ b/Cubical/Algebra/Group/Exact.agda @@ -1,10 +1,13 @@ {-# OPTIONS --safe #-} + module Cubical.Algebra.Group.Exact where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Function open import Cubical.Foundations.Structure +open import Cubical.Foundations.HLevels open import Cubical.Data.Empty open import Cubical.Data.Fin @@ -26,24 +29,34 @@ private variable ℓ ℓ' : Level --- TODO : Define exact sequences --- (perhaps short, finite, ℕ-indexed and ℤ-indexed) - - +-- Exactness except the intersecting Group is only propositionally equal isWeakExactAt : {A B B' C : Group ℓ} (f : GroupHom A B) (g : GroupHom B' C) (p : B ≡ B') → Type ℓ -isWeakExactAt {B = B} {B' = B'} f g p = - (b : ⟨ B ⟩) → (isInKer g (subst fst p b) → isInIm f b) × (isInIm f b → isInKer g (subst fst p b)) +isWeakExactAt {ℓ = ℓ} {B = B} {B' = B'} f g p = + (b : ⟨ B ⟩) → (isInKer g (subst (λ (a : Σ (Type ℓ) GroupStr) → fst a) p b) → isInIm f b) × (isInIm f b → isInKer g (subst fst p b)) isExactAt : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) → Type ℓ -isExactAt {B = B} f g = (b : ⟨ B ⟩) → isWeakExactAt f g refl +isExactAt {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b → isInIm f b) × (isInIm f b → isInKer g b) + +-- TODO: Is exactness preserved across association? + +isWeakExactAtRefl : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) + → isWeakExactAt f g refl ≡ isExactAt f g +isWeakExactAtRefl {ℓ = ℓ} {B = B} f g i = (b : ⟨ B ⟩) → (isInKer g (transportRefl b i) → isInIm f b) × (isInIm f b → isInKer g (transportRefl b i)) -- Fin-indexed sequences module _ where + -- finExactSeq : {len-2 : ℕ} + -- → (gSeq : (gIdx : Fin (suc (suc len-2))) → Group ℓ) + -- → (hSeq : (hIdx : Fin (suc len-2)) → GroupHom (gSeq (finj hIdx)) (gSeq (fsuc hIdx))) + -- → Type ℓ + -- finExactSeq {len-2 = len-2} gSeq hSeq = (pIdx : Fin len-2) → isWeakExactAt (hSeq (finj pIdx)) (hSeq (fsuc pIdx)) (cong gSeq (toℕ-injective refl)) + finExactSeq : {len-2 : ℕ} → (gSeq : (gIdx : Fin (suc (suc len-2))) → Group ℓ) → (hSeq : (hIdx : Fin (suc len-2)) → GroupHom (gSeq (finj hIdx)) (gSeq (fsuc hIdx))) → Type ℓ - finExactSeq {len-2 = len-2} gSeq hSeq = (pIdx : Fin len-2) → isWeakExactAt (hSeq (finj pIdx)) (hSeq (fsuc pIdx)) (cong gSeq (toℕ-injective refl)) + finExactSeq {ℓ = ℓ} {len-2 = len-2} gSeq hSeq + = (pIdx : Fin len-2) → isExactAt (subst (λ n → GroupHom (gSeq (finj (finj pIdx))) (gSeq n)) (toℕ-injective refl) (hSeq (finj pIdx))) (hSeq (fsuc pIdx)) -- ℕ-indexed sequences module _ where @@ -56,32 +69,53 @@ module _ where ℤExactSeq : (gSeq : (z : ℤ) → Group ℓ) → (hSeq : (z : ℤ) → GroupHom (gSeq z) (gSeq (sucℤ z))) → Type ℓ ℤExactSeq gSeq hSeq = (m : ℤ) → isExactAt (hSeq m) (hSeq (sucℤ m)) +module _ where + 0→_ : (A : Group ℓ) → GroupHom (UnitGroup {ℓ}) A + 0→ A = let open GroupStr (A .snd) in + (λ _ → 1g) , record { pres· = λ x y → sym (·IdR 1g) ; pres1 = refl ; presinv = λ x → sym (·InvL 1g) ∙ ·IdR (inv 1g) } + + _→0 : (A : Group ℓ) → GroupHom A (UnitGroup {ℓ}) + A →0 = (λ _ → tt*) , record { pres· = λ x y → refl ; pres1 = refl ; presinv = λ x → refl } + -- Short exact sequences module _ {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) where open import Cubical.Data.Vec - sesGVec : Vec (Group ℓ) 5 - sesGVec = UnitGroup ∷ A ∷ B ∷ C ∷ UnitGroup ∷ [] + private + sesGVec : Vec (Group ℓ) 5 + sesGVec = UnitGroup ∷ A ∷ B ∷ C ∷ UnitGroup ∷ [] - sesGSeq : (gIdx : Fin 5) → Group ℓ - sesGSeq gIdx = lookup (Fin→FinData 5 gIdx) sesGVec + sesGSeq : (gIdx : Fin 5) → Group ℓ + sesGSeq gIdx = lookup (Fin→FinData 5 gIdx) sesGVec - 0→A : GroupHom (UnitGroup {ℓ}) A - 0→A = let open GroupStr (A .snd) in - (λ _ → 1g) , record { pres· = λ x y → sym (·IdR 1g) ; pres1 = refl ; presinv = λ x → sym (·InvL 1g) ∙ ·IdR (inv 1g) } + sesHSeq : (hIdx : Fin 4) → GroupHom (sesGSeq (finj hIdx)) (sesGSeq (fsuc hIdx)) + sesHSeq (zero , _) = 0→ A + sesHSeq (suc zero , _) = f + sesHSeq (suc (suc zero) , _) = g + sesHSeq (suc (suc (suc zero)) , _) = C →0 + sesHSeq (suc (suc (suc (suc n))) , p) = Cubical.Data.Empty.rec (¬-<-zero (≤-k+-cancel p)) + + shortExactSeq2 : Type ℓ + shortExactSeq2 = finExactSeq sesGSeq sesHSeq + +module _ {A B : Group ℓ} (f : GroupHom A B) where + open import Cubical.Data.Vec + + private + sesGVec : Vec (Group ℓ) 4 + sesGVec = UnitGroup ∷ A ∷ B ∷ UnitGroup ∷ [] - C→0 : GroupHom C (UnitGroup {ℓ}) - C→0 = (λ _ → tt*) , record { pres· = λ x y → refl ; pres1 = refl ; presinv = λ x → refl } + sesGSeq : (gIdx : Fin 4) → Group ℓ + sesGSeq gIdx = lookup (Fin→FinData 4 gIdx) sesGVec - sesHSeq : (hIdx : Fin 4) → GroupHom (sesGSeq (finj hIdx)) (sesGSeq (fsuc hIdx)) - sesHSeq (zero , _) = 0→A - sesHSeq (suc zero , _) = f - sesHSeq (suc (suc zero) , _) = g - sesHSeq (suc (suc (suc zero)) , _) = C→0 - sesHSeq (suc (suc (suc (suc n))) , p) = Cubical.Data.Empty.rec (¬-<-zero (≤-k+-cancel p)) + sesHSeq : (hIdx : Fin 3) → GroupHom (sesGSeq (finj hIdx)) (sesGSeq (fsuc hIdx)) + sesHSeq (zero , _) = 0→ A + sesHSeq (suc zero , _) = f + sesHSeq (suc (suc zero) , _) = B →0 + sesHSeq (suc (suc (suc n)) , p) = Cubical.Data.Empty.rec (¬-<-zero (≤-k+-cancel p)) shortExactSeq : Type ℓ - shortExactSeq = (pIdx : Fin 4) → finExactSeq sesGSeq sesHSeq + shortExactSeq = finExactSeq sesGSeq sesHSeq SES→isEquiv : {L R : Group ℓ-zero} → {G : Group ℓ} {H : Group ℓ'} @@ -202,4 +236,4 @@ transportExact4 {G = G} {G₂ = G₂} {H = H} {H₂ = H₂} {L = L} {L₂ = L₂ (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))) - \ No newline at end of file + \ No newline at end of file diff --git a/Cubical/Algebra/Group/Five.agda b/Cubical/Algebra/Group/Five.agda new file mode 100644 index 0000000000..2747920539 --- /dev/null +++ b/Cubical/Algebra/Group/Five.agda @@ -0,0 +1,270 @@ +{-# OPTIONS --cubical #-} + +-- This module proves the Five lemma[1] over group homomorphisms. +-- +-- [1]: https://en.wikipedia.org/wiki/Five_lemma + +module Cubical.Algebra.Group.Five where + +open import Agda.Primitive + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Structure +open import Cubical.Foundations.Isomorphism + +open import Cubical.HITs.PropositionalTruncation.Base +open import Cubical.HITs.PropositionalTruncation as PT + +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Group.Exact +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Group.Morphisms + +open BijectionIso +open IsGroupHom + +private + variable + ℓ ℓ' : Level + +module _ + (A B C D E A' B' C' D' E' : Group ℓ) + (f : GroupHom A B) (g : GroupHom B C) (h : GroupHom C D) (j : GroupHom D E) + (l : GroupHom A A') (m : BijectionIso B B') (n : GroupHom C C') (p : BijectionIso D D') (q : GroupHom E E') + (r : GroupHom A' B') (s : GroupHom B' C') (t : GroupHom C' D') (u : GroupHom D' E') + (fg : isExactAt f g) (gh : isExactAt g h) (hj : isExactAt h j) + (rs : isExactAt r s) (st : isExactAt s t) (tu : isExactAt t u) + (lSurj : isSurjective l) + (qInj : isInjective q) + (sq1 : (a : fst A) → r .fst (l .fst a) ≡ m .fun .fst (f .fst a)) + (sq2 : (b : fst B) → s .fst (m .fun .fst b) ≡ n .fst (g .fst b)) + (sq3 : (c : fst C) → t .fst (n .fst c) ≡ p .fun .fst (h .fst c)) + (sq4 : (d : fst D) → u .fst (p .fun .fst d) ≡ q .fst (j .fst d)) + where + module _ where + nInjective : isInjective n + nInjective c c-in-ker[n] = goal where + goalTy = c ≡ C .snd .GroupStr.1g + goalTyIsProp = let open GroupStr (C .snd) in is-set c 1g + untrunc = λ (p : ∥ goalTy ∥₁) → PT.rec goalTyIsProp (λ x → x) p + + t[n[c]]≡0 : t .fst (n .fst c) ≡ D' .snd .GroupStr.1g + t[n[c]]≡0 = cong (t .fst) c-in-ker[n] ∙ t .snd .pres1 + + t[n[c]]≡p[h[c]] : t .fst (n .fst c) ≡ p .fun .fst (h .fst c) + t[n[c]]≡p[h[c]] = sq3 c + + p[h[c]]≡0 : p .fun .fst (h .fst c) ≡ D' .snd .GroupStr.1g + p[h[c]]≡0 = sym t[n[c]]≡p[h[c]] ∙ t[n[c]]≡0 + + h[c]≡0 : h .fst c ≡ D .snd .GroupStr.1g + h[c]≡0 = p .inj (h .fst c) p[h[c]]≡0 + + c-in-ker[h] : isInKer h c + c-in-ker[h] = h[c]≡0 + + c-in-im[g] : isInIm g c + c-in-im[g] = gh c .fst c-in-ker[h] + + rest : (b : ⟨ B ⟩) → (g .fst b ≡ c) → goalTy + + goal = untrunc (map (λ x → rest (fst x) (snd x)) c-in-im[g]) + + rest b g[b]≡c = goal2 where + + n[g[b]]≡0 : n .fst (g .fst b) ≡ C' .snd .GroupStr.1g + n[g[b]]≡0 = cong (n .fst) g[b]≡c ∙ c-in-ker[n] + + m[b] : ⟨ B' ⟩ + m[b] = m .fun .fst b + + s[m[b]]≡n[g[b]] : s .fst m[b] ≡ n .fst (g .fst b) + s[m[b]]≡n[g[b]] = sq2 b + + s[m[b]]≡0 : s .fst m[b] ≡ C' .snd .GroupStr.1g + s[m[b]]≡0 = s[m[b]]≡n[g[b]] ∙ n[g[b]]≡0 + + m[b]-in-ker[s] : isInKer s m[b] + m[b]-in-ker[s] = s[m[b]]≡0 + + m[b]-in-im[r] : isInIm r m[b] + m[b]-in-im[r] = rs m[b] .fst m[b]-in-ker[s] + + rest2 : (a' : ⟨ A' ⟩) → (r .fst a' ≡ m[b]) → (a : ⟨ A ⟩) → l .fst a ≡ a' → goalTy + + goal2 = + let inner = λ x → untrunc (map (λ y → rest2 (x .fst) (x .snd) (y .fst) (y .snd)) (lSurj (x .fst))) in + untrunc (map inner m[b]-in-im[r]) + + rest2 a' r[a']≡m[b] a l[a]≡a' = c≡0 where + + m[f[a]] : ⟨ B' ⟩ + m[f[a]] = m .fun .fst (f .fst a) + + r[l[a]]≡m[f[a]] : r .fst (l .fst a) ≡ m[f[a]] + r[l[a]]≡m[f[a]] = sq1 a + + m[f[a]]≡m[b] : m[f[a]] ≡ m[b] + m[f[a]]≡m[b] = sym r[l[a]]≡m[f[a]] ∙ cong (r .fst) l[a]≡a' ∙ r[a']≡m[b] + + f[a]≡b : f .fst a ≡ b + f[a]≡b = isInjective→isMono (m .fun) (m .inj) m[f[a]]≡m[b] + + g[f[a]]≡c : g .fst (f .fst a) ≡ c + g[f[a]]≡c = cong (g .fst) f[a]≡b ∙ g[b]≡c + + f[a]-in-im[f] : isInIm f (f .fst a) + f[a]-in-im[f] = ∣ a , refl ∣₁ + + f[a]-in-ker[g] : isInKer g (f .fst a) + f[a]-in-ker[g] = fg (f .fst a) .snd f[a]-in-im[f] + + g[f[a]]≡0 : g .fst (f .fst a) ≡ C .snd .GroupStr.1g + g[f[a]]≡0 = f[a]-in-ker[g] + + c≡0 : c ≡ C .snd .GroupStr.1g + c≡0 = sym g[f[a]]≡c ∙ g[f[a]]≡0 + + module _ where + nSurjective : isSurjective n + nSurjective c' = goal where + goalTy = isInIm n c' + untrunc = λ (p : ∥ goalTy ∥₁) → PT.rec (isPropIsInIm n c') (λ x → x) p + + d' : ⟨ D' ⟩ + d' = t .fst c' + + pGroupIso = BijectionIso→GroupIso p + pIso = pGroupIso .fst + pInv = Iso.inv pIso + + d : ⟨ D ⟩ + d = pInv d' + + p[d]≡t[c'] : p .fun .fst d ≡ t .fst c' + p[d]≡t[c'] = Iso.rightInv pIso d' + + u[p[d]] : ⟨ E' ⟩ + u[p[d]] = u .fst (p .fun .fst d) + + j[d] : ⟨ E ⟩ + j[d] = j .fst d + + q[j[d]] : ⟨ E' ⟩ + q[j[d]] = q .fst j[d] + + u[p[d]]≡q[j[d]] : u[p[d]] ≡ q[j[d]] + u[p[d]]≡q[j[d]] = sq4 d + + d'-in-ker[u] : isInKer u d' + d'-in-ker[u] = let im[t]→ker[u] = tu d' .snd in + im[t]→ker[u] ∣ (c' , refl) ∣₁ + + u[p[d]]≡0 : u[p[d]] ≡ E' .snd .GroupStr.1g + u[p[d]]≡0 = cong (u .fst) p[d]≡t[c'] ∙ d'-in-ker[u] + + q[j[d]]≡0 : q[j[d]] ≡ E' .snd .GroupStr.1g + q[j[d]]≡0 = sym u[p[d]]≡q[j[d]] ∙ u[p[d]]≡0 + + j[d]≡0 : j[d] ≡ E .snd .GroupStr.1g + j[d]≡0 = qInj j[d] q[j[d]]≡0 + + d-in-ker[j] : isInKer j d + d-in-ker[j] = j[d]≡0 + + d-in-im[h] : isInIm h d + d-in-im[h] = + let ker[j]→im[h] = hj d .fst in + ker[j]→im[h] d-in-ker[j] + + rest : (c : ⟨ C ⟩) → h .fst c ≡ d → goalTy + + goal = untrunc (map (λ x → rest (x .fst) (x .snd)) d-in-im[h]) + + rest c h[c]≡d = goal2 where + n[c] : ⟨ C' ⟩ + n[c] = n .fst c + + t[n[c]]≡p[h[c]] : t .fst n[c] ≡ p .fun .fst (h .fst c) + t[n[c]]≡p[h[c]] = sq3 c + + t[n[c]]≡t[c'] : t .fst n[c] ≡ t .fst c' + t[n[c]]≡t[c'] = + t .fst n[c] ≡⟨ t[n[c]]≡p[h[c]] ⟩ + p .fun .fst (h .fst c) ≡⟨ cong (p .fun .fst) h[c]≡d ⟩ + p .fun .fst d ≡⟨ p[d]≡t[c'] ⟩ + t .fst c' ∎ + + c'-n[c] : ⟨ C' ⟩ + c'-n[c] = let open GroupStr (C' .snd) in c' · (inv n[c]) + + t[c'-n[c]]≡0 : t .fst c'-n[c] ≡ D' .snd .GroupStr.1g + t[c'-n[c]]≡0 = + let open GroupStr (C' .snd) renaming (_·_ to _·ᶜ_; inv to invᶜ; 1g to 1gᶜ) in + let open GroupStr (D' .snd) renaming (_·_ to _·ᵈ_; inv to invᵈ; 1g to 1gᵈ) hiding (isGroup) in + t .fst (c' ·ᶜ (invᶜ n[c])) ≡⟨ t .snd .pres· c' (invᶜ n[c]) ⟩ + (t .fst c') ·ᵈ (t .fst (invᶜ n[c])) ≡⟨ cong ((t .fst c') ·ᵈ_) (t .snd .presinv n[c]) ⟩ + (t .fst c') ·ᵈ (invᵈ (t .fst n[c])) ≡⟨ cong (λ z → (t .fst c') ·ᵈ (invᵈ z)) t[n[c]]≡t[c'] ⟩ + (t .fst c') ·ᵈ (invᵈ (t .fst c')) ≡⟨ cong ((t .fst c') ·ᵈ_) (sym (t .snd .presinv c')) ⟩ + (t .fst c') ·ᵈ (t .fst (invᶜ c')) ≡⟨ sym (t .snd .pres· c' (invᶜ c')) ⟩ + t .fst (c' ·ᶜ (invᶜ c')) ≡⟨ cong (t .fst) (IsGroup.·InvR isGroup c') ⟩ + t .fst 1gᶜ ≡⟨ t .snd .pres1 ⟩ + 1gᵈ ∎ + + [c'-n[c]]-in-ker[t] : isInKer t c'-n[c] + [c'-n[c]]-in-ker[t] = t[c'-n[c]]≡0 + + [c'-n[c]]-in-im[s] : isInIm s c'-n[c] + [c'-n[c]]-in-im[s] = + let ker[t]→im[s] = st c'-n[c] .fst in + ker[t]→im[s] [c'-n[c]]-in-ker[t] + + rest2 : (b' : ⟨ B' ⟩) → s .fst b' ≡ c'-n[c] → goalTy + + goal2 = untrunc (map (λ x → rest2 (x .fst) (x .snd)) [c'-n[c]]-in-im[s]) + + rest2 b' s[b']≡c'-n[c] = goal3 where + mGroupIso = BijectionIso→GroupIso m + mIso = mGroupIso .fst + mInv = Iso.inv mIso + + b : ⟨ B ⟩ + b = mInv b' + + m[b]≡b' : m .fun .fst b ≡ b' + m[b]≡b' = Iso.rightInv mIso b' + + s[m[b]]≡s[b'] : s .fst (m .fun .fst b) ≡ s .fst b' + s[m[b]]≡s[b'] = cong (s .fst) m[b]≡b' + + s[m[b]]≡c'-n[c] : s .fst (m .fun .fst b) ≡ c'-n[c] + s[m[b]]≡c'-n[c] = s[m[b]]≡s[b'] ∙ s[b']≡c'-n[c] + + g[b] : ⟨ C ⟩ + g[b] = g .fst b + + g[b]+c : ⟨ C ⟩ + g[b]+c = C .snd .GroupStr._·_ g[b] c + + n[g[b]] : ⟨ C' ⟩ + n[g[b]] = n .fst g[b] + + n[g[b]]≡s[m[b]] : n[g[b]] ≡ s .fst (m .fun .fst b) + n[g[b]]≡s[m[b]] = sym (sq2 b) + + n[g[b]]≡c'-n[c] : n[g[b]] ≡ c'-n[c] + n[g[b]]≡c'-n[c] = n[g[b]]≡s[m[b]] ∙ s[m[b]]≡c'-n[c] + + n[g[b]]+n[c]≡c' : C' .snd .GroupStr._·_ n[g[b]] n[c] ≡ c' + n[g[b]]+n[c]≡c' = + let open GroupStr (C' .snd) in + cong (_· n[c]) n[g[b]]≡c'-n[c] ∙ sym (·Assoc c' (inv n[c]) n[c]) ∙ cong (c' ·_) (·InvL n[c]) ∙ ·IdR c' + + n[g[b]+c]≡c' : n .fst g[b]+c ≡ c' + n[g[b]+c]≡c' = n .snd .pres· g[b] c ∙ n[g[b]]+n[c]≡c' + + goal3 = ∣ (g[b]+c , n[g[b]+c]≡c') ∣₁ + + lemma : BijectionIso C C' + lemma = bijIso n nInjective nSurjective \ No newline at end of file From 66616631101565fc7ce69606d0fd084d8663d125 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 5 Nov 2024 22:48:41 -0600 Subject: [PATCH 3/9] make five safe --- Cubical/Algebra/Group/Five.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Algebra/Group/Five.agda b/Cubical/Algebra/Group/Five.agda index 2747920539..81b3527117 100644 --- a/Cubical/Algebra/Group/Five.agda +++ b/Cubical/Algebra/Group/Five.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical #-} +{-# OPTIONS --safe #-} -- This module proves the Five lemma[1] over group homomorphisms. -- From b5c0ff85715b24fbf3f7793bdbb33d0fcd666e1c Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 6 Nov 2024 11:38:02 -0600 Subject: [PATCH 4/9] fix newline --- Cubical/Algebra/Group/Exact.agda | 2 +- Cubical/Algebra/Group/Five.agda | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Cubical/Algebra/Group/Exact.agda b/Cubical/Algebra/Group/Exact.agda index 9b4106368d..ecc9e8fae6 100644 --- a/Cubical/Algebra/Group/Exact.agda +++ b/Cubical/Algebra/Group/Exact.agda @@ -236,4 +236,4 @@ transportExact4 {G = G} {G₂ = G₂} {H = H} {H₂ = H₂} {L = L} {L₂ = L₂ (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))) - \ No newline at end of file + diff --git a/Cubical/Algebra/Group/Five.agda b/Cubical/Algebra/Group/Five.agda index 81b3527117..3224c67c29 100644 --- a/Cubical/Algebra/Group/Five.agda +++ b/Cubical/Algebra/Group/Five.agda @@ -87,7 +87,7 @@ module _ m[b]-in-ker[s] : isInKer s m[b] m[b]-in-ker[s] = s[m[b]]≡0 - + m[b]-in-im[r] : isInIm r m[b] m[b]-in-im[r] = rs m[b] .fst m[b]-in-ker[s] @@ -267,4 +267,4 @@ module _ goal3 = ∣ (g[b]+c , n[g[b]+c]≡c') ∣₁ lemma : BijectionIso C C' - lemma = bijIso n nInjective nSurjective \ No newline at end of file + lemma = bijIso n nInjective nSurjective From 4e8aa9cbecf1492027b14ebd4fe654ff80e622e2 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 7 Nov 2024 00:11:03 -0600 Subject: [PATCH 5/9] exactness over a successor structure --- Cubical/Algebra/Group/Exact.agda | 35 ++++++++++++++------------------ 1 file changed, 15 insertions(+), 20 deletions(-) diff --git a/Cubical/Algebra/Group/Exact.agda b/Cubical/Algebra/Group/Exact.agda index ecc9e8fae6..d91f18ccd0 100644 --- a/Cubical/Algebra/Group/Exact.agda +++ b/Cubical/Algebra/Group/Exact.agda @@ -29,6 +29,9 @@ private variable ℓ ℓ' : Level +SuccStr : Type (ℓ-suc ℓ) +SuccStr {ℓ = ℓ} = TypeWithStr ℓ λ A → (A → A) + -- Exactness except the intersecting Group is only propositionally equal isWeakExactAt : {A B B' C : Group ℓ} (f : GroupHom A B) (g : GroupHom B' C) (p : B ≡ B') → Type ℓ isWeakExactAt {ℓ = ℓ} {B = B} {B' = B'} f g p = @@ -43,14 +46,8 @@ isWeakExactAtRefl : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) → isWeakExactAt f g refl ≡ isExactAt f g isWeakExactAtRefl {ℓ = ℓ} {B = B} f g i = (b : ⟨ B ⟩) → (isInKer g (transportRefl b i) → isInIm f b) × (isInIm f b → isInKer g (transportRefl b i)) --- Fin-indexed sequences +-- Finite exact sequence module _ where - -- finExactSeq : {len-2 : ℕ} - -- → (gSeq : (gIdx : Fin (suc (suc len-2))) → Group ℓ) - -- → (hSeq : (hIdx : Fin (suc len-2)) → GroupHom (gSeq (finj hIdx)) (gSeq (fsuc hIdx))) - -- → Type ℓ - -- finExactSeq {len-2 = len-2} gSeq hSeq = (pIdx : Fin len-2) → isWeakExactAt (hSeq (finj pIdx)) (hSeq (fsuc pIdx)) (cong gSeq (toℕ-injective refl)) - finExactSeq : {len-2 : ℕ} → (gSeq : (gIdx : Fin (suc (suc len-2))) → Group ℓ) → (hSeq : (hIdx : Fin (suc len-2)) → GroupHom (gSeq (finj hIdx)) (gSeq (fsuc hIdx))) @@ -58,16 +55,13 @@ module _ where finExactSeq {ℓ = ℓ} {len-2 = len-2} gSeq hSeq = (pIdx : Fin len-2) → isExactAt (subst (λ n → GroupHom (gSeq (finj (finj pIdx))) (gSeq n)) (toℕ-injective refl) (hSeq (finj pIdx))) (hSeq (fsuc pIdx)) --- ℕ-indexed sequences -module _ where - ℕExactSeq : (gSeq : (n : ℕ) → Group ℓ) → (hSeq : (n : ℕ) → GroupHom (gSeq n) (gSeq (suc n))) → Type ℓ - ℕExactSeq gSeq hSeq = (m : ℕ) → isExactAt (hSeq m) (hSeq (suc m)) - --- ℤ-indexed sequences +-- Exact sequence over successor structures module _ where - open import Cubical.Data.Int - ℤExactSeq : (gSeq : (z : ℤ) → Group ℓ) → (hSeq : (z : ℤ) → GroupHom (gSeq z) (gSeq (sucℤ z))) → Type ℓ - ℤExactSeq gSeq hSeq = (m : ℤ) → isExactAt (hSeq m) (hSeq (sucℤ m)) + exactSeq : (ss @ (N , succ) : SuccStr {ℓ = ℓ}) + → (gSeq : (gIdx : N) → Group ℓ') + → (hSeq : (hIdx : N) → GroupHom (gSeq hIdx) (gSeq (succ hIdx))) + → Type (ℓ-max ℓ ℓ') + exactSeq (N , succ) gSeq hSeq = (pIdx : N) → isExactAt (hSeq pIdx) (hSeq (succ pIdx)) module _ where 0→_ : (A : Group ℓ) → GroupHom (UnitGroup {ℓ}) A @@ -95,8 +89,8 @@ module _ {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) where sesHSeq (suc (suc (suc zero)) , _) = C →0 sesHSeq (suc (suc (suc (suc n))) , p) = Cubical.Data.Empty.rec (¬-<-zero (≤-k+-cancel p)) - shortExactSeq2 : Type ℓ - shortExactSeq2 = finExactSeq sesGSeq sesHSeq + shortExactSeq5 : Type ℓ + shortExactSeq5 = finExactSeq sesGSeq sesHSeq module _ {A B : Group ℓ} (f : GroupHom A B) where open import Cubical.Data.Vec @@ -114,8 +108,8 @@ module _ {A B : Group ℓ} (f : GroupHom A B) where sesHSeq (suc (suc zero) , _) = B →0 sesHSeq (suc (suc (suc n)) , p) = Cubical.Data.Empty.rec (¬-<-zero (≤-k+-cancel p)) - shortExactSeq : Type ℓ - shortExactSeq = finExactSeq sesGSeq sesHSeq + shortExactSeq4 : Type ℓ + shortExactSeq4 = finExactSeq sesGSeq sesHSeq SES→isEquiv : {L R : Group ℓ-zero} → {G : Group ℓ} {H : Group ℓ'} @@ -237,3 +231,4 @@ transportExact4 {G = G} {G₂ = G₂} {H = H} {H₂ = H₂} {L = L} {L₂ = L₂ (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))) + \ No newline at end of file From 3a0ddb7e88c1c8956c58a8ab6c17ac6929493e3f Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 8 Nov 2024 00:02:41 -0600 Subject: [PATCH 6/9] working again --- Cubical/Algebra/Group/Exact.agda | 76 ++++++++++---------------------- Cubical/Algebra/Group/Five.agda | 14 +++--- 2 files changed, 31 insertions(+), 59 deletions(-) diff --git a/Cubical/Algebra/Group/Exact.agda b/Cubical/Algebra/Group/Exact.agda index d91f18ccd0..91834bd3dc 100644 --- a/Cubical/Algebra/Group/Exact.agda +++ b/Cubical/Algebra/Group/Exact.agda @@ -16,6 +16,7 @@ open import Cubical.Data.Nat.Order open import Cubical.Data.Sigma open import Cubical.Data.Sum open import Cubical.Data.Unit +open import Cubical.Data.Vec open import Cubical.Algebra.Group.Base open import Cubical.Algebra.Group.Morphisms @@ -35,25 +36,36 @@ SuccStr {ℓ = ℓ} = TypeWithStr ℓ λ A → (A → A) -- Exactness except the intersecting Group is only propositionally equal isWeakExactAt : {A B B' C : Group ℓ} (f : GroupHom A B) (g : GroupHom B' C) (p : B ≡ B') → Type ℓ isWeakExactAt {ℓ = ℓ} {B = B} {B' = B'} f g p = - (b : ⟨ B ⟩) → (isInKer g (subst (λ (a : Σ (Type ℓ) GroupStr) → fst a) p b) → isInIm f b) × (isInIm f b → isInKer g (subst fst p b)) + (b : ⟨ B ⟩) → isInKer g (subst (λ (a : Σ (Type ℓ) GroupStr) → fst a) p b) ≃ isInIm f b isExactAt : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) → Type ℓ -isExactAt {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b → isInIm f b) × (isInIm f b → isInKer g b) +isExactAt {B = B} f g = (b : ⟨ B ⟩) → isInKer g b ≃ isInIm f b -- TODO: Is exactness preserved across association? isWeakExactAtRefl : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) → isWeakExactAt f g refl ≡ isExactAt f g -isWeakExactAtRefl {ℓ = ℓ} {B = B} f g i = (b : ⟨ B ⟩) → (isInKer g (transportRefl b i) → isInIm f b) × (isInIm f b → isInKer g (transportRefl b i)) +isWeakExactAtRefl {ℓ = ℓ} {B = B} f g i = (b : ⟨ B ⟩) → (isInKer g (transportRefl b i)) ≃ (isInIm f b) --- Finite exact sequence +-- Exact sequence based on vec module _ where - finExactSeq : {len-2 : ℕ} - → (gSeq : (gIdx : Fin (suc (suc len-2))) → Group ℓ) - → (hSeq : (hIdx : Fin (suc len-2)) → GroupHom (gSeq (finj hIdx)) (gSeq (fsuc hIdx))) - → Type ℓ - finExactSeq {ℓ = ℓ} {len-2 = len-2} gSeq hSeq - = (pIdx : Fin len-2) → isExactAt (subst (λ n → GroupHom (gSeq (finj (finj pIdx))) (gSeq n)) (toℕ-injective refl) (hSeq (finj pIdx))) (hSeq (fsuc pIdx)) + 2+_ = λ (n : ℕ) → suc (suc n) + 3+_ = λ (n : ℕ) → suc (suc (suc n)) + + data HomVec {ℓ : Level} : {n : ℕ} → Vec (Group ℓ) (2+ n) → Type (ℓ-suc ℓ) where + -- This needs to at least have 1 group in it or else the suc case doesn't have + -- a previous group to index by + end : {A B : Group ℓ} → GroupHom A B → HomVec {n = 0} (B ∷ A ∷ []) + cons : {n : ℕ} {gv : Vec (Group ℓ) (suc n)} {A B : Group ℓ} + → GroupHom A B → HomVec {n = n} (A ∷ gv) → HomVec {n = suc n} (B ∷ A ∷ gv) + + data ExactSeqVec {ℓ : Level} : {n : ℕ} → {gs : Vec (Group ℓ) (3+ n)} → HomVec gs → Type (ℓ-suc ℓ) where + nil : {A B C : Group ℓ} {f : GroupHom A B} {g : GroupHom B C} + → isExactAt f g → ExactSeqVec (cons g (end f)) + cons : {n : ℕ} {gv : Vec (Group ℓ) (suc n)} {A B C : Group ℓ} + → {f : GroupHom A B} {g : GroupHom B C} {hv : HomVec (A ∷ gv)} + → isExactAt f g + → ExactSeqVec (cons f hv) → ExactSeqVec (cons g (cons f hv)) -- Exact sequence over successor structures module _ where @@ -71,46 +83,6 @@ module _ where _→0 : (A : Group ℓ) → GroupHom A (UnitGroup {ℓ}) A →0 = (λ _ → tt*) , record { pres· = λ x y → refl ; pres1 = refl ; presinv = λ x → refl } --- Short exact sequences -module _ {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) where - open import Cubical.Data.Vec - - private - sesGVec : Vec (Group ℓ) 5 - sesGVec = UnitGroup ∷ A ∷ B ∷ C ∷ UnitGroup ∷ [] - - sesGSeq : (gIdx : Fin 5) → Group ℓ - sesGSeq gIdx = lookup (Fin→FinData 5 gIdx) sesGVec - - sesHSeq : (hIdx : Fin 4) → GroupHom (sesGSeq (finj hIdx)) (sesGSeq (fsuc hIdx)) - sesHSeq (zero , _) = 0→ A - sesHSeq (suc zero , _) = f - sesHSeq (suc (suc zero) , _) = g - sesHSeq (suc (suc (suc zero)) , _) = C →0 - sesHSeq (suc (suc (suc (suc n))) , p) = Cubical.Data.Empty.rec (¬-<-zero (≤-k+-cancel p)) - - shortExactSeq5 : Type ℓ - shortExactSeq5 = finExactSeq sesGSeq sesHSeq - -module _ {A B : Group ℓ} (f : GroupHom A B) where - open import Cubical.Data.Vec - - private - sesGVec : Vec (Group ℓ) 4 - sesGVec = UnitGroup ∷ A ∷ B ∷ UnitGroup ∷ [] - - sesGSeq : (gIdx : Fin 4) → Group ℓ - sesGSeq gIdx = lookup (Fin→FinData 4 gIdx) sesGVec - - sesHSeq : (hIdx : Fin 3) → GroupHom (sesGSeq (finj hIdx)) (sesGSeq (fsuc hIdx)) - sesHSeq (zero , _) = 0→ A - sesHSeq (suc zero , _) = f - sesHSeq (suc (suc zero) , _) = B →0 - sesHSeq (suc (suc (suc n)) , p) = Cubical.Data.Empty.rec (¬-<-zero (≤-k+-cancel p)) - - shortExactSeq4 : Type ℓ - shortExactSeq4 = finExactSeq sesGSeq sesHSeq - SES→isEquiv : {L R : Group ℓ-zero} → {G : Group ℓ} {H : Group ℓ'} → UnitGroup₀ ≡ L @@ -230,5 +202,5 @@ transportExact4 {G = G} {G₂ = G₂} {H = H} {H₂ = H₂} {L = L} {L₂ = L₂ (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))) - - \ No newline at end of file + + \ No newline at end of file diff --git a/Cubical/Algebra/Group/Five.agda b/Cubical/Algebra/Group/Five.agda index 3224c67c29..127d7833ac 100644 --- a/Cubical/Algebra/Group/Five.agda +++ b/Cubical/Algebra/Group/Five.agda @@ -69,7 +69,7 @@ module _ rest : (b : ⟨ B ⟩) → (g .fst b ≡ c) → goalTy - goal = untrunc (map (λ x → rest (fst x) (snd x)) c-in-im[g]) + goal = untrunc (PT.map (λ x → rest (fst x) (snd x)) c-in-im[g]) rest b g[b]≡c = goal2 where @@ -94,8 +94,8 @@ module _ rest2 : (a' : ⟨ A' ⟩) → (r .fst a' ≡ m[b]) → (a : ⟨ A ⟩) → l .fst a ≡ a' → goalTy goal2 = - let inner = λ x → untrunc (map (λ y → rest2 (x .fst) (x .snd) (y .fst) (y .snd)) (lSurj (x .fst))) in - untrunc (map inner m[b]-in-im[r]) + let inner = λ x → untrunc (PT.map (λ y → rest2 (x .fst) (x .snd) (y .fst) (y .snd)) (lSurj (x .fst))) in + untrunc (PT.map inner m[b]-in-im[r]) rest2 a' r[a']≡m[b] a l[a]≡a' = c≡0 where @@ -118,7 +118,7 @@ module _ f[a]-in-im[f] = ∣ a , refl ∣₁ f[a]-in-ker[g] : isInKer g (f .fst a) - f[a]-in-ker[g] = fg (f .fst a) .snd f[a]-in-im[f] + f[a]-in-ker[g] = invIsEq (fg (f .fst a) .snd) f[a]-in-im[f] g[f[a]]≡0 : g .fst (f .fst a) ≡ C .snd .GroupStr.1g g[f[a]]≡0 = f[a]-in-ker[g] @@ -158,7 +158,7 @@ module _ u[p[d]]≡q[j[d]] = sq4 d d'-in-ker[u] : isInKer u d' - d'-in-ker[u] = let im[t]→ker[u] = tu d' .snd in + d'-in-ker[u] = let im[t]→ker[u] = invIsEq (tu d' .snd) in im[t]→ker[u] ∣ (c' , refl) ∣₁ u[p[d]]≡0 : u[p[d]] ≡ E' .snd .GroupStr.1g @@ -180,7 +180,7 @@ module _ rest : (c : ⟨ C ⟩) → h .fst c ≡ d → goalTy - goal = untrunc (map (λ x → rest (x .fst) (x .snd)) d-in-im[h]) + goal = untrunc (PT.map (λ x → rest (x .fst) (x .snd)) d-in-im[h]) rest c h[c]≡d = goal2 where n[c] : ⟨ C' ⟩ @@ -222,7 +222,7 @@ module _ rest2 : (b' : ⟨ B' ⟩) → s .fst b' ≡ c'-n[c] → goalTy - goal2 = untrunc (map (λ x → rest2 (x .fst) (x .snd)) [c'-n[c]]-in-im[s]) + goal2 = untrunc (PT.map (λ x → rest2 (x .fst) (x .snd)) [c'-n[c]]-in-im[s]) rest2 b' s[b']≡c'-n[c] = goal3 where mGroupIso = BijectionIso→GroupIso m From e3fcc00673de49b2f52935d2628f492f9124bab1 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 8 Nov 2024 01:29:50 -0600 Subject: [PATCH 7/9] fix whitespace... --- Cubical/Algebra/Group/Exact.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Cubical/Algebra/Group/Exact.agda b/Cubical/Algebra/Group/Exact.agda index 91834bd3dc..11a7eba624 100644 --- a/Cubical/Algebra/Group/Exact.agda +++ b/Cubical/Algebra/Group/Exact.agda @@ -202,5 +202,4 @@ transportExact4 {G = G} {G₂ = G₂} {H = H} {H₂ = H₂} {L = L} {L₂ = L₂ (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))) - - \ No newline at end of file + From 07c87ff8db098599ef9b8273caf22a2b19cdad00 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 3 Dec 2024 17:20:08 -0600 Subject: [PATCH 8/9] clean up, just five --- Cubical/Algebra/Group/Exact.agda | 46 +++----------------------------- Cubical/Algebra/Group/Five.agda | 4 +-- 2 files changed, 6 insertions(+), 44 deletions(-) diff --git a/Cubical/Algebra/Group/Exact.agda b/Cubical/Algebra/Group/Exact.agda index 11a7eba624..36f23a5d47 100644 --- a/Cubical/Algebra/Group/Exact.agda +++ b/Cubical/Algebra/Group/Exact.agda @@ -35,53 +35,15 @@ SuccStr {ℓ = ℓ} = TypeWithStr ℓ λ A → (A → A) -- Exactness except the intersecting Group is only propositionally equal isWeakExactAt : {A B B' C : Group ℓ} (f : GroupHom A B) (g : GroupHom B' C) (p : B ≡ B') → Type ℓ -isWeakExactAt {ℓ = ℓ} {B = B} {B' = B'} f g p = - (b : ⟨ B ⟩) → isInKer g (subst (λ (a : Σ (Type ℓ) GroupStr) → fst a) p b) ≃ isInIm f b +isWeakExactAt {ℓ = ℓ} {B = B} {B' = B'} f g p = (b : ⟨ B ⟩) → (isInKer g (tr b) → isInIm f b) × (isInIm f b → isInKer g (tr b)) where + tr = λ (b : ⟨ B ⟩) → subst (λ (a : Σ (Type ℓ) GroupStr) → fst a) p b isExactAt : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) → Type ℓ -isExactAt {B = B} f g = (b : ⟨ B ⟩) → isInKer g b ≃ isInIm f b - --- TODO: Is exactness preserved across association? +isExactAt {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b → isInIm f b) × (isInIm f b → isInKer g b) isWeakExactAtRefl : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) → isWeakExactAt f g refl ≡ isExactAt f g -isWeakExactAtRefl {ℓ = ℓ} {B = B} f g i = (b : ⟨ B ⟩) → (isInKer g (transportRefl b i)) ≃ (isInIm f b) - --- Exact sequence based on vec -module _ where - 2+_ = λ (n : ℕ) → suc (suc n) - 3+_ = λ (n : ℕ) → suc (suc (suc n)) - - data HomVec {ℓ : Level} : {n : ℕ} → Vec (Group ℓ) (2+ n) → Type (ℓ-suc ℓ) where - -- This needs to at least have 1 group in it or else the suc case doesn't have - -- a previous group to index by - end : {A B : Group ℓ} → GroupHom A B → HomVec {n = 0} (B ∷ A ∷ []) - cons : {n : ℕ} {gv : Vec (Group ℓ) (suc n)} {A B : Group ℓ} - → GroupHom A B → HomVec {n = n} (A ∷ gv) → HomVec {n = suc n} (B ∷ A ∷ gv) - - data ExactSeqVec {ℓ : Level} : {n : ℕ} → {gs : Vec (Group ℓ) (3+ n)} → HomVec gs → Type (ℓ-suc ℓ) where - nil : {A B C : Group ℓ} {f : GroupHom A B} {g : GroupHom B C} - → isExactAt f g → ExactSeqVec (cons g (end f)) - cons : {n : ℕ} {gv : Vec (Group ℓ) (suc n)} {A B C : Group ℓ} - → {f : GroupHom A B} {g : GroupHom B C} {hv : HomVec (A ∷ gv)} - → isExactAt f g - → ExactSeqVec (cons f hv) → ExactSeqVec (cons g (cons f hv)) - --- Exact sequence over successor structures -module _ where - exactSeq : (ss @ (N , succ) : SuccStr {ℓ = ℓ}) - → (gSeq : (gIdx : N) → Group ℓ') - → (hSeq : (hIdx : N) → GroupHom (gSeq hIdx) (gSeq (succ hIdx))) - → Type (ℓ-max ℓ ℓ') - exactSeq (N , succ) gSeq hSeq = (pIdx : N) → isExactAt (hSeq pIdx) (hSeq (succ pIdx)) - -module _ where - 0→_ : (A : Group ℓ) → GroupHom (UnitGroup {ℓ}) A - 0→ A = let open GroupStr (A .snd) in - (λ _ → 1g) , record { pres· = λ x y → sym (·IdR 1g) ; pres1 = refl ; presinv = λ x → sym (·InvL 1g) ∙ ·IdR (inv 1g) } - - _→0 : (A : Group ℓ) → GroupHom A (UnitGroup {ℓ}) - A →0 = (λ _ → tt*) , record { pres· = λ x y → refl ; pres1 = refl ; presinv = λ x → refl } +isWeakExactAtRefl {ℓ = ℓ} {B = B} f g i = (b : ⟨ B ⟩) → (isInKer g (transportRefl b i) → isInIm f b) × (isInIm f b → isInKer g (transportRefl b i)) SES→isEquiv : {L R : Group ℓ-zero} → {G : Group ℓ} {H : Group ℓ'} diff --git a/Cubical/Algebra/Group/Five.agda b/Cubical/Algebra/Group/Five.agda index 127d7833ac..47c8d1f47c 100644 --- a/Cubical/Algebra/Group/Five.agda +++ b/Cubical/Algebra/Group/Five.agda @@ -118,7 +118,7 @@ module _ f[a]-in-im[f] = ∣ a , refl ∣₁ f[a]-in-ker[g] : isInKer g (f .fst a) - f[a]-in-ker[g] = invIsEq (fg (f .fst a) .snd) f[a]-in-im[f] + f[a]-in-ker[g] = fg (f .fst a) .snd f[a]-in-im[f] g[f[a]]≡0 : g .fst (f .fst a) ≡ C .snd .GroupStr.1g g[f[a]]≡0 = f[a]-in-ker[g] @@ -158,7 +158,7 @@ module _ u[p[d]]≡q[j[d]] = sq4 d d'-in-ker[u] : isInKer u d' - d'-in-ker[u] = let im[t]→ker[u] = invIsEq (tu d' .snd) in + d'-in-ker[u] = let im[t]→ker[u] = tu d' .snd in im[t]→ker[u] ∣ (c' , refl) ∣₁ u[p[d]]≡0 : u[p[d]] ≡ E' .snd .GroupStr.1g From 6363fa428ccf9628b19d7ac930ab4d55541cc62f Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 6 Dec 2024 17:33:06 -0600 Subject: [PATCH 9/9] clean up --- Cubical/Algebra/Group/Exact.agda | 3 --- 1 file changed, 3 deletions(-) diff --git a/Cubical/Algebra/Group/Exact.agda b/Cubical/Algebra/Group/Exact.agda index 36f23a5d47..ecc16ed5ec 100644 --- a/Cubical/Algebra/Group/Exact.agda +++ b/Cubical/Algebra/Group/Exact.agda @@ -30,9 +30,6 @@ private variable ℓ ℓ' : Level -SuccStr : Type (ℓ-suc ℓ) -SuccStr {ℓ = ℓ} = TypeWithStr ℓ λ A → (A → A) - -- Exactness except the intersecting Group is only propositionally equal isWeakExactAt : {A B B' C : Group ℓ} (f : GroupHom A B) (g : GroupHom B' C) (p : B ≡ B') → Type ℓ isWeakExactAt {ℓ = ℓ} {B = B} {B' = B'} f g p = (b : ⟨ B ⟩) → (isInKer g (tr b) → isInIm f b) × (isInIm f b → isInKer g (tr b)) where