Zulip Chat Archive

Stream: new members

Topic: Composition of Smooth Maps (on Manifolds)

Dominic Steinitz (Sep 17 2024 at 09:30):

I set myself the exercise of proving that the composition of 2 smooth maps is smooth. I've made a bit of progress but wanted to check I am on the right lines. I have managed to define 3 manifolds without boundary (so as in any elementary intro to differential geometry)

import Mathlib

open Manifold

variable
  (m : β„•) {M : Type*}
   [TopologicalSpace M]
   [ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
   [SmoothManifoldWithCorners (𝓑 m) M]

variable
  (n : β„•) {N : Type*}
   [TopologicalSpace N]
   [ChartedSpace (EuclideanSpace ℝ (Fin n)) N]
   [SmoothManifoldWithCorners (𝓑 n) N]

variable
  (p : β„•) {P : Type*}
   [TopologicalSpace P]
   [ChartedSpace (EuclideanSpace ℝ (Fin p)) P]
   [SmoothManifoldWithCorners (𝓑 p) P]

But now I need to work out how to say there is a chart on a manifold so I parked this and tried to prove the composition of 2 continuous maps is continuous. I have this

variable {X Y Z : Type} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]

theorem compositionOfContinuousFunctions {f : X β†’ Y} {g : Y -> Z} (hf : Continuous f) (hg : Continuous g) (IsOpen s) :=
  IsOpen s
  IsOpen (g ⁻¹' s)
  IsOpen (f ⁻¹' (g ⁻¹' s))
  Continuous (g ∘ f)

And lean seems happy with it but did I actually prove anything?

Luigi Massacci (Sep 17 2024 at 10:21):

Lean seems happy with it? I’m surprised because your theorem doesn’t have a type

Luigi Massacci (Sep 17 2024 at 10:21):

I didn’t know that was possible

Luigi Massacci (Sep 17 2024 at 10:22):

Also you haven’t declared s anywhere, among other problems. Are you sure you aren’t getting any syntax errors?

Luigi Massacci (Sep 17 2024 at 10:25):

/have you read #mil? It might be helpful

Dominic Steinitz (Sep 17 2024 at 10:26):

Indeed I by scrolling right I can see a syntax error. I am still getting used to the user experience of VS Code.

Dominic Steinitz (Sep 17 2024 at 10:27):

Luigi Massacci said:

/have you read #mil? It might be helpful

I am reading it but I wanted to actually write a proof.

Ruben Van de Velde (Sep 17 2024 at 10:29):

Try starting with this: 

variable {X Y Z : Type} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]

theorem compositionOfContinuousFunctions {f : X β†’ Y} {g : Y -> Z} (hf : Continuous f) (hg : Continuous g) :
    Continuous (g ∘ f) := by
  sorry

Dominic Steinitz (Sep 17 2024 at 13:22):

Ruben Van de Velde said:

Try starting with this: 

variable {X Y Z : Type} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]

theorem compositionOfContinuousFunctions {f : X β†’ Y} {g : Y -> Z} (hf : Continuous f) (hg : Continuous g) :
    Continuous (g ∘ f) := by
  sorry

Thank you - I am this far along the path

theorem compositionOfContinuousFunctions {f : X β†’ Y} {g : Y -> Z} (hf : Continuous f) (hg : Continuous g) (hS : IsOpen S) :
    Continuous (g ∘ f) := by
    have hg_preimage : IsOpen (g ⁻¹' S) := hg.isOpen_preimage S hS
    have fg_preimage : IsOpen (f⁻¹' (g⁻¹' S)) := hf.isOpen_preimage (g⁻¹' S) hg_preimage
    sorry

So now I need to say that g \circ f is continuous because the pre-image of an open set (under it) is open somehow.

Ruben Van de Velde (Sep 17 2024 at 13:27):

You brought back this set S, but there's nothing you can do with that in relation to the goal. Try this:

import Mathlib

variable {X Y Z : Type} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]

