Continuous uniqueElim

Stream: Is there code for X?

[Kevin Buzzard]

This works:

import Mathlib

def Homeomorph.pUnitPiEquiv (f : PUnit → Type*) [∀ x, TopologicalSpace (f x)] :
    (Π t, f t) ≃ₜ f () where
  toFun a := a ()
  invFun a _t := a
  left_inv _ := rfl
  right_inv _ := rfl
  continuous_toFun := by fun_prop
  continuous_invFun := by fun_prop

But this fails:

import Mathlib

def piUnique {α : Type*} [Unique α] (f : α → Type*) [∀ x, TopologicalSpace (f x)] :
    (Π t, f t) ≃ₜ f default where
  toFun a := a default
  invFun := uniqueElim
  left_inv f := by ext i; cases Unique.eq_default i; rfl
  right_inv _ := rfl
  continuous_toFun := by fun_prop
  continuous_invFun := by fun_prop -- fails

(continuity of uniqueElim is the issue). docs#uniqueElim is data defined with a rwso this scares me even more :-/ This also fails:

import Mathlib

def piUnique {α : Type*} [Unique α] (f : α → Type*) [∀ x, TopologicalSpace (f x)] :
    (Π t, f t) ≃ₜ f default where
  __ := Equiv.piUnique _
  continuous_toFun := by fun_prop
  continuous_invFun := by fun_prop -- fails

Do we have tools to prove Continuous uniqueElim or should I just bash it out?

[Kevin Buzzard]

Reduced it to this:

import Mathlib

lemma surely_we_have_this {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ β)
    (h : IsOpenMap e) : Continuous e.symm := by sorry

def piUnique {α : Type*} [Unique α] (f : α → Type*) [∀ x, TopologicalSpace (f x)] :
    (Π t, f t) ≃ₜ f default where
  __ := Equiv.piUnique _
  continuous_toFun := by fun_prop
  continuous_invFun := surely_we_have_this (Equiv.piUnique f) <| isOpenMap_eval default

[Kevin Buzzard]

Am I making a meal of this?

import Mathlib

lemma Equiv.continuous_symm_of_isOpenMap {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
    (e : α ≃ β) (h : IsOpenMap e) : Continuous e.symm := by
  rw [continuous_def]
  intro U hU
  specialize h U hU
  rwa [← Set.image_equiv_eq_preimage_symm]

def piUnique {α : Type*} [Unique α] (f : α → Type*) [∀ x, TopologicalSpace (f x)] :
    (Π t, f t) ≃ₜ f default where
  __ := Equiv.piUnique _
  continuous_toFun := by fun_prop
  continuous_invFun := Equiv.continuous_symm_of_isOpenMap (Equiv.piUnique f) <|
    isOpenMap_eval default

[Kevin Buzzard]

Added to #20195