include "basic_pairs_to_o-basic_pairs.ma".
include "apply_functor.ma".
-definition rOBP ≝ Apply ?? BP_to_OBP.
+definition rOBP ≝ Apply (category2_of_category1 BP) OBP BP_to_OBP.
include "o-basic_pairs_to_o-basic_topologies.ma".
+lemma category2_of_category1_respects_comp_r:
+ ∀C:category1.∀o1,o2,o3:C.
+ ∀f:arrows1 ? o1 o2.∀g:arrows1 ? o2 o3.
+ (comp1 ???? f g) =_\ID (comp2 (category2_of_category1 C) o1 o2 o3 f g).
+ intros; constructor 1;
+qed.
+
+lemma category2_of_category1_respects_comp:
+ ∀C:category1.∀o1,o2,o3:C.
+ ∀f:arrows1 ? o1 o2.∀g:arrows1 ? o2 o3.
+ (comp2 (category2_of_category1 C) o1 o2 o3 f g) =_\ID (comp1 ???? f g).
+ intros; constructor 1;
+qed.
+
+lemma POW_full':
+ ∀S,T:REL.∀f:arrows2 SET1 (POW S) (POW T).
+ arrows1 REL S T.
+ intros;
+ constructor 1; constructor 1;
+ [ intros (x y); apply (y ∈ c {(x)});
+ | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
+ apply (e1ࠠe); ]
+qed.
+
+(*
+lemma POW_full_image:
+ ∀S,T:REL.∀f:arrows2 SET1 (POW S) (POW T).
+ exT22 ? (λg:arrows1 REL S T.or_f ?? (map_arrows2 ?? POW S T g) = f).
+ intros; letin g ≝ (? : carr1 (arrows1 REL S T)); [
+ constructor 1; constructor 1;
+ [ intros (x y); apply (y ∈ f {(x)});
+ | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
+ apply (e1ࠠe); ]]
+exists [apply g]
+intro; split; intro; simplify; intro;
+[ whd in f1; change in f1:(? ? (λ_:?.? ? ? ? ? % ?)) with (a1 ∈ f {(x)});
+ cases f1; cases x; clear f1 x; change with (a1 ∈ f a);
+ lapply (f_image_monotone ?? (map_arrows2 ?? POW S T g) (singleton ? w) a ? a1);
+ [2: whd in Hletin;
+ change in Hletin:(? ? (λ_:?.? ? ? ? ? % ?))
+ with (a1 ∈ f {(x)}); cases Hletin; cases x;
+ [ intros 2; change in f3 with (eq1 ? w a2); change with (a2 ∈ a);
+ apply (. f3^-1‡#); assumption;
+ | assumption; ]
+
+
+
+ lapply (. (or_prop3 ?? (map_arrows2 ?? POW S T g) (singleton ? a1) a)^-1);
+ [ whd in Hletin:(? ? ? ? ? ? %);
+ change in Hletin:(? ? ? ? ? ? (? ? (? ? ? (λ_:?.? ? (λ_:?.? ? ? ? ? % ?)) ?)))
+ with (y ∈ f {(x)});
+ cases Hletin; cases x1; cases x2;
+
+ [ cases Hletin; change in x with (eq1 ? a1 w1); apply (. x‡#); assumption;
+ | exists; [apply w] assumption ]
+
+
+ clear g;
+ cases f1; cases x; simplify in f2; change with (a1 ∈ (f a));
+ lapply depth=0 (let x ≝ POW in or_prop3 (POW S) (POW T) (map_arrows2 ?? POW S T g));
+ lapply (Hletin {(w)} {(a1)}).
+ lapply (if ?? Hletin1); [2: clear Hletin Hletin1;
+ exists; [apply a1] [whd; exists[apply w] split; [assumption;|change with (w = w); apply rule #]]
+ change with (a1=a1); apply rule #;]
+ clear Hletin Hletin1; cases Hletin2; whd in x2;
+qed.
+*)
+lemma curry: ∀A,B,C.binary_morphism1 A B C → A → B ⇒ C.
+ intros;
+ constructor 1;
+ [ apply (b c);
+ | intros; apply (#‡e); ]
+qed.
+
+notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
+interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
+
+definition preserve_sup : ∀S,T.∀ f:Ω \sup S ⇒ Ω \sup T. CProp1.
+intros (S T f); apply (∀X:Ω \sup S. (f X) = ?);
+constructor 1; constructor 1;
+[ intro y; alias symbol "singl" = "singleton". alias symbol "and" = "and_morphism".
+ apply (∃x:S. x ∈ X ∧ y ∈ f {(x)});
+| intros (a b H); split; intro E; cases E; clear E; exists; [1,3:apply w]
+ [ apply (. #‡(H^-1‡#)); | apply (. #‡(H‡#));] assumption]
+qed.
+
+alias symbol "singl" = "singleton".
+lemma eq_cones_to_eq_rel:
+ ∀S,T. ∀f,g: arrows1 REL S T.
+ (∀x. curry ??? (image ??) f {(x)} = curry ??? (image ??) g {(x)}) → f = g.
+intros; intros 2 (a b); split; intro;
+[ cases (f1 a); lapply depth=0 (s b); clear s s1;
+ lapply (Hletin); clear Hletin;
+ [ cases Hletin1; cases x; change in f4 with (a = w);
+ change with (a ♮g b); apply (. f4‡#); assumption;
+ | exists; [apply a] split; [ assumption | change with (a=a); apply rule #;]]
+| cases (f1 a); lapply depth=0 (s1 b); clear s s1;
+ lapply (Hletin); clear Hletin;
+ [ cases Hletin1; cases x; change in f4 with (a = w);
+ change with (a ♮f b); apply (. f4‡#); assumption;
+ | exists; [apply a] split; [ assumption | change with (a=a); apply rule #;]]]
+qed.
+
+variant eq_cones_to_eq_rel':
+ ∀S,T. ∀f,g: arrows1 REL S T.
+ (∀x:S. or_f ?? (map_arrows2 ?? POW S T f) {(x)} = or_f ?? (map_arrows2 ?? POW S T g) {(x)}) →
+ f = g
+≝ eq_cones_to_eq_rel.
+
lemma rOR_full :
- ∀rS,rT:rOBP.∀f:arrows2 BTop (OR (ℱ_2 rS)) (OR (ℱ_2 rT)).
- exT22 ? (λg:arrows2 rOBP rS rT.
- map_arrows2 ?? OR ?? (ℳ_2 g) = f).
-intros; cases f (c H1 H2); simplify;
+ ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
+ exT22 ? (λg:arrows2 rOBP s t.
+ map_arrows2 ?? OR ?? (ℳ_2 g) = f).
+intros 2 (s t); cases s (s_2 s_1 s_eq); clear s;
+change in match (F2 ??? (mk_Fo ??????)) with s_2;
+cases s_eq; clear s_eq s_2;
+letin s1 ≝ (BP_to_OBP s_1); change in match (BP_to_OBP s_1) with s1;
+cases t (t_2 t_1 t_eq); clear t;
+change in match (F2 ??? (mk_Fo ??????)) with t_2;
+cases t_eq; clear t_eq t_2;
+letin t1 ≝ (BP_to_OBP t_1); change in match (BP_to_OBP t_1) with t1;
+whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
+intro; whd in s_1 t_1;
+letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1)));
+[2:
+ exists;
+ [ constructor 1;
+ [2: simplify; apply R;
+ | simplify; apply (fun12 ?? (map_arrows2 ?? BP_to_OBP s_1 t_1)); apply R;
+ | simplify; apply rule #; ]]
+ simplify;
+|1: constructor 1;
+ [2: apply (pi1exT22 ?? (POW_full (form s_1) (form t_1) f));
+ |1: letin u ≝ (or_f_star ?? (map_arrows2 ?? POW (concr t_1) (form t_1) (⊩ \sub t_1)));
+ letin r ≝ (u ∘ (or_f ?? f));
+ letin xxx ≝ (or_f ?? (map_arrows2 ?? POW (concr s_1) (form s_1) (⊩ \sub s_1)));
+ letin r' ≝ (r ∘ xxx); clearbody r';
+ apply (POW_full' (concr s_1) (concr t_1) r');
+ | simplify in ⊢ (? ? ? (? ? ? ? ? % ?) ?);
+ apply eq_cones_to_eq_rel'; intro;
+ apply
+ (cic:/matita/logic/equality/eq_elim_r''.con ?????
+ (category2_of_category1_respects_comp_r : ?));
+ apply rule (.= (#‡#));
+ apply (.= (respects_comp2 ?? POW (concr s_1) (concr t_1) (form t_1) ? (⊩\sub t_1))‡#);
+ apply sym2;
+ apply (.= (respects_comp2 ?? POW (concr s_1) (form s_1) (form t_1) (⊩\sub s_1) (pi1exT22 ?? (POW_full (form s_1) (form t_1) (Ocont_rel ?? f)))));
+ apply (let H ≝(\snd (POW_full (form s_1) (form t_1) (Ocont_rel ?? f))) in .= #‡H);
+ apply sym2;
+ ]
+
STOP;
3. Definire la funzione
Apply:
- \forall C1,C2: CAT2. F: arrows3 CAT2 C1 C2 -> CAT2
- :=
+ ∀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
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 ]
+ [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.
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).
+ basta prendere (OR ∘ 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'
projects / helm.git / blobdiff