Mercurial > hg > Members > kono > Proof > galois
changeset 281:803f909fdd17
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 29 Jan 2023 08:19:19 +0900 |
| parents | 523adaf1dcec |
| children | b70cc2534d2f |
| files | src/Fundamental.agda |
| diffstat | 1 files changed, 60 insertions(+), 74 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Fundamental.agda Sat Jan 28 17:10:05 2023 +0900 +++ b/src/Fundamental.agda Sun Jan 29 08:19:19 2023 +0900 @@ -50,7 +50,6 @@ -- Coset : N : NormalSubGroup → { a ∙ n | G ∋ a , N ∋ n } -- - open GroupMorphisms import Axiom.Extensionality.Propositional @@ -77,12 +76,6 @@ a n : Group.Carrier A aN=x : a ∙ ⟦ n ⟧ ≈ x -factor' : {A : Group c c } (N : NormalSubGroup A ) (f : (x : Group.Carrier A) → aN N x ) (a b : Group.Carrier A ) → Group.Carrier A -factor' = ? -is-factor' : {A : Group c c } (N : NormalSubGroup A ) (f : (x : Group.Carrier A) → aN N x ) → - (a b : Group.Carrier A ) → A < A < b ∙ ( NormalSubGroup.⟦_⟧ N (factor' {A} N f a b )) > ≈ a > -is-factor' {A} N f a b = ? - _/_ : (A : Group c c ) (N : NormalSubGroup A ) → Group c c _/_ A N = record { Carrier = (x : Group.Carrier A) → aN N x @@ -91,7 +84,7 @@ ; ε = qid ; _⁻¹ = qinv ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { - isEquivalence = record {refl = grefl ; trans = ? ; sym = ? } + isEquivalence = record {refl = ? ; 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 → ? ) } @@ -106,7 +99,7 @@ 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) ⟧ + f =n= g = {x y : Group.Carrier A } → ⟦ n (f x) ⟧ ≈ ⟦ n (g y) ⟧ qadd : (f g : (x : Group.Carrier A ) → aN N x ) → (x : Group.Carrier A ) → aN N x qadd f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where q00 : ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧ ≈ x @@ -138,11 +131,11 @@ 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 + qcong {x} {y} {u} {v} x=y u=v {w} {z} = 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 ( homo _ _) ⟩ - ⟦ n (y w) ∙ n (v w) ⟧ ∎ + ⟦ n (y z) ⟧ ∙ ⟦ n (v z) ⟧ ≈⟨ gsym (homo _ _ ) ⟩ + ⟦ n (y z) ∙ n (v z) ⟧ ∎ idL : (f : (x : Carrier )→ aN N x) → (qadd qid f ) =n= f idL f = ? @@ -171,7 +164,7 @@ record { cong = ? } }}} φe : (Algebra.Group.setoid G) Function.Equality.⟶ (Algebra.Group.setoid (G / K)) - φe = record { _⟨$⟩_ = φ ; cong = φ-cong } where + φe = record { _⟨$⟩_ = φ ; cong = ? } where φ-cong : {f g : Carrier } → f ≈ g → {x : Carrier } → ⟦ n (φ f x ) ⟧ ≈ ⟦ n (φ g x ) ⟧ φ-cong = ? @@ -180,22 +173,9 @@ -- (inv-φ f)K ≡ (af)K -- φ (inv-φ f) x → f (h0 x) -- f x → φ (inv-φ f) (h1 x) - -- - -- inv-φ f ≡ a (f ε) -- not af ≡ a (f x) - -- φ (inv-φ f) returns ( λ x → record { a = a (f ε) ; n = factor x (a (f ε)) ; is-factor x (a (f ε)) ) - -- it should be ( λ x → record { a = af ; n = factor x af ; is-factor x af - -- it should be ( λ x → record { a = af ; n = fn ; is-factor x af - -- ⟦ n (φ (inv-φ f) x) ⟧ ≈ ⟦ n (f x) ⟧ ≈ ⟦ fn ⟧ - -- ⟦ factor x (a (f ε)) ⟧ ≈ ⟦ n (f x) ⟧ ≈ ⟦ fn ⟧ ≈ ⟦ factor x g ⟧ - -- g ∙ ⟦ factor y (a (f ε)) ⟧ ≈ x - -- factor x g - -- g ∙ ⟦ factor y g ⟧ ≈ y inv-φ : Group.Carrier (G / K ) → Group.Carrier G - inv-φ f = a (f ε) - - _∋_ : (f : Group.Carrier (G / K)) (x : Carrier ) → Set c - _∋_ f x = a (f x) ∙ ⟦ n (f x) ⟧ ≈ x + inv-φ f = ⟦ n (f ε) ⟧ ⁻¹ an02 : (f : Group.Carrier (G / K)) → {x : Carrier } → a (f x) ≈ x ∙ ⟦ n (f x) ⟧ ⁻¹ an02 f {x} = begin @@ -225,28 +205,7 @@ an03 : {f : Group.Carrier (G / K)} → {x : Carrier } → a (f x) ⁻¹ ≈ x ∙ ⟦ n (f x) ⟧ an03 = ? - 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 : {f g : Group.Carrier (G / K ) } → ({x y : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (g y) ⟧ ) → inv-φ f ≈ inv-φ g cong-i = ? factor=nf : (f : (x : Carrier) → aN K x ) {y : Carrier} → ⟦ factor y ((a (f y)) ⁻¹ ) ⟧ ≈ ⟦ n (f y) ⟧ @@ -261,33 +220,56 @@ ⟦ fn ⟧ ∎ where z = fa ⁻¹ - φ-factor : (f : Group.Carrier ( G / K )) → {x y : Carrier } → f ∋ x → f ∋ y → ⟦ n (f x) ⟧ ≈ ⟦ n (f y) ⟧ - φ-factor f {x} {y} fx fy = begin + φ-factor : (f : Group.Carrier ( G / K )) → {x y : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (f y) ⟧ + φ-factor f {x} {y} = 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 x) ⟧ ∙ ε ≈⟨ ? ⟩ + ⟦ n (f x) ⟧ ∙ ( ⟦ n (f y) ⟧ ∙ ⟦ n (f y) ⟧ ⁻¹ ) ≈⟨ cdr ( cdr an07 ) ⟩ + ⟦ n (f x) ⟧ ∙ ( ⟦ n (f y) ⟧ ∙ ( ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ factor (⟦ n (f y) ⟧ ⁻¹) (⟦ n (f x) ⟧ ⁻¹) ⟧ )) ≈⟨ ? ⟩ + ⟦ n (f y) ⟧ ∙ ⟦ factor (⟦ n (f y) ⟧ ⁻¹) (⟦ n (f x) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ + ⟦ n (f y) ⟧ ∙ ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈⟨ ? ⟩ + ⟦ n (f y) ⟧ ∙ ε ≈⟨ ? ⟩ ⟦ n (f y) ⟧ ∎ where - fa00 : a (f x) ∙ ⟦ n (f x) ⟧ ≈ x - fa00 = fx - fa01 : a (f y) ∙ ⟦ n (f y) ⟧ ≈ y - fa01 = fy + fxy = ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f y) ⟧ + + fa11 : a (f (x ∙ y ⁻¹ )) ∙ ⟦ n (f (x ∙ y ⁻¹)) ⟧ ≈ x ∙ y ⁻¹ + fa11 = aN=x ( f ( x ∙ y ⁻¹ )) + + fa21 : a (f ε) ∙ ⟦ n (f ε) ⟧ ≈ ε + fa21 = aN=x ( f ε) + + fa22 : {x : Carrier } → a (f (x ⁻¹)) ∙ ⟦ n (f (x ⁻¹)) ⟧ ≈ x ⁻¹ + fa22 {x} = aN=x ( f (x ⁻¹)) + + fa14 : a (f x) ∙ ⟦ n (f x) ⟧ ≈ x + fa14 = aN=x ( f x) + + fa13 : a (f y) ∙ ⟦ n (f y) ⟧ ≈ y + fa13 = aN=x ( f y) + + fa12 : aN K ( x ∙ y ⁻¹ ) + fa12 = f (x ∙ y ⁻¹ ) 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)) an07 : {z w : Carrier} → z ≈ w ∙ ⟦ factor z w ⟧ an07 {z} {w} = gsym ( is-factor z w ) - an05 : {z : Carrier} → f ∋ z → ⟦ n (f z) ⟧ ≈ ⟦ factor z (a (f z)) ⟧ - an05 {z} fz = begin + an10 : ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈ ε + an10 = begin + ⟦ factor (a (f y) ∙ y ⁻¹) (a (f x) ∙ x ⁻¹) ⟧ ≈⟨ ? ⟩ + ( a (f x) ∙ x ⁻¹ ) ⁻¹ ∙ (a (f y) ∙ y ⁻¹) ≈⟨ ? ⟩ + x ∙ a (f x) ⁻¹ ∙ a (f y) ∙ y ⁻¹ ≈⟨ ? ⟩ + ε ∎ + an08 : ⟦ n (f y) ⟧ ∙ ⟦ n (f x) ⟧ ≈ ε + an08 = begin + ⟦ n (f y) ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + ε ∎ + an05 : {z : Carrier} → ⟦ n (f z) ⟧ ≈ ⟦ factor z (a (f z)) ⟧ + an05 {z} = begin ⟦ n (f z) ⟧ ≈⟨ ? ⟩ ((a (f z) ⁻¹) ∙ a (f z)) ∙ ⟦ n (f z) ⟧ ≈⟨ ? ⟩ - (a (f z) ⁻¹) ∙ ( a (f z) ∙ ⟦ n (f z) ⟧) ≈⟨ ∙-cong grefl fz ⟩ + (a (f z) ⁻¹) ∙ ( a (f z) ∙ ⟦ n (f z) ⟧) ≈⟨ ∙-cong grefl (aN=x (f z)) ⟩ (a (f z) ⁻¹) ∙ z ≈⟨ ∙-cong grefl ( gsym ( is-factor z (a (f z)))) ⟩ (a (f z) ⁻¹) ∙ (a (f z) ∙ ⟦ factor z (a (f z)) ⟧ ) ≈⟨ ? ⟩ ⟦ factor z ( a ( f z)) ⟧ ∎ @@ -309,13 +291,17 @@ ⟦ ε ⟧ ≈⟨ ? ⟩ -- ⟦ n (f x) ⟧ ≡ ⟦ n (g x) ⟧ → ⟦ factor (a (g x)) (a (f 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 ⟩ - ⟦ 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 + is-inverse : (f : (x : Carrier) → aN K x ) → {x y : Carrier} → ⟦ n (φ (inv-φ f) x) ⟧ ≈ ⟦ n (f y) ⟧ + is-inverse f {x} {y} = begin + ⟦ n (φ (inv-φ f) x) ⟧ ≈⟨ grefl ⟩ + ⟦ n (φ (⟦ n (f ε) ⟧ ⁻¹) x) ⟧ ≈⟨ grefl ⟩ + ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ + ε ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ + (x ∙ x ⁻¹ ) ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ≈⟨ ? ⟩ + x ∙ ( x ⁻¹ ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ ) ≈⟨ ? ⟩ + x ∙ ⟦ n (f ε) ⟧ ⁻¹ ≈⟨ ? ⟩ + y ∙ ⟦ n (f y) ⟧ ⁻¹ ≈⟨ ? ⟩ + ⟦ n (f y) ⟧ ∎ where afn : a (f ε) ∙ ⟦ n (f ε) ⟧ ≈ ε afn = aN=x (f ε) afn' = (a (f y)) ⁻¹ @@ -329,7 +315,7 @@ (a (f y)) ⁻¹ ∎ φ-surjective : Surjective φe - φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = is-inverse } + φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} } ; right-inverse-of = ? } record FundamentalHomomorphism (G H : Group c c ) (f : Group.Carrier G → Group.Carrier H )