From 52f4a3c6a3e47f1cb6a5912aeff3bcbdb76bc17f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 9 Sep 2008 15:34:07 +0000 Subject: [PATCH] Concrete spaces do form a category, after all :-) --- .../library/formal_topology/basic_pairs.ma | 8 +- .../formal_topology/concrete_spaces.ma | 77 ++++++++++++++----- 2 files changed, 63 insertions(+), 22 deletions(-) diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma index 3ee864937..63aedcd61 100644 --- a/helm/software/matita/library/formal_topology/basic_pairs.ma +++ b/helm/software/matita/library/formal_topology/basic_pairs.ma @@ -76,7 +76,7 @@ lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → ⊩ \cir ] qed. -definition id: ∀o:basic_pair. relation_pair o o. +definition id_relation_pair: ∀o:basic_pair. relation_pair o o. intro; constructor 1; [1,2: apply id1; @@ -119,17 +119,17 @@ definition BP: category1. constructor 1; [ apply basic_pair | apply relation_pair_setoid - | apply id + | apply id_relation_pair | apply relation_pair_composition | intros; change with (a12\sub\c ∘ a23\sub\c ∘ a34\sub\c ∘ ⊩ = (a12\sub\c ∘ (a23\sub\c ∘ a34\sub\c) ∘ ⊩)); apply (ASSOC1‡#); | intros; - change with ((id o1)\sub\c ∘ a\sub\c ∘ ⊩ = a\sub\c ∘ ⊩); + change with ((id_relation_pair o1)\sub\c ∘ a\sub\c ∘ ⊩ = a\sub\c ∘ ⊩); apply ((id_neutral_left1 ????)‡#); | intros; - change with (a\sub\c ∘ (id o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩); + change with (a\sub\c ∘ (id_relation_pair o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩); apply ((id_neutral_right1 ????)‡#); ] qed. \ No newline at end of file diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma index 175f9fbb8..462eefd00 100644 --- a/helm/software/matita/library/formal_topology/concrete_spaces.ma +++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma @@ -124,7 +124,7 @@ definition convergent_relation_space_setoid: concrete_space → concrete_space | intros 3; apply trans1]] qed. -definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 ? CS1 CS2 ≝ +definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝ λCS1,CS2,c.rp ?? c. coercion rp''. @@ -149,7 +149,7 @@ lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X. | change with (a = a); apply refl]]] qed. -lemma extS_id: ∀o:basic_pair.∀X.extS (concr o) (concr o) (id o) \sub \c X = X. +lemma extS_id: ∀o:BP.∀X.extS (concr o) (concr o) (id1 ? o) \sub \c X = X. intros; unfold extS; simplify; split; simplify; intros; @@ -163,13 +163,59 @@ lemma extS_id: ∀o:basic_pair.∀X.extS (concr o) (concr o) (id o) \sub \c X = | exists; [apply a] split; [ assumption | change with (a = a); apply refl]]] qed. -(* + +lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c1 ∘ c2) S = extS o1 o2 c1 (extS o2 o3 c2 S). + intros; unfold extS; simplify; split; intros; simplify; intros; + [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption] + cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6; + exists; [apply w1] split [2: assumption] constructor 1; [assumption] + exists; [apply w] split; assumption + | cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption] + cases H3 (H4 H5); cases H4 (w1 H6); clear H3 H4; cases H6 (w2 H7); clear H6; + cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split; + assumption] +qed. + +definition convergent_relation_space_composition: + ∀o1,o2,o3: concrete_space. + binary_morphism1 + (convergent_relation_space_setoid o1 o2) + (convergent_relation_space_setoid o2 o3) + (convergent_relation_space_setoid o1 o3). + intros; constructor 1; + [ intros; whd in c c1 ⊢ %; + constructor 1; + [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption] + | intros; + change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c); + change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?))) + with (c \sub \f ∘ c1 \sub \f); + change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?)))) + with (c \sub \f ∘ c1 \sub \f); + apply (.= (extS_com ??????)); + apply (.= (†(respects_converges ?????))); + apply (.= (respects_converges ?????)); + apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1))); + apply refl1; + | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c); + apply (.= (extS_com ??????)); + apply (.= (†(respects_all_covered ???))); + apply (.= respects_all_covered ???); + apply refl1] + | intros; + change with (a ∘ b = a' ∘ b'); + change in H with (rp'' ?? a = rp'' ?? a'); + change in H1 with (rp'' ?? b = rp ?? b'); + apply (.= (H‡H1)); + apply refl1] +qed. + definition CSPA: category1. constructor 1; [ apply concrete_space | apply convergent_relation_space_setoid | intro; constructor 1; - [ apply id + [ apply id1 | intros; unfold id; simplify; apply (.= (equalset_extS_id_X_X ??)); @@ -178,22 +224,17 @@ definition CSPA: category1. apply refl1; | apply (.= (extS_id ??)); apply refl1] - | intros; constructor 1; - [ intros; whd in c c1 ⊢ %; - constructor 1; - [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption] - | intros; - | - ] - | intros; - change with (a ∘ b = a' ∘ b'); - change in H with (rp'' ?? a = rp'' ?? a'); - change in H1 with (rp'' ?? b = rp ?? b'); - apply (.= (H‡H1)); - apply refl1] + | apply convergent_relation_space_composition | intros; simplify; change with ((a12 ∘ a23) ∘ a34 = a12 ∘ (a23 ∘ a34)); apply (.= ASSOC1); apply refl1 | intros; simplify; - change with (id o1 ∘ a = a);*) \ No newline at end of file + change with (id1 ? o1 ∘ a = a); + apply (.= id_neutral_left1 ????); + apply refl1 + | intros; simplify; + change with (a ∘ id1 ? o2 = a); + apply (.= id_neutral_right1 ????); + apply refl1] +qed. \ No newline at end of file -- 2.39.2