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 "o-basic_topologies.ma".
17 definition btop_carr: BTop → Type ≝ λo:BTop. carr1 (oa_P (carrbt o)).
21 definition btop_carr': BTop → setoid1 ≝ λo:BTop. carrbt o.
25 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
26 intros; constructor 1;
27 [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
28 intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
29 split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
30 | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
31 try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
34 interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
36 definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
37 intros; constructor 1;
38 [ apply (λU,V. ↓U ∩ ↓V);
39 | intros; apply (.= (†H)‡(†H1)); apply refl1]
42 interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
45 record formal_topology: Type ≝
47 converges: ∀U,V: bt. A ? (U ↓ V) = (A ? U ∧ A ? V)
51 definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
55 definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
56 intros; constructor 1;
57 [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
58 | intros; apply (.= (†H)‡(†H1)); apply refl1]
61 interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
63 record formal_map (S,T: formal_topology) : Type ≝
64 { cr:> continuous_relation_setoid S T;
65 C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
69 definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
70 λFT1,FT2,c. cr FT1 FT2 c.
74 definition formal_map_setoid: formal_topology → formal_topology → setoid1.
75 intros (S T); constructor 1;
76 [ apply (formal_map S T);
78 [ apply (λf,f1: formal_map S T.f=f1);
79 | simplify; intros 1; apply refl1
80 | simplify; intros 2; apply sym1
81 | simplify; intros 3; apply trans1]]
84 definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
89 definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
90 λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
95 ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
96 extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
98 definition formal_map_composition:
99 ∀o1,o2,o3: formal_topology.
101 (formal_map_setoid o1 o2)
102 (formal_map_setoid o2 o3)
103 (formal_map_setoid o1 o3).
104 intros; constructor 1;
105 [ intros; whd in c c1; constructor 1;
106 [ apply (comp1 BTop ??? c c1);
108 apply (.= (extS_com ??? c c1 ?));
109 apply (.= †(C1 ?????));
110 apply (.= (C1' ?????));
111 apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
112 apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
113 apply (.= (extS_singleton ????)‡(extS_singleton ????));
115 | apply (.= (extS_com ??? c c1 ?));
116 apply (.= (†(C2 ???)));
120 change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
121 apply prop1; assumption]