Strict group homs are stable by `Prod.map`

[ADedecker]

Mathlib now has the definition Topology.IsStrictMap of topologically strict maps. In general, the product (in the sense of Prod.map) of two strict maps need not be strict. However, strict group homomorphisms satisfy this property.

I don't think we need a definition of strictness specific to group homs, but we definitely need some API :

• we should restate the definitions and characterizations in terms of MonoidHom.rangeRestrict, QuotientGroup.kerLift, and QuotientGroup.quotientKerEquivRange
• thanks to MonoidHom.isOpenQuotientMap_of_isQuotientMap, we can replace IsQuotientMap by IsOpenQuotientMap in this setting
• then, the result should follow from IsOpenQuotientMap.prodMap (which is false for general quotient maps) and Homeomorph.Set.prod (and maybe an extra lemma saying that strict maps stay strict when we compose them with homeomorphisms)

[ADedecker]

@zw810-ctrl If you want to keep playing with strict maps, this might interest you! If not no problem of course

[zw810-ctrl]

@zw810-ctrl If you want to keep playing with strict maps, this might interest you! If not no problem of course

Thanks for the ping! I'm definitely interested. I'll take this on!

[ADedecker]

@zw810-ctrl Hey! Two small questions:

• What's your username on Zulip? I tried to find you but couldn't 😅
• I didn't realize this when writing this issue, but we may want to work on Fredholm operators during an upcoming workshop at ICERM from May 11th to May 16th. Do you think you would have a PR by then? If not then that's no big deal, we can just sorry this part of the argument, but if you do that'd be perfect.

[zw810-ctrl]

@zw810-ctrl Hey! Two small questions:

• What's your username on Zulip? I tried to find you but couldn't 😅
• I didn't realize this when writing this issue, but we may want to work on Fredholm operators during an upcoming workshop at ICERM from May 11th to May 16th. Do you think you would have a PR by then? If not then that's no big deal, we can just sorry this part of the argument, but if you do that'd be perfect.

Sorry for the delay, I recently in the final week so it is really busy.

1, My Zulip user number is 1054067, the name is Calix Wei

2, Sure! I've actually completed the proofs, but I'm still figuring out if I should add more API and fixing the code style (though the proofs are done, I'm still a bit unsure about the dependency hierarchy of some definitions in Lean and am currently looking into it). But I can definitely submit a draft PR in the next couple of days!

[zw810-ctrl]

@ADedecker Hi! I recently updated my Mathlib and ran into a strange issue. The lemma isHomeomorph_iff_isQuotientMap_injective (from Mathlib.Topology.Homeomorph.Lemmas) seems to have disappeared in my local environment. However, I can still find it in the online Mathlib documentation. Has this lemma been recently moved？Should I try other way to prove?

theorem isStrictMap_iff_isHomeomorph_quotientKerEquivRange :
    IsStrictMap f ↔
      IsHomeomorph (Setoid.quotientKerEquivRange f : Quotient (Setoid.ker f) → Set.range f) := by
  simp only [IsStrictMap, isHomeomorph_iff_isQuotientMap_injective, Equiv.injective, and_true]
  exact ⟨fun h => IsQuotientMap.of_comp_isQuotientMap isQuotientMap_quotient_mk' h,
         fun h ↦ h.comp isQuotientMap_quotient_mk'⟩

[ADedecker]

@zw810-ctrl I don't think the lemma has been removed. Do you have a branch on your fork where I could see your problem ?

[zw810-ctrl]

@zw810-ctrl I don't think the lemma has been removed. Do you have a branch on your fork where I could see your problem ?

It's Ok I fix that now. See PR #38937