helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basic_pairs_to_o-basic_pairs.ma".
  16 include "apply_functor.ma".
  17
  18 definition rOBP ≝ Apply (category2_of_category1 BP) OBP BP_to_OBP.
  19
  20 include "o-basic_pairs_to_o-basic_topologies.ma".
  21
  22 lemma category2_of_category1_respects_comp_r:
  23  ∀C:category1.∀o1,o2,o3:C.
  24   ∀f:arrows1 ? o1 o2.∀g:arrows1 ? o2 o3.
  25    (comp1 ???? f g) =_\ID (comp2 (category2_of_category1 C) o1 o2 o3 f g).
  26  intros; constructor 1;
  27 qed.
  28
  29 lemma category2_of_category1_respects_comp:
  30  ∀C:category1.∀o1,o2,o3:C.
  31   ∀f:arrows1 ? o1 o2.∀g:arrows1 ? o2 o3.
  32    (comp2 (category2_of_category1 C) o1 o2 o3 f g) =_\ID (comp1 ???? f g).
  33  intros; constructor 1;
  34 qed.
  35
  36 lemma POW_full':
  37   ∀S,T:REL.∀f:arrows2 SET1 (POW S) (POW T).
  38    arrows1 REL S T.
  39  intros;
  40  constructor 1; constructor 1;
  41   [ intros (x y); apply (y ∈ c {(x)});
  42   | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
  43     apply (e1‡††e); ]
  44 qed.
  45
  46 (*
  47 lemma POW_full_image:
  48   ∀S,T:REL.∀f:arrows2 SET1 (POW S) (POW T).
  49    exT22 ? (λg:arrows1 REL S T.or_f ?? (map_arrows2 ?? POW S T g) = f).
  50  intros; letin g ≝ (? : carr1 (arrows1 REL S T)); [
  51  constructor 1; constructor 1;
  52   [ intros (x y); apply (y ∈ f {(x)});
  53   | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
  54     apply (e1‡††e); ]]
  55 exists [apply g]
  56 intro; split; intro; simplify; intro;
  57 [ whd in f1; change in f1:(? ? (λ_:?.? ? ? ? ? % ?)) with (a1 ∈ f {(x)});
  58   cases f1; cases x; clear f1 x; change with (a1 ∈ f a);
  59   lapply (f_image_monotone ?? (map_arrows2 ?? POW S T g) (singleton ? w) a ? a1);
  60   [2: whd in Hletin;
  61       change in Hletin:(? ? (λ_:?.? ? ? ? ? % ?))
  62       with (a1 ∈ f {(x)}); cases Hletin; cases x;
  63            [ intros 2; change in f3 with (eq1 ? w a2); change with (a2 ∈ a);
  64              apply (. f3^-1‡#); assumption;
  65            | assumption; ]
  66
  67
  68
  69   lapply (. (or_prop3 ?? (map_arrows2 ?? POW S T g) (singleton ? a1) a)^-1);
  70    [ whd in Hletin:(? ? ? ? ? ? %);
  71      change in Hletin:(? ? ? ? ? ? (? ? (? ? ? (λ_:?.? ? (λ_:?.? ? ? ? ? % ?)) ?)))
  72      with (y ∈ f {(x)});
  73      cases Hletin; cases x1; cases x2;
  74
  75    [ cases Hletin; change in x with (eq1 ? a1 w1); apply (. x‡#); assumption;
  76    | exists; [apply w] assumption ]
  77
  78
  79   clear g;
  80  cases f1; cases x; simplify in f2; change with (a1 ∈ (f a));
  81   lapply depth=0 (let x ≝ POW in or_prop3 (POW S) (POW T) (map_arrows2 ?? POW S T g));
  82   lapply (Hletin {(w)} {(a1)}).
  83   lapply (if ?? Hletin1); [2: clear Hletin Hletin1;
  84     exists; [apply a1] [whd; exists[apply w] split; [assumption;|change with (w = w); apply rule #]]
  85     change with (a1=a1); apply rule #;]
  86   clear Hletin Hletin1; cases Hletin2; whd in x2;
  87 qed.
  88 *)
  89 lemma curry: ∀A,B,C.binary_morphism1 A B C → A → B ⇒ C.
  90  intros;
  91  constructor 1;
  92   [ apply (b c);
  93   | intros; apply (#‡e); ]
  94 qed.
  95
  96 notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
  97 interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
  98
  99 definition preserve_sup : ∀S,T.∀ f:Ω \sup S ⇒ Ω \sup T. CProp1.
 100 intros (S T f); apply (∀X:Ω \sup S. (f X) = ?);
 101 constructor 1; constructor 1;
 102 [ intro y; alias symbol "singl" = "singleton". alias symbol "and" = "and_morphism".
 103   apply (∃x:S. x ∈ X ∧ y ∈ f {(x)});
 104 | intros (a b H); split; intro E; cases E; clear E; exists; [1,3:apply w]
 105   [ apply (. #‡(H^-1‡#)); | apply (. #‡(H‡#));] assumption]
 106 qed.
 107
 108 alias symbol "singl" = "singleton".
 109 lemma eq_cones_to_eq_rel:
 110   ∀S,T. ∀f,g: arrows1 REL S T.
 111    (∀x. curry ??? (image ??) f {(x)} = curry ??? (image ??) g {(x)}) → f = g.
 112 intros; intros 2 (a b); split; intro;
 113 [ cases (f1 a); lapply depth=0 (s b); clear s s1;
 114   lapply (Hletin); clear Hletin;
 115    [ cases Hletin1; cases x; change in f4 with (a = w);
 116      change with (a ♮g b); apply (. f4‡#); assumption;
 117    | exists; [apply a] split; [ assumption | change with (a=a); apply rule #;]]
 118 | cases (f1 a); lapply depth=0 (s1 b); clear s s1;
 119   lapply (Hletin); clear Hletin;
 120    [ cases Hletin1; cases x; change in f4 with (a = w);
 121      change with (a ♮f b); apply (. f4‡#); assumption;
 122    | exists; [apply a] split; [ assumption | change with (a=a); apply rule #;]]]
 123 qed.
 124
 125 variant eq_cones_to_eq_rel':
 126   ∀S,T. ∀f,g: arrows1 REL S T.
 127    (∀x:S. or_f ?? (map_arrows2 ?? POW S T f) {(x)} = or_f ?? (map_arrows2 ?? POW S T g) {(x)}) →
 128     f = g
 129 ≝ eq_cones_to_eq_rel.
 130
 131 lemma rOR_full :
 132   ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
 133     exT22 ? (λg:arrows2 rOBP s t.
 134        map_arrows2 ?? OR ?? (ℳ_2 g) = f).
 135 intros 2 (s t); cases s (s_2 s_1 s_eq); clear s;
 136 change in match (F2 ??? (mk_Fo ??????)) with s_2;
 137 cases s_eq; clear s_eq s_2;
 138 letin s1 ≝ (BP_to_OBP s_1); change in match (BP_to_OBP s_1) with s1;
 139 cases t (t_2 t_1 t_eq); clear t;
 140 change in match (F2 ??? (mk_Fo ??????)) with t_2;
 141 cases t_eq; clear t_eq t_2;
 142 letin t1 ≝ (BP_to_OBP t_1); change in match (BP_to_OBP t_1) with t1;
 143 whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
 144 intro; whd in s_1 t_1;
 145 letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1)));
 146 [2:
 147   exists;
 148     [ constructor 1;
 149        [2: simplify; apply R;
 150        | simplify; apply (fun12 ?? (map_arrows2 ?? BP_to_OBP s_1 t_1)); apply R;
 151        | simplify; apply rule #; ]]
 152    simplify;
 153 |1: constructor 1;
 154     [2: apply (pi1exT22 ?? (POW_full (form s_1) (form t_1) f));
 155     |1: letin u ≝ (or_f_star ?? (map_arrows2 ?? POW (concr t_1) (form t_1) (⊩ \sub t_1)));
 156         letin r ≝ (u ∘ (or_f ?? f));
 157         letin xxx ≝ (or_f ?? (map_arrows2 ?? POW (concr s_1) (form s_1) (⊩ \sub s_1)));
 158         letin r' ≝ (r ∘ xxx); clearbody r';
 159         apply (POW_full' (concr s_1) (concr t_1) r');
 160     | simplify in ⊢ (? ? ? (? ? ? ? ? % ?) ?);
 161       apply eq_cones_to_eq_rel'; intro;
 162       apply
 163        (cic:/matita/logic/equality/eq_elim_r''.con ?????
 164          (category2_of_category1_respects_comp_r : ?));
 165       apply rule (.= (#‡#));
 166       apply (.= (respects_comp2 ?? POW (concr s_1) (concr t_1) (form t_1) ? (⊩\sub t_1))‡#);
 167       apply sym2;
 168       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)))));
 169       apply (let H ≝(\snd (POW_full (form s_1) (form t_1) (Ocont_rel ?? f))) in .= #‡H);
 170       apply sym2;
 171  ]
 172
 173 STOP;
 174
 175
 176 (* Todo: rename BTop → OBTop *)
 177
 178 (* scrivo gli statement qua cosi' verra' un conflitto :-)
 179
 180 1. definire il funtore OR
 181 2. dimostrare che ORel e' faithful
 182
 183 3. Definire la funzione
 184     Apply:
 185     ∀C1,C2: CAT2.  F: arrows3 CAT2 C1 C2 → CAT2
 186     ≝
 187      constructor 1;
 188       [ gli oggetti sono gli oggetti di C1 mappati da F
 189       | i morfismi i morfismi di C1 mappati da F
 190       | ....
 191       ]
 192
 193    E : objs CATS === Σx.∃y. F y = x
 194
 195    Quindi (Apply C1 C2 F) (che usando da ora in avanti una coercion
 196    scrivero' (F C1) ) e' l'immagine di C1 tramite F ed e'
 197    una sottocategoria di C2 (qualcosa da dimostare qui??? vedi sotto
 198    al punto 5)
 199
 200 4. Definire rOBP (le OBP rappresentabili) come (BP_to_OBP BP)
 201   [Si puo' fare lo stesso per le OA: rOA ≝ Rel_to_OA REL ]
 202
 203 5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
 204    quando applicato a rOBP.
 205    Nota: puo' darsi che faccia storie ad accettare lo statement.
 206    Infatti rOBP e' (BP_to_OBP BP) ed e' "una sottocategoria di OBP"
 207    e OR va da OBP a OBTop. Non so se tipa subito o se devi dare
 208    una "proiezione" da rOBP a OBP.
 209
 210 6. Definire rOBTop come (OBP_to_OBTop rOBP).
 211
 212 7. Per composizione si ha un funtore full and faithful da BP a rOBTop:
 213    basta prendere (OR ∘ BP_to_OBP).
 214
 215 8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
 216    esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'
 217    faithful e full (banale: tutta conversione).
 218
 219 9. Per composizione si ha un funtore full and faithful da BP a BTop.
 220
 221 10. Dimostrare che i seguenti funtori sono anche isomorphism-dense
 222     (http://planetmath.org/encyclopedia/DenseFunctor.html):
 223
 224     BP_to_OBP
 225     OBP_to_OBTop quando applicato alle rOBP
 226     OBTop_to_BTop quando applicato alle rOBTop
 227
 228     Concludere per composizione che anche il funtore da BP a BTop e'
 229     isomorphism-dense.
 230
 231 ====== Da qui in avanti non e' "necessario" nulla:
 232
 233 == altre cose mancanti
 234
 235 11. Dimostrare che le r* e le * orrizzontali
 236     sono isomorfe dando il funtore da r* a * e dimostrando che componendo i
 237     due funtori ottengo l'identita'
 238
 239 12. La definizione di r* fa schifo: in pratica dici solo come ottieni
 240     qualcosa, ma non come lo caratterizzeresti. Ora un teorema carino
 241     e' che una a* (e.g. una aOBP) e' sempre una rOBP dove "a" sta per
 242     atomic. Dimostrarlo per tutte le r*.
 243
 244 == categorish/future works
 245
 246 13. definire astrattamente la FG-completion e usare quella per
 247     ottenere le BP da Rel e le OBP da OA.
 248
 249 14. indebolire le OA, generalizzare le costruzioni, etc. come detto
 250     con Giovanni
 251
 252 *)
 253