helm/software/matita/library/formal_topology/concrete_spaces.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 "formal_topology/basic_pairs.ma".
  16
  17 definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b.
  18  apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x});
  19  intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1.
  20 qed.
  21
  22 interpretation "subset comprehension" 'comprehension s p =
  23  (comprehension s (mk_unary_morphism __ p _)).
  24
  25 definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
  26  apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
  27   [ intros; simplify; apply (.= (H‡#)); apply refl1
  28   | intros; simplify; split; intros; simplify; intros;
  29      [ apply (. #‡(#‡H)); assumption
  30      | apply (. #‡(#‡H\sup -1)); assumption]]
  31 qed.
  32
  33 definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o) ≝ λo.ext ? ? (rel o).
  34
  35 definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
  36  (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
  37  intros (X S r); constructor 1;
  38   [ intro F; constructor 1; constructor 1;
  39     [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
  40     | intros; split; intro; cases f (H1 H2); clear f; split;
  41        [ apply (. (H‡#)); assumption
  42        |3: apply (. (H\sup -1‡#)); assumption
  43        |2,4: cases H2 (w H3); exists; [1,3: apply w]
  44          [ apply (. (#‡(H‡#))); assumption
  45          | apply (. (#‡(H \sup -1‡#))); assumption]]]
  46   | intros; split; simplify; intros; cases f; cases H1; split;
  47      [1,3: assumption
  48      |2,4: exists; [1,3: apply w]
  49       [ apply (. (#‡H)‡#); assumption
  50       | apply (. (#‡H\sup -1)‡#); assumption]]]
  51 qed.
  52
  53 definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
  54  λo.extS ?? (rel o).
  55
  56 definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
  57  intros (o); constructor 1;
  58   [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
  59     intros; simplify; apply (.= (†H)‡#); apply refl1
  60   | intros; split; simplify; intros;
  61      [ apply (. #‡((†H)‡(†H1))); assumption
  62      | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
  63 qed.
  64
  65 interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
  66
  67 definition fintersectsS:
  68  ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
  69  intros (o); constructor 1;
  70   [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
  71     intros; simplify; apply (.= (†H)‡#); apply refl1
  72   | intros; split; simplify; intros;
  73      [ apply (. #‡((†H)‡(†H1))); assumption
  74      | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
  75 qed.
  76
  77 interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
  78
  79 definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
  80  intros (o); constructor 1;
  81   [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y);
  82   | intros; split; intros; cases H2; exists [1,3: apply w]
  83      [ apply (. (#‡H1)‡(H‡#)); assumption
  84      | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]]
  85 qed.
  86
  87 interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y).
  88 interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
  89
  90 record concrete_space : Type ≝
  91  { bp:> BP;
  92    converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
  93    all_covered: ∀x: concr bp. x ⊩ form bp
  94  }.
  95
  96 definition bp': concrete_space → basic_pair ≝ λc.bp c.
  97
  98 coercion bp'.
  99
 100 record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
 101  { rp:> arrows1 ? CS1 CS2;
 102    respects_converges:
 103     ∀b,c.
 104      extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
 105      BPextS CS1 ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
 106    respects_all_covered:
 107     extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1)
 108  }.
 109
 110 definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝
 111  λCS1,CS2,c. rp CS1 CS2 c.
 112
 113 coercion rp'.
 114
 115 definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1.
 116  intros;
 117  constructor 1;
 118   [ apply (convergent_relation_pair c c1)
 119   | constructor 1;
 120      [ intros;
 121        apply (relation_pair_equality c c1 c2 c3);
 122      | intros 1; apply refl1;
 123      | intros 2; apply sym1;
 124      | intros 3; apply trans1]]
 125 qed.
 126
 127 definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝
 128  λCS1,CS2,c.rp ?? c.
 129
 130 coercion rp''.
 131
 132 lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
 133  intros;
 134  unfold extS; simplify;
 135  split; simplify;
 136   [ intros 2; change with (a ∈ X);
 137     cases f; clear f;
 138     cases H; clear H;
 139     cases x; clear x;
 140     change in f2 with (eq1 ? a w);
 141     apply (. (f2\sup -1‡#));
 142     assumption
 143   | intros 2; change in f with (a ∈ X);
 144     split;
 145      [ whd; exact I
 146      | exists; [ apply a ]
 147        split;
 148         [ assumption
 149         | change with (a = a); apply refl]]]
 150 qed.
 151
 152 lemma extS_id: ∀o:BP.∀X.extS (concr o) (concr o) (id1 ? o) \sub \c X = X.
 153  intros;
 154  unfold extS; simplify;
 155  split; simplify; intros;
 156   [ change with (a ∈ X);
 157     cases f; cases H; cases x; change in f3 with (eq1 ? a w);
 158     apply (. (f3\sup -1‡#));
 159     assumption
 160   | change in f with (a ∈ X);
 161     split;
 162      [ apply I
 163      | exists; [apply a]
 164        split; [ assumption | change with (a = a); apply refl]]]
 165 qed.
 166
 167 lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c1 ∘ c2) S = extS o1 o2 c1 (extS o2 o3 c2 S).
 168  intros; unfold extS; simplify; split; intros; simplify; intros;
 169   [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
 170     cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6;
 171     exists; [apply w1] split [2: assumption] constructor 1; [assumption]
 172     exists; [apply w] split; assumption
 173   | cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
 174     cases H3 (H4 H5); cases H4 (w1 H6); clear H3 H4; cases H6 (w2 H7); clear H6;
 175     cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split;
 176     assumption]
 177 qed.
 178
 179 definition convergent_relation_space_composition:
 180  ∀o1,o2,o3: concrete_space.
 181   binary_morphism1
 182    (convergent_relation_space_setoid o1 o2)
 183    (convergent_relation_space_setoid o2 o3)
 184    (convergent_relation_space_setoid o1 o3).
 185  intros; constructor 1;
 186      [ intros; whd in c c1 ⊢ %;
 187        constructor 1;
 188         [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
 189         | intros;
 190           change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c);
 191           change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
 192             with (c \sub \f ∘ c1 \sub \f);
 193           change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
 194             with (c \sub \f ∘ c1 \sub \f);
 195           apply (.= (extS_com ??????));
 196           apply (.= (†(respects_converges ?????)));
 197           apply (.= (respects_converges ?????));
 198           apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
 199           apply refl1;
 200         | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c);
 201           apply (.= (extS_com ??????));
 202           apply (.= (†(respects_all_covered ???)));
 203           apply (.= respects_all_covered ???);
 204           apply refl1]
 205      | intros;
 206        change with (a ∘ b = a' ∘ b');
 207        change in H with (rp'' ?? a = rp'' ?? a');
 208        change in H1 with (rp'' ?? b = rp ?? b');
 209        apply (.= (H‡H1));
 210        apply refl1]
 211 qed.
 212
 213 definition CSPA: category1.
 214  constructor 1;
 215   [ apply concrete_space
 216   | apply convergent_relation_space_setoid
 217   | intro; constructor 1;
 218      [ apply id1
 219      | intros;
 220        unfold id; simplify;
 221        apply (.= (equalset_extS_id_X_X ??));
 222        apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡
 223                     (equalset_extS_id_X_X ??)\sup -1)));
 224        apply refl1;
 225      | apply (.= (extS_id ??));
 226        apply refl1]
 227   | apply convergent_relation_space_composition
 228   | intros; simplify;
 229     change with ((a12 ∘ a23) ∘ a34 = a12 ∘ (a23 ∘ a34));
 230     apply (.= ASSOC1);
 231     apply refl1
 232   | intros; simplify;
 233     change with (id1 ? o1 ∘ a = a);
 234     apply (.= id_neutral_left1 ????);
 235     apply refl1
 236   | intros; simplify;
 237     change with (a ∘ id1 ? o2 = a);
 238     apply (.= id_neutral_right1 ????);
 239     apply refl1]
 240 qed.