helm/software/matita/library/formal_topology/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 "formal_topology/basic_pairs_to_o-basic_pairs.ma".
  16 include "formal_topology/apply_functor.ma".
  17
  18 definition rOBP ≝ Apply (category2_of_category1 BP) OBP BP_to_OBP.
  19
  20 include "formal_topology/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.(A × B ⇒_1 C) → A → (B ⇒_1 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:Ω^S ⇒_1 Ω^T. CProp1.
 100 intros (S T f); apply (∀X:Ω \sup S. (f X) =_1 ?);
 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 (*
 132 lemma rOR_full :
 133   ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
 134     exT22 ? (λg:arrows2 rOBP s t.
 135        map_arrows2 ?? OR ?? (ℳ_2 g) = f).
 136 intros 2 (s t); cases s (s_2 s_1 s_eq); clear s;
 137 change in match (F2 ??? (mk_Fo ??????)) with s_2;
 138 cases s_eq; clear s_eq s_2;
 139 letin s1 ≝ (BP_to_OBP s_1); change in match (BP_to_OBP s_1) with s1;
 140 cases t (t_2 t_1 t_eq); clear t;
 141 change in match (F2 ??? (mk_Fo ??????)) with t_2;
 142 cases t_eq; clear t_eq t_2;
 143 letin t1 ≝ (BP_to_OBP t_1); change in match (BP_to_OBP t_1) with t1;
 144 whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
 145 intro; whd in s_1 t_1;
 146 letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1)));
 147 [2:
 148   exists;
 149     [ constructor 1;
 150        [2: simplify; apply R;
 151        | simplify; apply (fun12 ?? (map_arrows2 ?? BP_to_OBP s_1 t_1)); apply R;
 152        | simplify; apply rule #; ]]
 153    simplify;
 154 |1: constructor 1;
 155     [2: apply (pi1exT22 ?? (POW_full (form s_1) (form t_1) f));
 156     |1: letin u ≝ (or_f_star ?? (map_arrows2 ?? POW (concr t_1) (form t_1) (⊩ \sub t_1)));
 157         letin r ≝ (u ∘ (or_f ?? f));
 158         letin xxx ≝ (or_f ?? (map_arrows2 ?? POW (concr s_1) (form s_1) (⊩ \sub s_1)));
 159         letin r' ≝ (r ∘ xxx); clearbody r';
 160         apply (POW_full' (concr s_1) (concr t_1) r');
 161     | simplify in ⊢ (? ? ? (? ? ? ? ? % ?) ?);
 162       apply eq_cones_to_eq_rel'; intro;
 163       apply
 164        (cic:/matita/logic/equality/eq_elim_r''.con ?????
 165          (category2_of_category1_respects_comp_r : ?));
 166       apply rule (.= (#‡#));
 167       apply (.= (respects_comp2 ?? POW (concr s_1) (concr t_1) (form t_1) ? (⊩\sub t_1))‡#);
 168       apply sym2;
 169       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)))));
 170       apply (let H ≝(\snd (POW_full (form s_1) (form t_1) (Ocont_rel ?? f))) in .= #‡H);
 171       apply sym2;
 172  ]
 173
 174 STOP;
 175
 176
 177 (* Todo: rename BTop → OBTop *)
 178
 179 (* scrivo gli statement qua cosi' verra' un conflitto :-)
 180
 181 1. definire il funtore OR
 182 2. dimostrare che ORel e' faithful
 183
 184 3. Definire la funzione
 185     Apply:
 186     ∀C1,C2: CAT2.  F: arrows3 CAT2 C1 C2 → CAT2
 187     ≝
 188      constructor 1;
 189       [ gli oggetti sono gli oggetti di C1 mappati da F
 190       | i morfismi i morfismi di C1 mappati da F
 191       | ....
 192       ]
 193
 194    E : objs CATS === Σx.∃y. F y = x
 195
 196    Quindi (Apply C1 C2 F) (che usando da ora in avanti una coercion
 197    scrivero' (F C1) ) e' l'immagine di C1 tramite F ed e'
 198    una sottocategoria di C2 (qualcosa da dimostare qui??? vedi sotto
 199    al punto 5)
 200
 201 4. Definire rOBP (le OBP rappresentabili) come (BP_to_OBP BP)
 202   [Si puo' fare lo stesso per le OA: rOA ≝ Rel_to_OA REL ]
 203
 204 5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
 205    quando applicato a rOBP.
 206    Nota: puo' darsi che faccia storie ad accettare lo statement.
 207    Infatti rOBP e' (BP_to_OBP BP) ed e' "una sottocategoria di OBP"
 208    e OR va da OBP a OBTop. Non so se tipa subito o se devi dare
 209    una "proiezione" da rOBP a OBP.
 210
 211 6. Definire rOBTop come (OBP_to_OBTop rOBP).
 212
 213 7. Per composizione si ha un funtore full and faithful da BP a rOBTop:
 214    basta prendere (OR ∘ BP_to_OBP).
 215
 216 8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
 217    esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'
 218    faithful e full (banale: tutta conversione).
 219
 220 9. Per composizione si ha un funtore full and faithful da BP a BTop.
 221
 222 10. Dimostrare che i seguenti funtori sono anche isomorphism-dense
 223     (http://planetmath.org/encyclopedia/DenseFunctor.html):
 224
 225     BP_to_OBP
 226     OBP_to_OBTop quando applicato alle rOBP
 227     OBTop_to_BTop quando applicato alle rOBTop
 228
 229     Concludere per composizione che anche il funtore da BP a BTop e'
 230     isomorphism-dense.
 231
 232 ====== Da qui in avanti non e' "necessario" nulla:
 233
 234 == altre cose mancanti
 235
 236 11. Dimostrare che le r* e le * orrizzontali
 237     sono isomorfe dando il funtore da r* a * e dimostrando che componendo i
 238     due funtori ottengo l'identita'
 239
 240 12. La definizione di r* fa schifo: in pratica dici solo come ottieni
 241     qualcosa, ma non come lo caratterizzeresti. Ora un teorema carino
 242     e' che una a* (e.g. una aOBP) e' sempre una rOBP dove "a" sta per
 243     atomic. Dimostrarlo per tutte le r*.
 244
 245 == categorish/future works
 246
 247 13. definire astrattamente la FG-completion e usare quella per
 248     ottenere le BP da Rel e le OBP da OA.
 249
 250 14. indebolire le OA, generalizzare le costruzioni, etc. come detto
 251     con Giovanni
 252
 253 *)
 254
 255 *)