lifting continuous maps in `SeparationQuotient`

Stream: Is there code for X?

[Aaron Liu]

Does this exists in mathlib already? If it does not, which file should this go in?

import Mathlib.Topology.ContinuousMap.Basic

namespace SeparationQuotient
variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T0Space Y]

/--
Any continuous map whose codomain is a T₀ space can be lifted to the separation quotient.
-/
def liftContinuousMap : C(X, Y) ≃ C(SeparationQuotient X, Y) where
  toFun f := {toFun := SeparationQuotient.lift f fun x y hxy => (hxy.map f.continuous).eq}
  invFun f := f.comp {toFun := SeparationQuotient.mk}
  left_inv f := ContinuousMap.ext fun _ => rfl
  right_inv f := ContinuousMap.ext (Quotient.ind fun _ => rfl)

@[simp]
theorem liftContinuousMap_apply_mk (f : C(X, Y)) (x : X) :
    liftContinuousMap f (SeparationQuotient.mk x) = f x := rfl

@[simp]
theorem liftContinuousMap_symm_apply (f : C(SeparationQuotient X, Y)) (x : X) :
    liftContinuousMap.symm f x = f (SeparationQuotient.mk x) := rfl

end SeparationQuotient

[Eric Wieser]

I think there's an open PR somewhat related to this

[Yury G. Kudryashov]

Should we replace the current docs#SeparationQuotient.lift with this?