Mercurial > hg > Members > kono > Proof > galois
changeset 310:b4a3ed9301cb
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 15 Sep 2023 21:12:52 +0900 |
| parents | 4dd130b93b21 |
| children | 423efbcf6a09 |
| files | src/Homomorphism.agda |
| diffstat | 1 files changed, 42 insertions(+), 42 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Homomorphism.agda Thu Sep 14 13:03:17 2023 +0900 +++ b/src/Homomorphism.agda Fri Sep 15 21:12:52 2023 +0900 @@ -224,48 +224,6 @@ ε ∙ ε ≈⟨ proj₁ identity _ ⟩ ε ∎ -record IsImage {c d : Level} (G : Group c d) (H : Group c d) - {f : Group.Carrier G → Group.Carrier H } - (f-homo : IsGroupHomomorphism (GR G) (GR H) f ) (x : Group.Carrier H) : Set (c Level.⊔ d) where - field - gelm : Group.Carrier G - x=fg : H < x ≈ f gelm > - - -Im : {c d : Level} (G : Group c d) {H : Group c d} - {f : Group.Carrier G → Group.Carrier H } - (f-homo : IsGroupHomomorphism (GR G) (GR H) f ) → SubGroup {c Level.⊔ d} H -Im G {H} {f} f-homo = record { - P = λ x → IsImage G H f-homo x - ; Pε = record { gelm = Group.ε G ; x=fg = gsym ε-homo } - ; P⁻¹ = λ x imx → record { gelm = Group._⁻¹ G (gelm imx) ; x=fg = im00 (x=fg imx) } - ; P≈ = im01 - ; P∙ = im02 } where - open IsImage - open Group H - open Gutil H - open IsGroupHomomorphism f-homo - open EqReasoning (Algebra.Group.setoid H) - GC = Group.Carrier G - im00 : {x : Carrier } {y : GC } → x ≈ f y → x ⁻¹ ≈ f ((G Group.⁻¹) y ) - im00 {x} {y} x=fy = begin - x ⁻¹ ≈⟨ ⁻¹-cong x=fy ⟩ - (f y) ⁻¹ ≈⟨ gsym ( ⁻¹-homo _) ⟩ - f ((G Group.⁻¹) y ) ∎ - im01 : {a b : Carrier} → a ≈ b → IsImage G H f-homo a → IsImage G H f-homo b - im01 {a} {b} a=b ima = record { gelm = _ ; x=fg = gtrans (gsym a=b) (x=fg ima) } - im02 : {a b : Carrier} → - IsImage G H f-homo a → - IsImage G H f-homo b → IsImage G H f-homo (a ∙ b) - im02 {a} {b} isa isb = record { gelm = G < gelm isa ∙ gelm isb > ; x=fg = im03 } where - im03 : a ∙ b ≈ f (G < gelm isa ∙ gelm isb > ) - im03 = begin - a ∙ b ≈⟨ ∙-cong (x=fg isa) (x=fg isb) ⟩ - f (gelm isa ) ∙ f (gelm isb ) ≈⟨ gsym (homo _ _ ) ⟩ - f (G < gelm isa ∙ gelm isb > ) ∎ - - - module GK {c d : Level} (G : Group c d) (K : NormalSubGroup G ) where φ : Group.Carrier G → Group.Carrier (G / K ) -- a → aN @@ -338,6 +296,48 @@ -- Another from of Fundamental Homomorphism Theorm -- i.e. G / Ker f ≈ Im f +record IsImage {c d : Level} (G : Group c d) (H : Group c d) + {f : Group.Carrier G → Group.Carrier H } + (f-homo : IsGroupHomomorphism (GR G) (GR H) f ) (x : Group.Carrier H) : Set (c Level.⊔ d) where + field + gelm : Group.Carrier G + x=fg : H < x ≈ f gelm > + + +Im : {c d : Level} (G : Group c d) {H : Group c d} + {f : Group.Carrier G → Group.Carrier H } + (f-homo : IsGroupHomomorphism (GR G) (GR H) f ) → SubGroup {c Level.⊔ d} H +Im G {H} {f} f-homo = record { + P = λ x → IsImage G H f-homo x + ; Pε = record { gelm = Group.ε G ; x=fg = gsym ε-homo } + ; P⁻¹ = λ x imx → record { gelm = Group._⁻¹ G (gelm imx) ; x=fg = im00 (x=fg imx) } + ; P≈ = im01 + ; P∙ = im02 } where + open IsImage + open Group H + open Gutil H + open IsGroupHomomorphism f-homo + open EqReasoning (Algebra.Group.setoid H) + GC = Group.Carrier G + im00 : {x : Carrier } {y : GC } → x ≈ f y → x ⁻¹ ≈ f ((G Group.⁻¹) y ) + im00 {x} {y} x=fy = begin + x ⁻¹ ≈⟨ ⁻¹-cong x=fy ⟩ + (f y) ⁻¹ ≈⟨ gsym ( ⁻¹-homo _) ⟩ + f ((G Group.⁻¹) y ) ∎ + im01 : {a b : Carrier} → a ≈ b → IsImage G H f-homo a → IsImage G H f-homo b + im01 {a} {b} a=b ima = record { gelm = _ ; x=fg = gtrans (gsym a=b) (x=fg ima) } + im02 : {a b : Carrier} → + IsImage G H f-homo a → + IsImage G H f-homo b → IsImage G H f-homo (a ∙ b) + im02 {a} {b} isa isb = record { gelm = G < gelm isa ∙ gelm isb > ; x=fg = im03 } where + im03 : a ∙ b ≈ f (G < gelm isa ∙ gelm isb > ) + im03 = begin + a ∙ b ≈⟨ ∙-cong (x=fg isa) (x=fg isb) ⟩ + f (gelm isa ) ∙ f (gelm isb ) ≈⟨ gsym (homo _ _ ) ⟩ + f (G < gelm isa ∙ gelm isb > ) ∎ + + + im : {c d : Level} (G : Group c d) {H : Group c d} {f : Group.Carrier G → Group.Carrier H } → (f-homo : IsGroupHomomorphism (GR G) (GR H) f ) → (x : Group.Carrier G)