...

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

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
new file mode 100644 (file)
index 0000000..bba4662
--- /dev/null
+++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
@@ -0,0 +1,107 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_pairs_to_o-basic_pairs.ma".
+include "apply_functor.ma".
+
+definition rOBP ≝ Apply ?? BP_to_OBP.
+
+include "o-basic_pairs_to_o-basic_topologies.ma".
+
+lemma rOR_full : 
+  ∀rS,rT:rOBP.∀f:arrows2 ? (OR (F2 ??? rS)) (OR (F2 ??? rT)).
+    exT22 ? (λg:arrows2 OBP (F1 ??? rS) (F1 ??? rT).
+       map_arrows2 ? ? OR rS rT g = f).
+  ∀S,T.∀f. exT22 ? (λg. map_arrows2 ? ? OR S T g = f).
+arrows2 OBP S T
+unary_morphism1_setoid1 (OR S) (OR T)
+
+(* Todo: rename BTop → OBTop *)
+
+(* scrivo gli statement qua cosi' verra' un conflitto :-)
+
+1. definire il funtore OR
+2. dimostrare che ORel e' faithful
+
+3. Definire la funzione
+    Apply:
+     \forall 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
+      | ....
+      ]
+   
+   E : objs CATS === Σx.∃y. F y = x
+  
+   Quindi (Apply C1 C2 F) (che usando da ora in avanti una coercion
+   scrivero' (F C1) ) e' l'immagine di C1 tramite F ed e'
+   una sottocategoria di C2 (qualcosa da dimostare qui??? vedi sotto
+   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 ]
+
+5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
+   quando applicato a rOBP.
+   Nota: puo' darsi che faccia storie ad accettare lo statement.
+   Infatti rOBP e' (BP_to_OBP BP) ed e' "una sottocategoria di OBP"
+   e OR va da OBP a OBTop. Non so se tipa subito o se devi dare
+   una "proiezione" da rOBP a OBP.
+
+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).
+
+8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
+   esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'
+   faithful e full (banale: tutta conversione).
+
+9. Per composizione si ha un funtore full and faithful da BP a BTop.
+
+10. Dimostrare che i seguenti funtori sono anche isomorphism-dense
+    (http://planetmath.org/encyclopedia/DenseFunctor.html):
+
+    BP_to_OBP
+    OBP_to_OBTop quando applicato alle rOBP
+    OBTop_to_BTop quando applicato alle rOBTop
+
+    Concludere per composizione che anche il funtore da BP a BTop e'
+    isomorphism-dense.
+
+====== Da qui in avanti non e' "necessario" nulla:
+
+== altre cose mancanti
+
+11. Dimostrare che le r* e le * orrizzontali
+    sono isomorfe dando il funtore da r* a * e dimostrando che componendo i
+    due funtori ottengo l'identita'
+
+12. La definizione di r* fa schifo: in pratica dici solo come ottieni
+    qualcosa, ma non come lo caratterizzeresti. Ora un teorema carino
+    e' che una a* (e.g. una aOBP) e' sempre una rOBP dove "a" sta per
+    atomic. Dimostrarlo per tutte le r*.
+
+== categorish/future works
+
+13. definire astrattamente la FG-completion e usare quella per
+    ottenere le BP da Rel e le OBP da OA.
+
+14. indebolire le OA, generalizzare le costruzioni, etc. come detto
+    con Giovanni
+
+*)
+