Zulip Chat Archive

Stream: maths

Topic: extensions


view this post on Zulip Patrick Massot (Jul 16 2018 at 19:49):

@Johannes Hölzl At https://github.com/leanprover/mathlib/blob/master/analysis/topology/continuity.lean#L841-L843 do we really need that [inhabited γ]? It forces lots of other inhabited assumptions that seem unnecessary from a mathematical point of view. If γ is not inhabited then there shouldn't be that many f : α → γ to care about

view this post on Zulip Mario Carneiro (Jul 16 2018 at 19:55):

the inhabited is needed for lim

view this post on Zulip Mario Carneiro (Jul 16 2018 at 19:55):

because it takes a default value when the limit is not defined

view this post on Zulip Patrick Massot (Jul 16 2018 at 19:55):

I understand this

view this post on Zulip Patrick Massot (Jul 16 2018 at 19:55):

But one could hope for a definition not using lim then

view this post on Zulip Mario Carneiro (Jul 16 2018 at 19:57):

I recall puzzling over this definition a while ago; I also don't particularly like this style of definition

view this post on Zulip Mario Carneiro (Jul 16 2018 at 19:57):

it seems like we should already know that the limit is defined at this point

view this post on Zulip Mario Carneiro (Jul 16 2018 at 20:00):

I guess we need the assumption of continuous_ext to know the definition makes sense

view this post on Zulip Mario Carneiro (Jul 16 2018 at 20:02):

It forces lots of other inhabited assumptions that seem unnecessary from a mathematical point of view.

Do you have any particular examples?

view this post on Zulip Patrick Massot (Jul 16 2018 at 20:03):

Why? ext de is a function from α → γ to β → γ. Can't Lean be happy if both are uninhabited types and we don't write anything about the definition?

view this post on Zulip Patrick Massot (Jul 16 2018 at 20:04):

Examples are in my work in progress in the perfectoid project. I'm working on Hausdorff completions of uniform spaces.

view this post on Zulip Mario Carneiro (Jul 16 2018 at 20:04):

i mean maybe there is a way to pick an inhabitant in your setting

view this post on Zulip Patrick Massot (Jul 16 2018 at 20:04):

The completion functor, which is left-adjoint to the inclusion of Hausdorff and complete uniform spaces into all uniform spaces, is constructed on homs by extension

view this post on Zulip Patrick Massot (Jul 16 2018 at 20:05):

If I assume the starting uniform space is inhabited then its completion is also inhabited, no problem. But it mean I keep assuming spaces are inhabited

view this post on Zulip Mario Carneiro (Jul 16 2018 at 20:06):

No, I mean somehow argue the empty case so it's not needed

view this post on Zulip Patrick Massot (Jul 16 2018 at 20:07):

If this is possible there, why isn't possible right in the definition of dense_embedding.ext

view this post on Zulip Patrick Massot (Jul 16 2018 at 20:07):

(by the way, this name is confusion since it has nothing to do with extensionality)

view this post on Zulip Mario Carneiro (Jul 16 2018 at 20:08):

Agreed. Do you have a suggestion?

view this post on Zulip Patrick Massot (Jul 16 2018 at 20:08):

about the name?

view this post on Zulip Mario Carneiro (Jul 16 2018 at 20:08):

yes

view this post on Zulip Patrick Massot (Jul 16 2018 at 20:09):

dense_embedding.extension maybe?

view this post on Zulip Mario Carneiro (Jul 16 2018 at 20:19):

I managed this definition:

def extend (de : dense_embedding e) (f : α → γ) (b : β) : γ :=
have nonempty γ, from
let ⟨_, ⟨_, a, _⟩⟩ := exists_mem_of_ne_empty
  (mem_closure_iff.1 (de.dense b) _ is_open_univ trivial) in ⟨f a⟩,
@lim _ (classical.inhabited_of_nonempty this) _ (map f (vmap e (nhds b)))

view this post on Zulip Patrick Massot (Jul 16 2018 at 20:20):

Scary! But I don't mind being scared by the definition: can you prove the expected properties?

view this post on Zulip Mario Carneiro (Jul 16 2018 at 20:20):

It's mostly just a proof getting stuck into the inhabited γ slot - it doesn't change any of the proofs

view this post on Zulip Mario Carneiro (Jul 16 2018 at 20:21):

all the proofs immediately after the definition still work, I may have to hunt down other uses

view this post on Zulip Patrick Massot (Jul 16 2018 at 20:26):

and also hunt down the inhabited assumptions


Last updated: May 14 2021 at 19:21 UTC