monoid_hom coercion

Stream: new members

[María Inés de Frutos Fernández]

After #13273, if I apply uniform_group.uniform_continuous_iff_open_ker to a monoid_hom f : α →* β, a coercion from α →* β to α →* β appears in the goal. I can get rid of it using change (as in the mwe below), but what would be a better way to do that?

import topology.algebra.uniform_group

open_locale topological_space

variables {α β : Type*} [uniform_space α] [group α] [uniform_group α] [uniform_space β]
  [discrete_topology β] [group β] [uniform_group β] {f : α →* β} (h : filter.tendsto f (𝓝 1) (𝓝 1))

set_option pp.coercions true
example : continuous f :=
begin
  apply uniform_continuous.continuous,
  rw uniform_group.uniform_continuous_iff_open_ker,
  change is_open ↑(f.ker),
  sorry
end

[María Inés de Frutos Fernández]

@Anatole Dedecker

[Kevin Buzzard]

I thought at first that there was a typo in this question but it really does seem to be a coercion from α →* β to itself!

[Anatole Dedecker]

Oh yeah, I didn’t think about it but I totally see why it is happening

[Anatole Dedecker]

Tbh I don’t see any other solution that duplicating the lemma to keep the monoid_hom version :/

[Yaël Dillies]

The correct fix here is to make docs#monoid_hom.ker take in (f : F), where monoid_hom_class F α β, rather than f : α →* β.

[Yaël Dillies]

Then you don't need the coercion to apply it in uniform_group.uniform_continuous_iff_open_ker.

[Anatole Dedecker]

But that would break dot notation right ?

[Yaël Dillies]

Yeah

[Anatole Dedecker]

And there’s another problem : a linear map is an add_monoid_hom, but the kers have different types

[Yaël Dillies]

@Kyle Miller is working on preserving the dot notation in such cases but as far as I know this is still WIP.

[Yaël Dillies]

Is that a Lean problem, though?

[Yaël Dillies]

I'm not saying you should rename monoid_hom.ker to ker :rofl:

[Anatole Dedecker]

Yes but if we make dot notation work we won’t have an explicit distinction

[Yaël Dillies]

That's why I think we shouldn't care much about dot notation here.

[Yaël Dillies]

You can always open monoid_hom whenever you use monoid_hom.ker. As it happens, f.ker and ker f have the same number of characters.

[Anatole Dedecker]

Yes but the second one needs more parentheses x)

[Anatole Dedecker]

(Yeah, that’s not a big problem)

[Eric Wieser]

What's the coercion say the instance name is if you hover over it?

[Eric Wieser]

Just to check; does Yaël's suggestion actually break dot notation on monoid_homs if it remains in the monoid_hom namespace?

[Yaël Dillies]

I haven't checked in the infoview, but I know it is docs#monoid_hom.has_coe_t

[Eric Wieser]

I ran into this the other day; that instance is nasty because it has no (d)simp lemmas

[Yaël Dillies]

It does have a few, but we're missing lots.

[Yaël Dillies]

It currently causes a problem because Lean 3 doesn't have eta expansion for structures, so this series of instances is not defeq everywhere. If we were using old structures as @Anne Baanen suggests, this would be fine without waiting for Lean 4.

[María Inés de Frutos Fernández]

Eric Wieser said:

What's the coercion say the instance name is if you hover over it?

The infoview shows coe α →* β α →* β coe_to_lift f

[Eric Wieser]

@Yaël Dillies, where's the lemma that says ⇑↑f = ⇑f for that come?

[Yaël Dillies]

Likely missing.

[Eric Wieser]

@María Inés de Frutos Fernández, you can hover over coe_to_lift to dig deeper

[Eric Wieser]

Likely missing.

That's the most important lemma to have!

[María Inés de Frutos Fernández]

Eric Wieser said:

María Inés de Frutos Fernández, you can hover over coe_to_lift to dig deeper

True. That shows the monoid_hom.has_coe_t (has_coe_t (α →* β) (α →* β)).

[Eric Wieser]

As predicted by @Yaël Dillies then, thanks for confirming

[Anne Baanen]

One option that I have suggested before (might be in a different context): should we instead define subgroup.ker and submodule.ker as the closure of f⁻¹ {1} (or f⁻¹ {0} as applicable), where f is an arbitary function? Then we don't need to care about the precise kind of map f happens to be, and we can distinguish kernel-as-subgroup from kernel-as-submodule.