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 theorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S.
  27  intros 4; assumption.
  28 qed.
  29
  30 theorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
  31  intros; apply transitive_subseteq_operator; [apply S2] assumption.
  32 qed.
  33
  34 theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ⊆ A U.
  35  intros; apply (fi ?? (H ??)); apply subseteq_refl.
  36 qed.
  37
  38 theorem saturation_monotone:
  39  ∀C,A. is_saturation C A →
  40   ∀U,V. U ⊆ V → A U ⊆ A V.
  41  intros; apply (if ?? (H ??)); apply subseteq_trans; [apply V|3: apply saturation_expansive ]
  42  assumption.
  43 qed.
  44
  45 theorem saturation_idempotent: ∀C,A. is_saturation C A → ∀U. A (A U) = A U.
  46  intros; split;
  47   [ apply (if ?? (H ??)); apply subseteq_refl
  48   | apply saturation_expansive; assumption]
  49 qed.
  50
  51 record basic_topology: Type ≝
  52  { carrbt:> REL;
  53    A: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt);
  54    J: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt);
  55    A_is_saturation: is_saturation ? A;
  56    J_is_reduction: is_reduction ? J;
  57    compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V)
  58  }.
  59
  60 (* the same as ⋄ for a basic pair *)
  61 definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
  62  intros; constructor 1;
  63   [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S});
  64     intros; simplify; split; intro; cases H1; exists [1,3: apply w]
  65      [ apply (. (#‡H)‡#); assumption
  66      | apply (. (#‡H \sup -1)‡#); assumption]
  67   | intros; split; simplify; intros; cases H2; exists [1,3: apply w]
  68      [ apply (. #‡(#‡H1)); cases x; split; try assumption;
  69        apply (if ?? (H ??)); assumption
  70      | apply (. #‡(#‡H1 \sup -1)); cases x; split; try assumption;
  71        apply (if ?? (H \sup -1 ??)); assumption]]
  72 qed.
  73
  74 (* the same as □ for a basic pair *)
  75 definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
  76  intros; constructor 1;
  77   [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S});
  78     intros; simplify; split; intros; apply H1;
  79      [ apply (. #‡H \sup -1); assumption
  80      | apply (. #‡H); assumption]
  81   | intros; split; simplify; intros; [ apply (. #‡H1); | apply (. #‡H1 \sup -1)]
  82     apply H2; [ apply (if ?? (H \sup -1 ??)); | apply (if ?? (H ??)) ] assumption]
  83 qed.
  84
  85 (* minus_image is the same as ext *)
  86
  87 theorem image_id: ∀o,U. image o o (id1 REL o) U = U.
  88  intros; unfold image; simplify; split; simplify; intros;
  89   [ change with (a ∈ U);
  90     cases H; cases x; change in f with (eq1 ? w a); apply (. f‡#); assumption
  91   | change in f with (a ∈ U);
  92     exists; [apply a] split; [ change with (a = a); apply refl | assumption]]
  93 qed.
  94
  95 theorem minus_star_image_id: ∀o,U. minus_star_image o o (id1 REL o) U = U.
  96  intros; unfold minus_star_image; simplify; split; simplify; intros;
  97   [ change with (a ∈ U); apply H; change with (a=a); apply refl
  98   | change in f1 with (eq1 ? x a); apply (. f1 \sup -1‡#); apply f]
  99 qed.
 100
 101 theorem image_comp: ∀A,B,C,r,s,X. image A C (r ∘ s) X = image B C r (image A B s X).
 102  intros; unfold image; simplify; split; simplify; intros; cases H; clear H; cases x;
 103  clear x; [ cases f; clear f; | cases f1; clear f1 ]
 104  exists; try assumption; cases x; clear x; split; try assumption;
 105  exists; try assumption; split; assumption.
 106 qed.
 107
 108 theorem minus_star_image_comp:
 109  ∀A,B,C,r,s,X.
 110   minus_star_image A C (r ∘ s) X = minus_star_image B C r (minus_star_image A B s X).
 111  intros; unfold minus_star_image; simplify; split; simplify; intros; whd; intros;
 112   [ apply H; exists; try assumption; split; assumption
 113   | change with (x ∈ X); cases f; cases x1; apply H; assumption]
 114 qed.
 115
 116 record continuous_relation (S,T: basic_topology) : Type ≝
 117  { cont_rel:> arrows1 ? S T;
 118    reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U);
 119    saturated: ∀U. U = A ? U → minus_star_image ?? cont_rel U = A ? (minus_star_image ?? cont_rel U)
 120  }.
 121
 122 definition continuous_relation_setoid: basic_topology → basic_topology → setoid1.
 123  intros (S T); constructor 1;
 124   [ apply (continuous_relation S T)
 125   | constructor 1;
 126      [ apply (λr,s:continuous_relation S T.∀b. A ? (ext ?? r b) = A ? (ext ?? s b));
 127      | simplify; intros; apply refl1;
 128      | simplify; intros; apply sym1; apply H
 129      | simplify; intros; apply trans1; [2: apply H |3: apply H1; |1: skip]]]
 130 qed.
 131
 132 definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel.
 133
 134 coercion cont_rel'.
 135
 136 definition cont_rel'': ∀S,T: basic_topology. continuous_relation_setoid S T → binary_relation S T ≝ cont_rel.
 137
 138 coercion cont_rel''.
 139
 140 theorem ext_comp:
 141  ∀o1,o2,o3: REL.
 142   ∀a: arrows1 ? o1 o2.
 143    ∀b: arrows1 ? o2 o3.
 144     ∀x. ext ?? (b∘a) x = extS ?? a (ext ?? b x).
 145  intros;
 146  unfold ext; unfold extS; simplify; split; intro; simplify; intros;
 147  cases f; clear f; split; try assumption;
 148   [ cases f2; clear f2; cases x1; clear x1; exists; [apply w] split;
 149      [1: split] assumption;
 150   | cases H; clear H; cases x1; clear x1; exists [apply w]; split;
 151      [2: cases f] assumption]
 152 qed.
 153
 154 (*
 155 (* this proof is more logic-oriented than set/lattice oriented *)
 156 theorem continuous_relation_eqS:
 157  ∀o1,o2:basic_topology.∀a,a': continuous_relation_setoid o1 o2.
 158   a = a' → ∀X. A ? (extS ?? a X) = A ? (extS ?? a' X).
 159  intros;
 160  cut (∀a: arrows1 ? o1 ?.∀x. x ∈ extS ?? a X → ∃y:o2.y ∈ X ∧ x ∈ ext ?? a y);
 161   [2: intros; cases f; clear f; cases H1; exists [apply w] cases x1; split;
 162       try assumption; split; assumption]
 163  cut (∀a,a':continuous_relation_setoid o1 o2.eq1 ? a a' → ∀x. x ∈ extS ?? a X → ∃y:o2. y ∈ X ∧ x ∈ A ? (ext ?? a' y));
 164   [2: intros; cases (Hcut ?? f); exists; [apply w] cases x1; split; try assumption;
 165       apply (. #‡(H1 ?));
 166       apply (saturation_expansive ?? (A_is_saturation o1) (ext ?? a1 w) x);
 167       assumption;] clear Hcut;
 168  split; apply (if ?? (A_is_saturation ???)); intros 2;
 169   [lapply (Hcut1 a a' H a1 f) | lapply (Hcut1 a' a (H \sup -1) a1 f)]
 170   cases Hletin; clear Hletin; cases x; clear x;
 171  cut (∀a: arrows1 ? o1 ?. ext ?? a w ⊆ extS ?? a X);
 172   [2,4: intros 3; cases f3; clear f3; simplify in f5; split; try assumption;
 173       exists [1,3: apply w] split; assumption;]
 174  cut (∀a. A ? (ext o1 o2 a w) ⊆ A ? (extS o1 o2 a X));
 175   [2,4: intros; apply saturation_monotone; try (apply A_is_saturation); apply Hcut;]
 176  apply Hcut2; assumption.
 177 qed.
 178 *)
 179
 180 theorem continuous_relation_eq':
 181  ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
 182   a = a' → ∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X).
 183  intros; split; intro; unfold minus_star_image; simplify; intros;
 184   [ cut (ext ?? a a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;]
 185     lapply (if ?? (A_is_saturation ???) Hcut); clear Hcut;
 186     cut (A ? (ext ?? a' a1) ⊆ A ? X); [2: apply (. (H ?)‡#); assumption]
 187     lapply (fi ?? (A_is_saturation ???) Hcut);
 188     apply (Hletin1 x); change with (x ∈ ext ?? a' a1); split; simplify;
 189      [ apply I | assumption ]
 190   | cut (ext ?? a' a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;]
 191     lapply (if ?? (A_is_saturation ???) Hcut); clear Hcut;
 192     cut (A ? (ext ?? a a1) ⊆ A ? X); [2: apply (. (H ?)\sup -1‡#); assumption]
 193     lapply (fi ?? (A_is_saturation ???) Hcut);
 194     apply (Hletin1 x); change with (x ∈ ext ?? a a1); split; simplify;
 195      [ apply I | assumption ]]
 196 qed.
 197
 198 theorem extS_singleton:
 199  ∀o1,o2.∀a:arrows1 ? o1 o2.∀x.extS o1 o2 a (singleton o2 x) = ext o1 o2 a x.
 200  intros; unfold extS; unfold ext; unfold singleton; simplify;
 201  split; intros 2; simplify; cases f; split; try assumption;
 202   [ cases H; cases x1; change in f2 with (eq1 ? x w); apply (. #‡f2 \sup -1);
 203     assumption
 204   | exists; try assumption; split; try assumption; change with (x = x); apply refl]
 205 qed.
 206
 207 theorem continuous_relation_eq_inv':
 208  ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
 209   (∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X)) → a=a'.
 210  intros 6;
 211  cut (∀a,a': continuous_relation_setoid o1 o2.
 212   (∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X)) →
 213    ∀V:o2. A ? (ext ?? a' V) ⊆ A ? (ext ?? a V));
 214   [2: clear b H a' a; intros;
 215       lapply depth=0 (λV.saturation_expansive ??? (extS ?? a V)); [2: apply A_is_saturation;|skip]
 216        (* fundamental adjunction here! to be taken out *)
 217        cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a (A ? (extS ?? a V)));
 218         [2: intro; intros 2; unfold minus_star_image; simplify; intros;
 219             apply (Hletin V1 x); whd; split; [ exact I | exists; [apply a1] split; assumption]]
 220        clear Hletin;
 221        cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a' (A ? (extS ?? a V)));
 222         [2: intro; apply (. #‡(H ?)); apply Hcut] clear H Hcut;
 223        (* second half of the fundamental adjunction here! to be taken out too *)
 224       intro; lapply (Hcut1 (singleton ? V)); clear Hcut1;
 225       unfold minus_star_image in Hletin; unfold singleton in Hletin; simplify in Hletin;
 226       whd in Hletin; whd in Hletin:(?→?→%); simplify in Hletin;
 227       apply (if ?? (A_is_saturation ???));
 228       intros 2 (x H); lapply (Hletin V ? x ?);
 229        [ apply refl | cases H; assumption; ]
 230       change with (x ∈ A ? (ext ?? a V));
 231       apply (. #‡(†(extS_singleton ????)));
 232       assumption;]
 233  split; apply Hcut; [2: assumption | intro; apply sym1; apply H]
 234 qed.
 235
 236 definition continuous_relation_comp:
 237  ∀o1,o2,o3.
 238   continuous_relation_setoid o1 o2 →
 239    continuous_relation_setoid o2 o3 →
 240     continuous_relation_setoid o1 o3.
 241  intros (o1 o2 o3 r s); constructor 1;
 242   [ apply (s ∘ r)
 243   | intros;
 244     apply sym1;
 245     apply (.= †(image_comp ??????));
 246     apply (.= (reduced ?????)\sup -1);
 247      [ apply (.= (reduced ?????)); [ assumption | apply refl1 ]
 248      | apply (.= (image_comp ??????)\sup -1);
 249        apply refl1]
 250      | intros;
 251        apply sym1;
 252        apply (.= †(minus_star_image_comp ??????));
 253        apply (.= (saturated ?????)\sup -1);
 254         [ apply (.= (saturated ?????)); [ assumption | apply refl1 ]
 255         | apply (.= (minus_star_image_comp ??????)\sup -1);
 256           apply refl1]]
 257 qed.
 258
 259 definition BTop: category1.
 260  constructor 1;
 261   [ apply basic_topology
 262   | apply continuous_relation_setoid
 263   | intro; constructor 1;
 264      [ apply id1
 265      | intros;
 266        apply (.= (image_id ??));
 267        apply sym1;
 268        apply (.= †(image_id ??));
 269        apply sym1;
 270        assumption
 271      | intros;
 272        apply (.= (minus_star_image_id ??));
 273        apply sym1;
 274        apply (.= †(minus_star_image_id ??));
 275        apply sym1;
 276        assumption]
 277   | intros; constructor 1;
 278      [ apply continuous_relation_comp;
 279      | intros; simplify; intro x; simplify;
 280        lapply depth=0 (continuous_relation_eq' ???? H) as H';
 281        lapply depth=0 (continuous_relation_eq' ???? H1) as H1';
 282        letin K ≝ (λX.H1' (minus_star_image ?? a (A ? X))); clearbody K;
 283        cut (∀X:Ω \sup o1.
 284               minus_star_image o2 o3 b (A o2 (minus_star_image o1 o2 a (A o1 X)))
 285             = minus_star_image o2 o3 b' (A o2 (minus_star_image o1 o2 a' (A o1 X))));
 286         [2: intro; apply sym1; apply (.= #‡(†((H' ?)\sup -1))); apply sym1; apply (K X);]
 287        clear K H' H1';
 288        cut (∀X:Ω \sup o1.
 289               minus_star_image o1 o3 (b ∘ a) (A o1 X) = minus_star_image o1 o3 (b'∘a') (A o1 X));
 290         [2: intro;
 291             apply (.= (minus_star_image_comp ??????));
 292             apply (.= #‡(saturated ?????));
 293              [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ]
 294             apply sym1;
 295             apply (.= (minus_star_image_comp ??????));
 296             apply (.= #‡(saturated ?????));
 297              [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ]
 298            apply ((Hcut X) \sup -1)]
 299        clear Hcut; generalize in match x; clear x;
 300        apply (continuous_relation_eq_inv');
 301        apply Hcut1;]
 302   | intros; simplify; intro; do 2 (unfold continuous_relation_comp); simplify;
 303     apply (.= †(ASSOC1‡#));
 304     apply refl1
 305   | intros; simplify; intro; unfold continuous_relation_comp; simplify;
 306     apply (.= †((id_neutral_right1 ????)‡#));
 307     apply refl1
 308   | intros; simplify; intro; simplify;
 309     apply (.= †((id_neutral_left1 ????)‡#));
 310     apply refl1]
 311 qed.