The derivative of a chart is injective

Stream: Is there code for X?

[Dominic Steinitz]

I have the skeleton below and I have seen https://github.com/leanprover-community/mathlib4/pull/9273 although I am not clear how to apply the latter.

import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
import Mathlib.Geometry.Manifold.PartitionOfUnity
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Geometry.Manifold.VectorBundle.Tangent

variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB]
  {IB : ModelWithCorners ℝ EB HB}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B] [IsManifold IB ⊤ B]

lemma chart_mfderiv_injective (i p : B) (hp : p ∈ (chartAt HB i).source) :
    Function.Injective (mfderiv IB (modelWithCornersSelf ℝ EB) (extChartAt IB i) p) := by
  let ψ := extChartAt IB i
  let dψ := mfderiv IB (modelWithCornersSelf ℝ EB) ψ p
  let χ := ψ.symm
  let dχ := mfderiv (modelWithCornersSelf ℝ EB) IB ψ.symm (ψ p)

  have deriv_comp_eq_id : p ∈ ψ.source →
    mfderiv IB IB (χ ∘ ψ) p = ContinuousLinearMap.id ℝ (TangentSpace IB p) := by
    intro hp
    have : χ ∘ ψ = fun x ↦ x := by
      ext x
      exact sorry
    rw [this]
    exact mfderiv_id

  have h1 : MDifferentiableAt IB (modelWithCornersSelf ℝ EB) ψ p := by exact sorry
  have h2 : MDifferentiableAt (modelWithCornersSelf ℝ EB) IB χ (ψ p) := by exact sorry

  have chain : p ∈ ψ.source →
      mfderiv IB IB (χ ∘ ψ) p = dχ ∘L dψ := by
    intro hp
    have : mfderiv IB IB (χ ∘ ψ) p =
        (mfderiv (modelWithCornersSelf ℝ EB) IB χ (ψ p)).comp
        (mfderiv IB (modelWithCornersSelf ℝ EB) ψ p) := mfderiv_comp p h2 h1
    exact this

  have left_inv : p ∈ ψ.source → dχ ∘L dψ = ContinuousLinearMap.id ℝ (TangentSpace IB p) := by
    intro hp
    calc dχ ∘L dψ =  mfderiv IB IB (χ ∘ ψ) p := (chain hp).symm
         _ =  ContinuousLinearMap.id ℝ (TangentSpace IB p) := deriv_comp_eq_id hp

  sorry

[Michael Rothgang]

Do you assume your manifold has boundary/that you are working with an interior point? #9273 needs that assumption...

[Michael Rothgang]

Have you seen docs#isInvertible_mfderiv_extChartAt?

[Michael Rothgang]

I believe the latter answers your question.

[Dominic Steinitz]

In the end I solved my problem like this (exact inj (inj (inj (inj rfl))) was suggested by exact?):

import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
import Mathlib.Geometry.Manifold.PartitionOfUnity
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Geometry.Manifold.VectorBundle.Tangent
import Mathlib.Geometry.Manifold.MFDeriv.Atlas
import Mathlib.Topology.Algebra.Module.Equiv

variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB]
  {IB : ModelWithCorners ℝ EB HB}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B] [IsManifold IB ⊤ B]

noncomputable
def g (i : B) (p : B) (v w : (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p) : ℝ :=
  let ψ := extChartAt IB i
  let dψ := mfderiv IB (modelWithCornersSelf ℝ EB) ψ p
  let x : EB := dψ v
  let y : EB := dψ w
  @Inner.inner ℝ EB _ x y

def linearEquivToSemiLinearEquiv
  {E F : Type*} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F]
  [TopologicalSpace E] [TopologicalSpace F]
  (e : E ≃L[ℝ] F) :
  E ≃SL[RingHom.id ℝ] F :=
{ toFun := e.toFun,
  invFun := e.invFun,
  map_add' := e.map_add,
  map_smul' := by intro r x; exact e.map_smul r x,
  left_inv := e.left_inv,
  right_inv := e.right_inv }

