Zulip Chat Archive

Stream: maths

Topic: Convert smooth `M โ†’ ๐•Šโฟ` & `M โ†’ โ„โฟโบยน` to smooth `M โ†’ T๐•Šโฟ`

Miyahara Kล (Dec 18 2024 at 09:32):

I defined a M โ†’ T๐•Šโฟ function from smooth f : M โ†’ ๐•Šโฟ & g : M โ†’ โ„โฟโบยน which satisfy โˆ€ x, โŸชf x, g xโŸซ_โ„ = 0 and proved that it is smooth.
I don't have the energy to maintain a pull request of this, but I hope it helps!
Mathlib SHA: 2144977fb121989a45d3f6e4d74fd8ab2350db3e

import Mathlib.Geometry.Manifold.VectorBundle.Tangent
import Mathlib.Geometry.Manifold.Instances.Sphere

open Metric Module Function

open scoped Manifold ContDiff InnerProductSpace

open private stereographic'_neg from Mathlib.Geometry.Manifold.Instances.Sphere

noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace โ„ E] (v : E)

theorem contDiff_uncurry_stereoInvFunAux : ContDiff โ„ โˆž (uncurry (stereoInvFunAux (E := E))) := by
  have hโ‚€ : ContDiff โ„ โˆž fun p : E ร— E => โ€–p.2โ€– ^ 2 := contDiff_norm_sq โ„ |>.comp contDiff_snd
  have hโ‚ : ContDiff โ„ โˆž fun p : E ร— E => (โ€–p.2โ€– ^ 2 + 4)โปยน := by
    refine (hโ‚€.add contDiff_const).inv ?_
    intro x
    nlinarith
  have hโ‚‚ : ContDiff โ„ โˆž fun p : E ร— E => (4 : โ„) โ€ข p.2 + (โ€–p.2โ€– ^ 2 - 4) โ€ข p.1 := by
    refine (contDiff_const.smul contDiff_snd).add ?_
    exact (hโ‚€.sub contDiff_const).smul contDiff_fst
  exact hโ‚.smul hโ‚‚

theorem coe_sphere_comp_stereoInvFun (hv : โ€–vโ€– = 1) :
    ((โ†‘) : โ†ฅ(sphere (0 : E) 1) โ†’ E) โˆ˜ stereoInvFun hv = stereoInvFunAux v โˆ˜ Subtype.val :=
  rfl

variable {F : Type*} [NormedAddCommGroup F] [NormedSpace โ„ F]
variable {H : Type*} [TopologicalSpace H] {I : ModelWithCorners โ„ F H}
variable {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M]

def sphereTangentMap (n : โ„•) [Fact (finrank โ„ E = n + 1)]
    (f : M โ†’ sphere (0 : E) 1) (g : M โ†’ E)
    (hf : โˆ€ x, โŸช(โ†‘(f x) : E), g xโŸซ_โ„ = 0) (x : M) : TangentBundle (๐“ก n) (sphere (0 : E) 1) :=
  โŸจf x,
    (OrthonormalBasis.fromOrthogonalSpanSingleton n (ne_zero_of_mem_unit_sphere (-f x))).repr
      (โŸจg x, Submodule.mem_orthogonal_singleton_iff_inner_right.mpr (by simp [hf x])โŸฉ :
        (โ„ โˆ™ (-โ†‘(f x) : E))แ—ฎ)โŸฉ

omit [TopologicalSpace M] in
@[simp]
theorem sphereTangentMap_proj (n : โ„•) [Fact (finrank โ„ E = n + 1)]
    (f : M โ†’ sphere (0 : E) 1) (g : M โ†’ E)
    (hf : โˆ€ x, โŸช(โ†‘(f x) : E), g xโŸซ_โ„ = 0) (x : M) : (sphereTangentMap n f g hf x).proj = f x :=
  rfl

