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 ?? 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 intros; cases f (h H1 H2); clear f; simplify;
  27 change in ⊢ (? ? (λg:?.? ? ? (? ? ? %) ?)) with
  28   (o_continuous_relation_of_o_relation_pair ?? (ℳ_2 g)).
  29
  30 STOP;
  31
  32
  33 (* Todo: rename BTop → OBTop *)
  34
  35 (* scrivo gli statement qua cosi' verra' un conflitto :-)
  36
  37 1. definire il funtore OR
  38 2. dimostrare che ORel e' faithful
  39
  40 3. Definire la funzione
  41     Apply:
  42      \forall C1,C2: CAT2.  F: arrows3 CAT2 C1 C2 -> CAT2
  43     :=
  44      constructor 1;
  45       [ gli oggetti sono gli oggetti di C1 mappati da F
  46       | i morfismi i morfismi di C1 mappati da F
  47       | ....
  48       ]
  49
  50    E : objs CATS === Σx.∃y. F y = x
  51
  52    Quindi (Apply C1 C2 F) (che usando da ora in avanti una coercion
  53    scrivero' (F C1) ) e' l'immagine di C1 tramite F ed e'
  54    una sottocategoria di C2 (qualcosa da dimostare qui??? vedi sotto
  55    al punto 5)
  56
  57 4. Definire rOBP (le OBP rappresentabili) come (BP_to_OBP BP)
  58   [Si puo' fare lo stesso per le OA: rOA := Rel_to_OA REL ]
  59
  60 5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
  61    quando applicato a rOBP.
  62    Nota: puo' darsi che faccia storie ad accettare lo statement.
  63    Infatti rOBP e' (BP_to_OBP BP) ed e' "una sottocategoria di OBP"
  64    e OR va da OBP a OBTop. Non so se tipa subito o se devi dare
  65    una "proiezione" da rOBP a OBP.
  66
  67 6. Definire rOBTop come (OBP_to_OBTop rOBP).
  68
  69 7. Per composizione si ha un funtore full and faithful da BP a rOBTop:
  70    basta prendere (OR \circ BP_to_OBP).
  71
  72 8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
  73    esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'
  74    faithful e full (banale: tutta conversione).
  75
  76 9. Per composizione si ha un funtore full and faithful da BP a BTop.
  77
  78 10. Dimostrare che i seguenti funtori sono anche isomorphism-dense
  79     (http://planetmath.org/encyclopedia/DenseFunctor.html):
  80
  81     BP_to_OBP
  82     OBP_to_OBTop quando applicato alle rOBP
  83     OBTop_to_BTop quando applicato alle rOBTop
  84
  85     Concludere per composizione che anche il funtore da BP a BTop e'
  86     isomorphism-dense.
  87
  88 ====== Da qui in avanti non e' "necessario" nulla:
  89
  90 == altre cose mancanti
  91
  92 11. Dimostrare che le r* e le * orrizzontali
  93     sono isomorfe dando il funtore da r* a * e dimostrando che componendo i
  94     due funtori ottengo l'identita'
  95
  96 12. La definizione di r* fa schifo: in pratica dici solo come ottieni
  97     qualcosa, ma non come lo caratterizzeresti. Ora un teorema carino
  98     e' che una a* (e.g. una aOBP) e' sempre una rOBP dove "a" sta per
  99     atomic. Dimostrarlo per tutte le r*.
 100
 101 == categorish/future works
 102
 103 13. definire astrattamente la FG-completion e usare quella per
 104     ottenere le BP da Rel e le OBP da OA.
 105
 106 14. indebolire le OA, generalizzare le costruzioni, etc. come detto
 107     con Giovanni
 108
 109 *)
 110