theorem compositionOfContinuousFunctions {f : X β†’ Y} {g : Y -> Z} (hf : Continuous f) (hg : Continuous g) :
    Continuous (g ∘ f) := by
  rw [continuous_def] at *
  intro s hs
  sorry

Dominic Steinitz (Sep 17 2024 at 15:41):

Well I have this but crikey there's a lot going on behind the scenes (which I will write up). And it takes a bit of squinting to see that it looks like the proof you would normally see in a book or in an undergraduate course. Thanks for your help.

theorem compositionOfContinuousFunctions {f : X β†’ Y} {g : Y β†’ Z} (hf : Continuous f) (hg : Continuous g) :
    Continuous (g ∘ f) := by
  rw [continuous_def] at *
  intro s hs
  have hg_preimage : IsOpen (g ⁻¹' s) := hg s hs
  exact hf (g ⁻¹' s) hg_preimage

Kevin Buzzard (Sep 17 2024 at 17:57):

Is this really squinting? Not once you're familiar with a few basic tactics. This is literally the proof I teach to undergrads.

import Mathlib

variable {X Y Z : Type} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]

-- the composite of continuous functions is continuous
theorem compositionOfContinuousFunctions {f : X β†’ Y} {g : Y -> Z} (hf : Continuous f) (hg : Continuous g) :
    Continuous (g ∘ f) := by
  -- By definition of continuity, we need to show that the preimage of an open set is open
  rw [continuous_def] at *
  -- so let U be an open set in Z
  intro U hU
  -- and let V be its preimage
  let V := g ⁻¹' U
  -- By continuity of g, V is open
  have hV : IsOpen V := hg U hU
  -- By continuity of f, we deduce the result
  exact hf V hV

Dominic Steinitz (Sep 18 2024 at 09:05):

Well de gustibus but no doubt in a few months time of working in Lean such a proof will be lucidity itself. I am impressed by your undergraduates.

Here's my "squinting":

So rw [continuous_def] rewrites Continuous as given by the definition

β”Œβ”€β”€β”€β”€
β”‚ Continuous f ↔ βˆ€ s, IsOpen s β†’ IsOpen (f ⁻¹' s)
└────

By saying intro s hs, Lean somehow knows that ss is meant to be an open set in the codomain of g∘fg \circ f, which is ZZ (and hs is a proof of this?).

g ⁻¹' U is open by the proof(?) hg that g is continuous to the open set s(with a proof of openness hs).

β”Œβ”€β”€β”€β”€
β”‚ IsOpen (g ⁻¹' s) := hg s hs
└────

We next show that f ⁻¹' (g ⁻¹' s) is open using the proof(?) hf on the open set (g ⁻¹' s) (which is open by hg_preimage).

And we are done.

Riccardo Brasca (Sep 18 2024 at 09:14):

When you write intro s hs Lean looks at the goal, this is how it can understand that s must be a term of type Set Z.

Riccardo Brasca (Sep 18 2024 at 09:16):

We use the terminology "proof" even for what we would normally call "assumptions". For example writing

example (n : Nat) (hn : 0 < n) : ...

we say "hn is a proof that n is positive". This is because of the type theory Lean is based on, you think it is just terminology.

Kevin Buzzard (Sep 18 2024 at 09:24):

My claim regarding undergraduates is only "the comments indicate exactly the proof which I'd teach to undergraduates on the board in a non Lean situation". I'm just observing that I'm translating exactly the normal proof into Lean, nothing more subtle is going on. Your squinting looks spot on to me. Two $s for LaTeX in Zulip for some reason: $$s$$ not $s$ gives you ss (I am now so used to this that I'm constantly writing two dollars in LaTeX documents and accidentally starting new lines :-/ ).

Dominic Steinitz (Sep 24 2024 at 08:38):

I have got as far as this

import Mathlib

open Manifold

variable
  (m : β„•) {M : Type*}
  [TopologicalSpace M]
  [ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
  [SmoothManifoldWithCorners (𝓑 m) M]

variable
  (n : β„•) {N : Type*}
  [TopologicalSpace N]
  [ChartedSpace (EuclideanSpace ℝ (Fin n)) N]
  [SmoothManifoldWithCorners (𝓑 n) N]

variable
  (p : β„•) {P : Type*}
  [TopologicalSpace P]
  [ChartedSpace (EuclideanSpace ℝ (Fin p)) P]
  [SmoothManifoldWithCorners (𝓑 p) P]

-- Definition of a smooth map using charts of the manifolds
def smooth_map (f : M β†’ N) : Prop :=
  βˆ€ (x : M), Smooth (𝓑 m) (𝓑 n)
    ((chartAt (EuclideanSpace ℝ (Fin n)) (f x)).toFun ∘ f ∘ (chartAt (EuclideanSpace ℝ (Fin m)) x).invFun)

-- Theorem: Composition of smooth maps is smooth
theorem smooth_composition_of_smooth_maps {f : M β†’ N} {g : N β†’ P}
  (hf : smooth_map m n f) (hg : smooth_map n p g) : smooth_map m p (g ∘ f) :=
  fun x =>
    let Ο† := chartAt (EuclideanSpace ℝ (Fin p)) (g (f x))
    let ψ := chartAt (EuclideanSpace ℝ (Fin n)) (f x)
    let Ο‡ := chartAt (EuclideanSpace ℝ (Fin m)) x
    -- Show ψ ∘ f ∘ χ⁻¹ is smooth
    have h1 : Smooth (𝓑 m) (𝓑 n) (ψ.toFun ∘ f ∘ Ο‡.invFun) := hf x
    -- Show Ο† ∘ g ∘ ψ⁻¹ is smooth
    have h2 : Smooth (𝓑 n) (𝓑 p) (Ο†.toFun ∘ g ∘ ψ.invFun) := hg (f x)
    -- Now, combine these to show Ο† ∘ g ∘ f ∘ χ⁻¹ is smooth
    have : (Ο†.toFun ∘ g ∘ ψ.invFun ∘ ψ.toFun ∘ f ∘ Ο‡.invFun) =
           (Ο†.toFun ∘ g ∘ f ∘ Ο‡.invFun) := by simp [Function.comp]
    sorry

but get a red squiggly line under by simp [Function.comp] and in Lean Infoview I get

unsolved goals
m : β„•
M : Type u_1
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace (EuclideanSpace ℝ (Fin m)) M
inst✝⁢ : SmoothManifoldWithCorners π“˜(ℝ, EuclideanSpace ℝ (Fin m)) M
n : β„•
N : Type u_2
inst✝⁡ : TopologicalSpace N
inst✝⁴ : ChartedSpace (EuclideanSpace ℝ (Fin n)) N
inst✝³ : SmoothManifoldWithCorners π“˜(ℝ, EuclideanSpace ℝ (Fin n)) N
p : β„•
P : Type u_3
inst✝² : TopologicalSpace P
inst✝¹ : ChartedSpace (EuclideanSpace ℝ (Fin p)) P
inst✝ : SmoothManifoldWithCorners π“˜(ℝ, EuclideanSpace ℝ (Fin p)) P
f : M β†’ N
g : N β†’ P
hf : smooth_map m n f
hg : smooth_map n p g
x : M
Ο† : PartialHomeomorph P (EuclideanSpace ℝ (Fin p)) := chartAt (EuclideanSpace ℝ (Fin p)) (g (f x))
ψ : PartialHomeomorph N (EuclideanSpace ℝ (Fin n)) := chartAt (EuclideanSpace ℝ (Fin n)) (f x)
Ο‡ : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)) := chartAt (EuclideanSpace ℝ (Fin m)) x
h1 : Smooth π“˜(ℝ, EuclideanSpace ℝ (Fin m)) π“˜(ℝ, EuclideanSpace ℝ (Fin n)) (β†‘Οˆ.toPartialEquiv ∘ f ∘ Ο‡.invFun)
h2 : Smooth π“˜(ℝ, EuclideanSpace ℝ (Fin n)) π“˜(ℝ, EuclideanSpace ℝ (Fin p)) (↑φ.toPartialEquiv ∘ g ∘ ψ.invFun)
⊒ ↑φ ∘ g ∘ β†‘Οˆ.symm ∘ β†‘Οˆ ∘ f ∘ ↑χ.symm = ↑φ ∘ g ∘ f ∘ ↑χ.symm

I am not sure what this is telling me.

Ruben Van de Velde (Sep 24 2024 at 08:46):

Sounds like you haven't solved the goal. You'll need to cancel out the psis in the middle, but probably you need to move some implicit parentheses first

Kevin Buzzard (Sep 24 2024 at 09:28):

I am not sure what this is telling me.

It's telling you "right now, this is what needs proving" (and remember that there are implicit brackets everywhere as Ruben says).

Dominic Steinitz (Sep 24 2024 at 13:48):

I don't know what is meant by implicit brackets - I tried this

have h_eq : βˆ€ y ∈ ψ.source, ψ.invFun (ψ.toFun y) = y :=
      by intro y hy; exact PartialHomeomorph.left_inv ψ hy
    -- Show that Ο† ∘ g ∘ ψ⁻¹ ∘ ψ ∘ f ∘ χ⁻¹ = Ο† ∘ g ∘ f ∘ χ⁻¹ using the fact above that ψ⁻¹ ∘ ψ = id
    have h_nested : βˆ€ x ∈ Ο‡.target, Ο†.toFun (g (ψ.invFun (ψ.toFun (f (Ο‡.invFun x))))) =
                                    Ο†.toFun (g (f (Ο‡.invFun x))) := h_eq

So now my brackets are explicit?

At least I proved that Οˆβˆ’1∘ψ=1\psi^{-1} \circ \psi = \mathbb{1}. But how do I use it to prove that fβˆ˜Οˆβˆ’1∘ψ∘g=f∘gf \circ \psi^{-1} \circ \psi \circ g = f \circ g?

Ruben Van de Velde (Sep 24 2024 at 14:15):

The point is that f ∘ g ∘ h means f ∘ (g ∘ h). Notably, there isn't technically a subterm f ∘ g. I'm surprised to see there's no Function.comp_assoc though.

You can instead move to reasoning about the function applied to a general element rather than about the function itself:

    have : (Ο†.toFun ∘ g ∘ ψ.invFun ∘ ψ.toFun ∘ f ∘ Ο‡.invFun) =
           (Ο†.toFun ∘ g ∘ f ∘ Ο‡.invFun) := by
      ext x
      simp
      rw [PartialHomeomorph.left_inv]
      sorry

Luigi Massacci (Sep 24 2024 at 14:18):

Ah you beat me to it

Luigi Massacci (Sep 24 2024 at 14:19):

There is Function.comp.assoc, I’m more surprised there is no cancellation lemma using comp and you need to pass by points

Luigi Massacci (Sep 24 2024 at 14:20):

Though the Partial makes me think that probably there’s some requirement that the point be in the domain of whatever, so maybe it makes sense

Ruben Van de Velde (Sep 24 2024 at 14:26):

We used to have an assoc_rw tactic in lean 3, but it seems like it wasn't ported

Dominic Steinitz (Sep 25 2024 at 10:41):

Ruben Van de Velde said:

    have : (Ο†.toFun ∘ g ∘ ψ.invFun ∘ ψ.toFun ∘ f ∘ Ο‡.invFun) =
           (Ο†.toFun ∘ g ∘ f ∘ Ο‡.invFun) := by
      ext x
      simp
      rw [PartialHomeomorph.left_inv]
      sorry

So I need to prove f (↑χ.symm x) ∈ ψ.source which I interpret as f (Ο‡.invFun x) ∈ ψ.source. But this may not necessarily be true so we should make the open set at x a bit smaller

    let V_f_x := ψ.source
    let U_x := Ο‡.source ∩ f ⁻¹' V_f_x

But now how do I create a new chart? I'd like to do something like

let chart_U : chart (EuclideanSpace ℝ (Fin m)) (M) :=
  { toFun := Ο‡.toFun,
    invFun := Ο‡.invFun,
    source := U_x,
    target := Ο‡.target }

but I have been unable to find out if this can be done at all or whether I should be approaching the problem differently.

Kevin Buzzard (Sep 25 2024 at 12:30):

(deleted)

Dominic Steinitz (Sep 25 2024 at 14:06):

I now have this

theorem smooth_composition_of_smooth_maps {f : M β†’ N} {g : N β†’ P}
  (hf : smooth_map m n f) (hg : smooth_map n p g) : smooth_map m p (g ∘ f) :=
  fun x =>
    let Ο† := chartAt (EuclideanSpace ℝ (Fin p)) (g (f x))
    let ψ := chartAt (EuclideanSpace ℝ (Fin n)) (f x)
    let Ο‡ := chartAt (EuclideanSpace ℝ (Fin m)) x
    -- Make sure all values in the source of Ο‡ get mapped into the source of ψ by
    -- making the source smaller.
    let Ο‡.source := Ο‡.source ∩ f ⁻¹' ψ.source
    have h_eq : βˆ€ y ∈ ψ.source, ψ.invFun (ψ.toFun y) = y :=
      by intro y hy; exact PartialHomeomorph.left_inv ψ hy
    have h_nested : βˆ€ x ∈ Ο‡.target, Ο†.toFun (g (ψ.invFun (ψ.toFun (f (Ο‡.invFun x))))) =
                                    Ο†.toFun (g (f (Ο‡.invFun x))) := by
      intro x hx
      have hf_in_ψ : f (Ο‡.invFun x) ∈ ψ.source := sorry -- this is now true but what
                                                        -- does lean want
      rw [h_eq (f (Ο‡.invFun x)) hf_in_ψ]
    sorry

I was rather surprised (as a functional programmer) that I could do this but maybe there is an implicit monad somehow. Be that as it may, how do I tell lean that f (Ο‡.invFun x) ∈ ψ.source?

Luigi Massacci (Sep 25 2024 at 14:15):

I'm from phone, but I would hazard a guess that your new Ο‡.source is nonsense (in the sense it's become untied to Ο‡)

Luigi Massacci (Sep 25 2024 at 14:15):

You need to restrict the chart

Ruben Van de Velde (Sep 25 2024 at 14:20):

Yeah, you're introducing a new binding called literally Ο‡.source

Dominic Steinitz (Sep 25 2024 at 16:07):

Luigi Massacci said:

You need to restrict the chart

Is it obvious how to do that? I've looked through various bits of code but nothing jumped out.

Dominic Steinitz (Sep 25 2024 at 16:24):

I now have

-- Make sure all values in the source of Ο‡ get mapped into the source of ψ by
    -- making the source smaller.
    let ΞΆ := Ο‡.restr (Ο‡.source ∩ f ⁻¹' ψ.source)
    have h_eq : βˆ€ y ∈ ψ.source, ψ.invFun (ψ.toFun y) = y :=
      by intro y hy; exact PartialHomeomorph.left_inv ψ hy
    have h_nested : βˆ€ x ∈ ΞΆ.target, Ο†.toFun (g (ψ.invFun (ψ.toFun (f (ΞΆ.invFun x))))) =
                                    Ο†.toFun (g (f (ΞΆ.invFun x))) := by
      intro x hx
      have hf_in_ψ : f (΢.invFun x) ∈ ψ.source := sorry -- this is now true but what
                                                        -- does lean want
      rw [h_eq (f (΢.invFun x)) hf_in_ψ]
    sorry

But replacing the first sorry by "by exact" fails :-(

Dominic Steinitz (Sep 25 2024 at 16:43):

I have tried

have hf_in_ψ : f (΢.invFun x) ∈ ψ.source := by
        have h_΢_source : ΢.invFun x ∈ ΢.source := ΢.map_target hx
        exact h_ΞΆ_source.2

but get the error

type mismatch
  h_ΞΆ_source.right
has type
  ΞΆ.invFun x ∈ interior (Ο‡.source ∩ f ⁻¹' ψ.source) : Prop
but is expected to have type
  f (΢.invFun x) ∈ ψ.source : Prop

How do I persuade lean that the latter follows from the former?

Riccardo Brasca (Sep 25 2024 at 21:20):

I think that the way of doing it is: why this is mathematically true? Because interior S is a subset of S, and X ∩ Y is a subset of X. These two results are surely in mathlib, probably very close to the definition of the two operators.

Dominic Steinitz (Sep 26 2024 at 10:08):

Riccardo Brasca said:

I think that the way of doing it is: why this is mathematically true? Because interior S is a subset of S, and X ∩ Y is a subset of X. These two results are surely in mathlib, probably very close to the definition of the two operators.

The maths I don't have a problem with. It's convincing lean that is my problem. I can't even convince it that the intersection of the two open sets that I have is open

have h_open : IsOpen (Ο‡.source ∩ f ⁻¹' ψ.source) := IsOpen.inter (Ο‡.open_source) (????)

I presumably have a proof that ψ\psi.source is open (ψ\psi.open_source) but do I further need a proof that the preimage of an open set is open? Do I need to prove f is continuous? We only have a proof that it is smooth.

Riccardo Brasca (Sep 26 2024 at 10:17):

What I mean is that mathlib is set up in a way the usual math proof should work. What I usually do is to think why something is true mathematically, and look for the results I need in mathlib.

Riccardo Brasca (Sep 26 2024 at 10:17):

For example, the fact that a smooth map is continuous is surely there, maybe exact? can find it

Riccardo Brasca (Sep 26 2024 at 10:23):

Indeed

import Mathlib

variable  {π•œ : Type*} [NontriviallyNormedField π•œ] {E : Type*} [NormedAddCommGroup E]
  [NormedSpace π•œ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners π•œ E H) {M : Type*}
  [TopologicalSpace M] [ChartedSpace H M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace π•œ E']
  {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners π•œ E' H') {M' : Type*}
  [TopologicalSpace M'] [ChartedSpace H' M']

example (f : M β†’ M') (hf : Smooth I I' f) : Continuous f := by
  exact?

works (the answer is docs#ContMDiff.continuous)

Riccardo Brasca (Sep 26 2024 at 10:25):

Note that the names are set up in a way that hf.continuous is the fact that f is continuous, so this is very convenient (one could also have guessed this by following our name convention)

Riccardo Brasca (Sep 26 2024 at 10:25):

in general finding results in mathlib is a nontrivial task, but it gets easier and easier once one knows the tricks

Dominic Steinitz (Sep 26 2024 at 10:33):

I simultaneously found Continuous but I have defined a map to be smooth only if it is smooth on its charts

def smooth_map (f : M β†’ N) : Prop :=
  βˆ€ (x : M), Smooth (𝓑 m) (𝓑 n)
    ((chartAt (EuclideanSpace ℝ (Fin n)) (f x)).toFun ∘ f ∘ (chartAt (EuclideanSpace ℝ (Fin m)) x).invFun)

So although we know f is continuous from my definition, I assume that lean does not know it and I have to prove it?

Riccardo Brasca (Sep 26 2024 at 10:34):

Well, if you gave a new definition then Lean does not know anything about it.

Riccardo Brasca (Sep 26 2024 at 10:36):

I mean, you have to prove all the basic results about a new definition before starting using it. This is called the API of a definition, you can see in mathlib that this is done after basically every definition.

Riccardo Brasca (Sep 26 2024 at 10:36):

I am not saying it is hard, but it has to do be done.

Dominic Steinitz (Sep 26 2024 at 10:39):

Thanks very much for your help and I am learning a lot but I somehow thought proving the composition of smooth maps (defined as smooth if it is smooth on its charts - I think this is pretty standard) is smooth would be an easy intro to help me learn lean :laughter_tears:

Riccardo Brasca (Sep 26 2024 at 10:41):

I am not an expert of that part of the library, but differential manifold are surely hard to formalize, so I am not surprised this is not so easy. Sometimes we don't know how to translate arguments that are easy on paper to Lean... it's unfortunate, but it also what make formalization challenging!

Last updated: May 02 2025 at 03:31 UTC