X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fr-o-basic_pairs.ma;h=310ef55ebf53f23dbd552cda169685204ec5b17b;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=92e9e975d79682b1f39dc3d3d96233a755ab7f25;hpb=21cb6b92e615f08280e9f032718593b4a6a1d3a5;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
index 92e9e975d..310ef55eb 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
@@ -15,42 +15,159 @@
 include "basic_pairs_to_o-basic_pairs.ma".
 include "apply_functor.ma".
 
-definition rOBP ≝ Apply ?? BP_to_OBP.
+definition rOBP ≝ Apply (category2_of_category1 BP) OBP BP_to_OBP.
 
 include "o-basic_pairs_to_o-basic_topologies.ma".
 
+lemma category2_of_category1_respects_comp_r:
+ ∀C:category1.∀o1,o2,o3:C.
+  ∀f:arrows1 ? o1 o2.∀g:arrows1 ? o2 o3.
+   (comp1 ???? f g) =_\ID (comp2 (category2_of_category1 C) o1 o2 o3 f g).
+ intros; constructor 1; 
+qed.
+
+lemma category2_of_category1_respects_comp:
+ ∀C:category1.∀o1,o2,o3:C.
+  ∀f:arrows1 ? o1 o2.∀g:arrows1 ? o2 o3.
+   (comp2 (category2_of_category1 C) o1 o2 o3 f g) =_\ID (comp1 ???? f g).
+ intros; constructor 1; 
+qed.
+
+lemma POW_full': 
+  ∀S,T:REL.∀f:arrows2 SET1 (POW S) (POW T).
+   arrows1 REL S T.
+ intros;
+ constructor 1; constructor 1;
+  [ intros (x y); apply (y ∈ c {(x)});
+  | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
+    apply (e1ࠠe); ]
+qed.
+
+(*
+lemma POW_full_image: 
+  ∀S,T:REL.∀f:arrows2 SET1 (POW S) (POW T).
+   exT22 ? (λg:arrows1 REL S T.or_f ?? (map_arrows2 ?? POW S T g) = f).
+ intros; letin g ≝ (? : carr1 (arrows1 REL S T)); [
+ constructor 1; constructor 1;
+  [ intros (x y); apply (y ∈ f {(x)});
+  | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
+    apply (e1ࠠe); ]]
+exists [apply g]
+intro; split; intro; simplify; intro; 
+[ whd in f1; change in f1:(? ? (λ_:?.? ? ? ? ? % ?)) with (a1 ∈ f {(x)});
+  cases f1; cases x; clear f1 x; change with (a1 ∈ f a);
+  lapply (f_image_monotone ?? (map_arrows2 ?? POW S T g) (singleton ? w) a ? a1);
+  [2: whd in Hletin;
+      change in Hletin:(? ? (λ_:?.? ? ? ? ? % ?))
+      with (a1 ∈ f {(x)}); cases Hletin; cases x;
+           [ intros 2; change in f3 with (eq1 ? w a2); change with (a2 ∈ a);
+             apply (. f3^-1‡#); assumption;
+           | assumption; ]
+           
+           
+           
+  lapply (. (or_prop3 ?? (map_arrows2 ?? POW S T g) (singleton ? a1) a)^-1);
+   [ whd in Hletin:(? ? ? ? ? ? %);
+     change in Hletin:(? ? ? ? ? ? (? ? (? ? ? (λ_:?.? ? (λ_:?.? ? ? ? ? % ?)) ?)))
+     with (y ∈ f {(x)});
+     cases Hletin; cases x1; cases x2; 
+  
+   [ cases Hletin; change in x with (eq1 ? a1 w1); apply (. x‡#); assumption;
+   | exists; [apply w] assumption ]
+
+
+  clear g;
+ cases f1; cases x; simplify in f2; change with (a1 ∈ (f a));
+  lapply depth=0 (let x ≝ POW in or_prop3 (POW S) (POW T) (map_arrows2 ?? POW S T g));
+  lapply (Hletin {(w)} {(a1)}).
+  lapply (if ?? Hletin1); [2: clear Hletin Hletin1;
+    exists; [apply a1] [whd; exists[apply w] split; [assumption;|change with (w = w); apply rule #]]
+    change with (a1=a1); apply rule #;]
+  clear Hletin Hletin1; cases Hletin2; whd in x2; 
+qed.
+*)
+lemma curry: ∀A,B,C.binary_morphism1 A B C → A → B ⇒ C.
+ intros;
+ constructor 1;
+  [ apply (b c);
+  | intros; apply (#‡e); ]
+qed.
+
+notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
+interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
+
+definition preserve_sup : ∀S,T.∀ f:Ω \sup S ⇒ Ω \sup T. CProp1.
+intros (S T f); apply (∀X:Ω \sup S. (f X) = ?);
+constructor 1; constructor 1;
+[ intro y; alias symbol "singl" = "singleton". alias symbol "and" = "and_morphism".
+  apply (∃x:S. x ∈ X ∧ y ∈ f {(x)});
+| intros (a b H); split; intro E; cases E; clear E; exists; [1,3:apply w]
+  [ apply (. #‡(H^-1‡#)); | apply (. #‡(H‡#));] assumption]
+qed.
+
+alias symbol "singl" = "singleton".
+lemma eq_cones_to_eq_rel: 
+  ∀S,T. ∀f,g: arrows1 REL S T.
+   (∀x. curry ??? (image ??) f {(x)} = curry ??? (image ??) g {(x)}) → f = g.
+intros; intros 2 (a b); split; intro;
+[ cases (f1 a); lapply depth=0 (s b); clear s s1;
+  lapply (Hletin); clear Hletin;
+   [ cases Hletin1; cases x; change in f4 with (a = w);
+     change with (a ♮g b); apply (. f4‡#); assumption;
+   | exists; [apply a] split; [ assumption | change with (a=a); apply rule #;]]
+| cases (f1 a); lapply depth=0 (s1 b); clear s s1;
+  lapply (Hletin); clear Hletin;
+   [ cases Hletin1; cases x; change in f4 with (a = w);
+     change with (a ♮f b); apply (. f4‡#); assumption;
+   | exists; [apply a] split; [ assumption | change with (a=a); apply rule #;]]]
+qed.
+
+variant eq_cones_to_eq_rel': 
+  ∀S,T. ∀f,g: arrows1 REL S T.
+   (∀x:S. or_f ?? (map_arrows2 ?? POW S T f) {(x)} = or_f ?? (map_arrows2 ?? POW S T g) {(x)}) →
+    f = g
+≝ eq_cones_to_eq_rel.
+
 lemma rOR_full : 
   ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
     exT22 ? (λg:arrows2 rOBP s t.
-       map_arrows2 ?? OR ?? (ℳ_2 g) = f).
-intro; cases s (s_2 s_1 s_eq); clear s; cases s_eq; clear s_eq s_2;
-intro; cases t (t_2 t_1 t_eq); clear t; cases t_eq; clear t_eq t_2;
+       map_arrows2 ?? OR ?? (ℳ_2 g) = f). 
+intros 2 (s t); cases s (s_2 s_1 s_eq); clear s;
+change in match (F2 ??? (mk_Fo ??????)) with s_2;
+cases s_eq; clear s_eq s_2;
+letin s1 ≝ (BP_to_OBP s_1); change in match (BP_to_OBP s_1) with s1;
+cases t (t_2 t_1 t_eq); clear t;
+change in match (F2 ??? (mk_Fo ??????)) with t_2;
+cases t_eq; clear t_eq t_2;
+letin t1 ≝ (BP_to_OBP t_1); change in match (BP_to_OBP t_1) with t1;
 whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
-intro; whd in s_1 t_1;
-letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1)));
- [2:
-   exists;
+intro; whd in s_1 t_1; 
+letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1))); 
+[2:
+  exists;
     [ constructor 1;
        [2: simplify; apply R;
        | simplify; apply (fun12 ?? (map_arrows2 ?? BP_to_OBP s_1 t_1)); apply R;
        | simplify; apply rule #; ]]
    simplify;
- | constructor 1;
-    [2: constructor 1; constructor 1;
-      [ intros (x y); apply (y ∈ f (singleton ? x));
-      | intros; unfold FunClass_1_OF_Ocontinuous_relation;
-        unfold in ⊢ (? ? ? (? ? ? ? ? ? %) ?); apply (.= e1‡††e);
-        apply rule #; ]
-    |1: constructor 1; constructor 1;
-      [ intros (x y); apply (y ∈ star_image ?? (⊩ \sub t_1) (f (image ?? (⊩ \sub s_1) (singleton ? x))));
-      | intros; unfold FunClass_1_OF_Ocontinuous_relation;
-        unfold in ⊢ (? ? ? (? ? ? ? ? ? (? ? ? ? ? ? %)) ?);
-        apply (.= e1‡(#‡†(#‡†e))); apply rule #; ]
-    | whd; simplify; intros; split; intros; simplify; whd in f1 ⊢ %; simplify in f1 ⊢ %;
-      cases f1; clear f1; cases x1; clear x1;
-       [
-       | exists;
-       ]
+|1: constructor 1;   
+    [2: apply (pi1exT22 ?? (POW_full (form s_1) (form t_1) f));
+    |1: letin u ≝ (or_f_star ?? (map_arrows2 ?? POW (concr t_1) (form t_1) (⊩ \sub t_1)));
+        letin r ≝ (u ∘ (or_f ?? f));
+        letin xxx ≝ (or_f ?? (map_arrows2 ?? POW (concr s_1) (form s_1) (⊩ \sub s_1)));
+        letin r' ≝ (r ∘ xxx); clearbody r';
+        apply (POW_full' (concr s_1) (concr t_1) r');    
+    | simplify in ⊢ (? ? ? (? ? ? ? ? % ?) ?);
+      apply eq_cones_to_eq_rel'; intro;
+      apply
+       (cic:/matita/logic/equality/eq_elim_r''.con ?????
+         (category2_of_category1_respects_comp_r : ?));
+      apply rule (.= (#‡#));
+      apply (.= (respects_comp2 ?? POW (concr s_1) (concr t_1) (form t_1) ? (⊩\sub t_1))‡#); 
+      apply sym2;
+      apply (.= (respects_comp2 ?? POW (concr s_1) (form s_1) (form t_1) (⊩\sub s_1) (pi1exT22 ?? (POW_full (form s_1) (form t_1) (Ocont_rel ?? f)))));
+      apply (let H ≝(\snd (POW_full (form s_1) (form t_1) (Ocont_rel ?? f))) in .= #‡H);
+      apply sym2;      
  ]
 
 STOP;
@@ -65,8 +182,8 @@ STOP;
 
 3. Definire la funzione
     Apply:
-     \forall C1,C2: CAT2.  F: arrows3 CAT2 C1 C2 -> CAT2
-    :=
+    ∀C1,C2: CAT2.  F: arrows3 CAT2 C1 C2 → CAT2
+    ≝ 
      constructor 1;
       [ gli oggetti sono gli oggetti di C1 mappati da F
       | i morfismi i morfismi di C1 mappati da F
@@ -81,7 +198,7 @@ STOP;
    al punto 5)
 
 4. Definire rOBP (le OBP rappresentabili) come (BP_to_OBP BP)
-  [Si puo' fare lo stesso per le OA: rOA := Rel_to_OA REL ]
+  [Si puo' fare lo stesso per le OA: rOA ≝ Rel_to_OA REL ]
 
 5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
    quando applicato a rOBP.
@@ -93,7 +210,7 @@ STOP;
 6. Definire rOBTop come (OBP_to_OBTop rOBP).
 
 7. Per composizione si ha un funtore full and faithful da BP a rOBTop:
-   basta prendere (OR \circ BP_to_OBP).
+   basta prendere (OR ∘ BP_to_OBP).
 
 8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
    esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'