From 702253b774d81fffdb36e97dfb6f76d4e7f34588 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 22 Jan 2009 18:53:09 +0000 Subject: [PATCH] TODO --- .../o-basic_pairs_to_o-basic_topologies.ma | 74 +++++++++++++++++++ 1 file changed, 74 insertions(+) diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma index b78e7b037..432025c99 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma @@ -90,3 +90,77 @@ definition o_continuous_relation_of_o_relation_pair: change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U); apply (†e^-1);] qed. + +(* 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 + | .... + ] + + 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 + +*) -- 2.39.2