helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.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 "notation.ma".
  16 include "o-basic_pairs.ma".
  17 include "o-basic_topologies.ma".
  18
  19 alias symbol "eq" = "setoid1 eq".
  20
  21 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
  22 definition o_basic_topology_of_o_basic_pair: OBP → BTop.
  23  intro t;
  24  constructor 1;
  25   [ apply (Oform t);
  26   | apply (□_t ∘ Ext⎽t);
  27   | apply (◊_t ∘ Rest⎽t);
  28   | apply hide; intros 2; split; intro;
  29      [ change with ((⊩) \sup ⎻* ((⊩) \sup ⎻ U) ≤ (⊩) \sup ⎻* ((⊩) \sup ⎻ V));
  30        apply (. (#‡(lemma_10_4_a ?? (⊩) V)^-1));
  31        apply f_minus_star_image_monotone;
  32        apply f_minus_image_monotone;
  33        assumption
  34      | apply oa_leq_trans;
  35         [3: apply f;
  36         | skip
  37         | change with (U ≤ (⊩)⎻* ((⊩)⎻ U));
  38           apply (. (or_prop2 : ?) ^ -1);
  39           apply oa_leq_refl; ]]
  40   | apply hide; intros 2; split; intro;
  41      [ change with (◊_t ((⊩) \sup * U) ≤ ◊_t ((⊩) \sup * V));
  42        apply (. ((lemma_10_4_b ?? (⊩) U)^-1)‡#);
  43        apply (f_image_monotone ?? (⊩) ? ((⊩)* V));
  44        apply f_star_image_monotone;
  45        assumption;
  46      | apply oa_leq_trans;
  47         [2: apply f;
  48         | skip
  49         | change with ((⊩) ((⊩)* V) ≤ V);
  50           apply (. (or_prop1 : ?));
  51           apply oa_leq_refl; ]]
  52   | apply hide; intros;
  53     apply (.= (oa_overlap_sym' : ?));
  54     change with ((◊_t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊_t ((⊩)* V))));
  55     apply (.= (or_prop3 ?? (⊩) ((⊩)* V) ?));
  56     apply (.= #‡(lemma_10_3_a : ?));
  57     apply (.= (or_prop3 : ?)^-1);
  58     apply (oa_overlap_sym' ? ((⊩) ((⊩)* V)) U); ]
  59 qed.
  60
  61 definition o_continuous_relation_of_o_relation_pair:
  62  ∀BP1,BP2.arrows2 OBP BP1 BP2 →
  63   arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
  64  intros (BP1 BP2 t);
  65  constructor 1;
  66   [ apply (t \sub \f);
  67   | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
  68     apply sym1;
  69     apply (.= †(†e));
  70     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
  71     cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
  72       cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩)* U));]
  73     apply (.= †COM);
  74     change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
  75     apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
  76     apply (.= COM ^ -1);
  77     change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
  78     change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
  79     apply (†e^-1);
  80   | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
  81     apply sym1;
  82     apply (.= †(†e));
  83     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
  84     cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
  85       cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
  86     apply (.= †COM);
  87     change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
  88     apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
  89     apply (.= COM ^ -1);
  90     change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
  91     change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
  92     apply (†e^-1);]
  93 qed.
  94
  95
  96 definition OR : carr3 (arrows3 CAT2 OBP BTop).
  97 constructor 1;
  98 [ apply o_basic_topology_of_o_basic_pair;
  99 | intros; constructor 1;
 100   [ apply o_continuous_relation_of_o_relation_pair;
 101   | apply hide;
 102     intros; whd; unfold o_continuous_relation_of_o_relation_pair; simplify;;
 103     change with ((a \sub \f ⎻* ∘ A (o_basic_topology_of_o_basic_pair S)) =
 104                  (a' \sub \f ⎻*∘A (o_basic_topology_of_o_basic_pair S)));
 105     whd in e; cases e; clear e e2 e3 e4;
 106     change in ⊢ (? ? ? (? ? ? ? ? % ?) ?) with ((⊩\sub S)⎻* ∘ (⊩\sub S)⎻);
 107     apply (.= (comp_assoc2 ? ???? ?? a\sub\f⎻* ));
 108     change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a\sub\f ∘ ⊩\sub S)⎻*;
 109     apply (.= #‡†(Ocommute:?)^-1);
 110     apply (.= #‡e1);
 111     change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (⊩\sub T ∘ a'\sub\c)⎻*;
 112     apply (.= #‡†(Ocommute:?));
 113     change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a'\sub\f⎻* ∘ (⊩\sub S)⎻* );
 114     apply (.= (comp_assoc2 ? ???? ?? a'\sub\f⎻* )^-1);
 115     apply refl2;]
 116 | intros 2 (o a); apply rule #;
 117 | intros 6; apply refl1;]
 118 qed.
 119
 120 (*
 121 axiom DDD : False.
 122
 123 definition sigma_equivalence_relation2:
 124  ∀C2:CAT2.∀Q.∀X,Y:exT22 ? (λy:C2.Q y).∀P.
 125    equivalence_relation2 (exT22 ? (λf:arrows2 C2 (\fst X) (\fst Y).P f)).
 126 intros; constructor 1;
 127     [ intros(F G); apply (\fst F =_2 \fst G);
 128     | intro; apply refl2;
 129     | intros 3; apply sym2; assumption;
 130     | intros 5; apply (trans2 ?? ??? x1 x2);]
 131 qed.
 132
 133 definition Apply : ∀C1,C2: CAT2.arrows3 CAT2 C1 C2 → CAT2.
 134 intros (C1 C2 F);
 135 constructor 1;
 136 [ apply (exT22 ? (λx:C2.exT22 ? (λy:C1.map_objs2 ?? F y =_\ID x)));
 137 | intros (X Y); constructor 1;
 138   [ apply (exT22 ? (λf:arrows2 C2 (\fst X) (\fst Y).
 139            exT22 ? (λg:arrows2 C1 (\fst (\snd X)) (\fst (\snd Y)).
 140            ? (map_arrows2 ?? F ?? g) = f)));
 141     intro; apply hide; clear g f; cases X in c; cases Y; cases x; cases x1; clear X Y x x1;
 142     simplify; cases H; cases H1; intros; assumption;
 143   | apply sigma_equivalence_relation2;]
 144 | intro o; constructor 1;
 145    [ apply (id2 C2 (\fst o))
 146    | exists[apply (id2 C1 (\fst (\snd o)))]
 147      cases o; cases x; cases H; unfold hide; simplify;
 148      apply (respects_id2 ?? F);]
 149 | intros (o1 o2 o3); constructor 1;
 150   [ intros (f g); whd in f g; constructor 1;
 151     [ apply (comp2 C2 (\fst o1) (\fst o2) (\fst o3) (\fst f) (\fst g));
 152     | exists[apply (comp2 C1 (\fst (\snd o1)) (\fst (\snd o2)) (\fst (\snd o3)) (\fst (\snd f)) (\fst (\snd g)))]
 153     cases o1; cases x; cases H;
 154
 155 (* scrivo gli statement qua cosi' verra' un conflitto :-)
 156
 157 1. definire il funtore OR
 158 2. dimostrare che ORel e' faithful
 159
 160 3. Definire la funzione
 161     Apply:
 162      \forall C1,C2: CAT2.  F: arrows3 CAT2 C1 C2 -> CAT2
 163     :=
 164      constructor 1;
 165       [ gli oggetti sono gli oggetti di C1 mappati da F
 166       | i morfismi i morfismi di C1 mappati da F
 167       | ....
 168       ]
 169
 170    E : objs CATS === Σx.∃y. F y = x
 171
 172    Quindi (Apply C1 C2 F) (che usando da ora in avanti una coercion
 173    scrivero' (F C1) ) e' l'immagine di C1 tramite F ed e'
 174    una sottocategoria di C2 (qualcosa da dimostare qui??? vedi sotto
 175    al punto 5)
 176
 177 4. Definire rOBP (le OBP rappresentabili) come (BP_to_OBP BP)
 178   [Si puo' fare lo stesso per le OA: rOA := Rel_to_OA REL ]
 179
 180 5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
 181    quando applicato a rOBP.
 182    Nota: puo' darsi che faccia storie ad accettare lo statement.
 183    Infatti rOBP e' (BP_to_OBP BP) ed e' "una sottocategoria di OBP"
 184    e OR va da OBP a OBTop. Non so se tipa subito o se devi dare
 185    una "proiezione" da rOBP a OBP.
 186
 187 6. Definire rOBTop come (OBP_to_OBTop rOBP).
 188
 189 7. Per composizione si ha un funtore full and faithful da BP a rOBTop:
 190    basta prendere (OR \circ BP_to_OBP).
 191
 192 8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
 193    esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'
 194    faithful e full (banale: tutta conversione).
 195
 196 9. Per composizione si ha un funtore full and faithful da BP a BTop.
 197
 198 10. Dimostrare che i seguenti funtori sono anche isomorphism-dense
 199     (http://planetmath.org/encyclopedia/DenseFunctor.html):
 200
 201     BP_to_OBP
 202     OBP_to_OBTop quando applicato alle rOBP
 203     OBTop_to_BTop quando applicato alle rOBTop
 204
 205     Concludere per composizione che anche il funtore da BP a BTop e'
 206     isomorphism-dense.
 207
 208 ====== Da qui in avanti non e' "necessario" nulla:
 209
 210 == altre cose mancanti
 211
 212 11. Dimostrare che le r* e le * orrizzontali
 213     sono isomorfe dando il funtore da r* a * e dimostrando che componendo i
 214     due funtori ottengo l'identita'
 215
 216 12. La definizione di r* fa schifo: in pratica dici solo come ottieni
 217     qualcosa, ma non come lo caratterizzeresti. Ora un teorema carino
 218     e' che una a* (e.g. una aOBP) e' sempre una rOBP dove "a" sta per
 219     atomic. Dimostrarlo per tutte le r*.
 220
 221 == categorish/future works
 222
 223 13. definire astrattamente la FG-completion e usare quella per
 224     ottenere le BP da Rel e le OBP da OA.
 225
 226 14. indebolire le OA, generalizzare le costruzioni, etc. come detto
 227     con Giovanni
 228
 229 *)
 230