lemma g_pos (i p : B) (hp : p ∈ (extChartAt IB i).source)
            (v : (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p) :
  v ≠ 0 → 0 < g i p v v := by
  intro hv
  unfold g
  simp only
  let ψ := extChartAt IB i
  let dψ := mfderiv IB (modelWithCornersSelf ℝ EB) ψ p
  let x : EB := dψ v
  have h_invert : dψ.IsInvertible := isInvertible_mfderiv_extChartAt hp
  rcases h_invert with ⟨inv, left_inv⟩
  let e := linearEquivToSemiLinearEquiv inv
  have inj : Function.Injective e := ContinuousLinearEquiv.injective e
  have h1 : e v = dψ v := by
    unfold e
    rw[<-left_inv]
    exact inj (inj (inj (inj rfl)))
  have hx : x ≠ 0 := by
    intro h
    have h2 : e v = e 0 := by
      rw [h1]
      simp [x, h]
    have h3 := inj h2
    exact hv h3
  exact real_inner_self_pos.mpr hx

[Michael Rothgang]

Well, I'm glad the lemma helped. I just took a look at your code, and I think it can be simplified quite a bit.

[Michael Rothgang]

• why are you introducing linearEquivToSemiLinearEquiv? I think you can just remove it, and use inv instead of e all the time

[Michael Rothgang]

• you can shorten the definition of g a bit by inlining some of the helper definitions:

noncomputable def g (i : B) (p : B) (v w : (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p) : ℝ :=
  letI dψ := mfderiv IB (modelWithCornersSelf ℝ EB) (extChartAt IB i) p
  @Inner.inner ℝ EB _ (dψ v) (dψ w)

[Michael Rothgang]

I'm also using letI instead of let; that means you can skip unfolding g later

[Michael Rothgang]

• when stating g_pos, you want to apply the rule "hypothesis left of colon" from the style guide, i.e. start like this

lemma g_pos (i p : B) (hp : p ∈ (extChartAt IB i).source) (v : (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p) (hv : v ≠ 0) :
    0 < g i p v v := by

[Michael Rothgang]

• use can use notation: if you open Manifold, there's a nicer notation for modelWithCornersSelf available
• you're only using x once; I'd just inline that use

[Michael Rothgang]

In short, this is how your code can be rewritten without any substantial changes:

import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
import Mathlib.Geometry.Manifold.PartitionOfUnity
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Geometry.Manifold.VectorBundle.Tangent
import Mathlib.Geometry.Manifold.MFDeriv.Atlas
import Mathlib.Geometry.Manifold.Notation
import Mathlib.Topology.Algebra.Module.Equiv

variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB]
  {IB : ModelWithCorners ℝ EB HB}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B] [IsManifold IB ⊤ B]

open Manifold

noncomputable def g (i : B) (p : B) (v w : (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p) : ℝ :=
  letI dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  @Inner.inner ℝ EB _ (dψ v) (dψ w)

lemma g_pos (i p : B) (hp : p ∈ (extChartAt IB i).source) (v : (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p) (hv : v ≠ 0) :
    0 < g i p v v := by
  let ψ := extChartAt IB i
  let dψ := mfderiv IB 𝓘(ℝ, EB) ψ p
  have h_invert : dψ.IsInvertible := isInvertible_mfderiv_extChartAt hp
  obtain ⟨inv, left_inv⟩ := h_invert
  have inj : Function.Injective inv := inv.injective
  have h1 : inv v = dψ v := by
    rw[← left_inv]
    exact inj (inj (inj (inj rfl)))
  have hx : dψ v ≠ 0 := by
    intro h
    have h2 : inv v = inv 0 := by simp [h, h1]
    exact hv (inj h2)
  exact real_inner_self_pos.mpr hx

[Michael Rothgang]

After #30307, you'll also be able to write let dψ := mfderiv% ψ p instead

[Michael Rothgang]

Looking at your code, something is definitely not quite right: you need a lot of underscores about the tangent space, and inlining h_invert also fails. I have an inkling you're putting the wrong set of typeclasses at the beginning, but would need to investigate a bit more.

[Dominic Steinitz]

Michael Rothgang said:

Looking at your code, something is definitely not quite right: you need a lot of underscores about the tangent space, and inlining h_invert also fails. I have an inkling you're putting the wrong set of typeclasses at the beginning, but would need to investigate a bit more.

I am using tangent spaces rather than something more abstract as I feel on familiar ground. Once I have proved a Riemannian metric exists for this example then I will generalise and maybe the weirdness will then make its cause known.

[Michael Rothgang]

Sure, I know (and that's fine). I believe your current typeclasses are also off, but would need some (more) quiet time to try to diagnose why.

[Michael Rothgang]

That said, this issue will probably not manifest as-is for general vector bundles - so it's not strictly needed now.