# HG changeset patch # User Shinji KONO # Date 1694664197 -32400 # Node ID 4dd130b93b210cf9a4fe16bc3bf585af8defe3ce # Parent 76c80a6ad4e66bdb1f4443260193d75bc797f654 ... diff -r 76c80a6ad4e6 -r 4dd130b93b21 src/Homomorphism.agda --- a/src/Homomorphism.agda Mon Sep 11 16:08:09 2023 +0900 +++ b/src/Homomorphism.agda Thu Sep 14 13:03:17 2023 +0900 @@ -32,7 +32,7 @@ -- -- f -- G --→ H --- | / +-- | ↗ -- φ | / h -- ↓ / -- G/K @@ -61,8 +61,7 @@ open NormalSubGroup N open EqReasoning (Algebra.Group.setoid A) open Gutil A - open aNeq - -- + open aNeq -- -- (aN)(bN) = a(Nb)N = a(bN)N = (ab)NN = (ab)N. -- -- a =n= b ↔ a . b ⁻¹ ∈ N @@ -108,7 +107,7 @@ b ∙ n ≈⟨ car (gsym eq) ⟩ a ∙ n ≈⟨ eq1 ⟩ x ∎ - aneq : {a b : Carrier } → a ≈ b → aNeq N a b + aneq : {a b : Carrier } → a ≈ b → aNeq N a b -- a ≈ b → aN ≈ bN aneq {a} {b} eq = record { eq→ = λ {x} lt → an-cong eq lt ; eq← = λ lt → an-cong (gsym eq) lt } _=n=_ = aNeq N @@ -120,6 +119,9 @@ ntrans {x} {y} {z} x=y y=z = record { eq→ = λ {lt} ix → eq→ y=z (eq→ x=y ix) ; eq← = λ {lt} ix → eq← x=y (eq← y=z ix) } +-- factor group has the same carrier as the original group +-- so h = f + _/_ : {c d : Level} (A : Group c d ) (N : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) _/_ A N = record { Carrier = Group.Carrier A @@ -132,8 +134,7 @@ ; trans = ntrans ; sym = λ a=b → nsym a=b } ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gk00 x=y u=v } - ; assoc = gkassoc } - ; identity = (λ a → aneq (proj₁ identity _)) , (λ a → aneq (proj₂ identity _) ) } + ; assoc = gkassoc } ; identity = (λ a → aneq (proj₁ identity _)) , (λ a → aneq (proj₂ identity _) ) } ; inverse = (λ a → aneq (proj₁ inverse _)) , (λ x → aneq (proj₂ inverse _) ) ; ⁻¹-cong = gkcong⁻¹ } diff -r 76c80a6ad4e6 -r 4dd130b93b21 src/NormalSubGroup.agda --- a/src/NormalSubGroup.agda Mon Sep 11 16:08:09 2023 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,116 +0,0 @@ -{-# OPTIONS --allow-unsolved-metas #-} -open import Level hiding ( suc ; zero ) -module NormalSubgroup where - -open import Algebra -open import Algebra.Structures -open import Algebra.Definitions -open import Data.Product -open import Relation.Binary.PropositionalEquality -open import Algebra.Morphism.Structures -open import Data.Empty -open import Relation.Nullary - -open GroupMorphisms - -GR : {c l : Level } → Group c l → RawGroup c l -GR G = record { - Carrier = Carrier G - ; _≈_ = _≈_ G - ; _∙_ = _∙_ G - ; ε = ε G - ; _⁻¹ = _⁻¹ G - } where open Group - -record GAxiom {c l : Level } (G : Group c l) : Set ( c Level.⊔ l ) where - open Group G - field - ∙-cong : {x y u v : Carrier } → x ≈ y → u ≈ v → x ∙ u ≈ y ∙ v - assoc : (x y z : Carrier ) → x ∙ y ∙ z ≈ x ∙ ( y ∙ z ) - identity : ((y : Carrier) → ε ∙ y ≈ y ) × ((y : Carrier) → y ∙ ε ≈ y ) - inverse : ((y : Carrier) → y ⁻¹ ∙ y ≈ ε ) × ((y : Carrier) → y ∙ y ⁻¹ ≈ ε ) - ⁻¹-cong : {x y : Carrier } → x ≈ y → x ⁻¹ ≈ y ⁻¹ - -GA : {c l : Level } → (G : Group c l) → GAxiom G -GA G = record { - ∙-cong = IsMagma.∙-cong ( IsSemigroup.isMagma ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup))) - ; assoc = IsSemigroup.assoc ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup)) - ; identity = IsMonoid.identity ( IsGroup.isMonoid isGroup) - ; inverse = IsGroup.inverse isGroup - ; ⁻¹-cong = IsGroup.⁻¹-cong isGroup - } where open Group G - -open import Relation.Binary.Structures - -Eq : {c l : Level } → (G : Group c l) → IsEquivalence _ -Eq G = IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup - (IsGroup.isMonoid (Group.isGroup G ))) ) - -_<_∙_> : {c d : Level} (m : Group c d ) → Group.Carrier m → Group.Carrier m → Group.Carrier m -m < x ∙ y > = Group._∙_ m x y - -_<_≈_> : {c d : Level} (m : Group c d ) → (f g : Group.Carrier m ) → Set d -m < x ≈ y > = Group._≈_ m x y - -infixr 9 _<_∙_> - -record SubGroup {l c d : Level} (A : Group c d ) : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where - open Group A - field - P : Carrier → Set l - Pε : P ε - P⁻¹ : (a : Carrier ) → P a → P (a ⁻¹) - P≈ : {a b : Carrier } → a ≈ b → P a → P b - P∙ : {a b : Carrier } → P a → P b → P ( a ∙ b ) - --- assuming Homomorphism is too strong --- -record NormalSubGroup {l c d : Level} (A : Group c d ) : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where - open Group A - field - Psub : SubGroup {l} A - -- gN ≈ Ng - Pcomm : {a b : Carrier } → SubGroup.P Psub a → SubGroup.P Psub ( b ∙ ( a ∙ b ⁻¹ ) ) - P : Carrier → Set l - P = SubGroup.P Psub - Pε : P ε - Pε = SubGroup.Pε Psub - P⁻¹ : (a : Carrier ) → P a → P (a ⁻¹) - P⁻¹ = SubGroup.P⁻¹ Psub - P≈ : {a b : Carrier } → a ≈ b → P a → P b - P≈ = SubGroup.P≈ Psub - P∙ : {a b : Carrier } → P a → P b → P ( a ∙ b ) - P∙ = SubGroup.P∙ Psub - -import Relation.Binary.Reasoning.Setoid as EqReasoning - -record Nelm {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) : Set (Level.suc e ⊔ (Level.suc c ⊔ d)) where - open Group A - open SubGroup n - field - elm : Carrier - Pelm : P elm - -SGroup : {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) → Group (Level.suc e ⊔ (Level.suc c ⊔ d)) d -SGroup {_} {_} {_} A n = record { - Carrier = Nelm A n - ; _≈_ = λ x y → elm x ≈ elm y - ; _∙_ = λ x y → record { elm = elm x ∙ elm y ; Pelm = P∙ (Pelm x) (Pelm y) } - ; ε = record { elm = ε ; Pelm = Pε } - ; _⁻¹ = λ x → record { elm = (elm x) ⁻¹ ; Pelm = P⁻¹ (elm x) (Pelm x) } - ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { - isEquivalence = record { refl = IsEquivalence.refl (IsGroup.isEquivalence ga) - ; sym = IsEquivalence.sym (IsGroup.isEquivalence ga) - ; trans = IsEquivalence.trans (IsGroup.isEquivalence ga) } - ; ∙-cong = IsGroup.∙-cong ga } - ; assoc = λ a b c → IsGroup.assoc ga (elm a) (elm b) (elm c) } - ; identity = ( (λ q → proj₁ (IsGroup.identity ga) (elm q)) , (λ q → proj₂ (IsGroup.identity ga) (elm q)) ) } - ; inverse = ( (λ q → proj₁ (IsGroup.inverse ga) (elm q)) , (λ q → proj₂ (IsGroup.inverse ga) (elm q)) ) - ; ⁻¹-cong = IsGroup.⁻¹-cong ga } - } where - open Group A - open SubGroup n - open Nelm - ga = Group.isGroup A - - diff -r 76c80a6ad4e6 -r 4dd130b93b21 src/NormalSubgroup.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/NormalSubgroup.agda Thu Sep 14 13:03:17 2023 +0900 @@ -0,0 +1,116 @@ +{-# OPTIONS --allow-unsolved-metas #-} +open import Level hiding ( suc ; zero ) +module NormalSubgroup where + +open import Algebra +open import Algebra.Structures +open import Algebra.Definitions +open import Data.Product +open import Relation.Binary.PropositionalEquality +open import Algebra.Morphism.Structures +open import Data.Empty +open import Relation.Nullary + +open GroupMorphisms + +GR : {c l : Level } → Group c l → RawGroup c l +GR G = record { + Carrier = Carrier G + ; _≈_ = _≈_ G + ; _∙_ = _∙_ G + ; ε = ε G + ; _⁻¹ = _⁻¹ G + } where open Group + +record GAxiom {c l : Level } (G : Group c l) : Set ( c Level.⊔ l ) where + open Group G + field + ∙-cong : {x y u v : Carrier } → x ≈ y → u ≈ v → x ∙ u ≈ y ∙ v + assoc : (x y z : Carrier ) → x ∙ y ∙ z ≈ x ∙ ( y ∙ z ) + identity : ((y : Carrier) → ε ∙ y ≈ y ) × ((y : Carrier) → y ∙ ε ≈ y ) + inverse : ((y : Carrier) → y ⁻¹ ∙ y ≈ ε ) × ((y : Carrier) → y ∙ y ⁻¹ ≈ ε ) + ⁻¹-cong : {x y : Carrier } → x ≈ y → x ⁻¹ ≈ y ⁻¹ + +GA : {c l : Level } → (G : Group c l) → GAxiom G +GA G = record { + ∙-cong = IsMagma.∙-cong ( IsSemigroup.isMagma ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup))) + ; assoc = IsSemigroup.assoc ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup)) + ; identity = IsMonoid.identity ( IsGroup.isMonoid isGroup) + ; inverse = IsGroup.inverse isGroup + ; ⁻¹-cong = IsGroup.⁻¹-cong isGroup + } where open Group G + +open import Relation.Binary.Structures + +Eq : {c l : Level } → (G : Group c l) → IsEquivalence _ +Eq G = IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup + (IsGroup.isMonoid (Group.isGroup G ))) ) + +_<_∙_> : {c d : Level} (m : Group c d ) → Group.Carrier m → Group.Carrier m → Group.Carrier m +m < x ∙ y > = Group._∙_ m x y + +_<_≈_> : {c d : Level} (m : Group c d ) → (f g : Group.Carrier m ) → Set d +m < x ≈ y > = Group._≈_ m x y + +infixr 9 _<_∙_> + +record SubGroup {l c d : Level} (A : Group c d ) : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where + open Group A + field + P : Carrier → Set l + Pε : P ε + P⁻¹ : (a : Carrier ) → P a → P (a ⁻¹) + P≈ : {a b : Carrier } → a ≈ b → P a → P b + P∙ : {a b : Carrier } → P a → P b → P ( a ∙ b ) + +-- assuming Homomorphism is too strong +-- +record NormalSubGroup {l c d : Level} (A : Group c d ) : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where + open Group A + field + Psub : SubGroup {l} A + -- gN ≈ Ng + Pcomm : {a b : Carrier } → SubGroup.P Psub a → SubGroup.P Psub ( b ∙ ( a ∙ b ⁻¹ ) ) + P : Carrier → Set l + P = SubGroup.P Psub + Pε : P ε + Pε = SubGroup.Pε Psub + P⁻¹ : (a : Carrier ) → P a → P (a ⁻¹) + P⁻¹ = SubGroup.P⁻¹ Psub + P≈ : {a b : Carrier } → a ≈ b → P a → P b + P≈ = SubGroup.P≈ Psub + P∙ : {a b : Carrier } → P a → P b → P ( a ∙ b ) + P∙ = SubGroup.P∙ Psub + +import Relation.Binary.Reasoning.Setoid as EqReasoning + +record Nelm {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) : Set (Level.suc e ⊔ (Level.suc c ⊔ d)) where + open Group A + open SubGroup n + field + elm : Carrier + Pelm : P elm + +SGroup : {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) → Group (Level.suc e ⊔ (Level.suc c ⊔ d)) d +SGroup {_} {_} {_} A n = record { + Carrier = Nelm A n + ; _≈_ = λ x y → elm x ≈ elm y + ; _∙_ = λ x y → record { elm = elm x ∙ elm y ; Pelm = P∙ (Pelm x) (Pelm y) } + ; ε = record { elm = ε ; Pelm = Pε } + ; _⁻¹ = λ x → record { elm = (elm x) ⁻¹ ; Pelm = P⁻¹ (elm x) (Pelm x) } + ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { + isEquivalence = record { refl = IsEquivalence.refl (IsGroup.isEquivalence ga) + ; sym = IsEquivalence.sym (IsGroup.isEquivalence ga) + ; trans = IsEquivalence.trans (IsGroup.isEquivalence ga) } + ; ∙-cong = IsGroup.∙-cong ga } + ; assoc = λ a b c → IsGroup.assoc ga (elm a) (elm b) (elm c) } + ; identity = ( (λ q → proj₁ (IsGroup.identity ga) (elm q)) , (λ q → proj₂ (IsGroup.identity ga) (elm q)) ) } + ; inverse = ( (λ q → proj₁ (IsGroup.inverse ga) (elm q)) , (λ q → proj₂ (IsGroup.inverse ga) (elm q)) ) + ; ⁻¹-cong = IsGroup.⁻¹-cong ga } + } where + open Group A + open SubGroup n + open Nelm + ga = Group.isGroup A + + diff -r 76c80a6ad4e6 -r 4dd130b93b21 src/Solvable.agda --- a/src/Solvable.agda Mon Sep 11 16:08:09 2023 +0900 +++ b/src/Solvable.agda Thu Sep 14 13:03:17 2023 +0900 @@ -108,8 +108,6 @@ import Algebra.Morphism.Definitions as MorphismDefinitions open import Algebra.Morphism.Structures --- Commutator is normal subgroup of G - Pcomm : {a b : Carrier} → (i : ℕ) → deriving i a → deriving i (b ∙ (a ∙ b ⁻¹ )) Pcomm {a} {b} zero (lift tt) = lift tt Pcomm {.([ _ , _ ])} {b} (suc i) (comm {g} {h} pg ph ) = ccong cc2 (comm (Pcomm {_} {b} i pg) (Pcomm {_} {b} i ph)) where @@ -136,44 +134,42 @@ b ∙ ([ g , h ] ∙ b ⁻¹) ∎ Pcomm {a} {b} (suc i) (ccong f=a pa) = ccong (∙-cong grefl (∙-cong f=a grefl)) (Pcomm {_} {b} (suc i) pa) +-- Finitely Generated Commutator is normal subgroup of G + -- a proudct of commutators may not be a commutator -- so we have to use finite products of commutators -data iCommutator (i : ℕ) : (j : ℕ) → Carrier → Set (Level.suc n ⊔ m) where - iunit : {a : Carrier} → deriving i a → iCommutator i zero a - icoml : {j : ℕ} → {a b : Carrier} → deriving i a → iCommutator i j b → iCommutator i (suc j) (a ∙ b) - icomr : {j : ℕ} → {a b : Carrier} → deriving i a → iCommutator i j b → iCommutator i (suc j) (b ∙ a) - iccong : {j : ℕ} → {a b : Carrier} → a ≈ b → iCommutator i j b → iCommutator i j a +data iCommutator (i : ℕ) : Carrier → Set (Level.suc n ⊔ m) where + iunit : {a : Carrier} → deriving i a → iCommutator i a + i∙ : {a b : Carrier} → iCommutator i a → iCommutator i b → iCommutator i (a ∙ b) + iccong : {a b : Carrier} → a ≈ b → iCommutator i b → iCommutator i a -record IC (i : ℕ ) (ica : Carrier) : Set (Level.suc n ⊔ m) where - field - icn : ℕ - icc : iCommutator i icn ica - -CommGroup : (i : ℕ) → NormalSubGroup G -CommGroup i = record { - P = IC i - ; Pε = record { icn = 0; icc = iunit deriving-ε } +CommNormal : (i : ℕ) → NormalSubGroup G +CommNormal i = record { + Psub = record { + P = iCommutator i + ; Pε = iunit deriving-ε ; P⁻¹ = cg00 - ; P≈ = λ b=a ic → record { icn = icn ic ; icc = iccong (sym b=a) (icc ic) } - ; P∙ = cg01 - ; Pcomm = cg02 + ; P≈ = λ b=a ic → iccong (sym b=a) ic + ; P∙ = cg01 + } + ; Pcomm = cg02 } where - open IC - cg00 : (a : Carrier) → IC i a → IC i (a ⁻¹) - cg00 a record { icn = .zero ; icc = iunit x } = record { icn = 0 ; icc = iunit (deriving-inv x) } - cg00 .((G Group.∙ _) _) record { icn = suc j ; icc = icoml ia icc₁ } with cg00 _ record { icn = _ ; icc = icc₁ } - ... | ib = record { icn = suc (icn ib) ; icc = iccong (sym (lemma5 _ _ )) ( icomr (deriving-inv ia) (icc ib)) } - cg00 .((G Group.∙ _) _) record { icn = suc j ; icc = icomr ia icc₁ } with cg00 _ record { icn = _ ; icc = icc₁ } - ... | ib = record { icn = suc (icn ib) ; icc = iccong (sym (lemma5 _ _ )) ( icoml (deriving-inv ia) (icc ib)) } - cg00 _ record { icn = j ; icc = iccong eq icc₁ } with cg00 _ record { icn = _ ; icc = icc₁ } - ... | ib = record { icn = icn ib ; icc = iccong (⁻¹-cong eq) (icc ib) } - cg01 : {a b : Carrier} → IC i a → IC i b → IC i (a ∙ b) - cg01 {a} {b} record { icn = .zero ; icc = (iunit x) } ib = ? - cg01 {.((G Group.∙ _) _)} {b} record { icn = .(suc _) ; icc = (icoml x icc₁) } ib = ? - cg01 {.((G Group.∙ _) _)} {b} record { icn = .(suc _) ; icc = (icomr x icc₁) } ib = ? - cg01 {a} {b} record { icn = icn ; icc = (iccong x icc₁) } ib = ? - cg02 : {a b : Carrier} → IC i a → IC i (b ∙ (a ∙ b ⁻¹)) - cg02 = ? + cg00 : (a : Carrier) → iCommutator i a → iCommutator i (a ⁻¹) + cg00 a (iunit x) = iunit (deriving-inv x) + cg00 .((G Group.∙ _) _) (i∙ ic ic₁) = iccong (gsym (lemma5 _ _)) ( i∙ (cg00 _ ic₁) (cg00 _ ic) ) + cg00 a (iccong eq ic) = iccong (⁻¹-cong eq) (cg00 _ ic) + cg01 : {a b : Carrier} → iCommutator i a → iCommutator i b → iCommutator i (a ∙ b) + cg01 {a} {b} ia ib = i∙ ia ib + cg02 : {a b : Carrier} → iCommutator i a → iCommutator i (b ∙ (a ∙ b ⁻¹)) + cg02 {a} {b} (iunit da) = iunit ( Pcomm i da ) + cg02 {a} {b} (i∙ {a₁} {b₁} ia ib) = iccong cg03 (i∙ (cg02 {a₁} {b} ia) (cg02 {b₁} {b} ib)) where + cg03 : b ∙ (a₁ ∙ b₁ ∙ b ⁻¹) ≈ b ∙ (a₁ ∙ b ⁻¹) ∙ (b ∙ (b₁ ∙ b ⁻¹)) + cg03 = begin + b ∙ (a₁ ∙ b₁ ∙ b ⁻¹) ≈⟨ solve monoid ⟩ + b ∙ (a₁ ∙ ε ∙ b₁ ∙ b ⁻¹) ≈⟨ cdr (car (car (cdr (gsym (proj₁ inverse _))))) ⟩ + b ∙ (a₁ ∙ (b ⁻¹ ∙ b ) ∙ b₁ ∙ b ⁻¹) ≈⟨ solve monoid ⟩ + b ∙ (a₁ ∙ b ⁻¹) ∙ (b ∙ (b₁ ∙ b ⁻¹)) ∎ + cg02 {a} {b} (iccong eq ia) = iccong (cdr (car eq)) ( cg02 {_} {b} ia )