omit [TopologicalSpace M] in
@[simp]
theorem mfderiv_coe_sphere_sphereTangentMap_snd (n : โ„•) [Fact (finrank โ„ E = n + 1)]
    (f : M โ†’ sphere (0 : E) 1) (g : M โ†’ E)
    (hf : โˆ€ x, โŸช(โ†‘(f x) : E), g xโŸซ_โ„ = 0) (x : M) :
    mfderiv (๐“ก n) ๐“˜(โ„, E) ((โ†‘) : sphere (0 : E) 1 โ†’ E) (f x) (sphereTangentMap n f g hf x).snd =
      g x := by
  rw [((contMDiff_coe_sphere (f x)).mdifferentiableAt le_top).mfderiv]
  simp only [writtenInExtChartAt, extChartAt, PartialHomeomorph.extend,
    PartialHomeomorph.refl_partialEquiv, PartialEquiv.refl_source,
    PartialHomeomorph.singletonChartedSpace_chartAt_eq, modelWithCornersSelf_partialEquiv,
    PartialEquiv.trans_refl, PartialEquiv.refl_coe, PartialHomeomorph.coe_coe_symm,
    CompTriple.comp_eq, modelWithCornersSelf_coe, Set.range_id, PartialHomeomorph.toFun_eq_coe,
    chartAt, ChartedSpace.chartAt, stereographic'_neg, fderivWithin_univ]
  simp only [chartAt, ChartedSpace.chartAt, stereographic', coe_neg_sphere, stereographic,
    PartialHomeomorph.coe_trans_symm, PartialHomeomorph.mk_coe_symm, PartialEquiv.coe_symm_mk,
    Homeomorph.toPartialHomeomorph_symm_apply, LinearIsometryEquiv.toHomeomorph_symm,
    LinearIsometryEquiv.coe_toHomeomorph, โ† comp_assoc, coe_sphere_comp_stereoInvFun]
  simp only [comp_assoc]
  conv =>
    enter [1, 1]
    tactic =>
      rw [fderiv_comp]
      ยท exact contDiff_stereoInvFunAux.contDiffAt.differentiableAt (right_eq_inf.mp rfl)
      ยท exact
          (((โ„ โˆ™ (-โ†‘(f x) : E))แ—ฎ).subtypeL.comp
            (OrthonormalBasis.fromOrthogonalSpanSingleton (๐•œ := โ„) (E := E) n
              (ne_zero_of_mem_unit_sphere (-f x))
            ).repr.symm.toContinuousLinearEquiv.toContinuousLinearMap).differentiableAt
  conv =>
    enter [1, 1, 2]
    exact
      (((โ„ โˆ™ (-โ†‘(f x) : E))แ—ฎ).subtypeL.comp
        (OrthonormalBasis.fromOrthogonalSpanSingleton (๐•œ := โ„) (E := E) n
            (ne_zero_of_mem_unit_sphere (-f x))
          ).repr.symm.toContinuousLinearEquiv.toContinuousLinearMap).fderiv
  simp [sphereTangentMap, TangentSpace, (hasFDerivAt_stereoInvFunAux (-(โ†‘(f x) : E))).fderiv]

omit [SmoothManifoldWithCorners I M] in
private theorem contMDiff_sphereTangentMap_aux {n : โ„•} [Fact (finrank โ„ E = n + 1)] {m : โ„•โˆž}
    {f : M โ†’ โ†ฅ(sphere (0 : E) 1)} {g : M โ†’ E}
    (hf : ContMDiff I (๐“ก n) m f) (hf' : โˆ€ x, โŸช(โ†‘(f x) : E), g xโŸซ_โ„ = 0)
    (hg : ContMDiff I ๐“˜(โ„, E) m g) (p : โ†ฅ(sphere (0 : E) 1)) :
    ContMDiffOn I ๐“˜(โ„, EuclideanSpace โ„ (Fin n)) m
      (fun x =>
        (fderiv โ„
            (โ‡‘(chartAt (EuclideanSpace โ„ (Fin n)) p) โˆ˜
              โ‡‘(chartAt (EuclideanSpace โ„ (Fin n)) (f x)).symm) 0)
          (sphereTangentMap n f g hf' x).snd)
      (f โปยน' (chartAt (EuclideanSpace โ„ (Fin n)) p).source) := by
  conv =>
    enter [4, x, 1, 2]
    change โ‡‘(stereographic' n (-p)) โˆ˜ โ‡‘(stereographic' n (-f x)).symm
    simp only [stereographic', coe_neg_sphere, stereographic,
      PartialHomeomorph.coe_trans, Homeomorph.toPartialHomeomorph_apply,
      LinearIsometryEquiv.coe_toHomeomorph, PartialHomeomorph.mk_coe,
      PartialHomeomorph.coe_trans_symm, PartialHomeomorph.mk_coe_symm, PartialEquiv.coe_symm_mk,
      Homeomorph.toPartialHomeomorph_symm_apply, LinearIsometryEquiv.toHomeomorph_symm,
      comp_assoc]
    simp only [โ† comp_assoc Subtype.val, coe_sphere_comp_stereoInvFun]
    simp only [โ† comp_assoc]
    simp only [comp_assoc _ Subtype.val, comp_assoc _ (stereoToFun (-(โ†‘p : E)))]
  conv =>
    tactic =>
      apply propext โˆ˜ contMDiffOn_congr
      intro x hx
      rw [fderiv_comp]
      ยท refine
          (OrthonormalBasis.fromOrthogonalSpanSingleton (๐•œ := โ„) (E := E) n
            (ne_zero_of_mem_unit_sphere (-p))
          ).repr.toContinuousLinearEquiv.toContinuousLinearMap.differentiableAt.comp _
            (DifferentiableAt.comp _ ?_
              (contDiff_stereoInvFunAux.contDiffAt.differentiableAt (right_eq_inf.mp rfl)))
        simp only [coe_neg_sphere, comp_apply, map_zero, ZeroMemClass.coe_zero,
          stereoInvFunAux_apply, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
          zero_pow, zero_add, smul_zero, zero_sub, smul_neg, neg_smul, neg_neg, inv_smul_smulโ‚€]
        refine
          ((contDiffOn_stereoToFun (E := E) (v := -(โ†‘p : E))).contDiffAt (IsOpen.mem_nhds ?_ ?_)
            ).differentiableAt (right_eq_inf.mp rfl)
        ยท exact
            (innerSL โ„ (-(โ†‘p : E))).continuous.isOpen_preimage {1}แถœ isOpen_compl_singleton
        ยท simp only [innerSL_apply, ne_eq, Set.mem_setOf_eq, โ† sphere_ext_iff, โ† coe_neg_sphere]
          simpa [chartAt, ChartedSpace.chartAt, eq_comm (a := f x)] using hx
      ยท exact
          (((โ„ โˆ™ (-โ†‘(f x) : E))แ—ฎ).subtypeL.comp
            (OrthonormalBasis.fromOrthogonalSpanSingleton (๐•œ := โ„) (E := E) n
              (ne_zero_of_mem_unit_sphere (-f x))
            ).repr.symm.toContinuousLinearEquiv.toContinuousLinearMap).differentiableAt
  conv =>
    enter [4, x, 1, 2]
    exact
      (((โ„ โˆ™ (-โ†‘(f x) : E))แ—ฎ).subtypeL.comp
        (OrthonormalBasis.fromOrthogonalSpanSingleton (๐•œ := โ„) (E := E) n
            (ne_zero_of_mem_unit_sphere (-f x))
          ).repr.symm.toContinuousLinearEquiv.toContinuousLinearMap).fderiv
  simp only [comp_apply, map_zero, ZeroMemClass.coe_zero, coe_neg_sphere, sphereTangentMap,
    ContinuousLinearMap.coe_comp', Submodule.coe_subtypeL', Submodule.coe_subtype,
    ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_toContinuousLinearEquiv,
    LinearIsometryEquiv.symm_apply_apply]
  refine ContMDiffOn.clm_apply (fun x hx => ContMDiffAt.contMDiffWithinAt ?_) hg.contMDiffOn
  conv =>
    arg 4
    change
      (fun x => fderiv โ„ ((OrthonormalBasis.fromOrthogonalSpanSingleton n
        (ne_zero_of_mem_unit_sphere (-p))).repr โˆ˜ stereoToFun (-(โ†‘p : E)) โˆ˜
          stereoInvFunAux (-x)) 0) โˆ˜ ((โ†‘) : โ†ฅ(sphere (0 : E) 1) โ†’ E) โˆ˜ f
  refine
    ContMDiffAt.comp _ (ContMDiffAt.of_le ?_ le_top)
      (((contMDiff_coe_sphere (E := E) (n := n)).contMDiffAt.of_le le_top).comp _
        hf.contMDiffAt)
  rw [contMDiffAt_iff_contDiffAt]
  refine ContDiffAt.fderiv (n := โˆž) ?_ contDiffAt_const (right_eq_inf.mp rfl)
  conv =>
    arg 3
    change
      (OrthonormalBasis.fromOrthogonalSpanSingleton n (ne_zero_of_mem_unit_sphere (-p))).repr โˆ˜
        (stereoToFun (-(โ†‘p : E)) โˆ˜ uncurry stereoInvFunAux) โˆ˜ Prod.map Neg.neg id
  refine
    (OrthonormalBasis.fromOrthogonalSpanSingleton (๐•œ := โ„) (E := E) n
        (ne_zero_of_mem_unit_sphere (-p))
      ).repr.toContinuousLinearEquiv.toContinuousLinearMap.contDiff.contDiffAt.comp _ ?_
  refine ContDiffAt.comp _ ?_ (ContDiffAt.prod_map contDiff_neg.contDiffAt contDiffAt_id)
  refine ContDiffAt.comp _ ?_ contDiff_uncurry_stereoInvFunAux.contDiffAt
  simp only [coe_neg_sphere, comp_apply, Prod.map_apply, id_eq, uncurry_apply_pair,
    stereoInvFunAux_apply, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow,
    zero_add, smul_zero, zero_sub, smul_neg, neg_smul, neg_neg, inv_smul_smulโ‚€]
  refine
    (contDiffOn_stereoToFun (E := E) (v := -(โ†‘p : E))).contDiffAt (IsOpen.mem_nhds ?_ ?_)
  ยท exact
      (innerSL โ„ (-(โ†‘p : E))).continuous.isOpen_preimage {1}แถœ isOpen_compl_singleton
  ยท simp only [map_neg, ContinuousLinearMap.neg_apply, innerSL_apply, ne_eq,
      Set.mem_setOf_eq]
    have hp := inner_eq_norm_mul_iff_real (x := (โ†‘p : E)) (y := -(โ†‘(f x) : E))
    simp only [inner_neg_right, norm_eq_of_mem_sphere, norm_neg, mul_one, one_smul,
      smul_neg, chartAt, ChartedSpace.chartAt, stereographic'_source, Set.mem_compl_iff,
      Set.mem_singleton_iff] at hp hx
    rw [hp, โ† coe_neg_sphere, Subtype.val_inj, โ† neg_eq_iff_eq_neg, โ† ne_eq]
    symm; exact hx

(Split due to length limit)

Miyahara Kล (Dec 18 2024 at 09:32):

theorem contMDiff_sphereTangentMap {n : โ„•} [Fact (finrank โ„ E = n + 1)] {m : โ„•โˆž}
    {f : M โ†’ โ†ฅ(sphere (0 : E) 1)} {g : M โ†’ E}
    (hf : ContMDiff I (๐“ก n) m f) (hf' : โˆ€ x, โŸช(โ†‘(f x) : E), g xโŸซ_โ„ = 0)
    (hg : ContMDiff I ๐“˜(โ„, E) m g) : ContMDiff I (๐“ก n).tangent m (sphereTangentMap n f g hf') := by
  rw [contMDiff_iff_target]
  constructor
  ยท rw [continuous_generateFrom_iff]
    simp only [FiberBundleCore.localTrivAsPartialEquiv_source, FiberBundleCore.proj,
      FiberBundleCore.localTrivAsPartialEquiv_coe, Set.iUnion_coe_set, Set.mem_iUnion,
      Set.mem_singleton_iff, exists_prop, forall_exists_index, and_imp]
    rintro _ _ โŸจp, rflโŸฉ s hs rfl; rcases neg_surjective p with โŸจp, rflโŸฉ
    rw [Set.preimage_inter]
    conv =>
      enter [1, 1]
      change
        sphereTangentMap n f g hf' โปยน'
          (Bundle.TotalSpace.proj โปยน' (chartAt (EuclideanSpace โ„ (Fin n)) p).source)
    simp only [stereographic'_source, Set.preimage_compl, Set.preimage_preimage,
      sphereTangentMap_proj, FiberBundleCore.localTriv_apply,
      VectorBundleCore.toFiberBundleCore_indexAt, tangentBundleCore_indexAt,
      VectorBundleCore.coe_coordChange, tangentBundleCore_coordChange, PartialHomeomorph.extend,
      modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, PartialHomeomorph.toFun_eq_coe,
      coe_achart, PartialHomeomorph.coe_coe_symm, modelWithCornersSelf_coe, Set.range_id,
      fderivWithin_univ]
    refine
      ContinuousOn.isOpen_inter_preimage (ContinuousOn.prod (contMDiff_iff.mp hf).1.continuousOn ?_)
        ((contMDiff_iff.mp hf).1.isOpen_preimage _
          (chartAt (EuclideanSpace โ„ (Fin n)) p).open_source) hs
    simp only [chartAt, ChartedSpace.chartAt, stereographic'_neg]
    exact (contMDiffOn_iff.mp (contMDiff_sphereTangentMap_aux hf hf' hg p)).1
  ยท rintro โŸจp, vโŸฉ
    conv =>
      arg 4
      simp only [extChartAt, PartialHomeomorph.extend, TangentBundle.chartAt,
        FiberBundleCore.proj, โ† TangentBundle.trivializationAt_eq_localTriv,
        PartialHomeomorph.trans_toPartialEquiv, PartialHomeomorph.prod_toPartialEquiv,
        PartialHomeomorph.refl_partialEquiv, modelWithCorners_prod_toPartialEquiv,
        modelWithCornersSelf_partialEquiv, PartialEquiv.refl_prod_refl, PartialEquiv.coe_trans,
        PartialEquiv.refl_coe, PartialEquiv.prod_coe, PartialHomeomorph.toFun_eq_coe, id_eq,
        Trivialization.coe_coe, comp_def, TangentBundle.trivializationAt_apply,
        PartialEquiv.trans_refl, PartialHomeomorph.coe_coe_symm, modelWithCornersSelf_coe,
        Set.range_id, fderivWithin_univ, CompTriple.comp_eq, sphereTangentMap_proj,
        chartAt, ChartedSpace.chartAt, stereographic'_neg]
    conv =>
      arg 5
      tactic =>
        ext x
        simp only [extChartAt, PartialHomeomorph.extend, modelWithCorners_prod_toPartialEquiv,
          modelWithCornersSelf_partialEquiv, PartialEquiv.refl_prod_refl, PartialEquiv.trans_source,
          PartialHomeomorph.toFun_eq_coe, PartialEquiv.refl_source, Set.preimage_univ,
          Set.inter_univ, Set.mem_preimage, TangentBundle.mem_chart_source_iff,
          sphereTangentMap_proj]
        rw [โ† Set.mem_preimage]
    apply ContMDiffOn.prod_mk_space
    ยท rw [contMDiff_iff_target] at hf
      simpa using hf.2 p
    ยท exact contMDiff_sphereTangentMap_aux hf hf' hg p

Miyahara Kล (Jan 10 2025 at 07:20):

@Sรฉbastien Gouรซzel Are you interested in the PR?

Eric Wieser (Jan 10 2025 at 10:37):

Miyahara Kล said:

I don't have the energy to maintain a pull request of this, but I hope it helps!

I think it's still worth opening a draft pull request and marking it please-adopt, to increase the chance that someone picks it up

Miyahara Kล (Jan 11 2025 at 08:17):

#20656

Miyahara Kล (Jan 11 2025 at 08:19):

And I updated this to current Mathlib in this PR.

Miyahara Kล (Jan 11 2025 at 08:31):

The only one thing to do is proof cleanup so I created as an open PR, not draft.

Last updated: May 02 2025 at 03:31 UTC