From a484c51de8ba6c56f02f9c0758688d3c9186b63d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Jan 2009 17:55:31 +0000 Subject: [PATCH] ... --- .../formal_topology/overlap/apply_functor.ma | 84 ++++++++++ .../contribs/formal_topology/overlap/depends | 16 +- .../o-basic_pairs_to_o-basic_topologies.ma | 149 ------------------ .../overlap/r-o-basic_pairs.ma | 107 +++++++++++++ 4 files changed, 200 insertions(+), 156 deletions(-) create mode 100644 helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma create mode 100644 helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma diff --git a/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma b/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma new file mode 100644 index 000000000..e10bd351c --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma @@ -0,0 +1,84 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "categories.ma". +include "notation.ma". + +record Fo (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) : Type2 ≝ { + F2: C2; + F1: C1; + FP: map_objs2 ?? F F1 =_\ID F2 +}. + +lemma REW : ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀X,Y:Fo ?? F. + arrows2 C2 (F (F1 ??? X)) (F (F1 ??? Y)) → + arrows2 C2 (F2 ??? X) (F2 ??? Y). +intros 5; cases X; cases Y; clear X Y; +cases H; cases H1; intros; assumption; +qed. + +record Fm_c (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) (X,Y:Fo ?? F) : Type2 ≝ { + Fm2: arrows2 C2 (F2 ??? X) (F2 ??? Y); + Fm1: arrows2 C1 (F1 ??? X) (F1 ??? Y); + FmP: REW ?? F X Y (map_arrows2 ?? F ?? Fm1) = Fm2 +}. + +definition Fm : + ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2. + Fo ?? F → Fo ?? F → setoid2. +intros (C1 C2 F X Y); constructor 1; [apply (Fm_c C1 C2 F X Y)] +constructor 1; [apply (λf,g.Fm2 ????? f =_2 Fm2 ????? g);] +[ intro; apply refl2; +| intros 3; apply sym2; assumption; +| intros 5; apply (trans2 ?? ??? x1 x2);] +qed. + +definition F_id : + ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀o.Fm ?? F o o. +intros; constructor 1; + [ apply (id2 C2 (F2 ??? o)); + | apply (id2 C1 (F1 ??? o)); + | cases o; cases H; simplify; apply (respects_id2 ?? F);] +qed. + +definition F_comp : + ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀o1,o2,o3. + binary_morphism2 (Fm ?? F o1 o2) (Fm ?? F o2 o3) (Fm ?? F o1 o3). +intros; constructor 1; +[ intros (f g); constructor 1; + [ apply (comp2 C2 ??? (Fm2 ????? f) (Fm2 ????? g)); + | apply (comp2 C1 ??? (Fm1 ????? f) (Fm1 ????? g)); + | apply hide; cases o1 in f; cases o2 in g; cases o3; clear o1 o2 o3; + cases H; cases H1; cases H2; intros 2; cases c; cases c1; clear c c1; + simplify; apply (.= (respects_comp2:?)); apply (e1‡e);] +| intros 6; change with + ((Fm2 C1 C2 F o2 o3 b∘Fm2 C1 C2 F o1 o2 a) = + (Fm2 C1 C2 F o2 o3 b'∘Fm2 C1 C2 F o1 o2 a')); + change in e1 with (Fm2 ?? F ?? b = Fm2 ?? F ?? b'); + change in e with (Fm2 ?? F ?? a = Fm2 ?? F ?? a'); + apply (e‡e1);] +qed. + + +definition Apply : ∀C1,C2: CAT2.arrows3 CAT2 C1 C2 → CAT2. +intros (C1 C2 F); +constructor 1; +[ apply (Fo ?? F); +| apply (Fm ?? F); +| apply F_id; +| apply F_comp; +| intros; apply (comp_assoc2 C2 ???? (Fm2 ????? a12) (Fm2 ????? a23) (Fm2 ????? a34)); +| intros; apply (id_neutral_right2 C2 ?? (Fm2 ????? a)); +| intros; apply (id_neutral_left2 C2 ?? (Fm2 ????? a));] +qed. diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends index f80fe592c..c6d981528 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/depends +++ b/helm/software/matita/contribs/formal_topology/overlap/depends @@ -1,24 +1,26 @@ -o-basic_pairs.ma o-algebra.ma +o-basic_pairs.ma notation.ma o-algebra.ma basic_pairs_to_basic_topologies.ma basic_pairs.ma basic_pairs_to_o-basic_pairs.ma basic_topologies.ma o-basic_pairs_to_o-basic_topologies.ma -o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma o-saturations.ma o-algebra.ma saturations.ma relations.ma +o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma basic_pairs.ma notation.ma relations.ma -o-algebra.ma categories.ma -o-formal_topologies.ma o-basic_topologies.ma formal_topologies.ma basic_topologies.ma +o-algebra.ma categories.ma categories.ma cprop_connectives.ma +o-formal_topologies.ma o-basic_topologies.ma saturations_to_o-saturations.ma o-saturations.ma relations_to_o-algebra.ma saturations.ma -basic_topologies.ma relations.ma saturations.ma subsets.ma categories.ma +basic_topologies.ma relations.ma saturations.ma concrete_spaces.ma basic_pairs.ma +r-o-basic_pairs.ma apply_functor.ma basic_pairs_to_o-basic_pairs.ma relations.ma subsets.ma concrete_spaces_to_o-concrete_spaces.ma basic_pairs_to_o-basic_pairs.ma concrete_spaces.ma o-concrete_spaces.ma o-basic_topologies.ma o-algebra.ma o-saturations.ma +notation.ma basic_topologies_to_o-basic_topologies.ma basic_topologies.ma o-basic_topologies.ma relations_to_o-algebra.ma basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma -notation.ma +apply_functor.ma categories.ma cprop_connectives.ma logic/connectives.ma relations_to_o-algebra.ma o-algebra.ma relations.ma -o-basic_pairs_to_o-basic_topologies.ma o-basic_pairs.ma o-basic_topologies.ma +o-basic_pairs_to_o-basic_topologies.ma notation.ma o-basic_pairs.ma o-basic_topologies.ma logic/connectives.ma 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 4971b8ef9..b2dfffd02 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 @@ -117,152 +117,3 @@ constructor 1; | intros 6; apply refl1;] qed. -axiom DDD : False. - -definition Fo := - λC1,C2: CAT2.λF:arrows3 CAT2 C1 C2. - (exT22 ? (λx:C2.exT22 ? (λy:C1.map_objs2 ?? F y =_\ID x))). - -definition sigma_equivalence_relation2: - ∀C2:CAT2.∀Q.∀X,Y:exT22 ? (λy:C2.Q y).∀P. - equivalence_relation2 (exT22 ? (λf:arrows2 C2 (\fst X) (\fst Y).P f)). -intros; constructor 1; - [ intros(F G); apply (\fst F =_2 \fst G); - | intro; apply refl2; - | intros 3; apply sym2; assumption; - | intros 5; apply (trans2 ?? ??? x1 x2);] -qed. - -lemma REW : ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀X,Y:Fo ?? F. - arrows2 C2 (F (\fst (\snd X))) (F (\fst (\snd Y))) → - arrows2 C2 (\fst X) (\fst Y). -intros 5; cases X; cases Y; cases x; cases x1; clear X Y x x1; -cases H; cases H1; intros; assumption; -qed. - -definition Fm : - ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2. - Fo ?? F → Fo ?? F → setoid2. -intros (C1 C2 F X Y); constructor 1; - [ apply (exT22 ? (λf:arrows2 C2 (\fst X) (\fst Y). - exT22 ? (λg:arrows2 C1 (\fst (\snd X)) (\fst (\snd Y)). - REW ?? F X Y (map_arrows2 ?? F ?? g) = f))); - | apply sigma_equivalence_relation2;] -qed. - -definition F_id : - ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀o.Fm ?? F o o. -intros; constructor 1; - [ apply (id2 C2 (\fst o)); - | exists[apply (id2 C1 (\fst (\snd o)))] - cases o; cases x; cases H; unfold hide; simplify; - apply (respects_id2 ?? F);] -qed. - -definition F_comp : - ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀o1,o2,o3. - binary_morphism2 (Fm ?? F o1 o2) (Fm ?? F o2 o3) (Fm ?? F o1 o3). -intros; constructor 1; -[ intros (f g); constructor 1; - [ apply (comp2 C2 (\fst o1) (\fst o2) (\fst o3) (\fst f) (\fst g)); - | exists[apply (comp2 C1 (\fst (\snd o1)) (\fst (\snd o2)) (\fst (\snd o3)) (\fst (\snd f)) (\fst (\snd g)))] - cases o1 in f; cases o2 in g; cases o3; clear o1 o2 o3; - cases x; cases x1; cases x2; clear x x1 x2; - cases H; cases H1; cases H2; simplify; intros 2; - cases c; cases c1; cases x; cases x1; clear x x1 c c1; simplify; - apply (.= (respects_comp2:?)); - apply (x3‡x2);] -| (* DISABILITARE INNERTYPES *) - STOP - cases x3; cases x2; - apply refl2; - simplify; - -definition Apply : ∀C1,C2: CAT2.arrows3 CAT2 C1 C2 → CAT2. -intros (C1 C2 F); -constructor 1; -[ apply (Fo ?? F); -| apply (Fm ?? F); -| apply F_id; -| apply F_comp; intros (o1 o2 o3); constructor 1; - [ intros (f g); whd in f g; constructor 1; - [ apply (comp2 C2 (\fst o1) (\fst o2) (\fst o3) (\fst f) (\fst g)); - | exists[apply (comp2 C1 (\fst (\snd o1)) (\fst (\snd o2)) (\fst (\snd o3)) (\fst (\snd f)) (\fst (\snd g)))] - cases o1; cases x; cases H; - -(* 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 - | .... - ] - - E : objs CATS === Σx.∃y. F y = x - - 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 - -*) - diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma new file mode 100644 index 000000000..bba466269 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma @@ -0,0 +1,107 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_pairs_to_o-basic_pairs.ma". +include "apply_functor.ma". + +definition rOBP ≝ Apply ?? BP_to_OBP. + +include "o-basic_pairs_to_o-basic_topologies.ma". + +lemma rOR_full : + ∀rS,rT:rOBP.∀f:arrows2 ? (OR (F2 ??? rS)) (OR (F2 ??? rT)). + exT22 ? (λg:arrows2 OBP (F1 ??? rS) (F1 ??? rT). + map_arrows2 ? ? OR rS rT g = f). + ∀S,T.∀f. exT22 ? (λg. map_arrows2 ? ? OR S T g = f). +arrows2 OBP S T +unary_morphism1_setoid1 (OR S) (OR T) + +(* Todo: rename BTop → OBTop *) + +(* 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 + | .... + ] + + E : objs CATS === Σx.∃y. F y = x + + 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