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 rOR_full :
  23   ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
  24     exT22 ? (λg:arrows2 rOBP s t.
  25        map_arrows2 ?? OR ?? (ℳ_2 g) = f).
  26 intro; cases s (s_2 s_1 s_eq); clear s;
  27 whd in ⊢ (?→? (? ? (? ?? ? %) ?)→?);
  28 whd in ⊢ (?→?→? ? (λ_:?.? ? ? (? ? ? (? ? ? (? ? ? ? % ?) ?)) ?));;
  29 include "logic/equality.ma".
  30 lapply (
  31 match s_eq in eq return
  32  (λright_1:?.(λmatched:(eq (objs2 OBP) (map_objs2 (category2_of_category1 BP) OBP BP_to_OBP s_1) right_1).
  33   (∀t:(objs2 rOBP).
  34    (∀f:(carr2 (arrows2 OBTop (map_objs2 OBP OBTop OR right_1) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))).
  35     (exT22 (carr2 (arrows2 rOBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t))
  36      (λg:(carr2 (arrows2 rOBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t)).
  37       (eq_rel1 (carr1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))))
  38        (eq1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))))
  39        (carr1_OF_Ocontinuous_relation
  40          (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP (*XXX*)right_1 s_1 matched)))
  41          (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))
  42          (fun12
  43           (arrows2 OBP (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched)) (F2 (category2_of_category1 BP) OBP BP_to_OBP t))
  44           (arrows2 OBTop (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))
  45           (map_arrows2 OBP OBTop OR right_1 (F2 (category2_of_category1 BP) OBP BP_to_OBP t))
  46           (Fm2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP right_1 s_1 matched) t g)))
  47       ?)))))))
  48        with
  49        [ refl_eq ⇒ ?
  50 ]);
  51     STOP.
  52        (eq_rel1 (carr1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))))
  53         (eq1 (unary_morphism1_setoid1 (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)))) (objs2_OF_Obasic_topology (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)))))
  54         (carr1_OF_Ocontinuous_relation (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (fun12 (arrows2 OBP (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched)) (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (arrows2 OBTop (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t))) (map_arrows2 OBP OBTop OR ? (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) (Fm2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched) t g)))
  55         (carr1_OF_Ocontinuous_relation (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP (mk_Fo (category2_of_category1 BP) OBP BP_to_OBP ? s_1 matched))) (map_objs2 OBP OBTop OR (F2 (category2_of_category1 BP) OBP BP_to_OBP t)) f)))))))) with
  56  [ refl_eq ⇒ ?
  57 ]);
  58 cases s_eq; clear s_eq s_2;
  59 intro; cases t (t_2 t_1 t_eq); clear t; cases t_eq; clear t_eq t_2;
  60 whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
  61 intro; whd in s_1 t_1;
  62 letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1)));
  63  [2:
  64    exists;
  65     [ constructor 1;
  66        [2: simplify; apply R;
  67        | simplify; apply (fun12 ?? (map_arrows2 ?? BP_to_OBP s_1 t_1)); apply R;
  68        | simplify; apply rule #; ]]
  69    simplify;
  70  | constructor 1;
  71     [2: constructor 1; constructor 1;
  72       [ intros (x y); apply (y ∈ f (singleton ? x));
  73       | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
  74         unfold in ⊢ (? ? ? (? ? ? ? ? ? %) ?); apply (.= e1‡††e);
  75         apply rule #; ]
  76     |1: constructor 1; constructor 1;
  77       [ intros (x y); apply (y ∈ star_image ?? (⊩ \sub t_1) (f (image ?? (⊩ \sub s_1) (singleton ? x))));
  78       | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
  79         unfold in ⊢ (? ? ? (? ? ? ? ? ? (? ? ? ? ? ? %)) ?);
  80         apply (.= e1‡(#‡†(#‡†e))); apply rule #; ]
  81     | whd; simplify; intros; simplify;
  82       whd in ⊢ (? % %); simplify in ⊢ (? % %);
  83       lapply (Oreduced ?? f (image (concr s_1) (form s_1) (⊩ \sub s_1) (singleton ? x)));
  84        [ whd in Hletin; simplify in Hletin; cases Hletin; clear Hletin;
  85          lapply (s y); clear s;
  86 whd in Hletin:(? ? ? (? ? (? ? ? % ?)) ?); simplify in Hletin;
  87 whd in Hletin; simplify in Hletin;
  88          lapply (s1 y); clear s1;
  89      split; intros; simplify; whd in f1 ⊢ %; simplify in f1 ⊢ %;
  90       cases f1; clear f1; cases x1; clear x1;
  91        [
  92        | exists;
  93        ]
  94  ]
  95
  96 STOP;
  97
  98
  99 (* Todo: rename BTop → OBTop *)
 100
 101 (* scrivo gli statement qua cosi' verra' un conflitto :-)
 102
 103 1. definire il funtore OR
 104 2. dimostrare che ORel e' faithful
 105
 106 3. Definire la funzione
 107     Apply:
 108     ∀C1,C2: CAT2.  F: arrows3 CAT2 C1 C2 → CAT2
 109     ≝
 110      constructor 1;
 111       [ gli oggetti sono gli oggetti di C1 mappati da F
 112       | i morfismi i morfismi di C1 mappati da F
 113       | ....
 114       ]
 115
 116    E : objs CATS === Σx.∃y. F y = x
 117
 118    Quindi (Apply C1 C2 F) (che usando da ora in avanti una coercion
 119    scrivero' (F C1) ) e' l'immagine di C1 tramite F ed e'
 120    una sottocategoria di C2 (qualcosa da dimostare qui??? vedi sotto
 121    al punto 5)
 122
 123 4. Definire rOBP (le OBP rappresentabili) come (BP_to_OBP BP)
 124   [Si puo' fare lo stesso per le OA: rOA ≝ Rel_to_OA REL ]
 125
 126 5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
 127    quando applicato a rOBP.
 128    Nota: puo' darsi che faccia storie ad accettare lo statement.
 129    Infatti rOBP e' (BP_to_OBP BP) ed e' "una sottocategoria di OBP"
 130    e OR va da OBP a OBTop. Non so se tipa subito o se devi dare
 131    una "proiezione" da rOBP a OBP.
 132
 133 6. Definire rOBTop come (OBP_to_OBTop rOBP).
 134
 135 7. Per composizione si ha un funtore full and faithful da BP a rOBTop:
 136    basta prendere (OR ∘ BP_to_OBP).
 137
 138 8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
 139    esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'
 140    faithful e full (banale: tutta conversione).
 141
 142 9. Per composizione si ha un funtore full and faithful da BP a BTop.
 143
 144 10. Dimostrare che i seguenti funtori sono anche isomorphism-dense
 145     (http://planetmath.org/encyclopedia/DenseFunctor.html):
 146
 147     BP_to_OBP
 148     OBP_to_OBTop quando applicato alle rOBP
 149     OBTop_to_BTop quando applicato alle rOBTop
 150
 151     Concludere per composizione che anche il funtore da BP a BTop e'
 152     isomorphism-dense.
 153
 154 ====== Da qui in avanti non e' "necessario" nulla:
 155
 156 == altre cose mancanti
 157
 158 11. Dimostrare che le r* e le * orrizzontali
 159     sono isomorfe dando il funtore da r* a * e dimostrando che componendo i
 160     due funtori ottengo l'identita'
 161
 162 12. La definizione di r* fa schifo: in pratica dici solo come ottieni
 163     qualcosa, ma non come lo caratterizzeresti. Ora un teorema carino
 164     e' che una a* (e.g. una aOBP) e' sempre una rOBP dove "a" sta per
 165     atomic. Dimostrarlo per tutte le r*.
 166
 167 == categorish/future works
 168
 169 13. definire astrattamente la FG-completion e usare quella per
 170     ottenere le BP da Rel e le OBP da OA.
 171
 172 14. indebolire le OA, generalizzare le costruzioni, etc. come detto
 173     con Giovanni
 174
 175 *)
 176