Class mixing algebra and topology

Stream: mathlib4

[Nailin Guan]

Hello, when I was working on isomorphism of topological groups, I was suggested not to mix class involving both algebra and topology, but then turn out that there are still things like this in mathlib, such as ContinuousSemiLinearEquivClassand ContinuousLinearEquivClass, I don't know if there are other things like this, should these be deprecated and reconstructed?

[Nailin Guan]

I was once suggested to add instance to these but I don't think working on a thing that should be reconstructed soon is very reasonable. Is anybody already working on it or about to work on it?

[Jireh Loreaux]

Your PR (#18689 for everyone else) is exactly the thing that allows us in the future to remove docs#ContinuousSemilinearEquivClass if we choose. Indeed, in order to separate the algebra and topology in that class you need both the algebra piece (docs#SemilinearEquivClass) and the topology piece (your HomeomorphClass).

However, the decision to remove that combined class should not be part of your current PR (just for separation of concerns). This is why I asked you to add the instance. Until we do decide to remove that class, we should have the relevant API, and introducing one instance does not create a lot of work, neither at the time of writing nor of removal.

[Jireh Loreaux]

To answer your question, nobody is working on it because HomeomorphClass doesn't exist yet.

[Nailin Guan]

I met problem after this: without these classes, the coersion to it may be a mess, for example ContinuousMulEquiv to ContinuousMonoidHom, the composition and inverse of it may be difficult or need a lot of lemma, is there any way to resolve this?

[Nailin Guan]

This was initially for dealing with category with morphisms ContinuousMonoidHom, but it turned out having some difficulty.

[Jireh Loreaux]

I'm not sure I understand the problem. Can you be more specific about the issues you are encountering? There are certainly well-known issues regarding composition of FunLike morphisms (i.e., you just can't without coercing), and inverses with EquivLike.

[Nailin Guan]

I mean in a category with morphisms ContinuousMonoidHom, going from ContinuousMulEquiv A B to Category.Iso A B is having some problem, as I don't want to unfold or ext when proving hom_inv_id and inv_hom_id

[Jireh Loreaux]

So you're having problems with concrete categories? I'm still not clear what your issue is. Can you provide a #mwe highlighting your problem please?

[Nailin Guan]

import Mathlib.Topology.Algebra.ContinuousMonoidHom
import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

namespace ContinuousMulEquiv

variable {U V : Type*} [TopologicalSpace U] [TopologicalSpace V] [Monoid U] [Monoid V]

/--The coercion from `ContinuousMulEquiv` to `ContinuousMonoidHom` induced by `toMonoidHom`-/

def toContinuousMonoidHom (f : U ≃ₜ* V) : ContinuousMonoidHom U V :=

{ f.toMonoidHom with
  continuous_toFun := f.continuous_toFun }

lemma toContinuousMonoidHom_toMonoidHom (f : U ≃ₜ* V) : f.toContinuousMonoidHom = f.toMonoidHom :=
  rfl

lemma toContinuousMonoidHom_toContinuousMap (f : U ≃ₜ* V) : f.toContinuousMonoidHom = toContinuousMap f :=
  rfl

example (P Q : ProfiniteGrp) (e : P ≃ₜ* Q) : P ≅ Q where
  hom := e.toContinuousMonoidHom
  inv := e.symm.toContinuousMonoidHom
  hom_inv_id := sorry
  inv_hom_id := sorry

end ContinuousMulEquiv

[Nailin Guan]

I can't prove the two sorry easily without using ext and show only using the lemmas above.

[Jireh Loreaux]

There are several issues with what you have:

1. You shouldn't be defining a coercion from the equiv to the hom. Instead you should define a coercion toContinuousMonoidHom assuming the two relevant hom classes.
2. Then, unless we're missing instances for ContinuousMulEquiv, you will simply be able to coerce directly.
3. You're using ProfiniteGrp, which is a category. You shouldn't be using type-level equivalences, as those act on the coercion to type of a ProfiniteGrp. Instead you should be using morphisms in the relevant category.

[Nailin Guan]

For 1, it's very resonable, thanks! For 2, I think when design, the classes are enough to pick up these. For 3, may I ask for a look at the end of my PR #16992, I am only wanting to make it a bit shorter by introduce the aux ContinuousMulEquiv, any suggestions about it? Thank you.

[Jireh Loreaux]

I think Kevin and I are saying the same thing. You should work at the category-theoretic level, not at the type level, and if you want, deduce the type level result from the categorical one.

As far as your problem on #16992, it seems to me like you want to use docs#CategoryTheory.Functor.ReflectsIsomorphisms to say that you've got this morphism in ProfiniteGrp, which, as a function, is a bijection (i.e., the image under the forgetful functor is an isomorphism in Type), and therefore the morphisms is an isomorphism of ProfiniteGrp. You should never need to explicitly prove the continuity of the inverse with this approach (nor indeed even construct the inverse).

[Nailin Guan]

I added toContinuousMonoidHom, I think I resolved all the problems for now, thanks.