helm/software/matita/library/formal_topology/basic_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 "formal_topology/relations.ma".
  16 include "datatypes/categories.ma".
  17
  18 definition is_saturation ≝
  19  λC:REL.λA:unary_morphism (Ω \sup C) (Ω \sup C).
  20   ∀U,V. (U ⊆ A V) = (A U ⊆ A V).
  21
  22 definition is_reduction ≝
  23  λC:REL.λJ:unary_morphism (Ω \sup C) (Ω \sup C).
  24   ∀U,V. (J U ⊆ V) = (J U ⊆ J V).
  25
  26 record basic_topology: Type ≝
  27  { carrbt:> REL;
  28    A: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt);
  29    J: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt);
  30    A_is_saturation: is_saturation ? A;
  31    J_is_reduction: is_reduction ? J;
  32    compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V)
  33  }.
  34
  35 (* the same as ⋄ for a basic pair *)
  36 definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
  37  intros; constructor 1;
  38   [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S});
  39     intros; simplify; split; intro; cases H1; exists [1,3: apply w]
  40      [ apply (. (#‡H)‡#); assumption
  41      | apply (. (#‡H \sup -1)‡#); assumption]
  42   | intros; split; simplify; intros; cases H2; exists [1,3: apply w]
  43      [ apply (. #‡(#‡H1)); cases x; split; try assumption;
  44        apply (if ?? (H ??)); assumption
  45      | apply (. #‡(#‡H1 \sup -1)); cases x; split; try assumption;
  46        apply (if ?? (H \sup -1 ??)); assumption]]
  47 qed.
  48
  49 (* the same as □ for a basic pair *)
  50 definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
  51  intros; constructor 1;
  52   [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S});
  53     intros; simplify; split; intros; apply H1;
  54      [ apply (. #‡H \sup -1); assumption
  55      | apply (. #‡H); assumption]
  56   | intros; split; simplify; intros; [ apply (. #‡H1); | apply (. #‡H1 \sup -1)]
  57     apply H2; [ apply (if ?? (H \sup -1 ??)); | apply (if ?? (H ??)) ] assumption]
  58 qed.
  59
  60 (* minus_image is the same as ext *)
  61
  62 theorem image_id: ∀o,U. image o o (id1 REL o) U = U.
  63  intros; unfold image; simplify; split; simplify; intros;
  64   [ change with (a ∈ U);
  65     cases H; cases x; change in f with (eq1 ? w a); apply (. f‡#); assumption
  66   | change in f with (a ∈ U);
  67     exists; [apply a] split; [ change with (a = a); apply refl | assumption]]
  68 qed.
  69
  70 theorem minus_star_image_id: ∀o,U. minus_star_image o o (id1 REL o) U = U.
  71  intros; unfold minus_star_image; simplify; split; simplify; intros;
  72   [ change with (a ∈ U); apply H; change with (a=a); apply refl
  73   | change in f1 with (eq1 ? x a); apply (. f1 \sup -1‡#); apply f]
  74 qed.
  75
  76 theorem image_comp: ∀A,B,C,r,s,X. image A C (r ∘ s) X = image B C r (image A B s X).
  77  intros; unfold image; simplify; split; simplify; intros; cases H; clear H; cases x;
  78  clear x; [ cases f; clear f; | cases f1; clear f1 ]
  79  exists; try assumption; cases x; clear x; split; try assumption;
  80  exists; try assumption; split; assumption.
  81 qed.
  82
  83 theorem minus_star_image_comp:
  84  ∀A,B,C,r,s,X.
  85   minus_star_image A C (r ∘ s) X = minus_star_image B C r (minus_star_image A B s X).
  86  intros; unfold minus_star_image; simplify; split; simplify; intros; whd; intros;
  87   [ apply H; exists; try assumption; split; assumption
  88   | change with (x ∈ X); cases f; cases x1; apply H; assumption]
  89 qed.
  90
  91 record continuous_relation (S,T: basic_topology) : Type ≝
  92  { cont_rel:> arrows1 ? S T;
  93    reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U);
  94    saturated: ∀U. U = A ? U → minus_star_image ?? cont_rel U = A ? (minus_star_image ?? cont_rel U)
  95  }.
  96
  97 definition continuous_relation_setoid: basic_topology → basic_topology → setoid1.
  98  intros (S T); constructor 1;
  99   [ apply (continuous_relation S T)
 100   | constructor 1;
 101      [ apply (λr,s:continuous_relation S T.∀b. A ? (ext ?? r b) = A ? (ext ?? s b));
 102      | simplify; intros; apply refl1;
 103      | simplify; intros; apply sym1; apply H
 104      | simplify; intros; apply trans1; [2: apply H |3: apply H1; |1: skip]]]
 105 qed.
 106
 107 definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel.
 108
 109 coercion cont_rel'.
 110
 111 (*
 112 definition BTop: category1.
 113  constructor 1;
 114   [ apply basic_topology
 115   | apply continuous_relation_setoid
 116   | intro; constructor 1;
 117      [ apply id1
 118      | intros;
 119        apply (.= (image_id ??));
 120        apply sym1;
 121        apply (.= †(image_id ??));
 122        apply sym1;
 123        assumption
 124      | intros;
 125        apply (.= (minus_star_image_id ??));
 126        apply sym1;
 127        apply (.= †(minus_star_image_id ??));
 128        apply sym1;
 129        assumption]
 130   | intros; constructor 1;
 131      [ intros (r s); constructor 1;
 132         [ apply (s ∘ r)
 133         | intros;
 134           apply sym1;
 135           apply (.= †(image_comp ??????));
 136           apply (.= (reduced ?????)\sup -1);
 137            [ apply (.= (reduced ?????)); [ assumption | apply refl1 ]
 138            | apply (.= (image_comp ??????)\sup -1);
 139              apply refl1]
 140         | intros;
 141           apply sym1;
 142           apply (.= †(minus_star_image_comp ??????));
 143           apply (.= (saturated ?????)\sup -1);
 144            [ apply (.= (saturated ?????)); [ assumption | apply refl1 ]
 145            | apply (.= (minus_star_image_comp ??????)\sup -1);
 146              apply refl1]]
 147      | intros; simplify; intro; simplify; whd in H H1;
 148        apply (.= †(ext_comp ???));
 149      ]
 150   | intros; simplify; intro; simplify;
 151     apply (.= †(ASSOC1‡#));
 152     apply refl1
 153   | intros; simplify; intro; simplify;
 154     apply (.= †((id_neutral_right1 ????)‡#));
 155     apply refl1
 156   | intros; simplify; intro; simplify;
 157     apply (.= †((id_neutral_left1 ????)‡#));
 158     apply refl1]
 159 qed.*)