helm/software/matita/contribs/formal_topology/overlap/o-formal_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_topologies.ma".
  16
  17 (*
  18 definition btop_carr': BTop → setoid1 ≝ λo:BTop. carrbt o.
  19
  20 coercion btop_carr'.
  21
  22 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
  23  intros; constructor 1;
  24   [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
  25     intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
  26     split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
  27   | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
  28     try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
  29 qed.
  30
  31 interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
  32
  33 definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
  34  intros; constructor 1;
  35   [ apply (λU,V. ↓U ∩ ↓V);
  36   | intros; apply (.= (†H)‡(†H1)); apply refl1]
  37 qed.
  38
  39 interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
  40 *)
  41
  42 record formal_topology: Type ≝
  43  { bt:> BTop;
  44    converges: ∀U,V: bt. A ? (U ↓ V) = (A ? U ∧ A ? V)
  45  }.
  46
  47 (*
  48 definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
  49
  50 coercion bt'.
  51
  52 definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
  53  intros; constructor 1;
  54   [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
  55   | intros; apply (.= (†H)‡(†H1)); apply refl1]
  56 qed.
  57
  58 interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
  59 *)
  60 record formal_map (S,T: formal_topology) : Type ≝
  61  { cr:> continuous_relation_setoid S T;
  62    C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
  63    C2: extS ?? cr T = S
  64  }.
  65
  66 definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
  67  λFT1,FT2,c. cr FT1 FT2 c.
  68
  69 coercion cr'.
  70
  71 definition formal_map_setoid: formal_topology → formal_topology → setoid1.
  72  intros (S T); constructor 1;
  73   [ apply (formal_map S T);
  74   | constructor 1;
  75      [ apply (λf,f1: formal_map S T.f=f1);
  76      | simplify; intros 1; apply refl1
  77      | simplify; intros 2; apply sym1
  78      | simplify; intros 3; apply trans1]]
  79 qed.
  80
  81 definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
  82  λFT1,FT2,c.cr ?? c.
  83
  84 coercion cr''.
  85
  86 definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
  87  λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
  88
  89 coercion cr'''.
  90
  91 axiom C1':
  92  ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
  93   extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
  94
  95 definition formal_map_composition:
  96  ∀o1,o2,o3: formal_topology.
  97   binary_morphism1
  98    (formal_map_setoid o1 o2)
  99    (formal_map_setoid o2 o3)
 100    (formal_map_setoid o1 o3).
 101  intros; constructor 1;
 102   [ intros; whd in c c1; constructor 1;
 103      [ apply (comp1 BTop ??? c c1);
 104      | intros;
 105        apply (.= (extS_com ??? c c1 ?));
 106        apply (.= †(C1 ?????));
 107        apply (.= (C1' ?????));
 108        apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
 109        apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
 110        apply (.= (extS_singleton ????)‡(extS_singleton ????));
 111        apply refl1;
 112      | apply (.= (extS_com ??? c c1 ?));
 113        apply (.= (†(C2 ???)));
 114        apply (.= (C2 ???));
 115        apply refl1;]
 116   | intros; simplify;
 117     change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
 118     apply prop1; assumption]
 119 qed.
 120