The first omomorphism theorem for whole sets (i.e. setoids + morphisms, not

sets + morphisms).

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 5ec6f42a8c7f9858f7b6201ac0a4c4228c2f3a75..a7e033c15c43119ecec9380f98fa0769fc2c7236 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -145,3 +145,59 @@ ndefinition image: ∀A,B. (carr A → carr B) → Ω \sup A → Ω \sup B ≝
 ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
  λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}.
 *)
+
+(******************* compatible equivalence relations **********************)
+
+nrecord compatible_equivalence_relation (A: setoid) : Type[1] ≝
+ { rel:> equivalence_relation A;
+   compatibility: ∀x,x':A. x=x' → eq_rel ? rel x x' (* coercion qui non va *)
+ }.
+
+ndefinition quotient: ∀A. compatible_equivalence_relation A → setoid.
+ #A; #R; napply mk_setoid
+  [ napply A
+  | napply R]
+nqed.
+
+(******************* first omomorphism theorem for sets **********************)
+
+ndefinition eqrel_of_morphism:
+ ∀A,B. unary_morphism A B → compatible_equivalence_relation A.
+ #A; #B; #f; napply mk_compatible_equivalence_relation
+  [ napply mk_equivalence_relation
+     [ napply (λx,y. f x = f y)
+     | #x; napply refl | #x; #y; napply sym | #x; #y; #z; napply trans]
+##| #x; #x'; #H; nwhd; napply (.= (†H)); napply refl ]
+nqed.
+
+ndefinition canonical_proj: ∀A,R. unary_morphism A (quotient A R).
+ #A; #R; napply mk_unary_morphism
+  [ napply (λx.x) | #a; #a'; #H; napply (compatibility ? R … H) ]
+nqed.
+
+ndefinition quotiented_mor:
+ ∀A,B.∀f:unary_morphism A B.
+  unary_morphism (quotient ? (eqrel_of_morphism ?? f)) B.
+ #A; #B; #f; napply mk_unary_morphism
+  [ napply f | #a; #a'; #H; nassumption]
+nqed.
+
+nlemma first_omomorphism_theorem_functions1:
+ ∀A,B.∀f: unary_morphism A B.
+  ∀x. f x = quotiented_mor ??? (canonical_proj ? (eqrel_of_morphism ?? f) x).
+ #A; #B; #f; #x; napply refl;
+nqed.
+
+ndefinition surjective ≝ λA,B.λf:unary_morphism A B. ∀y.∃x. f x = y.
+
+ndefinition injective ≝ λA,B.λf:unary_morphism A B. ∀x,x'. f x = f x' → x = x'.
+
+nlemma first_omomorphism_theorem_functions2:
+ ∀A,B.∀f: unary_morphism A B. surjective ?? (canonical_proj ? (eqrel_of_morphism ?? f)).
+ #A; #B; #f; nwhd; #y; napply (ex_intro … y); napply refl.
+nqed.
+
+nlemma first_omomorphism_theorem_functions3:
+ ∀A,B.∀f: unary_morphism A B. injective ?? (quotiented_mor ?? f).
+ #A; #B; #f; nwhd; #x; #x'; #H; nassumption.
+nqed.
\ No newline at end of file