1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_pairs_to_o-basic_pairs.ma".
16 include "apply_functor.ma".
18 definition rOBP ≝ Apply ?? BP_to_OBP.
20 include "o-basic_pairs_to_o-basic_topologies.ma".
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; cases s_eq; clear s_eq s_2;
27 intro; cases t (t_2 t_1 t_eq); clear t; cases t_eq; clear t_eq t_2;
28 whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
29 intro; whd in s_1 t_1;
30 letin y ≝ (f⎻* ); clearbody y;
31 change in y with (carr2 (POW (form s_1) ⇒ POW (form t_1)));
32 alias symbol "Vdash" = "basic pair relation for subsets (non applied)".
33 letin z ≝ (image ?? (⊩ \sub s_1)); clearbody z;
34 change in z with ((POW (concr s_1) → POW (form s_1)));
35 (*change in z with (carr2 (POW (concr s_1) ⇒ POW (form s_1)));*)
39 letin R ≝ (f* );∘ (⊩ \sub s_1));
43 whd in ⊢ (? % ?→?); cases s_eq; intro; whd in f;
45 intro; cases f (g H1 H2); clear f; exists;
48 | unfold F1; simplify;
54 cases f (h H1 H2); clear f; simplify;
55 change in ⊢ (? ? (λg:?.? ? ? (? ? ? %) ?)) with
56 (o_continuous_relation_of_o_relation_pair ?? (ℳ_2 g)).
61 (* Todo: rename BTop → OBTop *)
63 (* scrivo gli statement qua cosi' verra' un conflitto :-)
65 1. definire il funtore OR
66 2. dimostrare che ORel e' faithful
68 3. Definire la funzione
70 \forall C1,C2: CAT2. F: arrows3 CAT2 C1 C2 -> CAT2
73 [ gli oggetti sono gli oggetti di C1 mappati da F
74 | i morfismi i morfismi di C1 mappati da F
78 E : objs CATS === Σx.∃y. F y = x
80 Quindi (Apply C1 C2 F) (che usando da ora in avanti una coercion
81 scrivero' (F C1) ) e' l'immagine di C1 tramite F ed e'
82 una sottocategoria di C2 (qualcosa da dimostare qui??? vedi sotto
85 4. Definire rOBP (le OBP rappresentabili) come (BP_to_OBP BP)
86 [Si puo' fare lo stesso per le OA: rOA := Rel_to_OA REL ]
88 5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
89 quando applicato a rOBP.
90 Nota: puo' darsi che faccia storie ad accettare lo statement.
91 Infatti rOBP e' (BP_to_OBP BP) ed e' "una sottocategoria di OBP"
92 e OR va da OBP a OBTop. Non so se tipa subito o se devi dare
93 una "proiezione" da rOBP a OBP.
95 6. Definire rOBTop come (OBP_to_OBTop rOBP).
97 7. Per composizione si ha un funtore full and faithful da BP a rOBTop:
98 basta prendere (OR \circ BP_to_OBP).
100 8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
101 esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'
102 faithful e full (banale: tutta conversione).
104 9. Per composizione si ha un funtore full and faithful da BP a BTop.
106 10. Dimostrare che i seguenti funtori sono anche isomorphism-dense
107 (http://planetmath.org/encyclopedia/DenseFunctor.html):
110 OBP_to_OBTop quando applicato alle rOBP
111 OBTop_to_BTop quando applicato alle rOBTop
113 Concludere per composizione che anche il funtore da BP a BTop e'
116 ====== Da qui in avanti non e' "necessario" nulla:
118 == altre cose mancanti
120 11. Dimostrare che le r* e le * orrizzontali
121 sono isomorfe dando il funtore da r* a * e dimostrando che componendo i
122 due funtori ottengo l'identita'
124 12. La definizione di r* fa schifo: in pratica dici solo come ottieni
125 qualcosa, ma non come lo caratterizzeresti. Ora un teorema carino
126 e' che una a* (e.g. una aOBP) e' sempre una rOBP dove "a" sta per
127 atomic. Dimostrarlo per tutte le r*.
129 == categorish/future works
131 13. definire astrattamente la FG-completion e usare quella per
132 ottenere le BP da Rel e le OBP da OA.
134 14. indebolire le OA, generalizzare le costruzioni, etc. come detto