Mercurial > hg > Members > kono > Proof > galois
changeset 293:ec6fc84284f7
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 02 Sep 2023 12:06:39 +0900 |
| parents | f59a9f4cfd78 |
| children | e153b9a96665 |
| files | src/FundamentalHomorphism.agda src/Gutil0.agda src/Solvable.agda src/fin.agda src/homomorphism.agda |
| diffstat | 5 files changed, 556 insertions(+), 312 deletions(-) [+] |
line wrap: on
line diff
--- a/src/FundamentalHomorphism.agda Sun Jun 11 08:46:32 2023 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,272 +0,0 @@ --- fundamental homomorphism theorem --- - -open import Level hiding ( suc ; zero ) -module FundamentalHomorphism (c : Level) where - -open import Algebra -open import Algebra.Structures -open import Algebra.Definitions -open import Algebra.Core -open import Algebra.Bundles - -open import Data.Product -open import Relation.Binary.PropositionalEquality -open import Gutil0 -import Gutil -import Function.Definitions as FunctionDefinitions - -import Algebra.Morphism.Definitions as MorphismDefinitions -open import Algebra.Morphism.Structures - -open import Tactic.MonoidSolver using (solve; solve-macro) - --- --- Given two groups G and H and a group homomorphism f : G → H, --- let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K --- (where G/K is the quotient group of G by K). --- If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ. --- https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms --- --- f --- G --→ H --- | / --- φ | / h --- ↓ / --- G/K --- - -import Relation.Binary.Reasoning.Setoid as EqReasoning - -_<_∙_> : (m : Group c c ) → Group.Carrier m → Group.Carrier m → Group.Carrier m -m < x ∙ y > = Group._∙_ m x y - -_<_≈_> : (m : Group c c ) → (f g : Group.Carrier m ) → Set c -m < x ≈ y > = Group._≈_ m x y - -infixr 9 _<_∙_> - --- --- Coset : N : NormalSubGroup → { a ∙ n | G ∋ a , N ∋ n } --- - -open GroupMorphisms - --- import Axiom.Extensionality.Propositional --- postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m - -open import Data.Empty -open import Relation.Nullary - -record NormalSubGroup (A : Group c c ) : Set c where - open Group A - field - ⟦_⟧ : Group.Carrier A → Group.Carrier A - normal : IsGroupHomomorphism (GR A) (GR A) ⟦_⟧ - comm : {a b : Carrier } → b ∙ ⟦ a ⟧ ≈ ⟦ a ⟧ ∙ b - --- Set of a ∙ ∃ n ∈ N --- -record an {A : Group c c } (N : NormalSubGroup A ) (n x : Group.Carrier A ) : Set c where - open Group A - open NormalSubGroup N - field - a : Carrier - aN=x : a ∙ ⟦ n ⟧ ≈ x - -record aN {A : Group c c } (N : NormalSubGroup A ) : Set c where - open Group A - field - n : Carrier - is-an : (x : Carrier) → an N n x - -f0 : {A : Group c c } (N : NormalSubGroup A ) (x y : Group.Carrier A) → an N x y -f0 {A} N x y = record { a = y ∙ ⟦ x ⟧ ⁻¹ ; aN=x = gk02 } where - open Group A - open NormalSubGroup N - open IsGroupHomomorphism normal - open EqReasoning (Algebra.Group.setoid A) - open Gutil A - gk02 : {x g : Carrier } → x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈ x - gk02 {x} {g} = begin x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈⟨ solve monoid ⟩ - x ∙ ( ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧) ≈⟨ ∙-cong grefl (proj₁ inverse _ ) ⟩ - x ∙ ε ≈⟨ proj₂ identity _ ⟩ - x ∎ - -_/_ : (A : Group c c ) (N : NormalSubGroup A ) → Group c c -_/_ A N = record { - Carrier = aN N - ; _≈_ = λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧ - ; _∙_ = qadd - ; ε = qid - ; _⁻¹ = λ f → record { n = n f ⁻¹ ; is-an = λ x → record { a = an.a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧ ; aN=x = qinv0 f x } } - ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { - isEquivalence = record {refl = grefl ; trans = gtrans ; sym = gsym } - ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gtrans (homo _ _) ( gtrans (∙-cong x=y u=v) (gsym (homo _ _) )) } - ; assoc = qassoc } - ; identity = (λ q → ⟦⟧-cong (proj₁ identity _) ) , (λ q → ⟦⟧-cong (proj₂ identity _) ) } - ; inverse = (λ x → ⟦⟧-cong (proj₁ inverse _ )) , (λ x → ⟦⟧-cong (proj₂ inverse _ ) ) - ; ⁻¹-cong = λ {x} {y} → i-conv {x} {y} - } - } where - open Group A - open aN - open an - open NormalSubGroup N - open IsGroupHomomorphism normal - open EqReasoning (Algebra.Group.setoid A) - open Gutil A - qadd : (f g : aN N) → aN N - qadd f g = record { n = n f ∙ n g ; is-an = λ x → record { a = x ⁻¹ ∙ ( a (is-an f x) ∙ a (is-an g x)) ; aN=x = qadd0 } } where - qadd0 : {x : Carrier} → x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈ x - qadd0 {x} = begin - x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈⟨ solve monoid ⟩ - x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x) ∙ ⟦ n f ∙ n g ⟧) ≈⟨ ? ⟩ - x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x) ∙ ( ⟦ n f ⟧ ∙ ⟦ n g ⟧ )) ≈⟨ solve monoid ⟩ - x ⁻¹ ∙ (a (is-an f x) ∙ ( a (is-an g x) ∙ ⟦ n f ⟧) ∙ ⟦ n g ⟧) ≈⟨ ? ⟩ - x ⁻¹ ∙ (a (is-an f x) ∙ ( ⟦ n f ⟧ ∙ a (is-an g x) ) ∙ ⟦ n g ⟧) ≈⟨ ? ⟩ - x ⁻¹ ∙ ((a (is-an f x) ∙ ⟦ n f ⟧ ) ∙ ( a (is-an g x) ∙ ⟦ n g ⟧)) ≈⟨ ? ⟩ - x ⁻¹ ∙ (x ∙ x) ≈⟨ solve monoid ⟩ - (x ⁻¹ ∙ x ) ∙ x ≈⟨ ? ⟩ - ε ∙ x ≈⟨ solve monoid ⟩ - x ∎ - qinv0 : (f : aN N) → (x : Carrier ) → (a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧) ∙ ⟦ n f ⁻¹ ⟧ ≈ x - qinv0 f x = begin - (a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧) ∙ ⟦ n f ⁻¹ ⟧ ≈⟨ ? ⟩ - a (is-an f x) ∙ ⟦ n f ⟧ ≈⟨ an.aN=x (is-an f x) ⟩ - x ∎ - qid : aN N - qid = record { n = ε ; is-an = λ x → record { a = x ; aN=x = qid1 } } where - qid1 : {x : Carrier } → x ∙ ⟦ ε ⟧ ≈ x - qid1 {x} = begin - x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong grefl ε-homo ⟩ - x ∙ ε ≈⟨ proj₂ identity _ ⟩ - x ∎ - qassoc : (f g h : aN N) → ⟦ n ( qadd (qadd f g) h) ⟧ ≈ ⟦ n( qadd f (qadd g h)) ⟧ - qassoc f g h = ⟦⟧-cong (assoc _ _ _ ) - i-conv : {x y : aN N} → ⟦ n x ⟧ ≈ ⟦ n y ⟧ → ⟦ n x ⁻¹ ⟧ ≈ ⟦ n y ⁻¹ ⟧ - i-conv {x} {y} nx=ny = begin - ⟦ n x ⁻¹ ⟧ ≈⟨ ⁻¹-homo _ ⟩ - ⟦ n x ⟧ ⁻¹ ≈⟨ ⁻¹-cong nx=ny ⟩ - ⟦ n y ⟧ ⁻¹ ≈⟨ gsym ( ⁻¹-homo _) ⟩ - ⟦ n y ⁻¹ ⟧ ∎ - - --- K ⊂ ker(f) -K⊆ker : (G H : Group c c) (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c -K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε where - open Group H - open NormalSubGroup K - -open import Function.Surjection -open import Function.Equality - -module GK (G : Group c c) (K : NormalSubGroup G) where - open Group G - open aN - open an - open NormalSubGroup K - open IsGroupHomomorphism normal - open EqReasoning (Algebra.Group.setoid G) - open Gutil G - - φ : Group.Carrier G → Group.Carrier (G / K ) - φ g = record { n = g ; is-an = λ x → record { a = x ∙ ( ⟦ g ⟧ ⁻¹) ; aN=x = gk02 } } where - gk02 : {x : Carrier } → x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈ x - gk02 {x} = begin x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈⟨ solve monoid ⟩ - x ∙ ( ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧) ≈⟨ ∙-cong grefl (proj₁ inverse _ ) ⟩ - x ∙ ε ≈⟨ proj₂ identity _ ⟩ - x ∎ - - φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ - φ-homo = record {⁻¹-homo = λ g → ? ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism = - record { cong = ? } }}} - - -- gk03 : {f : Group.Carrier (G / K) } → ⟦ n f ⟧ ≈ ⟦ ⟦ n f ⟧ ⟧ -- a (is-an f x) ∙ ⟦ n f ⟧ ≡ x - -- gk03 {x} = ? -- - - φe : (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K)) - φe = record { _⟨$⟩_ = φ ; cong = ? } where - φ-cong : {f g : Carrier } → f ≈ g → ⟦ n (φ f ) ⟧ ≈ ⟦ n (φ g ) ⟧ - φ-cong = ? - - inv-φ : Group.Carrier (G / K ) → Group.Carrier G - inv-φ f = n f -- ⟦ n f ⟧ ( if we have gk03 ) - - cong-i : {f g : Group.Carrier (G / K ) } → ⟦ n f ⟧ ≈ ⟦ n g ⟧ → inv-φ f ≈ inv-φ g - cong-i {f} {g} nf=ng = ? - - is-inverse : (f : aN K ) → ⟦ n (φ (inv-φ f) ) ⟧ ≈ ⟦ n f ⟧ - is-inverse f = begin - ⟦ n (φ (inv-φ f) ) ⟧ ≈⟨ grefl ⟩ - ⟦ n (φ ( n f ) ) ⟧ ≈⟨ grefl ⟩ - ⟦ n f ⟧ ∎ - - φ-surjective : Surjective φe - φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse } - - gk01 : (x : Group.Carrier (G / K ) ) → (G / K) < φ ( inv-φ x ) ≈ x > - gk01 x = begin - ⟦ inv-φ x ⟧ ≈⟨ grefl ⟩ - ⟦ n x ⟧ ∎ - - -record FundamentalHomomorphism (G H : Group c c ) - (f : Group.Carrier G → Group.Carrier H ) - (homo : IsGroupHomomorphism (GR G) (GR H) f ) - (K : NormalSubGroup G ) (kf : K⊆ker G H K f) : Set c where - open Group H - open GK G K - field - h : Group.Carrier (G / K ) → Group.Carrier H - h-homo : IsGroupHomomorphism (GR (G / K) ) (GR H) h - is-solution : (x : Group.Carrier G) → f x ≈ h ( φ x ) - unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 ) - → ( (x : Group.Carrier G) → f x ≈ h1 ( φ x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) - -FundamentalHomomorphismTheorm : (G H : Group c c) - (f : Group.Carrier G → Group.Carrier H ) - (homo : IsGroupHomomorphism (GR G) (GR H) f ) - (K : NormalSubGroup G ) → (kf : K⊆ker G H K f) → FundamentalHomomorphism G H f homo K kf -FundamentalHomomorphismTheorm G H f homo K kf = record { - h = h - ; h-homo = h-homo - ; is-solution = is-solution - ; unique = unique - } where - open GK G K - open Group H - open Gutil H - open NormalSubGroup K - open IsGroupHomomorphism homo - open aN - h : Group.Carrier (G / K ) → Group.Carrier H - h r = f ( inv-φ r ) - h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y - h03 x y = {!!} - h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h - h-homo = record { - isMonoidHomomorphism = record { - isMagmaHomomorphism = record { - isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } - ; homo = h03 } - ; ε-homo = {!!} } - ; ⁻¹-homo = {!!} } - open EqReasoning (Algebra.Group.setoid H) - is-solution : (x : Group.Carrier G) → f x ≈ h ( φ x ) - is-solution x = begin - f x ≈⟨ grefl ⟩ - h ( φ x ) ∎ - unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (h1-homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 ) - → ( (x : Group.Carrier G) → f x ≈ h1 ( φ x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) - unique h1 h1-homo h1-is-solution x = begin - h x ≈⟨ grefl ⟩ - f ( inv-φ x ) ≈⟨ h1-is-solution _ ⟩ - h1 ( φ ( inv-φ x ) ) ≈⟨ IsGroupHomomorphism.⟦⟧-cong h1-homo (gk01 x) ⟩ - h1 x ∎ - - - - - -
--- a/src/Gutil0.agda Sun Jun 11 08:46:32 2023 +0900 +++ b/src/Gutil0.agda Sat Sep 02 12:06:39 2023 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --allow-unsolved-metas #-} open import Level hiding ( suc ; zero ) module Gutil0 where @@ -45,46 +46,55 @@ 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 --- record NormalSubGroup {c l : Level } ( G : Group c l ) : Set ( c Level.⊔ l ) where --- open Group G --- field --- sub : Carrier → Carrier --- s-homo : IsGroupHomomorphism (GR G) (GR G) sub --- commute : ( g n : Carrier ) → g ∙ sub n ≈ sub n ∙ g --- -- it has at least one element other than ε --- -- anElement : Carrier --- -- notE : ¬ ( Group._≈_ G anElement (Group.ε G) ) +_<_≈_> : {c d : Level} (m : Group c d ) → (f g : Group.Carrier m ) → Set d +m < x ≈ y > = Group._≈_ m x y + +infixr 9 _<_∙_> --- open import Relation.Binary.Morphism.Structures +-- assuming Homomorphism is too strong +-- +record NormalSubGroup {c d : Level} (A : Group c d ) : Set (Level.suc (Level.suc (c Level.⊔ d))) where + open Group A + field + P : Carrier → Set (Level.suc c ⊔ d) + Pε : P ε + P⁻¹ : (a : Carrier ) → P a → P (a ⁻¹) + P∙ : {a b : Carrier } → P a → P b → P ( a ∙ b ) + -- gN ≈ Ng + Pcomm : {a b : Carrier } → P a → P ( b ∙ ( a ∙ b ⁻¹ ) ) import Relation.Binary.Reasoning.Setoid as EqReasoning --- record HomoMorphism {c l : Level } (G : Group c l) (f : Group.Carrier G → Group.Carrier G) : Set ( c Level.⊔ l ) where --- open Group G --- field --- f-cong : {x y : Carrier } → x ≈ y → f x ≈ f y --- f-homo : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y --- f-ε : f ( ε ) ≈ ε --- f-inv : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹ +record Nelm {c d : Level} {A : Group c d } (n : NormalSubGroup A) : Set (Level.suc c ⊔ d) where + open Group A + open NormalSubGroup n + field + elm : Carrier + Pelm : P elm --- HM : {c l : Level } → (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) --- → IsGroupHomomorphism (GR G) (GR G) f → HomoMorphism G f --- HM G f homo = record { --- f-cong = λ eq → IsRelHomomorphism.cong ( IsMagmaHomomorphism.isRelHomomorphism --- ( IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))) eq --- ; f-homo = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo)) --- ; f-ε = IsMonoidHomomorphism.ε-homo ( IsGroupHomomorphism.isMonoidHomomorphism homo) --- ; f-inv = IsGroupHomomorphism.⁻¹-homo homo --- } --- --- open HomoMorphism --- --- hm : {c l : Level } → (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) --- → HomoMorphism G f --- → IsGroupHomomorphism (GR G) (GR G) f --- hm G f hm = record { isMonoidHomomorphism = record { isMagmaHomomorphism = record { --- isRelHomomorphism = record { cong = λ {x} {y} eq → f-cong hm {x} {y} eq } --- ; homo = f-homo hm } ; ε-homo = f-ε hm } ; ⁻¹-homo = f-inv hm --- } --- +NGroup : {c d : Level} {A : Group c d } (n : NormalSubGroup A) → Group (Level.suc c ⊔ d) d +NGroup {_} {_} {A} n = record { + Carrier = Nelm 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 NormalSubGroup n + open Nelm + ga = Group.isGroup A + +
--- a/src/Solvable.agda Sun Jun 11 08:46:32 2023 +0900 +++ b/src/Solvable.agda Sat Sep 02 12:06:39 2023 +0900 @@ -42,6 +42,8 @@ import Relation.Binary.Reasoning.Setoid as EqReasoning open EqReasoning (Algebra.Group.setoid G) +open import Tactic.MonoidSolver using (solve; solve-macro) + lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹ lemma4 g h = begin @@ -101,3 +103,59 @@ comm-resp : {g h g1 h1 : Carrier } → g ≈ g1 → h ≈ h1 → [ g , h ] ≈ [ g1 , h1 ] comm-resp {g} {h} {g1} {h1} g=g1 h=h1 = ∙-cong (∙-cong (∙-cong (⁻¹-cong g=g1 ) (⁻¹-cong h=h1 )) g=g1 ) h=h1 +open import Gutil0 +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 + cc2 : [ b ∙ (g ∙ b ⁻¹) , b ∙ (h ∙ b ⁻¹) ] ≈ b ∙ ([ g , h ] ∙ b ⁻¹) + cc2 = begin + [ b ∙ (g ∙ b ⁻¹) , b ∙ (h ∙ b ⁻¹) ] ≈⟨ grefl ⟩ + (b ∙ (g ∙ b ⁻¹) ) ⁻¹ ∙ ( b ∙ (h ∙ b ⁻¹)) ⁻¹ ∙ (b ∙ (g ∙ b ⁻¹)) ∙ (b ∙ (h ∙ b ⁻¹)) + ≈⟨ car (car (∙-cong (sym (lemma5 _ _)) (sym (lemma5 _ _)))) ⟩ + ((g ∙ b ⁻¹) ⁻¹ ∙ b ⁻¹ ) ∙ ( (h ∙ b ⁻¹) ⁻¹ ∙ b ⁻¹ ) ∙ (b ∙ (g ∙ b ⁻¹)) ∙ (b ∙ (h ∙ b ⁻¹)) + ≈⟨ car (car (∙-cong (car (sym (lemma5 _ _))) (car (sym (lemma5 _ _))))) ⟩ + (((b ⁻¹ )⁻¹ ∙ g ⁻¹ ) ∙ b ⁻¹ ) ∙ ( ((b ⁻¹) ⁻¹ ∙ h ⁻¹ ) ∙ b ⁻¹ ) ∙ (b ∙ (g ∙ b ⁻¹)) ∙ (b ∙ (h ∙ b ⁻¹)) + ≈⟨ car (car (∙-cong (car (car f⁻¹⁻¹≈f)) (car (car f⁻¹⁻¹≈f)))) ⟩ + ((b ∙ g ⁻¹ ) ∙ b ⁻¹ ) ∙ ( (b ∙ h ⁻¹ ) ∙ b ⁻¹ ) ∙ (b ∙ (g ∙ b ⁻¹)) ∙ (b ∙ (h ∙ b ⁻¹)) ≈⟨ solve monoid ⟩ + (((b ∙ g ⁻¹ ) ∙ (b ⁻¹ ∙ b ) ∙ h ⁻¹ ) ∙ b ⁻¹ ) ∙ (b ∙ (g ∙ b ⁻¹)) ∙ (b ∙ (h ∙ b ⁻¹)) ≈⟨ car (car (car (car (cdr (proj₁ inverse _))))) ⟩ + (((b ∙ g ⁻¹ ) ∙ ε ∙ h ⁻¹ ) ∙ b ⁻¹ ) ∙ (b ∙ (g ∙ b ⁻¹)) ∙ (b ∙ (h ∙ b ⁻¹)) ≈⟨ solve monoid ⟩ + ((b ∙ (g ⁻¹ ∙ ε) ∙ h ⁻¹ ) ∙ b ⁻¹ ) ∙ (b ∙ (g ∙ (b ⁻¹ ∙ b ) ∙ (h ∙ b ⁻¹))) ≈⟨ cdr (cdr (car (cdr (proj₁ inverse _)))) ⟩ + ((b ∙ (g ⁻¹ ∙ ε) ∙ h ⁻¹ ) ∙ b ⁻¹ ) ∙ (b ∙ (g ∙ ε ∙ (h ∙ b ⁻¹))) ≈⟨ + ∙-cong (car (car (cdr (proj₂ identity _)))) (cdr (car (proj₂ identity _))) ⟩ + (((b ∙ g ⁻¹ ) ∙ h ⁻¹ ) ∙ b ⁻¹ ) ∙ (b ∙ (g ∙ (h ∙ b ⁻¹))) ≈⟨ solve monoid ⟩ + ((b ∙ g ⁻¹ ) ∙ h ⁻¹ ) ∙ (b ⁻¹ ∙ b ) ∙ (g ∙ (h ∙ b ⁻¹)) ≈⟨ ∙-cong (∙-cong grefl (proj₁ inverse _) ) grefl ⟩ + ((b ∙ g ⁻¹ ) ∙ h ⁻¹ ) ∙ ε ∙ (g ∙ (h ∙ b ⁻¹)) ≈⟨ ∙-cong (proj₂ identity _) grefl ⟩ + ((b ∙ g ⁻¹ ) ∙ h ⁻¹ ) ∙ (g ∙ (h ∙ b ⁻¹)) ≈⟨ solve monoid ⟩ + b ∙ (( g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h ) ∙ b ⁻¹) ≈⟨ grefl ⟩ + 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) + +comp : {a b : Carrier} → (i : ℕ) → deriving i a → deriving i b → deriving i (a ∙ b) +comp {a} {b} zero (lift tt) (lift tt) = lift tt +comp (suc i) (comm {a} {b} pa pb) (comm {c} {d} pc pd) = ccong cc1 ( comm (comp i pa pb) (comp i pc pd) ) where + cc1 : [ a ∙ b , c ∙ d ] ≈ [ a , b ] ∙ [ c , d ] + cc1 = begin + [ a ∙ b , c ∙ d ] ≈⟨ grefl ⟩ + (a ∙ b) ⁻¹ ∙ (c ∙ d) ⁻¹ ∙ (a ∙ b) ∙ (c ∙ d) ≈⟨ ∙-cong (∙-cong (∙-cong (sym (lemma5 _ _)) (sym (lemma5 _ _)) ) grefl) grefl ⟩ + (b ⁻¹ ∙ a ⁻¹) ∙ (d ⁻¹ ∙ c ⁻¹) ∙ (a ∙ b) ∙ (c ∙ d) ≈⟨ ? ⟩ + (a ⁻¹ ∙ b ⁻¹ ∙ (b ∙ a )) ∙ ((b ⁻¹ ∙ a ⁻¹) ∙ (d ⁻¹ ∙ c ⁻¹) ∙ (a ∙ b) ∙ (c ∙ d)) ≈⟨ ? ⟩ + a ⁻¹ ∙ b ⁻¹ ∙ a ∙ b ∙ (c ⁻¹ ∙ d ⁻¹ ∙ c ∙ d ) ≈⟨ grefl ⟩ + [ a , b ] ∙ [ c , d ] ∎ +comp (suc i) (comm a pa) (ccong g=b pb) = ccong (∙-cong grefl g=b ) (comp (suc i) (comm a pa) pb ) +comp {a} (suc i) (ccong f=a pa) (comm b pb) = ccong (∙-cong f=a grefl ) (comp (suc i) pa (comm b pb) ) +comp {a} {b} (suc i) (ccong f=a pa) (ccong g=b pb) = ccong (∙-cong f=a g=b) (comp (suc i) pa pb ) + +CommGroup : (i : ℕ) → NormalSubGroup G +CommGroup i = record { + P = deriving i + ; Pε = deriving-ε + ; P⁻¹ = λ a pa → deriving-inv pa + ; P∙ = comp i + ; Pcomm = ? + } +
--- a/src/fin.agda Sun Jun 11 08:46:32 2023 +0900 +++ b/src/fin.agda Sat Sep 02 12:06:39 2023 +0900 @@ -2,9 +2,10 @@ module fin where -open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ) -open import Data.Fin.Properties hiding ( <-trans ) +open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ ) +open import Data.Fin.Properties hiding (≤-trans ; <-trans ; ≤-refl ) renaming ( <-cmp to <-fcmp ) open import Data.Nat +open import Data.Nat.Properties open import logic open import nat open import Relation.Binary.PropositionalEquality @@ -87,7 +88,6 @@ lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = cong suc ( lemma12 {n} {m} n<m f refl ) open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -open import Data.Fin.Properties -- <-irrelevant <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n @@ -114,4 +114,187 @@ ∎ where open ≡-Reasoning +x<y→fin-1 : {n : ℕ } → { x y : Fin (suc n)} → toℕ x < toℕ y → Fin n +x<y→fin-1 {n} {x} {y} lt = fromℕ< (≤-trans lt (fin≤n _ )) +x<y→fin-1-eq : {n : ℕ } → { x y : Fin (suc n)} → (lt : toℕ x < toℕ y ) → toℕ x ≡ toℕ (x<y→fin-1 lt ) +x<y→fin-1-eq {n} {x} {y} lt = sym ( begin + toℕ (fromℕ< (≤-trans lt (fin≤n y)) ) ≡⟨ toℕ-fromℕ< _ ⟩ + toℕ x ∎ ) where open ≡-Reasoning + +f<→< : {n : ℕ } → { x y : Fin n} → x Data.Fin.< y → toℕ x < toℕ y +f<→< {_} {zero} {suc y} (s≤s lt) = s≤s z≤n +f<→< {_} {suc x} {suc y} (s≤s lt) = s≤s (f<→< {_} {x} {y} lt) + +f≡→≡ : {n : ℕ } → { x y : Fin n} → x ≡ y → toℕ x ≡ toℕ y +f≡→≡ refl = refl + +open import Data.List +open import Relation.Binary.Definitions + + +----- +-- +-- find duplicate element in a List (Fin n) +-- +-- if the length is longer than n, we can find duplicate element as FDup-in-list +-- +-- How about do it in ℕ ? + +-- fin-count : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → ℕ +-- fin-count q p[ = 0 +-- fin-count q (q0 ∷ qs ) with <-fcmp q q0 +-- ... | tri-e = suc (fin-count q qs) +-- ... | false = fin-count q qs + +-- fin-not-dup-in-list : { n : ℕ} (qs : List (Fin n) ) → Set +-- fin-not-dup-in-list {n} qs = (q : Fin n) → fin-count q ≤ 1 + +-- this is far easier +-- fin-not-dup-in-list→len<n : { n : ℕ} (qs : List (Fin n) ) → ( (q : Fin n) → fin-not-dup-in-list qs q) → length qs ≤ n +-- fin-not-dup-in-list→len<n = ? + +fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool -- find the dup +fin-phase2 q [] = false +fin-phase2 q (x ∷ qs) with <-fcmp q x +... | tri< a ¬b ¬c = fin-phase2 q qs +... | tri≈ ¬a b ¬c = true +... | tri> ¬a ¬b c = fin-phase2 q qs +fin-phase1 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool -- find the first element +fin-phase1 q [] = false +fin-phase1 q (x ∷ qs) with <-fcmp q x +... | tri< a ¬b ¬c = fin-phase1 q qs +... | tri≈ ¬a b ¬c = fin-phase2 q qs +... | tri> ¬a ¬b c = fin-phase1 q qs + +fin-dup-in-list : { n : ℕ} (q : Fin n) (qs : List (Fin n) ) → Bool +fin-dup-in-list {n} q qs = fin-phase1 q qs + +record FDup-in-list (n : ℕ ) (qs : List (Fin n)) : Set where + field + dup : Fin n + is-dup : fin-dup-in-list dup qs ≡ true + +list-less : {n : ℕ } → List (Fin (suc n)) → List (Fin n) +list-less [] = [] +list-less {n} (i ∷ ls) with <-fcmp (fromℕ< a<sa) i +... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ i < suc k ) (sym fin<asa) (fin≤n _ ))) +... | tri≈ ¬a b ¬c = list-less ls +... | tri> ¬a ¬b c = x<y→fin-1 c ∷ list-less ls + +fin010 : {n m : ℕ } {x : Fin n} (c : suc (toℕ x) ≤ toℕ (fromℕ< {m} a<sa) ) → toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡ toℕ x +fin010 {_} {_} {x} c = begin + toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡⟨ toℕ-fromℕ< _ ⟩ + toℕ x ∎ where open ≡-Reasoning + +--- +--- if List (Fin n) is longer than n, there is at most one duplication +--- +fin-dup-in-list>n : {n : ℕ } → (qs : List (Fin n)) → (len> : length qs > n ) → FDup-in-list n qs +fin-dup-in-list>n {zero} [] () +fin-dup-in-list>n {zero} (() ∷ qs) lt +fin-dup-in-list>n {suc n} qs lt = fdup-phase0 where + open import Level using ( Level ) + -- make a dup from one level below + fdup+1 : (qs : List (Fin (suc n))) (i : Fin n) → fin-dup-in-list (fromℕ< a<sa ) qs ≡ false + → fin-dup-in-list i (list-less qs) ≡ true → FDup-in-list (suc n) qs + fdup+1 qs i ne p = record { dup = fin+1 i ; is-dup = f1-phase1 qs p (case1 ne) } where + -- we have two loops on the max element and the current level. The disjuction means the phases may differ. + f1-phase2 : (qs : List (Fin (suc n)) ) → fin-phase2 i (list-less qs) ≡ true + → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false) + → fin-phase2 (fin+1 i) qs ≡ true + f1-phase2 (x ∷ qs) p (case1 q1) with <-fcmp (fromℕ< a<sa) x + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) + f1-phase2 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x + ... | tri< a ¬b ¬c₁ = f1-phase2 qs p (case2 q1) + ... | tri≈ ¬a₁ b₁ ¬c₁ = refl + ... | tri> ¬a₁ ¬b c = f1-phase2 qs p (case2 q1) + -- two fcmp is only different in the size of Fin, but to develop both f1-phase and list-less both fcmps are required + f1-phase2 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x + ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case1 q1) + ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) + ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) + ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a )) + ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = refl + ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase2 qs p (case1 q1) + f1-phase2 (x ∷ qs) p (case2 q1) with <-fcmp (fromℕ< a<sa) x + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) + f1-phase2 (x ∷ qs) p (case2 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x + ... | tri< a ¬b ¬c₁ = ⊥-elim ( ¬-bool q1 refl ) + ... | tri≈ ¬a₁ b₁ ¬c₁ = refl + ... | tri> ¬a₁ ¬b c = ⊥-elim ( ¬-bool q1 refl ) + f1-phase2 (x ∷ qs) p (case2 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x + ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase2 qs p (case2 q1) + ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) + ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) + ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a )) + ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = refl + ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase2 qs p (case2 q1 ) + f1-phase1 : (qs : List (Fin (suc n)) ) → fin-phase1 i (list-less qs) ≡ true + → (fin-phase1 (fromℕ< a<sa) qs ≡ false ) ∨ (fin-phase2 (fromℕ< a<sa) qs ≡ false) + → fin-phase1 (fin+1 i) qs ≡ true + f1-phase1 (x ∷ qs) p (case1 q1) with <-fcmp (fromℕ< a<sa) x + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) + f1-phase1 (x ∷ qs) p (case1 q1) | tri≈ ¬a b ¬c with <-fcmp (fin+1 i) x + ... | tri< a ¬b ¬c₁ = f1-phase1 qs p (case2 q1) + ... | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (fdup-10 b b₁) where + fdup-10 : fromℕ< a<sa ≡ x → fin+1 i ≡ x → ⊥ + fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) fin<n ) + ... | tri> ¬a₁ ¬b c = f1-phase1 qs p (case2 q1) + f1-phase1 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x + ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case1 q1) + ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) + ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) + ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a )) + ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case1 q1) + ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case1 q1) + f1-phase1 (x ∷ qs) p (case2 q1) with <-fcmp (fromℕ< a<sa) x + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) + f1-phase1 (x ∷ qs) p (case2 q1) | tri≈ ¬a b ¬c = ⊥-elim ( ¬-bool q1 refl ) + f1-phase1 (x ∷ qs) p (case2 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x + ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case2 q1) + ... | tri< a ¬b₁ ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) + ... | tri< a ¬b₁ ¬c | tri> ¬a₁ ¬b₂ c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) (sym fin+1-toℕ) (toℕ-fromℕ< _) a )) + ... | tri≈ ¬a₁ b ¬c | tri< a ¬b₁ ¬c₁ = ⊥-elim ( ¬a₁ (subst₂ (λ j k → j < k) fin+1-toℕ (sym (toℕ-fromℕ< _)) a )) + ... | tri≈ ¬a₁ b ¬c | tri≈ ¬a₂ b₁ ¬c₁ = f1-phase2 qs p (case2 q1) + ... | tri≈ ¬a₁ b ¬c | tri> ¬a₂ ¬b₁ c₁ = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) fin+1-toℕ (sym (toℕ-fromℕ< _)) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri< a ¬b₂ ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) + ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case2 q1) + fdup-phase0 : FDup-in-list (suc n) qs + fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs | inspect (fin-dup-in-list (fromℕ< a<sa)) qs + ... | true | record { eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq } + ... | false | record { eq = ne } = fdup+1 qs (FDup-in-list.dup fdup) ne (FDup-in-list.is-dup fdup) where + -- if no dup in the max element, the list without the element is only one length shorter + fless : (qs : List (Fin (suc n))) → length qs > suc n → fin-dup-in-list (fromℕ< a<sa) qs ≡ false → n < length (list-less qs) + fless qs lt p = fl-phase1 n qs lt p where + fl-phase2 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > n1 → fin-phase2 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs) + fl-phase2 zero (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) + ... | tri> ¬a ¬b c = s≤s z≤n + fl-phase2 (suc n1) (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) + ... | tri> ¬a ¬b c = s≤s ( fl-phase2 n1 qs lt p ) + fl-phase1 : (n1 : ℕ) (qs : List (Fin (suc n))) → length qs > suc n1 → fin-phase1 (fromℕ< a<sa) qs ≡ false → n1 < length (list-less qs) + fl-phase1 zero (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) + ... | tri≈ ¬a b ¬c = fl-phase2 0 qs lt p + ... | tri> ¬a ¬b c = s≤s z≤n + fl-phase1 (suc n1) (x ∷ qs) (s≤s lt) p with <-fcmp (fromℕ< a<sa) x + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (subst (λ k → toℕ x < suc k ) (sym fin<asa) (fin≤n _ ))) + ... | tri≈ ¬a b ¬c = fl-phase2 (suc n1) qs lt p + ... | tri> ¬a ¬b c = s≤s ( fl-phase1 n1 qs lt p ) + -- if the list without the max element is only one length shorter, we can recurse + fdup : FDup-in-list n (list-less qs) + fdup = fin-dup-in-list>n (list-less qs) (fless qs lt ne) + +--
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/homomorphism.agda Sat Sep 02 12:06:39 2023 +0900 @@ -0,0 +1,265 @@ +-- fundamental homomorphism theorem +-- + +open import Level hiding ( suc ; zero ) +module homomorphism (c d : Level) where + +open import Algebra +open import Algebra.Structures +open import Algebra.Definitions +open import Algebra.Core +open import Algebra.Bundles + +open import Data.Product +open import Relation.Binary.PropositionalEquality +open import Gutil0 +import Gutil +import Function.Definitions as FunctionDefinitions + +import Algebra.Morphism.Definitions as MorphismDefinitions +open import Algebra.Morphism.Structures + +open import Tactic.MonoidSolver using (solve; solve-macro) + +-- +-- Given two groups G and H and a group homomorphism f : G → H, +-- let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K +-- (where G/K is the quotient group of G by K). +-- If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ. +-- https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms +-- +-- f +-- G --→ H +-- | / +-- φ | / h +-- ↓ / +-- G/K +-- + +import Relation.Binary.Reasoning.Setoid as EqReasoning + +-- _<_∙_> : (m : Group c c ) → Group.Carrier m → Group.Carrier m → Group.Carrier m +-- m < x ∙ y > = Group._∙_ m x y + +-- _<_≈_> : (m : Group c c ) → (f g : Group.Carrier m ) → Set c +-- m < x ≈ y > = Group._≈_ m x y + +-- infixr 9 _<_∙_> + +-- +-- Coset : N : NormalSubGroup → { a ∙ n | G ∋ a , N ∋ n } +-- + +open GroupMorphisms + +-- import Axiom.Extensionality.Propositional +-- postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m + +open import Data.Empty +open import Relation.Nullary + +-- Set of a ∙ ∃ n ∈ N +-- +record an {A : Group c c } (N : NormalSubGroup A ? ) (n x : Group.Carrier A ) : Set c where + open Group A + open NormalSubGroup N + field + a : Carrier + aN=x : a ∙ ⟦ n ⟧ ≈ x + +record aN {A : Group c c } (N : NormalSubGroup A ? ) : Set c where + open Group A + field + n : Carrier + is-an : (x : Carrier) → an N n x + +f0 : {A : Group c c } (N : NormalSubGroup A ? ) (x y : Group.Carrier A) → an N x y +f0 {A} N x y = record { a = y ∙ ⟦ x ⟧ ⁻¹ ; aN=x = gk02 } where + open Group A + open NormalSubGroup N + open IsGroupHomomorphism normal + open EqReasoning (Algebra.Group.setoid A) + open Gutil A + gk02 : {x g : Carrier } → x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈ x + gk02 {x} {g} = begin x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈⟨ solve monoid ⟩ + x ∙ ( ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧) ≈⟨ ∙-cong grefl (proj₁ inverse _ ) ⟩ + x ∙ ε ≈⟨ proj₂ identity _ ⟩ + x ∎ + +_/_ : (A : Group c c ) (N : NormalSubGroup A ? ) → Group c c +_/_ A N = record { + Carrier = aN N + ; _≈_ = λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧ + ; _∙_ = qadd + ; ε = qid + ; _⁻¹ = λ f → record { n = n f ⁻¹ ; is-an = λ x → record { a = an.a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧ ; aN=x = qinv0 f x } } + ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { + isEquivalence = record {refl = grefl ; trans = gtrans ; sym = gsym } + ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gtrans (homo _ _) ( gtrans (∙-cong x=y u=v) (gsym (homo _ _) )) } + ; assoc = qassoc } + ; identity = (λ q → ⟦⟧-cong (proj₁ identity _) ) , (λ q → ⟦⟧-cong (proj₂ identity _) ) } + ; inverse = (λ x → ⟦⟧-cong (proj₁ inverse _ )) , (λ x → ⟦⟧-cong (proj₂ inverse _ ) ) + ; ⁻¹-cong = λ {x} {y} → i-conv {x} {y} + } + } where + open Group A + open aN + open an + open NormalSubGroup N + open IsGroupHomomorphism normal + open EqReasoning (Algebra.Group.setoid A) + open Gutil A + qadd : (f g : aN N) → aN N + qadd f g = record { n = n f ∙ n g ; is-an = λ x → record { a = x ⁻¹ ∙ ( a (is-an f x) ∙ a (is-an g x)) ; aN=x = qadd0 } } where + qadd0 : {x : Carrier} → x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈ x + qadd0 {x} = begin + x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈⟨ solve monoid ⟩ + x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x) ∙ ⟦ n f ∙ n g ⟧) ≈⟨ ? ⟩ + x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x) ∙ ( ⟦ n f ⟧ ∙ ⟦ n g ⟧ )) ≈⟨ solve monoid ⟩ + x ⁻¹ ∙ (a (is-an f x) ∙ ( a (is-an g x) ∙ ⟦ n f ⟧) ∙ ⟦ n g ⟧) ≈⟨ ? ⟩ + x ⁻¹ ∙ (a (is-an f x) ∙ ( ⟦ n f ⟧ ∙ a (is-an g x) ) ∙ ⟦ n g ⟧) ≈⟨ ? ⟩ + x ⁻¹ ∙ ((a (is-an f x) ∙ ⟦ n f ⟧ ) ∙ ( a (is-an g x) ∙ ⟦ n g ⟧)) ≈⟨ ? ⟩ + x ⁻¹ ∙ (x ∙ x) ≈⟨ solve monoid ⟩ + (x ⁻¹ ∙ x ) ∙ x ≈⟨ ? ⟩ + ε ∙ x ≈⟨ solve monoid ⟩ + x ∎ + qinv0 : (f : aN N) → (x : Carrier ) → (a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧) ∙ ⟦ n f ⁻¹ ⟧ ≈ x + qinv0 f x = begin + (a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧) ∙ ⟦ n f ⁻¹ ⟧ ≈⟨ ? ⟩ + a (is-an f x) ∙ ⟦ n f ⟧ ≈⟨ an.aN=x (is-an f x) ⟩ + x ∎ + qid : aN N + qid = record { n = ε ; is-an = λ x → record { a = x ; aN=x = qid1 } } where + qid1 : {x : Carrier } → x ∙ ⟦ ε ⟧ ≈ x + qid1 {x} = begin + x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong grefl ε-homo ⟩ + x ∙ ε ≈⟨ proj₂ identity _ ⟩ + x ∎ + qassoc : (f g h : aN N) → ⟦ n ( qadd (qadd f g) h) ⟧ ≈ ⟦ n( qadd f (qadd g h)) ⟧ + qassoc f g h = ⟦⟧-cong (assoc _ _ _ ) + i-conv : {x y : aN N} → ⟦ n x ⟧ ≈ ⟦ n y ⟧ → ⟦ n x ⁻¹ ⟧ ≈ ⟦ n y ⁻¹ ⟧ + i-conv {x} {y} nx=ny = begin + ⟦ n x ⁻¹ ⟧ ≈⟨ ⁻¹-homo _ ⟩ + ⟦ n x ⟧ ⁻¹ ≈⟨ ⁻¹-cong nx=ny ⟩ + ⟦ n y ⟧ ⁻¹ ≈⟨ gsym ( ⁻¹-homo _) ⟩ + ⟦ n y ⁻¹ ⟧ ∎ + + +-- K ⊂ ker(f) +K⊆ker : (G H : Group c c) (K : NormalSubGroup G ?) (f : Group.Carrier G → Group.Carrier H ) → Set c +K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε where + open Group H + open NormalSubGroup K + +open import Function.Surjection +open import Function.Equality + +module GK (G : Group c c) (K : NormalSubGroup G ? ) where + open Group G + open aN + open an + open NormalSubGroup K + open IsGroupHomomorphism normal + open EqReasoning (Algebra.Group.setoid G) + open Gutil G + + φ : Group.Carrier G → Group.Carrier (G / K ) + φ g = record { n = g ; is-an = λ x → record { a = x ∙ ( ⟦ g ⟧ ⁻¹) ; aN=x = gk02 } } where + gk02 : {x : Carrier } → x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈ x + gk02 {x} = begin x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈⟨ solve monoid ⟩ + x ∙ ( ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧) ≈⟨ ∙-cong grefl (proj₁ inverse _ ) ⟩ + x ∙ ε ≈⟨ proj₂ identity _ ⟩ + x ∎ + + φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ + φ-homo = record {⁻¹-homo = λ g → ? ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism = + record { cong = ? } }}} + + -- gk03 : {f : Group.Carrier (G / K) } → ⟦ n f ⟧ ≈ ⟦ ⟦ n f ⟧ ⟧ -- a (is-an f x) ∙ ⟦ n f ⟧ ≡ x + -- gk03 {x} = ? -- + + φe : (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K)) + φe = record { _⟨$⟩_ = φ ; cong = ? } where + φ-cong : {f g : Carrier } → f ≈ g → ⟦ n (φ f ) ⟧ ≈ ⟦ n (φ g ) ⟧ + φ-cong = ? + + inv-φ : Group.Carrier (G / K ) → Group.Carrier G + inv-φ f = n f -- ⟦ n f ⟧ ( if we have gk03 ) + + cong-i : {f g : Group.Carrier (G / K ) } → ⟦ n f ⟧ ≈ ⟦ n g ⟧ → inv-φ f ≈ inv-φ g + cong-i {f} {g} nf=ng = ? + + is-inverse : (f : aN K ) → ⟦ n (φ (inv-φ f) ) ⟧ ≈ ⟦ n f ⟧ + is-inverse f = begin + ⟦ n (φ (inv-φ f) ) ⟧ ≈⟨ grefl ⟩ + ⟦ n (φ ( n f ) ) ⟧ ≈⟨ grefl ⟩ + ⟦ n f ⟧ ∎ + + φ-surjective : Surjective φe + φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse } + + gk01 : (x : Group.Carrier (G / K ) ) → (G / K) < φ ( inv-φ x ) ≈ x > + gk01 x = begin + ⟦ inv-φ x ⟧ ≈⟨ grefl ⟩ + ⟦ n x ⟧ ∎ + + +record FundamentalHomomorphism (G H : Group c c ) + (f : Group.Carrier G → Group.Carrier H ) + (homo : IsGroupHomomorphism (GR G) (GR H) f ) + (K : NormalSubGroup G ? ) (kf : K⊆ker G H K f) : Set c where + open Group H + -- open GK G K + field + h : Group.Carrier (G / K ) → Group.Carrier H + h-homo : IsGroupHomomorphism (GR (G / K) ) (GR H) h + is-solution : (x : Group.Carrier G) → f x ≈ h ? -- ( GK.φ ? x ) + unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 ) + → ( (x : Group.Carrier G) → f x ≈ h1 ? ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) + +FundamentalHomomorphismTheorm : (G H : Group c c) + (f : Group.Carrier G → Group.Carrier H ) + (homo : IsGroupHomomorphism (GR G) (GR H) f ) + (K : NormalSubGroup G ? ) → (kf : K⊆ker G H K f) → FundamentalHomomorphism G H f homo K kf +FundamentalHomomorphismTheorm G H f homo K kf = record { + h = h + ; h-homo = h-homo + ; is-solution = is-solution + ; unique = unique + } where + -- open GK G K + open Group H + open Gutil H + -- open NormalSubGroup K ? + open IsGroupHomomorphism homo + open aN + h : Group.Carrier (G / K ) → Group.Carrier H + h r = f ( GK.inv-φ ? ? ? ) + h03 : (x y : Group.Carrier (G / K ) ) → h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y + h03 x y = {!!} + h-homo : IsGroupHomomorphism (GR (G / K ) ) (GR H) h + h-homo = record { + isMonoidHomomorphism = record { + isMagmaHomomorphism = record { + isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } + ; homo = h03 } + ; ε-homo = {!!} } + ; ⁻¹-homo = {!!} } + open EqReasoning (Algebra.Group.setoid H) + is-solution : (x : Group.Carrier G) → f x ≈ h ( GK.φ ? ? x ) + is-solution x = begin + f x ≈⟨ grefl ⟩ + h ( GK.φ ? ? x ) ∎ + unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H) → (h1-homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 ) + → ( (x : Group.Carrier G) → f x ≈ h1 ( GK.φ ? ? x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x ) + unique h1 h1-homo h1-is-solution x = begin + h x ≈⟨ grefl ⟩ + f ( GK.inv-φ ? ? x ) ≈⟨ h1-is-solution _ ⟩ + h1 ( GK.φ ? ? ( GK.inv-φ ? ? x ) ) ≈⟨ IsGroupHomomorphism.⟦⟧-cong h1-homo (GK.gk01 ? ? x) ⟩ + h1 x ∎ + + + + + +