From 29216d26cb509f07666af55901f82c13d7faab20 Mon Sep 17 00:00:00 2001 From: Patrick Stevens Date: Sun, 23 Feb 2020 12:12:53 +0000 Subject: [PATCH] Met and Top lecture 1 (#99) --- Everything/Safe.agda | 7 + Graphs/Bipartite.agda | 13 ++ Graphs/Complement.agda | 21 +++ Graphs/InducedSubgraph.agda | 18 ++ Groups/Homomorphisms/Lemmas2.agda | 52 ++++++ LectureNotes/MetAndTop/Chapter1.agda | 241 +++++++++++++++++++++++++++ LectureNotes/MetAndTop/Chapter2.agda | 29 ++++ Lists/Lists.agda | 31 ++++ Rings/Homomorphisms/Lemmas.agda | 63 +++++++ 9 files changed, 475 insertions(+) create mode 100644 Graphs/Bipartite.agda create mode 100644 Graphs/Complement.agda create mode 100644 Graphs/InducedSubgraph.agda create mode 100644 Groups/Homomorphisms/Lemmas2.agda create mode 100644 LectureNotes/MetAndTop/Chapter1.agda create mode 100644 LectureNotes/MetAndTop/Chapter2.agda create mode 100644 Rings/Homomorphisms/Lemmas.agda diff --git a/Everything/Safe.agda b/Everything/Safe.agda index 3de1cae..4e75650 100644 --- a/Everything/Safe.agda +++ b/Everything/Safe.agda @@ -26,6 +26,7 @@ open import Groups.QuotientGroup.Definition open import Groups.QuotientGroup.Lemmas open import Groups.FiniteGroups.Definition open import Groups.Homomorphisms.Lemmas +open import Groups.Homomorphisms.Lemmas2 open import Groups.Homomorphisms.Examples open import Groups.Isomorphisms.Lemmas open import Groups.FinitePermutations @@ -83,6 +84,7 @@ open import Rings.Irreducibles.Definition open import Rings.Divisible.Definition open import Rings.Associates.Lemmas open import Rings.InitialRing +open import Rings.Homomorphisms.Lemmas open import Setoids.Setoids open import Setoids.DirectSum @@ -138,5 +140,10 @@ open import Graphs.CycleGraph open import Graphs.UnionGraph open import Graphs.CompleteGraph open import Graphs.Colouring +open import Graphs.Bipartite +open import Graphs.Complement +open import Graphs.InducedSubgraph + +open import LectureNotes.MetAndTop.Chapter1 module Everything.Safe where diff --git a/Graphs/Bipartite.agda b/Graphs/Bipartite.agda new file mode 100644 index 0000000..fcf2496 --- /dev/null +++ b/Graphs/Bipartite.agda @@ -0,0 +1,13 @@ +{-# OPTIONS --warning=error --safe --without-K #-} + +open import LogicalFormulae +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) +open import Functions +open import Setoids.Setoids +open import Setoids.Subset +open import Graphs.Definition + +module Graphs.Bipartite where + +Bipartite : {a b : _} {c : _} {V' : Set a} {V : Setoid {a} {b} V'} (G : Graph c V) → Set _ +Bipartite {V' = V'} {V = V} G = Sg (V' → Set) (λ partition → ((x y : V') → (Setoid._∼_ V x y) → partition x → partition y) & ((x : V') → (partition x) || ((partition x) → False)) & ((x y : V') → (Graph._<->_ G x y) → (partition x) → ((partition y) → False))) diff --git a/Graphs/Complement.agda b/Graphs/Complement.agda new file mode 100644 index 0000000..a3112a1 --- /dev/null +++ b/Graphs/Complement.agda @@ -0,0 +1,21 @@ +{-# OPTIONS --warning=error --safe --without-K #-} + +open import LogicalFormulae +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) +open import Functions +open import Setoids.Setoids +open import Setoids.Subset +open import Graphs.Definition +open import Sets.EquivalenceRelations + +module Graphs.Complement {a b c : _} {V' : Set a} {V : Setoid {a} {b} V'} (G : Graph c V) where + +open Graph G +open Setoid V +open Equivalence eq + +complement : Graph (b ⊔ c) V +Graph._<->_ complement x y = ((x <-> y) → False) && ((x ∼ y) → False) +Graph.noSelfRelation complement x (pr1 ,, pr2) = pr2 reflexive +Graph.symmetric complement (x!-y ,, x!=y) = (λ pr → x!-y (Graph.symmetric G pr)) ,, λ pr → x!=y (Equivalence.symmetric eq pr) +Graph.wellDefined complement x=y r=s (x!-r ,, x!=r) = (λ y-s → x!-r (wellDefined (Equivalence.symmetric eq x=y) (Equivalence.symmetric eq r=s) y-s)) ,, λ y=s → x!=r (transitive x=y (transitive y=s (Equivalence.symmetric eq r=s))) diff --git a/Graphs/InducedSubgraph.agda b/Graphs/InducedSubgraph.agda new file mode 100644 index 0000000..44df677 --- /dev/null +++ b/Graphs/InducedSubgraph.agda @@ -0,0 +1,18 @@ +{-# OPTIONS --warning=error --safe --without-K #-} + +open import LogicalFormulae +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) +open import Functions +open import Setoids.Setoids +open import Setoids.Subset +open import Graphs.Definition + +module Graphs.InducedSubgraph {a b c : _} {V' : Set a} {V : Setoid {a} {b} V'} (G : Graph c V) where + +open Graph G + +inducedSubgraph : {d : _} {pred : V' → Set d} (sub : subset V pred) → Graph c (subsetSetoid V sub) +Graph._<->_ (inducedSubgraph sub) (x , _) (y , _) = x <-> y +Graph.noSelfRelation (inducedSubgraph sub) (x , _) x=x = noSelfRelation x x=x +Graph.symmetric (inducedSubgraph sub) {x , _} {y , _} x=y = symmetric x=y +Graph.wellDefined (inducedSubgraph sub) {x , _} {y , _} {z , _} {w , _} x=y z=w x-z = wellDefined x=y z=w x-z diff --git a/Groups/Homomorphisms/Lemmas2.agda b/Groups/Homomorphisms/Lemmas2.agda new file mode 100644 index 0000000..eca07ec --- /dev/null +++ b/Groups/Homomorphisms/Lemmas2.agda @@ -0,0 +1,52 @@ +{-# OPTIONS --safe --warning=error --without-K #-} + +open import LogicalFormulae +open import Groups.Groups +open import Groups.Homomorphisms.Definition +open import Groups.Definition +open import Numbers.Naturals.Naturals +open import Setoids.Orders +open import Setoids.Setoids +open import Functions +open import Sets.EquivalenceRelations + +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) + +module Groups.Homomorphisms.Lemmas2 {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ : A → A → A} (G : Group S _+A_) where + +imageGroup : {c d : _} {B : Set c} {T : Setoid {c} {d} B} {_+B_ : B → B → B} → (f : A → B) → SetoidSurjection S T f → ({x y : A} → Setoid._∼_ T (f (x +A y)) ((f x) +B (f y))) → ({x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x +B y) (m +B n)) → Group T _+B_ +Group.+WellDefined (imageGroup f surj respects+ wd) {m} {n} {x} {y} = wd +Group.0G (imageGroup f surj respects+ wd) = f (Group.0G G) +Group.inverse (imageGroup f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) b with surjective {b} +Group.inverse (imageGroup f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) b | a , fa=b = f (Group.inverse G a) +Group.+Associative (imageGroup {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {a} {b} {c} with surjective {a} +... | x , fx=a with surjective {b} +... | y , fy=b with surjective {c} +... | z , fz=c = transitive (wd (symmetric fx=a) (transitive (wd (symmetric fy=b) (symmetric fz=c)) (symmetric respects+))) (transitive (transitive (symmetric respects+) (transitive (wellDefined (Group.+Associative G)) respects+)) (wd (transitive respects+ (wd fx=a fy=b)) fz=c)) + where + open Setoid T + open Equivalence eq +Group.identRight (imageGroup {T = T} f record { wellDefined = wd ; surjective = surjective } respects+ bWd) {b} with surjective {b} +... | a , fa=b = transitive (bWd (symmetric fa=b) reflexive) (transitive (symmetric respects+) (transitive (wd (Group.identRight G)) fa=b)) + where + open Setoid T + open Equivalence eq +Group.identLeft (imageGroup {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {b} with surjective {b} +... | a , fa=b = transitive (wd reflexive (symmetric fa=b)) (transitive (symmetric respects+) (transitive (wellDefined (Group.identLeft G)) fa=b)) + where + open Setoid T + open Equivalence eq +Group.invLeft (imageGroup {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {b} with surjective {b} +Group.invLeft (imageGroup {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {b} | a , fa=b = transitive (wd reflexive (symmetric fa=b)) (transitive (symmetric respects+) (wellDefined (Group.invLeft G))) + where + open Setoid T + open Equivalence eq +Group.invRight (imageGroup f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {b} with surjective {b} +Group.invRight (imageGroup {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ wd) {b} | a , fa=b = transitive (wd (symmetric fa=b) reflexive) (transitive (symmetric respects+) (wellDefined (Group.invRight G))) + where + open Setoid T + open Equivalence eq + +homToImageGroup : {c d : _} {B : Set c} {T : Setoid {c} {d} B} {_+B_ : B → B → B} → (f : A → B) → (surj : SetoidSurjection S T f) → (respects+ : {x y : A} → Setoid._∼_ T (f (x +A y)) ((f x) +B (f y))) → (wd : {x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x +B y) (m +B n)) → GroupHom G (imageGroup f surj respects+ wd) f +GroupHom.groupHom (homToImageGroup f surj respects+ wd) = respects+ +GroupHom.wellDefined (homToImageGroup f surj respects+ wd) = SetoidSurjection.wellDefined surj diff --git a/LectureNotes/MetAndTop/Chapter1.agda b/LectureNotes/MetAndTop/Chapter1.agda new file mode 100644 index 0000000..d047ccb --- /dev/null +++ b/LectureNotes/MetAndTop/Chapter1.agda @@ -0,0 +1,241 @@ +{-# OPTIONS --safe --warning=error --without-K #-} + +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_; Setω) + +open import Setoids.Setoids +open import Setoids.Subset +open import Setoids.Functions.Definition +open import LogicalFormulae +open import Functions +open import Lists.Lists + +module LectureNotes.MetAndTop.Chapter1 where + +PowerSet : {a : _} (A : Set a) → {b : _} → Set (a ⊔ lsuc b) +PowerSet A {b} = A → Set b + +equality : {a b c : _} (A : Set a) → PowerSet A {b} → PowerSet A {c} → Set (a ⊔ b ⊔ c) +equality A x y = (z : A) → (x z → y z) && (y z → x z) + +trans : {a b c d : _} {A : Set a} → {x : PowerSet A {b}} {y : PowerSet A {c}} {z : PowerSet A {d}} → equality A x y → equality A y z → equality A x z +trans {x} {y} {z} x=y y=z i with x=y i +... | r ,, s with y=z i +... | t ,, u = (λ z → t (r z)) ,, λ z → s (r (_&&_.snd (x=y i) (u z))) + +symm : {a b c : _} {A : Set a} → {x : PowerSet A {b}} {y : PowerSet A {c}} → equality A x y → equality A y x +symm x=y i with x=y i +... | r ,, s = s ,, r + +reflex : {a b : _} {A : Set a} → (x : PowerSet A {b}) → equality A x x +reflex x i = (λ z → z) ,, λ z → z + +mapPower : {a b c : _} {A : Set a} {B : Set b} (f : A → B) → PowerSet B {c} → PowerSet A {c} +mapPower f p a = p (f a) + +mapF : {a b c : _} {A : Set a} {B : Set b} (f : A → B) → PowerSet A {c} → PowerSet B {_} +mapF {A = A} f p b = Sg A (λ a → (p a) && (f a ≡ b)) + +singleton : {a b : _} {A : Set a} → (decidableEquality : (x y : A) → (x ≡ y) || ((x ≡ y) → False)) → A → PowerSet A {b} +singleton decidable a n with decidable a n +singleton decidable a n | inl x = True' +singleton decidable a n | inr x = False' + +intersection : {a b c : _} {A : Set a} {B : Set b} (sets : A → PowerSet B {c}) → PowerSet B {a ⊔ c} +intersection {A = A} sets x = (a : A) → (sets a) x + +union : {a b c : _} {A : Set a} {B : Set b} (sets : A → PowerSet B {c}) → PowerSet B {a ⊔ c} +union {A = A} sets x = Sg A λ i → sets i x + +complement : {a b : _} {A : Set a} → (x : PowerSet A {b}) → PowerSet A +complement x t = x t → False + +emptySet : {a b : _} (A : Set a) → PowerSet A {b} +emptySet A x = False' + +decideIt : {a b : _} {A : Set a} → {f : A → Set b} → ((x : A) → (f x) || ((f x) → False)) → A → Set _ +decideIt decide a with decide a +decideIt decide a | inl x = True +decideIt decide a | inr x = False + +fromExtension : {a : _} {A : Set a} → ((x y : A) → (x ≡ y) || ((x ≡ y) → False)) → List A → PowerSet A +fromExtension decideEquality l = decideIt {f = contains l} (containsDecidable decideEquality l) + +private + + data !1234 : Set where + !1 : !1234 + !2 : !1234 + !3 : !1234 + !4 : !1234 + + decidable1234 : (x y : !1234) → (x ≡ y) || ((x ≡ y) → False) + decidable1234 !1 !1 = inl refl + decidable1234 !1 !2 = inr (λ ()) + decidable1234 !1 !3 = inr (λ ()) + decidable1234 !1 !4 = inr (λ ()) + decidable1234 !2 !1 = inr (λ ()) + decidable1234 !2 !2 = inl refl + decidable1234 !2 !3 = inr (λ ()) + decidable1234 !2 !4 = inr (λ ()) + decidable1234 !3 !1 = inr (λ ()) + decidable1234 !3 !2 = inr (λ ()) + decidable1234 !3 !3 = inl refl + decidable1234 !3 !4 = inr (λ ()) + decidable1234 !4 !1 = inr (λ ()) + decidable1234 !4 !2 = inr (λ ()) + decidable1234 !4 !3 = inr (λ ()) + decidable1234 !4 !4 = inl refl + + f : !1234 → !1234 + f !1 = !1 + f !2 = !1 + f !3 = !4 + f !4 = !3 + + exercise1'1i1 : {b : _} → equality {b = b} !1234 (mapPower f (singleton decidable1234 !1)) (fromExtension decidable1234 (!1 :: !2 :: [])) + exercise1'1i1 !1 = (λ x → record {}) ,, (λ x → record {}) + exercise1'1i1 !2 = (λ x → record {}) ,, (λ x → record {}) + exercise1'1i1 !3 = (λ ()) ,, (λ ()) + exercise1'1i1 !4 = (λ ()) ,, λ () + + exercise1'1i2 : {b : _} → equality {b = b} !1234 (mapPower f (singleton decidable1234 !2)) (λ _ → False) + exercise1'1i2 !1 = (λ ()) ,, λ () + exercise1'1i2 !2 = (λ ()) ,, (λ ()) + exercise1'1i2 !3 = (λ ()) ,, (λ ()) + exercise1'1i2 !4 = (λ ()) ,, (λ ()) + + exercise1'1i3 : equality !1234 (mapPower f (fromExtension decidable1234 (!3 :: !4 :: []))) (fromExtension decidable1234 (!3 :: !4 :: [])) + exercise1'1i3 !1 = (λ x → x) ,, (λ x → x) + exercise1'1i3 !2 = (λ x → x) ,, (λ x → x) + exercise1'1i3 !3 = (λ x → record {}) ,, (λ x → record {}) + exercise1'1i3 !4 = (λ x → record {}) ,, (λ x → record {}) + + exercise1'1ii1 : {a b c t : _} {A : Set a} {B : Set b} {T : Set t} → (f : A → B) → (sets : T → PowerSet B {c}) → equality A (mapPower f (union sets)) (union λ x → mapPower f (sets x)) + exercise1'1ii1 f sets i = (λ x → x) ,, (λ x → x) + + exercise1'1ii2 : {a b c t : _} {A : Set a} {B : Set b} {T : Set t} → (f : A → B) → (sets : T → PowerSet B {c}) → equality A (mapPower f (intersection sets)) (intersection λ x → mapPower f (sets x)) + exercise1'1ii2 f sets i = (λ x → x) ,, (λ x → x) + + exercise1'1ii3 : {a b : _} {A : Set a} {B : Set b} → (f : A → B) → equality A (mapPower f (λ i → True)) (λ i → True) + exercise1'1ii3 f = λ z → (λ x → record {}) ,, (λ x → record {}) + + exercise1'1ii4 : {a b c : _} {A : Set a} {B : Set b} → (f : A → B) → equality A (mapPower f (emptySet {b = c} B)) (emptySet A) + exercise1'1ii4 f = λ z → (λ x → x) ,, (λ x → x) + + exercise1'1ii5 : {a b c : _} {A : Set a} {B : Set b} → (f : A → B) → (u : PowerSet B {c}) → equality A (mapPower f (complement u)) (complement (mapPower f u)) + exercise1'1ii5 f u z = (λ x → x) ,, (λ x → x) + + exercise1'1iii1 : {a b c t : _} {A : Set a} {B : Set b} {T : Set t} → (f : A → B) (sets : T → PowerSet A {c}) → equality B (mapF f (union sets)) (union λ t → mapF f (sets t)) + exercise1'1iii1 {A = A} {T = T} f sets z = x ,, y + where + x : mapF f (union sets) z → union (λ t → mapF f (sets t)) z + x (a , ((t , isIn) ,, snd)) = t , (a , (isIn ,, snd)) + y : union (λ t → mapF f (sets t)) z → mapF f (union sets) z + y (t , (r , s)) = r , ((t , _&&_.fst s) ,, _&&_.snd s) + + exercise1'1iii2 : {a b c d : _} {A : Set a} {B : Set b} → (f : A → B) → equality B (mapF f (emptySet {b = c} A)) (emptySet {b = d} B) + exercise1'1iii2 {A = A} {B = B} f z = x ,, λ () + where + x : mapF f (emptySet A) z → emptySet B z + x (a , ()) + + ex4F : !1234 → !1234 + ex4F !1 = !1 + ex4F !2 = !2 + ex4F !3 = !1 + ex4F !4 = !4 + + v1 : PowerSet !1234 + v1 !1 = True + v1 !2 = True + v1 !3 = False + v1 !4 = False + v2 : PowerSet !1234 + v2 !1 = False + v2 !2 = True + v2 !3 = True + v2 !4 = False + + v1AndV2 : Bool → !1234 → Set + v1AndV2 BoolTrue = v1 + v1AndV2 BoolFalse = v2 + + lhs : equality {c = lzero} !1234 (mapF ex4F (intersection v1AndV2)) (singleton decidable1234 !2) + lhs !1 = ans ,, λ () + where + ans : mapF ex4F (intersection v1AndV2) !1 → False' + ans (!1 , (fst ,, refl)) with fst BoolFalse + ans (!1 , (fst ,, refl)) | () + ans (!3 , (fst ,, refl)) with fst BoolTrue + ans (!3 , (fst ,, refl)) | () + lhs !2 = (λ _ → record {}) ,, ans + where + u : intersection v1AndV2 !2 + u BoolTrue = record {} + u BoolFalse = record {} + ans : singleton decidable1234 !2 !2 → mapF ex4F (intersection v1AndV2) !2 + ans _ = !2 , (u ,, refl) + lhs !3 = ans ,, λ () + where + ans : mapF ex4F (intersection v1AndV2) !3 → False' + ans (!3 , (fst ,, ())) + lhs !4 = ans ,, λ () + where + ans : mapF ex4F (intersection v1AndV2) !4 → False' + ans (!4 , (fst ,, refl)) with fst BoolTrue + ans (!4 , (fst ,, refl)) | () + + fv1AndV2 : Bool → !1234 → Set + fv1AndV2 BoolTrue = mapF ex4F v1 + fv1AndV2 BoolFalse = mapF ex4F v2 + + rhs : equality {c = lzero} !1234 (intersection fv1AndV2) (fromExtension decidable1234 (!2 :: !1 :: [])) + rhs !1 = (λ _ → record {}) ,, λ _ → a + where + a : intersection fv1AndV2 !1 + a BoolTrue = !1 , (record {} ,, refl) + a BoolFalse = !3 , (record {} ,, refl) + rhs !2 = (λ _ → record {}) ,, λ _ → a + where + a : intersection fv1AndV2 !2 + a BoolTrue = !2 , (record {} ,, refl) + a BoolFalse = !2 , (record {} ,, refl) + rhs !3 = a ,, λ () + where + a : intersection fv1AndV2 !3 → fromExtension decidable1234 (!2 :: !1 :: []) !4 + a pr with pr BoolTrue + a pr | !1 , (fst ,, ()) + a pr | !2 , (fst ,, ()) + a pr | !3 , (fst ,, snd) = fst + a pr | !4 , (fst ,, snd) = fst + rhs !4 = a ,, λ () + where + a : intersection fv1AndV2 !4 → fromExtension decidable1234 (!2 :: !1 :: []) !4 + a pr with pr BoolTrue + a pr | !1 , (x ,, ()) + a pr | !2 , (x ,, ()) + a pr | !3 , (x ,, ()) + a pr | !4 , (x ,, _) = x + + exercise1'1iv1 : (equality !1234 (mapF ex4F (intersection v1AndV2)) (intersection fv1AndV2)) → False + exercise1'1iv1 pr = ohno + where + bad : equality !1234 (fromExtension decidable1234 (!2 :: !1 :: [])) (singleton decidable1234 !2) + bad = trans (symm rhs) (trans (symm pr) lhs) + ohno : False + ohno with bad !1 + ohno | fst ,, snd with fst record {} + ... | () + + exercise1'1iv2 : (equality !1234 (mapF ex4F (λ _ → True)) (λ _ → True)) → False + exercise1'1iv2 pr with pr !3 + exercise1'1iv2 pr | fst ,, snd with snd _ + exercise1'1iv2 pr | fst ,, snd | !1 , () + exercise1'1iv2 pr | fst ,, snd | !2 , () + exercise1'1iv2 pr | fst ,, snd | !3 , () + exercise1'1iv2 pr | fst ,, snd | !4 , () + + exercise1'1iv3 : equality !1234 (mapF ex4F (complement v1)) (complement v1) → False + exercise1'1iv3 pr with pr !1 + exercise1'1iv3 pr | fst ,, snd with fst (!3 , ((λ i → i) ,, refl)) (record {}) + ... | () diff --git a/LectureNotes/MetAndTop/Chapter2.agda b/LectureNotes/MetAndTop/Chapter2.agda new file mode 100644 index 0000000..3c5d665 --- /dev/null +++ b/LectureNotes/MetAndTop/Chapter2.agda @@ -0,0 +1,29 @@ +{-# OPTIONS --safe --warning=error --without-K #-} + +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_; Setω) + +open import Setoids.Setoids +open import Setoids.Subset +open import Setoids.Functions.Definition +open import LogicalFormulae +open import Functions +open import Lists.Lists +open import Setoids.Orders +open import Rings.Orders.Partial.Definition +open import Rings.Definition + +module LectureNotes.MetAndTop.Chapter2 {a b c : _} {R : Set a} {S : Setoid {a} {b} R} {_<_ : Rel {a} {c} R} {_+_ _*_ : R → R → R} {ring : Ring S _+_ _*_} {ps : SetoidPartialOrder S _<_} (pRing : PartiallyOrderedRing ring ps) where + +open Setoid S renaming (_∼_ to _∼R_) +open Ring ring + +record Metric {d1 e : _} {A : Set d1} {T : Setoid {d1} {e} A} (d : A → A → R) : Set (a ⊔ b ⊔ c ⊔ d1 ⊔ e) where + open Setoid T + field + dWellDefined : (x y v w : A) → x ∼ y → v ∼ w → (d x v) ∼R (d w y) + dZero : (x y : A) → (d x y) ∼R 0R → x ∼ y + dZero' : (x y : A) → x ∼ y → (d x y) ∼R 0R + dSymmetric : (x y : A) → (d x y) ∼R (d y x) + dTriangle : (x y z : A) → ((d x z) < ((d x y) + (d y z))) || ((d x z) ∼R ((d x y) + (d y z))) + dNonnegative : (x y : A) → (0R < d x y) || (0R ∼R (d x y)) + dNonnegative x y = {!!} diff --git a/Lists/Lists.agda b/Lists/Lists.agda index eb0e9fd..13bb81b 100644 --- a/Lists/Lists.agda +++ b/Lists/Lists.agda @@ -46,3 +46,34 @@ contains (x :: l) needle = (x ≡ needle) || contains l needle containsMap : {a b : _} {A : Set a} {B : Set b} (f : A → B) (l : List A) (needle : A) → (contains l needle) → contains (map f l) (f needle) containsMap f (x :: l) needle (inl cont) = inl (applyEquality f cont) containsMap f (x :: l) needle (inr cont) = inr (containsMap f l needle cont) + +containsAppend : {a : _} {A : Set a} (l1 l2 : List A) (needle : A) → (contains (l1 ++ l2) needle) → (contains l1 needle) || (contains l2 needle) +containsAppend [] l2 needle cont = inr cont +containsAppend (x :: l1) l2 needle (inl pr) = inl (inl pr) +containsAppend (x :: l1) l2 needle (inr pr) with containsAppend l1 l2 needle pr +containsAppend (x :: l1) l2 needle (inr pr) | inl ans = inl (inr ans) +containsAppend (x :: l1) l2 needle (inr pr) | inr ans = inr ans + +containsAppend' : {a : _} {A : Set a} (l1 l2 : List A) (needle : A) → (contains l1 needle) || (contains l2 needle) → contains (l1 ++ l2) needle +containsAppend' (x :: l1) l2 needle (inl (inl pr)) = inl pr +containsAppend' (x :: l1) l2 needle (inl (inr pr)) = inr (containsAppend' l1 l2 needle (inl pr)) +containsAppend' [] l2 needle (inr pr) = pr +containsAppend' (x :: l1) l2 needle (inr pr) = inr (containsAppend' l1 l2 needle (inr pr)) + +containsCons : {a : _} {A : Set a} (x : A) (l : List A) (needle : A) → (contains (x :: l) needle) → (x ≡ needle) || (contains l needle) +containsCons x l needle pr = pr + +containsCons' : {a : _} {A : Set a} (x : A) (l : List A) (needle : A) → (x ≡ needle) || (contains l needle) → (contains (x :: l) needle) +containsCons' x l needle pr = pr + +containsDecidable : {a : _} {A : Set a} (decidableEquality : (x y : A) → (x ≡ y) || ((x ≡ y) → False)) → (l : List A) → (needle : A) → (contains l needle) || ((contains l needle) → False) +containsDecidable decide [] needle = inr λ () +containsDecidable decide (x :: l) needle with decide x needle +containsDecidable decide (x :: l) .x | inl refl = inl (inl refl) +containsDecidable decide (x :: l) needle | inr x!=n with containsDecidable decide l needle +containsDecidable decide (x :: l) needle | inr x!=n | inl isIn = inl (inr isIn) +containsDecidable decide (x :: l) needle | inr x!=n | inr notIn = inr t + where + t : ((x ≡ needle) || contains l needle) → False + t (inl x) = x!=n x + t (inr x) = notIn x diff --git a/Rings/Homomorphisms/Lemmas.agda b/Rings/Homomorphisms/Lemmas.agda new file mode 100644 index 0000000..9a77e59 --- /dev/null +++ b/Rings/Homomorphisms/Lemmas.agda @@ -0,0 +1,63 @@ +{-# OPTIONS --safe --warning=error --without-K #-} + +open import LogicalFormulae +open import Groups.Groups +open import Groups.Homomorphisms.Definition +open import Groups.Definition +open import Numbers.Naturals.Naturals +open import Setoids.Orders +open import Setoids.Setoids +open import Functions +open import Sets.EquivalenceRelations +open import Rings.Definition +open import Rings.Homomorphisms.Definition + +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) + +module Rings.Homomorphisms.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ _*A_ : A → A → A} (R : Ring S _+A_ _*A_) where + +open import Groups.Homomorphisms.Lemmas2 (Ring.additiveGroup R) + +imageRing : {c d : _} {B : Set c} {T : Setoid {c} {d} B} {_+B_ : B → B → B} {_*B_ : B → B → B} → (f : A → B) → SetoidSurjection S T f → ({x y : A} → Setoid._∼_ T (f (x +A y)) ((f x) +B (f y))) → ({x y : A} → Setoid._∼_ T (f (x *A y)) ((f x) *B (f y))) → ({x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x +B y) (m +B n)) → ({x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x *B y) (m *B n)) → Ring T _+B_ _*B_ +Ring.additiveGroup (imageRing f surj respects+ respects* +wd *wd) = imageGroup f surj respects+ +wd +Ring.*WellDefined (imageRing f surj respects+ respects* +wd *wd) = *wd +Ring.1R (imageRing f surj respects+ respects* +wd *wd) = f (Ring.1R R) +Ring.groupIsAbelian (imageRing {T = T} f record { surjective = surjective ; wellDefined = wellDefined } respects+ respects* +wd *wd) {a} {b} with surjective {a} +... | x , fx=a with surjective {b} +... | y , fy=b = transitive (+wd (symmetric fx=a) (symmetric fy=b)) (transitive (transitive (symmetric respects+) (transitive (wellDefined (Ring.groupIsAbelian R)) respects+)) (+wd fy=b fx=a)) + where + open Setoid T + open Equivalence eq +Ring.*Associative (imageRing {T = T} f record { surjective = surjective ; wellDefined = wellDefined } respects+ respects* +wd *wd) {a} {b} {c} with surjective {a} +... | x , fx=a with surjective {b} +... | y , fy=b with surjective {c} +... | z , fz=c = transitive (*wd (symmetric fx=a) (transitive (*wd (symmetric fy=b) (symmetric fz=c)) (symmetric respects*))) (transitive (transitive (symmetric respects*) (transitive (wellDefined (Ring.*Associative R)) respects*)) (*wd (transitive respects* (*wd fx=a fy=b)) fz=c)) + where + open Setoid T + open Equivalence eq +Ring.*Commutative (imageRing {T = T} f record { surjective = surjective ; wellDefined = wellDefined } respects+ respects* +wd *wd) {a} {b} with surjective {a} +... | x , fx=a with surjective {b} +... | y , fy=b = transitive (*wd (symmetric fx=a) (symmetric fy=b)) (transitive (transitive (symmetric respects*) (transitive (wellDefined (Ring.*Commutative R)) respects*)) (*wd fy=b fx=a)) + where + open Setoid T + open Equivalence eq +Ring.*DistributesOver+ (imageRing {T = T} f record { surjective = surjective ; wellDefined = wellDefined } respects+ respects* +wd *wd) {a} {b} {c} with surjective {a} +... | x , fx=a with surjective {b} +... | y , fy=b with surjective {c} +... | z , fz=c = transitive (*wd (symmetric fx=a) (+wd (symmetric fy=b) (symmetric fz=c))) (transitive (transitive (transitive (*wd reflexive (symmetric respects+)) (symmetric respects*)) (transitive (transitive (wellDefined (Ring.*DistributesOver+ R)) respects+) (+wd respects* respects*))) (+wd (*wd fx=a fy=b) (*wd fx=a fz=c))) + where + open Setoid T + open Equivalence eq +Ring.identIsIdent (imageRing {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ respects* +wd *wd) {b} with surjective {b} +Ring.identIsIdent (imageRing {T = T} f record { wellDefined = wellDefined ; surjective = surjective } respects+ respects* +wd *wd) {b} | a , fa=b = transitive (transitive (*wd reflexive (symmetric fa=b)) (transitive (symmetric respects*) (wellDefined (Ring.identIsIdent R)))) fa=b + where + open Setoid T + open Equivalence eq + +homToImageRing : {c d : _} {B : Set c} {T : Setoid {c} {d} B} {_+B_ : B → B → B} {_*B_ : B → B → B} → (f : A → B) → (surj : SetoidSurjection S T f) → (respects+ : {x y : A} → Setoid._∼_ T (f (x +A y)) ((f x) +B (f y))) → (respects* : {x y : A} → Setoid._∼_ T (f (x *A y)) ((f x) *B (f y))) → (+wd : {x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x +B y) (m +B n)) → (*wd : {x y m n : B} → Setoid._∼_ T x m → Setoid._∼_ T y n → Setoid._∼_ T (x *B y) (m *B n)) → RingHom R (imageRing f surj respects+ respects* +wd *wd) f +RingHom.preserves1 (homToImageRing {T = T} f surj respects+ respects* +wd *wd) = reflexive + where + open Setoid T + open Equivalence eq +RingHom.ringHom (homToImageRing f surj respects+ respects* +wd *wd) = respects* +RingHom.groupHom (homToImageRing f surj respects+ respects* +wd *wd) = homToImageGroup f surj respects+ +wd