Riemannian Metric Diamond?

Stream: new members

[Dominic Steinitz]

I am trying to prove the existence of a Riemannian metric and I have been struggling to show Lean that a linear continuous function is a linear continuous function. I thought innerSL would be my salvation.

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

open Bundle ContDiff Manifold

variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]

noncomputable
def g_bilin (i p : B) :
  (TangentSpace IB) p →L[ℝ]  ((TangentSpace IB) p →L[ℝ] Trivial B ℝ p) := by
  let dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  let inner := innerSL ℝ (E := EB)
  exact inner.comp dψ |>.flip.comp dψ

But Lean tells me that

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  @NormedSpace.toModule ℝ EB Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup inst✝⁴
inferred
  @NormedSpace.toModule ℝ EB Real.instRCLike.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup
    inst✝³.toNormedSpace

and further that

  dψ
has type
  @ContinuousLinearMap ℝ ℝ Field.toSemifield.toDivisionSemiring.toSemiring
    Field.toSemifield.toDivisionSemiring.toSemiring (RingHom.id ℝ) (TangentSpace IB p)
    (instTopologicalSpaceTangentSpace IB p) NormedAddCommGroup.toENormedAddCommMonoid.toAddCommMonoid
    (TangentSpace 𝓘(ℝ, EB) (↑(extChartAt IB i) p)) (instTopologicalSpaceTangentSpace 𝓘(ℝ, EB) (↑(extChartAt IB i) p))
    NormedAddCommGroup.toENormedAddCommMonoid.toAddCommMonoid (instModuleTangentSpace IB p)
    (instModuleTangentSpace 𝓘(ℝ, EB) (↑(extChartAt IB i) p))
but is expected to have type
  @ContinuousLinearMap ?m.96 ℝ ?m.99 Field.toSemifield.toSemiring ?m.102 ?m.105 ?m.106 ?m.107 EB
    PseudoMetricSpace.toUniformSpace.toTopologicalSpace NormedAddCommGroup.toSeminormedAddCommGroup.toAddCommMonoid
    ?m.114 inst✝³.toModule
in the application
  inner.comp dψ

[Michael Rothgang]

Quick answer: I'm pretty sure you're having one typeclass too much. Try deleting the [NormedSpace ℝ EB].

[Dominic Steinitz]

Marvellous - this checks

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

open Bundle ContDiff Manifold

variable
  {EB : Type*} [NormedAddCommGroup EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]

noncomputable instance (p : B) : NormedAddCommGroup (TangentSpace IB p) := by
  change NormedAddCommGroup EB
  infer_instance

noncomputable instance (p : B) : NormedSpace ℝ (TangentSpace IB p) := by
  change NormedSpace ℝ EB
  infer_instance

noncomputable
def g_bilin (i p : B) :
  (TangentSpace IB) p →L[ℝ]  ((TangentSpace IB) p →L[ℝ] Trivial B ℝ p) := by
  let dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  let inner := innerSL ℝ (E := EB)
  exact inner.comp dψ |>.flip.comp dψ

[Michael Rothgang]

Long version/explanation: writing variable {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB] [InnerProductSpace ℝ EB] tells Lean "let EB be a real normed space" and "let EB be a real inner product space", but these algebraic operations need not be related: you will have two scalar multiplications (and it's easy to get yourself or Lean confused as to which one you're using at the moment). Since you want to use only one operation, and an inner product space always has a norm (induced by the inner product), you want to delete the first typeclass.

[Sébastien Gouëzel]

Dominic Steinitz said:

Marvellous - this checks

noncomputable instance (p : B) : NormedAddCommGroup (TangentSpace IB p) := by
  change NormedAddCommGroup EB
  infer_instance

Sorry, but please don't do that, it will only bring you pain. What you're doing here is saying: At a point p, I have some chart through which I can identity the tangent space at p with the model space. Let's copy the norm from the model space to the tangent space through this identification.

This gives you a norm on the tangent space, but it's completely noncanonical, and in particular it will depend on p in a very wild way.

[Sébastien Gouëzel]

(If you only want to use this to define g_bilin, it's kind of fine because in the end the normed structure is not really used, but your instances should definitely only be local instances)

[Dominic Steinitz]

All I want to do is convince Lean that a continuous linear function is a continuous linear function. If there is a better way to do this then I am eager to learn.

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

open Bundle ContDiff Manifold

variable
  {EB : Type*} [NormedAddCommGroup EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]

noncomputable instance (p : B) : NormedAddCommGroup (TangentSpace IB p) := by
  change NormedAddCommGroup EB
  infer_instance

noncomputable instance (p : B) : NormedSpace ℝ (TangentSpace IB p) := by
  change NormedSpace ℝ EB
  infer_instance

noncomputable
def g_bilin (i p : B) :
  (TangentSpace IB) p →L[ℝ]  ((TangentSpace IB) p →L[ℝ] Trivial B ℝ p) := by
  let dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  let inner := innerSL ℝ (E := EB)
  exact inner.comp dψ |>.flip.comp dψ

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

g i p is linear continuous but I have not been able to convince Lean that it is. I thought to do it by construction.