Topology on sets with manifold structure

Stream: mathlib4

[Michael Lee]

I'm just getting into how manifolds are implemented in mathlib with aim of adding a toy example showing that the graph of a continuous function between two topological manifolds is a submanifold of their product. I'm starting with f : R^n → R^k because that seemed easiest to conceptualize (i.e. that for graph f the graph of f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k) and Continuous f, we have HasGroupoid (graph f) (contDiffGroupoid 0 (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))))). It then shouldn't be too much of a stretch to show that this is actually a SmoothManifoldWithCorners in the case that f is C^∞. I imagine that the graph and the global chart should look something like this:

def graph (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)) :
    Set (EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin k)) := setOf (fun x => x.snd = f x.fst)

def projChart (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)) (hf : Continuous f) :
    LocalHomeomorph (graph f) (EuclideanSpace ℝ (Fin n)) where
  source := univ
  target := univ
  toFun x := x.1.fst
  invFun x := ⟨(x, f x), rfl⟩
  map_source' := by simp only [mem_univ, implies_true]
  map_target' := by simp only [mem_univ, implies_true]
  left_inv' := by simp only [mem_univ, forall_true_left, Subtype.forall, Subtype.mk.injEq,
    Prod.forall, Prod.mk.injEq, true_and, graph, mem_setOf_eq, forall_eq, eq_self, implies_true]
  right_inv' := by simp only [mem_univ, forall_true_left, forall_const]
  open_source := by simp
  open_target := by simp
  continuous_toFun := by
    apply Continuous.continuousOn
    simp only [LocalEquiv.toFun]
    exact continuous_fst
  continuous_invFun := by
    apply Continuous.continuousOn
    apply Continuous.subtype_mk
    exact continuous_prod_mk.mpr (And.intro continuous_id hf)

I have the sneaking suspicion that I'm not correctly specifying how graph f is inheriting the subspace topology from R^n × R^k, however. Namely, I'm getting a synthInstance error in trying to apply continuous_fst in the proof of continuous_toFun, saying that it's stuck trying to synthesize a TopologicalSpace of some metavariable. Does anyone know what I might be missing here? Thanks!

[Kevin Buzzard]

I don't know this part of the library at all but often the way to fix that error on a function foo is to explicitly supply the metavariable using the foo (X := \R) ... syntax, where X is the name of the variable used by foo

[Michael Lee]

Ah, I think I was actually just using the wrong theorem here. I tried apply Continuous.fst and realized that Lean still wanted me to show that the inclusion from graph f into R^n × R^k was continuous, which I could just do with exact Continuous.subtype_val continuous_id.

[Oliver Nash]

If you're interested in trying out the manifold part of the library, here's something that is missing that I think shouldn't be too hard:

import Mathlib.Geometry.Manifold.Complex
import Mathlib.LinearAlgebra.ProjectiveSpace.Basic

set_option quotPrecheck false

open Manifold

variable {n : ℕ}

local notation "ℂⁿ" => Fin n → ℂ
local notation "ℂℙⁿ" => Projectivization ℂ (Fin (n + 1) → ℂ)

instance : TopologicalSpace ℂℙⁿ := by rw [Projectivization]; infer_instance

instance : ChartedSpace ℂⁿ ℂℙⁿ := sorry -- Data

instance : SmoothManifoldWithCorners 𝓘(ℂ, ℂⁿ) ℂℙⁿ := sorry -- Prop

[Oliver Nash]

Of course it's true for more general fields and I suppose, infinite dimensions too. I've only written it for ℂ because I've pasted that code in from a snippet I had somewhere.

[Michael Lee]

@Oliver Nash Sure, I'd love to tackle this next! Actually, my long-term goal is to formalize as much of Jack Lee's Introduction to Smooth Manifolds as I can (and as makes sense within the structure of the existing manifold part of the library), and eventually to make it to Introduction to Riemannian Manifolds as well. I finished the example above (which is Example 1.3 in Smooth Manifolds) and am generalizing it to the graph of a C^k function between two C^k manifolds now. Example 1.4 is spheres (already done by @Heather Macbeth ), and Example 1.5 is projective spaces (which I'll aim to similarly generalize to nontrivially normed fields).

[Oliver Nash]

That sounds wonderful. I believe Heather actually has a branch which defines Riemannian manifolds but I think it's mostly proof-of-concept, rather than a proposal for the Mathlib definition. Projective spaces are of course just special cases of Grassmannians but I think the latter can wait.

[Michael Lee]

Oliver Nash said:

That sounds wonderful. I believe Heather actually has a branch which defines Riemannian manifolds but I think it's mostly proof-of-concept, rather than a proposal for the Mathlib definition. Projective spaces are of course just special cases of Grassmannians but I think the latter can wait.

Good point. Although, I think we're missing a couple of key results to show this. Actually, maybe I should focus on embedded submanifolds (which would both trivialize the above example and enable formalizing the Grassmannian as an embedded submanifold of C^(n × n)).

[Winston Yin (尹維晨)]

@Michael Lee How is this coming along? I've also been formalising parts of Lee's Introduction to Smooth Manifolds, specifically the parts on integral curves. At some point we can't avoid referring to submanifolds, e.g. vector fields tangent to a submanifold, Lie subgroups. Should there be a (immersed/embedded) Submanifold structure?