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 extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
  34  (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
  35  intros (X S r); constructor 1;
  36   [ intro F; constructor 1; constructor 1;
  37     [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
  38     | intros; split; intro; cases f (H1 H2); clear f; split;
  39        [ apply (. (H‡#)); assumption
  40        |3: apply (. (H\sup -1‡#)); assumption
  41        |2,4: cases H2 (w H3); exists; [1,3: apply w]
  42          [ apply (. (#‡(H‡#))); assumption
  43          | apply (. (#‡(H \sup -1‡#))); assumption]]]
  44   | intros; split; simplify; intros; cases f; cases H1; split;
  45      [1,3: assumption
  46      |2,4: exists; [1,3: apply w]
  47       [ apply (. (#‡H)‡#); assumption
  48       | apply (. (#‡H\sup -1)‡#); assumption]]]
  49 qed.
  50
  51 definition fintersects: ∀o: basic_pair. form o → form o → Ω \sup (form o).
  52  apply
  53   (λo: basic_pair.λa,b: form o.
  54     {c | ext ?? (rel o) c ⊆ ext ?? (rel o) a ∩ ext ?? (rel o) b });
  55  intros; simplify; apply (.= (†H)‡#); apply refl1.
  56 qed.
  57
  58 interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
  59
  60 definition fintersectsS:
  61  ∀o:basic_pair. Ω \sup (form o) → Ω \sup (form o) → Ω \sup (form o).
  62  apply (λo: basic_pair.λa,b: Ω \sup (form o).
  63   {c | ext ?? (rel o) c ⊆ extS ?? (rel o) a ∩ extS ?? (rel o) b });
  64  intros; simplify; apply (.= (†H)‡#); apply refl1.
  65 qed.
  66
  67 interpretation "fintersectsS" 'fintersects U V = (fintersectsS _ U V).
  68
  69 (*
  70 definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp.
  71
  72
  73  apply (λo:basic_pair.λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧
  74    (* OK: FunClass_2_OF_binary_relation (concr o) (form o) (rel o) x y *)
  75    ?);
  76    change in x with (carr1 (setoid1_of_setoid (concr o)));
  77    apply (FunClass_2_OF_binary_relation ?? (rel ?) x y);
  78 x ⊩ y);
  79
  80  rel (concr o) o -> binary_relation ...
  81  rel ? = seotid1_OF_setoid ?
  82  carr rel ? = Type_OF_objs1 (concr o) ->
  83          carr (setoid1_of_REL (concr o))
  84
  85 interpretation "basic pair relation for subsets" 'Vdash2 x y = (relS _ x y).
  86 interpretation "basic pair relation for subsets (non applied)" 'Vdash = (relS _).
  87
  88 record concrete_space : Type ≝
  89  { bp:> basic_pair;
  90    converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
  91    all_covered: ∀x: concr bp. x ⊩ form bp
  92  }.
  93
  94 record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
  95  { rp:> relation_pair CS1 CS2;
  96    respects_converges:
  97     ∀b,c.
  98      extS ?? rp \sub\c (extS ?? (rel CS2) (b ↓ c)) =
  99      extS ?? (rel CS1) ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
 100    respects_all_covered:
 101     extS ?? rp\sub\c (extS ?? (rel CS2) (form CS2)) =
 102     extS ?? (rel CS1) (form CS1)
 103  }.
 104
 105 definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid.
 106  intros;
 107  constructor 1;
 108   [ apply (convergent_relation_pair c c1)
 109   | constructor 1;
 110      [ intros;
 111        apply (relation_pair_equality c c1 c2 c3);
 112      | intros 1; apply refl;
 113      | intros 2; apply sym;
 114      | intros 3; apply trans]]
 115 qed.
 116
 117 lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id ? o) X = X.
 118  intros;
 119  unfold extS;
 120  split;
 121   [ intros 2;
 122     cases m; clear m;
 123     cases H; clear H;
 124     cases H1; clear H1;
 125     whd in H;
 126     apply (eq_elim_r'' ????? H);
 127     assumption
 128   | intros 2;
 129     constructor 1;
 130      [ whd; exact I
 131      | exists; [ apply a ]
 132        split;
 133         [ assumption
 134         | whd; constructor 1]]]
 135 qed.
 136
 137 definition CSPA: category.
 138  constructor 1;
 139   [ apply concrete_space
 140   | apply convergent_relation_space_setoid
 141   | intro; constructor 1;
 142      [ apply id
 143      | intros;
 144        unfold id; simplify;
 145        apply (.= (equalset_extS_id_X_X ??));
 146
 147      |
 148      ]
 149   |*)