Voici l’exercice qu’on va abord\u00e9 dans ce billet :<\/p>\n\n\n\n
Soit \\((X, T )\\) un espace topologique s\u00e9par\u00e9. Montrer que la diagonale \\(\\Delta\\) de \\(X \u00d7X\\) est ferm\u00e9e dans
\\(X \u00d7 X\\).<\/p>http:\/\/math.univ-lille1.fr\/~bodin\/exolic1\/exolic.pdf<\/cite><\/blockquote>\n\n\n\nApart\u00e9 sur les topologies initiales<\/h2>\n\n\n\n
Mon livre de topologie d\u00e9finit les produits de topologies comme la topologie initiale des fonctions de projections \\(p_i = (x_1, x_2) \\in X, X \\to x_i\\). Ce qui nous am\u00e8ne \u00e0 regarder ce qu’est une topologie initiale.<\/p>\n\n\n\n
Pour \u00eatre transparent, je vois \u00e9galement le terme de \u00ab\u00a0topologie faible\u00a0\u00bb utilis\u00e9 ; c’est justement le terme utilis\u00e9 par coq-topology… Je n’ai pour l’instant pas trouv\u00e9 s’il y a une diff\u00e9rence entre les 2 concepts, dans la suite je pars du principe qu’il s’agit de la m\u00eame chose.<\/p>\n\n\n\n
Une topologie initiale permet de construire une topologie sur un espace qui n’en dispose pas \u00e0 partir de fonctions de cet espace sur un espace qui, lui, est topologique. Ainsi, si on dispose d’un espace X, et de fonctions \\(f_i:X \\to Y_i\\) avec \\(Y_i\\) topologique, on d\u00e9finit une topologie sur X comme \u00e9tant l’ensemble des intersections des \\(f_i^{-1}(O_i)\\) avec \\(O_i\\) ouvert de \\(Y_i\\). Ceci permet d’assurer que, par construction, ces fonctions sont continues.<\/p>\n\n\n\n
Dans le cas des fonctions produits, les ouverts sont donc de la forme \\(O_1 x O_2\\) avec \\(O_1\\) un ouvert de \\(Y_1\\) et \\(O_2\\) un ouvert de \\(Y_2\\).<\/p>\n\n\n\n
Preuve en Coq<\/h2>\n\n\n\n
Le module coq-topology dispose d’un module ProductTopology<\/a> qui lui-m\u00eame se base sur le module WeakTopology<\/a> qui impl\u00e9mente les d\u00e9finitions du paragraphe pr\u00e9c\u00e9dent.<\/p>\n\n\n\n
Comme souvent la principale difficult\u00e9 n’est pas \u00e0 trouver dans les math\u00e9matiques, il ne s’agit que de d\u00e9rouler des d\u00e9finitions ; en revanche, ces d\u00e9finitions sont particuli\u00e8rement peu digestes en Coq.<\/p>\n\n\n\n
On va utiliser \u00e9galement les axiomes de s\u00e9parations d\u00e9j\u00e0 d\u00e9finis dans coq-topology.<\/p>\n\n\n
\nFrom Topology Require Import TopologicalSpaces.\nFrom Topology Require Import InteriorsClosures.\nFrom Topology Require Import Neighborhoods.\nFrom Topology Require Import ProductTopology.\nFrom Topology Require Import SeparatednessAxioms.\n<\/pre><\/div>\n\n\nOn dispose de quelques fonctions dans coq-topology pour faciliter l’\u00e9criture de produit de 2 topologies, qui se basent sur les fonctions built-in fst et snd de Coq. L’\u00e9nonc\u00e9 devient :<\/p>\n\n\n
\n\nTheorem exo (X:TopologicalSpace):\n Hausdorff X -> closed (fun x:point_set (ProductTopology2 X X) => fst x = snd x).\nProof.\n<\/pre><\/div>\n\n\nOn va d\u00e9plier les d\u00e9finitions :<\/p>\n\n\n
\n unfold Hausdorff.\n intros HypSep.\n unfold closed.\n<\/pre><\/div>\n\n\nPour plus de lisibilit\u00e9, on va associer \u00e0 l’ensemble \\(\\Delta\\) une variable :<\/p>\n\n\n
\n remember (Complement (fun x : point_set (ProductTopology2 X X) => fst x = snd x)) as ExtDiagonale.\n<\/pre><\/div>\n\n\nOn passe ensuite par un r\u00e9sultat interm\u00e9diaire sur cette diagonale pour caract\u00e9riser les \u00e9l\u00e9ments qui y appartiennent :<\/p>\n\n\n
\n assert (forall x y, not (x=y) <-> In ExtDiagonale (x,y)).\n split;intros.\n - rewrite HeqExtDiagonale. eauto with sets.\n - rewrite HeqExtDiagonale in H. eauto with sets.\n<\/pre><\/div>\n\n\nPour r\u00e9soudre l’exercice, on va utiliser une base des ouverts sur le produit de topologie.<\/p>\n\n\n
\n - refine (coverable_by_open_basis_impl_open (ProductTopology2_basis X X) _ _ _). apply ProductTopology2_basis_is_basis.\n intros x0 x0inExtDiag. assert (x0 = (fst x0, snd x0)). apply surjective_pairing. rewrite H0 in x0inExtDiag. pose (tmp:=H (fst x0) (snd x0)). rewrite <- tmp in x0inExtDiag. destruct (HypSep (fst x0) (snd x0) x0inExtDiag) as [U [V ]].\n exists (fun x => In U (fst x) \/\\ In V (snd x)). inversion H1 as [openU [openV [x0InU [x0inV InterUVEmpty]]]].\n split.\n + replace (fun x : point_set X * point_set X => In U (fst x) \/\\ In V (snd x)) with [p : point_set (ProductTopology2 X X) | let (x, y) := p in In U x \/\\ In V y]. constructor ; repeat assumption. simpl. apply functional_extensionality. intros. Search ([_:_ | _]). rewrite characteristic_function_to_ensemble_is_identity. autounfold with *. assert (x=(fst x, snd x)). apply surjective_pairing. rewrite H2. simpl. trivial.\n + split.\n * autounfold with *. intros. pose (tmp2:=surjective_pairing x). rewrite tmp2. rewrite <- H. unfold In in H2. inversion H2. unfold not. intro. rewrite H5 in H3. assert(In (Intersection U V) (snd x)). eauto with *. rewrite InterUVEmpty in H6. Search Empty_set. apply Noone_in_empty in H6. assumption.\n * autounfold with *. eauto with *.\nQed.\n<\/pre><\/div>","protected":false},"excerpt":{"rendered":"Voici l’exercice qu’on va abord\u00e9 dans ce billet : Soit un espace topologique s\u00e9par\u00e9. Montrer que la diagonale de est ferm\u00e9e dans . http:\/\/math.univ-lille1.fr\/~bodin\/exolic1\/exolic.pdf Apart\u00e9 sur les topologies initiales Mon livre de topologie d\u00e9finit les produits de topologies comme la topologie initiale des fonctions de projections . Ce qui nous am\u00e8ne \u00e0 regarder ce qu’est […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[1],"tags":[],"_links":{"self":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/124"}],"collection":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=124"}],"version-history":[{"count":5,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/124\/revisions"}],"predecessor-version":[{"id":129,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/124\/revisions\/129"}],"wp:attachment":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=124"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=124"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=124"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}