extensions

Stream: maths

[Patrick Massot]

@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

[Mario Carneiro]

the inhabited is needed for lim

[Mario Carneiro]

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

[Patrick Massot]

I understand this

[Patrick Massot]

But one could hope for a definition not using lim then

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

Do you have any particular examples?

[Patrick Massot]

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?

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

Agreed. Do you have a suggestion?

[Patrick Massot]

about the name?

[Mario Carneiro]

yes

[Patrick Massot]

dense_embedding.extension maybe?

[Mario Carneiro]

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)))

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

and also hunt down the inhabited assumptions