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.