Mul of pos is pos

Stream: new members

[Rida Hamadani]

I'm proving that composition of orientation preserving maps is orientation preserving, and the part I'm having trouble with is, believe it or not, proving that the product of two positives is a positive.

import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners

variable (𝕜 : Type*) [NormedAddCommGroup 𝕜] [NontriviallyNormedField 𝕜] [LT 𝕜] {H : Type*}
  [NormedAddCommGroup H] [NormedSpace 𝕜 H] [Preorder 𝕜] [PosMulStrictMono 𝕜]

def OrientationPreserving (f : H → H) (s : Set H) : Prop :=
  ∀ x ∈ s, 0 < (fderiv 𝕜 f x).det

lemma orientationPreserving_comp (f g : H → H) (u v : Set H) (hf : OrientationPreserving 𝕜 f u)
    (hg : OrientationPreserving 𝕜 g v) : OrientationPreserving 𝕜 (g ∘ f) (u ∩ f ⁻¹' v) := by
  dsimp [OrientationPreserving] at *
  intro x ⟨hxu, hxv⟩
  rw [fderiv.comp _ _ _]
  · have h₁ : 0 < (fderiv 𝕜 f x).det := hf x hxu
    have h₂ : 0 < (fderiv 𝕜 g (f x)).det := hg (f x) hxv
    unfold ContinuousLinearMap.det ContinuousLinearMap.comp
    rw [(fderiv 𝕜 g (f x)).toLinearMap.det_comp (fderiv 𝕜 f x).toLinearMap]
    exact mul_pos h₂ h₁
  · sorry
  · sorry

Ignore the last 2 sorries, in the exact mul_pos h₂ h₁ line, I'm running into a problem with a metavariable, although I've added instances to 𝕜 so that I can use mul_pos. How can I fix this?

[Daniel Weber]

Using convert instead of exact can often show the problem in these cases. Here, you have a diamond with the LT instance on 𝕜 and the one obtained from the Preorder, which aren't necessarily equal

[Daniel Weber]

Removing the LT instance solves this

[Rida Hamadani]

I see, thank you!

[Daniel Weber]

Note that the NormedAddCommGroup also conflicts with the one derived from NontriviallyNormedField and should be removed

[Rida Hamadani]

It never occurred to me that instances can conflict, it makes sense.

[Rida Hamadani]

I'm still running into similar problems. Using convert in the code below gives me 4 new goals, does this mean that I have 4 conflicting instances?
In general, how can one make sure to not run into this sort of "inheritance problems"? And how do we figure out how to fix them if they arise?

import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners

variable (𝕜 : Type*) [NontriviallyNormedField 𝕜] [Preorder 𝕜] [PosMulStrictMono 𝕜] {H : Type*}
  [NormedAddCommGroup H] [NormedSpace 𝕜 H]

def OrientationPreserving (f : H → H) (s : Set H) : Prop :=
  ∀ x ∈ s,
    DifferentiableAt 𝕜 f x ∧
    0 < (fderiv 𝕜 f x).det

def orientationPreservingPregroupoid : Pregroupoid H where
  property f s := OrientationPreserving 𝕜 f s
  comp {f g u v} hf hg _ _ _ := by
    intro x ⟨hxu, hxv⟩
    rw [fderiv.comp _ (hg (f x) hxv).1 (hf x hxu).1]
    · have h₁ : 0 < (fderiv 𝕜 f x).det := (hf x hxu).2
      have h₂ : 0 < (fderiv 𝕜 g (f x)).det := (hg (f x) hxv).2
      unfold ContinuousLinearMap.det ContinuousLinearMap.comp
      rw [(fderiv 𝕜 g (f x)).toLinearMap.det_comp (fderiv 𝕜 f x).toLinearMap]
      apply And.intro ?_ <| mul_pos h₂ h₁
      apply DifferentiableAt.comp
      · exact (hg (f x) hxv).1
      · exact (hf x hxu).1
  id_mem := by
    intro x hx
    simp only [Set.mem_univ, differentiableAt_id, fderiv_id, true_and]
    unfold ContinuousLinearMap.id ContinuousLinearMap.det
    rw [LinearMap.det_id]
    convert zero_lt_one

[Daniel Weber]

I believe you need to use docs#NormedLinearOrderedField

[Heather Macbeth]

Frankly, you can just use ℝ ... this is a case where I don't think extra generality is useful!