Add manifolds and smooth manifolds

[siraben]

An n-dimensional manifold M is a second countable Hausdorff space that is locally homeomorphic to Rⁿ . There seems to be several parts in the library already:

• second_countable
• Hausdorff
• homeomorphic

The "locally homeomorphic" part requires that every point p ∈ M there is an open neighborhood U ⊂ M and a homeomorphism x : U -> U' for open U' ⊂ Rⁿ.

For smooth manifolds, the definition is a bit more involved and involves chart transformations and (Euclidean then topological) smoothness, which doesn't seem to be here yet.

[stop-cran]

For local homeomorphism I'd propose the following definition:

From Topology Require Import Homeomorphisms SubspaceTopology.

Definition restriction {X Y: Type} (f : X -> Y) (U : Ensemble X): {x | U x} -> {y | Im U f y}.
intro x.
apply (exist _ (f (proj1_sig x))).
apply (Im_intro _ _ _ _ _ (proj2_sig x)).
reflexivity.
Defined.

Inductive local_homeomorphism {X Y : TopologicalSpace}
                              (f : point_set X -> point_set Y) : Prop :=
| intro_local_homeomorphism:
  (forall (x: point_set X),
    exists U:Ensemble (point_set X),
      open_neighborhood U x /\
      open (Im U f) /\
      @homeomorphism (SubspaceTopology U) (SubspaceTopology (Im U f)) (restriction f U)) ->
    local_homeomorphism f.

Feel free to submit a PR with more definitions and proofs!

[siraben]

With more Euclidean space theories we would be able to talk about Riemannian and pesudo-Riemannian manifolds

[siraben]

@stop-cran because of the use of sigmas in restriction, it seems to make proving some things more difficult such as, in proving locally_homeomorphic is reflexive, it requires one to prove the goal

continuous (restriction (fun p : X => p) Full_set)

So, naturally one would like to prove something like restriction (fun p : X => p) Full_set = (fun p : X => p), but it fails:

Fail Lemma restriction_full (X : TopologicalSpace) :
  restriction (fun p : X => p) Full_set = (fun p : X => p).
(* The command has indeed failed with message: *)
(* Found type "point_set X" where "{x : X | Full_set x}" was expected. *)

How would I deal with this, would I have to use projections?

[stop-cran]

@siraben restriction of a function on a full set, similar to SubspaceTopology Full_Set looks like a place, where mathematicians implicitly use the univalence axiom. For Coq f and restriction f Full_Set are still different objects though. I'll try to prove some simple facts a bit later and see if we can come up with a more convenient definition.

[siraben]

@stop-cran thank you, I'll familiarize myself with the style of proof and definitions in the topology library. The tracking PR is #30, branch manifolds

[stop-cran]

@siraben try this proof for locally_homeomorphic_refl:

From Topology Require Import Homeomorphisms.
From Topology Require Import SubspaceTopology.
From Coq Require Import Image.

Definition restriction {X Y: Type} (f : X -> Y) (U : Ensemble X): {x | U x} -> {y | Im U f y}.
intro x.
exists (f (proj1_sig x)).
now apply (Im_intro _ _ _ _ _ (proj2_sig x)).
Defined.

Inductive local_homeomorphism {X Y : TopologicalSpace}
                              (f : point_set X -> point_set Y) : Prop :=
| intro_local_homeomorphism:
  (forall (x: point_set X),
    exists U:Ensemble (point_set X),
      open_neighborhood U x /\
      open (Im U f) /\
      @homeomorphism (SubspaceTopology U) (SubspaceTopology (Im U f)) (restriction f U)) ->
    local_homeomorphism f.

Definition locally_homeomorphic (X Y:TopologicalSpace) : Prop :=
  exists (f : point_set X -> point_set Y), local_homeomorphism f.

Lemma homeomorphism_refl (X : TopologicalSpace) : @homeomorphism X X id.
Proof.
econstructor;
  (apply continuous_identity || now intros).
Qed.

Lemma restriction_continuous {X Y: TopologicalSpace} (f : point_set X -> point_set Y) (U : Ensemble X):
  continuous f -> @continuous (SubspaceTopology U) (SubspaceTopology (Im U f)) (restriction f U).
Proof.
  intros Hcont V [F H].
  rewrite inverse_image_family_union_image.
  apply open_family_union.
  intros.
  destruct H0.
  subst.
  apply H in H0.
  clear H F V.
  induction H0.
  - match goal with
     | [ |- open ?S ] => replace S with (@Full_set (SubspaceTopology U))
    end.
    + apply open_full.
    + extensionality_ensembles;
        repeat constructor.
  - destruct H, a.
    match goal with
     | [ |- open ?S ] => replace S with (inverse_image (subspace_inc U) (inverse_image f V))
    end.
    + now apply subspace_inc_continuous, Hcont.
    + extensionality_ensembles;
        now repeat constructor.
  - rewrite inverse_image_intersection.
    now apply open_intersection2.
