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 (category2_of_category1 BP) OBP 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 intros 2 (s t); cases s (s_2 s_1 s_eq); clear s;
27 change in match (F2 ??? (mk_Fo ??????)) with s_2;
28 cases s_eq; clear s_eq s_2;
29 letin s1 ≝ (BP_to_OBP s_1); change in match (BP_to_OBP s_1) with s1;
30 cases t (t_2 t_1 t_eq); clear t;
31 change in match (F2 ??? (mk_Fo ??????)) with t_2;
32 cases t_eq; clear t_eq t_2;
33 letin t1 ≝ (BP_to_OBP t_1); change in match (BP_to_OBP t_1) with t1;
34 whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
35 intro; whd in s_1 t_1;
36 letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1)));
40 [2: simplify; apply R;
41 | simplify; apply (fun12 ?? (map_arrows2 ?? BP_to_OBP s_1 t_1)); apply R;
42 | simplify; apply rule #; ]]
45 [2: constructor 1; constructor 1;
46 [ intros (x y); apply (y ∈ f (singleton ? x));
47 | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
48 unfold in ⊢ (? ? ? (? ? ? ? ? ? %) ?); apply (.= e1‡††e);
50 |1: constructor 1; constructor 1;
51 [ intros (x y); apply (y ∈ star_image ?? (⊩ \sub t_1) (f (image ?? (⊩ \sub s_1) (singleton ? x))));
52 | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
53 unfold in ⊢ (? ? ? (? ? ? ? ? ? (? ? ? ? ? ? %)) ?);
54 apply (.= e1‡(#‡†(#‡†e))); apply rule #; ]
55 | whd; simplify; intros; simplify;
56 whd in ⊢ (? % %); simplify in ⊢ (? % %);
57 lapply (Oreduced ?? f (image (concr s_1) (form s_1) (⊩ \sub s_1) (singleton ? x)));
58 [ cases Hletin; clear Hletin;
59 lapply (s y); clear s;
60 whd in Hletin:(? ? ? (? ? (? ? ? % ?)) ?); simplify in Hletin;
61 whd in Hletin; simplify in Hletin;
62 lapply (s1 y); clear s1;
63 split; intros; simplify; whd in f1 ⊢ %; simplify in f1 ⊢ %;
64 cases f1; clear f1; cases x1; clear x1;
73 (* Todo: rename BTop → OBTop *)
75 (* scrivo gli statement qua cosi' verra' un conflitto :-)
77 1. definire il funtore OR
78 2. dimostrare che ORel e' faithful
80 3. Definire la funzione
82 ∀C1,C2: CAT2. F: arrows3 CAT2 C1 C2 → CAT2
85 [ gli oggetti sono gli oggetti di C1 mappati da F
86 | i morfismi i morfismi di C1 mappati da F
90 E : objs CATS === Σx.∃y. F y = x
92 Quindi (Apply C1 C2 F) (che usando da ora in avanti una coercion
93 scrivero' (F C1) ) e' l'immagine di C1 tramite F ed e'
94 una sottocategoria di C2 (qualcosa da dimostare qui??? vedi sotto
97 4. Definire rOBP (le OBP rappresentabili) come (BP_to_OBP BP)
98 [Si puo' fare lo stesso per le OA: rOA ≝ Rel_to_OA REL ]
100 5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
101 quando applicato a rOBP.
102 Nota: puo' darsi che faccia storie ad accettare lo statement.
103 Infatti rOBP e' (BP_to_OBP BP) ed e' "una sottocategoria di OBP"
104 e OR va da OBP a OBTop. Non so se tipa subito o se devi dare
105 una "proiezione" da rOBP a OBP.
107 6. Definire rOBTop come (OBP_to_OBTop rOBP).
109 7. Per composizione si ha un funtore full and faithful da BP a rOBTop:
110 basta prendere (OR ∘ BP_to_OBP).
112 8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
113 esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'
114 faithful e full (banale: tutta conversione).
116 9. Per composizione si ha un funtore full and faithful da BP a BTop.
118 10. Dimostrare che i seguenti funtori sono anche isomorphism-dense
119 (http://planetmath.org/encyclopedia/DenseFunctor.html):
122 OBP_to_OBTop quando applicato alle rOBP
123 OBTop_to_BTop quando applicato alle rOBTop
125 Concludere per composizione che anche il funtore da BP a BTop e'
128 ====== Da qui in avanti non e' "necessario" nulla:
130 == altre cose mancanti
132 11. Dimostrare che le r* e le * orrizzontali
133 sono isomorfe dando il funtore da r* a * e dimostrando che componendo i
134 due funtori ottengo l'identita'
136 12. La definizione di r* fa schifo: in pratica dici solo come ottieni
137 qualcosa, ma non come lo caratterizzeresti. Ora un teorema carino
138 e' che una a* (e.g. una aOBP) e' sempre una rOBP dove "a" sta per
139 atomic. Dimostrarlo per tutte le r*.
141 == categorish/future works
143 13. definire astrattamente la FG-completion e usare quella per
144 ottenere le BP da Rel e le OBP da OA.
146 14. indebolire le OA, generalizzare le costruzioni, etc. come detto