Subtype Synthesis Problem

Stream: new members

[Jeff Lee]

Hi all, I'm having some trouble with instance synthesis of a subtype. In the Lean code I've pasted, I'm trying to call Continuous.strictMono_of_inj on a transition map that I've proved is continuous and injective. However, Lean is having trouble recognizing that the domain of this map possesses the properties required to call this lemma e.g. OrderTopology α. I've even tried having a direct proof of OrderTopology { x : ℝ // x ∈ Iio a } within the proof but Lean fails to recognize this in its synthesis attempt. Does anyone have any tips to fix this kind of problem? Thanks!

import Mathlib

open Set Function

variable {X : Type*} [TopologicalSpace X]

def TφSymm [ConnectedSpace X] (a : ℝ) {φ ψ : PartialHomeomorph X ℝ}
    (hφ : φ.target = univ) (hA : φ '' (φ.source ∩ ψ.source) = Iio a) : {x // x ∈ Iio a} → {y // y ∈ φ.source ∧ y ∈ ψ.source} :=
  fun x => ⟨((Iio a).restrict φ.symm) x, by
  constructor
  · simp_all only [restrict_apply, mem_univ, PartialHomeomorph.map_target]
  · have h1 : x.val ∈ φ '' (φ.source ∩ ψ.source) := by
      rw [hA]
      exact Subtype.coe_prop x
    -- So there exists some y ∈ φ.source ∩ ψ.source such that φ y = x.val
    obtain ⟨y, hy_mem, hy_eq⟩ := h1
    -- We have φ.symm (x.val) = φ.symm (φ y) = y (since y ∈ φ.source)
    have h2 : φ.symm x.val = y := by
      rw [← hy_eq]
      refine PartialHomeomorph.left_inv φ ?_
      exact mem_of_mem_inter_left hy_mem
    -- Therefore φ.symm x.val ∈ ψ.source since y ∈ ψ.source
    subst h2
    exact hy_mem.2
  ⟩

def Tψ [ConnectedSpace X] (b : ℝ) {φ ψ : PartialHomeomorph X ℝ}
    (hB : ψ '' (φ.source ∩ ψ.source) = Ioi b) :
    {y // y ∈ φ.source ∧ y ∈ ψ.source} → {x // x ∈ Ioi b} :=
  fun y => ⟨((φ.source ∩ ψ.source).restrict ψ) y, by
  have hy_mem : y.val ∈ φ.source ∩ ψ.source := ⟨y.property.1, y.property.2⟩
  rw [← hB]
  exact mem_image_of_mem (↑ψ) hy_mem
  ⟩

def TransitionMap [ConnectedSpace X] (a b : ℝ) {φ ψ : PartialHomeomorph X ℝ} (hφ : φ.target = univ) (hA : φ '' (φ.source ∩ ψ.source) = Iio a) (hB : ψ '' (φ.source ∩ ψ.source) = Ioi b) :
    {x // x ∈ Iio a} → {y // y ∈ Ioi b} := (Tψ b hB) ∘ (TφSymm a hφ hA)

/- Continuity of transition map for the (-∞, a) → (b, ∞) case. -/
lemma continuous_transition₁ [ConnectedSpace X] (a b : ℝ) {φ ψ : PartialHomeomorph X ℝ} (hφ : φ.target = univ) (hA : φ '' (φ.source ∩ ψ.source) = Iio a) (hB : ψ '' (φ.source ∩ ψ.source) = Ioi b) :
    Continuous (TransitionMap a b hφ hA hB : {x : ℝ // x ∈ Iio a} → {y : ℝ // y ∈ Ioi b}) := by
  -- result alread proven; sorry as a placeholder to save space in MWE
  sorry

/- Injectivity of transition map for the (-∞, a) → (b, ∞) case. -/
lemma injective_transition₁ [ConnectedSpace X] (a b : ℝ) {φ ψ : PartialHomeomorph X ℝ} (hφ : φ.target = univ) (hA : φ '' (φ.source ∩ ψ.source) = Iio a) (hB : ψ '' (φ.source ∩ ψ.source) = Ioi b) :
    Injective (TransitionMap a b hφ hA hB : {x : ℝ // x ∈ Iio a} → {y : ℝ // y ∈ Ioi b}) := by
  -- result alread proven; sorry as a placeholder to save space in MWE
  sorry

/- Monotonicity of transition map for the (-∞, a) → (b, ∞) case. -/
lemma monotone_transition₁ [ConnectedSpace X] (a b : ℝ) {φ ψ : PartialHomeomorph X ℝ}
  (hφ : φ.target = univ) (hA : φ '' (φ.source ∩ ψ.source) = Iio a)
  (hB : ψ '' (φ.source ∩ ψ.source) = Ioi b) :
  StrictMono (TransitionMap a b hφ hA hB : {x : ℝ // x ∈ Iio a} → {y : ℝ // y ∈ Ioi b})  := by
  have h1 : Continuous (TransitionMap a b hφ hA hB : {x : ℝ // x ∈ Iio a} → {y : ℝ // y ∈ Ioi b}) :=
    continuous_transition₁ a b hφ hA hB
  have h2 : Injective (TransitionMap a b hφ hA hB : {x : ℝ // x ∈ Iio a} → {y : ℝ // y ∈ Ioi b}) :=
    injective_transition₁ a b hφ hA hB

  haveI : Inhabited (Iio a) := ⟨⟨a - 1, by norm_num⟩⟩
  have : (Iio a).OrdConnected := by exact ordConnected_Iio
  haveI : ConditionallyCompleteLinearOrder (Iio a) :=
    ordConnectedSubsetConditionallyCompleteLinearOrder (Iio a)

  haveI : OrderTopology { x : ℝ // x ∈ Iio a } := by
    exact orderTopology_of_ordConnected

  exact Continuous.strictMono_of_inj h1 h2

[Kevin Buzzard]

Note that your goal is of the form strictMono f but (to my surprise) the conclusion of Continuous.strictMono_of_inj h1 h2 is of the form strictMono f \or strictAnti f so exact isn't going to work here, but this is not your problem. Your problem seems to be that you have two incompatible orders on Preorder { x // x ∈ Iio a }:

...
  haveI : OrderTopology { x : ℝ // x ∈ Iio a } := by
    exact orderTopology_of_ordConnected
  have foo : StrictMono (TransitionMap a b hφ hA hB) ∨ StrictAnti (TransitionMap a b hφ hA hB) := by
    convert Continuous.strictMono_of_inj h1 h2
    /-
    ...
    this✝ : ConditionallyCompleteLinearOrder ↑(Iio a)
    ...
    ⊢ (Subtype.preorder fun x ↦ x ∈ Iio a) = this✝.toSemilatticeInf.toPreorder
    -/
    repeat sorry
  sorry

From this I can diagnose that the problem is your line

  haveI : ConditionallyCompleteLinearOrder (Iio a) :=
    ordConnectedSubsetConditionallyCompleteLinearOrder (Iio a)

which uses have to create data, which is instantly forgotten (so one of your instances has no definition, which is causing the problem). Changing this line to

  letI : ConditionallyCompleteLinearOrder (Iio a) :=
    ordConnectedSubsetConditionallyCompleteLinearOrder (Iio a)

solves your problem.

[Jeff Lee]

Thank you for the help! It seems I jumped the gun on making haveI statements for every property that I wanted Iio a to have. Even commenting out everything after haveI : Inhabited (Iio a) := ⟨⟨a - 1, by norm_num⟩⟩ solves the problem as well since Lean is smart enough to synthesize the missing info.