Qed.

Definition full_set_unrestriction (X : TopologicalSpace):
  @SubspaceTopology X (@Im X X (@Full_set X) (@id X)) -> @SubspaceTopology X (@Full_set X).
intro x.
now exists (proj1_sig x).
Defined.

Lemma full_set_unrestriction_continuous (X : TopologicalSpace): continuous (full_set_unrestriction X).
Proof.
  intros V [F H].
  rewrite inverse_image_family_union_image.
  apply open_family_union.
  intros.
  destruct H0.
  subst.
  apply H in H0.
  induction H0.
  - rewrite inverse_image_full_set.
    apply open_full.
  - destruct H0, a.
    unfold full_set_unrestriction.
    match goal with
     | [ |- open ?S ] => replace S with (inverse_image (subspace_inc (Im (@Full_set X) id)) V0)
    end.
    + now apply subspace_inc_continuous.
    + extensionality_ensembles;
        now repeat constructor.
  - rewrite inverse_image_intersection.
    now apply open_intersection2.
Qed.

Lemma locally_homeomorphic_refl (X : TopologicalSpace) : locally_homeomorphic X X.
Proof.
  exists id.
  constructor.
  intro.
  exists Full_set.
  repeat split.
  - apply X.
  - replace (Im Full_set id) with (@Full_set X).
    + apply X.
    + extensionality_ensembles;
        repeat econstructor.
  - econstructor.
    + apply restriction_continuous, continuous_identity.
    + apply full_set_unrestriction_continuous.
    + now intros [x0 []].
    + intros [x0 [x1 [] ?]].
      now subst.
Qed.

[siraben]

@stop-cran great, this works!

[siraben]

How would you express the notion of an atlas? I'm not sure if I should use an IndexedFamily or Ensemble here (maybe there are resources you could recommend, since I've mostly learned via Software Foundations and CPDT).

A collection of charts {x_α : U_α → U_α′ } covering M (i.e. such that the union ⋃U_α of the chart domains is M) is called an atlas.

[siraben]

@stop-cran Ah, the problem with

Definition locally_homeomorphic (X Y:TopologicalSpace) : Prop :=
  exists (f : point_set X -> point_set Y), local_homeomorphism f.

Is that it fixes an f that would work globally over X, whereas in differential topology it is allowed for chart domains to overlap (and have possibly different outputs).

[stop-cran]

@siraben Family is more generic, since does not require an explicit indices, whereas IndexedFamily is sometimes easier to use. One more thought is about functoriality. Since Ensemble is a contravariant functor on it's single argument T (as any function type on it's input argument), Family as a composition of two contravariant functors is a (covariant) functor. Whereas IndexedFamily A is contravariant functor on T. It depends which functoriality is better in each case.

[Columbus240]

Hello @siraben.

We might want to introduce a dependency on a linear algebra library for definitions and properties of vector spaces. Otherwise we need to introduce all this ourselves as we go.
I don’t think we can introduce differential geometry/topology easily without some major parts of analysis. I know I don’t have the time to develop such a theory, but feel free to do so. I think using an existing library could make it easier.
I haven’t yet looked around for libraries that’d make good candidates.

[siraben]

We might want to introduce a dependency on a linear algebra library for definitions and properties of vector spaces.

Yes, this would be necessary when we talk about immersions, embeddings and the rank theorem.

I don’t think we can introduce differential geometry/topology easily without some major parts of analysis.

This seems necessary to do as well, since partial derivatives in Rⁿ and the Jacobian come up quite often. I have only worked with the stdlib's real analysis but I've read that Coquelicot is well-designed.

[Columbus240]

I can’t take the time at the moment to inform myself, which library would be appropriate etc. Can’t support you in that regard. But Coquelicot seems ok at first glance, but I didn’t find out whether the library is still supported. There might be some other libraries for real analysis and linear algebra floating around in coq-community, the ssreflect or the mathematical-components communities.

Edit: I should be honest: I am not interested enough in developing the theory of manifolds, to help decide on a library. It isn’t so much a problem of having time.
But if you find a library that works, feel free to create pull requests etc to add it.

[Columbus240]

Maybe we can avoid depending a lot on the construction of euclidean spaces, if we first characterize them up to homeomorphism and then work with "axiomatized euclidean spaces".
We still would need to construct one example of R^n, to show our axiomatization is correct, and would still need to choose a library for linear algebra, before we could develop theory about manifolds.

[Columbus240]

We could do the

• Classification of compact manifolds without boundary.
  A proof is included in Munkres' Topology book. For a part of the proof a separate paper is needed, which is referenced in the book.

[Columbus240]

We have a proof that glueing the ends of an interval together results in a circle. This is an example of a more general construction, described in "suspension of spheres" on the nlab. There's links to other more or less algebraic results on constructions of manifolds. (I wanted to preserve this note from #39) So another possibility is

• Introduce the "suspension" construction and prove that it maps spheres to spheres.