From e02f49c46df6d4583bcc1b92f88d733675afc235 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 5 Nov 2024 01:08:16 -0600 Subject: [PATCH] wip --- src/Misc/{ => FiveLemma}/Exact.agda | 0 src/Misc/{ => FiveLemma}/FiveLemma.agda | 0 src/Misc/FiveLemma/FiveLemmaGroup.lagda.md | 195 +++++++++++++++++++++ src/Misc/FiveLemma/GroupMorphisms.agda | 61 +++++++ src/Misc/{ => FiveLemma}/SnakeLemma.agda | 0 src/Misc/FiveLemmaGroup.lagda.md | 113 ------------ 6 files changed, 256 insertions(+), 113 deletions(-) rename src/Misc/{ => FiveLemma}/Exact.agda (100%) rename src/Misc/{ => FiveLemma}/FiveLemma.agda (100%) create mode 100644 src/Misc/FiveLemma/FiveLemmaGroup.lagda.md create mode 100644 src/Misc/FiveLemma/GroupMorphisms.agda rename src/Misc/{ => FiveLemma}/SnakeLemma.agda (100%) delete mode 100644 src/Misc/FiveLemmaGroup.lagda.md diff --git a/src/Misc/Exact.agda b/src/Misc/FiveLemma/Exact.agda similarity index 100% rename from src/Misc/Exact.agda rename to src/Misc/FiveLemma/Exact.agda diff --git a/src/Misc/FiveLemma.agda b/src/Misc/FiveLemma/FiveLemma.agda similarity index 100% rename from src/Misc/FiveLemma.agda rename to src/Misc/FiveLemma/FiveLemma.agda diff --git a/src/Misc/FiveLemma/FiveLemmaGroup.lagda.md b/src/Misc/FiveLemma/FiveLemmaGroup.lagda.md new file mode 100644 index 0000000..ab2b6f9 --- /dev/null +++ b/src/Misc/FiveLemma/FiveLemmaGroup.lagda.md @@ -0,0 +1,195 @@ +``` +{-# OPTIONS --cubical #-} + +module Misc.FiveLemma.FiveLemmaGroup where + +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Group.GroupPath +open import Cubical.Algebra.Group.Instances.Unit +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Algebra.Group.Properties +open import Cubical.Algebra.Monoid +open import Cubical.Algebra.Semigroup +open import Cubical.Data.Unit +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Structure +open import Cubical.HITs.PropositionalTruncation.Base +open import Cubical.HITs.PropositionalTruncation.Properties + renaming (rec to propTruncRec ; map to propTruncMap ; rec2 to propTruncRec2 ; map2 to propTruncMap2 ; elim to propTruncElim) +open import Cubical.HITs.Pushout.Base +open import Cubical.HITs.Pushout + +open import Misc.FiveLemma.GroupMorphisms + +open BijectionIso' +open IsGroupHom +open GroupStr using (1g) + +private + variable + ℓ ℓ' : Level + +isExact : {A B C : Group ℓ} → (f : GroupHom A B) → (g : GroupHom B C) → Type ℓ +isExact {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b) ≃ (isInIm' f b) + +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 : isExact f g) (gh : isExact g h) (hj : isExact h j) + (rs : isExact r s) (st : isExact s t) (tu : isExact t u) + (lEpi : isSurjective' l) + (qMono : isMono 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 + + sur : isSurjective' n + -- Let c′ be an element of C′. + sur c' = + let + d' : ⟨ D' ⟩ + d' = t .fst c' + + -- Since p is surjective, there exists an element d in D with p(d) = t(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] = invIsEq (tu d' .snd) in + im[t]→ker[u] (c' , refl) + + u[p[d]]≡0 : u[p[d]] ≡ E' .snd .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 .1g + q[j[d]]≡0 = sym u[p[d]]≡q[j[d]] ∙ u[p[d]]≡0 + + j[d]≡0 : j[d] ≡ E .snd .1g + j[d]≡0 = qMono (q[j[d]]≡0 ∙ sym (q .snd .IsGroupHom.pres1)) + + 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] + + c : ⟨ C ⟩ + c = d-in-im[h] .fst + + h[c]≡d : h .fst c ≡ d + h[c]≡d = d-in-im[h] .snd + + 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 .1g + t[c'-n[c]]≡0 = + let open GroupStr (C' .snd) renaming (_·_ to _·ᶜ_; inv to invᶜ) in + let open GroupStr (D' .snd) renaming (_·_ to _·ᵈ_; inv to invᵈ) 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 (C' .snd .1g) ≡⟨ t .snd .pres1 ⟩ + D' .snd .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] + + b' : ⟨ B' ⟩ + b' = [c'-n[c]]-in-im[s] .fst + + s[b']≡c'-n[c] : s .fst b' ≡ c'-n[c] + s[b']≡c'-n[c] = [c'-n[c]]-in-im[s] .snd + + 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] + + n[g[b]] : ⟨ C' ⟩ + n[g[b]] = n .fst (g .fst 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' + in c , {! !} + + mono : isMono n + mono x = {! !} + + lemma : isIso (n .fst) + lemma = gg , {! !} , {! !} where + gg : C' .fst → C .fst + gg c' = {! !} + +``` diff --git a/src/Misc/FiveLemma/GroupMorphisms.agda b/src/Misc/FiveLemma/GroupMorphisms.agda new file mode 100644 index 0000000..84516ed --- /dev/null +++ b/src/Misc/FiveLemma/GroupMorphisms.agda @@ -0,0 +1,61 @@ +{-# OPTIONS --cubical #-} + +-- I'm doing this just because isInIm is defined to be a mere prop +-- Not sure why it's defined this way yet +-- TODO: Find out + +module Misc.FiveLemma.GroupMorphisms where + +open import Agda.Primitive +open import Cubical.Algebra.Group +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Algebra.Semigroup +open import Cubical.Data.Sigma +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Structure +open import Cubical.HITs.PropositionalTruncation + +private + variable + ℓ ℓ' : Level + G H : Group ℓ + +isInIm' : GroupHom G H → ⟨ H ⟩ → Type _ +isInIm' {G = G} ϕ h = Σ[ g ∈ ⟨ G ⟩ ] ϕ .fst g ≡ h + +Im' : GroupHom G H → Type _ +Im' {H = H} ϕ = Σ[ x ∈ ⟨ H ⟩ ] isInIm' ϕ x + +isSurjective' : GroupHom G H → Type _ +isSurjective' {H = H} ϕ = (x : ⟨ H ⟩) → isInIm' ϕ x + +-- Group bijections +record BijectionIso' (G : Group ℓ) (H : Group ℓ') : Type (ℓ-max ℓ ℓ') where + constructor bijIso' + + field + fun : GroupHom G H + inj : isInjective fun + surj : isSurjective' fun + +module _ where + open GroupStr + open BijectionIso' + + BijectionIso'→GroupIso : BijectionIso' G H → GroupIso G H + BijectionIso'→GroupIso {G = G} {H = H} i = grIso + where + f = fst (fun i) + + helper : (b : _) → isProp (Σ[ a ∈ ⟨ G ⟩ ] f a ≡ b) + helper _ (a , ha) (b , hb) = + Σ≡Prop (λ _ → is-set (snd H) _ _) + (isInjective→isMono (fun i) (inj i) (ha ∙ sym hb) ) + + grIso : GroupIso G H + grIso = iso f g fg gf , snd (fun i) where + g = λ b → rec (helper b) (λ a → a) ∣ (surj i b) ∣₁ .fst + fg = λ b → rec (helper b) (λ a → a) ∣ (surj i b) ∣₁ .snd + gf = λ b j → rec (helper (f b)) (λ a → a) (squash₁ ∣ (surj i (f b)) ∣₁ ∣ (b , refl) ∣₁ j) .fst \ No newline at end of file diff --git a/src/Misc/SnakeLemma.agda b/src/Misc/FiveLemma/SnakeLemma.agda similarity index 100% rename from src/Misc/SnakeLemma.agda rename to src/Misc/FiveLemma/SnakeLemma.agda diff --git a/src/Misc/FiveLemmaGroup.lagda.md b/src/Misc/FiveLemmaGroup.lagda.md deleted file mode 100644 index 8324ea3..0000000 --- a/src/Misc/FiveLemmaGroup.lagda.md +++ /dev/null @@ -1,113 +0,0 @@ -``` -{-# OPTIONS --cubical #-} - -module Misc.FiveLemmaGroup where - -open import Cubical.Algebra.Group.Base -open import Cubical.Algebra.Group.GroupPath -open import Cubical.Algebra.Group.Instances.Unit -open import Cubical.Algebra.Group.MorphismProperties -open import Cubical.Algebra.Group.Morphisms -open import Cubical.Algebra.Group.Properties -open import Cubical.Data.Unit -open import Cubical.Foundations.Equiv -open import Cubical.Foundations.Function -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Structure -open import Cubical.HITs.PropositionalTruncation.Base -open import Cubical.HITs.PropositionalTruncation.Properties - renaming (rec to propTruncRec ; map to propTruncMap ; rec2 to propTruncRec2 ; map2 to propTruncMap2 ; elim to propTruncElim) -open import Cubical.HITs.Pushout.Base -open import Cubical.HITs.Pushout - -open BijectionIso -open GroupStr - -private - variable - ℓ ℓ' : Level - -isExact : {A B C : Group ℓ} → (f : GroupHom A B) → (g : GroupHom B C) → Type ℓ -isExact f g = Ker g ≃ Im f - -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 : isExact f g) (gh : isExact g h) (hj : isExact h j) - (rs : isExact r s) (st : isExact s t) (tu : isExact t u) - (lEpi : isSurjective l) - (qMono : isMono 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 - - sur : isSurjective n - -- Let c′ be an element of C′. - sur c' = - let - d' : fst D' - d' = t .fst c' - - -- Since p is surjective, there exists an element d in D with p(d) = t(c′). - d : ∥ ⟨ D ⟩ ∥₁ - d = propTruncMap fst (p .surj d') - - -- By commutativity of the diagram, u(p(d)) = q(j(d)). - u[p[d]] : ∥ ⟨ E' ⟩ ∥₁ - u[p[d]] = propTruncMap (λ d → u .fst (p .fun .fst d)) d - - u[t[c']] : ∥ ⟨ E' ⟩ ∥₁ - u[t[c']] = ∣ (u .fst (t .fst c')) ∣₁ - - u[p[d]]≡u[t[c']] : u[p[d]] ≡ u[t[c']] - u[p[d]]≡u[t[c']] = squash₁ u[p[d]] u[t[c']] - - q[j[d]] : ∥ ⟨ E' ⟩ ∥₁ - q[j[d]] = propTruncMap2 (λ e' d → subst (λ _ → ⟨ E' ⟩) (sq4 d) e') u[p[d]] d - - u[p[d]]≡q[j[d]] : u[p[d]] ≡ q[j[d]] - u[p[d]]≡q[j[d]] = squash₁ u[p[d]] q[j[d]] - - j[d] = ∥ ⟨ E ⟩ ∥₁ - j[d] = propTruncMap (λ d → j .fst d) d - - -- Since im t = ker u by exactness, 0 = u(t(c′)) = u(p(d)) = q(j(d)). - - -- d' is in the kernel of u - d'-ker-u : Ker u - d'-ker-u = invIsEq (tu .snd) (d' , ∣ (c' , refl) ∣₁) - - u[t[c']]≡0 : isInKer u (fst d'-ker-u) - u[t[c']]≡0 = snd d'-ker-u - - q[j[d]]≡0 : q[j[d]] ≡ ∣ (E' .snd .1g) ∣₁ - q[j[d]]≡0 = squash₁ q[j[d]] ∣ (E' .snd .1g) ∣₁ - -- q[j[d]]≡0 = sym u[p[d]]≡q[j[d]] ∙ {! !} ∙ cong ∣_∣₁ u[t[c']]≡0 - - j[d]≡0 : j[d] ≡ ∣ (E .snd .1g) ∣₁ - j[d]≡0 = {! !} - in - - -- let pSurj = p .surj in - -- let t[c'] = t .fst c' in - -- let step1 = pSurj t[c'] in - -- let d-thing = snd D in - -- let d-is-group = isPropIsGroup {! !} {! !} {! !} in - -- let step2 = propTruncRec {! !} (λ x → fst x) step1 in - {! !} - - mono : isMono n - mono x = {! !} - - lemma : isIso (n .fst) - lemma = gg , {! !} , {! !} where - gg : C' .fst → C .fst - gg c' = {! !} - -``` \ No newline at end of file