notation for coercion to completion

Stream: mathlib4

[Kevin Buzzard]

These lines (with (α : Type*) [UniformSpace α])

/-- The map from a uniform space to its completion.

porting note: this was added to create a target for the `@[coe]` attribute. -/
@[coe] def coe' : α → Completion α := SeparationQuotient.mk ∘ pureCauchy

/-- Automatic coercion from `α` to its completion. Not always injective. -/
instance : Coe α (Completion α) :=
  ⟨coe' α⟩

in Mathlib.Topology.UniformSpace.Completion cause the coercion of k : K (a number field) to its completion wrt a valuation (a p-adic field) to be written as ↑K k. Is this intended? I stared at ↑K trying to figure out what K was being coerced to for a bit before it dawned on me what was going on. Is everyone else used to this and I only just noticed it?

[Yaël Dillies]

That looks like a bug in the delaborator

[Ruben Van de Velde]

I noticed it during the port (and haven't been touching anything that triggers it since then)

[Ruben Van de Velde]

Maybe someone should file an issue

[Kevin Buzzard]

I'm on a train but will do it later if nobody else does it first.

[Kyle Miller]

It's not a bug in the delaborator, it's a misapplied @[coe] attribute. The assumption with @[coe] is that the first explicit argument is the value being coerced. However, the first explicit argument of coe' is the type of the value being coerced.

[Kyle Miller]

This seems to work:

protected def coe : α → Completion α := SeparationQuotient.mk ∘ pureCauchy

run_cmd Lean.Elab.Command.liftTermElabM do
  Lean.Meta.registerCoercion ``Completion.coe
    (some { numArgs := 3, coercee := 2, type := .coe })

/-- Automatic coercion from `α` to its completion. Not always injective. -/
instance : Coe α (Completion α) :=
  ⟨Completion.coe α⟩

[Patrick Massot]

Having an explicit argument here is weird. One could also argue this should not be a coercion but this is another debate.

[Kyle Miller]

Assuming it's a good idea for it to be a coercion, a benefit to having the type being explicit here is that ((↑) : α → Completion α), which appears frequently in the file, appears as Completion.coe α, which is more readable than just Completion.coe.

[Patrick Massot]

I think that ((↑) : α → Completion α) is more explicit than Completion.coe α.

[Anatole Dedecker]

I agree, although I think I would also like if we had a cleaner canonical notation for "the coercion map between foo and bar".

[Patrick Massot]

I have a hard time imagining how it could be more concise and explicit than the above spelling.

[Anatole Dedecker]

At least by removing some parentheses ?

[Patrick Massot]

Indeed that would be nice.

[Kyle Miller]

@Patrick Massot I meant the way it pretty prints. There's no mechanism for pretty printing as ((↑) : α → Completion α) yet.

[Patrick Massot]

Oh, I see.

[Kyle Miller]

The module consistently uses this notation in the source code at least.

[Mitchell Lee]

The name for this map is very inconsistent. If it's a uniformly continuous function it's called docs#UniformSpace.Completion.coe'. If it's a uniform additive group homomorphism it's called docs#UniformSpace.Completion.toCompl. If it's a uniform ring homomorphism it's called docs#UniformSpace.Completion.coeRingHom.

[Kevin Buzzard]

#20514 makes alpha implicit. Mathlib still compiles fine.