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 "o-basic_pairs.ma".
  16 include "o-basic_topologies.ma".
  17
  18 alias symbol "eq" = "setoid1 eq".
  19
  20 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
  21 definition o_basic_topology_of_o_basic_pair: OBP → BTop.
  22  intro t;
  23  constructor 1;
  24   [ apply (Oform t);
  25   | apply (□_t ∘ Ext⎽t);
  26   | apply (◊_t ∘ Rest⎽t);
  27   | intros 2; split; intro;
  28      [ change with ((⊩) \sup ⎻* ((⊩) \sup ⎻ U) ≤ (⊩) \sup ⎻* ((⊩) \sup ⎻ V));
  29        apply (. (#‡(lemma_10_4_a ?? (⊩) V)^-1));
  30        apply f_minus_star_image_monotone;
  31        apply f_minus_image_monotone;
  32        assumption
  33      | apply oa_leq_trans;
  34         [3: apply f;
  35         | skip
  36         | change with (U ≤ (⊩)⎻* ((⊩)⎻ U));
  37           apply (. (or_prop2 : ?) ^ -1);
  38           apply oa_leq_refl; ]]
  39   | intros 2; split; intro;
  40      [ change with (◊_t ((⊩) \sup * U) ≤ ◊_t ((⊩) \sup * V));
  41        apply (. ((lemma_10_4_b ?? (⊩) U)^-1)‡#);
  42        apply (f_image_monotone ?? (⊩) ? ((⊩)* V));
  43        apply f_star_image_monotone;
  44        assumption;
  45      | apply oa_leq_trans;
  46         [2: apply f;
  47         | skip
  48         | change with ((⊩) ((⊩)* V) ≤ V);
  49           apply (. (or_prop1 : ?));
  50           apply oa_leq_refl; ]]
  51   | intros;
  52     apply (.= (oa_overlap_sym' : ?));
  53     change with ((◊_t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊_t ((⊩)* V))));
  54     apply (.= (or_prop3 ?? (⊩) ((⊩)* V) ?));
  55     apply (.= #‡(lemma_10_3_a : ?));
  56     apply (.= (or_prop3 : ?)^-1);
  57     apply (oa_overlap_sym' ? ((⊩) ((⊩)* V)) U); ]
  58 qed.
  59
  60 definition o_continuous_relation_of_o_relation_pair:
  61  ∀BP1,BP2.arrows2 OBP BP1 BP2 →
  62   arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
  63  intros (BP1 BP2 t);
  64  constructor 1;
  65   [ apply (t \sub \f);
  66   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
  67     apply sym1;
  68     apply (.= †(†e));
  69     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
  70     cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
  71       cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩)* U));]
  72     apply (.= †COM);
  73     change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
  74     apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
  75     apply (.= COM ^ -1);
  76     change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
  77     change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
  78     apply (†e^-1);
  79   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
  80     apply sym1;
  81     apply (.= †(†e));
  82     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
  83     cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
  84       cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
  85     apply (.= †COM);
  86     change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
  87     apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
  88     apply (.= COM ^ -1);
  89     change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
  90     change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
  91     apply (†e^-1);]
  92 qed.
  93
  94 (* scrivo gli statement qua cosi' verra' un conflitto :-)
  95
  96 1. definire il funtore OR
  97 2. dimostrare che ORel e' faithful
  98
  99 3. Definire la funzione
 100     Apply:
 101      \forall C1,C2: CAT2.  F: arrows3 CAT2 C1 C2 -> CAT2
 102     :=
 103      constructor 1;
 104       [ gli oggetti sono gli oggetti di C1 mappati da F
 105       | i morfismi i morfismi di C1 mappati da F
 106       | ....
 107       ]
 108
 109    Quindi (Apply C1 C2 F) (che usando da ora in avanti una coercion
 110    scrivero' (F C1) ) e' l'immagine di C1 tramite F ed e'
 111    una sottocategoria di C2 (qualcosa da dimostare qui??? vedi sotto
 112    al punto 5)
 113
 114 4. Definire rOBP (le OBP rappresentabili) come (BP_to_OBP BP)
 115   [Si puo' fare lo stesso per le OA: rOA := Rel_to_OA REL ]
 116
 117 5. Dimostrare che OR (il funtore faithful da OBP a OBTop) e' full
 118    quando applicato a rOBP.
 119    Nota: puo' darsi che faccia storie ad accettare lo statement.
 120    Infatti rOBP e' (BP_to_OBP BP) ed e' "una sottocategoria di OBP"
 121    e OR va da OBP a OBTop. Non so se tipa subito o se devi dare
 122    una "proiezione" da rOBP a OBP.
 123
 124 6. Definire rOBTop come (OBP_to_OBTop rOBP).
 125
 126 7. Per composizione si ha un funtore full and faithful da BP a rOBTop:
 127    basta prendere (OR \circ BP_to_OBP).
 128
 129 8. Dimostrare (banale: quasi tutti i campi sono per conversione) che
 130    esiste un funtore da rOBTop a BTop. Dimostrare che tale funtore e'
 131    faithful e full (banale: tutta conversione).
 132
 133 9. Per composizione si ha un funtore full and faithful da BP a BTop.
 134
 135 10. Dimostrare che i seguenti funtori sono anche isomorphism-dense
 136     (http://planetmath.org/encyclopedia/DenseFunctor.html):
 137
 138     BP_to_OBP
 139     OBP_to_OBTop quando applicato alle rOBP
 140     OBTop_to_BTop quando applicato alle rOBTop
 141
 142     Concludere per composizione che anche il funtore da BP a BTop e'
 143     isomorphism-dense.
 144
 145 ====== Da qui in avanti non e' "necessario" nulla:
 146
 147 == altre cose mancanti
 148
 149 11. Dimostrare che le r* e le * orrizzontali
 150     sono isomorfe dando il funtore da r* a * e dimostrando che componendo i
 151     due funtori ottengo l'identita'
 152
 153 12. La definizione di r* fa schifo: in pratica dici solo come ottieni
 154     qualcosa, ma non come lo caratterizzeresti. Ora un teorema carino
 155     e' che una a* (e.g. una aOBP) e' sempre una rOBP dove "a" sta per
 156     atomic. Dimostrarlo per tutte le r*.
 157
 158 == categorish/future works
 159
 160 13. definire astrattamente la FG-completion e usare quella per
 161     ottenere le BP da Rel e le OBP da OA.
 162
 163 14. indebolire le OA, generalizzare le costruzioni, etc. come detto
 164     con Giovanni
 165
 166 *)