Met and Top lecture 1 (#99)

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

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)))

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)))

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

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

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 {})
+  ... | ()

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 = {!!}

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

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