!4#3705 (Topology.Category.Profinite.Basic)

Stream: mathlib4

[Scott Morrison]

!4#3705 (Topology.Category.Profinite.Basic) is hopefully not far from done. Some simp lemmas must be missing at the remaining sorries, because the goal is not as nice as the corresponding point in mathlib3.

If any of the "Profinite people" (@Kevin Buzzard, @Adam Topaz?) would like to take over this one I'm done for the day.

[Adam Topaz]

I don’t think I’m totally disconnected, but I can take a look in a couple of hours anyway ;)

[Adam Topaz]

Okay, I got the file to build by adding the following lemma:

-- Porting note: This lemma was not needed in mathlib3
@[simp]
lemma forget_ContinuousMap_mk {X Y : Profinite} (f : X → Y) (hf : Continuous f) :
    (forget Profinite).map (ContinuousMap.mk f hf) = f :=
  rfl

Presumably the changes to start-port.sh should be split off to a separate PR?

[Adam Topaz]

I think a similar lemma would be helpful for TopCat and CompHaus as well.

[Matthew Ballard]

Yeah that is a good idea

[Adam Topaz]

In the long run (i.e. after the port) I think we should make homs in concrete categories such as Type, TopCat, etc. into structures so lean doesn't get so easily confused about when something should be a morphism and when it should be a function/continuousMap

[Adam Topaz]

Well, it looks like we still have some linting errors. I think the simp lemmas around coercions to functions need to be shuffled a bit.