!4#3841 Topology.Algebra.Equicontinuity

Stream: mathlib4

[Felix Weilacher]

Hi all,

!4#3841 is my first attempt at porting a file. I've gotten it to compile but I wanted to ask about a few of the changes I had to make to make sure I'm doing things correctly.

The original file had statements and hypotheses about coe_fn ∘ F. Lean 4 did not understand these. Following https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#consequences-for-porting, I replaced each coe_fn with MulHom.toFun ∘ MulHomClass.toMulHom. This is quite cumbersome to write so often and I'm not sure if I chose the correct way to write this coercion or if this is even the correct thing to do generally.

In Lean 4, when the type G →* (ι → M) is mentioned, ι → M is assumed to have the usual Pi topology, whereas in this context it needs the uniform convergence topology. I had to change it to ι →ᵤ M. Actually here the end result seems fine to me. What I'm more confused about is what changed between Lean 3 and Lean 4 to make this change necessary. I guess I don't understand how Lean 3 knew to use uniform convergence.

[Kevin Buzzard]

Can you link to an explicit lean 3 example of where you're claiming that mathlib3 is using a topology other than the usual Pi topology on a pi type?

[Moritz Doll]

@Jake Levinson and @Felix Weilacher, I've had a look and fixed the errors. Quick rundown of my thought process: first I disabled auto-implicits (set_option autoImplicit false) because we have some experience that they tend to get in the way with explicit coercions, because names changed. Then I changed coeFun which was the class and not the function to the arrow. At that point the error messages got more sensible and the only visible error was the last line, which had a 'inferred vs synthesized instance' error and giving the correct instance explicitly solved the error.

[Moritz Doll]

I am confused why the mathlib3 version has coe_fn and not the coe from fun_like, which is the function that comes from [monoid_hom_class hom G M].

[Felix Weilacher]

Kevin Buzzard said:

Can you link to an explicit lean 3 example of where you're claiming that mathlib3 is using a topology other than the usual Pi topology on a pi type?

the mathlib3 version of this file

[Felix Weilacher]

See the proof of docs#equicontinuous_of_equicontinuous_at_one

[Felix Weilacher]

Moritz Doll said:

Jake Levinson and Felix Weilacher, I've had a look and fixed the errors. Quick rundown of my thought process: first I disabled auto-implicits (set_option autoImplicit false) because we have some experience that they tend to get in the way with explicit coercions, because names changed. Then I changed coeFun which was the class and not the function to the arrow. At that point the error messages got more sensible and the only visible error was the last line, which had a 'inferred vs synthesized instance' error and giving the correct instance explicitly solved the error.

Thanks for the help. The (↑) is much better than what I was doing.

[Jake Levinson]

@Moritz Doll Thanks for the explanations behind your thought process! I went through your changes and I think I understand the steps you did.