Differential Geometry - Mizar

There seems to be some work done on topological manifolds, but not much on differential manifolds. So far, there does not appear to be a notion of atlases or charts (so far as I can tell, at least).

• mfold_0 on topological manifolds is a retcon, retroactively introducing a notion of a locally Euclidean space which covers manifolds with and without boundary.
  • locally_euclidean means for every point \(p\in M\) there exists a neighborhood \(p\in U\subset M\) such that there exists an \(n\in\mathbb{N}\) such that \(M|_{U}\) is homeomorphic to the n-dimensional disk.
  • topological_manifold is a non-empty Hausdorff second-countable locally-Euclidean topological space
• mfold_1 formalizes the definition of topological manifolds following Jack Lee.
  • MFOLD_1:8 proves the unit ball and \(\mathbb{R}^{n}\) are homeomorphic
  • connsp_2 formalizes notions related to being a neighborhood to a point in a topological space, which is used when defining the attribute locally_euclidean (MFOLD_0:def2).
  • n-manifold is defined as a Hausdorff, second-countable, \(n\) locally Euclidean space.
• mfold_2 formalizes examples of manifolds, namely planes, spheres, and stereographic projection.
• connsp_1 formalizes notions of connected spaces
  • pathwise_connected is an attribute defined in BORSKU_2:Def3
• connsp_3 formalizes notions of components

However, what is lacking is…well, a bit. For example:

• Charts and Atlases
  • This is tricky, because there are two conventions for defining a chart, and they are completely opposite of each other.
    • Convention 1: Given a manifold \(M\) we could define a chart as \(\varphi\colon U\subset M\to\mathbb{R}^{n}\) being a homeomorphism with its image. The mapping in this direction (from patch of manifold to Euclidean space) is called the local coordinate for the patch.
      • Bourbaki follows this convention, at least I infer as much from Lie Groups, III §1.1 Lemma 1 (page 210 of my paperback copy);
      • Warner's Foundations of Differential Geometry and Lie Groups (Def.1.3) follows this convention;
      • Isham's Modern Differential Geometry for Physicists follows this convention (Def.2.1 in §2.2).
      • Spivak's Comprehensive Introduction to Differential Geometry, vol. I, appears to follow this convention (for every \(x\in M\) there is a neighborhood \(U\subset M\) of \(x\in U\) which is homeomorphic to an open subset of \(\mathbb{R}^{n}\) — pg 1; but also see chapter 2, where smooth structures are defined using charts following this convention)
      • If I recall correctly, both Tu and Lee follow this convention.
    • Convention 2: Given a manifold, a chart is a mapping \(\varphi\colon V\subset\mathbb{R}^{n}\to M\) which is a homeomorphism with its image. The mapping in this direction (from a patch of Euclidean space to the manifold) is called a local parametrization for the manifold.
      • Milnor follows this convention,
      • do Carmo's Riemannian Geometry uses this convention.
      • Besse's Einstein Manifolds (§1.41) appears to have a chart be from a patch of Euclidean space to the manifold.
      • When I took Dr Fuchs's course on differential topology, the convention used followed Milnor (I suspect to avoid people copying proofs from Tu, Lee, and friends).
  • Compatible charts
  • Atlas = family of pairwise compatible charts which cover the manifold
  • Equivalent atlases = the union of the atlases is another atlas
  • Two atlases are equivalent if and only if every chart from one atlas is compatible with every chart from the other atlas.
  • The relation (equivalent atlases) is transitive
  • A subset of the manifold is open (with respect to an atlas) if blah blah blah. Atlases induce a topology.
• Mappings between manifolds
  • Embedding, Immersion, Submersion, Diffeomorphism, Local Diffeomorphism
  • Partitions of Unity
• Products of Manifolds
  • There are other related constructions (the disjoint union of manifolds of the same dimension, and the connected sum), but I'm not sure how necessary they are to begin with…
• Submanifolds
• Tangent Vectors and Vector Fields
  • Tangent bundle, double tangent bundle
• Differentials of Smooth Maps
• Morse Theory
• Differential Forms