Zulip Chat Archive

Stream: general

Topic: extension and coercion


Patrick Massot (Mar 13 2018 at 16:18):

A long time ago, I wrote:

structure homeo (α β) [topological_space α] [topological_space β] extends equiv α β :=
(fun_con : continuous to_fun)
(inv_con : continuous inv_fun)

instance : has_coe_to_fun (homeo α β) := ⟨_, λ f, f.to_fun

But now it seems I have trouble, probably because a homeo f and f.to_equiv don't have defeq coercion to function. I'm especially interested in direct images of subsets under homeomorphisms. For instance, I'd like to prove (f : homeo X X) (s : set X) : f '' closure s = closure (f '' s), using image_closure_subset_closure_image from mathlib

Patrick Massot (Mar 13 2018 at 16:19):

How should I setup this?

Johannes Hölzl (Mar 13 2018 at 16:33):

this works for me

example (h : homeo α β) : (h : α  β) = h.to_equiv := rfl

Patrick Massot (Mar 13 2018 at 16:48):

hum. Maybe the problem is something else. Do you manage to prove my closure lemma using this coercion? In principle this a trivial lemma once you have image_closure_subset_closure_image (to be applied to both f and its inverse)

Johannes Hölzl (Mar 13 2018 at 16:57):

My solution looks like this now:

import analysis.topology.continuity data.equiv
open set
variables {α : Type*} {β : Type*} [topological_space α] [topological_space β]
structure homeo (α β) [topological_space α] [topological_space β] extends equiv α β :=
(fun_con : continuous to_fun)
(inv_con : continuous inv_fun)
instance : has_coe_to_fun (homeo α β) := ⟨_, λ f, f.to_fun
lemma homeo_coe_to_equiv_coe (h : homeo α β) : (h : α  β) = h.to_equiv := rfl
lemma equiv.image_eq_preimage {α β} (e : α  β) (s : set α) : e '' s = e.symm ⁻¹' s := ext $ assume x, mem_image_iff_of_inverse e.left_inv e.right_inv

example (f : homeo α α) (s : set α) : f '' closure s = closure (f '' s) :=
subset.antisymm
  (image_closure_subset_closure_image f.fun_con)
  begin
    rw [homeo_coe_to_equiv_coe, f.to_equiv.image_eq_preimage (closure s),  image_subset_iff],
    refine subset.trans (image_closure_subset_closure_image f.inv_con) _,
    simp [(image_comp _ _ _).symm, f.to_equiv.inverse_apply_apply],
    show closure (id '' s)  closure s, by rw [image_id]; exact subset.refl _
  end

One problem is that rw and the simplifier can now see through the coercion. So when you want to apply equiv lemmas you need to apply homeo_coe_to_equiv_coe first. Another solution is to make a calc proof, which might be a little bit nicer and one has the opportunity to state the goal in the required form.

Patrick Massot (Mar 13 2018 at 17:04):

Thanks you very much. I feared needing to invoke something like homeo_coe_to_equiv_coe but it doesn't seem so bad in the end, especially if a calc proof works (I'll try).

Patrick Massot (Mar 13 2018 at 17:05):

I see this is also a good opportunity for my poor man tactic (as Kevin would put it):

meta def by_double_inclusion : tactic unit := do
`[apply set.subset.antisymm_iff.2, split]

Obviously it's a bit ridiculous but the main point is readablity

Johannes Hölzl (Mar 13 2018 at 17:16):

If you add some infrastructure for homeo it gets also nicer:

import analysis.topology.continuity data.equiv
open set

variables {α : Type*} {β : Type*} [topological_space α] [topological_space β]

structure homeo (α β) [topological_space α] [topological_space β] extends equiv α β :=
(fun_con : continuous to_fun)
(inv_con : continuous inv_fun)

instance : has_coe_to_fun (homeo α β) := ⟨_, λ f, f.to_fun

def homeo.id (α) [topological_space α] : homeo α α :=
{ fun_con := continuous_id, inv_con := continuous_id, .. equiv.refl α }

lemma home.id_apply : (homeo.id α : α  α) = id := rfl

def homeo.symm (h : homeo α β) : homeo β α :=
{ fun_con := h.inv_con, inv_con := h.fun_con, .. h.to_equiv.symm }

lemma homeo.symm_comp (h : homeo α β) : (h.symm)  h = homeo.id α :=
funext h.left_inv

lemma homeo_coe_to_equiv_coe (h : homeo α β) : (h : α  β) = h.to_equiv := rfl

lemma equiv.image_eq_preimage {α β} (e : α  β) (s : set α) : e '' s = e.symm ⁻¹' s :=
ext $ assume x, mem_image_iff_of_inverse e.left_inv e.right_inv

lemma equiv.subset_image {α β} (e : α  β) (s : set α) (t : set β) : t  e '' s  e.symm '' t  s :=
by rw [image_subset_iff, e.image_eq_preimage]

example (f : homeo α β) (s : set α) : f '' closure s = closure (f '' s) :=
subset.antisymm
  (image_closure_subset_closure_image f.fun_con)
  ((f.to_equiv.subset_image _ _).2 $
    calc f.symm '' closure (f '' s)  closure (f.symm '' (f '' s)) :
        image_closure_subset_closure_image f.inv_con
      ... = closure s :
        by rw [ image_comp, f.symm_comp, home.id_apply, image_id])

I don't see the value in by_double_inclusion. You could just use apply subset.antisymm. I would prefer if people wrote term style proofs.

Patrick Massot (Mar 14 2018 at 09:31):

Thank you very much @Johannes Hölzl I'm sorry my Lean time is very fragmented those days, so I suddenly stopped answering. I already had some infrastructure but it is only partially compatible with what you wrote. I'll need time to make the whole story consistent, including probably some more lemmas assuming only injectivity or surjectivity.


Last updated: Dec 20 2023 at 11:08 UTC