Voici l’exercice qu’on va abordé dans ce billet :

Soit \((X, T )\) un espace topologique séparé. Montrer que la diagonale \(\Delta\) de \(X ×X\) est fermée dans
\(X × X\).

http://math.univ-lille1.fr/~bodin/exolic1/exolic.pdf

Aparté sur les topologies initiales

Mon livre de topologie définit 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ène à regarder ce qu’est une topologie initiale.

Pour être transparent, je vois également le terme de « topologie faible » utilisé ; c’est justement le terme utilisé par coq-topology… Je n’ai pour l’instant pas trouvé s’il y a une différence entre les 2 concepts, dans la suite je pars du principe qu’il s’agit de la même chose.

Une topologie initiale permet de construire une topologie sur un espace qui n’en dispose pas à 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éfinit une topologie sur X comme étant 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.

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\).

Preuve en Coq

Le module coq-topology dispose d’un module ProductTopology qui lui-même se base sur le module WeakTopology qui implémente les définitions du paragraphe précédent.

Comme souvent la principale difficulté n’est pas à trouver dans les mathématiques, il ne s’agit que de dérouler des définitions ; en revanche, ces définitions sont particulièrement peu digestes en Coq.

On va utiliser également les axiomes de séparations déjà définis dans coq-topology.

From Topology Require Import TopologicalSpaces.
From Topology Require Import InteriorsClosures.
From Topology Require Import Neighborhoods.
From Topology Require Import ProductTopology.
From Topology Require Import SeparatednessAxioms.

On dispose de quelques fonctions dans coq-topology pour faciliter l’écriture de produit de 2 topologies, qui se basent sur les fonctions built-in fst et snd de Coq. L’énoncé devient :

Theorem exo (X:TopologicalSpace):
  Hausdorff X -> closed (fun x:point_set (ProductTopology2 X X) => fst x = snd x).
Proof.

On va déplier les définitions :

  unfold Hausdorff.
  intros HypSep.
  unfold closed.

Pour plus de lisibilité, on va associer à l’ensemble \(\Delta\) une variable :

  remember (Complement (fun x : point_set (ProductTopology2 X X) => fst x = snd x)) as ExtDiagonale.

On passe ensuite par un résultat intermédiaire sur cette diagonale pour caractériser les éléments qui y appartiennent :

  assert (forall x y, not (x=y) <-> In ExtDiagonale (x,y)).
  split;intros.
  - rewrite HeqExtDiagonale. eauto with sets.
  - rewrite HeqExtDiagonale in H. eauto with sets.

Pour résoudre l’exercice, on va utiliser une base des ouverts sur le produit de topologie.

  - refine (coverable_by_open_basis_impl_open (ProductTopology2_basis X X) _ _ _). apply ProductTopology2_basis_is_basis.
    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 ]].
    exists (fun x => In U (fst x) /\ In V (snd x)). inversion H1 as [openU [openV [x0InU [x0inV InterUVEmpty]]]].
    split.
    + 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.
    + split.
      * 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.
      * autounfold with *. eauto with *.
Qed.