Mercurial > hg > Members > kono > Proof > galois
changeset 279:386ece574509
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 28 Jan 2023 10:55:32 +0900 |
| parents | ed06f82988c1 |
| children | 523adaf1dcec |
| files | src/Fundamental.agda src/Gutil.agda src/Gutil0.agda src/Solvable.agda |
| diffstat | 4 files changed, 108 insertions(+), 141 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Fundamental.agda Fri Jan 27 11:12:14 2023 +0900 +++ b/src/Fundamental.agda Sat Jan 28 10:55:32 2023 +0900 @@ -13,6 +13,7 @@ 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 @@ -61,7 +62,7 @@ ⟦_⟧ : Group.Carrier A → Group.Carrier A normal : IsGroupHomomorphism (GR A) (GR A) ⟦_⟧ comm : {a b : Carrier } → b ∙ ⟦ a ⟧ ≈ ⟦ a ⟧ ∙ b - -- this is not explict stared in the standard group theory + -- factor : (a b : Carrier) → Carrier is-factor : (a b : Carrier) → b ∙ ⟦ factor a b ⟧ ≈ a @@ -84,7 +85,7 @@ ; ε = qid ; _⁻¹ = qinv ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { - isEquivalence = record {refl = grefl A ; trans = ? ; sym = ? } + isEquivalence = record {refl = grefl ; trans = ? ; sym = ? } ; ∙-cong = λ {x} {y} {u} {v} x=y u=v {w} → qcong {x} {y} {u} {v} x=y u=v {w} } ; assoc = ? } ; identity = idL , (λ q → ? ) } @@ -97,6 +98,7 @@ open NormalSubGroup N open IsGroupHomomorphism normal open EqReasoning (Algebra.Group.setoid A) + open Gutil A _=n=_ : (f g : (x : Group.Carrier A ) → aN N x ) → Set c f =n= g = {x : Group.Carrier A } → ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ qadd : (f g : (x : Group.Carrier A ) → aN N x ) → (x : Group.Carrier A ) → aN N x @@ -105,18 +107,18 @@ q00 = begin ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩ x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧ ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩ - x ⁻¹ ∙ (a (f x) ∙ ((a (g x) ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl A) (∙-cong (grefl A) (∙-cong comm (grefl A) )) ⟩ + x ⁻¹ ∙ (a (f x) ∙ ((a (g x) ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl ) (∙-cong (grefl ) (∙-cong comm (grefl ) )) ⟩ x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧ ∙ a (g x)) ∙ ⟦ n (g x) ⟧ )) ≈⟨ solve monoid ⟩ - x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ ) ≈⟨ ∙-cong (grefl A) (aN=x (g x) ) ⟩ - x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x ≈⟨ ∙-cong (∙-cong (grefl A) (aN=x (f x))) (grefl A) ⟩ - (x ⁻¹ ∙ x ) ∙ x ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl A) ⟩ + x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ ) ≈⟨ ∙-cong (grefl ) (aN=x (g x) ) ⟩ + x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x ≈⟨ ∙-cong (∙-cong (grefl ) (aN=x (f x))) (grefl ) ⟩ + (x ⁻¹ ∙ x ) ∙ x ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl ) ⟩ ε ∙ x ≈⟨ solve monoid ⟩ x ∎ qid : ( x : Carrier ) → aN N x qid x = record { a = x ; n = ε ; aN=x = qid1 } where qid1 : x ∙ ⟦ ε ⟧ ≈ x qid1 = begin - x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl A) ε-homo ⟩ + x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl ) ε-homo ⟩ x ∙ ε ≈⟨ solve monoid ⟩ x ∎ qinv : (( x : Carrier ) → aN N x) → ( x : Carrier ) → aN N x @@ -126,14 +128,14 @@ x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ x ∙ ⟦ (n (f x)) ⁻¹ ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ x ∙ ⟦ ((n (f x)) ⁻¹ ) ∙ n (f x) ⟧ ≈⟨ ? ⟩ - x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl A) ε-homo ⟩ + x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl ) ε-homo ⟩ x ∙ ε ≈⟨ solve monoid ⟩ x ∎ qcong : { x y u v : (x₁ : Carrier) → aN N x₁ } → (x=y : x =n= y) ( u=v : u =n= v ) → qadd x u =n= qadd y v qcong {x} {y} {u} {v} x=y u=v {w} = begin ⟦ n (x w) ∙ n (u w) ⟧ ≈⟨ homo _ _ ⟩ ⟦ n (x w) ⟧ ∙ ⟦ n (u w) ⟧ ≈⟨ ∙-cong x=y u=v ⟩ - ⟦ n (y w) ⟧ ∙ ⟦ n (v w) ⟧ ≈⟨ gsym A ( homo _ _) ⟩ + ⟦ n (y w) ⟧ ∙ ⟦ n (v w) ⟧ ≈⟨ gsym ( homo _ _) ⟩ ⟦ n (y w) ∙ n (v w) ⟧ ∎ idL : (f : (x : Carrier )→ aN N x) → (qadd qid f ) =n= f idL f = ? @@ -153,6 +155,7 @@ open NormalSubGroup K open IsGroupHomomorphism normal open EqReasoning (Algebra.Group.setoid G) + open Gutil G φ : Group.Carrier G → Group.Carrier (G / K ) φ g x = record { a = g ; n = factor x g ; aN=x = is-factor x g } @@ -166,7 +169,7 @@ φ-cong : {f g : Carrier } → f ≈ g → {x : Carrier } → ⟦ n (φ f x ) ⟧ ≈ ⟦ n (φ g x ) ⟧ φ-cong = ? - -- inverse of φ + -- inverse ofφ -- f = λ x → record { a = af ; n = fn ; aN=x = x ≈ af ∙ ⟦ fn ⟧ ) = (af)K , fn ≡ factor x af , af ≡ a (f x) -- (inv-φ f)K ≡ (af)K -- φ (inv-φ f) x → f (h0 x) @@ -188,23 +191,54 @@ _∋_ : (f : Group.Carrier (G / K)) (x : Carrier ) → Set c _∋_ f x = a (f x) ∙ ⟦ n (f x) ⟧ ≈ x - aNeq : {f g : Group.Carrier (G / K)} → (G / K) < f ≈ g > - → ( {x : Carrier } → f ∋ x → g ∋ x ) × ( {x : Carrier } → g ∋ x → f ∋ x ) - aNeq {f} {g} f=g = an00 , ? where - an00 : {x : Carrier} → f ∋ x → g ∋ x - an00 {x} fnx = begin - a (g x) ∙ ⟦ n (g x) ⟧ ≈⟨ ∙-cong (gsym G (an01 (fgf ⁻¹ ∙ a (f x)))) (gsym G f=g) ⟩ - (fgf ⁻¹ ∙ a (f x)) ∙ ⟦ factor (a (g x)) (⟦ factor (a (g x)) (a (f x)) ⟧ ⁻¹ ∙ a (f x)) ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ - (a (f x) ∙ fgf ⁻¹ ) ∙ ( ⟦ factor (a (g x)) (a (f x)) ⟧ ∙ ⟦ n (f x) ⟧ ) ≈⟨ ? ⟩ - a (f x) ∙ ⟦ n (f x) ⟧ ≈⟨ fnx ⟩ - x ∎ where - fgf = ⟦ factor (a (g x)) (a (f x)) ⟧ - an01 : (y : Carrier) → y ∙ ⟦ factor (a (g x)) y ⟧ ≈ a (g x) - an01 y = is-factor (a (g x)) y - an03 : ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε + an02 : (f : Group.Carrier (G / K)) → {x : Carrier } → a (f x) ≈ x ∙ ⟦ n (f x) ⟧ ⁻¹ + an02 f {x} = begin + a (f x ) ≈⟨ gsym ( proj₂ identity _) ⟩ + a (f x ) ∙ ε ≈⟨ ∙-cong (grefl ) (gsym (proj₂ inverse _)) ⟩ + a (f x ) ∙ ( ⟦ n (f x) ⟧ ∙ ⟦ n (f x) ⟧ ⁻¹) ≈⟨ solve monoid ⟩ + (a (f x ) ∙ ⟦ n (f x) ⟧) ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ ∙-cong (aN=x (f x)) (grefl ) ⟩ + x ∙ ⟦ n (f x) ⟧ ⁻¹ ∎ + + aNeqε : {f g : Group.Carrier (G / K)} → (G / K) < f ≈ g > + → {x : Carrier } → ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε + aNeqε {f} {g} f=g {x} = begin + ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ ? ⟩ + ε ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ ? ⟩ + (a (f x) ⁻¹ ∙ a (f x)) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ solve monoid ⟩ + a (f x) ⁻¹ ∙ (a (f x) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ) ≈⟨ ? ⟩ + a (f x) ⁻¹ ∙ a (g x) ≈⟨ ∙-cong (⁻¹-cong (an02 f) ) (an02 g) ⟩ + (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⁻¹ ∙ (x ∙ ⟦ n (g x) ⟧ ⁻¹ ) ≈⟨ ? ⟩ + (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⁻¹ ∙ (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ≈⟨ ? ⟩ + ( ⟦ n (f x) ⟧ ∙ x ⁻¹ ) ∙ (x ∙ ⟦ n (f x) ⟧ ⁻¹ ) ≈⟨ ? ⟩ + ⟦ n (f x) ⟧ ∙ ( x ⁻¹ ∙ x ) ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ ? ⟩ + ⟦ n (f x) ⟧ ∙ ε ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ solve monoid ⟩ + ⟦ n (f x) ⟧ ∙ ⟦ n (f x) ⟧ ⁻¹ ≈⟨ proj₂ inverse _ ⟩ + ε ∎ where + an01 : a (f x) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ a (g x) + an01 = is-factor (a (g x)) (a (f x)) + an03 : {f : Group.Carrier (G / K)} → {x : Carrier } → a (f x) ⁻¹ ≈ x ∙ ⟦ n (f x) ⟧ an03 = ? - an02 : ⟦ factor (a (g x)) (⟦ factor (a (g x)) (a (f x)) ⟧ ⁻¹ ∙ a (f x)) ⟧ ≈ ⟦ factor (a (g x)) (a (f x)) ⟧ - an02 = ? + + f≈g→g⊆f : {f g : Group.Carrier (G / K)} → (G / K) < f ≈ g > → {x : Carrier} → f ∋ x → g ∋ x + f≈g→g⊆f {f} {g} f=g {x} fnx = begin + a (g x) ∙ ⟦ n (g x) ⟧ ≈⟨ ∙-cong (gsym (an01 (fgf ⁻¹ ∙ a (f x)))) (gsym f=g) ⟩ + (fgf ⁻¹ ∙ a (f x)) ∙ ⟦ factor (a (g x)) (⟦ factor (a (g x)) (a (f x)) ⟧ ⁻¹ ∙ a (f x)) ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + (fgf ⁻¹ ∙ a (f x)) ∙ ⟦ factor (a (g x)) (ε ⁻¹ ∙ a (f x)) ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + (fgf ⁻¹ ∙ a (f x)) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + (a (f x) ∙ fgf ⁻¹ ) ∙ ( ⟦ factor (a (g x)) (a (f x)) ⟧ ∙ ⟦ n (f x) ⟧ ) ≈⟨ solve monoid ⟩ + a (f x) ∙ (fgf ⁻¹ ∙ ⟦ factor (a (g x)) (a (f x)) ⟧) ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + a (f x) ∙ ε ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + a (f x) ∙ ⟦ n (f x) ⟧ ≈⟨ fnx ⟩ + x ∎ where + fgf = ⟦ factor (a (g x)) (a (f x)) ⟧ + an01 : (y : Carrier) → y ∙ ⟦ factor (a (g x)) y ⟧ ≈ a (g x) + an01 y = is-factor (a (g x)) y + an03 : ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε + an03 = ? + + f≈g→f=g : {f g : Group.Carrier (G / K)} → (G / K) < f ≈ g > + → ( {x : Carrier } → f ∋ x → g ∋ x ) × ( {x : Carrier } → g ∋ x → f ∋ x ) + f≈g→f=g {f} {g} f=g = f≈g→g⊆f {f} {g} f=g , f≈g→g⊆f {g} {f} (gsym f=g) cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ f ≈ inv-φ g cong-i = ? @@ -214,28 +248,45 @@ ... | record { a = fa ; n = fn ; aN=x = faN=x } = begin ⟦ factor y z ⟧ ≈⟨ ? ⟩ z ⁻¹ ∙ ( z ∙ ⟦ factor y z ⟧ ) ≈⟨ ? ⟩ - z ⁻¹ ∙ y ≈⟨ ∙-cong (grefl G) (gsym G faN=x ) ⟩ + z ⁻¹ ∙ y ≈⟨ ∙-cong (grefl ) (gsym faN=x ) ⟩ z ⁻¹ ∙ ( fa ∙ ⟦ fn ⟧ ) ≈⟨ ? ⟩ (z ⁻¹ ∙ fa ) ∙ ⟦ fn ⟧ ≈⟨ ? ⟩ ε ∙ ⟦ fn ⟧ ≈⟨ solve monoid ⟩ ⟦ fn ⟧ ∎ where z = fa ⁻¹ - k*factor : {x y z : Carrier } → ⟦ factor y x ⟧ ≈ ⟦ factor (z ∙ y) x ⟧ - k*factor {x} {y} {z} = ? - - cong-factor : {x y z : Carrier } → ⟦ factor y x ⟧ ≈ ⟦ factor y z ⟧ - cong-factor {x} {y} {z} = begin - ⟦ factor y x ⟧ ≈⟨ ? ⟩ - ⟦ factor ( x ∙ z ⁻¹ ∙ y ) x ⟧ ≈⟨ ? ⟩ - x ⁻¹ ∙ ( x ∙ z ⁻¹ ∙ y ) ≈⟨ ? ⟩ - z ⁻¹ ∙ y ≈⟨ ? ⟩ - ⟦ factor y z ⟧ ∎ + φ-factor : (f : Group.Carrier ( G / K )) → {x y : Carrier } → f ∋ x → f ∋ y → ⟦ n (f x) ⟧ ≈ ⟦ n (f y) ⟧ + φ-factor f {x} {y} gx gy = begin + ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + (a (f x)) ⁻¹ ∙ x ≈⟨ ? ⟩ + (((a (f y)) ⁻¹ ∙ y ) ∙ ((a (f y)) ⁻¹ ∙ y )) ⁻¹ ∙ ( (a (f x)) ⁻¹ ∙ x ) ≈⟨ ? ⟩ + ((a (f y)) ⁻¹ ∙ y ) ∙ (((a (f y)) ⁻¹ ∙ y ) ⁻¹ ∙ ( (a (f x)) ⁻¹ ∙ x )) ≈⟨ ? ⟩ + ((a (f y)) ⁻¹ ∙ y ) ∙ (⟦ n (f y) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧) ≈⟨ ? ⟩ + ((a (f y)) ⁻¹ ∙ y ) ∙ (⟦ n (f y) ⁻¹ ⟧ ∙ ⟦ n (f x) ⟧) ≈⟨ ? ⟩ + ((a (f y)) ⁻¹ ∙ y ) ∙ (⟦ n (f y) ⁻¹ ∙ n (f x) ⟧) ≈⟨ ? ⟩ + ((a (f y)) ⁻¹ ∙ y ) ∙ ε ≈⟨ ? ⟩ + (a (f y)) ⁻¹ ∙ y ≈⟨ ? ⟩ + ⟦ n (f y) ⟧ ∎ where + fa00 : a (f x) ∙ ⟦ n (f x) ⟧ ≈ x + fa00 = gx + fa01 : a (f y) ∙ ⟦ n (f y) ⟧ ≈ y + fa01 = gy + an01 : (y : Carrier) → y ∙ ⟦ factor (a (f x)) y ⟧ ≈ a (f x) + an01 y = is-factor (a (f x)) y + an04 : a (f y) ∙ ⟦ factor (a (f x)) (a (f y)) ⟧ ≈ a (f x) + an04 = is-factor (a (f x)) (a (f y)) + an03 : ⟦ n (f y) ⁻¹ ∙ n (f x) ⟧ ≈ ε + an03 = begin + ⟦ n (f y) ⁻¹ ∙ n (f x) ⟧ ≈⟨ ? ⟩ + ⟦ n (f y) ⁻¹ ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + ⟦ n (f y) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + ⟦ n (f y) ⟧ ⁻¹ ∙ (a (f x) ∙ x ⁻¹ ) ≈⟨ ? ⟩ + ε ∎ is-inverse : (f : (x : Carrier) → aN K x ) → {y : Carrier} → ⟦ n (φ (inv-φ f) y) ⟧ ≈ ⟦ n (f y) ⟧ is-inverse f {y} = begin - ⟦ n (φ (inv-φ f) y) ⟧ ≈⟨ grefl G ⟩ - ⟦ n (φ (a (f ε)) y) ⟧ ≈⟨ grefl G ⟩ + ⟦ n (φ (inv-φ f) y) ⟧ ≈⟨ grefl ⟩ + ⟦ n (φ (a (f ε)) y) ⟧ ≈⟨ grefl ⟩ ⟦ factor y (a (f ε)) ⟧ ≈⟨ ? ⟩ -- a (f ε) ∙ ⟦ factor y ( a (f ε)) ⟧ ≈ y ⟦ factor y ((a (f y)) ⁻¹) ⟧ ≈⟨ factor=nf f ⟩ -- a (f y) ∙ ⟦ factor y ( a (f y)) ⟧ ≈ y ⟦ n (f y) ⟧ ∎ where -- a (f y) ∙ ⟦ n (f y) ⟧ ≈ y @@ -252,7 +303,7 @@ (a (f y)) ⁻¹ ∎ φ-surjective : Surjective φe - φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse } where + φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse } record FundamentalHomomorphism (G H : Group c c ) (f : Group.Carrier G → Group.Carrier H )
--- a/src/Gutil.agda Fri Jan 27 11:12:14 2023 +0900 +++ b/src/Gutil.agda Sat Jan 28 10:55:32 2023 +0900 @@ -20,15 +20,15 @@ grefl = Algebra.Group.refl G gtrans = Algebra.Group.trans G -lemma3 : ε ≈ ε ⁻¹ -lemma3 = begin +ε≈ε⁻¹ : ε ≈ ε ⁻¹ +ε≈ε⁻¹ = begin ε ≈⟨ gsym (proj₁ inverse _) ⟩ ε ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩ ε ⁻¹ ∎ where open EqReasoning (Algebra.Group.setoid G) -lemma6 : {f : Carrier } → ( f ⁻¹ ) ⁻¹ ≈ f -lemma6 {f} = begin +f⁻¹⁻¹≈f : {f : Carrier } → ( f ⁻¹ ) ⁻¹ ≈ f +f⁻¹⁻¹≈f {f} = begin ( f ⁻¹ ) ⁻¹ ≈⟨ gsym ( proj₁ identity _) ⟩ ε ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩ (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ assoc _ _ _ ⟩ @@ -40,100 +40,23 @@ ≡→≈ : {f g : Carrier } → f ≡ g → f ≈ g ≡→≈ refl = grefl ---- --- to avoid assoc storm, flatten multiplication according to the template --- - -data MP : Carrier → Set (Level.suc n) where - am : (x : Carrier ) → MP x - _o_ : {x y : Carrier } → MP x → MP y → MP ( x ∙ y ) - -mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier -mpf (am x) y = x ∙ y -mpf (m o m₁) y = mpf m ( mpf m₁ y ) - -mp-flatten : {x : Carrier } → (m : MP x ) → Carrier -mp-flatten m = mpf m ε +car : {f g h : Carrier } → f ≈ g → f ∙ h ≈ g ∙ h +car f=g = ∙-cong f=g grefl -mpl1 : Carrier → {x : Carrier } → MP x → Carrier -mpl1 x (am y) = x ∙ y -mpl1 x (y o y1) = mpl1 ( mpl1 x y ) y1 - -mpl : {x z : Carrier } → MP x → MP z → Carrier -mpl (am x) m = mpl1 x m -mpl (m o m1) m2 = mpl m (m1 o m2) - -mp-flattenl : {x : Carrier } → (m : MP x ) → Carrier -mp-flattenl m = mpl m (am ε) - -test1 : ( f g : Carrier ) → Carrier -test1 f g = mp-flattenl ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) - -test2 : ( f g : Carrier ) → test1 f g ≡ g ⁻¹ ∙ f ⁻¹ ∙ f ∙ g ∙ (f ∙ g) ⁻¹ ∙ ε -test2 f g = _≡_.refl - -test3 : ( f g : Carrier ) → Carrier -test3 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) +cdr : {f g h : Carrier } → f ≈ g → h ∙ f ≈ h ∙ g +cdr f=g = ∙-cong grefl f=g -test4 : ( f g : Carrier ) → test3 f g ≡ g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))) -test4 f g = _≡_.refl +-- module _ where +-- open EqReasoning (Algebra.Group.setoid G) +-- _≈⟨⟩_ : (a : Carrier ) → {b : Carrier} → a IsRelatedTo b → a IsRelatedTo b +-- _ ≈⟨⟩ a = a - -∙-flatten : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten m -∙-flatten {x} (am x) = gsym (proj₂ identity _) -∙-flatten {_} (am x o q) = ∙-cong grefl ( ∙-flatten q ) -∙-flatten (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ ( ∙-flatten {x ∙ y } (p o q )) ( ∙-flatten {z} r ) where - mp-cong : {p q r : Carrier} → (P : MP p) → q ≈ r → mpf P q ≈ mpf P r - mp-cong (am x) q=r = ∙-cong grefl q=r - mp-cong (P o P₁) q=r = mp-cong P ( mp-cong P₁ q=r ) - mp-assoc : {p q r : Carrier} → (P : MP p) → mpf P q ∙ r ≈ mpf P (q ∙ r ) - mp-assoc (am x) = assoc _ _ _ - mp-assoc {p} {q} {r} (P o P₁) = begin - mpf P (mpf P₁ q) ∙ r ≈⟨ mp-assoc P ⟩ - mpf P (mpf P₁ q ∙ r) ≈⟨ mp-cong P (mp-assoc P₁) ⟩ mpf P ((mpf P₁) (q ∙ r)) - ∎ where open EqReasoning (Algebra.Group.setoid G) - lemma9 : (x y z : Carrier) → x ∙ y ≈ mpf p (mpf q ε) → z ≈ mpf r ε → x ∙ y ∙ z ≈ mp-flatten ((p o q) o r) - lemma9 x y z t s = begin - x ∙ y ∙ z ≈⟨ ∙-cong t grefl ⟩ - mpf p (mpf q ε) ∙ z ≈⟨ mp-assoc p ⟩ - mpf p (mpf q ε ∙ z) ≈⟨ mp-cong p (mp-assoc q ) ⟩ - mpf p (mpf q (ε ∙ z)) ≈⟨ mp-cong p (mp-cong q (proj₁ identity _ )) ⟩ - mpf p (mpf q z) ≈⟨ mp-cong p (mp-cong q s) ⟩ - mpf p (mpf q (mpf r ε)) - ∎ where open EqReasoning (Algebra.Group.setoid G) - -grepl : { x y0 y1 z : Carrier } → x ∙ y0 ≈ y1 → x ∙ ( y0 ∙ z ) ≈ y1 ∙ z -grepl eq = gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl ) - -grm : { x y0 y1 z : Carrier } → x ∙ y0 ≈ ε → x ∙ ( y0 ∙ z ) ≈ z -grm eq = gtrans ( gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl )) ( proj₁ identity _ ) - --- ∙-flattenl : {x : Carrier } → (m : MP x ) → x ≈ mp-flattenl m --- ∙-flattenl (am x) = gsym (proj₂ identity _) --- ∙-flattenl (q o am x) with ∙-flattenl q -- x₁ ∙ x ≈ mpl q (am x o am ε) , t : x₁ ≈ mpl q (am ε) --- ... | t = {!!} --- ∙-flattenl (q o (x o y )) with ∙-flattenl q --- ... | t = gtrans (gsym (assoc _ _ _ )) {!!} +open import Tactic.MonoidSolver using (solve; solve-macro) lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹ lemma5 f g = begin g ⁻¹ ∙ f ⁻¹ ≈⟨ gsym (proj₂ identity _) ⟩ g ⁻¹ ∙ f ⁻¹ ∙ ε ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩ - g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ ∙-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) ⟩ - g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))) ≈⟨ ∙-cong grefl (gsym (assoc _ _ _ )) ⟩ - g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))) ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩ - g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)) ≈⟨ gsym (assoc _ _ _) ⟩ - (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε) ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩ - (f ∙ g) ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩ - (f ∙ g) ⁻¹ - ∎ where open EqReasoning (Algebra.Group.setoid G) - -open import Tactic.MonoidSolver using (solve; solve-macro) - -lemma7 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹ -lemma7 f g = begin - g ⁻¹ ∙ f ⁻¹ ≈⟨ gsym (proj₂ identity _) ⟩ - g ⁻¹ ∙ f ⁻¹ ∙ ε ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩ g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ solve monoid ⟩ g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))) ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩ g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)) ≈⟨ solve monoid ⟩ @@ -142,3 +65,4 @@ (f ∙ g) ⁻¹ ∎ where open EqReasoning (Algebra.Group.setoid G) +
--- a/src/Gutil0.agda Fri Jan 27 11:12:14 2023 +0900 +++ b/src/Gutil0.agda Sat Jan 28 10:55:32 2023 +0900 @@ -45,14 +45,6 @@ Eq G = IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup (IsGroup.isMonoid (Group.isGroup G ))) ) -grefl : {c l : Level } → (G : Group c l ) → {x : Group.Carrier G} → Group._≈_ G x x -grefl G = IsGroup.refl ( Group.isGroup G ) - -gsym : {c l : Level } → (G : Group c l ) → {x y : Group.Carrier G} → Group._≈_ G x y → Group._≈_ G y x -gsym G = IsGroup.sym ( Group.isGroup G ) - -gtrans : {c l : Level } → (G : Group c l ) → {x y z : Group.Carrier G} → Group._≈_ G x y → Group._≈_ G y z → Group._≈_ G x z -gtrans G = IsGroup.trans ( Group.isGroup G ) -- record NormalSubGroup {c l : Level } ( G : Group c l ) : Set ( c Level.⊔ l ) where -- open Group G
--- a/src/Solvable.agda Fri Jan 27 11:12:14 2023 +0900 +++ b/src/Solvable.agda Sat Jan 28 10:55:32 2023 +0900 @@ -47,7 +47,7 @@ lemma4 g h = begin [ h , g ] ≈⟨ grefl ⟩ (h ⁻¹ ∙ g ⁻¹ ∙ h ) ∙ g ≈⟨ assoc _ _ _ ⟩ - h ⁻¹ ∙ g ⁻¹ ∙ (h ∙ g) ≈⟨ ∙-cong grefl (gsym (∙-cong lemma6 lemma6)) ⟩ + h ⁻¹ ∙ g ⁻¹ ∙ (h ∙ g) ≈⟨ ∙-cong grefl (gsym (∙-cong f⁻¹⁻¹≈f f⁻¹⁻¹≈f)) ⟩ h ⁻¹ ∙ g ⁻¹ ∙ ((h ⁻¹) ⁻¹ ∙ (g ⁻¹) ⁻¹) ≈⟨ ∙-cong grefl (lemma5 _ _ ) ⟩ h ⁻¹ ∙ g ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹) ⁻¹ ≈⟨ assoc _ _ _ ⟩ h ⁻¹ ∙ (g ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹) ⁻¹) ≈⟨ ∙-cong grefl (lemma5 (g ⁻¹ ∙ h ⁻¹ ) g ) ⟩ @@ -63,7 +63,7 @@ idcomtr : (g : Carrier ) → [ g , ε ] ≈ ε idcomtr g = begin - (g ⁻¹ ∙ ε ⁻¹ ∙ g ∙ ε ) ≈⟨ ∙-cong (∙-cong (∙-cong grefl (sym lemma3 )) grefl ) grefl ⟩ + (g ⁻¹ ∙ ε ⁻¹ ∙ g ∙ ε ) ≈⟨ ∙-cong (∙-cong (∙-cong grefl (sym ε≈ε⁻¹ )) grefl ) grefl ⟩ (g ⁻¹ ∙ ε ∙ g ∙ ε ) ≈⟨ ∙-cong (∙-cong (proj₂ identity _) grefl) grefl ⟩ (g ⁻¹ ∙ g ∙ ε ) ≈⟨ ∙-cong (proj₁ inverse _ ) grefl ⟩ ( ε ∙ ε ) ≈⟨ proj₂ identity _ ⟩ @@ -73,7 +73,7 @@ idcomtl : (g : Carrier ) → [ ε , g ] ≈ ε idcomtl g = begin (ε ⁻¹ ∙ g ⁻¹ ∙ ε ∙ g ) ≈⟨ ∙-cong (proj₂ identity _) grefl ⟩ - (ε ⁻¹ ∙ g ⁻¹ ∙ g ) ≈⟨ ∙-cong (∙-cong (sym lemma3 ) grefl ) grefl ⟩ + (ε ⁻¹ ∙ g ⁻¹ ∙ g ) ≈⟨ ∙-cong (∙-cong (sym ε≈ε⁻¹ ) grefl ) grefl ⟩ (ε ∙ g ⁻¹ ∙ g ) ≈⟨ ∙-cong (proj₁ identity _) grefl ⟩ (g ⁻¹ ∙ g ) ≈⟨ proj₁ inverse _ ⟩ ε