X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fformal_topologies.ma;h=f47323e000f2fea00e57e3e29d7a8d15e643a34e;hb=a99fe3ca5a39b4d9754b69863b5f9fb0f91ed286;hp=e29ba16f7dd1f156c2480d74ea8a0583f80a7e0d;hpb=2afec2cc82077163425701cc02ffb719a6345fb6;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/formal_topologies.ma b/helm/software/matita/library/formal_topology/formal_topologies.ma
index e29ba16f7..f47323e00 100644
--- a/helm/software/matita/library/formal_topology/formal_topologies.ma
+++ b/helm/software/matita/library/formal_topology/formal_topologies.ma
@@ -24,7 +24,7 @@ coercion btop_carr'.
 
 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
  intros; constructor 1;
-  [ apply (λU:Ω \sup S.{a | ∃b. b ∈ U ∧ a ∈ A ? (singleton ? b)});
+  [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
     intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
     split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
   | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
@@ -41,7 +41,81 @@ qed.
 
 interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
 
-record formal_topology : Type ≝
+record formal_topology: Type ≝
  { bt:> BTop;
    converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
- }.
\ No newline at end of file
+ }.
+
+definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
+
+coercion bt'.
+
+definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
+ intros; constructor 1;
+  [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
+  | intros; apply (.= (†H)‡(†H1)); apply refl1]
+qed.
+
+interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
+
+record formal_map (S,T: formal_topology) : Type ≝
+ { cr:> continuous_relation_setoid S T;
+   C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
+   C2: extS ?? cr T = S
+ }.
+
+definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
+ λFT1,FT2,c. cr FT1 FT2 c.
+
+coercion cr'.
+
+definition formal_map_setoid: formal_topology → formal_topology → setoid1.
+ intros (S T); constructor 1;
+  [ apply (formal_map S T);
+  | constructor 1;
+     [ apply (λf,f1: formal_map S T.f=f1);
+     | simplify; intros 1; apply refl1
+     | simplify; intros 2; apply sym1
+     | simplify; intros 3; apply trans1]]
+qed.
+
+definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
+ λFT1,FT2,c.cr ?? c.
+
+coercion cr''.
+
+definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
+ λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
+
+coercion cr'''.
+
+axiom C1':
+ ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
+  extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
+
+definition formal_map_composition:
+ ∀o1,o2,o3: formal_topology.
+  binary_morphism1
+   (formal_map_setoid o1 o2)
+   (formal_map_setoid o2 o3)
+   (formal_map_setoid o1 o3).
+ intros; constructor 1;
+  [ intros; whd in c c1; constructor 1;
+     [ apply (comp1 BTop ??? c c1);
+     | intros;
+       apply (.= (extS_com ??? c c1 ?));
+       apply (.= †(C1 ?????));
+       apply (.= (C1' ?????));
+       apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
+       apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
+       apply (.= (extS_singleton ????)‡(extS_singleton ????));
+       apply refl1;
+     | apply (.= (extS_com ??? c c1 ?));
+       apply (.= (†(C2 ???)));
+       apply (.= (C2 ???));
+       apply refl1;]
+  | intros; simplify;
+    change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
+    apply prop1; assumption]
+qed.
+